From 30986d7a3f5d496b208c89516cb5765a27ef9500 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Fri, 24 Jul 2026 15:05:09 +0000 Subject: [PATCH] feat: intrinsic verification syntax for do-notation loops and def contracts MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds intrinsic verification syntax for `Std.Internal.Do` do-notation: loop invariants and function contracts that `vcgen` discharges automatically. A `for x in xs invariant cur => I do …` loop annotates its invariant onto the loop combinator, elaborated in the loop body's scope so mutable variables and outer-loop variables resolve by name; nested loops are supported. A `def` may carry `require P` and `ensures b => Q` clauses on its signature, expanding to the plain definition plus an `@[spec]`-tagged specification theorem `f.spec : ⦃P⦄ f args ⦃fun b => Q⦄` proved by `vcgen [f] with finish`. --- src/Init/Control/Id.lean | 4 +- src/Lean/Elab/BuiltinDo/For.lean | 46 ++++- src/Lean/Elab/Do/InferControlInfo.lean | 2 +- src/Lean/Elab/Do/Legacy.lean | 6 +- src/Lean/Elab/Tactic/Do.lean | 1 + src/Lean/Elab/Tactic/Do/Contract.lean | 79 ++++++++ src/Lean/Parser/Basic.lean | 24 +++ src/Lean/Parser/Command.lean | 21 ++- src/Lean/Parser/Do.lean | 14 +- src/Lean/PrettyPrinter/Formatter.lean | 4 + src/Lean/PrettyPrinter/Parenthesizer.lean | 4 + src/Std/Do/Triple/SpecLemmas.lean | 4 + src/Std/Internal/Do.lean | 1 + src/Std/Internal/Do/Gadget/ForIn.lean | 169 ++++++++++++++++++ src/Std/Internal/Do/Triple/SpecLemmas.lean | 2 - tests/elab/doForInvariant.lean | 106 ----------- tests/elab/formatTerm.lean | 4 + tests/elab/formatTerm.lean.out.expected | 7 + tests/elab/intrinsicVerification.lean | 108 +++++++++++ .../intrinsicVerificationMissingImport.lean | 16 ++ .../partialSyntaxTraces.lean.out.expected | 8 + 21 files changed, 507 insertions(+), 123 deletions(-) create mode 100644 src/Lean/Elab/Tactic/Do/Contract.lean create mode 100644 src/Std/Internal/Do/Gadget/ForIn.lean delete mode 100644 tests/elab/doForInvariant.lean create mode 100644 tests/elab/intrinsicVerification.lean create mode 100644 tests/elab/intrinsicVerificationMissingImport.lean diff --git a/src/Init/Control/Id.lean b/src/Init/Control/Id.lean index d5d5f9265119..1fd3400c1fce 100644 --- a/src/Init/Control/Id.lean +++ b/src/Init/Control/Id.lean @@ -82,9 +82,9 @@ instance : LawfulMonadAttach Id where end Id /-- Turn a collection with a pure `ForIn` instance into an array. -/ -def ForIn.toArray {α : Type u} [inst : ForIn Id ρ α] (xs : ρ) : Array α := +@[expose] def ForIn.toArray {α : Type u} [inst : ForIn Id ρ α] (xs : ρ) : Array α := ForIn.forIn xs Array.empty (fun a acc => pure (.yield (acc.push a))) |> Id.run /-- Turn a collection with a pure `ForIn` instance into a list. -/ -def ForIn.toList {α : Type u} [ForIn Id ρ α] (xs : ρ) : List α := +@[expose] def ForIn.toList {α : Type u} [ForIn Id ρ α] (xs : ρ) : List α := ForIn.toArray xs |>.toList diff --git a/src/Lean/Elab/BuiltinDo/For.lean b/src/Lean/Elab/BuiltinDo/For.lean index 7e4c13368113..d0cf63b3f4e4 100644 --- a/src/Lean/Elab/BuiltinDo/For.lean +++ b/src/Lean/Elab/BuiltinDo/For.lean @@ -9,6 +9,7 @@ prelude public import Lean.Elab.BuiltinDo.Basic meta import Lean.Parser.Do import Init.Control.Do +import Init.While import Lean.Meta.ProdN public section @@ -20,10 +21,13 @@ open Lean.Meta @[builtin_macro Lean.Parser.Term.doFor] def expandDoFor : Macro := fun stx => do match stx with - | `(doFor| for $[$_ : ]? $_:ident in $_ do $_) => + | `(doFor| for $[$_ : ]? $_:ident in $_ $[$_inv:doForInvariant]? do $_) => -- This is the target form of the expander, handled by `elabDoFor` below. Macro.throwUnsupported - | `(doFor| for%$tk $decls:doForDecl,* do $body) => + | `(doFor| for%$tk $decls:doForDecl,* $[$inv:doForInvariant]? do $body) => + if let some inv := inv then + Macro.throwErrorAt inv "The `invariant` clause is only supported on `for x in xs do …` \ + with a single identifier binder." let decls := decls.getElems let `(doForDecl| $[$h? : ]? $pattern in $xs) := decls[0]! | Macro.throwUnsupported let mut doElems := #[] @@ -78,8 +82,40 @@ open Lean.Meta `(doElem| do $doElems*) | _ => Macro.throwUnsupported +/-- Rebuild the already-elaborated loop as a `forInWithInvariant` call carrying the `invariant` +clause: `ForIn.forInWithInvariant`, or `ForIn'.forInWithInvariant'` for a membership-proof binder +(`for h : x in xs`). The state tuple's layout is `[return?, mutVars…, unit?]`, so the invariant can +name the loop's mutable variables directly; the early-return slot becomes a wildcard. -/ +private def mkForInWithInvariant (invClause : Syntax) (h? : Option Syntax) + (xs preS body σ : Expr) (loopMutVars : Array MutVar) (returnsEarly : Bool) + (mi : MonadInfo) : DoElabM Expr := do + let `(doForInvariant| invariant $cursorBinders* => $invBody) := invClause | throwUnsupportedSyntax + let hole ← `(_) + let mut binders : Array Term := #[] + if returnsEarly then binders := binders.push hole + for mv in loopMutVars do binders := binders.push ⟨mv.ident.raw⟩ + if returnsEarly && loopMutVars.isEmpty then binders := binders.push hole + let statePat : Term ← match binders with + | #[] => `(_) + | #[b] => pure b + | _ => `(⟨$binders,*⟩) + let stateId := mkIdentFrom invClause (← mkFreshUserName `__s) + let invLam ← `(fun $cursorBinders* $stateId:ident => + match $stateId:ident with | $statePat => $invBody) + -- The `forInWithInvariant` gadgets live downstream of this module, so they are referenced by an + -- unresolved name that resolves in the user's context (which imports the metatheory). + let gadget := if h?.isSome then `Std.Internal.Do.ForIn'.forInWithInvariant' + else `Std.Internal.Do.ForIn.forInWithInvariant + unless (← getEnv).contains gadget do + throwErrorAt invClause + "the `invariant` clause elaborates to a `vcgen` gadget; add `import Std.Internal.Do` to use it." + let call ← `($(mkIdent gadget) + $(← Term.exprToSyntax xs) $(← Term.exprToSyntax preS) $(← Term.exprToSyntax body) $invLam) + Term.elabTermEnsuringType call (mkApp mi.m σ) + @[builtin_doElem_elab Lean.Parser.Term.doFor] def elabDoFor : DoElab := fun stx dec => do - let `(doFor| for%$tk $[$h? : ]? $x:ident in $xs do $body) := stx | throwUnsupportedSyntax + let `(doFor| for%$tk $[$h? : ]? $x:ident in $xs $[$inv?:doForInvariant]? do $body) := stx + | throwUnsupportedSyntax let dec ← dec.ensureUnitAt tk checkMutVarsForShadowing #[x] let uα ← mkFreshLevelMVar @@ -176,7 +212,9 @@ open Lean.Meta -- Elaborate the loop body, which must have result type `PUnit`, just like the whole `for` loop. elabDoSeq body { dec with k := continueCont, kind := .duplicable } - let forIn := mkApp app body + let forIn ← match inv? with + | none => pure (mkApp app body) + | some invClause => mkForInWithInvariant invClause h? xs preS body σ loopMutVars info.returnsEarly mi let γ := (← read).doBlockResultType let rest ← diff --git a/src/Lean/Elab/Do/InferControlInfo.lean b/src/Lean/Elab/Do/InferControlInfo.lean index 95a73b1bf28e..fece02f7c4fd 100644 --- a/src/Lean/Elab/Do/InferControlInfo.lean +++ b/src/Lean/Elab/Do/InferControlInfo.lean @@ -185,7 +185,7 @@ partial def ofElem (stx : DoElem) : TermElabM ControlInfo := do | `(doElem| unless $_ do $elseSeq) => ControlInfo.alternative {} <$> ofSeq elseSeq -- For/Repeat - | `(doElem| for $[$[$_ :]? $_ in $_],* do $bodySeq) => + | `(doElem| for $[$[$_ :]? $_ in $_],* $[$_:doForInvariant]? do $bodySeq) => let info ← ofSeq bodySeq return { info with -- keep only reassigns and returnsEarly numRegularExits := 1, diff --git a/src/Lean/Elab/Do/Legacy.lean b/src/Lean/Elab/Do/Legacy.lean index 9d7b9f53f68f..214a068c4348 100644 --- a/src/Lean/Elab/Do/Legacy.lean +++ b/src/Lean/Elab/Do/Legacy.lean @@ -1563,7 +1563,7 @@ mutual `doFor` is of the form ``` def doForDecl := leading_parser termParser >> " in " >> withForbidden "do" termParser - def doFor := leading_parser "for " >> sepBy1 doForDecl ", " >> "do " >> doSeq + def doFor := leading_parser "for " >> sepBy1 doForDecl ", " >> optional doForInvariant >> " do " >> doSeq ``` -/ partial def doForToCode (doFor : Syntax) (doElems : List Syntax) : M CodeBlock := do @@ -1593,7 +1593,7 @@ mutual let y := doForDecl[1] let ys := doForDecl[3] let doForDecls := doForDecls.eraseIdx 1 - let body := doFor[3] + let body := doFor[4] withFreshMacroScope do /- Recall that `@` (explicit) disables `coeAtOutParam`. We used `@` at `Stream` functions to make sure `resultIsOutParamSupport` is not used. -/ @@ -1612,7 +1612,7 @@ mutual let x := doForDecls[0]![1] withRef x <| checkNotShadowingMutable (← getPatternVarsEx x) let xs := doForDecls[0]![3] - let forElems := getDoSeqElems doFor[3] + let forElems := getDoSeqElems doFor[4] let forInBodyCodeBlock ← withFor (doSeqToCode forElems) let ⟨uvars, forInBody⟩ ← mkForInBody x forInBodyCodeBlock let ctx ← read diff --git a/src/Lean/Elab/Tactic/Do.lean b/src/Lean/Elab/Tactic/Do.lean index e5976f0efbe7..d7628ba0067a 100644 --- a/src/Lean/Elab/Tactic/Do.lean +++ b/src/Lean/Elab/Tactic/Do.lean @@ -9,6 +9,7 @@ prelude public import Lean.Elab.Tactic.Do.ProofMode public import Lean.Elab.Tactic.Do.Syntax public import Lean.Elab.Tactic.Do.Attr +public import Lean.Elab.Tactic.Do.Contract public import Lean.Elab.Tactic.Do.LetElim public import Lean.Elab.Tactic.Do.Spec public import Lean.Elab.Tactic.Do.VCGen diff --git a/src/Lean/Elab/Tactic/Do/Contract.lean b/src/Lean/Elab/Tactic/Do/Contract.lean new file mode 100644 index 000000000000..74e7d042ce0f --- /dev/null +++ b/src/Lean/Elab/Tactic/Do/Contract.lean @@ -0,0 +1,79 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sebastian Graf +-/ +module + +prelude +public import Std.Tactic.Do.Syntax +public import Std.Internal.Do +public import Lean.Elab.Util +import Lean.DocString.Extension +meta import Lean.Parser.Command +meta import Lean.Parser.Term +import Init.Syntax +import Init.Grind.Interactive + +/-! +# `require`/`ensures` contracts on `def` + +A definition carrying `require P` / `ensures b => Q` clauses expands to the plain definition plus a +`vcgen`-proven, `@[spec]`-tagged specification theorem `f.spec`. +-/ + +public section + +open Lean Lean.Parser.Command Std.Internal.Do Lean.Order + +namespace Lean.Elab.Tactic.Do + +/-- The identifiers bound by an explicit `(…)` binder, used to apply the definition in its spec. -/ +def contractBinderIdents (binder : Syntax) : Array Ident := + match binder with + | `(Lean.Parser.Term.bracketedBinderF| ($ids* $[: $_]? $(_annot?)?)) => + ids.filterMap fun b => if b.raw.isIdent then some ⟨b.raw⟩ else none + | _ => + if binder.isIdent then #[⟨binder⟩] else #[] + +/-- Expand a `def` carrying `require`/`ensures` clauses into the plain `def` plus a spec theorem +`@[spec] theorem f.spec : ⦃P⦄ f args ⦃fun b => Q⦄ := by vcgen [f] with finish`. -/ +@[builtin_macro Lean.Parser.Command.declaration] +def expandDefContract : Macro := fun stx => do + let decl := stx[1] + unless decl.isOfKind ``Lean.Parser.Command.definition do Macro.throwUnsupported + -- `definition = "def "(0) >> declId(1) >> optDeclSig(2) >> (declVal <|> contractDeclVal)(3) >> …` + -- `contractDeclVal = optional requireClause(0) >> optional ensuresClause(1) >> declVal(2)` + let val := decl[3] + unless val.isOfKind ``Lean.Parser.Command.contractDeclVal do Macro.throwUnsupported + let requireStx := val[0] + let ensuresStx := val[1] + -- Replace the contract-carrying value with its inner `declVal` so the `def` elaborates normally. + let cleanDeclaration := stx.setArg 1 (decl.setArg 3 val[2]) + if requireStx.isNone && ensuresStx.isNone then + return cleanDeclaration + unless (← Macro.hasDecl ``Std.Internal.Do.Triple) do + Macro.throwErrorAt (if requireStx.isNone then ensuresStx else requireStx) + "`require`/`ensures` contracts elaborate to a `vcgen`-proved specification theorem; \ +add `import Std.Internal.Do` and `import Std.Tactic.Do` to use them." + let sig := decl[2] + let fId : Ident := ⟨decl[1][0]⟩ + let specId := mkIdentFrom fId (fId.getId ++ `spec) + let sigBinders := sig[0].getArgs + let binders : TSyntaxArray [`ident, ``Lean.Parser.Term.hole, ``Lean.Parser.Term.bracketedBinder] := + sigBinders.map (⟨·⟩) + let args := sigBinders.flatMap contractBinderIdents + let pre : Term ← if requireStx.isNone then `(⊤) else + match requireStx[0] with + | `(requireClause| require $p) => pure p + | _ => Macro.throwUnsupported + let post : Term ← if ensuresStx.isNone then `(fun _ => ⊤) else + match ensuresStx[0] with + | `(ensuresClause| ensures $bs* => $q) => `(fun $bs* => $q) + | _ => Macro.throwUnsupported + let thm ← `(command| + @[spec] theorem $specId $binders* : ⦃ $pre ⦄ $fId $args* ⦃ $post ⦄ := by + vcgen [$fId:ident] with finish) + return mkNullNode #[cleanDeclaration, thm] + +end Lean.Elab.Tactic.Do diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index 56ad17794c0b..0e1351766482 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -1595,6 +1595,30 @@ This parser has the same arity as `p` - it just forwards the results of `p`. -/ (fun c => if c.forbiddenTks.contains tk then c else { c with forbiddenTks := c.forbiddenTks.push tk }) p +/-- Appends the tokens from `tks` missing from `init`; the tokens in `tks` must be distinct. -/ +private def mergeForbiddenTks (init tks : Array Token) : Array Token := Id.run do + -- Membership is tested on the prefix seeded from `init`, so the loop does not hold a second + -- reference to the original array while pushing. + let size := init.size + let mut ts := init + for tk in tks do + unless ts.any (· == tk) (stop := size) do + ts := ts.push tk + return ts + +/-- `withForbiddens(tks, p)` runs `p` with every token in `tks` treated as forbidden, i.e. the +combined effect of nesting `withForbidden` for each token (see `withForbidden`). The tokens in +`tks` must be distinct. + +This parser has the same arity as `p` - it just forwards the results of `p`. -/ +@[builtin_doc] def withForbiddens (tks : Array Token) (p : Parser) + (_h : tks.toList.Nodup := by decide) : Parser := + adaptCacheableContext (fun c => + if c.forbiddenTks.isEmpty then + { c with forbiddenTks := tks } + else + { c with forbiddenTks := mergeForbiddenTks c.forbiddenTks tks }) p + /-- `withoutForbidden(p)` runs `p` disabling the "forbidden token" (see `withForbidden`), if any. This is usually used by bracketing constructs like `(...)` because there is no parsing ambiguity inside these nested constructs. diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 593b92e505e0..22974b82c256 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -129,10 +129,20 @@ def declId := leading_parser -- @[builtin_doc] -- FIXME: suppress the hover def declSig := leading_parser many (ppSpace >> (Term.binderIdent <|> Term.bracketedBinder)) >> Term.typeSpec +/-- The `require P` precondition clause of a `def` contract. -/ +def requireClause := leading_parser + ppIndent (ppSpace >> nonReservedSymbol "require" >> ppSpace >> withForbidden "ensures" termParser) +/-- The `ensures b => Q` postcondition clause of a `def` contract, binding the result `b`. -/ +def ensuresClause := leading_parser + ppIndent (ppSpace >> nonReservedSymbol "ensures" >> Term.basicFun) +/-- The `: type` of a `def`. It may carry contract clauses, so we forbid `require`/`ensures` in the type. -/ +def defTypeSpec := withForbiddens #["require", "ensures"] Term.typeSpec /-- `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type` -/ -- @[builtin_doc] -- FIXME: suppress the hover def optDeclSig := leading_parser - many (ppSpace >> (Term.binderIdent <|> Term.bracketedBinder)) >> Term.optType + withForbiddens #["require", "ensures"] + (many (ppSpace >> (Term.binderIdent <|> Term.bracketedBinder))) >> + optional defTypeSpec /-- Right-hand side of a `:=` in a declaration, a term. -/ def declBody : Parser := /- @@ -184,6 +194,12 @@ def whereStructInst := leading_parser -- Issue #753 shows an example that fails to be parsed when we used `Term.whereDecls`. withAntiquot (mkAntiquot "declVal" decl_name% (isPseudoKind := true)) <| declValSimple <|> declValEqns <|> whereStructInst +/-- `require P`/`ensures b => Q` contract clauses followed by the value of a `def`. Tried only +after `declVal` fails, so contract-free definitions parse without probing for the clauses. +`withoutInfo` avoids collecting `declVal`'s tokens and kinds a second time at startup; they are +already registered through the `declVal` alternative of `definition`. -/ +def contractDeclVal := leading_parser + optional requireClause >> optional ensuresClause >> withoutInfo declVal def «abbrev» := leading_parser "abbrev " >> declId >> ppIndent optDeclSig >> declVal def derivingClass := leading_parser @@ -192,7 +208,8 @@ def derivingClasses := sepBy1 derivingClass ", " def optDefDeriving := optional (ppDedent ppLine >> atomic ("deriving " >> notSymbol "instance" >> notSymbol "noncomputable") >> derivingClasses) def definition := leading_parser - "def " >> recover declId skipUntilWsOrDelim >> ppIndent optDeclSig >> declVal >> optDefDeriving + "def " >> recover declId skipUntilWsOrDelim >> ppIndent optDeclSig >> + (declVal <|> contractDeclVal) >> optDefDeriving def «theorem» := leading_parser "theorem " >> recover declId skipUntilWsOrDelim >> ppIndent declSig >> declVal def «opaque» := leading_parser diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean index 9b887bf4c68b..0a763637d086 100644 --- a/src/Lean/Parser/Do.lean +++ b/src/Lean/Parser/Do.lean @@ -175,7 +175,15 @@ def doIfCond := @[builtin_doElem_parser] def doUnless := leading_parser "unless " >> withForbidden "do" termParser >> " do " >> doSeq def doForDecl := leading_parser - optional (atomic (ident >> " : ")) >> termParser >> " in " >> withForbidden "do" termParser + optional (atomic (ident >> " : ")) >> termParser >> " in " >> + withForbiddens #["do", "invariant"] termParser +/-- +The optional `invariant cur => e` clause of a `for` loop. The invariant annotates the loop so +`vcgen` reads it from the program, with `cur` bound to the iteration cursor and mutable variables +referenced by name. +-/ +def doForInvariant := leading_parser + ppSpace >> nonReservedSymbol "invariant" >> withForbidden "do" basicFun /-- `for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass. `break` and `continue` are supported inside `for` loops. @@ -184,7 +192,7 @@ until at least one of them is exhausted. The types of `e2` etc. must implement the `Std.ToStream` typeclass. -/ @[builtin_doElem_parser] def doFor := leading_parser - "for " >> sepBy1 doForDecl ", " >> " do " >> doSeq + "for " >> sepBy1 doForDecl ", " >> optional doForInvariant >> " do " >> doSeq def dependentParam := leading_parser atomic ("(" >> nonReservedSymbol "dependent") >> " := " >> @@ -334,7 +342,7 @@ They expand into `do unless ...`, `do for ...`, `do try ...`, and `do return ... @[builtin_term_parser] def termUnless := leading_parser "unless " >> withForbidden "do" termParser >> " do " >> doSeq @[builtin_term_parser] def termFor := leading_parser - "for " >> sepBy1 doForDecl ", " >> " do " >> doSeq + "for " >> sepBy1 doForDecl ", " >> optional doForInvariant >> " do " >> doSeq @[builtin_term_parser] def termTry := leading_parser "try " >> doSeq >> many (doCatch <|> doCatchMatch) >> optional doFinally /-- diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index 2067634ee568..cf52cecbaacd 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -346,6 +346,10 @@ def node.formatter (k : SyntaxNodeKind) (p : Formatter) : Formatter := do @[combinator_formatter withFn, expose] def withFn.formatter (_ : ParserFn → ParserFn) (p : Formatter) : Formatter := p +@[combinator_formatter withForbiddens, expose] +def withForbiddens.formatter (tks : Array Token) (p : Formatter) (_h : tks.toList.Nodup) : + Formatter := p + @[combinator_formatter trailingNode, expose] def trailingNode.formatter (k : SyntaxNodeKind) (_ _ : Nat) (p : Formatter) : Formatter := do checkKind k diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index e9738d1e854c..e16218c329e0 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -451,6 +451,10 @@ def checkPrec.parenthesizer (prec : Nat) : Parenthesizer := @[combinator_parenthesizer withFn, expose] def withFn.parenthesizer (_ : ParserFn → ParserFn) (p : Parenthesizer) : Parenthesizer := p +@[combinator_parenthesizer withForbiddens, expose] +def withForbiddens.parenthesizer (tks : Array Token) (p : Parenthesizer) + (_h : tks.toList.Nodup) : Parenthesizer := p + @[combinator_parenthesizer leadingNode, expose] def leadingNode.parenthesizer (k : SyntaxNodeKind) (prec : Nat) (p : Parenthesizer) : Parenthesizer := do node.parenthesizer k p diff --git a/src/Std/Do/Triple/SpecLemmas.lean b/src/Std/Do/Triple/SpecLemmas.lean index c5e7f1f70edd..0ce4289b1c46 100644 --- a/src/Std/Do/Triple/SpecLemmas.lean +++ b/src/Std/Do/Triple/SpecLemmas.lean @@ -75,6 +75,10 @@ structure Cursor {α : Type u} (l : List α) : Type u where /-- Appending the prefix to the suffix yields the original list. -/ property : «prefix» ++ suffix = l +/-- Transports a cursor along an equality of the list it ranges over. -/ +@[inline] def Cursor.cast {α} {l l' : List α} (c : Cursor l) (h : l = l') : Cursor l' := + ⟨c.prefix, c.suffix, h ▸ c.property⟩ + /-- Creates a cursor at position `n` in the list `l`. The prefix contains the first `n` elements, and the suffix contains the remaining elements. diff --git a/src/Std/Internal/Do.lean b/src/Std/Internal/Do.lean index 5d69a00a4298..c848a2e37dd0 100644 --- a/src/Std/Internal/Do.lean +++ b/src/Std/Internal/Do.lean @@ -8,3 +8,4 @@ module prelude public import Std.Internal.Do.WP public import Std.Internal.Do.Triple +public import Std.Internal.Do.Gadget.ForIn diff --git a/src/Std/Internal/Do/Gadget/ForIn.lean b/src/Std/Internal/Do/Gadget/ForIn.lean new file mode 100644 index 000000000000..371fa17078f4 --- /dev/null +++ b/src/Std/Internal/Do/Gadget/ForIn.lean @@ -0,0 +1,169 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sebastian Graf +-/ +module + +prelude +public import Std.Internal.Do.Triple.SpecLemmas +import Init.Data.Array.Bootstrap +import Init.Data.List.Monadic + +/-! +# `forIn` loop-invariant gadgets + +`ForIn.forInWithInvariant` and `ForIn'.forInWithInvariant'` annotate a `forIn`/`forIn'` loop with its +invariant so that `vcgen` reads the invariant from the program. The gadgets come first, then the +`@[spec]` specifications that restate `Spec.forIn_list`/`Spec.forIn'_list` for each container. +-/ + +@[expose] public section + +namespace Std.Internal.Do + +open Lean.Order + +universe u₁ u₂ v w +variable {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} + {Pred : Type (max u₁ u₂)} {EPred : Type (max u₁ u₂)} +variable [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] + +/-! ## Gadgets -/ + +set_option linter.unusedVariables false in +/-- A `forIn` loop annotated with its loop invariant, which `vcgen` reads from the `inv` argument. +It is definitionally `forIn xs init f`, so the annotation is erased at runtime. The invariant +ranges over the loop's iteration cursor, viewed through `ForIn.toList`. -/ +@[inline] def ForIn.forInWithInvariant {ρ : Type w} [ForIn m ρ α] [ForIn Id ρ α] (xs : ρ) (init : β) + (f : α → β → m (ForInStep β)) (inv : Invariant (ForIn.toList xs) β Pred) : m β := + forIn xs init f + +set_option linter.unusedVariables false in +/-- A membership-aware `forIn'` loop annotated with its loop invariant, which `vcgen` reads from the +`inv` argument. It is definitionally `forIn' xs init f`, so the annotation is erased at runtime. The +invariant ranges over the loop's iteration cursor, viewed through `ForIn.toList`. -/ +@[inline] def ForIn'.forInWithInvariant' {ρ : Type w} {d : Membership α ρ} [ForIn' m ρ α d] + [ForIn Id ρ α] (xs : ρ) (init : β) (f : (a : α) → a ∈ xs → β → m (ForInStep β)) + (inv : Invariant (ForIn.toList xs) β Pred) : m β := + forIn' xs init f + +/-! ## Bridge lemmas + +`ForIn.toList xs` unfolds to the concrete list of each container, so the specifications below can +present their cursors over that concrete list and keep `ForIn.toList` out of the verification +conditions. -/ + +private theorem foldl_push_toList {γ : Type u₁} (xs : List γ) (acc : Array γ) : + (xs.foldl (fun acc a => acc.push a) acc).toList = acc.toList ++ xs := by + induction xs generalizing acc with + | nil => simp + | cons a xs ih => rw [List.foldl_cons, ih, Array.toList_push]; simp + +theorem ForIn.toList_list {γ : Type u₁} (xs : List γ) : ForIn.toList xs = xs := by + simp only [ForIn.toList, ForIn.toArray, Id.run, List.forIn_pure_yield_eq_foldl] + change (List.foldl (fun acc a => acc.push a) #[] xs).toList = xs + rw [foldl_push_toList]; simp + +theorem ForIn.toList_range (r : Std.Legacy.Range) : ForIn.toList r = r.toList := by + simp only [ForIn.toList, ForIn.toArray, Id.run, Std.Legacy.Range.forIn_eq_forIn_range', + List.forIn_pure_yield_eq_foldl] + change (List.foldl (fun acc a => acc.push a) #[] + (List.range' r.start r.size r.step)).toList = r.toList + rw [foldl_push_toList]; simp [Std.Legacy.Range.toList, Std.Legacy.Range.size] + +/-! ## Specifications -/ + +@[spec] +theorem Spec.forInWithInvariant_list + {xs : List α} {init : β} {f : α → β → m (ForInStep β)} + (inv : Invariant (ForIn.toList xs) β Pred) + {epost : EPred} + (step : ∀ pref cur suff (h : xs = pref ++ cur :: suff) b, + Triple + (f cur b) + (inv ⟨pref, cur::suff, by simp [ForIn.toList_list, h]⟩ b) + (fun r => match r with + | .yield b' => inv ⟨pref ++ [cur], suff, by simp [ForIn.toList_list, h]⟩ b' + | .done b' => inv ⟨xs, [], by simp [ForIn.toList_list]⟩ b') + epost) : + Triple + (ForIn.forInWithInvariant xs init f inv) + (inv ⟨[], xs, by simp [ForIn.toList_list]⟩ init) + (fun b => inv ⟨xs, [], by simp [ForIn.toList_list]⟩ b) + epost := by + have key : ForIn.toList xs = xs := ForIn.toList_list xs + unfold ForIn.forInWithInvariant + exact Spec.forIn_list (inv := fun c b => inv (c.cast key.symm) b) step + +@[spec] +theorem Spec.forInWithInvariant_range {β : Type u} {m : Type u → Type v} {Pred EPred : Type u} + [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] + {xs : Std.Legacy.Range} {init : β} {f : Nat → β → m (ForInStep β)} + (inv : Invariant (ForIn.toList xs) β Pred) + {epost : EPred} + (step : ∀ pref cur suff (h : xs.toList = pref ++ cur :: suff) b, + Triple + (f cur b) + (inv ⟨pref, cur::suff, by simp [ForIn.toList_range, h]⟩ b) + (fun r => match r with + | .yield b' => inv ⟨pref ++ [cur], suff, by simp [ForIn.toList_range, h]⟩ b' + | .done b' => inv ⟨xs.toList, [], by simp [ForIn.toList_range]⟩ b') + epost) : + Triple + (ForIn.forInWithInvariant xs init f inv) + (inv ⟨[], xs.toList, by simp [ForIn.toList_range]⟩ init) + (fun b => inv ⟨xs.toList, [], by simp [ForIn.toList_range]⟩ b) + epost := by + have key : ForIn.toList xs = xs.toList := ForIn.toList_range xs + unfold ForIn.forInWithInvariant + rw [show (forIn xs init f : m β) = forIn xs.toList init f by + simp [Std.Legacy.Range.forIn_eq_forIn_range', Std.Legacy.Range.toList, Std.Legacy.Range.size]] + exact Spec.forIn_list (inv := fun c b => inv (c.cast key.symm) b) step + +@[spec] +theorem Spec.forInWithInvariant'_list + {xs : List α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} + (inv : Invariant (ForIn.toList xs) β Pred) + {epost : EPred} + (step : ∀ pref cur suff (h : xs = pref ++ cur :: suff) b, + Triple + (f cur (by simp [h]) b) + (inv ⟨pref, cur::suff, by simp [ForIn.toList_list, h]⟩ b) + (fun r => match r with + | .yield b' => inv ⟨pref ++ [cur], suff, by simp [ForIn.toList_list, h]⟩ b' + | .done b' => inv ⟨xs, [], by simp [ForIn.toList_list]⟩ b') + epost) : + Triple + (ForIn'.forInWithInvariant' xs init f inv) + (inv ⟨[], xs, by simp [ForIn.toList_list]⟩ init) + (fun b => inv ⟨xs, [], by simp [ForIn.toList_list]⟩ b) + epost := by + have key : ForIn.toList xs = xs := ForIn.toList_list xs + unfold ForIn'.forInWithInvariant' + exact Spec.forIn'_list (inv := fun c b => inv (c.cast key.symm) b) step + +@[spec] +theorem Spec.forInWithInvariant'_range {β : Type u} {m : Type u → Type v} {Pred EPred : Type u} + [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] + {xs : Std.Legacy.Range} {init : β} {f : (a : Nat) → a ∈ xs → β → m (ForInStep β)} + (inv : Invariant (ForIn.toList xs) β Pred) + {epost : EPred} + (step : ∀ pref cur suff (h : xs.toList = pref ++ cur :: suff) b, + Triple + (f cur (by simp [Std.Legacy.Range.mem_of_mem_range', h]) b) + (inv ⟨pref, cur::suff, by simp [ForIn.toList_range, h]⟩ b) + (fun r => match r with + | .yield b' => inv ⟨pref ++ [cur], suff, by simp [ForIn.toList_range, h]⟩ b' + | .done b' => inv ⟨xs.toList, [], by simp [ForIn.toList_range]⟩ b') + epost) : + Triple + (ForIn'.forInWithInvariant' xs init f inv) + (inv ⟨[], xs.toList, by simp [ForIn.toList_range]⟩ init) + (fun b => inv ⟨xs.toList, [], by simp [ForIn.toList_range]⟩ b) + epost := by + have key : ForIn.toList xs = xs.toList := ForIn.toList_range xs + unfold ForIn'.forInWithInvariant' + exact Spec.forIn'_range (inv := fun c b => inv (c.cast key.symm) b) step + +end Std.Internal.Do diff --git a/src/Std/Internal/Do/Triple/SpecLemmas.lean b/src/Std/Internal/Do/Triple/SpecLemmas.lean index 0f0a8216ceb7..e6ef9adc8a7a 100644 --- a/src/Std/Internal/Do/Triple/SpecLemmas.lean +++ b/src/Std/Internal/Do/Triple/SpecLemmas.lean @@ -720,8 +720,6 @@ theorem Spec.forIn_list simp only [← forIn'_eq_forIn] exact Spec.forIn'_list inv step - - theorem Spec.forIn_list_const_inv {xs : List α} {init : β} {f : α → β → m (ForInStep β)} {inv : (β → Pred)} diff --git a/tests/elab/doForInvariant.lean b/tests/elab/doForInvariant.lean deleted file mode 100644 index 28248b35a00c..000000000000 --- a/tests/elab/doForInvariant.lean +++ /dev/null @@ -1,106 +0,0 @@ -import Lean -import Std.Tactic.Do - -open Lean Parser Meta Elab Do - -set_option linter.unusedVariables false - -/-! -Hypothetical intrinsic invariant syntax support: --/ - -@[inline] -def ForIn.forInInv {m} {ρ : Type u} {α : Type v} [ForIn m ρ α] {β} - (xs : ρ) (s : β) (f : α → β → m (ForInStep β)) - [Monad m] [inst : ForIn.{u,v,v,v} Id ρ α] {ps} [Std.Do.WP m ps] (inv : Std.Do.Invariant (inst.toList xs) β ps) : m β := - forIn xs s f - -meta def doInvariant := leading_parser - "invariant " >> withPosition ( - ppGroup (many1 (ppSpace >> termParser argPrec) >> unicodeSymbol " ↦" " =>" (preserveForPP := true)) >> ppSpace >> withForbidden "do" termParser) -syntax (name := doForInvariant) "for " Term.doForDecl ppSpace doInvariant "do " doSeq : doElem - -elab_rules : doElem <= dec - | `(doElem| for $x:ident in $xs invariant $cursorBinder $stateBinders* => $body do $doSeq) => do - let call ← elabDoElem (← `(doElem| for $x:ident in $xs do $doSeq)) dec (catchExPostpone := false) - let_expr bind@Bind.bind m instBind σ γ call k := call - | throwError "Internal elaboration error: `for` loop did not elaborate to a call of `Bind.bind`; got {call}." - let_expr ForIn.forIn m ρ α instForIn σ xs s f := call - | throwError "Internal elaboration error: `for` loop bind argument did not elaborate to a call of `ForIn.forIn`; got {call}." - call.withApp fun head args => do - let [u, v, w, x] := head.constLevels! - | throwError "`Foldable.foldrEta` had wrong number of levels {head.constLevels!}" - let mi := (← read).monadInfo - unless ← isLevelDefEq mi.u (mkLevelMax v w) do - throwError "The universe level of the monadic result type {mi.u} was not the maximum of that of the state tuple {w} and elements {v}. Cannot elaborate invariants for this case." - unless ← isLevelDefEq mi.v x do - throwError "The universe level of the result type {mi.v} and that of the continuation result type {x} were different. Cannot elaborate invariants for this case." - -- First the non-ghost arguments - let instMonad ← Term.mkInstMVar (mkApp (mkConst ``Monad [mi.u, mi.v]) mi.m) - let app := mkConst ``ForIn.forInInv [u, v, w, x] - let app := mkApp5 app m ρ α instForIn σ - let app := mkApp3 app xs s f - -- Now the ghost arguments - let instForIn ← Term.mkInstMVar (mkApp3 (mkConst ``ForIn [u, v, v, v]) (mkConst ``Id [v]) ρ α) - let ps ← mkFreshExprMVar (mkConst ``Std.Do.PostShape [mi.u]) - let instWP ← Term.mkInstMVar (mkApp2 (mkConst ``Std.Do.WP [mi.u, mi.v]) (← read).monadInfo.m ps) - let xsToList := mkApp4 (mkConst ``ForIn.toList [u, v]) ρ α instForIn xs - let cursor := mkApp2 (mkConst ``List.Cursor [v]) α xsToList - let assertion := mkApp (mkConst ``Std.Do.Assertion [mi.u]) ps - let mut tuple := s - let mut reassignments := #[] - while !tuple.isAppOf ``PUnit.unit do - let (var, more) ← - if tuple.isAppOf ``Prod.mk then - let fst := tuple.getArg! 2 - tuple := tuple.getArg! 3 - pure (fst, true) - else - pure (tuple, false) - match var.fvarId? with - | none => -- Likely the return value slot. Push a wildcard - reassignments := reassignments.push (← `(_)) - | some fvarId => - let decl ← fvarId.getDecl - let .some mutVar := (← read).mutVars.find? (·.getId = decl.userName) | continue - reassignments := reassignments.push mutVar.ident - unless more do break - let mutVarBinders ← Term.Quotation.mkTuple reassignments - let cursorσ := mkApp2 (mkConst ``Prod [v, mi.u]) cursor σ - let success ← Term.elabFun (← `(fun ($cursorBinder, $(⟨mutVarBinders⟩)) $stateBinders* => $body)) (← mkArrow cursorσ assertion) - let inv := mkApp3 (mkConst ``Std.Do.PostCond.noThrow [mkLevelMax v mi.u]) cursorσ ps success - let forIn := mkApp5 app instMonad instForIn ps instWP inv - return mkApp6 bind m instBind σ γ forIn k - -/-- -info: (let x := 42; - let y := 0; - let z := 1; - do - let __s ← - ForIn.forInInv [1, 2, 3] (x, y) - (fun i __s => - let x := __s.fst; - let y := __s.snd; - let x := x + i; - let y := y + 7; - pure (ForInStep.yield (x, y))) - (PostCond.noThrow fun x => - match x with - | (xs, x, y) => ⌜xs.pos = 3 ∧ x = y + z⌝) - let x : Nat := __s.fst - let y : Nat := __s.snd - pure (x + y + z)).run : Nat --/ -#guard_msgs (info) in -open Std.Do in -#check Id.run do - let mut x := 42 - let mut y := 0 - let mut z := 1 - -- NB: `z` is constant in the invariant, so it will refer to the `let`. - -- In contrast, `x` and `y` will refer to lambda bound variables from the invariant. - for i in [1,2,3] invariant xs => ⌜xs.pos = 3 ∧ x = y + z⌝ do - x := x + i - y := y + 7 - return x + y + z diff --git a/tests/elab/formatTerm.lean b/tests/elab/formatTerm.lean index 3d2929ce387a..1376d2da2417 100644 --- a/tests/elab/formatTerm.lean +++ b/tests/elab/formatTerm.lean @@ -14,6 +14,10 @@ def fmt (stx : CoreM Syntax) : CoreM Format := do PrettyPrinter.ppTerm ⟨← st #eval fmt `(do let mut acc := 0; for x in xs do acc := acc + x; return acc) #eval fmt `(do while c do pure ()) #eval fmt `(do unless c do pure ()) +-- intrinsic-verification clauses: `invariant` inline with the loop, `require`/`ensures` inline with `def` +#eval fmt `(do for x in xs invariant cur => 0 ≤ acc do pure ()) +#eval fmt `(command| def clampLow (n lo : Nat) : Id Nat require lo ≤ n ensures r => r = n := pure n) +#eval fmt `(command| def g (x : Nat) require x > 0 ensures r => r ≥ x := pure x) #eval fmt `(def foo := by · skip; skip diff --git a/tests/elab/formatTerm.lean.out.expected b/tests/elab/formatTerm.lean.out.expected index cdedcc009a98..c00385266df5 100644 --- a/tests/elab/formatTerm.lean.out.expected +++ b/tests/elab/formatTerm.lean.out.expected @@ -46,6 +46,13 @@ do do unless c✝ do pure✝ () +do + for x✝ in xs✝ invariant cur✝ => 0 ≤ acc✝ do + pure✝ () +def clampLow✝ (n✝ lo✝ : Nat✝) : Id✝ Nat✝ require lo✝ ≤ n✝ ensures r✝ => r✝ = n✝ := + pure✝ n✝ +def g✝ (x✝ : Nat✝) require x✝ > 0 ensures r✝ => r✝ ≥ x✝ := + pure✝ x✝ def foo✝ := by · skip; skip · skip; skip diff --git a/tests/elab/intrinsicVerification.lean b/tests/elab/intrinsicVerification.lean new file mode 100644 index 000000000000..fc8b4a9e310d --- /dev/null +++ b/tests/elab/intrinsicVerification.lean @@ -0,0 +1,108 @@ +import Std.Internal.Do +import Std.Tactic.Do + +/-! Tests for `def` contracts. A `def` carrying `require`/`ensures` clauses elaborates to the +definition plus an `@[spec]`-tagged `f.spec` Hoare triple that `vcgen` proves automatically; a +`for … invariant` clause inside the body supplies the loop invariant it needs. New cases go here. -/ + +open Std.Internal.Do Lean.Order + +set_option mvcgen.warning false + +/-! ## An `ensures` contract with a `for … invariant` loop, proved with no manual steps -/ + +def findSmallest (s : Array Nat) : Id (Option Nat) + ensures r => match r with + | none => s.size = 0 + | some min => s.size > 0 ∧ (∃ i, i < s.size ∧ s[i]! = min) + ∧ (∀ j, j < s.size → min ≤ s[j]!) + := do + if s.size = 0 then + return none + else + let mut minIndex := 0 + for i in [1:s.size] + invariant xs => minIndex < s.size ∧ s[minIndex]! ≤ s[0]! ∧ + ∀ j, j ∈ xs.prefix → s[minIndex]! ≤ s[j]! + do + if s[i]! < s[minIndex]! then + minIndex := i + return some s[minIndex]! + +-- The contract synthesizes an `@[spec]`-tagged `findSmallest.spec` Hoare triple. +#guard_msgs (drop info) in +#check @findSmallest.spec + +/-! ## `require` + `ensures` -/ + +def clampLow (n lo : Nat) : Id Nat + require lo ≤ n + ensures r => r = n + := do return n + +#guard_msgs (drop info) in +#check @clampLow.spec + +/-! ## A contract over a membership-proof binder (`for h : x in xs invariant …`) -/ + +def sumWithMem (xs : List Nat) : Id Nat + ensures r => 0 ≤ r := do + let mut acc := 0 + for h : x in xs invariant cur => 0 ≤ acc do + acc := acc + x + return acc + +#guard_msgs (drop info) in +#check @sumWithMem.spec + +-- The membership binder also works over a legacy `Range`. +def sumRangeMem (n : Nat) : Id Nat + ensures r => 0 ≤ r := do + let mut acc := 0 + for h : i in [0:n] invariant cur => 0 ≤ acc do + acc := acc + i + return acc + +#guard_msgs (drop info) in +#check @sumRangeMem.spec + +/-! ## The contract telescope is transplanted faithfully to `f.spec` + +`f.spec` re-binds the definition's telescope verbatim, applies `f` to exactly the explicit arguments, +and uses `⊤` for an omitted `require`. These cover implicit, instance, strict-implicit, and autobound +binders, and a contract written without a `: type` ascription. -/ + +def specImplicit {α : Type} [Inhabited α] (x : α) (n : Nat) : Id α + require n > 0 + ensures r => r = x := + pure x + +/-- info: @specImplicit.spec : ∀ {α : Type} [inst : Inhabited α] (x : α) (n : Nat), ⦃ n > 0 ⦄ specImplicit x n ⦃ fun r => r = x ⦄ -/ +#guard_msgs in +#check @specImplicit.spec + +def specAutobound (v : Vector Nat n) : Id Nat + require n > 0 + ensures r => r = n := + pure v.size + +/-- info: @specAutobound.spec : ∀ {n : Nat} (v : Vector Nat n), ⦃ n > 0 ⦄ specAutobound v ⦃ fun r => r = n ⦄ -/ +#guard_msgs in +#check @specAutobound.spec + +def specStrict ⦃α : Type⦄ [Inhabited α] (x : α) : Id α + ensures r => r = x := + pure x + +/-- info: specStrict.spec : ∀ ⦃α : Type⦄ [inst : Inhabited α] (x : α), ⦃ ⊤ ⦄ specStrict x ⦃ fun r => r = x ⦄ -/ +#guard_msgs in +#check @specStrict.spec + +def specNoType (x : Nat) + require x > 0 + ensures r => r ≥ x := + (pure x : Id Nat) + +/-- info: specNoType.spec : ∀ (x : Nat), ⦃ x > 0 ⦄ specNoType x ⦃ fun r => r ≥ x ⦄ -/ +#guard_msgs in +#check @specNoType.spec diff --git a/tests/elab/intrinsicVerificationMissingImport.lean b/tests/elab/intrinsicVerificationMissingImport.lean new file mode 100644 index 000000000000..92876e5d2e2e --- /dev/null +++ b/tests/elab/intrinsicVerificationMissingImport.lean @@ -0,0 +1,16 @@ +/-! A `def` contract or a `for … invariant` clause used without the `Std` metatheory reports a +helpful error naming the missing import, rather than a downstream elaboration failure. -/ + +/-- +error: `require`/`ensures` contracts elaborate to a `vcgen`-proved specification theorem; add `import Std.Internal.Do` and `import Std.Tactic.Do` to use them. +-/ +#guard_msgs in +def f (x : Nat) : Id Nat require x > 0 ensures r => r ≥ x := pure x + +/-- error: the `invariant` clause elaborates to a `vcgen` gadget; add `import Std.Internal.Do` to use it. -/ +#guard_msgs in +def g (xs : List Nat) : Id Nat := do + let mut acc := 0 + for x in xs invariant cur => 0 ≤ acc do + acc := acc + x + return acc diff --git a/tests/elab_fail/partialSyntaxTraces.lean.out.expected b/tests/elab_fail/partialSyntaxTraces.lean.out.expected index cbcfe7e4faeb..67ae05315731 100644 --- a/tests/elab_fail/partialSyntaxTraces.lean.out.expected +++ b/tests/elab_fail/partialSyntaxTraces.lean.out.expected @@ -3,4 +3,12 @@ partialSyntaxTraces.lean:6:0: error: unexpected end of input; expected ':=', 'wh (Command.declaration (Command.declModifiers [] [] [] [] [] [] []) (Command.definition "def" (Command.declId `f []) (Command.optDeclSig [] []) (Command.whereStructInst ))) +[Elab.command] ✅️ [Error pretty printing syntax: parenthesize: uncaught backtrack exception. Falling back to raw printer.] + (Command.declaration + (Command.declModifiers [] [] [] [] [] [] []) + (Command.definition + "def" + (Command.declId `f []) + (Command.optDeclSig [] []) + (Command.contractDeclVal [] [] (Command.whereStructInst )))) [Elab.command] ✅️