From fbadfefb19f5834d9d7ad07d720ac001939c1817 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 9 Jan 2026 14:17:18 -0600 Subject: [PATCH 01/11] Add SpaceSepBy and SpacePrefixedBy constructs to DDM - Implemented SpaceSepBy, SpaceSepByNonEmpty, SpacePrefixedBy, SpacePrefixedByNonEmpty - Added support in AST, Parser, Format, Ion, Elab, and code generation - Updated SMT dialect to use new constructs, removing manual list categories - Simplified SMT dialect by eliminating IndexList, SMTSortList, TermList, etc. - All constructs parse elements with automatic whitespace handling - Formatting adds spaces between (SpaceSepBy) or before (SpacePrefixedBy) elements - Fixed unused variable warnings --- Strata/DDM/AST.lean | 12 ++ Strata/DDM/BuiltinDialects/Init.lean | 12 ++ Strata/DDM/Elab/Core.lean | 40 +++++ Strata/DDM/Elab/Tree.lean | 36 ++++ Strata/DDM/Format.lean | 20 +++ Strata/DDM/Integration/Lean/Gen.lean | 76 ++++++++ Strata/DDM/Integration/Lean/OfAstM.lean | 44 +++++ Strata/DDM/Integration/Lean/ToExpr.lean | 12 ++ Strata/DDM/Ion.lean | 54 +++++- Strata/DDM/Parser.lean | 93 +++++++++- Strata/DL/SMT/DDMTransform/Parse.lean | 189 ++++++-------------- Strata/DL/SMT/DDMTransform/Translate.lean | 80 +++------ StrataTest/Languages/B3/DDMFormatTests.lean | 4 + 13 files changed, 481 insertions(+), 191 deletions(-) diff --git a/Strata/DDM/AST.lean b/Strata/DDM/AST.lean index c8c46aeb8..e1053345d 100644 --- a/Strata/DDM/AST.lean +++ b/Strata/DDM/AST.lean @@ -168,6 +168,10 @@ inductive ArgF (α : Type) : Type where | option (ann : α) (l : Option (ArgF α)) | seq (ann : α) (l : Array (ArgF α)) | commaSepList (ann : α) (l : Array (ArgF α)) +| spaceSepList (ann : α) (l : Array (ArgF α)) +| spaceSepListNonEmpty (ann : α) (l : Array (ArgF α)) +| spacePrefixedList (ann : α) (l : Array (ArgF α)) +| spacePrefixedListNonEmpty (ann : α) (l : Array (ArgF α)) deriving Inhabited, Repr end @@ -193,6 +197,10 @@ def ArgF.ann {α : Type} : ArgF α → α | .option ann _ => ann | .seq ann _ => ann | .commaSepList ann _ => ann +| .spaceSepList ann _ => ann +| .spaceSepListNonEmpty ann _ => ann +| .spacePrefixedList ann _ => ann +| .spacePrefixedListNonEmpty ann _ => ann end @@ -1292,6 +1300,10 @@ partial def foldOverArgBindingSpecs {α β} | .option _ (some a) => foldOverArgBindingSpecs m f init a | .seq _ a => a.attach.foldl (init := init) fun init ⟨a, _⟩ => foldOverArgBindingSpecs m f init a | .commaSepList _ a => a.attach.foldl (init := init) fun init ⟨a, _⟩ => foldOverArgBindingSpecs m f init a + | .spaceSepList _ a => a.attach.foldl (init := init) fun init ⟨a, _⟩ => foldOverArgBindingSpecs m f init a + | .spaceSepListNonEmpty _ a => a.attach.foldl (init := init) fun init ⟨a, _⟩ => foldOverArgBindingSpecs m f init a + | .spacePrefixedList _ a => a.attach.foldl (init := init) fun init ⟨a, _⟩ => foldOverArgBindingSpecs m f init a + | .spacePrefixedListNonEmpty _ a => a.attach.foldl (init := init) fun init ⟨a, _⟩ => foldOverArgBindingSpecs m f init a /-- Invoke a function `f` over each of the declaration specifications for an operator. diff --git a/Strata/DDM/BuiltinDialects/Init.lean b/Strata/DDM/BuiltinDialects/Init.lean index 1bd9bbe8c..0ce2ddcf0 100644 --- a/Strata/DDM/BuiltinDialects/Init.lean +++ b/Strata/DDM/BuiltinDialects/Init.lean @@ -18,6 +18,10 @@ namespace Strata def SyntaxCat.mkOpt (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.Option, args := #[c] } def SyntaxCat.mkSeq (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.Seq, args := #[c] } def SyntaxCat.mkCommaSepBy (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.CommaSepBy, args := #[c] } +def SyntaxCat.mkSpaceSepBy (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.SpaceSepBy, args := #[c] } +def SyntaxCat.mkSpaceSepByNonEmpty (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.SpaceSepByNonEmpty, args := #[c] } +def SyntaxCat.mkSpacePrefixedBy (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.SpacePrefixedBy, args := #[c] } +def SyntaxCat.mkSpacePrefixedByNonEmpty (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.SpacePrefixedByNonEmpty, args := #[c] } def initDialect : Dialect := BuiltinM.create! "Init" #[] do let Ident : ArgDeclKind := .cat <| .atom .none q`Init.Ident @@ -50,6 +54,14 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do declareCat q`Init.CommaSepBy #["a"] + declareCat q`Init.SpaceSepBy #["a"] + + declareCat q`Init.SpaceSepByNonEmpty #["a"] + + declareCat q`Init.SpacePrefixedBy #["a"] + + declareCat q`Init.SpacePrefixedByNonEmpty #["a"] + let QualifiedIdent := q`Init.QualifiedIdent declareCat QualifiedIdent declareOp { diff --git a/Strata/DDM/Elab/Core.lean b/Strata/DDM/Elab/Core.lean index cda280d03..f1dc9bfa9 100644 --- a/Strata/DDM/Elab/Core.lean +++ b/Strata/DDM/Elab/Core.lean @@ -1123,6 +1123,46 @@ partial def catElaborator (c : SyntaxCat) : TypingContext → Syntax → ElabM T let (args, resultCtx) ← stx.getSepArgs.foldlM f (#[], tctx) let info : CommaSepInfo := { inputCtx := tctx, loc := loc, args := args.map (·.arg), resultCtx } pure <| .node (.ofCommaSepInfo info) args + | q`Init.SpaceSepBy => + assert! c.args.size = 1 + let a := c.args[0]! + let f := elabManyElement (catElaborator a) + fun tctx stx => do + let some loc := mkSourceRange? stx + | panic! s!"spaceSepBy missing source location {repr stx}" + let (args, resultCtx) ← stx.getSepArgs.foldlM f (#[], tctx) + let info : SpaceSepInfo := { inputCtx := tctx, loc := loc, args := args.map (·.arg), resultCtx } + pure <| .node (.ofSpaceSepInfo info) args + | q`Init.SpaceSepByNonEmpty => + assert! c.args.size = 1 + let a := c.args[0]! + let f := elabManyElement (catElaborator a) + fun tctx stx => do + let some loc := mkSourceRange? stx + | panic! s!"spaceSepByNonEmpty missing source location {repr stx}" + let (args, resultCtx) ← stx.getSepArgs.foldlM f (#[], tctx) + let info : SpaceSepNonEmptyInfo := { inputCtx := tctx, loc := loc, args := args.map (·.arg), resultCtx } + pure <| .node (.ofSpaceSepNonEmptyInfo info) args + | q`Init.SpacePrefixedBy => + assert! c.args.size = 1 + let a := c.args[0]! + let f := elabManyElement (catElaborator a) + fun tctx stx => do + let some loc := mkSourceRange? stx + | panic! s!"spacePrefixedBy missing source location {repr stx}" + let (args, resultCtx) ← stx.getArgs.foldlM f (#[], tctx) + let info : SpacePrefixedInfo := { inputCtx := tctx, loc := loc, args := args.map (·.arg), resultCtx } + pure <| .node (.ofSpacePrefixedInfo info) args + | q`Init.SpacePrefixedByNonEmpty => + assert! c.args.size = 1 + let a := c.args[0]! + let f := elabManyElement (catElaborator a) + fun tctx stx => do + let some loc := mkSourceRange? stx + | panic! s!"spacePrefixedByNonEmpty missing source location {repr stx}" + let (args, resultCtx) ← stx.getArgs.foldlM f (#[], tctx) + let info : SpacePrefixedNonEmptyInfo := { inputCtx := tctx, loc := loc, args := args.map (·.arg), resultCtx } + pure <| .node (.ofSpacePrefixedNonEmptyInfo info) args | _ => assert! c.args.isEmpty elabOperation diff --git a/Strata/DDM/Elab/Tree.lean b/Strata/DDM/Elab/Tree.lean index 46dbf0601..9d9f86e57 100644 --- a/Strata/DDM/Elab/Tree.lean +++ b/Strata/DDM/Elab/Tree.lean @@ -246,6 +246,26 @@ structure CommaSepInfo extends ElabInfo where resultCtx : TypingContext deriving Inhabited, Repr +structure SpaceSepInfo extends ElabInfo where + args : Array Arg + resultCtx : TypingContext +deriving Inhabited, Repr + +structure SpaceSepNonEmptyInfo extends ElabInfo where + args : Array Arg + resultCtx : TypingContext +deriving Inhabited, Repr + +structure SpacePrefixedInfo extends ElabInfo where + args : Array Arg + resultCtx : TypingContext +deriving Inhabited, Repr + +structure SpacePrefixedNonEmptyInfo extends ElabInfo where + args : Array Arg + resultCtx : TypingContext +deriving Inhabited, Repr + inductive Info | ofOperationInfo (info : OperationInfo) | ofCatInfo (info : CatInfo) @@ -259,6 +279,10 @@ inductive Info | ofOptionInfo (info : OptionInfo) | ofSeqInfo (info : SeqInfo) | ofCommaSepInfo (info : CommaSepInfo) +| ofSpaceSepInfo (info : SpaceSepInfo) +| ofSpaceSepNonEmptyInfo (info : SpaceSepNonEmptyInfo) +| ofSpacePrefixedInfo (info : SpacePrefixedInfo) +| ofSpacePrefixedNonEmptyInfo (info : SpacePrefixedNonEmptyInfo) deriving Inhabited, Repr namespace Info @@ -293,6 +317,10 @@ def elabInfo (info : Info) : ElabInfo := | .ofOptionInfo info => info.toElabInfo | .ofSeqInfo info => info.toElabInfo | .ofCommaSepInfo info => info.toElabInfo + | .ofSpaceSepInfo info => info.toElabInfo + | .ofSpaceSepNonEmptyInfo info => info.toElabInfo + | .ofSpacePrefixedInfo info => info.toElabInfo + | .ofSpacePrefixedNonEmptyInfo info => info.toElabInfo def inputCtx (info : Info) : TypingContext := info.elabInfo.inputCtx @@ -340,6 +368,10 @@ def arg : Tree → Arg .option info.loc r | .ofSeqInfo info => .seq info.loc info.args | .ofCommaSepInfo info => .commaSepList info.loc info.args + | .ofSpaceSepInfo info => .spaceSepList info.loc info.args + | .ofSpaceSepNonEmptyInfo info => .spaceSepListNonEmpty info.loc info.args + | .ofSpacePrefixedInfo info => .spacePrefixedList info.loc info.args + | .ofSpacePrefixedNonEmptyInfo info => .spacePrefixedListNonEmpty info.loc info.args theorem sizeOf_children (t : Tree) (i : Nat) (p : i < t.children.size) : sizeOf t[i] < sizeOf t := by match t with @@ -362,6 +394,10 @@ def resultContext (t : Tree) : TypingContext := info.inputCtx | .ofSeqInfo info => info.resultCtx | .ofCommaSepInfo info => info.resultCtx + | .ofSpaceSepInfo info => info.resultCtx + | .ofSpaceSepNonEmptyInfo info => info.resultCtx + | .ofSpacePrefixedInfo info => info.resultCtx + | .ofSpacePrefixedNonEmptyInfo info => info.resultCtx termination_by t def isSpecificOp (tree : Tree) (expected : QualifiedIdent) : Bool := diff --git a/Strata/DDM/Format.lean b/Strata/DDM/Format.lean index b44486407..e3ef03abe 100644 --- a/Strata/DDM/Format.lean +++ b/Strata/DDM/Format.lean @@ -388,6 +388,26 @@ private partial def ArgF.mformatM {α} : ArgF α → FormatM PrecFormat let f i q s := return s ++ ", " ++ (← entries[i].mformatM).format let a := (← entries[0].mformatM).format .atom <$> entries.size.foldlM f (start := 1) a +| .spaceSepList _ entries => do + if z : entries.size = 0 then + pure (.atom .nil) + else do + let f i q s := return s ++ " " ++ (← entries[i].mformatM).format + let a := (← entries[0].mformatM).format + .atom <$> entries.size.foldlM f (start := 1) a +| .spaceSepListNonEmpty _ entries => do + if z : entries.size = 0 then + pure (.atom .nil) + else do + let f i q s := return s ++ " " ++ (← entries[i].mformatM).format + let a := (← entries[0].mformatM).format + .atom <$> entries.size.foldlM f (start := 1) a +| .spacePrefixedList _ entries => do + .atom <$> entries.foldlM (init := .nil) fun p a => + return (p ++ " " ++ (← a.mformatM).format) +| .spacePrefixedListNonEmpty _ entries => do + .atom <$> entries.foldlM (init := .nil) fun p a => + return (p ++ " " ++ (← a.mformatM).format) private partial def ppArgs (f : StrataFormat) (rargs : Array Arg) : FormatM PrecFormat := if rargs.isEmpty then diff --git a/Strata/DDM/Integration/Lean/Gen.lean b/Strata/DDM/Integration/Lean/Gen.lean index 5a2339964..ec694ec67 100644 --- a/Strata/DDM/Integration/Lean/Gen.lean +++ b/Strata/DDM/Integration/Lean/Gen.lean @@ -573,6 +573,14 @@ partial def ppCatWithUnwrap (annType : Ident) (c : SyntaxCat) (unwrap : Bool) : match c.name, eq : args.size with | q`Init.CommaSepBy, 1 => return mkCApp ``Ann #[mkCApp ``Array #[args[0]], annType] + | q`Init.SpaceSepBy, 1 => + return mkCApp ``Ann #[mkCApp ``Array #[args[0]], annType] + | q`Init.SpaceSepByNonEmpty, 1 => + return mkCApp ``Ann #[mkCApp ``Array #[args[0]], annType] + | q`Init.SpacePrefixedBy, 1 => + return mkCApp ``Ann #[mkCApp ``Array #[args[0]], annType] + | q`Init.SpacePrefixedByNonEmpty, 1 => + return mkCApp ``Ann #[mkCApp ``Array #[args[0]], annType] | q`Init.Option, 1 => return mkCApp ``Ann #[mkCApp ``Option #[args[0]], annType] | q`Init.Seq, 1 => @@ -741,6 +749,50 @@ partial def toAstApplyArg (vn : Name) (cat : SyntaxCat) (unwrap : Bool := false) mkCApp ``Array.attach #[mkCApp ``Ann.val #[v]] ] return mkAnnWithTerm ``ArgF.commaSepList v args + | q`Init.SpaceSepBy => do + assert! cat.args.size = 1 + let c := cat.args[0]! + let e ← genFreshLeanName "e" + let canE ← genIdentFrom e (canonical := true) + let t ← toAstApplyArg e c + let args := mkCApp ``Array.map #[ + ←`(fun ⟨$canE, _⟩ => $t), + mkCApp ``Array.attach #[mkCApp ``Ann.val #[v]] + ] + return mkAnnWithTerm ``ArgF.spaceSepList v args + | q`Init.SpaceSepByNonEmpty => do + assert! cat.args.size = 1 + let c := cat.args[0]! + let e ← genFreshLeanName "e" + let canE ← genIdentFrom e (canonical := true) + let t ← toAstApplyArg e c + let args := mkCApp ``Array.map #[ + ←`(fun ⟨$canE, _⟩ => $t), + mkCApp ``Array.attach #[mkCApp ``Ann.val #[v]] + ] + return mkAnnWithTerm ``ArgF.spaceSepListNonEmpty v args + | q`Init.SpacePrefixedBy => do + assert! cat.args.size = 1 + let c := cat.args[0]! + let e ← genFreshLeanName "e" + let canE ← genIdentFrom e (canonical := true) + let t ← toAstApplyArg e c + let args := mkCApp ``Array.map #[ + ←`(fun ⟨$canE, _⟩ => $t), + mkCApp ``Array.attach #[mkCApp ``Ann.val #[v]] + ] + return mkAnnWithTerm ``ArgF.spacePrefixedList v args + | q`Init.SpacePrefixedByNonEmpty => do + assert! cat.args.size = 1 + let c := cat.args[0]! + let e ← genFreshLeanName "e" + let canE ← genIdentFrom e (canonical := true) + let t ← toAstApplyArg e c + let args := mkCApp ``Array.map #[ + ←`(fun ⟨$canE, _⟩ => $t), + mkCApp ``Array.attach #[mkCApp ``Ann.val #[v]] + ] + return mkAnnWithTerm ``ArgF.spacePrefixedListNonEmpty v args | q`Init.Option => do assert! cat.args.size = 1 let c := cat.args[0]! @@ -912,6 +964,26 @@ partial def getOfIdentArgWithUnwrap (varName : String) (cat : SyntaxCat) (unwrap let (vc, vi) ← genFreshIdentPair varName let body ← getOfIdentArg varName c vi ``(OfAstM.ofCommaSepByM $e fun $vc _ => $body) + | q`Init.SpaceSepBy => do + let c := cat.args[0]! + let (vc, vi) ← genFreshIdentPair varName + let body ← getOfIdentArg varName c vi + ``(OfAstM.ofSpaceSepByM $e fun $vc _ => $body) + | q`Init.SpaceSepByNonEmpty => do + let c := cat.args[0]! + let (vc, vi) ← genFreshIdentPair varName + let body ← getOfIdentArg varName c vi + ``(OfAstM.ofSpaceSepByNonEmptyM $e fun $vc _ => $body) + | q`Init.SpacePrefixedBy => do + let c := cat.args[0]! + let (vc, vi) ← genFreshIdentPair varName + let body ← getOfIdentArg varName c vi + ``(OfAstM.ofSpacePrefixedByM $e fun $vc _ => $body) + | q`Init.SpacePrefixedByNonEmpty => do + let c := cat.args[0]! + let (vc, vi) ← genFreshIdentPair varName + let body ← getOfIdentArg varName c vi + ``(OfAstM.ofSpacePrefixedByNonEmptyM $e fun $vc _ => $body) | q`Init.Option => do let c := cat.args[0]! let (vc, vi) ← genFreshIdentPair varName @@ -1102,6 +1174,10 @@ def checkInhabited (cat : QualifiedIdent) (ops : Array DefaultCtor) : StateT Inh match arg.cat.name with | q`Init.Seq => true | q`Init.CommaSepBy => true + | q`Init.SpaceSepBy => true + | q`Init.SpaceSepByNonEmpty => true + | q`Init.SpacePrefixedBy => true + | q`Init.SpacePrefixedByNonEmpty => true | q`Init.Option => true | c => c ∈ inhabited if !isInhabited then diff --git a/Strata/DDM/Integration/Lean/OfAstM.lean b/Strata/DDM/Integration/Lean/OfAstM.lean index 58f85370d..cece63ac4 100644 --- a/Strata/DDM/Integration/Lean/OfAstM.lean +++ b/Strata/DDM/Integration/Lean/OfAstM.lean @@ -188,6 +188,50 @@ def ofSeqM {α β} [Repr α] [SizeOf α] pure { ann := ann, val := val } | _ => throwExpected "seq" arg +def ofSpaceSepByM {α β} [Repr α] [SizeOf α] + (arg : ArgF α) + (act : ∀(e : ArgF α), sizeOf e < sizeOf arg → OfAstM β) + : OfAstM (Ann (Array β) α) := + match arg with + | .spaceSepList ann a => do + let val ← a.attach.mapM fun ⟨v, vIn⟩ => + act v (by decreasing_tactic) + pure { ann := ann, val := val } + | _ => throwExpected "spaceSepBy" arg + +def ofSpaceSepByNonEmptyM {α β} [Repr α] [SizeOf α] + (arg : ArgF α) + (act : ∀(e : ArgF α), sizeOf e < sizeOf arg → OfAstM β) + : OfAstM (Ann (Array β) α) := + match arg with + | .spaceSepListNonEmpty ann a => do + let val ← a.attach.mapM fun ⟨v, vIn⟩ => + act v (by decreasing_tactic) + pure { ann := ann, val := val } + | _ => throwExpected "spaceSepByNonEmpty" arg + +def ofSpacePrefixedByM {α β} [Repr α] [SizeOf α] + (arg : ArgF α) + (act : ∀(e : ArgF α), sizeOf e < sizeOf arg → OfAstM β) + : OfAstM (Ann (Array β) α) := + match arg with + | .spacePrefixedList ann a => do + let val ← a.attach.mapM fun ⟨v, vIn⟩ => + act v (by decreasing_tactic) + pure { ann := ann, val := val } + | _ => throwExpected "spacePrefixedBy" arg + +def ofSpacePrefixedByNonEmptyM {α β} [Repr α] [SizeOf α] + (arg : ArgF α) + (act : ∀(e : ArgF α), sizeOf e < sizeOf arg → OfAstM β) + : OfAstM (Ann (Array β) α) := + match arg with + | .spacePrefixedListNonEmpty ann a => do + let val ← a.attach.mapM fun ⟨v, vIn⟩ => + act v (by decreasing_tactic) + pure { ann := ann, val := val } + | _ => throwExpected "spacePrefixedByNonEmpty" arg + /-- Get the expression at index `lvl` in the arguments. diff --git a/Strata/DDM/Integration/Lean/ToExpr.lean b/Strata/DDM/Integration/Lean/ToExpr.lean index 9a1d96f4e..625a3a58a 100644 --- a/Strata/DDM/Integration/Lean/ToExpr.lean +++ b/Strata/DDM/Integration/Lean/ToExpr.lean @@ -165,6 +165,18 @@ private def ArgF.toExpr {α} [ToExpr α] : ArgF α → Lean.Expr | .commaSepList ann a => let tpe := ArgF.typeExpr α astAnnExpr! ArgF.commaSepList ann <| arrayToExpr .zero tpe <| a.map (·.toExpr) +| .spaceSepList ann a => + let tpe := ArgF.typeExpr α + astAnnExpr! ArgF.spaceSepList ann <| arrayToExpr .zero tpe <| a.map (·.toExpr) +| .spaceSepListNonEmpty ann a => + let tpe := ArgF.typeExpr α + astAnnExpr! ArgF.spaceSepListNonEmpty ann <| arrayToExpr .zero tpe <| a.map (·.toExpr) +| .spacePrefixedList ann a => + let tpe := ArgF.typeExpr α + astAnnExpr! ArgF.spacePrefixedList ann <| arrayToExpr .zero tpe <| a.map (·.toExpr) +| .spacePrefixedListNonEmpty ann a => + let tpe := ArgF.typeExpr α + astAnnExpr! ArgF.spacePrefixedListNonEmpty ann <| arrayToExpr .zero tpe <| a.map (·.toExpr) termination_by a => sizeOf a private protected def OperationF.toExpr {α} [ToExpr α] (op : OperationF α) : Lean.Expr := diff --git a/Strata/DDM/Ion.lean b/Strata/DDM/Ion.lean index b691d2e29..53b71457b 100644 --- a/Strata/DDM/Ion.lean +++ b/Strata/DDM/Ion.lean @@ -513,13 +513,25 @@ private protected def ArgF.toIon {α} [ToIon α] (refs : SymbolIdCache) (arg : A let args : Array (Ion _) := #[ ionSymbol! "commaSepList", ← toIon ann ] let args ← l.attach.mapM_off (init := args) fun ⟨v, _⟩ => v.toIon refs return .sexp args + | .spaceSepList ann l => do + let args : Array (Ion _) := #[ ionSymbol! "spaceSepList", ← toIon ann ] + let args ← l.attach.mapM_off (init := args) fun ⟨v, _h⟩ => v.toIon refs + return .sexp args + | .spaceSepListNonEmpty ann l => do + let args : Array (Ion _) := #[ ionSymbol! "spaceSepListNonEmpty", ← toIon ann ] + let args ← l.attach.mapM_off (init := args) fun ⟨v, _h⟩ => v.toIon refs + return .sexp args + | .spacePrefixedList ann l => do + let args : Array (Ion _) := #[ ionSymbol! "spacePrefixedList", ← toIon ann ] + let args ← l.attach.mapM_off (init := args) fun ⟨v, _h⟩ => v.toIon refs + return .sexp args + | .spacePrefixedListNonEmpty ann l => do + let args : Array (Ion _) := #[ ionSymbol! "spacePrefixedListNonEmpty", ← toIon ann ] + let args ← l.attach.mapM_off (init := args) fun ⟨v, _h⟩ => v.toIon refs + return .sexp args termination_by sizeOf arg decreasing_by - · decreasing_tactic - · decreasing_tactic - · decreasing_tactic - · decreasing_tactic - · decreasing_tactic + all_goals decreasing_tactic end @@ -629,6 +641,30 @@ private protected def ArgF.fromIon {α} [FromIon α] (v : Ion SymbolId) : FromIo let args ← sexp.attach.mapM_off (start := 2) fun ⟨u, _⟩ => Strata.ArgF.fromIon u return .commaSepList ann args + | "spaceSepList" => do + let ⟨p⟩ ← .checkArgMin "spaceSepList" sexp 2 + let ann ← fromIon sexp[1] + let args ← sexp.attach.mapM_off (start := 2) fun ⟨u, _⟩ => + Strata.ArgF.fromIon u + return .spaceSepList ann args + | "spaceSepListNonEmpty" => do + let ⟨p⟩ ← .checkArgMin "spaceSepListNonEmpty" sexp 2 + let ann ← fromIon sexp[1] + let args ← sexp.attach.mapM_off (start := 2) fun ⟨u, _⟩ => + Strata.ArgF.fromIon u + return .spaceSepListNonEmpty ann args + | "spacePrefixedList" => do + let ⟨p⟩ ← .checkArgMin "spacePrefixedList" sexp 2 + let ann ← fromIon sexp[1] + let args ← sexp.attach.mapM_off (start := 2) fun ⟨u, _⟩ => + Strata.ArgF.fromIon u + return .spacePrefixedList ann args + | "spacePrefixedListNonEmpty" => do + let ⟨p⟩ ← .checkArgMin "spacePrefixedListNonEmpty" sexp 2 + let ann ← fromIon sexp[1] + let args ← sexp.attach.mapM_off (start := 2) fun ⟨u, _⟩ => + Strata.ArgF.fromIon u + return .spacePrefixedListNonEmpty ann args | str => throw s!"Unexpected identifier {str}" termination_by v @@ -643,6 +679,14 @@ decreasing_by decreasing_tactic · have _ : sizeOf u < sizeOf sexp := by decreasing_tactic decreasing_tactic + · have _ : sizeOf u < sizeOf sexp := by decreasing_tactic + decreasing_tactic + · have _ : sizeOf u < sizeOf sexp := by decreasing_tactic + decreasing_tactic + · have _ : sizeOf u < sizeOf sexp := by decreasing_tactic + decreasing_tactic + · have _ : sizeOf u < sizeOf sexp := by decreasing_tactic + decreasing_tactic end diff --git a/Strata/DDM/Parser.lean b/Strata/DDM/Parser.lean index 7f9e81112..146586b42 100644 --- a/Strata/DDM/Parser.lean +++ b/Strata/DDM/Parser.lean @@ -775,6 +775,13 @@ def checkLeftRec (thisCatName : QualifiedIdent) (argDecls : ArgDecls) (as : List .invalid mf!"Leading symbol cannot be recursive call to {c}" else .isLeading as + | q`Init.SpaceSepBy | q`Init.SpaceSepByNonEmpty | q`Init.SpacePrefixedBy | q`Init.SpacePrefixedByNonEmpty => + assert! cat.args.size = 1 + let c := cat.args[0]! + if c.name == thisCatName then + .invalid mf!"Leading symbol cannot be recursive call to {c}" + else + .isLeading as | q`Init.Option => assert! cat.args.size = 1 let c := cat.args[0]! @@ -840,6 +847,59 @@ private def sepByParser (p sep : Parser) (allowTrailingSep : Bool := false) : Pa s } +private def sepBy1Parser (p sep : Parser) (allowTrailingSep : Bool := false) : Parser := { + info := sepByInfo p.info sep.info + fn := fun c s => + let s := sepByFn allowTrailingSep p.fn sep.fn c s + if s.hasError then + s + else + match s.stxStack.back with + | .node .none k args => + if args.isEmpty then + -- Require at least one element + s.mkError "expected at least one element" + else + s + | _ => + s +} + +private def spacePrefixedParser (p : Parser) : Parser := { + info := noFirstTokenInfo p.info + fn := fun c s => + let s := manyFn (andthenFn (symbolNoAntiquot " ").fn p.fn) c s + if s.hasError then + s + else + match s.stxStack.back with + | .node .none _k args => + if args.isEmpty then + s.popSyntax.pushSyntax (.node (emptySourceInfo c s.pos) _k args) + else + s + | _ => + s +} + +private def spacePrefixed1Parser (p : Parser) : Parser := { + info := noFirstTokenInfo p.info + fn := fun c s => + let s := manyFn (andthenFn (symbolNoAntiquot " ").fn p.fn) c s + if s.hasError then + s + else + match s.stxStack.back with + | .node .none _k args => + if args.isEmpty then + -- Require at least one element + s.mkError "expected at least one element" + else + s + | _ => + s +} + def manyParser (p : Parser) : Parser := { info := noFirstTokenInfo p.info fn := fun c s => @@ -848,9 +908,26 @@ def manyParser (p : Parser) : Parser := { s else match s.stxStack.back with - | .node .none k args => + | .node .none _k args => if args.isEmpty then - s.popSyntax.pushSyntax (.node (emptySourceInfo c s.pos) k args) + s.popSyntax.pushSyntax (.node (emptySourceInfo c s.pos) _k args) + else + s + | _ => + s +} + +def many1Parser (p : Parser) : Parser := { + info := p.info + fn := fun c s => + let s := manyFn p.fn c s + if s.hasError then + s + else + match s.stxStack.back with + | .node .none _k args => + if args.isEmpty then + s.mkError "expected at least one element" else s | _ => @@ -863,6 +940,18 @@ partial def catParser (ctx : ParsingContext) (cat : SyntaxCat) : Except SyntaxCa | q`Init.CommaSepBy => assert! cat.args.size = 1 (sepByParser · (symbolNoAntiquot ",")) <$> catParser ctx cat.args[0]! + | q`Init.SpaceSepBy => + assert! cat.args.size = 1 + manyParser <$> catParser ctx cat.args[0]! + | q`Init.SpaceSepByNonEmpty => + assert! cat.args.size = 1 + many1Parser <$> catParser ctx cat.args[0]! + | q`Init.SpacePrefixedBy => + assert! cat.args.size = 1 + manyParser <$> catParser ctx cat.args[0]! + | q`Init.SpacePrefixedByNonEmpty => + assert! cat.args.size = 1 + many1Parser <$> catParser ctx cat.args[0]! | q`Init.Option => assert! cat.args.size = 1 optionalNoAntiquot <$> catParser ctx cat.args[0]! diff --git a/Strata/DL/SMT/DDMTransform/Parse.lean b/Strata/DL/SMT/DDMTransform/Parse.lean index e573c74f3..c8b50aa7e 100644 --- a/Strata/DL/SMT/DDMTransform/Parse.lean +++ b/Strata/DL/SMT/DDMTransform/Parse.lean @@ -160,10 +160,6 @@ op simple_symbol_some () : SimpleSymbol => "some"; category Symbol; op symbol (@[unwrap] s:SimpleSymbol) : Symbol => s; -category SymbolList; // For spacing, has at least one element -op symbol_list_one (se:Symbol) : SymbolList => se; -op symbol_list_cons (se:Symbol, sse:SymbolList) : SymbolList => se " " sse; - category Keyword; op kw_symbol (@[unwrap] s:SimpleSymbol) : Keyword => ":" s; @@ -191,11 +187,7 @@ op se_symbol (s:Symbol) : SExpr => s; op se_reserved (s:Reserved) : SExpr => s; op se_keyword (s:Keyword) : SExpr => s; -category SExprList; // For spacing, has at least one element -op sexpr_list_one (se:SExpr) : SExprList => se; -op sexpr_list_cons (se:SExpr, sse:SExprList) : SExprList => se " " sse; - -op se_ls (s:Option SExprList) : SExpr => "(" s ")"; +op se_ls (s:SpaceSepBy SExpr) : SExpr => "(" s ")"; category SMTIdentifier; @@ -207,11 +199,7 @@ op ind_symbol (@[unwrap] s:Symbol) : Index => s; op iden_simple (s:Symbol) : SMTIdentifier => s; -category IndexList; // For spacing; has at least one element -op index_list_one (i:Index) : IndexList => i; -op index_list_cons (i:Index, spi:IndexList) : IndexList => i " " spi; - -op iden_indexed (s:Symbol, si:IndexList) : SMTIdentifier => +op iden_indexed (s:Symbol, si:SpaceSepByNonEmpty Index) : SMTIdentifier => "(" "_ " s " " si ")"; @@ -219,11 +207,7 @@ op iden_indexed (s:Symbol, si:IndexList) : SMTIdentifier => category SMTSort; op smtsort_ident (s:SMTIdentifier) : SMTSort => s; -category SMTSortList; // For spacing; has at least one element -op smtsort_list_one (i:SMTSort) : SMTSortList => i; -op smtsort_list_cons (i:SMTSort, spi:SMTSortList) : SMTSortList => i " " spi; - -op smtsort_param (s:SMTIdentifier, sl:SMTSortList) : SMTSort +op smtsort_param (s:SMTIdentifier, sl:SpaceSepByNonEmpty SMTSort) : SMTSort => "(" s " " sl ")"; @@ -236,10 +220,6 @@ op av_sel (s:Seq SExpr) : AttributeValue => "(" s ")"; category Attribute; op att_kw (k:Keyword, av:Option AttributeValue) : Attribute => k av; -category AttributeList; // For spacing; has at least one element -op att_list_one (i:Attribute) : AttributeList => i; -op att_list_cons (i:Attribute, spi:AttributeList) : AttributeList => i " " spi; - // 6. Terms category QualIdentifier; @@ -249,41 +229,29 @@ op qi_isort (i:SMTIdentifier, s:SMTSort) : QualIdentifier => category Term; // Forward declaration -category TermList; // For Spacing -op term_list_one (i:Term) : TermList => i:0; -op term_list_cons (i:Term, spi:TermList) : TermList => i:0 " " spi:0; - category ValBinding; op val_binding (s:Symbol, t:Term) : ValBinding => "(" s " " t ")"; -category ValBindingList; // For spacing; has at least one element -op val_binding_list_one (i:ValBinding) : ValBindingList => i; -op val_binding_list_cons (i:ValBinding, spi:ValBindingList) : ValBindingList => i " " spi; - category SortedVar; op sorted_var (s:Symbol, so:SMTSort) : SortedVar => "(" s " " so ")"; -category SortedVarList; // For spacing; has at least one element -op sorted_var_list_one (i:SortedVar) : SortedVarList => i; -op sorted_var_list_cons (i:SortedVar, spi:SortedVarList) : SortedVarList => i " " spi; - // TODO: support the match statement // category Pattern; op spec_constant_term (sc:SpecConstant) : Term => sc; op qual_identifier (qi:QualIdentifier) : Term => qi; -op qual_identifier_args (qi:QualIdentifier, ts:TermList) : Term => +op qual_identifier_args (qi:QualIdentifier, ts:SpaceSepByNonEmpty Term) : Term => "(" qi " " ts ")"; -op let_smt (vbps: ValBindingList, t:Term) : Term => +op let_smt (vbps: SpaceSepByNonEmpty ValBinding, t:Term) : Term => "(" "let" "(" vbps ")" t ")"; -op lambda_smt (svs: SortedVarList, t:Term) : Term => +op lambda_smt (svs: SpaceSepByNonEmpty SortedVar, t:Term) : Term => "(" "lambda" "(" svs ")" t ")"; -op forall_smt (svs: SortedVarList, t:Term) : Term => +op forall_smt (svs: SpaceSepByNonEmpty SortedVar, t:Term) : Term => "(" "forall" "(" svs ")" t ")"; -op exists_smt (svs: SortedVarList, t:Term) : Term => +op exists_smt (svs: SpaceSepByNonEmpty SortedVar, t:Term) : Term => "(" "exists" "(" svs ")" t ")"; -op bang (t:Term, attrs:AttributeList) : Term => +op bang (t:Term, attrs:SpaceSepByNonEmpty Attribute) : Term => "(" "!" t " " attrs ")"; @@ -345,40 +313,18 @@ op smtoption_attr (a:Attribute) : SMTOption => a; category SortDec; op sort_dec (s:Symbol, n:Num) : SortDec => "(" s n ")"; -category SortDecList; // For spacing; has at least one element -op sort_dec_list_one (i:SortDec) : SortDecList => i; -op sort_dec_list_cons (i:SortDec, spi:SortDecList) : SortDecList => - i " " spi; - category SelectorDec; op selector_dec (s:Symbol, so:SMTSort) : SelectorDec => "(" s so ")"; -category SelectorDecList; // For spacing; has at least one element -op selector_dec_list_one (i:SelectorDec) : SelectorDecList => i; -op selector_dec_list_cons (i:SelectorDec, spi:SelectorDecList) : SelectorDecList => - i " " spi; - category ConstructorDec; -op constructor_dec (s:Symbol, sdl:Option SelectorDecList) : ConstructorDec => - "(" s " " sdl ")"; - -category ConstructorDecList; // For spacing; has at least one element -op constructor_list_one (i:ConstructorDec) : ConstructorDecList => i; -op constructor_list_cons (i:ConstructorDec, spi:ConstructorDecList) - : ConstructorDecList => - i " " spi; +op constructor_dec (s:Symbol, sdl:SpaceSepBy SelectorDec) : ConstructorDec => + "(" s sdl ")"; category DatatypeDec; -op datatype_dec (cs:ConstructorDecList) : DatatypeDec +op datatype_dec (cs:SpaceSepByNonEmpty ConstructorDec) : DatatypeDec => "(" cs ")"; -op datatype_dec_par (symbols: SymbolList, cs:ConstructorDecList) : DatatypeDec - => "(" "par " "(" symbols ")" "(" cs ")" ")"; - -category DatatypeDecList; // For spacing; has at least one element -op datatype_dec_list_one (i:DatatypeDec) : DatatypeDecList => i; -op datatype_dec_list_cons (i:DatatypeDec, spi:DatatypeDecList) - : DatatypeDecList => - i " " spi; +op datatype_dec_par (symbols: SpaceSepByNonEmpty Symbol, cs:SpaceSepByNonEmpty ConstructorDec) : DatatypeDec + => "(" "par" "(" symbols ")" "(" cs ")" ")"; category FunctionDec; op function_dec (s:Symbol, sv:Seq SortedVar, so:SMTSort) : FunctionDec @@ -388,12 +334,6 @@ category FunctionDef; op function_def (s:Symbol, sv:Seq SortedVar, so:SMTSort, t:Term) : FunctionDef => s "(" sv ")" so t; -category FunctionDefList; // For spacing; has at least one element -op function_def_list_one (i:FunctionDef) : FunctionDefList => i; -op function_def_list_cons (i:FunctionDef, spi:FunctionDefList) - : FunctionDefList => - i " " spi; - #end @@ -406,53 +346,53 @@ import SMTCore; // 11. Commands (cont.) // cmd_' is necessary, otherwise it raises "unexpected token 'assert'; expected identifier" -op cmd_assert (t:Term) : Command => "(" "assert " t ")"; +op cmd_assert (t:Term) : Command => "(" "assert" t ")"; op check_sat () : Command => "(" "check-sat" ")"; -op check_sat_assuming (ts:Option TermList) : Command => - "(" "check-sat-assuming " ts ")"; +op check_sat_assuming (ts:SpacePrefixedBy Term) : Command => + "(" "check-sat-assuming" ts ")"; op declare_const (s:Symbol, so:SMTSort) : Command => - "(" "declare-const " s so ")"; + "(" "declare-const" s so ")"; op declare_datatype (s:Symbol, so:DatatypeDec) : Command => - "(" "declare-datatype " s so ")"; + "(" "declare-datatype" s so ")"; // The size of SortDec and DatatypeDec must be equal, but omit the check in // this DDM definition because its representation can be quite ugly. -op declare_datatypes (s:SortDecList, so:DatatypeDecList) : Command => +op declare_datatypes (s:SpaceSepByNonEmpty SortDec, so:SpaceSepByNonEmpty DatatypeDec) : Command => "(" "declare-datatypes" "(" s ")" "(" so ")" ")"; -op declare_fun (s:Symbol, sol:Option SMTSortList, range:SMTSort) : Command => - "(" "declare-fun " s "(" sol ")" range ")"; +op declare_fun (s:Symbol, sol:SpaceSepBy SMTSort, range:SMTSort) : Command => + "(" "declare-fun" s "(" sol ")" range ")"; op declare_sort (s:Symbol, n:Num) : Command => - "(" "declare-sort " s n ")"; + "(" "declare-sort" s n ")"; op declare_sort_parameter (s:Symbol) : Command => - "(" "declare-sort-parameter " s ")"; + "(" "declare-sort-parameter" s ")"; op define_const (s:Symbol, so:SMTSort, t:Term) : Command => - "(" "define-const " s so t ")"; + "(" "define-const" s so t ")"; op define_fun (fdef:FunctionDef) : Command => - "(" "define-fun " fdef ")"; + "(" "define-fun" fdef ")"; op define_fun_rec (fdef:FunctionDef) : Command => - "(" "define-fun-rec " fdef ")"; -op define_funs_rec (fdefs:FunctionDefList, terms:TermList) : Command => + "(" "define-fun-rec" fdef ")"; +op define_funs_rec (fdefs:SpaceSepByNonEmpty FunctionDef, terms:SpaceSepByNonEmpty Term) : Command => "(" "define-funs-rec" "(" fdefs ")" "(" terms ")" ")"; op define_sort (s:Symbol, sl:Seq Symbol, so:SMTSort) : Command => - "(" "define-sort " s "(" sl ")" so ")"; -op cmd_echo (s:Str) : Command => "(" "echo " s ")"; + "(" "define-sort" s "(" sl ")" so ")"; +op cmd_echo (s:Str) : Command => "(" "echo" s ")"; op cmd_exit () : Command => "(" "exit" ")"; op get_assertions () : Command => "(" "get-assertions" ")"; op get_assignment () : Command => "(" "get-assignment" ")"; -op get_info (x:InfoFlag) : Command => "(" "get-info " x ")"; +op get_info (x:InfoFlag) : Command => "(" "get-info" x ")"; op get_model () : Command => "(" "get-model" ")"; -op get_option (kw:Keyword) : Command => "(" "get-option " kw ")"; +op get_option (kw:Keyword) : Command => "(" "get-option" kw ")"; op get_proof () : Command => "(" "get-proof" ")"; op get_unsat_assumptions () : Command => "(" "get-unsat-assumptions" ")"; op get_unsat_core () : Command => "(" "get-unsat-core" ")"; -op get_value (tl:TermList) : Command => +op get_value (tl:SpaceSepByNonEmpty Term) : Command => "(" "get-value" "(" tl ")" ")"; -op cmd_pop (n:Num) : Command => "(" "pop " n ")"; -op cmd_push (n:Num) : Command => "(" "push " n ")"; +op cmd_pop (n:Num) : Command => "(" "pop" n ")"; +op cmd_push (n:Num) : Command => "(" "push" n ")"; op cmd_reset () : Command => "(" "reset" ")"; op reset_assertions () : Command => "(" "reset-assertions" ")"; -op set_info (a:Attribute) : Command => "(" "set-info " a ")"; -op set_logic (s:Symbol) : Command => "(" "set-logic " s ")"; -op set_option (s:SMTOption) : Command => "(" "set-option " s ")"; +op set_info (a:Attribute) : Command => "(" "set-info" a ")"; +op set_logic (s:Symbol) : Command => "(" "set-logic" s ")"; +op set_option (s:SMTOption) : Command => "(" "set-option" s ")"; #end @@ -496,29 +436,12 @@ op ir_unknown (r:ReasonUnknown) : InfoResponse => ":reason-unknown " r; op ir_ver (s:Str) : InfoResponse => ":version " s; op ir_attr (a:Attribute) : InfoResponse => a; -category InfoResponseList; -op ir_list_one (i: InfoResponse) : InfoResponseList => i; -op ir_list_cons (i: InfoResponse, is: InfoResponseList) : InfoResponseList - => i is; - category ValuationPair; op valuation_pair (t1:Term, t2:Term) : ValuationPair => "(" t1 " " t2 ")"; -category ValuationPairList; -op valuation_pair_list_one (i: ValuationPair) : ValuationPairList => i; -op valuation_pair_list_cons (i: ValuationPair, is: ValuationPairList) - : ValuationPairList - => i is; - category TValuationPair; op t_valuation_pair (t1:Symbol, t2:BValue) : TValuationPair => "(" t1 " " t2 ")"; -category TValuationPairList; -op t_valuation_pair_list_one (i: TValuationPair) : TValuationPairList => i; -op t_valuation_pair_list_cons (i: TValuationPair, is: TValuationPairList) - : TValuationPairList - => i is; - category CheckSatResponse; op csr_sat () : CheckSatResponse => "sat"; op csr_unsat () : CheckSatResponse => "unsat"; @@ -528,20 +451,20 @@ category EchoResponse; op echo_response (s:Str) : EchoResponse => s; category GetAssertionsResponse; -op get_assertions_response (t:Option TermList) : GetAssertionsResponse => +op get_assertions_response (t:SpaceSepBy Term) : GetAssertionsResponse => "(" t ")"; category GetAssignmentResponse; -op get_assignment_response (t:Option TValuationPairList) +op get_assignment_response (t:SpaceSepBy TValuationPair) : GetAssignmentResponse => "(" t ")"; category GetInfoResponse; -op get_info_response (i2:InfoResponseList) : GetInfoResponse => +op get_info_response (i2:SpaceSepBy InfoResponse) : GetInfoResponse => "(" i2 ")"; category GetModelResponse; -op get_model_response (mr:SeqModelResponse) : GetModelResponse => +op get_model_response (mr:SpaceSepBy ModelResponse) : GetModelResponse => "(" mr ")"; category GetOptionResponse; @@ -551,15 +474,15 @@ category GetProofResponse; op get_proof_response (s:SExpr) : GetProofResponse => s; category GetUnsatAssumpResponse; -op get_unsat_assump_response (ts:Option TermList) : GetUnsatAssumpResponse => +op get_unsat_assump_response (ts:SpaceSepBy Term) : GetUnsatAssumpResponse => "(" ts ")"; category GetUnsatCoreResponse; -op get_unsat_core_response (ss:Option SymbolList) : GetUnsatCoreResponse => +op get_unsat_core_response (ss:SpaceSepBy Symbol) : GetUnsatCoreResponse => "(" ss ")"; category GetValueResponse; -op get_value_response (vps:Option ValuationPairList) +op get_value_response (vps:SpaceSepBy ValuationPair) : GetValueResponse => "(" vps ")"; category SpecificSuccessResponse; @@ -816,23 +739,23 @@ namespace SMTDDM deriving instance BEq for -- Sequences SpecConstant, QualifiedIdent, SimpleSymbol, - Symbol, SymbolList, - SortDec, SortDecList, + Symbol, + SortDec, Reserved, Keyword, SExpr, AttributeValue, BValue, - Attribute, AttributeList, + Attribute, SMTOption, - Index, IndexList, + Index, SMTIdentifier, - SMTSort, SMTSortList, - SortedVar, SortedVarList, + SMTSort, + SortedVar, QualIdentifier, ValBinding, - Term, TermList, + Term, InfoFlag, - SelectorDec, SelectorDecList, - ConstructorDec, ConstructorDecList, - DatatypeDec, DatatypeDecList, - FunctionDef, FunctionDefList, + SelectorDec, + ConstructorDec, + DatatypeDec, + FunctionDef, Command end SMTDDM diff --git a/Strata/DL/SMT/DDMTransform/Translate.lean b/Strata/DL/SMT/DDMTransform/Translate.lean index ec5a7f853..69e73bccf 100644 --- a/Strata/DL/SMT/DDMTransform/Translate.lean +++ b/Strata/DL/SMT/DDMTransform/Translate.lean @@ -71,22 +71,14 @@ private def translateFromTermPrim (t:SMT.TermPrim): let bvty := mkSymbol (s!"bv{bv.toNat}") let val:Index SourceRange := .ind_numeral srnone bv.width return (.qual_identifier srnone - (.qi_ident srnone (.iden_indexed srnone bvty (.index_list_one srnone val)))) + (.qi_ident srnone (.iden_indexed srnone bvty (Ann.mk srnone #[val])))) | .string s => return .spec_constant_term srnone (.sc_str srnone s) --- List of SMTSort to SeqPSMTSort. --- Hope this could be elided away later. :( +-- List of SMTSort to Array. private def translateFromSMTSortList (l: List (SMTSort SourceRange)): - Option (SMTSortList SourceRange) := - let srnone := SourceRange.none - match l with - | [] => .none - | h::[] => .some (.smtsort_list_one srnone h) - | h1::h2::t => .some ( - match translateFromSMTSortList t with - | .none => .smtsort_list_cons srnone h1 (.smtsort_list_one srnone h2) - | .some t => .smtsort_list_cons srnone h1 (.smtsort_list_cons srnone h2 t)) + Array (SMTSort SourceRange) := + l.toArray private def translateFromTermType (t:SMT.TermType): Except String (SMTDDM.SMTSort SourceRange) := do @@ -95,10 +87,11 @@ private def translateFromTermType (t:SMT.TermType): | .prim tp => match tp with | .bitvec n => + let idx : Index SourceRange := .ind_numeral srnone n return (.smtsort_ident srnone (.iden_indexed srnone (mkSymbol "BitVec") - (.index_list_one srnone (.ind_numeral srnone n)))) + (Ann.mk srnone #[idx]))) | .trigger => throw "don't know how to translate a trigger type" | _ => @@ -114,37 +107,21 @@ private def translateFromTermType (t:SMT.TermType): throw "don't know how to translate an option type" | .constr id args => let argtys <- args.mapM translateFromTermType - match translateFromSMTSortList argtys with - | .none => throw "empty argument to type constructor" - | .some argtys => - return .smtsort_param srnone (mkIdentifier id) argtys + let argtys_array := translateFromSMTSortList argtys + if argtys_array.isEmpty then + throw "empty argument to type constructor" + else + return .smtsort_param srnone (mkIdentifier id) (Ann.mk srnone argtys_array) --- List of SortedVar to SeqPSortedVar. --- Hope this could be elided away later. :( +-- List of SortedVar to Array. private def translateFromSortedVarList (l: List (SortedVar SourceRange)): - Option (SortedVarList SourceRange) := - let srnone := SourceRange.none - match l with - | [] => .none - | h::[] => .some (.sorted_var_list_one srnone h) - | h1::h2::t => .some ( - match translateFromSortedVarList t with - | .none => .sorted_var_list_cons srnone h1 (.sorted_var_list_one srnone h2) - | .some t => - .sorted_var_list_cons srnone h1 (.sorted_var_list_cons srnone h2 t)) - --- List of SortedVar to SeqPSortedVar. --- Hope this could be elided away later. :( + Array (SortedVar SourceRange) := + l.toArray + +-- List of Term to Array. private def translateFromTermList (l: List (Term SourceRange)): - Option (TermList SourceRange) := - let srnone := SourceRange.none - match l with - | [] => .none - | h::[] => .some (.term_list_one srnone h) - | h1::h2::t => .some ( - match translateFromTermList t with - | .none => .term_list_cons srnone h1 (.term_list_one srnone h2) - | .some t => .term_list_cons srnone h1 (.term_list_cons srnone h2 t)) + Array (Term SourceRange) := + l.toArray def translateFromTerm (t:SMT.Term): Except String (SMTDDM.Term SourceRange) := do let srnone := SourceRange.none @@ -156,27 +133,28 @@ def translateFromTerm (t:SMT.Term): Except String (SMTDDM.Term SourceRange) := d | .none _ | .some _ => throw "don't know how to translate none and some" | .app op args _ => let args' <- args.mapM translateFromTerm - match translateFromTermList args' with - | .some args => - return (.qual_identifier_args srnone - (.qi_ident srnone (mkIdentifier op.mkName)) args) - | .none => + let args_array := translateFromTermList args' + if args_array.isEmpty then return (.qual_identifier srnone (.qi_ident srnone (mkIdentifier op.mkName))) + else + return (.qual_identifier_args srnone + (.qi_ident srnone (mkIdentifier op.mkName)) (Ann.mk srnone args_array)) | .quant qkind args _tr body => let args_sorted:List (SMTDDM.SortedVar SourceRange) <- args.mapM (fun ⟨name,ty⟩ => do let ty' <- translateFromTermType ty return .sorted_var srnone (mkSymbol name) ty') - match translateFromSortedVarList args_sorted with - | .none => throw "empty quantifier" - | .some args_sorted => + let args_array := translateFromSortedVarList args_sorted + if args_array.isEmpty then + throw "empty quantifier" + else let body <- translateFromTerm body match qkind with | .all => - return .forall_smt srnone args_sorted body + return .forall_smt srnone (Ann.mk srnone args_array) body | .exist => - return .exists_smt srnone args_sorted body + return .exists_smt srnone (Ann.mk srnone args_array) body private def dummy_prg_for_toString := diff --git a/StrataTest/Languages/B3/DDMFormatTests.lean b/StrataTest/Languages/B3/DDMFormatTests.lean index 2f321f143..93b427d0e 100644 --- a/StrataTest/Languages/B3/DDMFormatTests.lean +++ b/StrataTest/Languages/B3/DDMFormatTests.lean @@ -116,6 +116,10 @@ mutual | .option () ma => .option default (ma.map argFUnitToSourceRange) | .seq () entries => .seq default (entries.map argFUnitToSourceRange) | .commaSepList () entries => .commaSepList default (entries.map argFUnitToSourceRange) + | .spaceSepList () entries => .spaceSepList default (entries.map argFUnitToSourceRange) + | .spaceSepListNonEmpty () entries => .spaceSepListNonEmpty default (entries.map argFUnitToSourceRange) + | .spacePrefixedList () entries => .spacePrefixedList default (entries.map argFUnitToSourceRange) + | .spacePrefixedListNonEmpty () entries => .spacePrefixedListNonEmpty default (entries.map argFUnitToSourceRange) partial def typeExprFUnitToSourceRange : TypeExprF Unit → TypeExprF SourceRange | .ident () tp a => .ident default tp (a.map typeExprFUnitToSourceRange) From 10c7058d34828769725187bf154568b9e7005d93 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 9 Jan 2026 16:08:40 -0600 Subject: [PATCH 02/11] Restored whitespace --- Strata/DL/SMT/DDMTransform/Parse.lean | 36 +++++++++++++-------------- 1 file changed, 18 insertions(+), 18 deletions(-) diff --git a/Strata/DL/SMT/DDMTransform/Parse.lean b/Strata/DL/SMT/DDMTransform/Parse.lean index c8b50aa7e..5042603f1 100644 --- a/Strata/DL/SMT/DDMTransform/Parse.lean +++ b/Strata/DL/SMT/DDMTransform/Parse.lean @@ -324,7 +324,7 @@ category DatatypeDec; op datatype_dec (cs:SpaceSepByNonEmpty ConstructorDec) : DatatypeDec => "(" cs ")"; op datatype_dec_par (symbols: SpaceSepByNonEmpty Symbol, cs:SpaceSepByNonEmpty ConstructorDec) : DatatypeDec - => "(" "par" "(" symbols ")" "(" cs ")" ")"; + => "(" "par " "(" symbols ")" "(" cs ")" ")"; category FunctionDec; op function_dec (s:Symbol, sv:Seq SortedVar, so:SMTSort) : FunctionDec @@ -351,48 +351,48 @@ op check_sat () : Command => "(" "check-sat" ")"; op check_sat_assuming (ts:SpacePrefixedBy Term) : Command => "(" "check-sat-assuming" ts ")"; op declare_const (s:Symbol, so:SMTSort) : Command => - "(" "declare-const" s so ")"; + "(" "declare-const " s so ")"; op declare_datatype (s:Symbol, so:DatatypeDec) : Command => - "(" "declare-datatype" s so ")"; + "(" "declare-datatype " s so ")"; // The size of SortDec and DatatypeDec must be equal, but omit the check in // this DDM definition because its representation can be quite ugly. op declare_datatypes (s:SpaceSepByNonEmpty SortDec, so:SpaceSepByNonEmpty DatatypeDec) : Command => "(" "declare-datatypes" "(" s ")" "(" so ")" ")"; op declare_fun (s:Symbol, sol:SpaceSepBy SMTSort, range:SMTSort) : Command => - "(" "declare-fun" s "(" sol ")" range ")"; + "(" "declare-fun " s "(" sol ")" range ")"; op declare_sort (s:Symbol, n:Num) : Command => - "(" "declare-sort" s n ")"; + "(" "declare-sort " s n ")"; op declare_sort_parameter (s:Symbol) : Command => - "(" "declare-sort-parameter" s ")"; + "(" "declare-sort-parameter " s ")"; op define_const (s:Symbol, so:SMTSort, t:Term) : Command => - "(" "define-const" s so t ")"; + "(" "define-const " s so t ")"; op define_fun (fdef:FunctionDef) : Command => - "(" "define-fun" fdef ")"; + "(" "define-fun " fdef ")"; op define_fun_rec (fdef:FunctionDef) : Command => - "(" "define-fun-rec" fdef ")"; + "(" "define-fun-rec " fdef ")"; op define_funs_rec (fdefs:SpaceSepByNonEmpty FunctionDef, terms:SpaceSepByNonEmpty Term) : Command => "(" "define-funs-rec" "(" fdefs ")" "(" terms ")" ")"; op define_sort (s:Symbol, sl:Seq Symbol, so:SMTSort) : Command => - "(" "define-sort" s "(" sl ")" so ")"; -op cmd_echo (s:Str) : Command => "(" "echo" s ")"; + "(" "define-sort " s "(" sl ")" so ")"; +op cmd_echo (s:Str) : Command => "(" "echo " s ")"; op cmd_exit () : Command => "(" "exit" ")"; op get_assertions () : Command => "(" "get-assertions" ")"; op get_assignment () : Command => "(" "get-assignment" ")"; -op get_info (x:InfoFlag) : Command => "(" "get-info" x ")"; +op get_info (x:InfoFlag) : Command => "(" "get-info " x ")"; op get_model () : Command => "(" "get-model" ")"; -op get_option (kw:Keyword) : Command => "(" "get-option" kw ")"; +op get_option (kw:Keyword) : Command => "(" "get-option " kw ")"; op get_proof () : Command => "(" "get-proof" ")"; op get_unsat_assumptions () : Command => "(" "get-unsat-assumptions" ")"; op get_unsat_core () : Command => "(" "get-unsat-core" ")"; op get_value (tl:SpaceSepByNonEmpty Term) : Command => "(" "get-value" "(" tl ")" ")"; -op cmd_pop (n:Num) : Command => "(" "pop" n ")"; -op cmd_push (n:Num) : Command => "(" "push" n ")"; +op cmd_pop (n:Num) : Command => "(" "pop " n ")"; +op cmd_push (n:Num) : Command => "(" "push " n ")"; op cmd_reset () : Command => "(" "reset" ")"; op reset_assertions () : Command => "(" "reset-assertions" ")"; -op set_info (a:Attribute) : Command => "(" "set-info" a ")"; -op set_logic (s:Symbol) : Command => "(" "set-logic" s ")"; -op set_option (s:SMTOption) : Command => "(" "set-option" s ")"; +op set_info (a:Attribute) : Command => "(" "set-info " a ")"; +op set_logic (s:Symbol) : Command => "(" "set-logic " s ")"; +op set_option (s:SMTOption) : Command => "(" "set-option " s ")"; #end From 6072b82c1fae9ece8adb08cbbb2ccc8f7deb2178 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 13 Jan 2026 14:16:16 -0600 Subject: [PATCH 03/11] Implement @[nonempty] attribute to replace NonEmpty list variants - Add @[nonempty] metadata attribute in StrataDDL - Remove SpaceSepByNonEmpty and SpacePrefixedByNonEmpty categories - Remove spaceSepListNonEmpty and spacePrefixedListNonEmpty AST constructors - Update parser to check @[nonempty] metadata and use many1Parser/sepBy1Parser - Update all supporting files (Format, Ion, ToExpr, OfAstM, Gen, Elab) - Replace all SpaceSepByNonEmpty usage with @[nonempty] SpaceSepBy in SMT dialect - Add comprehensive tests in StrataTest/DDM/NonemptyAttribute.lean - Clarify that SpaceSepBy/SpacePrefixedBy/Seq parse identically, differ only in formatting --- Strata/DDM/AST.lean | 6 -- Strata/DDM/BuiltinDialects/Init.lean | 6 -- Strata/DDM/BuiltinDialects/StrataDDL.lean | 1 + Strata/DDM/Elab/Core.lean | 20 ---- Strata/DDM/Elab/Tree.lean | 18 ---- Strata/DDM/Format.lean | 10 -- Strata/DDM/Integration/Lean/Gen.lean | 26 ----- Strata/DDM/Integration/Lean/OfAstM.lean | 22 ----- Strata/DDM/Integration/Lean/ToExpr.lean | 6 -- Strata/DDM/Ion.lean | 24 ----- Strata/DDM/Parser.lean | 33 +++---- Strata/DL/SMT/DDMTransform/Parse.lean | 26 ++--- StrataTest/DDM/NonemptyAttribute.lean | 100 ++++++++++++++++++++ StrataTest/Languages/B3/DDMFormatTests.lean | 2 - 14 files changed, 129 insertions(+), 171 deletions(-) create mode 100644 StrataTest/DDM/NonemptyAttribute.lean diff --git a/Strata/DDM/AST.lean b/Strata/DDM/AST.lean index e1053345d..64bacfc91 100644 --- a/Strata/DDM/AST.lean +++ b/Strata/DDM/AST.lean @@ -169,9 +169,7 @@ inductive ArgF (α : Type) : Type where | seq (ann : α) (l : Array (ArgF α)) | commaSepList (ann : α) (l : Array (ArgF α)) | spaceSepList (ann : α) (l : Array (ArgF α)) -| spaceSepListNonEmpty (ann : α) (l : Array (ArgF α)) | spacePrefixedList (ann : α) (l : Array (ArgF α)) -| spacePrefixedListNonEmpty (ann : α) (l : Array (ArgF α)) deriving Inhabited, Repr end @@ -198,9 +196,7 @@ def ArgF.ann {α : Type} : ArgF α → α | .seq ann _ => ann | .commaSepList ann _ => ann | .spaceSepList ann _ => ann -| .spaceSepListNonEmpty ann _ => ann | .spacePrefixedList ann _ => ann -| .spacePrefixedListNonEmpty ann _ => ann end @@ -1301,9 +1297,7 @@ partial def foldOverArgBindingSpecs {α β} | .seq _ a => a.attach.foldl (init := init) fun init ⟨a, _⟩ => foldOverArgBindingSpecs m f init a | .commaSepList _ a => a.attach.foldl (init := init) fun init ⟨a, _⟩ => foldOverArgBindingSpecs m f init a | .spaceSepList _ a => a.attach.foldl (init := init) fun init ⟨a, _⟩ => foldOverArgBindingSpecs m f init a - | .spaceSepListNonEmpty _ a => a.attach.foldl (init := init) fun init ⟨a, _⟩ => foldOverArgBindingSpecs m f init a | .spacePrefixedList _ a => a.attach.foldl (init := init) fun init ⟨a, _⟩ => foldOverArgBindingSpecs m f init a - | .spacePrefixedListNonEmpty _ a => a.attach.foldl (init := init) fun init ⟨a, _⟩ => foldOverArgBindingSpecs m f init a /-- Invoke a function `f` over each of the declaration specifications for an operator. diff --git a/Strata/DDM/BuiltinDialects/Init.lean b/Strata/DDM/BuiltinDialects/Init.lean index 0ce2ddcf0..1c9942297 100644 --- a/Strata/DDM/BuiltinDialects/Init.lean +++ b/Strata/DDM/BuiltinDialects/Init.lean @@ -19,9 +19,7 @@ def SyntaxCat.mkOpt (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init. def SyntaxCat.mkSeq (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.Seq, args := #[c] } def SyntaxCat.mkCommaSepBy (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.CommaSepBy, args := #[c] } def SyntaxCat.mkSpaceSepBy (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.SpaceSepBy, args := #[c] } -def SyntaxCat.mkSpaceSepByNonEmpty (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.SpaceSepByNonEmpty, args := #[c] } def SyntaxCat.mkSpacePrefixedBy (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.SpacePrefixedBy, args := #[c] } -def SyntaxCat.mkSpacePrefixedByNonEmpty (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.SpacePrefixedByNonEmpty, args := #[c] } def initDialect : Dialect := BuiltinM.create! "Init" #[] do let Ident : ArgDeclKind := .cat <| .atom .none q`Init.Ident @@ -56,12 +54,8 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do declareCat q`Init.SpaceSepBy #["a"] - declareCat q`Init.SpaceSepByNonEmpty #["a"] - declareCat q`Init.SpacePrefixedBy #["a"] - declareCat q`Init.SpacePrefixedByNonEmpty #["a"] - let QualifiedIdent := q`Init.QualifiedIdent declareCat QualifiedIdent declareOp { diff --git a/Strata/DDM/BuiltinDialects/StrataDDL.lean b/Strata/DDM/BuiltinDialects/StrataDDL.lean index af442a448..9df6ff6d5 100644 --- a/Strata/DDM/BuiltinDialects/StrataDDL.lean +++ b/Strata/DDM/BuiltinDialects/StrataDDL.lean @@ -156,6 +156,7 @@ def StrataDDL : Dialect := BuiltinM.create! "StrataDDL" #[initDialect] do declareMetadata { name := "scope", args := #[.mk "scope" .ident] } declareMetadata { name := "unwrap", args := #[] } + declareMetadata { name := "nonempty", args := #[] } declareMetadata { name := "declareType", args := #[.mk "name" .ident, .mk "args" (.opt .ident)] } declareMetadata { name := "aliasType", args := #[.mk "name" .ident, .mk "args" (.opt .ident), .mk "def" .ident] } declareMetadata { name := "declare", args := #[.mk "name" .ident, .mk "type" .ident] } diff --git a/Strata/DDM/Elab/Core.lean b/Strata/DDM/Elab/Core.lean index f1dc9bfa9..bd6d1dc68 100644 --- a/Strata/DDM/Elab/Core.lean +++ b/Strata/DDM/Elab/Core.lean @@ -1133,16 +1133,6 @@ partial def catElaborator (c : SyntaxCat) : TypingContext → Syntax → ElabM T let (args, resultCtx) ← stx.getSepArgs.foldlM f (#[], tctx) let info : SpaceSepInfo := { inputCtx := tctx, loc := loc, args := args.map (·.arg), resultCtx } pure <| .node (.ofSpaceSepInfo info) args - | q`Init.SpaceSepByNonEmpty => - assert! c.args.size = 1 - let a := c.args[0]! - let f := elabManyElement (catElaborator a) - fun tctx stx => do - let some loc := mkSourceRange? stx - | panic! s!"spaceSepByNonEmpty missing source location {repr stx}" - let (args, resultCtx) ← stx.getSepArgs.foldlM f (#[], tctx) - let info : SpaceSepNonEmptyInfo := { inputCtx := tctx, loc := loc, args := args.map (·.arg), resultCtx } - pure <| .node (.ofSpaceSepNonEmptyInfo info) args | q`Init.SpacePrefixedBy => assert! c.args.size = 1 let a := c.args[0]! @@ -1153,16 +1143,6 @@ partial def catElaborator (c : SyntaxCat) : TypingContext → Syntax → ElabM T let (args, resultCtx) ← stx.getArgs.foldlM f (#[], tctx) let info : SpacePrefixedInfo := { inputCtx := tctx, loc := loc, args := args.map (·.arg), resultCtx } pure <| .node (.ofSpacePrefixedInfo info) args - | q`Init.SpacePrefixedByNonEmpty => - assert! c.args.size = 1 - let a := c.args[0]! - let f := elabManyElement (catElaborator a) - fun tctx stx => do - let some loc := mkSourceRange? stx - | panic! s!"spacePrefixedByNonEmpty missing source location {repr stx}" - let (args, resultCtx) ← stx.getArgs.foldlM f (#[], tctx) - let info : SpacePrefixedNonEmptyInfo := { inputCtx := tctx, loc := loc, args := args.map (·.arg), resultCtx } - pure <| .node (.ofSpacePrefixedNonEmptyInfo info) args | _ => assert! c.args.isEmpty elabOperation diff --git a/Strata/DDM/Elab/Tree.lean b/Strata/DDM/Elab/Tree.lean index 9d9f86e57..cde90ae05 100644 --- a/Strata/DDM/Elab/Tree.lean +++ b/Strata/DDM/Elab/Tree.lean @@ -251,21 +251,11 @@ structure SpaceSepInfo extends ElabInfo where resultCtx : TypingContext deriving Inhabited, Repr -structure SpaceSepNonEmptyInfo extends ElabInfo where - args : Array Arg - resultCtx : TypingContext -deriving Inhabited, Repr - structure SpacePrefixedInfo extends ElabInfo where args : Array Arg resultCtx : TypingContext deriving Inhabited, Repr -structure SpacePrefixedNonEmptyInfo extends ElabInfo where - args : Array Arg - resultCtx : TypingContext -deriving Inhabited, Repr - inductive Info | ofOperationInfo (info : OperationInfo) | ofCatInfo (info : CatInfo) @@ -280,9 +270,7 @@ inductive Info | ofSeqInfo (info : SeqInfo) | ofCommaSepInfo (info : CommaSepInfo) | ofSpaceSepInfo (info : SpaceSepInfo) -| ofSpaceSepNonEmptyInfo (info : SpaceSepNonEmptyInfo) | ofSpacePrefixedInfo (info : SpacePrefixedInfo) -| ofSpacePrefixedNonEmptyInfo (info : SpacePrefixedNonEmptyInfo) deriving Inhabited, Repr namespace Info @@ -318,9 +306,7 @@ def elabInfo (info : Info) : ElabInfo := | .ofSeqInfo info => info.toElabInfo | .ofCommaSepInfo info => info.toElabInfo | .ofSpaceSepInfo info => info.toElabInfo - | .ofSpaceSepNonEmptyInfo info => info.toElabInfo | .ofSpacePrefixedInfo info => info.toElabInfo - | .ofSpacePrefixedNonEmptyInfo info => info.toElabInfo def inputCtx (info : Info) : TypingContext := info.elabInfo.inputCtx @@ -369,9 +355,7 @@ def arg : Tree → Arg | .ofSeqInfo info => .seq info.loc info.args | .ofCommaSepInfo info => .commaSepList info.loc info.args | .ofSpaceSepInfo info => .spaceSepList info.loc info.args - | .ofSpaceSepNonEmptyInfo info => .spaceSepListNonEmpty info.loc info.args | .ofSpacePrefixedInfo info => .spacePrefixedList info.loc info.args - | .ofSpacePrefixedNonEmptyInfo info => .spacePrefixedListNonEmpty info.loc info.args theorem sizeOf_children (t : Tree) (i : Nat) (p : i < t.children.size) : sizeOf t[i] < sizeOf t := by match t with @@ -395,9 +379,7 @@ def resultContext (t : Tree) : TypingContext := | .ofSeqInfo info => info.resultCtx | .ofCommaSepInfo info => info.resultCtx | .ofSpaceSepInfo info => info.resultCtx - | .ofSpaceSepNonEmptyInfo info => info.resultCtx | .ofSpacePrefixedInfo info => info.resultCtx - | .ofSpacePrefixedNonEmptyInfo info => info.resultCtx termination_by t def isSpecificOp (tree : Tree) (expected : QualifiedIdent) : Bool := diff --git a/Strata/DDM/Format.lean b/Strata/DDM/Format.lean index e3ef03abe..8cc52efb4 100644 --- a/Strata/DDM/Format.lean +++ b/Strata/DDM/Format.lean @@ -395,19 +395,9 @@ private partial def ArgF.mformatM {α} : ArgF α → FormatM PrecFormat let f i q s := return s ++ " " ++ (← entries[i].mformatM).format let a := (← entries[0].mformatM).format .atom <$> entries.size.foldlM f (start := 1) a -| .spaceSepListNonEmpty _ entries => do - if z : entries.size = 0 then - pure (.atom .nil) - else do - let f i q s := return s ++ " " ++ (← entries[i].mformatM).format - let a := (← entries[0].mformatM).format - .atom <$> entries.size.foldlM f (start := 1) a | .spacePrefixedList _ entries => do .atom <$> entries.foldlM (init := .nil) fun p a => return (p ++ " " ++ (← a.mformatM).format) -| .spacePrefixedListNonEmpty _ entries => do - .atom <$> entries.foldlM (init := .nil) fun p a => - return (p ++ " " ++ (← a.mformatM).format) private partial def ppArgs (f : StrataFormat) (rargs : Array Arg) : FormatM PrecFormat := if rargs.isEmpty then diff --git a/Strata/DDM/Integration/Lean/Gen.lean b/Strata/DDM/Integration/Lean/Gen.lean index ec694ec67..b297590ff 100644 --- a/Strata/DDM/Integration/Lean/Gen.lean +++ b/Strata/DDM/Integration/Lean/Gen.lean @@ -575,12 +575,8 @@ partial def ppCatWithUnwrap (annType : Ident) (c : SyntaxCat) (unwrap : Bool) : return mkCApp ``Ann #[mkCApp ``Array #[args[0]], annType] | q`Init.SpaceSepBy, 1 => return mkCApp ``Ann #[mkCApp ``Array #[args[0]], annType] - | q`Init.SpaceSepByNonEmpty, 1 => - return mkCApp ``Ann #[mkCApp ``Array #[args[0]], annType] | q`Init.SpacePrefixedBy, 1 => return mkCApp ``Ann #[mkCApp ``Array #[args[0]], annType] - | q`Init.SpacePrefixedByNonEmpty, 1 => - return mkCApp ``Ann #[mkCApp ``Array #[args[0]], annType] | q`Init.Option, 1 => return mkCApp ``Ann #[mkCApp ``Option #[args[0]], annType] | q`Init.Seq, 1 => @@ -760,17 +756,6 @@ partial def toAstApplyArg (vn : Name) (cat : SyntaxCat) (unwrap : Bool := false) mkCApp ``Array.attach #[mkCApp ``Ann.val #[v]] ] return mkAnnWithTerm ``ArgF.spaceSepList v args - | q`Init.SpaceSepByNonEmpty => do - assert! cat.args.size = 1 - let c := cat.args[0]! - let e ← genFreshLeanName "e" - let canE ← genIdentFrom e (canonical := true) - let t ← toAstApplyArg e c - let args := mkCApp ``Array.map #[ - ←`(fun ⟨$canE, _⟩ => $t), - mkCApp ``Array.attach #[mkCApp ``Ann.val #[v]] - ] - return mkAnnWithTerm ``ArgF.spaceSepListNonEmpty v args | q`Init.SpacePrefixedBy => do assert! cat.args.size = 1 let c := cat.args[0]! @@ -782,17 +767,6 @@ partial def toAstApplyArg (vn : Name) (cat : SyntaxCat) (unwrap : Bool := false) mkCApp ``Array.attach #[mkCApp ``Ann.val #[v]] ] return mkAnnWithTerm ``ArgF.spacePrefixedList v args - | q`Init.SpacePrefixedByNonEmpty => do - assert! cat.args.size = 1 - let c := cat.args[0]! - let e ← genFreshLeanName "e" - let canE ← genIdentFrom e (canonical := true) - let t ← toAstApplyArg e c - let args := mkCApp ``Array.map #[ - ←`(fun ⟨$canE, _⟩ => $t), - mkCApp ``Array.attach #[mkCApp ``Ann.val #[v]] - ] - return mkAnnWithTerm ``ArgF.spacePrefixedListNonEmpty v args | q`Init.Option => do assert! cat.args.size = 1 let c := cat.args[0]! diff --git a/Strata/DDM/Integration/Lean/OfAstM.lean b/Strata/DDM/Integration/Lean/OfAstM.lean index cece63ac4..781d14ebd 100644 --- a/Strata/DDM/Integration/Lean/OfAstM.lean +++ b/Strata/DDM/Integration/Lean/OfAstM.lean @@ -199,17 +199,6 @@ def ofSpaceSepByM {α β} [Repr α] [SizeOf α] pure { ann := ann, val := val } | _ => throwExpected "spaceSepBy" arg -def ofSpaceSepByNonEmptyM {α β} [Repr α] [SizeOf α] - (arg : ArgF α) - (act : ∀(e : ArgF α), sizeOf e < sizeOf arg → OfAstM β) - : OfAstM (Ann (Array β) α) := - match arg with - | .spaceSepListNonEmpty ann a => do - let val ← a.attach.mapM fun ⟨v, vIn⟩ => - act v (by decreasing_tactic) - pure { ann := ann, val := val } - | _ => throwExpected "spaceSepByNonEmpty" arg - def ofSpacePrefixedByM {α β} [Repr α] [SizeOf α] (arg : ArgF α) (act : ∀(e : ArgF α), sizeOf e < sizeOf arg → OfAstM β) @@ -221,17 +210,6 @@ def ofSpacePrefixedByM {α β} [Repr α] [SizeOf α] pure { ann := ann, val := val } | _ => throwExpected "spacePrefixedBy" arg -def ofSpacePrefixedByNonEmptyM {α β} [Repr α] [SizeOf α] - (arg : ArgF α) - (act : ∀(e : ArgF α), sizeOf e < sizeOf arg → OfAstM β) - : OfAstM (Ann (Array β) α) := - match arg with - | .spacePrefixedListNonEmpty ann a => do - let val ← a.attach.mapM fun ⟨v, vIn⟩ => - act v (by decreasing_tactic) - pure { ann := ann, val := val } - | _ => throwExpected "spacePrefixedByNonEmpty" arg - /-- Get the expression at index `lvl` in the arguments. diff --git a/Strata/DDM/Integration/Lean/ToExpr.lean b/Strata/DDM/Integration/Lean/ToExpr.lean index 625a3a58a..c7c4e4607 100644 --- a/Strata/DDM/Integration/Lean/ToExpr.lean +++ b/Strata/DDM/Integration/Lean/ToExpr.lean @@ -168,15 +168,9 @@ private def ArgF.toExpr {α} [ToExpr α] : ArgF α → Lean.Expr | .spaceSepList ann a => let tpe := ArgF.typeExpr α astAnnExpr! ArgF.spaceSepList ann <| arrayToExpr .zero tpe <| a.map (·.toExpr) -| .spaceSepListNonEmpty ann a => - let tpe := ArgF.typeExpr α - astAnnExpr! ArgF.spaceSepListNonEmpty ann <| arrayToExpr .zero tpe <| a.map (·.toExpr) | .spacePrefixedList ann a => let tpe := ArgF.typeExpr α astAnnExpr! ArgF.spacePrefixedList ann <| arrayToExpr .zero tpe <| a.map (·.toExpr) -| .spacePrefixedListNonEmpty ann a => - let tpe := ArgF.typeExpr α - astAnnExpr! ArgF.spacePrefixedListNonEmpty ann <| arrayToExpr .zero tpe <| a.map (·.toExpr) termination_by a => sizeOf a private protected def OperationF.toExpr {α} [ToExpr α] (op : OperationF α) : Lean.Expr := diff --git a/Strata/DDM/Ion.lean b/Strata/DDM/Ion.lean index 53b71457b..065b4276f 100644 --- a/Strata/DDM/Ion.lean +++ b/Strata/DDM/Ion.lean @@ -517,18 +517,10 @@ private protected def ArgF.toIon {α} [ToIon α] (refs : SymbolIdCache) (arg : A let args : Array (Ion _) := #[ ionSymbol! "spaceSepList", ← toIon ann ] let args ← l.attach.mapM_off (init := args) fun ⟨v, _h⟩ => v.toIon refs return .sexp args - | .spaceSepListNonEmpty ann l => do - let args : Array (Ion _) := #[ ionSymbol! "spaceSepListNonEmpty", ← toIon ann ] - let args ← l.attach.mapM_off (init := args) fun ⟨v, _h⟩ => v.toIon refs - return .sexp args | .spacePrefixedList ann l => do let args : Array (Ion _) := #[ ionSymbol! "spacePrefixedList", ← toIon ann ] let args ← l.attach.mapM_off (init := args) fun ⟨v, _h⟩ => v.toIon refs return .sexp args - | .spacePrefixedListNonEmpty ann l => do - let args : Array (Ion _) := #[ ionSymbol! "spacePrefixedListNonEmpty", ← toIon ann ] - let args ← l.attach.mapM_off (init := args) fun ⟨v, _h⟩ => v.toIon refs - return .sexp args termination_by sizeOf arg decreasing_by all_goals decreasing_tactic @@ -647,24 +639,12 @@ private protected def ArgF.fromIon {α} [FromIon α] (v : Ion SymbolId) : FromIo let args ← sexp.attach.mapM_off (start := 2) fun ⟨u, _⟩ => Strata.ArgF.fromIon u return .spaceSepList ann args - | "spaceSepListNonEmpty" => do - let ⟨p⟩ ← .checkArgMin "spaceSepListNonEmpty" sexp 2 - let ann ← fromIon sexp[1] - let args ← sexp.attach.mapM_off (start := 2) fun ⟨u, _⟩ => - Strata.ArgF.fromIon u - return .spaceSepListNonEmpty ann args | "spacePrefixedList" => do let ⟨p⟩ ← .checkArgMin "spacePrefixedList" sexp 2 let ann ← fromIon sexp[1] let args ← sexp.attach.mapM_off (start := 2) fun ⟨u, _⟩ => Strata.ArgF.fromIon u return .spacePrefixedList ann args - | "spacePrefixedListNonEmpty" => do - let ⟨p⟩ ← .checkArgMin "spacePrefixedListNonEmpty" sexp 2 - let ann ← fromIon sexp[1] - let args ← sexp.attach.mapM_off (start := 2) fun ⟨u, _⟩ => - Strata.ArgF.fromIon u - return .spacePrefixedListNonEmpty ann args | str => throw s!"Unexpected identifier {str}" termination_by v @@ -683,10 +663,6 @@ decreasing_by decreasing_tactic · have _ : sizeOf u < sizeOf sexp := by decreasing_tactic decreasing_tactic - · have _ : sizeOf u < sizeOf sexp := by decreasing_tactic - decreasing_tactic - · have _ : sizeOf u < sizeOf sexp := by decreasing_tactic - decreasing_tactic end diff --git a/Strata/DDM/Parser.lean b/Strata/DDM/Parser.lean index 146586b42..2f52f4180 100644 --- a/Strata/DDM/Parser.lean +++ b/Strata/DDM/Parser.lean @@ -775,7 +775,7 @@ def checkLeftRec (thisCatName : QualifiedIdent) (argDecls : ArgDecls) (as : List .invalid mf!"Leading symbol cannot be recursive call to {c}" else .isLeading as - | q`Init.SpaceSepBy | q`Init.SpaceSepByNonEmpty | q`Init.SpacePrefixedBy | q`Init.SpacePrefixedByNonEmpty => + | q`Init.SpaceSepBy | q`Init.SpacePrefixedBy => assert! cat.args.size = 1 let c := cat.args[0]! if c.name == thisCatName then @@ -934,30 +934,27 @@ def many1Parser (p : Parser) : Parser := { s } +/-- Helper to choose between sepByParser and sepBy1Parser based on nonempty flag -/ +private def commaSepByParserHelper (nonempty : Bool) (p : Parser) : Parser := + if nonempty then + sepBy1Parser p (symbolNoAntiquot ",") + else + sepByParser p (symbolNoAntiquot ",") + /-- Parser function for given syntax category -/ -partial def catParser (ctx : ParsingContext) (cat : SyntaxCat) : Except SyntaxCat Parser := +partial def catParser (ctx : ParsingContext) (cat : SyntaxCat) (metadata : Metadata := {}) : Except SyntaxCat Parser := match cat.name with | q`Init.CommaSepBy => assert! cat.args.size = 1 - (sepByParser · (symbolNoAntiquot ",")) <$> catParser ctx cat.args[0]! - | q`Init.SpaceSepBy => - assert! cat.args.size = 1 - manyParser <$> catParser ctx cat.args[0]! - | q`Init.SpaceSepByNonEmpty => + let isNonempty := q`StrataDDL.nonempty ∈ metadata + commaSepByParserHelper isNonempty <$> catParser ctx cat.args[0]! + | q`Init.SpaceSepBy | q`Init.SpacePrefixedBy | q`Init.Seq => assert! cat.args.size = 1 - many1Parser <$> catParser ctx cat.args[0]! - | q`Init.SpacePrefixedBy => - assert! cat.args.size = 1 - manyParser <$> catParser ctx cat.args[0]! - | q`Init.SpacePrefixedByNonEmpty => - assert! cat.args.size = 1 - many1Parser <$> catParser ctx cat.args[0]! + let isNonempty := q`StrataDDL.nonempty ∈ metadata + (if isNonempty then many1Parser else manyParser) <$> catParser ctx cat.args[0]! | q`Init.Option => assert! cat.args.size = 1 optionalNoAntiquot <$> catParser ctx cat.args[0]! - | q`Init.Seq => - assert! cat.args.size = 1 - manyParser <$> catParser ctx cat.args[0]! | qid => if cat.args.isEmpty then .ok (atomCatParser ctx qid) @@ -977,7 +974,7 @@ private def prependSyntaxDefAtomParser (ctx : ParsingContext) (argDecls : ArgDec let addParser (p : Parser) := let q : Parser := Lean.Parser.adaptCacheableContext ({ · with prec }) p q >> r - match catParser ctx argDecls[v].kind.categoryOf with + match catParser ctx argDecls[v].kind.categoryOf argDecls[v].metadata with | .ok p => addParser p | .error c => diff --git a/Strata/DL/SMT/DDMTransform/Parse.lean b/Strata/DL/SMT/DDMTransform/Parse.lean index 5042603f1..57a5831b8 100644 --- a/Strata/DL/SMT/DDMTransform/Parse.lean +++ b/Strata/DL/SMT/DDMTransform/Parse.lean @@ -199,7 +199,7 @@ op ind_symbol (@[unwrap] s:Symbol) : Index => s; op iden_simple (s:Symbol) : SMTIdentifier => s; -op iden_indexed (s:Symbol, si:SpaceSepByNonEmpty Index) : SMTIdentifier => +op iden_indexed (s:Symbol, @[nonempty] si:SpaceSepBy Index) : SMTIdentifier => "(" "_ " s " " si ")"; @@ -207,7 +207,7 @@ op iden_indexed (s:Symbol, si:SpaceSepByNonEmpty Index) : SMTIdentifier => category SMTSort; op smtsort_ident (s:SMTIdentifier) : SMTSort => s; -op smtsort_param (s:SMTIdentifier, sl:SpaceSepByNonEmpty SMTSort) : SMTSort +op smtsort_param (s:SMTIdentifier, @[nonempty] sl:SpaceSepBy SMTSort) : SMTSort => "(" s " " sl ")"; @@ -240,18 +240,18 @@ op sorted_var (s:Symbol, so:SMTSort) : SortedVar => "(" s " " so ")"; op spec_constant_term (sc:SpecConstant) : Term => sc; op qual_identifier (qi:QualIdentifier) : Term => qi; -op qual_identifier_args (qi:QualIdentifier, ts:SpaceSepByNonEmpty Term) : Term => +op qual_identifier_args (qi:QualIdentifier, @[nonempty] ts:SpaceSepBy Term) : Term => "(" qi " " ts ")"; -op let_smt (vbps: SpaceSepByNonEmpty ValBinding, t:Term) : Term => +op let_smt (@[nonempty] vbps: SpaceSepBy ValBinding, t:Term) : Term => "(" "let" "(" vbps ")" t ")"; -op lambda_smt (svs: SpaceSepByNonEmpty SortedVar, t:Term) : Term => +op lambda_smt (@[nonempty] svs: SpaceSepBy SortedVar, t:Term) : Term => "(" "lambda" "(" svs ")" t ")"; -op forall_smt (svs: SpaceSepByNonEmpty SortedVar, t:Term) : Term => +op forall_smt (@[nonempty] svs: SpaceSepBy SortedVar, t:Term) : Term => "(" "forall" "(" svs ")" t ")"; -op exists_smt (svs: SpaceSepByNonEmpty SortedVar, t:Term) : Term => +op exists_smt (@[nonempty] svs: SpaceSepBy SortedVar, t:Term) : Term => "(" "exists" "(" svs ")" t ")"; -op bang (t:Term, attrs:SpaceSepByNonEmpty Attribute) : Term => +op bang (t:Term, @[nonempty] attrs:SpaceSepBy Attribute) : Term => "(" "!" t " " attrs ")"; @@ -321,9 +321,9 @@ op constructor_dec (s:Symbol, sdl:SpaceSepBy SelectorDec) : ConstructorDec => "(" s sdl ")"; category DatatypeDec; -op datatype_dec (cs:SpaceSepByNonEmpty ConstructorDec) : DatatypeDec +op datatype_dec (@[nonempty] cs:SpaceSepBy ConstructorDec) : DatatypeDec => "(" cs ")"; -op datatype_dec_par (symbols: SpaceSepByNonEmpty Symbol, cs:SpaceSepByNonEmpty ConstructorDec) : DatatypeDec +op datatype_dec_par (@[nonempty] symbols: SpaceSepBy Symbol, @[nonempty] cs:SpaceSepBy ConstructorDec) : DatatypeDec => "(" "par " "(" symbols ")" "(" cs ")" ")"; category FunctionDec; @@ -356,7 +356,7 @@ op declare_datatype (s:Symbol, so:DatatypeDec) : Command => "(" "declare-datatype " s so ")"; // The size of SortDec and DatatypeDec must be equal, but omit the check in // this DDM definition because its representation can be quite ugly. -op declare_datatypes (s:SpaceSepByNonEmpty SortDec, so:SpaceSepByNonEmpty DatatypeDec) : Command => +op declare_datatypes (@[nonempty] s:SpaceSepBy SortDec, @[nonempty] so:SpaceSepBy DatatypeDec) : Command => "(" "declare-datatypes" "(" s ")" "(" so ")" ")"; op declare_fun (s:Symbol, sol:SpaceSepBy SMTSort, range:SMTSort) : Command => "(" "declare-fun " s "(" sol ")" range ")"; @@ -370,7 +370,7 @@ op define_fun (fdef:FunctionDef) : Command => "(" "define-fun " fdef ")"; op define_fun_rec (fdef:FunctionDef) : Command => "(" "define-fun-rec " fdef ")"; -op define_funs_rec (fdefs:SpaceSepByNonEmpty FunctionDef, terms:SpaceSepByNonEmpty Term) : Command => +op define_funs_rec (@[nonempty] fdefs:SpaceSepBy FunctionDef, @[nonempty] terms:SpaceSepBy Term) : Command => "(" "define-funs-rec" "(" fdefs ")" "(" terms ")" ")"; op define_sort (s:Symbol, sl:Seq Symbol, so:SMTSort) : Command => "(" "define-sort " s "(" sl ")" so ")"; @@ -384,7 +384,7 @@ op get_option (kw:Keyword) : Command => "(" "get-option " kw ")"; op get_proof () : Command => "(" "get-proof" ")"; op get_unsat_assumptions () : Command => "(" "get-unsat-assumptions" ")"; op get_unsat_core () : Command => "(" "get-unsat-core" ")"; -op get_value (tl:SpaceSepByNonEmpty Term) : Command => +op get_value (@[nonempty] tl:SpaceSepBy Term) : Command => "(" "get-value" "(" tl ")" ")"; op cmd_pop (n:Num) : Command => "(" "pop " n ")"; op cmd_push (n:Num) : Command => "(" "push " n ")"; diff --git a/StrataTest/DDM/NonemptyAttribute.lean b/StrataTest/DDM/NonemptyAttribute.lean new file mode 100644 index 000000000..66bae3dee --- /dev/null +++ b/StrataTest/DDM/NonemptyAttribute.lean @@ -0,0 +1,100 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.DDM.Integration.Lean + +/-! +# Tests for @[nonempty] attribute on list constructs + +This file tests that the @[nonempty] attribute properly enforces non-empty lists +for CommaSepBy, SpaceSepBy, and SpacePrefixedBy constructs. +-/ + +#dialect +dialect NonemptyTest; + +category Item; +op item (n : Num) : Item => n; + +// Operations with @[nonempty] - require at least one element +op comma1 (@[nonempty] items : CommaSepBy Item) : Command => "comma1(" items ")"; +op space1 (@[nonempty] items : SpaceSepBy Item) : Command => "space1(" items ")"; +op prefixed1 (@[nonempty] items : SpacePrefixedBy Item) : Command => "prefixed1(" items ")"; + +// Operations without @[nonempty] - allow zero elements +op comma0 (items : CommaSepBy Item) : Command => "comma0(" items ")"; +op space0 (items : SpaceSepBy Item) : Command => "space0(" items ")"; + +#end + +namespace NonemptyTest + +#strata_gen NonemptyTest + +end NonemptyTest + +namespace NonemptyTest.Tests + +-- Test that @[nonempty] CommaSepBy accepts non-empty lists +#guard_msgs in +private def test_nonempty_comma_success := #strata +program NonemptyTest; +comma1(1, 2, 3) +#end + +-- Test that @[nonempty] CommaSepBy rejects empty lists +/-- error: expected expected at least one element -/ +#guard_msgs in +private def test_nonempty_comma_empty := #strata +program NonemptyTest; +comma1() +#end + +-- Test that @[nonempty] SpaceSepBy accepts non-empty lists +#guard_msgs in +private def test_nonempty_space_success := #strata +program NonemptyTest; +space1(1 2 3) +#end + +-- Test that @[nonempty] SpaceSepBy rejects empty lists +/-- error: expected expected at least one element -/ +#guard_msgs in +private def test_nonempty_space_empty := #strata +program NonemptyTest; +space1() +#end + +-- Test that @[nonempty] SpacePrefixedBy accepts non-empty lists +#guard_msgs in +private def test_nonempty_prefixed_success := #strata +program NonemptyTest; +prefixed1(1 2 3) +#end + +-- Test that @[nonempty] SpacePrefixedBy rejects empty lists +/-- error: expected expected at least one element -/ +#guard_msgs in +private def test_nonempty_prefixed_empty := #strata +program NonemptyTest; +prefixed1() +#end + +-- Test that regular (non-@[nonempty]) CommaSepBy allows empty lists +#guard_msgs in +private def test_maybe_empty_comma := #strata +program NonemptyTest; +comma0() +#end + +-- Test that regular (non-@[nonempty]) SpaceSepBy allows empty lists +#guard_msgs in +private def test_maybe_empty_space := #strata +program NonemptyTest; +space0() +#end + +end NonemptyTest.Tests diff --git a/StrataTest/Languages/B3/DDMFormatTests.lean b/StrataTest/Languages/B3/DDMFormatTests.lean index 93b427d0e..c4ee0fa0d 100644 --- a/StrataTest/Languages/B3/DDMFormatTests.lean +++ b/StrataTest/Languages/B3/DDMFormatTests.lean @@ -117,9 +117,7 @@ mutual | .seq () entries => .seq default (entries.map argFUnitToSourceRange) | .commaSepList () entries => .commaSepList default (entries.map argFUnitToSourceRange) | .spaceSepList () entries => .spaceSepList default (entries.map argFUnitToSourceRange) - | .spaceSepListNonEmpty () entries => .spaceSepListNonEmpty default (entries.map argFUnitToSourceRange) | .spacePrefixedList () entries => .spacePrefixedList default (entries.map argFUnitToSourceRange) - | .spacePrefixedListNonEmpty () entries => .spacePrefixedListNonEmpty default (entries.map argFUnitToSourceRange) partial def typeExprFUnitToSourceRange : TypeExprF Unit → TypeExprF SourceRange | .ident () tp a => .ident default tp (a.map typeExprFUnitToSourceRange) From 4c8bf6477c2fb6dd4e3be88a9ab36160fe31a3e5 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 15 Jan 2026 04:16:56 +0100 Subject: [PATCH 04/11] Refactor list constructors to use unified SepFormat and rename SpacePrefixedBy - Unify commaSepList, spaceSepList, spacePrefixedList into single .seq constructor - Add SepFormat enum (.none, .comma, .space, .spacePrefix) to specify formatting - Rename SpacePrefixedBy to SpacePrefixSepBy throughout codebase - Remove unused spacePrefixedParser and spacePrefixed1Parser functions - Update all files to use new unified structure (AST, Format, Ion, ToExpr, OfAstM, Gen) - Update dialect translation files (Boogie, C_Simp, SMT) - Rename ofSpacePrefixedByM to ofSpacePrefixSepByM - Update documentation in docs/verso/DDMDoc.lean: - Document SpaceSepBy and SpacePrefixSepBy categories - Document @[nonempty] attribute for enforcing non-empty lists - Clarify parsing vs formatting differences for list categories --- Strata/DDM/AST.lean | 29 ++++++------- Strata/DDM/BuiltinDialects/Init.lean | 4 +- Strata/DDM/Elab/Core.lean | 4 +- Strata/DDM/Elab/Tree.lean | 8 ++-- Strata/DDM/Format.lean | 42 ++++++++++--------- Strata/DDM/Integration/Lean/Gen.lean | 34 ++++++--------- Strata/DDM/Integration/Lean/OfAstM.lean | 14 +++---- Strata/DDM/Integration/Lean/ToExpr.lean | 25 ++++++----- Strata/DDM/Ion.lean | 31 ++++++-------- Strata/DDM/Parser.lean | 39 +---------------- Strata/DL/SMT/DDMTransform/Parse.lean | 10 +---- Strata/DL/SMT/DDMTransform/Translate.lean | 14 +------ .../Boogie/DDMTransform/Translate.lean | 12 +++--- .../C_Simp/DDMTransform/Translate.lean | 6 +-- StrataTest/DDM/NonemptyAttribute.lean | 8 ++-- StrataTest/Languages/B3/DDMFormatTests.lean | 5 +-- docs/verso/DDMDoc.lean | 17 +++++++- 17 files changed, 124 insertions(+), 178 deletions(-) diff --git a/Strata/DDM/AST.lean b/Strata/DDM/AST.lean index 64bacfc91..bffef440a 100644 --- a/Strata/DDM/AST.lean +++ b/Strata/DDM/AST.lean @@ -140,6 +140,14 @@ termination_by d end TypeExprF +/-- Separator format for sequence formatting -/ +inductive SepFormat where +| none -- No separator (original Seq) +| comma -- Comma separator (CommaSepBy) +| space -- Space separator (SpaceSepBy) +| spacePrefix -- Space before each element (SpacePrefixSepBy) +deriving Inhabited, Repr, BEq + mutual inductive ExprF (α : Type) : Type where @@ -166,10 +174,7 @@ inductive ArgF (α : Type) : Type where | strlit (ann : α) (i : String) | bytes (ann : α) (a : ByteArray) | option (ann : α) (l : Option (ArgF α)) -| seq (ann : α) (l : Array (ArgF α)) -| commaSepList (ann : α) (l : Array (ArgF α)) -| spaceSepList (ann : α) (l : Array (ArgF α)) -| spacePrefixedList (ann : α) (l : Array (ArgF α)) +| seq (ann : α) (sep : SepFormat) (l : Array (ArgF α)) deriving Inhabited, Repr end @@ -193,10 +198,7 @@ def ArgF.ann {α : Type} : ArgF α → α | .bytes ann _ => ann | .strlit ann _ => ann | .option ann _ => ann -| .seq ann _ => ann -| .commaSepList ann _ => ann -| .spaceSepList ann _ => ann -| .spacePrefixedList ann _ => ann +| .seq ann _ _ => ann end @@ -292,10 +294,8 @@ private def ArgF.beq {α} [BEq α] (a1 a2 : ArgF α) : Bool := | .none, .none => true | .some v1, .some v2 => ArgF.beq v1 v2 | _, _ => false - | .seq a1 v1, .seq a2 v2 => - a1 == a2 && ArgF.array_beq v1 v2 - | .commaSepList a1 v1, .commaSepList a2 v2 => - a1 == a2 && ArgF.array_beq v1 v2 + | .seq a1 sep1 v1, .seq a2 sep2 v2 => + a1 == a2 && sep1 == sep2 && ArgF.array_beq v1 v2 | _, _ => false termination_by sizeOf a1 @@ -1294,10 +1294,7 @@ partial def foldOverArgBindingSpecs {α β} | .expr _ | .type _ | .cat _ | .ident .. | .num .. | .decimal .. | .bytes .. | .strlit .. => init | .option _ none => init | .option _ (some a) => foldOverArgBindingSpecs m f init a - | .seq _ a => a.attach.foldl (init := init) fun init ⟨a, _⟩ => foldOverArgBindingSpecs m f init a - | .commaSepList _ a => a.attach.foldl (init := init) fun init ⟨a, _⟩ => foldOverArgBindingSpecs m f init a - | .spaceSepList _ a => a.attach.foldl (init := init) fun init ⟨a, _⟩ => foldOverArgBindingSpecs m f init a - | .spacePrefixedList _ a => a.attach.foldl (init := init) fun init ⟨a, _⟩ => foldOverArgBindingSpecs m f init a + | .seq _ _ a => a.attach.foldl (init := init) fun init ⟨a, _⟩ => foldOverArgBindingSpecs m f init a /-- Invoke a function `f` over each of the declaration specifications for an operator. diff --git a/Strata/DDM/BuiltinDialects/Init.lean b/Strata/DDM/BuiltinDialects/Init.lean index 1c9942297..4af5c68ef 100644 --- a/Strata/DDM/BuiltinDialects/Init.lean +++ b/Strata/DDM/BuiltinDialects/Init.lean @@ -19,7 +19,7 @@ def SyntaxCat.mkOpt (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init. def SyntaxCat.mkSeq (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.Seq, args := #[c] } def SyntaxCat.mkCommaSepBy (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.CommaSepBy, args := #[c] } def SyntaxCat.mkSpaceSepBy (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.SpaceSepBy, args := #[c] } -def SyntaxCat.mkSpacePrefixedBy (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.SpacePrefixedBy, args := #[c] } +def SyntaxCat.mkSpacePrefixSepBy (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.SpacePrefixSepBy, args := #[c] } def initDialect : Dialect := BuiltinM.create! "Init" #[] do let Ident : ArgDeclKind := .cat <| .atom .none q`Init.Ident @@ -54,7 +54,7 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do declareCat q`Init.SpaceSepBy #["a"] - declareCat q`Init.SpacePrefixedBy #["a"] + declareCat q`Init.SpacePrefixSepBy #["a"] let QualifiedIdent := q`Init.QualifiedIdent declareCat QualifiedIdent diff --git a/Strata/DDM/Elab/Core.lean b/Strata/DDM/Elab/Core.lean index 83d47f229..da577f7a1 100644 --- a/Strata/DDM/Elab/Core.lean +++ b/Strata/DDM/Elab/Core.lean @@ -1136,13 +1136,13 @@ partial def catElaborator (c : SyntaxCat) : TypingContext → Syntax → ElabM T let (args, resultCtx) ← stx.getSepArgs.foldlM f (#[], tctx) let info : SpaceSepInfo := { inputCtx := tctx, loc := loc, args := args.map (·.arg), resultCtx } pure <| .node (.ofSpaceSepInfo info) args - | q`Init.SpacePrefixedBy => + | q`Init.SpacePrefixSepBy => assert! c.args.size = 1 let a := c.args[0]! let f := elabManyElement (catElaborator a) fun tctx stx => do let some loc := mkSourceRange? stx - | panic! s!"spacePrefixedBy missing source location {repr stx}" + | panic! s!"spacePrefixSepBy missing source location {repr stx}" let (args, resultCtx) ← stx.getArgs.foldlM f (#[], tctx) let info : SpacePrefixedInfo := { inputCtx := tctx, loc := loc, args := args.map (·.arg), resultCtx } pure <| .node (.ofSpacePrefixedInfo info) args diff --git a/Strata/DDM/Elab/Tree.lean b/Strata/DDM/Elab/Tree.lean index cde90ae05..59a221bd9 100644 --- a/Strata/DDM/Elab/Tree.lean +++ b/Strata/DDM/Elab/Tree.lean @@ -352,10 +352,10 @@ def arg : Tree → Arg | #[x] => some x.arg | _ => panic! "Unexpected option" .option info.loc r - | .ofSeqInfo info => .seq info.loc info.args - | .ofCommaSepInfo info => .commaSepList info.loc info.args - | .ofSpaceSepInfo info => .spaceSepList info.loc info.args - | .ofSpacePrefixedInfo info => .spacePrefixedList info.loc info.args + | .ofSeqInfo info => .seq info.loc .none info.args + | .ofCommaSepInfo info => .seq info.loc .comma info.args + | .ofSpaceSepInfo info => .seq info.loc .space info.args + | .ofSpacePrefixedInfo info => .seq info.loc .spacePrefix info.args theorem sizeOf_children (t : Tree) (i : Nat) (p : i < t.children.size) : sizeOf t[i] < sizeOf t := by match t with diff --git a/Strata/DDM/Format.lean b/Strata/DDM/Format.lean index 8cc52efb4..1fc44110e 100644 --- a/Strata/DDM/Format.lean +++ b/Strata/DDM/Format.lean @@ -378,26 +378,28 @@ private partial def ArgF.mformatM {α} : ArgF α → FormatM PrecFormat match ma with | none => pure (.atom .nil) | some a => a.mformatM -| .seq _ entries => do - .atom <$> entries.foldlM (init := .nil) fun p a => - return (p ++ (← a.mformatM).format) -| .commaSepList _ entries => do - if z : entries.size = 0 then - pure (.atom .nil) - else do - let f i q s := return s ++ ", " ++ (← entries[i].mformatM).format - let a := (← entries[0].mformatM).format - .atom <$> entries.size.foldlM f (start := 1) a -| .spaceSepList _ entries => do - if z : entries.size = 0 then - pure (.atom .nil) - else do - let f i q s := return s ++ " " ++ (← entries[i].mformatM).format - let a := (← entries[0].mformatM).format - .atom <$> entries.size.foldlM f (start := 1) a -| .spacePrefixedList _ entries => do - .atom <$> entries.foldlM (init := .nil) fun p a => - return (p ++ " " ++ (← a.mformatM).format) +| .seq _ sep entries => do + match sep with + | .none => + .atom <$> entries.foldlM (init := .nil) fun p a => + return (p ++ (← a.mformatM).format) + | .comma => + if z : entries.size = 0 then + pure (.atom .nil) + else do + let f i q s := return s ++ ", " ++ (← entries[i].mformatM).format + let a := (← entries[0].mformatM).format + .atom <$> entries.size.foldlM f (start := 1) a + | .space => + if z : entries.size = 0 then + pure (.atom .nil) + else do + let f i q s := return s ++ " " ++ (← entries[i].mformatM).format + let a := (← entries[0].mformatM).format + .atom <$> entries.size.foldlM f (start := 1) a + | .spacePrefix => + .atom <$> entries.foldlM (init := .nil) fun p a => + return (p ++ " " ++ (← a.mformatM).format) private partial def ppArgs (f : StrataFormat) (rargs : Array Arg) : FormatM PrecFormat := if rargs.isEmpty then diff --git a/Strata/DDM/Integration/Lean/Gen.lean b/Strata/DDM/Integration/Lean/Gen.lean index 7e26769c1..62d814201 100644 --- a/Strata/DDM/Integration/Lean/Gen.lean +++ b/Strata/DDM/Integration/Lean/Gen.lean @@ -564,7 +564,7 @@ partial def ppCatWithUnwrap (annType : Ident) (c : SyntaxCat) (unwrap : Bool) : return mkCApp ``Ann #[mkCApp ``Array #[args[0]], annType] | q`Init.SpaceSepBy, 1 => return mkCApp ``Ann #[mkCApp ``Array #[args[0]], annType] - | q`Init.SpacePrefixedBy, 1 => + | q`Init.SpacePrefixSepBy, 1 => return mkCApp ``Ann #[mkCApp ``Array #[args[0]], annType] | q`Init.Option, 1 => return mkCApp ``Ann #[mkCApp ``Option #[args[0]], annType] @@ -733,7 +733,8 @@ partial def toAstApplyArg (vn : Name) (cat : SyntaxCat) (unwrap : Bool := false) ←`(fun ⟨$canE, _⟩ => $t), mkCApp ``Array.attach #[mkCApp ``Ann.val #[v]] ] - return mkAnnWithTerm ``ArgF.commaSepList v args + let sepExpr := mkCApp ``SepFormat.comma #[] + return mkCApp ``ArgF.seq #[mkCApp ``Ann.ann #[v], sepExpr, args] | q`Init.SpaceSepBy => do assert! cat.args.size = 1 let c := cat.args[0]! @@ -744,8 +745,9 @@ partial def toAstApplyArg (vn : Name) (cat : SyntaxCat) (unwrap : Bool := false) ←`(fun ⟨$canE, _⟩ => $t), mkCApp ``Array.attach #[mkCApp ``Ann.val #[v]] ] - return mkAnnWithTerm ``ArgF.spaceSepList v args - | q`Init.SpacePrefixedBy => do + let sepExpr := mkCApp ``SepFormat.space #[] + return mkCApp ``ArgF.seq #[mkCApp ``Ann.ann #[v], sepExpr, args] + | q`Init.SpacePrefixSepBy => do assert! cat.args.size = 1 let c := cat.args[0]! let e ← genFreshLeanName "e" @@ -755,7 +757,8 @@ partial def toAstApplyArg (vn : Name) (cat : SyntaxCat) (unwrap : Bool := false) ←`(fun ⟨$canE, _⟩ => $t), mkCApp ``Array.attach #[mkCApp ``Ann.val #[v]] ] - return mkAnnWithTerm ``ArgF.spacePrefixedList v args + let sepExpr := mkCApp ``SepFormat.spacePrefix #[] + return mkCApp ``ArgF.seq #[mkCApp ``Ann.ann #[v], sepExpr, args] | q`Init.Option => do assert! cat.args.size = 1 let c := cat.args[0]! @@ -777,7 +780,8 @@ partial def toAstApplyArg (vn : Name) (cat : SyntaxCat) (unwrap : Bool := false) ←`(fun ⟨$canE, _⟩ => $t), mkCApp ``Array.attach #[mkCApp ``Ann.val #[v]] ] - return mkAnnWithTerm ``ArgF.seq v args + let sepExpr := mkCApp ``SepFormat.none #[] + return mkCApp ``ArgF.seq #[mkCApp ``Ann.ann #[v], sepExpr, args] | qid => do assert! cat.args.size = 0 let toAst ← toAstIdentM qid @@ -932,21 +936,11 @@ partial def getOfIdentArgWithUnwrap (varName : String) (cat : SyntaxCat) (unwrap let (vc, vi) ← genFreshIdentPair varName let body ← getOfIdentArg varName c vi ``(OfAstM.ofSpaceSepByM $e fun $vc _ => $body) - | q`Init.SpaceSepByNonEmpty => do + | q`Init.SpacePrefixSepBy => do let c := cat.args[0]! let (vc, vi) ← genFreshIdentPair varName let body ← getOfIdentArg varName c vi - ``(OfAstM.ofSpaceSepByNonEmptyM $e fun $vc _ => $body) - | q`Init.SpacePrefixedBy => do - let c := cat.args[0]! - let (vc, vi) ← genFreshIdentPair varName - let body ← getOfIdentArg varName c vi - ``(OfAstM.ofSpacePrefixedByM $e fun $vc _ => $body) - | q`Init.SpacePrefixedByNonEmpty => do - let c := cat.args[0]! - let (vc, vi) ← genFreshIdentPair varName - let body ← getOfIdentArg varName c vi - ``(OfAstM.ofSpacePrefixedByNonEmptyM $e fun $vc _ => $body) + ``(OfAstM.ofSpacePrefixSepByM $e fun $vc _ => $body) | q`Init.Option => do let c := cat.args[0]! let (vc, vi) ← genFreshIdentPair varName @@ -1138,9 +1132,7 @@ def checkInhabited (cat : QualifiedIdent) (ops : Array DefaultCtor) : StateT Inh | q`Init.Seq => true | q`Init.CommaSepBy => true | q`Init.SpaceSepBy => true - | q`Init.SpaceSepByNonEmpty => true - | q`Init.SpacePrefixedBy => true - | q`Init.SpacePrefixedByNonEmpty => true + | q`Init.SpacePrefixSepBy => true | q`Init.Option => true | c => c ∈ inhabited if !isInhabited then diff --git a/Strata/DDM/Integration/Lean/OfAstM.lean b/Strata/DDM/Integration/Lean/OfAstM.lean index 781d14ebd..6c027950f 100644 --- a/Strata/DDM/Integration/Lean/OfAstM.lean +++ b/Strata/DDM/Integration/Lean/OfAstM.lean @@ -171,18 +171,18 @@ def ofCommaSepByM {α β} [Repr α] [SizeOf α] (act : ∀(e : ArgF α), sizeOf e < sizeOf arg → OfAstM β) : OfAstM (Ann (Array β) α) := match arg with - | .commaSepList ann a => do + | .seq ann .comma a => do let val ← a.attach.mapM fun ⟨v, vIn⟩ => do act v (by decreasing_tactic) pure { ann := ann, val := val } - | _ => throwExpected "seq" arg + | _ => throwExpected "commaSepBy" arg def ofSeqM {α β} [Repr α] [SizeOf α] (arg : ArgF α) (act : ∀(e : ArgF α), sizeOf e < sizeOf arg → OfAstM β) : OfAstM (Ann (Array β) α) := match arg with - | .seq ann a => do + | .seq ann .none a => do let val ← a.attach.mapM fun ⟨v, vIn⟩ => act v (by decreasing_tactic) pure { ann := ann, val := val } @@ -193,22 +193,22 @@ def ofSpaceSepByM {α β} [Repr α] [SizeOf α] (act : ∀(e : ArgF α), sizeOf e < sizeOf arg → OfAstM β) : OfAstM (Ann (Array β) α) := match arg with - | .spaceSepList ann a => do + | .seq ann .space a => do let val ← a.attach.mapM fun ⟨v, vIn⟩ => act v (by decreasing_tactic) pure { ann := ann, val := val } | _ => throwExpected "spaceSepBy" arg -def ofSpacePrefixedByM {α β} [Repr α] [SizeOf α] +def ofSpacePrefixSepByM {α β} [Repr α] [SizeOf α] (arg : ArgF α) (act : ∀(e : ArgF α), sizeOf e < sizeOf arg → OfAstM β) : OfAstM (Ann (Array β) α) := match arg with - | .spacePrefixedList ann a => do + | .seq ann .spacePrefix a => do let val ← a.attach.mapM fun ⟨v, vIn⟩ => act v (by decreasing_tactic) pure { ann := ann, val := val } - | _ => throwExpected "spacePrefixedBy" arg + | _ => throwExpected "spacePrefixSepBy" arg /-- Get the expression at index `lvl` in the arguments. diff --git a/Strata/DDM/Integration/Lean/ToExpr.lean b/Strata/DDM/Integration/Lean/ToExpr.lean index c7c4e4607..cb9fcadea 100644 --- a/Strata/DDM/Integration/Lean/ToExpr.lean +++ b/Strata/DDM/Integration/Lean/ToExpr.lean @@ -19,6 +19,18 @@ namespace Strata open Lean +namespace SepFormat + +instance : ToExpr SepFormat where + toTypeExpr := private mkConst ``SepFormat + toExpr + | .none => mkConst ``SepFormat.none + | .comma => mkConst ``SepFormat.comma + | .space => mkConst ``SepFormat.space + | .spacePrefix => mkConst ``SepFormat.spacePrefix + +end SepFormat + namespace QualifiedIdent instance : ToExpr QualifiedIdent where @@ -159,18 +171,9 @@ private def ArgF.toExpr {α} [ToExpr α] : ArgF α → Lean.Expr | .option ann a => let tpe := ArgF.typeExpr α astAnnExpr! ArgF.option ann (optionToExpr tpe <| a.attach.map fun ⟨e, _⟩ => e.toExpr) -| .seq ann a => - let tpe := ArgF.typeExpr α - astAnnExpr! ArgF.seq ann <| arrayToExpr .zero tpe <| a.map (·.toExpr) -| .commaSepList ann a => - let tpe := ArgF.typeExpr α - astAnnExpr! ArgF.commaSepList ann <| arrayToExpr .zero tpe <| a.map (·.toExpr) -| .spaceSepList ann a => - let tpe := ArgF.typeExpr α - astAnnExpr! ArgF.spaceSepList ann <| arrayToExpr .zero tpe <| a.map (·.toExpr) -| .spacePrefixedList ann a => +| .seq ann sep a => let tpe := ArgF.typeExpr α - astAnnExpr! ArgF.spacePrefixedList ann <| arrayToExpr .zero tpe <| a.map (·.toExpr) + astAnnExpr! ArgF.seq ann (toExpr sep) <| arrayToExpr .zero tpe <| a.map (·.toExpr) termination_by a => sizeOf a private protected def OperationF.toExpr {α} [ToExpr α] (op : OperationF α) : Lean.Expr := diff --git a/Strata/DDM/Ion.lean b/Strata/DDM/Ion.lean index 065b4276f..560c89632 100644 --- a/Strata/DDM/Ion.lean +++ b/Strata/DDM/Ion.lean @@ -505,22 +505,15 @@ private protected def ArgF.toIon {α} [ToIon α] (refs : SymbolIdCache) (arg : A | some a => args := args.push (← a.toIon refs ) return .sexp args - | .seq ann l => do - let args : Array (Ion _) := #[ ionSymbol! "seq", ← toIon ann ] + | .seq ann sep l => do + let annIon ← toIon ann + let args : Array (Ion _) := match sep with + | .none => #[ ionSymbol! "seq", annIon ] + | .comma => #[ ionSymbol! "commaSepList", annIon ] + | .space => #[ ionSymbol! "spaceSepList", annIon ] + | .spacePrefix => #[ ionSymbol! "spacePrefixedList", annIon ] let args ← l.attach.mapM_off (init := args) fun ⟨v, _⟩ => v.toIon refs return .sexp args - | .commaSepList ann l => do - let args : Array (Ion _) := #[ ionSymbol! "commaSepList", ← toIon ann ] - let args ← l.attach.mapM_off (init := args) fun ⟨v, _⟩ => v.toIon refs - return .sexp args - | .spaceSepList ann l => do - let args : Array (Ion _) := #[ ionSymbol! "spaceSepList", ← toIon ann ] - let args ← l.attach.mapM_off (init := args) fun ⟨v, _h⟩ => v.toIon refs - return .sexp args - | .spacePrefixedList ann l => do - let args : Array (Ion _) := #[ ionSymbol! "spacePrefixedList", ← toIon ann ] - let args ← l.attach.mapM_off (init := args) fun ⟨v, _h⟩ => v.toIon refs - return .sexp args termination_by sizeOf arg decreasing_by all_goals decreasing_tactic @@ -626,25 +619,25 @@ private protected def ArgF.fromIon {α} [FromIon α] (v : Ion SymbolId) : FromIo let ann ← fromIon sexp[1] let args ← sexp.attach.mapM_off (start := 2) fun ⟨u, _⟩ => Strata.ArgF.fromIon u - return .seq ann args + return .seq ann .none args | "commaSepList" => do - let ⟨p⟩ ← .checkArgMin "seq" sexp 2 + let ⟨p⟩ ← .checkArgMin "commaSepList" sexp 2 let ann ← fromIon sexp[1] let args ← sexp.attach.mapM_off (start := 2) fun ⟨u, _⟩ => Strata.ArgF.fromIon u - return .commaSepList ann args + return .seq ann .comma args | "spaceSepList" => do let ⟨p⟩ ← .checkArgMin "spaceSepList" sexp 2 let ann ← fromIon sexp[1] let args ← sexp.attach.mapM_off (start := 2) fun ⟨u, _⟩ => Strata.ArgF.fromIon u - return .spaceSepList ann args + return .seq ann .space args | "spacePrefixedList" => do let ⟨p⟩ ← .checkArgMin "spacePrefixedList" sexp 2 let ann ← fromIon sexp[1] let args ← sexp.attach.mapM_off (start := 2) fun ⟨u, _⟩ => Strata.ArgF.fromIon u - return .spacePrefixedList ann args + return .seq ann .spacePrefix args | str => throw s!"Unexpected identifier {str}" termination_by v diff --git a/Strata/DDM/Parser.lean b/Strata/DDM/Parser.lean index 2f52f4180..1771ff696 100644 --- a/Strata/DDM/Parser.lean +++ b/Strata/DDM/Parser.lean @@ -775,7 +775,7 @@ def checkLeftRec (thisCatName : QualifiedIdent) (argDecls : ArgDecls) (as : List .invalid mf!"Leading symbol cannot be recursive call to {c}" else .isLeading as - | q`Init.SpaceSepBy | q`Init.SpacePrefixedBy => + | q`Init.SpaceSepBy | q`Init.SpacePrefixSepBy => assert! cat.args.size = 1 let c := cat.args[0]! if c.name == thisCatName then @@ -865,41 +865,6 @@ private def sepBy1Parser (p sep : Parser) (allowTrailingSep : Bool := false) : P s } -private def spacePrefixedParser (p : Parser) : Parser := { - info := noFirstTokenInfo p.info - fn := fun c s => - let s := manyFn (andthenFn (symbolNoAntiquot " ").fn p.fn) c s - if s.hasError then - s - else - match s.stxStack.back with - | .node .none _k args => - if args.isEmpty then - s.popSyntax.pushSyntax (.node (emptySourceInfo c s.pos) _k args) - else - s - | _ => - s -} - -private def spacePrefixed1Parser (p : Parser) : Parser := { - info := noFirstTokenInfo p.info - fn := fun c s => - let s := manyFn (andthenFn (symbolNoAntiquot " ").fn p.fn) c s - if s.hasError then - s - else - match s.stxStack.back with - | .node .none _k args => - if args.isEmpty then - -- Require at least one element - s.mkError "expected at least one element" - else - s - | _ => - s -} - def manyParser (p : Parser) : Parser := { info := noFirstTokenInfo p.info fn := fun c s => @@ -948,7 +913,7 @@ partial def catParser (ctx : ParsingContext) (cat : SyntaxCat) (metadata : Metad assert! cat.args.size = 1 let isNonempty := q`StrataDDL.nonempty ∈ metadata commaSepByParserHelper isNonempty <$> catParser ctx cat.args[0]! - | q`Init.SpaceSepBy | q`Init.SpacePrefixedBy | q`Init.Seq => + | q`Init.SpaceSepBy | q`Init.SpacePrefixSepBy | q`Init.Seq => assert! cat.args.size = 1 let isNonempty := q`StrataDDL.nonempty ∈ metadata (if isNonempty then many1Parser else manyParser) <$> catParser ctx cat.args[0]! diff --git a/Strata/DL/SMT/DDMTransform/Parse.lean b/Strata/DL/SMT/DDMTransform/Parse.lean index 57a5831b8..41406cba7 100644 --- a/Strata/DL/SMT/DDMTransform/Parse.lean +++ b/Strata/DL/SMT/DDMTransform/Parse.lean @@ -346,9 +346,9 @@ import SMTCore; // 11. Commands (cont.) // cmd_' is necessary, otherwise it raises "unexpected token 'assert'; expected identifier" -op cmd_assert (t:Term) : Command => "(" "assert" t ")"; +op cmd_assert (t:Term) : Command => "(" "assert " t ")"; op check_sat () : Command => "(" "check-sat" ")"; -op check_sat_assuming (ts:SpacePrefixedBy Term) : Command => +op check_sat_assuming (ts:SpacePrefixSepBy Term) : Command => "(" "check-sat-assuming" ts ")"; op declare_const (s:Symbol, so:SMTSort) : Command => "(" "declare-const " s so ")"; @@ -421,12 +421,6 @@ op mr_deffunrec (fdef:FunctionDef) : ModelResponse => "(" "define-fun-rec " fdef ")"; // TODO: define-funs-rec -category SeqModelResponse; -op seqmr_nil () : SeqModelResponse => ; -op seqmr_one (i: ModelResponse) : SeqModelResponse => i; -op seqmr_cons (i: ModelResponse, is: SeqModelResponse) : SeqModelResponse - => i is; - category InfoResponse; op ir_stack_levels (n:Num) : InfoResponse => ":assertion-stack-response " n; op ir_authors (s:Str) : InfoResponse => ":authors " s; diff --git a/Strata/DL/SMT/DDMTransform/Translate.lean b/Strata/DL/SMT/DDMTransform/Translate.lean index 69e73bccf..50ab8637e 100644 --- a/Strata/DL/SMT/DDMTransform/Translate.lean +++ b/Strata/DL/SMT/DDMTransform/Translate.lean @@ -113,16 +113,6 @@ private def translateFromTermType (t:SMT.TermType): else return .smtsort_param srnone (mkIdentifier id) (Ann.mk srnone argtys_array) --- List of SortedVar to Array. -private def translateFromSortedVarList (l: List (SortedVar SourceRange)): - Array (SortedVar SourceRange) := - l.toArray - --- List of Term to Array. -private def translateFromTermList (l: List (Term SourceRange)): - Array (Term SourceRange) := - l.toArray - def translateFromTerm (t:SMT.Term): Except String (SMTDDM.Term SourceRange) := do let srnone := SourceRange.none match t with @@ -133,7 +123,7 @@ def translateFromTerm (t:SMT.Term): Except String (SMTDDM.Term SourceRange) := d | .none _ | .some _ => throw "don't know how to translate none and some" | .app op args _ => let args' <- args.mapM translateFromTerm - let args_array := translateFromTermList args' + let args_array := args'.toArray if args_array.isEmpty then return (.qual_identifier srnone (.qi_ident srnone (mkIdentifier op.mkName))) else @@ -145,7 +135,7 @@ def translateFromTerm (t:SMT.Term): Except String (SMTDDM.Term SourceRange) := d (fun ⟨name,ty⟩ => do let ty' <- translateFromTermType ty return .sorted_var srnone (mkSymbol name) ty') - let args_array := translateFromSortedVarList args_sorted + let args_array := args_sorted.toArray if args_array.isEmpty then throw "empty quantifier" else diff --git a/Strata/Languages/Boogie/DDMTransform/Translate.lean b/Strata/Languages/Boogie/DDMTransform/Translate.lean index ffb6e670b..b3f215a1f 100644 --- a/Strata/Languages/Boogie/DDMTransform/Translate.lean +++ b/Strata/Languages/Boogie/DDMTransform/Translate.lean @@ -89,7 +89,7 @@ def checkOpArg (arg : Arg) (name : QualifiedIdent) (argc : Nat) : TransM (Array def translateCommaSep [Inhabited α] (f : Strata.Arg → TransM α) (arg : Strata.Arg) : TransM (Array α) := do - let .commaSepList _ args := arg + let .seq _ .comma args := arg | TransM.error s!"Expected commaSepList: {repr arg}" args.mapM f @@ -294,7 +294,7 @@ def translateTypeSynonym (bindings : TransBindings) (op : Operation) : let bargs ← checkOpArg arg q`Boogie.mkBindings 1 let args ← match bargs[0]! with - | .commaSepList _ args => + | .seq _ .comma args => let (arr, bindings) ← translateTypeBindings bindings args return (arr.toList, bindings) | _ => TransM.error @@ -319,7 +319,7 @@ def translateTypeDecl (bindings : TransBindings) (op : Operation) : let bargs ← checkOpArg arg q`Boogie.mkBindings 1 let numargs ← match bargs[0]! with - | .commaSepList _ args => pure args.size + | .seq _ .comma args => pure args.size | _ => TransM.error s!"translateTypeDecl expects a comma separated list: {repr bargs[0]!}") op.args[1]! @@ -1011,7 +1011,7 @@ partial def translateStmt (p : Program) (bindings : TransBindings) (arg : Arg) : partial def translateBlock (p : Program) (bindings : TransBindings) (arg : Arg) : TransM ((List Boogie.Statement) × TransBindings) := do let args ← checkOpArg arg q`Boogie.block 1 - let .seq _ stmts := args[0]! + let .seq _ .none stmts := args[0]! | TransM.error s!"Invalid block {repr args[0]!}" let (a, bindings) ← stmts.foldlM (init := (#[], bindings)) fun (a, b) s => do let (s, b) ← translateStmt p b s @@ -1051,7 +1051,7 @@ def translateBindings (bindings : TransBindings) (op : Arg) : TransM (ListMap BoogieIdent LMonoTy) := do let bargs ← checkOpArg op q`Boogie.mkBindings 1 match bargs[0]! with - | .commaSepList _ args => + | .seq _ .comma args => let arr ← translateInitMkBindings bindings args return arr.toList | _ => @@ -1108,7 +1108,7 @@ def translateSpecElem (p : Program) (name : BoogieIdent) (count : Nat) (bindings partial def translateSpec (p : Program) (name : BoogieIdent) (bindings : TransBindings) (arg : Arg) : TransM (List BoogieIdent × ListMap BoogieLabel Procedure.Check × ListMap BoogieLabel Procedure.Check) := do let sargs ← checkOpArg arg q`Boogie.spec_mk 1 - let .seq _ args := sargs[0]! + let .seq _ .none args := sargs[0]! | TransM.error s!"Invalid specs {repr sargs[0]!}" go 0 args.size args where go (count max : Nat) (args : Array Arg) := do diff --git a/Strata/Languages/C_Simp/DDMTransform/Translate.lean b/Strata/Languages/C_Simp/DDMTransform/Translate.lean index 8cae3842f..b7df8b3b4 100644 --- a/Strata/Languages/C_Simp/DDMTransform/Translate.lean +++ b/Strata/Languages/C_Simp/DDMTransform/Translate.lean @@ -77,7 +77,7 @@ def checkOpArg (arg : Arg) (name : QualifiedIdent) (argc : Nat) : TransM (Array def translateCommaSep [Inhabited α] (f : Strata.Arg → TransM α) (arg : Strata.Arg) : TransM (Array α) := do - let .commaSepList _ args := arg + let .seq _ .comma args := arg | TransM.error s!"Expected commaSepList: {repr arg}" args.mapM f @@ -338,7 +338,7 @@ def translateBindings (bindings : TransBindings) (op : Arg) : TransM (ListMap Expression.Ident LMonoTy) := do let bargs ← checkOpArg op q`C_Simp.mkBindings 1 match bargs[0]! with - | .commaSepList _ args => + | .seq _ .comma args => let arr ← args.mapM (fun op => do let bargs ← checkOpArg op q`C_Simp.mkBinding 2 let id ← translateIdent bargs[0]! @@ -411,7 +411,7 @@ partial def translateStmt (bindings : TransBindings) (arg : Arg) : partial def translateBlock (bindings : TransBindings) (arg : Arg) : TransM (List Statement) := do let args ← checkOpArg arg q`C_Simp.block 1 - let .seq _ stmts := args[0]! + let .seq _ .none stmts := args[0]! | TransM.error s!"Invalid block {repr args[0]!}" let (a, _) ← stmts.foldlM (init := (#[], bindings)) fun (a, b) s => do let (s, b) ← translateStmt b s diff --git a/StrataTest/DDM/NonemptyAttribute.lean b/StrataTest/DDM/NonemptyAttribute.lean index 66bae3dee..06a05aaff 100644 --- a/StrataTest/DDM/NonemptyAttribute.lean +++ b/StrataTest/DDM/NonemptyAttribute.lean @@ -10,7 +10,7 @@ import Strata.DDM.Integration.Lean # Tests for @[nonempty] attribute on list constructs This file tests that the @[nonempty] attribute properly enforces non-empty lists -for CommaSepBy, SpaceSepBy, and SpacePrefixedBy constructs. +for CommaSepBy, SpaceSepBy, and SpacePrefixSepBy constructs. -/ #dialect @@ -22,7 +22,7 @@ op item (n : Num) : Item => n; // Operations with @[nonempty] - require at least one element op comma1 (@[nonempty] items : CommaSepBy Item) : Command => "comma1(" items ")"; op space1 (@[nonempty] items : SpaceSepBy Item) : Command => "space1(" items ")"; -op prefixed1 (@[nonempty] items : SpacePrefixedBy Item) : Command => "prefixed1(" items ")"; +op prefixed1 (@[nonempty] items : SpacePrefixSepBy Item) : Command => "prefixed1(" items ")"; // Operations without @[nonempty] - allow zero elements op comma0 (items : CommaSepBy Item) : Command => "comma0(" items ")"; @@ -68,14 +68,14 @@ program NonemptyTest; space1() #end --- Test that @[nonempty] SpacePrefixedBy accepts non-empty lists +-- Test that @[nonempty] SpacePrefixSepBy accepts non-empty lists #guard_msgs in private def test_nonempty_prefixed_success := #strata program NonemptyTest; prefixed1(1 2 3) #end --- Test that @[nonempty] SpacePrefixedBy rejects empty lists +-- Test that @[nonempty] SpacePrefixSepBy rejects empty lists /-- error: expected expected at least one element -/ #guard_msgs in private def test_nonempty_prefixed_empty := #strata diff --git a/StrataTest/Languages/B3/DDMFormatTests.lean b/StrataTest/Languages/B3/DDMFormatTests.lean index c4ee0fa0d..e28b39423 100644 --- a/StrataTest/Languages/B3/DDMFormatTests.lean +++ b/StrataTest/Languages/B3/DDMFormatTests.lean @@ -114,10 +114,7 @@ mutual | .strlit () s => .strlit default s | .bytes () v => .bytes default v | .option () ma => .option default (ma.map argFUnitToSourceRange) - | .seq () entries => .seq default (entries.map argFUnitToSourceRange) - | .commaSepList () entries => .commaSepList default (entries.map argFUnitToSourceRange) - | .spaceSepList () entries => .spaceSepList default (entries.map argFUnitToSourceRange) - | .spacePrefixedList () entries => .spacePrefixedList default (entries.map argFUnitToSourceRange) + | .seq () sep entries => .seq default sep (entries.map argFUnitToSourceRange) partial def typeExprFUnitToSourceRange : TypeExprF Unit → TypeExprF SourceRange | .ident () tp a => .ident default tp (a.map typeExprFUnitToSourceRange) diff --git a/docs/verso/DDMDoc.lean b/docs/verso/DDMDoc.lean index d271d823f..c297bfd60 100644 --- a/docs/verso/DDMDoc.lean +++ b/docs/verso/DDMDoc.lean @@ -373,6 +373,8 @@ metadata scope(name : Ident); metadata declare(name : Ident, type : TypeOrCat); -- Declares a new variable in the resulting scope with metadata determined -- by an argument. +-- Marks a list argument as requiring at least one element +metadata nonempty; ``` As an example, Boogie variable declaration syntax can be defined in Strata using the @@ -417,9 +419,20 @@ be defined in user definable dialects. `c` may be read in or the empty string. * `Init.Seq c` denotes a sequence of values with category `c`. Each value of `c` is - separated by whitespace. + separated by whitespace. When formatted, values are concatenated with no separator. - * `Init.CommaSepBy c` denotes a comma-separated list of values of type `c`. + * `Init.CommaSepBy c` denotes a comma-separated list of values of type `c`. When formatted, + values are separated by `, ` (comma followed by space). + + * `Init.SpaceSepBy c` denotes a space-separated list of values of type `c`. Parsing is + identical to `Init.Seq`, but when formatted, values are separated by a single space. + + * `Init.SpacePrefixSepBy c` denotes a space-prefix-separated list of values of type `c`. + Parsing is identical to `Init.Seq`, but when formatted, each value is prefixed with a space. + + All list categories (`CommaSepBy`, `SpaceSepBy`, `SpacePrefixSepBy`, `Seq`) can be marked + with the `@[nonempty]` metadata attribute to require at least one element during parsing. + For example: `@[nonempty] items : SpaceSepBy Item` will reject empty lists with a parse error. * Parsing for primitive literals and identifiers cannot be directly in syntax definitions. To accomodate this, the `Init` dialect introduces the syntactic categories for this: From 1a20aa88257f04d74b6702a3e1b3bdbbe9aa1f79 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 15 Jan 2026 05:11:33 +0100 Subject: [PATCH 05/11] Fix Java TestGen to use new seq constructor with SepFormat --- StrataTest/DDM/Integration/Java/TestGen.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/StrataTest/DDM/Integration/Java/TestGen.lean b/StrataTest/DDM/Integration/Java/TestGen.lean index 8dc4012e5..40d390af4 100644 --- a/StrataTest/DDM/Integration/Java/TestGen.lean +++ b/StrataTest/DDM/Integration/Java/TestGen.lean @@ -314,7 +314,7 @@ elab "#testRoundtrip" : command => do if prog.commands.size != 1 then Lean.logError "Expected 1 command"; return let cmd := prog.commands[0]! if cmd.name != (⟨"Simple", "block"⟩ : Strata.QualifiedIdent) then Lean.logError "Expected block command"; return - if let .seq _ stmts := cmd.args[0]! then + if let .seq _ _ stmts := cmd.args[0]! then if stmts.size != 4 then Lean.logError s!"Expected 4 statements, got {stmts.size}" else Lean.logError "Expected seq argument" From 196f13aadcb29e54dac08ca568a57dde6e92bc3a Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 15 Jan 2026 05:16:47 +0100 Subject: [PATCH 06/11] Fix remaining .seq references in tests - Update Java TestGen to use .seq with 3 arguments (ann, sep, array) - Update DDM Gen test expected output to show SepFormat.comma instead of commaSepList --- StrataTest/DDM/Gen.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/StrataTest/DDM/Gen.lean b/StrataTest/DDM/Gen.lean index ed073024f..71fddb740 100644 --- a/StrataTest/DDM/Gen.lean +++ b/StrataTest/DDM/Gen.lean @@ -145,7 +145,7 @@ info: Strata.ExprF.app () (Strata.ArgF.type (Strata.TypeExprF.ident () { dialect := "TestDialect", name := "bool" } (Array.mkEmpty 0)))) (Strata.ArgF.op { ann := (), name := { dialect := "TestDialect", name := "mkBindings" }, - args := (Array.mkEmpty 1).push (Strata.ArgF.commaSepList () (Array.mkEmpty 0)) })) + args := (Array.mkEmpty 1).push (Strata.ArgF.seq () Strata.SepFormat.comma (Array.mkEmpty 0)) })) (Strata.ArgF.expr (Strata.ExprF.fn () { dialect := "TestDialect", name := "trueExpr" })) -/ #guard_msgs in From 0910cd2966caaae8516f034bb6c76b847153cf80 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 15 Jan 2026 05:31:55 +0100 Subject: [PATCH 07/11] Fix Laurel translator to use unified .seq constructor - Update translateParameters to match .seq _ .comma - Update translateStmtExpr to match .seq _ .comma - Update translateSeqCommand to match .seq _ .none --- .../Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean index dddb18df2..e79088187 100644 --- a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean +++ b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean @@ -108,7 +108,7 @@ def translateParameter (arg : Arg) : TransM Parameter := do def translateParameters (arg : Arg) : TransM (List Parameter) := do match arg with - | .commaSepList _ args => + | .seq _ .comma args => args.toList.mapM translateParameter | _ => pure [] @@ -184,7 +184,7 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExpr := do | .Identifier name => name | _ => "" let argsList ← match argsSeq with - | .commaSepList _ args => args.toList.mapM translateStmtExpr + | .seq _ .comma args => args.toList.mapM translateStmtExpr | _ => pure [] return .StaticCall calleeName argsList | q`Laurel.return, #[arg0] => @@ -209,7 +209,7 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExpr := do | _ => TransM.error s!"translateStmtExpr expects operation" partial def translateSeqCommand (arg : Arg) : TransM (List StmtExpr) := do - let .seq _ args := arg + let .seq _ .none args := arg | TransM.error s!"translateSeqCommand expects seq" let mut stmts : List StmtExpr := [] for arg in args do @@ -264,7 +264,7 @@ def parseProgram (prog : Strata.Program) : TransM Laurel.Program := do if prog.commands.size == 1 && prog.commands[0]!.name == q`Laurel.program then -- Extract procedures from the program operation's first argument (Seq Procedure) match prog.commands[0]!.args[0]! with - | .seq _ procs => procs.filterMap fun arg => + | .seq _ .none procs => procs.filterMap fun arg => match arg with | .op op => some op | _ => none From 9abd1bd7998519faee2467765b2ae8f7ecbaf0d4 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 15 Jan 2026 06:35:38 +0100 Subject: [PATCH 08/11] Add @[nonempty] tests for Seq category - Add seq1 operation with @[nonempty] Seq - Add seq0 operation without @[nonempty] - Verify @[nonempty] enforcement works with Seq - Verify empty Seq is allowed without @[nonempty] --- StrataTest/DDM/NonemptyAttribute.lean | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/StrataTest/DDM/NonemptyAttribute.lean b/StrataTest/DDM/NonemptyAttribute.lean index 06a05aaff..ee176a85c 100644 --- a/StrataTest/DDM/NonemptyAttribute.lean +++ b/StrataTest/DDM/NonemptyAttribute.lean @@ -23,10 +23,12 @@ op item (n : Num) : Item => n; op comma1 (@[nonempty] items : CommaSepBy Item) : Command => "comma1(" items ")"; op space1 (@[nonempty] items : SpaceSepBy Item) : Command => "space1(" items ")"; op prefixed1 (@[nonempty] items : SpacePrefixSepBy Item) : Command => "prefixed1(" items ")"; +op seq1 (@[nonempty] items : Seq Item) : Command => "seq1(" items ")"; // Operations without @[nonempty] - allow zero elements op comma0 (items : CommaSepBy Item) : Command => "comma0(" items ")"; op space0 (items : SpaceSepBy Item) : Command => "space0(" items ")"; +op seq0 (items : Seq Item) : Command => "seq0(" items ")"; #end @@ -98,3 +100,25 @@ space0() #end end NonemptyTest.Tests + +-- Test that @[nonempty] Seq accepts non-empty lists +#guard_msgs in +private def test_nonempty_seq_success := #strata +program NonemptyTest; +seq1(1 2 3) +#end + +-- Test that @[nonempty] Seq rejects empty lists +/-- error: expected expected at least one element -/ +#guard_msgs in +private def test_nonempty_seq_empty := #strata +program NonemptyTest; +seq1() +#end + +-- Test that regular (non-@[nonempty]) Seq allows empty lists +#guard_msgs in +private def test_maybe_empty_seq := #strata +program NonemptyTest; +seq0() +#end From 6e1caca0964ee4c57e9e59bd3ce4779550098e96 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 15 Jan 2026 07:58:42 +0100 Subject: [PATCH 09/11] Address reviewer feedback: extract helpers and centralize string definitions - Added SepFormat.fromIonName? with roundtrip theorem - Extracted toAstApplyArgSeq helper in Gen.lean to eliminate duplication - Added ofSeqSeqM wrapper in OfAstM.lean for plain Seq category - Refactored Ion.lean ArgF.fromIon to use SepFormat.fromIonName? instead of four separate cases - Simplified Parser.lean checkLeftRec with consolidated if statement - Extracted getOfIdentArgSeq helper in Gen.lean where clause --- Strata/DDM/AST.lean | 30 ++++++++ Strata/DDM/Integration/Lean/Gen.lean | 97 +++++++++---------------- Strata/DDM/Integration/Lean/OfAstM.lean | 48 ++++++------ Strata/DDM/Ion.lean | 71 +++++++----------- Strata/DDM/Parser.lean | 36 +++------ 5 files changed, 124 insertions(+), 158 deletions(-) diff --git a/Strata/DDM/AST.lean b/Strata/DDM/AST.lean index cd5eb8adb..901dbeb90 100644 --- a/Strata/DDM/AST.lean +++ b/Strata/DDM/AST.lean @@ -149,6 +149,36 @@ inductive SepFormat where | spacePrefix -- Space before each element (SpacePrefixSepBy) deriving Inhabited, Repr, BEq +namespace SepFormat + +def toString : SepFormat → String + | .none => "seq" + | .comma => "commaSepBy" + | .space => "spaceSepBy" + | .spacePrefix => "spacePrefixSepBy" + +def toIonName : SepFormat → String + | .none => "seq" + | .comma => "commaSepList" + | .space => "spaceSepList" + | .spacePrefix => "spacePrefixedList" + +def fromIonName? : String → Option SepFormat + | "seq" => some .none + | "commaSepList" => some .comma + | "spaceSepList" => some .space + | "spacePrefixedList" => some .spacePrefix + | _ => none + +theorem fromIonName_toIonName_roundtrip (sep : SepFormat) : + fromIonName? (toIonName sep) = some sep := by + cases sep <;> rfl + +instance : ToString SepFormat where + toString := SepFormat.toString + +end SepFormat + mutual inductive ExprF (α : Type) : Type where diff --git a/Strata/DDM/Integration/Lean/Gen.lean b/Strata/DDM/Integration/Lean/Gen.lean index 7c58d01be..82e23669a 100644 --- a/Strata/DDM/Integration/Lean/Gen.lean +++ b/Strata/DDM/Integration/Lean/Gen.lean @@ -673,6 +673,21 @@ def mkAnnWithTerm (argCtor : Name) (annTerm v : Term) : Term := def annToAst (argCtor : Name) (annTerm : Term) : Term := mkCApp argCtor #[mkCApp ``Ann.ann #[annTerm], mkCApp ``Ann.val #[annTerm]] +mutual + +partial def toAstApplyArgSeq (v : Ident) (cat : SyntaxCat) (sepFormat : Name) : GenM Term := do + assert! cat.args.size = 1 + let c := cat.args[0]! + let e ← genFreshLeanName "e" + let canE ← genIdentFrom e (canonical := true) + let t ← toAstApplyArg e c + let args := mkCApp ``Array.map #[ + ←`(fun ⟨$canE, _⟩ => $t), + mkCApp ``Array.attach #[mkCApp ``Ann.val #[v]] + ] + let sepExpr := mkCApp sepFormat #[] + return mkCApp ``ArgF.seq #[mkCApp ``Ann.ann #[v], sepExpr, args] + partial def toAstApplyArg (vn : Name) (cat : SyntaxCat) (unwrap : Bool := false) : GenM Term := do let v := mkIdentFrom (←read).src vn match cat.name with @@ -724,41 +739,13 @@ partial def toAstApplyArg (vn : Name) (cat : SyntaxCat) (unwrap : Bool := false) let toAst ← toAstIdentM cat.name ``($toAst $v) | q`Init.CommaSepBy => do - assert! cat.args.size = 1 - let c := cat.args[0]! - let e ← genFreshLeanName "e" - let canE ← genIdentFrom e (canonical := true) - let t ← toAstApplyArg e c - let args := mkCApp ``Array.map #[ - ←`(fun ⟨$canE, _⟩ => $t), - mkCApp ``Array.attach #[mkCApp ``Ann.val #[v]] - ] - let sepExpr := mkCApp ``SepFormat.comma #[] - return mkCApp ``ArgF.seq #[mkCApp ``Ann.ann #[v], sepExpr, args] + toAstApplyArgSeq v cat ``SepFormat.comma | q`Init.SpaceSepBy => do - assert! cat.args.size = 1 - let c := cat.args[0]! - let e ← genFreshLeanName "e" - let canE ← genIdentFrom e (canonical := true) - let t ← toAstApplyArg e c - let args := mkCApp ``Array.map #[ - ←`(fun ⟨$canE, _⟩ => $t), - mkCApp ``Array.attach #[mkCApp ``Ann.val #[v]] - ] - let sepExpr := mkCApp ``SepFormat.space #[] - return mkCApp ``ArgF.seq #[mkCApp ``Ann.ann #[v], sepExpr, args] + toAstApplyArgSeq v cat ``SepFormat.space | q`Init.SpacePrefixSepBy => do - assert! cat.args.size = 1 - let c := cat.args[0]! - let e ← genFreshLeanName "e" - let canE ← genIdentFrom e (canonical := true) - let t ← toAstApplyArg e c - let args := mkCApp ``Array.map #[ - ←`(fun ⟨$canE, _⟩ => $t), - mkCApp ``Array.attach #[mkCApp ``Ann.val #[v]] - ] - let sepExpr := mkCApp ``SepFormat.spacePrefix #[] - return mkCApp ``ArgF.seq #[mkCApp ``Ann.ann #[v], sepExpr, args] + toAstApplyArgSeq v cat ``SepFormat.spacePrefix + | q`Init.Seq => do + toAstApplyArgSeq v cat ``SepFormat.none | q`Init.Option => do assert! cat.args.size = 1 let c := cat.args[0]! @@ -770,23 +757,13 @@ partial def toAstApplyArg (vn : Name) (cat : SyntaxCat) (unwrap : Bool := false) mkCApp ``Option.attach #[mkCApp ``Ann.val #[v]] ] return mkAnnWithTerm ``ArgF.option v args - | q`Init.Seq => do - assert! cat.args.size = 1 - let c := cat.args[0]! - let e ← genFreshLeanName "e" - let canE ← genIdentFrom e (canonical := true) - let t ← toAstApplyArg e c - let args := mkCApp ``Array.map #[ - ←`(fun ⟨$canE, _⟩ => $t), - mkCApp ``Array.attach #[mkCApp ``Ann.val #[v]] - ] - let sepExpr := mkCApp ``SepFormat.none #[] - return mkCApp ``ArgF.seq #[mkCApp ``Ann.ann #[v], sepExpr, args] | qid => do assert! cat.args.size = 0 let toAst ← toAstIdentM qid ``(ArgF.op ($toAst $v)) +end + abbrev MatchAlt := TSyntax ``Lean.Parser.Term.matchAlt def toAstBuiltinMatches (cat : QualifiedIdent) : GenM (Array MatchAlt) := do @@ -927,36 +904,32 @@ partial def getOfIdentArgWithUnwrap (varName : String) (cat : SyntaxCat) (unwrap let ofAst ← ofAstIdentM cid pure <| mkApp ofAst #[e] | q`Init.CommaSepBy => do - let c := cat.args[0]! - let (vc, vi) ← genFreshIdentPair varName - let body ← getOfIdentArg varName c vi - ``(OfAstM.ofCommaSepByM $e fun $vc _ => $body) + getOfIdentArgSeq varName cat e ``OfAstM.ofCommaSepByM | q`Init.SpaceSepBy => do - let c := cat.args[0]! - let (vc, vi) ← genFreshIdentPair varName - let body ← getOfIdentArg varName c vi - ``(OfAstM.ofSpaceSepByM $e fun $vc _ => $body) + getOfIdentArgSeq varName cat e ``OfAstM.ofSpaceSepByM | q`Init.SpacePrefixSepBy => do - let c := cat.args[0]! - let (vc, vi) ← genFreshIdentPair varName - let body ← getOfIdentArg varName c vi - ``(OfAstM.ofSpacePrefixSepByM $e fun $vc _ => $body) + getOfIdentArgSeq varName cat e ``OfAstM.ofSpacePrefixSepByM + | q`Init.Seq => do + getOfIdentArgSeq varName cat e ``OfAstM.ofSeqSeqM | q`Init.Option => do let c := cat.args[0]! let (vc, vi) ← genFreshIdentPair varName let body ← getOfIdentArg varName c vi ``(OfAstM.ofOptionM $e fun $vc _ => $body) - | q`Init.Seq => do - let c := cat.args[0]! - let (vc, vi) ← genFreshIdentPair varName - let body ← getOfIdentArg "e" c vi - ``(OfAstM.ofSeqM $e fun $vc _ => $body) | cid => do assert! cat.args.isEmpty let (vc, vi) ← genFreshIdentPair varName let ofAst ← ofAstIdentM cid ``(OfAstM.ofOperationM $e fun $vc _ => $ofAst $vi) +where + getOfIdentArgSeq (varName : String) (cat : SyntaxCat) (e : Term) (ofAstFn : Name) : GenM Term := do + let c := cat.args[0]! + let (vc, vi) ← genFreshIdentPair varName + let body ← getOfIdentArg varName c vi + let ofAstFnTerm := mkCApp ofAstFn #[] + ``($ofAstFnTerm $e fun $vc _ => $body) + end def ofAstArgs (argDecls : Array GenArgDecl) (argsVar : Ident) : GenM (Array Ident × Array (TSyntax ``doSeqItem)) := do diff --git a/Strata/DDM/Integration/Lean/OfAstM.lean b/Strata/DDM/Integration/Lean/OfAstM.lean index 6c027950f..42d32786a 100644 --- a/Strata/DDM/Integration/Lean/OfAstM.lean +++ b/Strata/DDM/Integration/Lean/OfAstM.lean @@ -166,49 +166,45 @@ def ofOptionM {α β} [Repr α] [SizeOf α] (fun v => { ann := ann, val := some v }) <$> act v (by decreasing_tactic) | _ => throwExpected "option" arg -def ofCommaSepByM {α β} [Repr α] [SizeOf α] +def ofSeqM {α β} [Repr α] [SizeOf α] + (sep : SepFormat) (arg : ArgF α) (act : ∀(e : ArgF α), sizeOf e < sizeOf arg → OfAstM β) : OfAstM (Ann (Array β) α) := match arg with - | .seq ann .comma a => do - let val ← a.attach.mapM fun ⟨v, vIn⟩ => do - act v (by decreasing_tactic) - pure { ann := ann, val := val } - | _ => throwExpected "commaSepBy" arg - -def ofSeqM {α β} [Repr α] [SizeOf α] + | .seq ann sep' a => + if sep == sep' then do + let val ← a.attach.mapM fun ⟨v, vIn⟩ => + act v (by decreasing_tactic) + pure { ann := ann, val := val } + else + throwExpected sep.toString arg + | _ => throwExpected sep.toString arg + +-- Convenience wrappers for backward compatibility +def ofCommaSepByM {α β} [Repr α] [SizeOf α] (arg : ArgF α) (act : ∀(e : ArgF α), sizeOf e < sizeOf arg → OfAstM β) : OfAstM (Ann (Array β) α) := - match arg with - | .seq ann .none a => do - let val ← a.attach.mapM fun ⟨v, vIn⟩ => - act v (by decreasing_tactic) - pure { ann := ann, val := val } - | _ => throwExpected "seq" arg + ofSeqM .comma arg act def ofSpaceSepByM {α β} [Repr α] [SizeOf α] (arg : ArgF α) (act : ∀(e : ArgF α), sizeOf e < sizeOf arg → OfAstM β) : OfAstM (Ann (Array β) α) := - match arg with - | .seq ann .space a => do - let val ← a.attach.mapM fun ⟨v, vIn⟩ => - act v (by decreasing_tactic) - pure { ann := ann, val := val } - | _ => throwExpected "spaceSepBy" arg + ofSeqM .space arg act def ofSpacePrefixSepByM {α β} [Repr α] [SizeOf α] (arg : ArgF α) (act : ∀(e : ArgF α), sizeOf e < sizeOf arg → OfAstM β) : OfAstM (Ann (Array β) α) := - match arg with - | .seq ann .spacePrefix a => do - let val ← a.attach.mapM fun ⟨v, vIn⟩ => - act v (by decreasing_tactic) - pure { ann := ann, val := val } - | _ => throwExpected "spacePrefixSepBy" arg + ofSeqM .spacePrefix arg act + +def ofSeqSeqM {α β} [Repr α] [SizeOf α] + (arg : ArgF α) + (act : ∀(e : ArgF α), sizeOf e < sizeOf arg → OfAstM β) + : OfAstM (Ann (Array β) α) := + ofSeqM .none arg act /-- Get the expression at index `lvl` in the arguments. diff --git a/Strata/DDM/Ion.lean b/Strata/DDM/Ion.lean index 781a1ebc8..160367da3 100644 --- a/Strata/DDM/Ion.lean +++ b/Strata/DDM/Ion.lean @@ -507,11 +507,12 @@ private protected def ArgF.toIon {α} [ToIon α] (refs : SymbolIdCache) (arg : A return .sexp args | .seq ann sep l => do let annIon ← toIon ann - let args : Array (Ion _) := match sep with - | .none => #[ ionSymbol! "seq", annIon ] - | .comma => #[ ionSymbol! "commaSepList", annIon ] - | .space => #[ ionSymbol! "spaceSepList", annIon ] - | .spacePrefix => #[ ionSymbol! "spacePrefixedList", annIon ] + let sepName := sep.toIonName + let symb := if sepName == "seq" then ionSymbol! "seq" + else if sepName == "commaSepList" then ionSymbol! "commaSepList" + else if sepName == "spaceSepList" then ionSymbol! "spaceSepList" + else ionSymbol! "spacePrefixedList" + let args : Array (Ion _) := #[ symb, annIon ] let args ← l.attach.mapM_off (init := args) fun ⟨v, _⟩ => v.toIon refs return .sexp args termination_by sizeOf arg @@ -614,48 +615,30 @@ private protected def ArgF.fromIon {α} [FromIon α] (v : Ion SymbolId) : FromIo | 3 => some <$> Strata.ArgF.fromIon sexp[2] | _ => throw "Option expects at most one value." return .option ann v - | "seq" => do - let ⟨p⟩ ← .checkArgMin "seq" sexp 2 - let ann ← fromIon sexp[1] - let args ← sexp.attach.mapM_off (start := 2) fun ⟨u, _⟩ => - Strata.ArgF.fromIon u - return .seq ann .none args - | "commaSepList" => do - let ⟨p⟩ ← .checkArgMin "commaSepList" sexp 2 - let ann ← fromIon sexp[1] - let args ← sexp.attach.mapM_off (start := 2) fun ⟨u, _⟩ => - Strata.ArgF.fromIon u - return .seq ann .comma args - | "spaceSepList" => do - let ⟨p⟩ ← .checkArgMin "spaceSepList" sexp 2 - let ann ← fromIon sexp[1] - let args ← sexp.attach.mapM_off (start := 2) fun ⟨u, _⟩ => - Strata.ArgF.fromIon u - return .seq ann .space args - | "spacePrefixedList" => do - let ⟨p⟩ ← .checkArgMin "spacePrefixedList" sexp 2 - let ann ← fromIon sexp[1] - let args ← sexp.attach.mapM_off (start := 2) fun ⟨u, _⟩ => - Strata.ArgF.fromIon u - return .seq ann .spacePrefix args | str => - throw s!"Unexpected identifier {str}" + match SepFormat.fromIonName? str with + | some sep => do + let ⟨p⟩ ← .checkArgMin str sexp 2 + let ann ← fromIon sexp[1] + let args ← sexp.attach.mapM_off (start := 2) fun ⟨u, _⟩ => + Strata.ArgF.fromIon u + return .seq ann sep args + | none => + throw s!"Unexpected identifier {str}" termination_by v decreasing_by - · have _ : sizeOf sexp[1] < sizeOf sexp := by decreasing_tactic - decreasing_tactic - · have _ : sizeOf sexp[1] < sizeOf sexp := by decreasing_tactic - decreasing_tactic - · have _ : sizeOf sexp[2] < sizeOf sexp := by decreasing_tactic - decreasing_tactic - · have _ : sizeOf u < sizeOf sexp := by decreasing_tactic - decreasing_tactic - · have _ : sizeOf u < sizeOf sexp := by decreasing_tactic - decreasing_tactic - · have _ : sizeOf u < sizeOf sexp := by decreasing_tactic - decreasing_tactic - · have _ : sizeOf u < sizeOf sexp := by decreasing_tactic - decreasing_tactic + all_goals + first + | have h : sizeOf sexp[1] < sizeOf sexp := by decreasing_tactic + have : sizeOf sexp < sizeOf v := sexpP.2 + omega + | have h : sizeOf sexp[2] < sizeOf sexp := by decreasing_tactic + have : sizeOf sexp < sizeOf v := sexpP.2 + omega + | have h : sizeOf u < sizeOf sexp := by decreasing_tactic + have : sizeOf sexp < sizeOf v := sexpP.2 + omega + | decreasing_tactic end diff --git a/Strata/DDM/Parser.lean b/Strata/DDM/Parser.lean index 1771ff696..eb4d3df02 100644 --- a/Strata/DDM/Parser.lean +++ b/Strata/DDM/Parser.lean @@ -767,36 +767,20 @@ def checkLeftRec (thisCatName : QualifiedIdent) (argDecls : ArgDecls) (as : List let .isTrue lt := inferInstanceAs (Decidable (v < argDecls.size)) | return panic! "Invalid index" let cat := argDecls[v].kind.categoryOf - match cat.name with - | q`Init.CommaSepBy => + let isListCategory := cat.name == q`Init.CommaSepBy || + cat.name == q`Init.SpaceSepBy || + cat.name == q`Init.SpacePrefixSepBy || + cat.name == q`Init.Seq || + cat.name == q`Init.Option + if isListCategory then assert! cat.args.size = 1 let c := cat.args[0]! if c.name == thisCatName then .invalid mf!"Leading symbol cannot be recursive call to {c}" else .isLeading as - | q`Init.SpaceSepBy | q`Init.SpacePrefixSepBy => - assert! cat.args.size = 1 - let c := cat.args[0]! - if c.name == thisCatName then - .invalid mf!"Leading symbol cannot be recursive call to {c}" - else - .isLeading as - | q`Init.Option => - assert! cat.args.size = 1 - let c := cat.args[0]! - if c.name == thisCatName then - .invalid mf!"Leading symbol cannot be recursive call to {c}" - else - .isLeading as - | q`Init.Seq => - assert! cat.args.size = 1 - let c := cat.args[0]! - if c.name == thisCatName then - .invalid mf!"Leading symbol cannot be recursive call to {c}" - else - .isLeading as - | qid => + else + let qid := cat.name if cat.args.size > 0 then panic! s!"Unknown parametric category '{eformat cat}' is not supported." if qid == thisCatName then @@ -873,9 +857,9 @@ def manyParser (p : Parser) : Parser := { s else match s.stxStack.back with - | .node .none _k args => + | .node .none k args => if args.isEmpty then - s.popSyntax.pushSyntax (.node (emptySourceInfo c s.pos) _k args) + s.popSyntax.pushSyntax (.node (emptySourceInfo c s.pos) k args) else s | _ => From cfc54c60927d1449c6cc80d9a01d4c7f7e9ced3a Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 15 Jan 2026 08:15:44 +0100 Subject: [PATCH 10/11] Inline wrapper functions and call ofSeqM directly with SepFormat - Removed ofCommaSepByM, ofSpaceSepByM, ofSpacePrefixSepByM, ofSeqSeqM wrappers - Updated getOfIdentArgSeq to pass SepFormat directly to ofSeqM - Simplifies code by eliminating unnecessary one-line wrapper functions --- Strata/DDM/Integration/Lean/Gen.lean | 14 +++++++------- Strata/DDM/Integration/Lean/OfAstM.lean | 25 ------------------------- 2 files changed, 7 insertions(+), 32 deletions(-) diff --git a/Strata/DDM/Integration/Lean/Gen.lean b/Strata/DDM/Integration/Lean/Gen.lean index 82e23669a..79aa80ab5 100644 --- a/Strata/DDM/Integration/Lean/Gen.lean +++ b/Strata/DDM/Integration/Lean/Gen.lean @@ -904,13 +904,13 @@ partial def getOfIdentArgWithUnwrap (varName : String) (cat : SyntaxCat) (unwrap let ofAst ← ofAstIdentM cid pure <| mkApp ofAst #[e] | q`Init.CommaSepBy => do - getOfIdentArgSeq varName cat e ``OfAstM.ofCommaSepByM + getOfIdentArgSeq varName cat e ``SepFormat.comma | q`Init.SpaceSepBy => do - getOfIdentArgSeq varName cat e ``OfAstM.ofSpaceSepByM + getOfIdentArgSeq varName cat e ``SepFormat.space | q`Init.SpacePrefixSepBy => do - getOfIdentArgSeq varName cat e ``OfAstM.ofSpacePrefixSepByM + getOfIdentArgSeq varName cat e ``SepFormat.spacePrefix | q`Init.Seq => do - getOfIdentArgSeq varName cat e ``OfAstM.ofSeqSeqM + getOfIdentArgSeq varName cat e ``SepFormat.none | q`Init.Option => do let c := cat.args[0]! let (vc, vi) ← genFreshIdentPair varName @@ -923,12 +923,12 @@ partial def getOfIdentArgWithUnwrap (varName : String) (cat : SyntaxCat) (unwrap ``(OfAstM.ofOperationM $e fun $vc _ => $ofAst $vi) where - getOfIdentArgSeq (varName : String) (cat : SyntaxCat) (e : Term) (ofAstFn : Name) : GenM Term := do + getOfIdentArgSeq (varName : String) (cat : SyntaxCat) (e : Term) (sepFormat : Name) : GenM Term := do let c := cat.args[0]! let (vc, vi) ← genFreshIdentPair varName let body ← getOfIdentArg varName c vi - let ofAstFnTerm := mkCApp ofAstFn #[] - ``($ofAstFnTerm $e fun $vc _ => $body) + let sepFormatTerm := mkCApp sepFormat #[] + ``(OfAstM.ofSeqM $sepFormatTerm $e fun $vc _ => $body) end diff --git a/Strata/DDM/Integration/Lean/OfAstM.lean b/Strata/DDM/Integration/Lean/OfAstM.lean index 42d32786a..91b0a3d90 100644 --- a/Strata/DDM/Integration/Lean/OfAstM.lean +++ b/Strata/DDM/Integration/Lean/OfAstM.lean @@ -181,31 +181,6 @@ def ofSeqM {α β} [Repr α] [SizeOf α] throwExpected sep.toString arg | _ => throwExpected sep.toString arg --- Convenience wrappers for backward compatibility -def ofCommaSepByM {α β} [Repr α] [SizeOf α] - (arg : ArgF α) - (act : ∀(e : ArgF α), sizeOf e < sizeOf arg → OfAstM β) - : OfAstM (Ann (Array β) α) := - ofSeqM .comma arg act - -def ofSpaceSepByM {α β} [Repr α] [SizeOf α] - (arg : ArgF α) - (act : ∀(e : ArgF α), sizeOf e < sizeOf arg → OfAstM β) - : OfAstM (Ann (Array β) α) := - ofSeqM .space arg act - -def ofSpacePrefixSepByM {α β} [Repr α] [SizeOf α] - (arg : ArgF α) - (act : ∀(e : ArgF α), sizeOf e < sizeOf arg → OfAstM β) - : OfAstM (Ann (Array β) α) := - ofSeqM .spacePrefix arg act - -def ofSeqSeqM {α β} [Repr α] [SizeOf α] - (arg : ArgF α) - (act : ∀(e : ArgF α), sizeOf e < sizeOf arg → OfAstM β) - : OfAstM (Ann (Array β) α) := - ofSeqM .none arg act - /-- Get the expression at index `lvl` in the arguments. From ae6349ae35701aca399e36ba6014bd7e426f9794 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 15 Jan 2026 08:48:18 +0100 Subject: [PATCH 11/11] Unify sequence info structures and eliminate duplication - Replaced CommaSepInfo, SpaceSepInfo, SpacePrefixedInfo with single SeqInfo taking SepFormat parameter - Removed duplicate Info constructors (ofCommaSepInfo, ofSpaceSepInfo, ofSpacePrefixedInfo) - Updated asCommaSepInfo functions to check sep field - Extracted elabSeqWith helper in Core.lean to consolidate four similar elaboration cases - Reduces code duplication by ~50 lines across Tree.lean and Core.lean --- Strata/DDM/Elab/Core.lean | 48 ++++++++++++--------------------------- Strata/DDM/Elab/Tree.lean | 44 ++++++++++------------------------- 2 files changed, 26 insertions(+), 66 deletions(-) diff --git a/Strata/DDM/Elab/Core.lean b/Strata/DDM/Elab/Core.lean index cca1caa83..e67e56b72 100644 --- a/Strata/DDM/Elab/Core.lean +++ b/Strata/DDM/Elab/Core.lean @@ -1165,48 +1165,28 @@ partial def catElaborator (c : SyntaxCat) : TypingContext → Syntax → ElabM T let a := c.args[0]! elabOption (catElaborator a) | q`Init.Seq => - assert! c.args.size = 1 - let a := c.args[0]! - let f := elabManyElement (catElaborator a) - fun tctx stx => do - let some loc := mkSourceRange? stx - | panic! "seq missing source location" - let (args, resultCtx) ← stx.getArgs.foldlM f (#[], tctx) - let info : SeqInfo := { inputCtx := tctx, loc := loc, args := args.map (·.arg), resultCtx } - pure <| .node (.ofSeqInfo info) args + elabSeqWith c .none "seq" (·.getArgs) | q`Init.CommaSepBy => - assert! c.args.size = 1 - let a := c.args[0]! - let f := elabManyElement (catElaborator a) - fun tctx stx => do - let some loc := mkSourceRange? stx - | panic! s!"commaSepBy missing source location {repr stx}" - let (args, resultCtx) ← stx.getSepArgs.foldlM f (#[], tctx) - let info : CommaSepInfo := { inputCtx := tctx, loc := loc, args := args.map (·.arg), resultCtx } - pure <| .node (.ofCommaSepInfo info) args + elabSeqWith c .comma "commaSepBy" (·.getSepArgs) | q`Init.SpaceSepBy => - assert! c.args.size = 1 - let a := c.args[0]! - let f := elabManyElement (catElaborator a) - fun tctx stx => do - let some loc := mkSourceRange? stx - | panic! s!"spaceSepBy missing source location {repr stx}" - let (args, resultCtx) ← stx.getSepArgs.foldlM f (#[], tctx) - let info : SpaceSepInfo := { inputCtx := tctx, loc := loc, args := args.map (·.arg), resultCtx } - pure <| .node (.ofSpaceSepInfo info) args + elabSeqWith c .space "spaceSepBy" (·.getSepArgs) | q`Init.SpacePrefixSepBy => + elabSeqWith c .spacePrefix "spacePrefixSepBy" (·.getArgs) + | _ => + assert! c.args.isEmpty + elabOperation + +where + elabSeqWith (c : SyntaxCat) (sep : SepFormat) (name : String) (getArgsFrom : Syntax → Array Syntax) : TypingContext → Syntax → ElabM Tree := assert! c.args.size = 1 let a := c.args[0]! let f := elabManyElement (catElaborator a) fun tctx stx => do let some loc := mkSourceRange? stx - | panic! s!"spacePrefixSepBy missing source location {repr stx}" - let (args, resultCtx) ← stx.getArgs.foldlM f (#[], tctx) - let info : SpacePrefixedInfo := { inputCtx := tctx, loc := loc, args := args.map (·.arg), resultCtx } - pure <| .node (.ofSpacePrefixedInfo info) args - | _ => - assert! c.args.isEmpty - elabOperation + | panic! s!"{name} missing source location {repr stx}" + let (args, resultCtx) ← (getArgsFrom stx).foldlM f (#[], tctx) + let info : SeqInfo := { inputCtx := tctx, loc := loc, sep := sep, args := args.map (·.arg), resultCtx } + pure <| .node (.ofSeqInfo info) args partial def elabExpr (tctx : TypingContext) (stx : Syntax) : ElabM Tree := do match stx.getKind with diff --git a/Strata/DDM/Elab/Tree.lean b/Strata/DDM/Elab/Tree.lean index c7b285867..be2a17e8f 100644 --- a/Strata/DDM/Elab/Tree.lean +++ b/Strata/DDM/Elab/Tree.lean @@ -246,21 +246,7 @@ structure OptionInfo extends ElabInfo where deriving Inhabited, Repr structure SeqInfo extends ElabInfo where - args : Array Arg - resultCtx : TypingContext -deriving Inhabited, Repr - -structure CommaSepInfo extends ElabInfo where - args : Array Arg - resultCtx : TypingContext -deriving Inhabited, Repr - -structure SpaceSepInfo extends ElabInfo where - args : Array Arg - resultCtx : TypingContext -deriving Inhabited, Repr - -structure SpacePrefixedInfo extends ElabInfo where + sep : SepFormat args : Array Arg resultCtx : TypingContext deriving Inhabited, Repr @@ -277,9 +263,6 @@ inductive Info | ofBytesInfo (info : ConstInfo ByteArray) | ofOptionInfo (info : OptionInfo) | ofSeqInfo (info : SeqInfo) -| ofCommaSepInfo (info : CommaSepInfo) -| ofSpaceSepInfo (info : SpaceSepInfo) -| ofSpacePrefixedInfo (info : SpacePrefixedInfo) deriving Inhabited, Repr namespace Info @@ -313,9 +296,6 @@ def elabInfo (info : Info) : ElabInfo := | .ofBytesInfo info => info.toElabInfo | .ofOptionInfo info => info.toElabInfo | .ofSeqInfo info => info.toElabInfo - | .ofCommaSepInfo info => info.toElabInfo - | .ofSpaceSepInfo info => info.toElabInfo - | .ofSpacePrefixedInfo info => info.toElabInfo def inputCtx (info : Info) : TypingContext := info.elabInfo.inputCtx @@ -361,10 +341,7 @@ def arg : Tree → Arg | #[x] => some x.arg | _ => panic! "Unexpected option" .option info.loc r - | .ofSeqInfo info => .seq info.loc .none info.args - | .ofCommaSepInfo info => .seq info.loc .comma info.args - | .ofSpaceSepInfo info => .seq info.loc .space info.args - | .ofSpacePrefixedInfo info => .seq info.loc .spacePrefix info.args + | .ofSeqInfo info => .seq info.loc info.sep info.args theorem sizeOf_children (t : Tree) (i : Nat) (p : i < t.children.size) : sizeOf t[i] < sizeOf t := by match t with @@ -386,9 +363,6 @@ def resultContext (t : Tree) : TypingContext := else info.inputCtx | .ofSeqInfo info => info.resultCtx - | .ofCommaSepInfo info => info.resultCtx - | .ofSpaceSepInfo info => info.resultCtx - | .ofSpacePrefixedInfo info => info.resultCtx termination_by t def isSpecificOp (tree : Tree) (expected : QualifiedIdent) : Bool := @@ -402,14 +376,20 @@ def asOption? (t : Tree) : Option (Option Tree) := | _ => none def asCommaSepInfo? (t : Tree) : Option (Array Tree) := - if let .ofCommaSepInfo _ := t.info then - some t.children + if let .ofSeqInfo info := t.info then + if info.sep == .comma then + some t.children + else + none else none def asCommaSepInfo! (t : Tree) : Array Tree := - if let .ofCommaSepInfo _ := t.info then - t.children + if let .ofSeqInfo info := t.info then + if info.sep == .comma then + t.children + else + panic! "Expected commaSepInfo" else panic! "Expected commaSepInfo"