From 07b3d7964735d4b0eed06120d962860478373845 Mon Sep 17 00:00:00 2001 From: Josh Cohen Date: Wed, 28 Jan 2026 13:58:53 -0500 Subject: [PATCH 01/12] Add mutual types to DDM as forward declarations, add tests No polymorphism yet Add forward declarations to DDM Add name to fvar to keep track within block Change Translate to translate to mutual blocks Add rose tree test --- Strata/DDM/AST.lean | 114 ++++++-- Strata/DDM/BuiltinDialects/StrataDDL.lean | 1 + Strata/DDM/Elab/Core.lean | 20 +- Strata/DDM/Elab/DialectM.lean | 2 +- Strata/DDM/Elab/Tree.lean | 37 ++- Strata/DDM/Format.lean | 4 +- Strata/DDM/Integration/Lean/ToExpr.lean | 9 +- Strata/DDM/Ion.lean | 46 ++- Strata/DL/Lambda/TypeFactory.lean | 6 + Strata/Languages/Core/DDMTransform/Parse.lean | 10 + .../Core/DDMTransform/Translate.lean | 236 ++++++++++++++-- StrataTest/Languages/B3/DDMFormatTests.lean | 2 +- .../Core/Examples/DDMAxiomsExtraction.lean | 44 +-- .../Core/Examples/DatatypeRoseTree.lean | 262 ++++++++++++++++++ .../Core/Examples/RemoveIrrelevantAxioms.lean | 10 +- StrataTest/Languages/Core/ExprEvalTest.lean | 2 +- StrataTest/Transform/ProcedureInlining.lean | 12 +- 17 files changed, 704 insertions(+), 113 deletions(-) create mode 100644 StrataTest/Languages/Core/Examples/DatatypeRoseTree.lean diff --git a/Strata/DDM/AST.lean b/Strata/DDM/AST.lean index 1077807c3..c65226387 100644 --- a/Strata/DDM/AST.lean +++ b/Strata/DDM/AST.lean @@ -93,8 +93,9 @@ inductive TypeExprF (α : Type) where | ident (ann : α) (name : QualifiedIdent) (args : Array (TypeExprF α)) /-- A bound type variable at the given deBruijn index in the context. -/ | bvar (ann : α) (index : Nat) - /-- A reference to a global variable along with any arguments to ensure it is well-typed. -/ -| fvar (ann : α) (fvar : FreeVarIndex) (args : Array (TypeExprF α)) + /-- A reference to a global variable along with any arguments to ensure it is well-typed. + The name field stores the original type name for lookup in mutual blocks. -/ +| fvar (ann : α) (fvar : FreeVarIndex) (name : Option String) (args : Array (TypeExprF α)) /-- A function type. -/ | arrow (ann : α) (arg : TypeExprF α) (res : TypeExprF α) deriving BEq, Inhabited, Repr @@ -104,7 +105,7 @@ namespace TypeExprF def ann {α} : TypeExprF α → α | .ident ann _ _ => ann | .bvar ann _ => ann -| .fvar ann _ _ => ann +| .fvar ann _ _ _ => ann | .arrow ann _ _ => ann def mkFunType {α} (n : α) (bindings : Array (String × TypeExprF α)) (res : TypeExprF α) : TypeExprF α := @@ -113,14 +114,14 @@ def mkFunType {α} (n : α) (bindings : Array (String × TypeExprF α)) (res : T protected def incIndices {α} (tp : TypeExprF α) (count : Nat) : TypeExprF α := match tp with | .ident n i args => .ident n i (args.attach.map fun ⟨e, _⟩ => e.incIndices count) - | .fvar n f args => .fvar n f (args.attach.map fun ⟨e, _⟩ => e.incIndices count) + | .fvar n f name args => .fvar n f name (args.attach.map fun ⟨e, _⟩ => e.incIndices count) | .bvar n idx => .bvar n (idx + count) | .arrow n a r => .arrow n (a.incIndices count) (r.incIndices count) /-- Return true if type expression has a bound variable. -/ protected def hasUnboundVar {α} (bindingCount : Nat := 0) : TypeExprF α → Bool | .ident _ _ args => args.attach.any (fun ⟨e, _⟩ => e.hasUnboundVar bindingCount) -| .fvar _ _ args => args.attach.any (fun ⟨e, _⟩ => e.hasUnboundVar bindingCount) +| .fvar _ _ _ args => args.attach.any (fun ⟨e, _⟩ => e.hasUnboundVar bindingCount) | .bvar _ idx => idx ≥ bindingCount | .arrow _ a r => a.hasUnboundVar bindingCount || r.hasUnboundVar bindingCount termination_by e => e @@ -138,7 +139,7 @@ protected def instTypeM {m α} [Monad m] (d : TypeExprF α) (bindings : α → N | .ident n i a => .ident n i <$> a.attach.mapM (fun ⟨e, _⟩ => e.instTypeM bindings) | .bvar n idx => bindings n idx - | .fvar n idx a => .fvar n idx <$> a.attach.mapM (fun ⟨e, _⟩ => e.instTypeM bindings) + | .fvar n idx name a => .fvar n idx name <$> a.attach.mapM (fun ⟨e, _⟩ => e.instTypeM bindings) | .arrow n a b => .arrow n <$> a.instTypeM bindings <*> b.instTypeM bindings termination_by d @@ -546,7 +547,7 @@ inductive PreType where /-- A bound type variable at the given deBruijn index in the context. -/ | bvar (ann : SourceRange) (index : Nat) /-- A reference to a global variable along with any arguments to ensure it is well-typed. -/ -| fvar (ann : SourceRange) (fvar : FreeVarIndex) (args : Array PreType) +| fvar (ann : SourceRange) (fvar : FreeVarIndex) (name : Option String) (args : Array PreType) /-- A function type. -/ | arrow (ann : SourceRange) (arg : PreType) (res : PreType) /-- A function created from a reference to bindings and a result type. -/ @@ -559,14 +560,14 @@ namespace PreType def ann : PreType → SourceRange | .ident ann _ _ => ann | .bvar ann _ => ann -| .fvar ann _ _ => ann +| .fvar ann _ _ _ => ann | .arrow ann _ _ => ann | .funMacro ann _ _ => ann def ofType : TypeExprF SourceRange → PreType | .ident loc name args => .ident loc name (args.map fun a => .ofType a) | .bvar loc idx => .bvar loc idx -| .fvar loc idx args => .fvar loc idx (args.map fun a => .ofType a) +| .fvar loc idx name args => .fvar loc idx name (args.map fun a => .ofType a) | .arrow loc a r => .arrow loc (.ofType a) (.ofType r) termination_by tp => tp @@ -789,9 +790,9 @@ structure ConstructorInfo where Build a TypeExpr reference to the datatype with type parameters, using `.fvar` for the datatype's GlobalContext index. -/ -def mkDatatypeTypeRef (ann : SourceRange) (datatypeIndex : FreeVarIndex) (typeParams : Array String) : TypeExpr := +def mkDatatypeTypeRef (ann : SourceRange) (datatypeIndex : FreeVarIndex) (typeParams : Array String) (datatypeName : Option String := none) : TypeExpr := let typeArgs := typeParams.mapIdx fun i _ => TypeExprF.bvar ann i - TypeExprF.fvar ann datatypeIndex typeArgs + TypeExprF.fvar ann datatypeIndex datatypeName typeArgs /-- Build an arrow type from field types to the datatype type. E.g. for cons, @@ -954,6 +955,7 @@ A spec for introducing a new binding into a type context. inductive BindingSpec (argDecls : ArgDecls) where | value (_ : ValueBindingSpec argDecls) | type (_ : TypeBindingSpec argDecls) +| typeForward (_ : TypeBindingSpec argDecls) -- Forward declaration (no AST node) | datatype (_ : DatatypeBindingSpec argDecls) deriving Repr @@ -962,6 +964,7 @@ namespace BindingSpec def nameIndex {argDecls} : BindingSpec argDecls → DebruijnIndex argDecls.size | .value v => v.nameIndex | .type v => v.nameIndex +| .typeForward v => v.nameIndex | .datatype v => v.nameIndex end BindingSpec @@ -1044,6 +1047,22 @@ def parseNewBindings (md : Metadata) (argDecls : ArgDecls) : Array (BindingSpec pure <| some ⟨idx, argsP⟩ | _ => newBindingErr "declareType args invalid."; return none some <$> .type <$> pure { nameIndex, argsIndex, defIndex := none } + | q`StrataDDL.declareTypeForward => do + let #[.catbvar nameIndex, .option mArgsArg ] := attr.args + | newBindingErr s!"declareTypeForward has bad arguments {repr attr.args}."; return none + let .isTrue nameP := inferInstanceAs (Decidable (nameIndex < argDecls.size)) + | return panic! "Invalid name index" + let nameIndex := ⟨nameIndex, nameP⟩ + checkNameIndexIsIdent argDecls nameIndex + let argsIndex ← + match mArgsArg with + | none => pure none + | some (.catbvar idx) => + let .isTrue argsP := inferInstanceAs (Decidable (idx < argDecls.size)) + | return panic! "Invalid arg index" + pure <| some ⟨idx, argsP⟩ + | _ => newBindingErr "declareTypeForward args invalid."; return none + some <$> .typeForward <$> pure { nameIndex, argsIndex, defIndex := none } | q`StrataDDL.aliasType => do let #[.catbvar nameIndex, .option mArgsArg, .catbvar defIndex] := attr.args | newBindingErr "aliasType missing arguments."; return none @@ -1670,6 +1689,12 @@ inductive GlobalKind where | type (params : List String) (definition : Option TypeExpr) deriving BEq, Inhabited, Repr +/-- State of a symbol in the GlobalContext -/ +inductive DeclState where + | forward -- Symbol is forward-declared (no AST node will be generated) + | defined -- Symbol has a complete definition +deriving BEq, DecidableEq, Repr, Inhabited + /-- Resolves a binding spec into a global kind. -/ partial def resolveBindingIndices { argDecls : ArgDecls } (m : DialectMap) (src : SourceRange) (b : BindingSpec argDecls) (args : Vector Arg argDecls.size) : GlobalKind := match b with @@ -1696,7 +1721,7 @@ partial def resolveBindingIndices { argDecls : ArgDecls } (m : DialectMap) (src panic! s!"Expected new binding to be Type instead of {repr c}." | a => panic! s!"Expected new binding to be bound to type instead of {repr a}." - | .type b => + | .type b | .typeForward b => let params : Array String := match b.argsIndex with | none => #[] @@ -1732,7 +1757,7 @@ Typing environment created from declarations in an environment. -/ structure GlobalContext where nameMap : Std.HashMap Var FreeVarIndex - vars : Array (Var × GlobalKind) + vars : Array (Var × GlobalKind × DeclState) deriving Repr namespace GlobalContext @@ -1752,21 +1777,54 @@ instance : Membership Var GlobalContext where def instDecidableMem (v : Var) (ctx : GlobalContext) : Decidable (v ∈ ctx) := inferInstanceAs (Decidable (v ∈ ctx.nameMap)) -def push (ctx : GlobalContext) (v : Var) (k : GlobalKind) : GlobalContext := +/-- Add a forward declaration (must not exist). Used by @[declareTypeForward]. + This adds to GlobalContext for name resolution but will NOT generate an AST node. -/ +def declareForward (ctx : GlobalContext) (v : Var) (k : GlobalKind) : Except String GlobalContext := if v ∈ ctx then - panic! s!"Var {v} already defined" + .error s!"Symbol '{v}' is already in scope" else let idx := ctx.vars.size - { nameMap := ctx.nameMap.insert v idx, vars := ctx.vars.push (v, k) } + .ok { nameMap := ctx.nameMap.insert v idx, + vars := ctx.vars.push (v, k, .forward) } + +/-- Define a symbol. Used by @[declareDatatype], @[declareFn] with body, etc. + Replaces forward declaration, or adds new as defined. -/ +def define (ctx : GlobalContext) (v : Var) (k : GlobalKind) : Except String GlobalContext := + match ctx.nameMap.get? v with + | none => + -- Not declared, add as defined directly + let idx := ctx.vars.size + .ok { nameMap := ctx.nameMap.insert v idx, + vars := ctx.vars.push (v, k, .defined) } + | some idx => + let (name, _, state) := ctx.vars[idx]! + match state with + | .forward => + -- Replace forward declaration with definition (update in place) + .ok { ctx with vars := ctx.vars.set! idx (name, k, .defined) } + | .defined => + .error s!"Symbol '{v}' is already defined" + +/-- Check if a symbol is forward-declared (not yet defined). -/ +def isForward (ctx : GlobalContext) (idx : FreeVarIndex) : Bool := + match ctx.vars[idx]? with + | some (_, _, .forward) => true + | _ => false + +/-- Add a symbol as defined (backward compatible with existing code). -/ +def push (ctx : GlobalContext) (v : Var) (k : GlobalKind) : GlobalContext := + match ctx.define v k with + | .ok ctx' => ctx' + | .error msg => panic! msg /-- Return the index of the variable with the given name. -/ def findIndex? (ctx : GlobalContext) (v : Var) : Option FreeVarIndex := ctx.nameMap.get? v -def nameOf? (ctx : GlobalContext) (idx : FreeVarIndex) : Option String := ctx.vars[idx]? |>.map (·.fst) +def nameOf? (ctx : GlobalContext) (idx : FreeVarIndex) : Option String := ctx.vars[idx]? |>.map (·.1) def kindOf! (ctx : GlobalContext) (idx : FreeVarIndex) : GlobalKind := assert! idx < ctx.vars.size - ctx.vars[idx]!.snd + ctx.vars[idx]!.2.1 /-! ## Annotation-based Constructor Info Extraction @@ -1967,10 +2025,13 @@ private def addDatatypeBindings let constructorInfo := extractConstructorInfo dialects args[b.constructorsIndex.toLevel] - -- Step 1: Add datatype type - let gctx := gctx.push datatypeName (GlobalKind.type typeParams.toList none) - let datatypeIndex := gctx.vars.size - 1 - let datatypeType := mkDatatypeTypeRef src datatypeIndex typeParams + -- Step 1: Add datatype type (or update forward declaration) + let gctx := match gctx.define datatypeName (GlobalKind.type typeParams.toList none) with + | .ok gctx' => gctx' + | .error msg => panic! s!"addDatatypeBindings: {msg}" + -- Get the actual index - may be from forward declaration or newly added + let datatypeIndex := gctx.findIndex? datatypeName |>.getD (gctx.vars.size - 1) + let datatypeType := mkDatatypeTypeRef src datatypeIndex typeParams (some datatypeName) -- Step 2: Add constructor signatures let gctx := constructorInfo.foldl (init := gctx) fun gctx constr => @@ -1994,6 +2055,15 @@ def addCommand (dialects : DialectMap) (init : GlobalContext) (op : Operation) : match b with | .datatype datatypeSpec => addDatatypeBindings dialects gctx l dialectName datatypeSpec args + | .typeForward typeSpec => + let name := + match args[typeSpec.nameIndex.toLevel] with + | .ident _ e => e + | a => panic! s!"Expected ident at {typeSpec.nameIndex.toLevel} {repr a}" + let kind := resolveBindingIndices dialects l b args + match gctx.declareForward name kind with + | .ok gctx' => gctx' + | .error msg => panic! msg | _ => let name := match args[b.nameIndex.toLevel] with diff --git a/Strata/DDM/BuiltinDialects/StrataDDL.lean b/Strata/DDM/BuiltinDialects/StrataDDL.lean index 417a84af7..609c2292f 100644 --- a/Strata/DDM/BuiltinDialects/StrataDDL.lean +++ b/Strata/DDM/BuiltinDialects/StrataDDL.lean @@ -164,6 +164,7 @@ def StrataDDL : Dialect := BuiltinM.create! "StrataDDL" #[initDialect] do -- Metadata for marking an operation as a constructor list push (list followed by constructor) declareMetadata { name := "constructorListPush", args := #[.mk "list" .ident, .mk "constructor" .ident] } declareMetadata { name := "declareType", args := #[.mk "name" .ident, .mk "args" (.opt .ident)] } + declareMetadata { name := "declareTypeForward", 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] } declareMetadata { name := "declareFn", args := #[.mk "name" .ident, .mk "args" .ident, .mk "type" .ident] } diff --git a/Strata/DDM/Elab/Core.lean b/Strata/DDM/Elab/Core.lean index 92c52cf28..77e2282ce 100644 --- a/Strata/DDM/Elab/Core.lean +++ b/Strata/DDM/Elab/Core.lean @@ -53,7 +53,7 @@ partial def expandMacros (m : DialectMap) (f : PreType) (args : Nat → Option A match f with | .ident loc i a => .ident loc i <$> a.mapM fun e => expandMacros m e args | .arrow loc a b => .arrow loc <$> expandMacros m a args <*> expandMacros m b args - | .fvar loc i a => .fvar loc i <$> a.mapM fun e => expandMacros m e args + | .fvar loc i name a => .fvar loc i name <$> a.mapM fun e => expandMacros m e args | .bvar loc idx => pure (.bvar loc idx) | .funMacro loc i r => do let r ← expandMacros m r args @@ -79,7 +79,7 @@ the head is in a normal form. partial def hnf (tctx : TypingContext) (e : TypeExpr) : TypeExpr := match e with | .arrow .. | .ident .. => e - | .fvar _ idx args => + | .fvar _ idx _ args => let gctx := tctx.globalContext match gctx.kindOf! idx with | .expr _ => panic! "Type free variable bound to expression." @@ -197,7 +197,7 @@ def resolveTypeBinding (tctx : TypingContext) (loc : SourceRange) (name : String | logErrorMF c.info.loc mf!"Expected type" tpArgs := tpArgs.push cinfo.typeExpr children := children.push c - let tp := .fvar loc fidx tpArgs + let tp := .fvar loc fidx (some name) tpArgs let info : TypeInfo := { inputCtx := tctx, loc := loc, typeExpr := tp, isInferred := false } return .node (.ofTypeInfo info) children else if let some a := args[params.size]? then @@ -328,7 +328,7 @@ N.B. This expects that macros have already been expanded in e. partial def headExpandTypeAlias (gctx : GlobalContext) (e : TypeExpr) : TypeExpr := match e with | .arrow .. | .ident .. | .bvar .. => e - | .fvar _ idx args => + | .fvar _ idx _ args => match gctx.kindOf! idx with | .expr _ => panic! "Type free variable bound to expression." | .type params (some d) => @@ -358,7 +358,7 @@ partial def checkExpressionType (tctx : TypingContext) (itype rtype : TypeExpr) return false | .bvar _ ii, .bvar _ ri => return ii = ri - | .fvar _ ii ia, .fvar _ ri ra => + | .fvar _ ii _ ia, .fvar _ ri _ ra => if p : ii = ri ∧ ia.size = ra.size then do for i in Fin.range ia.size do if !(← checkExpressionType tctx ia[i] ra[i]) then @@ -436,9 +436,9 @@ partial def unifyTypes | _ => logErrorMF exprLoc mf!"Encountered {inferredHead} expression when {expectedType} expected." return args - | .fvar _ eid ea => + | .fvar _ eid _ ea => match tctx.hnf inferredType with - | .fvar _ iid ia => + | .fvar _ iid _ ia => if eid != iid then logErrorMF exprLoc mf!"Encountered {inferredType} expression when {expectedType} expected." return args @@ -449,7 +449,7 @@ partial def unifyTypes return args | .bvar _ idx => let .isTrue idxP := inferInstanceAs (Decidable (idx < argLevel)) - | return panic! "Invalid index" + | return panic! s!"Invalid index: idx={idx} argLevel={argLevel} expectedType={repr expectedType} inferredType={repr inferredType}" let typeLevel := argLevel - (idx + 1) -- Verify type level is a type parameter. assert! b[typeLevel].kind.isType @@ -736,7 +736,7 @@ def translateBindingKind (tree : Tree) : ElabM BindingKind := do | .type params _ => let params := params.toArray if params.size = tpArgs.size then - return .expr (.fvar nameLoc fidx tpArgs) + return .expr (.fvar nameLoc fidx (some name) tpArgs) else if let some a := tpArgs[params.size]? then logErrorMF a.ann mf!"Unexpected argument to {name}." return default @@ -822,7 +822,7 @@ def evalBindingSpec panic! s!"Cannot bind {ident}: Type at {b.typeIndex.val} has unexpected arg {repr arg}" -- TODO: Decide if new bindings for Type and Expr (or other categories) and should not be allowed? pure { ident, kind } - | .type b => + | .type b | .typeForward b => let ident := evalBindingNameIndex args b.nameIndex let params ← elabArgIndex initSize args b.argsIndex fun argLoc b => do match b.kind with diff --git a/Strata/DDM/Elab/DialectM.lean b/Strata/DDM/Elab/DialectM.lean index 997b13819..0fd4461bc 100644 --- a/Strata/DDM/Elab/DialectM.lean +++ b/Strata/DDM/Elab/DialectM.lean @@ -27,7 +27,7 @@ Note this does not return variables referenced by .funMacro. private def foldBoundTypeVars {α} (tp : PreType) (init : α) (f : α → Nat → α) : α := match tp with | .ident _ _ a => a.attach.foldl (init := init) fun r ⟨e, _⟩ => e.foldBoundTypeVars r f - | .fvar _ _ a => a.attach.foldl (init := init) fun r ⟨e, _⟩ => e.foldBoundTypeVars r f + | .fvar _ _ _ a => a.attach.foldl (init := init) fun r ⟨e, _⟩ => e.foldBoundTypeVars r f | .bvar _ i => f init i | .arrow _ a r => r.foldBoundTypeVars (a.foldBoundTypeVars init f) f | .funMacro _ _ r => r.foldBoundTypeVars init f diff --git a/Strata/DDM/Elab/Tree.lean b/Strata/DDM/Elab/Tree.lean index be2a17e8f..d0629e5fc 100644 --- a/Strata/DDM/Elab/Tree.lean +++ b/Strata/DDM/Elab/Tree.lean @@ -178,19 +178,32 @@ inductive VarBinding | fvar (idx : FreeVarIndex) (tp : GlobalKind) protected def lookupVar (tctx : TypingContext) (var : String) : Option VarBinding := - let a := tctx.map.getD var #[] - match a.back? with - | some lvl => - assert! lvl < tctx.bindings.size - let idx := tctx.bindings.size - 1 - lvl - some (.bvar idx tctx.bindings[lvl]!.kind) + let gctx := tctx.globalContext + -- Check if there's a forward declaration in global context - those take precedence + match gctx.findIndex? var with + | some gidx => + if gctx.isForward gidx then + -- Forward declaration - use global + some (.fvar gidx (gctx.kindOf! gidx)) + else + -- Not forward-declared, check local first for shadowing + let a := tctx.map.getD var #[] + match a.back? with + | some lvl => + assert! lvl < tctx.bindings.size + let idx := tctx.bindings.size - 1 - lvl + some (.bvar idx tctx.bindings[lvl]!.kind) + | none => + some (.fvar gidx (gctx.kindOf! gidx)) | none => - let gctx := tctx.globalContext - match gctx.findIndex? var with - | some idx => - some (.fvar idx (gctx.kindOf! idx)) - | none => - none + -- Not in global, check local + let a := tctx.map.getD var #[] + match a.back? with + | some lvl => + assert! lvl < tctx.bindings.size + let idx := tctx.bindings.size - 1 - lvl + some (.bvar idx tctx.bindings[lvl]!.kind) + | none => none end TypingContext diff --git a/Strata/DDM/Format.lean b/Strata/DDM/Format.lean index 03fdd0f16..7389d2869 100644 --- a/Strata/DDM/Format.lean +++ b/Strata/DDM/Format.lean @@ -272,7 +272,7 @@ private protected def mformat : TypeExprF α → StrataFormat | .ident _ tp a => a.attach.foldl (init := mformat tp) fun m ⟨e, _⟩ => mf!"{m} {e.mformat.ensurePrec (appPrec + 1)}".setPrec appPrec | .bvar _ idx => .bvar idx -| .fvar _ idx a => a.attach.foldl (init := .fvar idx) fun m ⟨e, _⟩ => +| .fvar _ idx _ a => a.attach.foldl (init := .fvar idx) fun m ⟨e, _⟩ => mf!"{m} {e.mformat.ensurePrec (appPrec + 1)}".setPrec appPrec | .arrow _ a r => mf!"{a.mformat.ensurePrec (arrowPrec+1)} -> {r.mformat.ensurePrec arrowPrec}" @@ -286,7 +286,7 @@ namespace PreType private protected def mformat : PreType → StrataFormat | .ident _ tp a => a.attach.foldl (init := mformat tp) (fun m ⟨e, _⟩ => mf!"{m} {e.mformat}") | .bvar _ idx => .bvar idx -| .fvar _ idx a => a.attach.foldl (init := .fvar idx) (fun m ⟨e, _⟩ => mf!"{m} {e.mformat}") +| .fvar _ idx _ a => a.attach.foldl (init := .fvar idx) (fun m ⟨e, _⟩ => mf!"{m} {e.mformat}") | .arrow _ a r => mf!"{a.mformat} -> {r.mformat}" | .funMacro _ idx r => mf!"fnOf({StrataFormat.bvar idx}, {r.mformat})" diff --git a/Strata/DDM/Integration/Lean/ToExpr.lean b/Strata/DDM/Integration/Lean/ToExpr.lean index 16b5e302e..a14974b04 100644 --- a/Strata/DDM/Integration/Lean/ToExpr.lean +++ b/Strata/DDM/Integration/Lean/ToExpr.lean @@ -126,9 +126,9 @@ private protected def toExpr {α} [ToExpr α] : TypeExprF α → Lean.Expr astAnnExpr! ident ann (toExpr nm) ae | .bvar ann idx => astAnnExpr! bvar ann (toExpr idx) -| .fvar ann idx a => +| .fvar ann idx name a => let ae := arrayToExpr levelZero (TypeExprF.typeExpr (toTypeExpr α)) (a.map (·.toExpr)) - astAnnExpr! fvar ann (toExpr idx) ae + astAnnExpr! fvar ann (toExpr idx) (toExpr name) ae | .arrow ann a r => astAnnExpr! arrow ann a.toExpr r.toExpr @@ -218,9 +218,9 @@ private protected def toExpr : PreType → Lean.Expr let args := arrayToExpr .zero PreType.typeExpr (a.map (·.toExpr)) astExpr! ident (toExpr loc) (toExpr nm) args | .bvar loc idx => astExpr! bvar (toExpr loc) (toExpr idx) -| .fvar loc idx a => +| .fvar loc idx name a => let args := arrayToExpr .zero PreType.typeExpr (a.map (·.toExpr)) - astExpr! fvar (toExpr loc) (toExpr idx) args + astExpr! fvar (toExpr loc) (toExpr idx) (toExpr name) args | .arrow loc a r => astExpr! arrow (toExpr loc) a.toExpr r.toExpr | .funMacro loc i r => @@ -410,6 +410,7 @@ private def toExpr {argDecls} (bi : BindingSpec argDecls) (argDeclsExpr : Lean.E match bi with | .value b => astExpr! value argDeclsExpr (b.toExpr argDeclsExpr) | .type b => astExpr! type argDeclsExpr (b.toExpr argDeclsExpr) + | .typeForward b => astExpr! typeForward argDeclsExpr (b.toExpr argDeclsExpr) | .datatype b => astExpr! datatype argDeclsExpr (b.toExpr argDeclsExpr) end BindingSpec diff --git a/Strata/DDM/Ion.lean b/Strata/DDM/Ion.lean index 34313c03f..890158403 100644 --- a/Strata/DDM/Ion.lean +++ b/Strata/DDM/Ion.lean @@ -309,6 +309,16 @@ private def deserializeValue {α} (bs : ByteArray) (act : Ion SymbolId → FromI | .ok res => pure res +protected def fromIonString (v : Ion SymbolId) : FromIonM String := + match v.app with + | .string s => pure s + | _ => throw s!"Expected string, got {repr v}" + +protected def fromIonOption {α} (f : Ion SymbolId → FromIonM α) (v : Ion SymbolId) : FromIonM (Option α) := + match v.app with + | .null => pure none + | _ => some <$> f v + end FromIonM class FromIon (α : Type) where @@ -316,6 +326,12 @@ class FromIon (α : Type) where export FromIon (fromIon) +instance : FromIon String where + fromIon := FromIonM.fromIonString + +instance {α} [FromIon α] : FromIon (Option α) where + fromIon := FromIonM.fromIonOption fromIon + namespace FromIon def deserialize {α} [FromIon α] (bs : ByteArray) : Except String α := @@ -351,6 +367,14 @@ private class ToIon (α : Type) where private abbrev toIon := @ToIon.toIon +private instance : ToIon String where + toIon s := pure (.string s) + +private instance {α} [ToIon α] : ToIon (Option α) where + toIon + | some a => toIon a + | none => pure .null + namespace SyntaxCatF private protected def toIon {α} [ToIon α] (cat : SyntaxCatF α) : Ion.InternM (Ion SymbolId) := do @@ -395,8 +419,8 @@ private protected def toIon {α} [ToIon α] (refs : SymbolIdCache) (tpe : TypeEx -- A bound type variable with the given index. | .bvar ann vidx => return Ion.sexp #[ionSymbol! "bvar", ← toIon ann, .int vidx] - | .fvar ann idx a => do - let s : Array (Ion SymbolId) := #[ionSymbol! "fvar", ← toIon ann, .int idx] + | .fvar ann idx name a => do + let s : Array (Ion SymbolId) := #[ionSymbol! "fvar", ← toIon ann, .int idx, ← toIon name] let s ← a.attach.mapM_off (init := s) fun ⟨e, _⟩ => e.toIon refs return Ion.sexp s @@ -427,12 +451,13 @@ private protected def fromIon {α} [FromIon α] (v : Ion SymbolId) : FromIonM (T (← FromIon.fromIon args[1]) (← .asNat "Type expression bvar" args[2]) | "fvar" => - let ⟨p⟩ ← .checkArgMin "Type expression free variable" args 3 + let ⟨p⟩ ← .checkArgMin "Type expression free variable" args 4 let ann ← FromIon.fromIon args[1] let idx ← .asNat "Type expression free variable index" args[2] - let a ← args.attach.mapM_off (start := 3) fun ⟨e, _⟩ => + let name ← FromIon.fromIon args[3] + let a ← args.attach.mapM_off (start := 4) fun ⟨e, _⟩ => TypeExprF.fromIon e - pure <| .fvar ann idx a + pure <| .fvar ann idx name a | "ident" => let ⟨p⟩ ← .checkArgMin "TypeExpr identifier" args 3 let ann ← FromIon.fromIon args[1] @@ -941,8 +966,8 @@ private protected def toIon (refs : SymbolIdCache) (tpe : PreType) : InternM (Io -- A bound type variable with the given index. | .bvar loc vidx => return Ion.sexp #[ionSymbol! "bvar", ← toIon loc, .int vidx] - | .fvar loc idx a => do - let s : Array (Ion SymbolId) := #[ionSymbol! "fvar", ← toIon loc, .int idx] + | .fvar loc idx name a => do + let s : Array (Ion SymbolId) := #[ionSymbol! "fvar", ← toIon loc, .int idx, ← toIon name] let s ← a.attach.mapM_off (init := s) fun ⟨e, _⟩ => e.toIon refs return Ion.sexp s | .arrow loc l r => do @@ -969,12 +994,13 @@ private protected def fromIon (v : Ion SymbolId) : FromIonM PreType := do (← fromIon args[1]) (← .asNat "TypeExpr bvar" args[2]) | "fvar" => - let ⟨p⟩ ← .checkArgMin "fvar" args 3 + let ⟨p⟩ ← .checkArgMin "fvar" args 4 let ann ← fromIon args[1] let idx ← .asNat "fvar" args[2] - let a ← args.attach.mapM_off (start := 3) fun ⟨e, _⟩ => + let name ← fromIon args[3] + let a ← args.attach.mapM_off (start := 4) fun ⟨e, _⟩ => PreType.fromIon e - pure <| .fvar ann idx a + pure <| .fvar ann idx name a | "ident" => let ⟨p⟩ ← .checkArgMin "ident" args 3 let ann ← fromIon args[1] diff --git a/Strata/DL/Lambda/TypeFactory.lean b/Strata/DL/Lambda/TypeFactory.lean index 223b6f7d3..7ee0c9d76 100644 --- a/Strata/DL/Lambda/TypeFactory.lean +++ b/Strata/DL/Lambda/TypeFactory.lean @@ -47,6 +47,9 @@ structure LConstr (IDMeta : Type) where testerName : String := "is" ++ name.name deriving Repr, DecidableEq +instance [Inhabited IDMeta] : Inhabited (LConstr IDMeta) where + default := { name := default, args := [] } + instance: ToFormat (LConstr IDMeta) where format c := f!"Name:{Format.line}{c.name}{Format.line}\ Args:{Format.line}{c.args}{Format.line}\ @@ -63,6 +66,9 @@ structure LDatatype (IDMeta : Type) where constrs_ne : constrs.length != 0 deriving Repr, DecidableEq +instance [Inhabited IDMeta] : Inhabited (LDatatype IDMeta) where + default := { name := "", typeArgs := [], constrs := [default], constrs_ne := rfl } + instance : ToFormat (LDatatype IDMeta) where format d := f!"type:{Format.line}{d.name}{Format.line}\ Type Arguments:{Format.line}{d.typeArgs}{Format.line}\ diff --git a/Strata/Languages/Core/DDMTransform/Parse.lean b/Strata/Languages/Core/DDMTransform/Parse.lean index 24cb43c80..e388562fc 100644 --- a/Strata/Languages/Core/DDMTransform/Parse.lean +++ b/Strata/Languages/Core/DDMTransform/Parse.lean @@ -249,6 +249,10 @@ op command_procedure (name : Ident, op command_typedecl (name : Ident, args : Option Bindings) : Command => "type " name args ";\n"; +@[declareTypeForward(name, some args)] +op command_forward_typedecl (name : Ident, args : Option Bindings) : Command => + "forward type " name args ";\n"; + @[aliasType(name, some args, rhs)] op command_typesynonym (name : Ident, args : Option Bindings, @@ -323,6 +327,12 @@ op command_datatype (name : Ident, @[scopeDatatype(name, typeParams)] constructors : ConstructorList) : Command => "datatype " name typeParams " {" constructors "}" ";\n"; +// Mutual block for defining mutually recursive types +// Types should be forward-declared before the mutual block +@[scope(commands)] +op command_mutual (commands : SpacePrefixSepBy Command) : Command => + "mutual\n" indent(2, commands) "end;\n"; + #end namespace CoreDDM diff --git a/Strata/Languages/Core/DDMTransform/Translate.lean b/Strata/Languages/Core/DDMTransform/Translate.lean index 76fd36317..da75a8920 100644 --- a/Strata/Languages/Core/DDMTransform/Translate.lean +++ b/Strata/Languages/Core/DDMTransform/Translate.lean @@ -237,7 +237,7 @@ partial def translateLMonoTy (bindings : TransBindings) (arg : Arg) : | .ident _ i argst => let argst' ← translateLMonoTys bindings (argst.map ArgF.type) pure <| (.tcons i.name argst'.toList.reverse) - | .fvar _ i argst => + | .fvar _ i typeName argst => assert! i < bindings.freeVars.size let decl := bindings.freeVars[i]! let ty_core ← match decl with @@ -251,13 +251,18 @@ partial def translateLMonoTy (bindings : TransBindings) (arg : Arg) : | .type (.syn syn) _md => let ty := syn.toLHSLMonoTy pure ty - | .type (.data (ldatatype :: _)) _md => - -- Datatype Declaration - -- TODO: Handle mutual blocks, need to find the specific datatype by name + | .type (.data block) _md => + -- Datatype Declaration (possibly mutual) + -- Use the type name stored in the fvar to find the right datatype in the block + let ldatatype := match typeName, block with + | some name, _ => + match block.find? (fun (d : LDatatype Visibility) => d.name == name) with + | some d => d + | none => panic! "Error: datatype {name} not found in block {block}" + | none, d :: _ => d + | none, [] => panic! "Empty datatype block" let args := ldatatype.typeArgs.map LMonoTy.ftvar pure (.tcons ldatatype.name args) - | .type (.data []) _md => - TransM.error "Empty mutual datatype block" | _ => TransM.error s!"translateLMonoTy not yet implemented for this declaration: \ @@ -341,6 +346,33 @@ def translateTypeDecl (bindings : TransBindings) (op : Operation) : let decl := Core.Decl.type (.con { name := name, numargs := numargs }) md return (decl, { bindings with freeVars := bindings.freeVars.push decl }) +/-- +Translate a forward type declaration. This creates a placeholder entry that will +be replaced when the actual datatype definition is encountered in a mutual block. +-/ +def translateForwardTypeDecl (bindings : TransBindings) (op : Operation) : + TransM (Core.Decl × TransBindings) := do + let _ ← @checkOp (Core.Decl × TransBindings) op q`Core.command_forward_typedecl 2 + let name ← translateIdent TyIdentifier op.args[0]! + let numargs ← + translateOption + (fun maybearg => + do match maybearg with + | none => pure 0 + | some arg => + let bargs ← checkOpArg arg q`Core.mkBindings 1 + let numargs ← + match bargs[0]! with + | .seq _ .comma args => pure args.size + | _ => TransM.error + s!"translateForwardTypeDecl expects a comma separated list: {repr bargs[0]!}") + op.args[1]! + let md ← getOpMetaData op + -- Create a placeholder type constructor that will be replaced by the actual + -- datatype definition in a mutual block + let decl := Core.Decl.type (.con { name := name, numargs := numargs }) md + return (decl, { bindings with freeVars := bindings.freeVars.push decl }) + --------------------------------------------------------------------- def translateLhs (arg : Arg) : TransM CoreIdent := do @@ -421,7 +453,7 @@ def translateOptionMonoDeclList (bindings : TransBindings) (arg : Arg) : partial def dealiasTypeExpr (p : Program) (te : TypeExpr) : TypeExpr := match te with - | (.fvar _ idx #[]) => + | (.fvar _ idx _ #[]) => match p.globalContext.kindOf! idx with | .expr te => te | .type [] (.some te) => te @@ -1431,6 +1463,159 @@ def translateDatatype (p : Program) (bindings : TransBindings) (op : Operation) return (allDecls, bindings) +/-- +Translate a mutual block containing mutually recursive datatype definitions. +This collects all datatypes, creates a single TypeDecl.data with all of them, +and updates the forward-declared entries in bindings.freeVars. +-/ +def translateMutualBlock (p : Program) (bindings : TransBindings) (op : Operation) : + TransM (Core.Decls × TransBindings) := do + let _ ← @checkOp (Core.Decls × TransBindings) op q`Core.command_mutual 1 + + -- Extract commands from the SpacePrefixSepBy + let .seq _ _ commands := op.args[0]! + | TransM.error s!"translateMutualBlock expected sequence: {repr op.args[0]!}" + + -- Filter to only datatype commands + let datatypeOps := commands.filterMap fun arg => + match arg with + | .op op => if op.name == q`Core.command_datatype then some op else none + | _ => none + + if datatypeOps.size == 0 then + TransM.error "Mutual block must contain at least one datatype" + else + -- First pass: collect all datatype names, type args, and their indices in freeVars + -- The forward declarations should already be in bindings.freeVars + let mut datatypeInfos : Array (String × List TyIdentifier × Nat) := #[] + let mut bindingsWithPlaceholders := bindings + + for dtOp in datatypeOps do + let datatypeName ← translateIdent String dtOp.args[0]! + let (typeArgs, _) ← + translateOption + (fun maybearg => + do match maybearg with + | none => pure ([], bindings) + | some arg => + let bargs ← checkOpArg arg q`Core.mkBindings 1 + let args ← + match bargs[0]! with + | .seq _ .comma args => + let (arr, _) ← translateTypeBindings bindings args + return (arr.toList, bindings) + | _ => TransM.error + s!"translateMutualBlock expects a comma separated list: {repr bargs[0]!}") + dtOp.args[1]! + + -- Find the index of this datatype in freeVars (from forward declaration) + -- or add a new placeholder if not forward-declared + let idx := bindingsWithPlaceholders.freeVars.size + let placeholderLDatatype : LDatatype Visibility := + { name := datatypeName + typeArgs := typeArgs + constrs := [{ name := datatypeName, args := [], testerName := "" }] + constrs_ne := by simp } + let placeholderDecl := Core.Decl.type (.data [placeholderLDatatype]) + + -- Check if there's already an entry for this datatype (from forward declaration) + let existingIdx := bindings.freeVars.findIdx? fun decl => + match decl with + | .type t _ => t.names.contains datatypeName + | _ => false + + match existingIdx with + | some i => + -- Update existing entry with placeholder + datatypeInfos := datatypeInfos.push (datatypeName, typeArgs, i) + bindingsWithPlaceholders := { bindingsWithPlaceholders with + freeVars := bindingsWithPlaceholders.freeVars.set! i placeholderDecl } + | none => + -- Add new placeholder + datatypeInfos := datatypeInfos.push (datatypeName, typeArgs, idx) + bindingsWithPlaceholders := { bindingsWithPlaceholders with + freeVars := bindingsWithPlaceholders.freeVars.push placeholderDecl } + + -- Second pass: translate all constructors with all placeholders in scope + let mut ldatatypes : List (LDatatype Visibility) := [] + + for (dtOp, (datatypeName, typeArgs, _idx)) in datatypeOps.zip datatypeInfos do + -- Extract constructor information + let constructors ← translateConstructorList p bindingsWithPlaceholders dtOp.args[2]! + + if h : constructors.size == 0 then + TransM.error s!"Datatype {datatypeName} must have at least one constructor" + else + -- Build LConstr list + let testerPattern : Array NamePatternPart := #[.datatype, .literal "..is", .constructor] + let lConstrs : List (LConstr Visibility) := constructors.toList.map fun constr => + let testerName := expandNamePattern testerPattern datatypeName (some constr.name.name) + { name := constr.name + args := constr.fields.toList.map fun (fieldName, fieldType) => (fieldName, fieldType) + testerName := testerName } + + have constrs_ne : lConstrs.length != 0 := by + simp [lConstrs] + intro heq; subst_vars; apply h; rfl + + let ldatatype : LDatatype Visibility := + { name := datatypeName + typeArgs := typeArgs + constrs := lConstrs + constrs_ne := constrs_ne } + + ldatatypes := ldatatypes ++ [ldatatype] + + -- Generate factory functions for the ENTIRE mutual block at once + let factory ← match genBlockFactory ldatatypes (T := CoreLParams) with + | .ok f => pure f + | .error e => TransM.error s!"Failed to generate datatype factory: {e}" + let allFuncDecls : List Core.Decl := factory.toList.map fun func => + Core.Decl.func func + + -- Create the mutual TypeDecl with all datatypes + let md ← getOpMetaData op + let mutualTypeDecl := Core.Decl.type (.data ldatatypes) md + + -- Update bindings.freeVars: replace forward-declared entries with the mutual block + -- For each datatype, update its entry to point to the mutual TypeDecl + let mut finalBindings := bindings + + for (_datatypeName, _typeArgs, idx) in datatypeInfos do + if idx < finalBindings.freeVars.size then + finalBindings := { finalBindings with + freeVars := finalBindings.freeVars.set! idx mutualTypeDecl } + else + finalBindings := { finalBindings with + freeVars := finalBindings.freeVars.push mutualTypeDecl } + + -- Add constructor, tester, and accessor functions for each datatype + for ldatatype in ldatatypes do + let constructorNames := ldatatype.constrs.map fun c => c.name.name + let testerNames := ldatatype.constrs.map fun c => c.testerName + let fieldNames := ldatatype.constrs.foldl (fun acc c => + acc ++ (c.args.map fun (fieldName, _) => fieldName.name)) [] + + let constructorDecls := allFuncDecls.filter fun decl => + match decl with + | .func f => constructorNames.contains f.name.name + | _ => false + + let testerDecls := allFuncDecls.filter fun decl => + match decl with + | .func f => testerNames.contains f.name.name + | _ => false + + let fieldAccessorDecls := allFuncDecls.filter fun decl => + match decl with + | .func f => fieldNames.contains f.name.name + | _ => false + + for d in constructorDecls ++ testerDecls ++ fieldAccessorDecls do + finalBindings := { finalBindings with freeVars := finalBindings.freeVars.push d } + + return ([mutualTypeDecl], finalBindings) + --------------------------------------------------------------------- def translateGlobalVar (bindings : TransBindings) (op : Operation) : @@ -1459,30 +1644,45 @@ partial def translateCoreDecls (p : Program) (bindings : TransBindings) : match op.name with | q`Core.command_datatype => translateDatatype p bindings op + | q`Core.command_mutual => + translateMutualBlock p bindings op | _ => -- All other commands produce a single declaration - let (decl, bindings) ← + let (decls, bindings) ← match op.name with | q`Core.command_var => - translateGlobalVar bindings op + let (decl, bindings) ← translateGlobalVar bindings op + pure ([decl], bindings) | q`Core.command_constdecl => - translateConstant bindings op + let (decl, bindings) ← translateConstant bindings op + pure ([decl], bindings) | q`Core.command_typedecl => - translateTypeDecl bindings op + let (decl, bindings) ← translateTypeDecl bindings op + pure ([decl], bindings) + | q`Core.command_forward_typedecl => + -- Forward declarations do NOT produce AST nodes - they only update bindings + let (_, bindings) ← translateForwardTypeDecl bindings op + pure ([], bindings) | q`Core.command_typesynonym => - translateTypeSynonym bindings op + let (decl, bindings) ← translateTypeSynonym bindings op + pure ([decl], bindings) | q`Core.command_axiom => - translateAxiom p bindings op + let (decl, bindings) ← translateAxiom p bindings op + pure ([decl], bindings) | q`Core.command_distinct => - translateDistinct p bindings op + let (decl, bindings) ← translateDistinct p bindings op + pure ([decl], bindings) | q`Core.command_procedure => - translateProcedure p bindings op + let (decl, bindings) ← translateProcedure p bindings op + pure ([decl], bindings) | q`Core.command_fndef => - translateFunction .Definition p bindings op + let (decl, bindings) ← translateFunction .Definition p bindings op + pure ([decl], bindings) | q`Core.command_fndecl => - translateFunction .Declaration p bindings op + let (decl, bindings) ← translateFunction .Declaration p bindings op + pure ([decl], bindings) | _ => TransM.error s!"translateCoreDecls unimplemented for {repr op}" - pure ([decl], bindings) + pure (decls, bindings) let (decls, bindings) ← go (count + 1) max bindings ops return (newDecls ++ decls, bindings) diff --git a/StrataTest/Languages/B3/DDMFormatTests.lean b/StrataTest/Languages/B3/DDMFormatTests.lean index e28b39423..a2666be76 100644 --- a/StrataTest/Languages/B3/DDMFormatTests.lean +++ b/StrataTest/Languages/B3/DDMFormatTests.lean @@ -119,7 +119,7 @@ mutual partial def typeExprFUnitToSourceRange : TypeExprF Unit → TypeExprF SourceRange | .ident () tp a => .ident default tp (a.map typeExprFUnitToSourceRange) | .bvar () idx => .bvar default idx - | .fvar () idx a => .fvar default idx (a.map typeExprFUnitToSourceRange) + | .fvar () idx n a => .fvar default idx n (a.map typeExprFUnitToSourceRange) | .arrow () a r => .arrow default (typeExprFUnitToSourceRange a) (typeExprFUnitToSourceRange r) partial def syntaxCatFUnitToSourceRange : SyntaxCatF Unit → SyntaxCatF SourceRange diff --git a/StrataTest/Languages/Core/Examples/DDMAxiomsExtraction.lean b/StrataTest/Languages/Core/Examples/DDMAxiomsExtraction.lean index f01e4ebe7..b9c5df81b 100644 --- a/StrataTest/Languages/Core/Examples/DDMAxiomsExtraction.lean +++ b/StrataTest/Languages/Core/Examples/DDMAxiomsExtraction.lean @@ -157,11 +157,11 @@ info: #[{ ann := { start := { byteIdx := 296 }, stop := { byteIdx := 303 } }, (TypeExprF.fvar { start := { byteIdx := 350 }, stop := { byteIdx := 351 } } - 1 (Array.mkEmpty 0))).push + 1 (some "v") (Array.mkEmpty 0))).push (TypeExprF.fvar { start := { byteIdx := 348 }, stop := { byteIdx := 349 } } - 0 (Array.mkEmpty 0))))) }) })).push + 0 (some "k") (Array.mkEmpty 0))))) }) })).push (ArgF.op { ann := { start := { byteIdx := 353 }, stop := { byteIdx := 358 } }, name := { dialect := "Core", name := "bind_mk" }, @@ -174,7 +174,7 @@ info: #[{ ann := { start := { byteIdx := 296 }, stop := { byteIdx := 303 } }, none)).push (ArgF.type (TypeExprF.fvar { start := { byteIdx := 357 }, stop := { byteIdx := 358 } } - 0 (Array.mkEmpty 0))) }) })).push + 0 (some "k") (Array.mkEmpty 0))) }) })).push (ArgF.op { ann := { start := { byteIdx := 360 }, stop := { byteIdx := 365 } }, name := { dialect := "Core", name := "bind_mk" }, @@ -184,7 +184,7 @@ info: #[{ ann := { start := { byteIdx := 296 }, stop := { byteIdx := 303 } }, "vv")).push (ArgF.option { start := { byteIdx := 364 }, stop := { byteIdx := 364 } } none)).push (ArgF.type - (TypeExprF.fvar { start := { byteIdx := 364 }, stop := { byteIdx := 365 } } 1 + (TypeExprF.fvar { start := { byteIdx := 364 }, stop := { byteIdx := 365 } } 1 (some "v") (Array.mkEmpty 0))) }) })) (ArgF.expr (ExprF.app { start := { byteIdx := 369 }, stop := { byteIdx := 390 } } @@ -193,7 +193,8 @@ info: #[{ ann := { start := { byteIdx := 296 }, stop := { byteIdx := 303 } }, (ExprF.fn { start := { byteIdx := 369 }, stop := { byteIdx := 390 } } { dialect := "Core", name := "equal" }) (ArgF.type - (TypeExprF.fvar { start := { byteIdx := 350 }, stop := { byteIdx := 351 } } 1 (Array.mkEmpty 0)))) + (TypeExprF.fvar { start := { byteIdx := 350 }, stop := { byteIdx := 351 } } 1 (some "v") + (Array.mkEmpty 0)))) (ArgF.expr (ExprF.app { start := { byteIdx := 369 }, stop := { byteIdx := 384 } } (ExprF.app { start := { byteIdx := 369 }, stop := { byteIdx := 384 } } @@ -202,10 +203,10 @@ info: #[{ ann := { start := { byteIdx := 296 }, stop := { byteIdx := 303 } }, (ExprF.fn { start := { byteIdx := 369 }, stop := { byteIdx := 384 } } { dialect := "Core", name := "map_get" }) (ArgF.type - (TypeExprF.fvar { start := { byteIdx := 348 }, stop := { byteIdx := 349 } } 0 + (TypeExprF.fvar { start := { byteIdx := 348 }, stop := { byteIdx := 349 } } 0 (some "k") (Array.mkEmpty 0)))) (ArgF.type - (TypeExprF.fvar { start := { byteIdx := 350 }, stop := { byteIdx := 351 } } 1 + (TypeExprF.fvar { start := { byteIdx := 350 }, stop := { byteIdx := 351 } } 1 (some "v") (Array.mkEmpty 0)))) (ArgF.expr (ExprF.app { start := { byteIdx := 369 }, stop := { byteIdx := 380 } } @@ -217,10 +218,10 @@ info: #[{ ann := { start := { byteIdx := 296 }, stop := { byteIdx := 303 } }, { dialect := "Core", name := "map_set" }) (ArgF.type (TypeExprF.fvar { start := { byteIdx := 348 }, stop := { byteIdx := 349 } } 0 - (Array.mkEmpty 0)))) + (some "k") (Array.mkEmpty 0)))) (ArgF.type (TypeExprF.fvar { start := { byteIdx := 350 }, stop := { byteIdx := 351 } } 1 - (Array.mkEmpty 0)))) + (some "v") (Array.mkEmpty 0)))) (ArgF.expr (ExprF.bvar { start := { byteIdx := 369 }, stop := { byteIdx := 370 } } 2))) (ArgF.expr (ExprF.bvar { start := { byteIdx := 371 }, stop := { byteIdx := 373 } } 1))) (ArgF.expr (ExprF.bvar { start := { byteIdx := 377 }, stop := { byteIdx := 379 } } 0))))) @@ -291,11 +292,11 @@ info: #[{ ann := { start := { byteIdx := 296 }, stop := { byteIdx := 303 } }, (TypeExprF.fvar { start := { byteIdx := 433 }, stop := { byteIdx := 434 } } - 1 (Array.mkEmpty 0))).push + 1 (some "v") (Array.mkEmpty 0))).push (TypeExprF.fvar { start := { byteIdx := 431 }, stop := { byteIdx := 432 } } - 0 (Array.mkEmpty 0))))) }) })).push + 0 (some "k") (Array.mkEmpty 0))))) }) })).push (ArgF.op { ann := { start := { byteIdx := 436 }, stop := { byteIdx := 442 } }, name := { dialect := "Core", name := "bind_mk" }, @@ -311,7 +312,7 @@ info: #[{ ann := { start := { byteIdx := 296 }, stop := { byteIdx := 303 } }, (ArgF.type (TypeExprF.fvar { start := { byteIdx := 441 }, stop := { byteIdx := 442 } } 0 - (Array.mkEmpty 0))) }) })).push + (some "k") (Array.mkEmpty 0))) }) })).push (ArgF.op { ann := { start := { byteIdx := 444 }, stop := { byteIdx := 449 } }, name := { dialect := "Core", name := "bind_mk" }, @@ -324,7 +325,7 @@ info: #[{ ann := { start := { byteIdx := 296 }, stop := { byteIdx := 303 } }, none)).push (ArgF.type (TypeExprF.fvar { start := { byteIdx := 448 }, stop := { byteIdx := 449 } } - 0 (Array.mkEmpty 0))) }) })).push + 0 (some "k") (Array.mkEmpty 0))) }) })).push (ArgF.op { ann := { start := { byteIdx := 451 }, stop := { byteIdx := 456 } }, name := { dialect := "Core", name := "bind_mk" }, @@ -334,7 +335,7 @@ info: #[{ ann := { start := { byteIdx := 296 }, stop := { byteIdx := 303 } }, "vv")).push (ArgF.option { start := { byteIdx := 455 }, stop := { byteIdx := 455 } } none)).push (ArgF.type - (TypeExprF.fvar { start := { byteIdx := 455 }, stop := { byteIdx := 456 } } 1 + (TypeExprF.fvar { start := { byteIdx := 455 }, stop := { byteIdx := 456 } } 1 (some "v") (Array.mkEmpty 0))) }) })) (ArgF.expr (ExprF.app { start := { byteIdx := 460 }, stop := { byteIdx := 486 } } @@ -343,7 +344,8 @@ info: #[{ ann := { start := { byteIdx := 296 }, stop := { byteIdx := 303 } }, (ExprF.fn { start := { byteIdx := 460 }, stop := { byteIdx := 486 } } { dialect := "Core", name := "equal" }) (ArgF.type - (TypeExprF.fvar { start := { byteIdx := 433 }, stop := { byteIdx := 434 } } 1 (Array.mkEmpty 0)))) + (TypeExprF.fvar { start := { byteIdx := 433 }, stop := { byteIdx := 434 } } 1 (some "v") + (Array.mkEmpty 0)))) (ArgF.expr (ExprF.app { start := { byteIdx := 460 }, stop := { byteIdx := 476 } } (ExprF.app { start := { byteIdx := 460 }, stop := { byteIdx := 476 } } @@ -352,10 +354,10 @@ info: #[{ ann := { start := { byteIdx := 296 }, stop := { byteIdx := 303 } }, (ExprF.fn { start := { byteIdx := 460 }, stop := { byteIdx := 476 } } { dialect := "Core", name := "map_get" }) (ArgF.type - (TypeExprF.fvar { start := { byteIdx := 431 }, stop := { byteIdx := 432 } } 0 + (TypeExprF.fvar { start := { byteIdx := 431 }, stop := { byteIdx := 432 } } 0 (some "k") (Array.mkEmpty 0)))) (ArgF.type - (TypeExprF.fvar { start := { byteIdx := 433 }, stop := { byteIdx := 434 } } 1 + (TypeExprF.fvar { start := { byteIdx := 433 }, stop := { byteIdx := 434 } } 1 (some "v") (Array.mkEmpty 0)))) (ArgF.expr (ExprF.app { start := { byteIdx := 460 }, stop := { byteIdx := 471 } } @@ -367,10 +369,10 @@ info: #[{ ann := { start := { byteIdx := 296 }, stop := { byteIdx := 303 } }, { dialect := "Core", name := "map_set" }) (ArgF.type (TypeExprF.fvar { start := { byteIdx := 431 }, stop := { byteIdx := 432 } } 0 - (Array.mkEmpty 0)))) + (some "k") (Array.mkEmpty 0)))) (ArgF.type (TypeExprF.fvar { start := { byteIdx := 433 }, stop := { byteIdx := 434 } } 1 - (Array.mkEmpty 0)))) + (some "v") (Array.mkEmpty 0)))) (ArgF.expr (ExprF.bvar { start := { byteIdx := 460 }, stop := { byteIdx := 461 } } 3))) (ArgF.expr (ExprF.bvar { start := { byteIdx := 462 }, stop := { byteIdx := 464 } } 1))) (ArgF.expr (ExprF.bvar { start := { byteIdx := 468 }, stop := { byteIdx := 470 } } 0))))) @@ -383,10 +385,10 @@ info: #[{ ann := { start := { byteIdx := 296 }, stop := { byteIdx := 303 } }, (ExprF.fn { start := { byteIdx := 480 }, stop := { byteIdx := 486 } } { dialect := "Core", name := "map_get" }) (ArgF.type - (TypeExprF.fvar { start := { byteIdx := 431 }, stop := { byteIdx := 432 } } 0 + (TypeExprF.fvar { start := { byteIdx := 431 }, stop := { byteIdx := 432 } } 0 (some "k") (Array.mkEmpty 0)))) (ArgF.type - (TypeExprF.fvar { start := { byteIdx := 433 }, stop := { byteIdx := 434 } } 1 + (TypeExprF.fvar { start := { byteIdx := 433 }, stop := { byteIdx := 434 } } 1 (some "v") (Array.mkEmpty 0)))) (ArgF.expr (ExprF.bvar { start := { byteIdx := 480 }, stop := { byteIdx := 481 } } 3))) (ArgF.expr (ExprF.bvar { start := { byteIdx := 482 }, stop := { byteIdx := 485 } } 2)))))))) }] diff --git a/StrataTest/Languages/Core/Examples/DatatypeRoseTree.lean b/StrataTest/Languages/Core/Examples/DatatypeRoseTree.lean new file mode 100644 index 000000000..9cbaba8c2 --- /dev/null +++ b/StrataTest/Languages/Core/Examples/DatatypeRoseTree.lean @@ -0,0 +1,262 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Languages.Core.Verifier + +/-! +# Datatype Rose Tree Integration Test + +Tests mutually recursive Rose Tree datatypes using the DDM datatype declaration syntax. +A rose tree is a tree where each node has a value and a list of children (forest). + +This requires mutually recursive types: +- RoseTree: a node with a value and a forest of children +- Forest: a list of rose trees + +Verifies: +- Parsing of mutually recursive datatype declarations +- Tester functions for both types +- Destructor functions for field access +- Type-checking and verification with mutually recursive types +-/ + +namespace Strata.DatatypeRoseTreeTest + +--------------------------------------------------------------------- +-- Test 1: Basic Rose Tree Datatype Declaration and Tester Functions +--------------------------------------------------------------------- + +def roseTreeTesterPgm : Program := +#strata +program Core; + +// Define mutually recursive Rose Tree and Forest datatypes using mutual block +// Forest is a list of RoseTrees +forward type RoseTree; +forward type Forest; +mutual + datatype Forest { FNil(), FCons(head: RoseTree, tail: Forest) }; + datatype RoseTree { Node(val: int, children: Forest) }; +end; + +procedure TestRoseTreeTesters() returns () +spec { + ensures true; +} +{ + var t : RoseTree; + var f : Forest; + + // Create an empty forest + f := FNil(); + + // Test that f is FNil + assert [isFNil]: Forest..isFNil(f); + + // Test that f is not FCons + assert [notFCons]: !Forest..isFCons(f); + + // Create a leaf node (node with empty forest) + t := Node(42, FNil()); + + // Test that t is Node + assert [isNode]: RoseTree..isNode(t); + + // Create a non-empty forest + f := FCons(Node(1, FNil()), FNil()); + + // Test that f is FCons + assert [isFCons]: Forest..isFCons(f); + + // Test that f is not FNil + assert [notFNil]: !Forest..isFNil(f); +}; +#end + +/-- info: true -/ +#guard_msgs in +#eval TransM.run Inhabited.default (translateProgram roseTreeTesterPgm) |>.snd |>.isEmpty + +/-- +info: +Obligation: isFNil +Property: assert +Result: ✅ pass + +Obligation: notFCons +Property: assert +Result: ✅ pass + +Obligation: isNode +Property: assert +Result: ✅ pass + +Obligation: isFCons +Property: assert +Result: ✅ pass + +Obligation: notFNil +Property: assert +Result: ✅ pass + +Obligation: TestRoseTreeTesters_ensures_0 +Property: assert +Result: ✅ pass +-/ +#guard_msgs in +#eval verify "cvc5" roseTreeTesterPgm Inhabited.default Options.quiet + +--------------------------------------------------------------------- +-- Test 2: Rose Tree Destructor Functions +--------------------------------------------------------------------- + +def roseTreeDestructorPgm : Program := +#strata +program Core; + +forward type RoseTree; +forward type Forest; +mutual + datatype Forest { FNil(), FCons(head: RoseTree, tail: Forest) }; + datatype RoseTree { Node(val: int, children: Forest) }; +end; + +procedure TestRoseTreeDestructor() returns () +spec { + ensures true; +} +{ + var t : RoseTree; + var f : Forest; + var v : int; + var c : Forest; + + // Create a leaf node + t := Node(42, FNil()); + + // Extract the value + v := val(t); + assert [valIs42]: v == 42; + + // Extract the children (should be empty forest) + c := children(t); + assert [childrenIsNil]: Forest..isFNil(c); + + // Create a forest with one tree + f := FCons(Node(10, FNil()), FNil()); + + // Extract the head + t := head(f); + assert [headIsNode]: RoseTree..isNode(t); + assert [headVal]: val(t) == 10; + + // Extract the tail + f := tail(f); + assert [tailIsNil]: Forest..isFNil(f); +}; +#end + +/-- info: true -/ +#guard_msgs in +#eval TransM.run Inhabited.default (translateProgram roseTreeDestructorPgm) |>.snd |>.isEmpty + +/-- +info: +Obligation: valIs42 +Property: assert +Result: ✅ pass + +Obligation: childrenIsNil +Property: assert +Result: ✅ pass + +Obligation: headIsNode +Property: assert +Result: ✅ pass + +Obligation: headVal +Property: assert +Result: ✅ pass + +Obligation: tailIsNil +Property: assert +Result: ✅ pass + +Obligation: TestRoseTreeDestructor_ensures_0 +Property: assert +Result: ✅ pass +-/ +#guard_msgs in +#eval verify "cvc5" roseTreeDestructorPgm Inhabited.default Options.quiet + +--------------------------------------------------------------------- +-- Test 3: Rose Tree Equality +--------------------------------------------------------------------- + +def roseTreeEqualityPgm : Program := +#strata +program Core; + +forward type RoseTree; +forward type Forest; +mutual + datatype Forest { FNil(), FCons(head: RoseTree, tail: Forest) }; + datatype RoseTree { Node(val: int, children: Forest) }; +end; + +procedure TestRoseTreeEquality() returns () +spec { + ensures true; +} +{ + var t1 : RoseTree; + var t2 : RoseTree; + var f1 : Forest; + var f2 : Forest; + + // Create two identical leaf nodes + t1 := Node(42, FNil()); + t2 := Node(42, FNil()); + assert [leafEquality]: t1 == t2; + + // Create two identical empty forests + f1 := FNil(); + f2 := FNil(); + assert [emptyForestEquality]: f1 == f2; + + // Create two identical non-empty forests + f1 := FCons(Node(1, FNil()), FNil()); + f2 := FCons(Node(1, FNil()), FNil()); + assert [forestEquality]: f1 == f2; +}; +#end + +/-- info: true -/ +#guard_msgs in +#eval TransM.run Inhabited.default (translateProgram roseTreeEqualityPgm) |>.snd |>.isEmpty + +/-- +info: +Obligation: leafEquality +Property: assert +Result: ✅ pass + +Obligation: emptyForestEquality +Property: assert +Result: ✅ pass + +Obligation: forestEquality +Property: assert +Result: ✅ pass + +Obligation: TestRoseTreeEquality_ensures_0 +Property: assert +Result: ✅ pass +-/ +#guard_msgs in +#eval verify "cvc5" roseTreeEqualityPgm Inhabited.default Options.quiet + +end Strata.DatatypeRoseTreeTest diff --git a/StrataTest/Languages/Core/Examples/RemoveIrrelevantAxioms.lean b/StrataTest/Languages/Core/Examples/RemoveIrrelevantAxioms.lean index 90a10b922..e4ee62fcc 100644 --- a/StrataTest/Languages/Core/Examples/RemoveIrrelevantAxioms.lean +++ b/StrataTest/Languages/Core/Examples/RemoveIrrelevantAxioms.lean @@ -39,7 +39,7 @@ procedure P() returns () assert f(23); assert f(-(5)); } - end : {} + end1 : {} }; procedure Q0(x : int) returns () @@ -49,7 +49,7 @@ procedure Q0(x : int) returns () assert (x == 2); assert (x == 2); } - end : {} + end1 : {} }; procedure Q1(x : int) returns () @@ -59,7 +59,7 @@ procedure Q1(x : int) returns () assert (x == 2); assert (x == 2); } - end : {} + end1 : {} }; procedure Q2(x : int) returns () @@ -69,7 +69,7 @@ procedure Q2(x : int) returns () assert (x == 2); assert (x == 2); } - end : {} + end1 : {} }; procedure Q3(x : int) returns () @@ -79,7 +79,7 @@ procedure Q3(x : int) returns () assert (x == 2); assert (x == 2); } - end : {} + end1 : {} }; #end diff --git a/StrataTest/Languages/Core/ExprEvalTest.lean b/StrataTest/Languages/Core/ExprEvalTest.lean index d0d73c937..3dcc4f464 100644 --- a/StrataTest/Languages/Core/ExprEvalTest.lean +++ b/StrataTest/Languages/Core/ExprEvalTest.lean @@ -189,7 +189,7 @@ open Lambda.LTy.Syntax -- This may take a while (~ 5min) -#eval (checkFactoryOps false) +-- #eval (checkFactoryOps false) open Plausible TestGen diff --git a/StrataTest/Transform/ProcedureInlining.lean b/StrataTest/Transform/ProcedureInlining.lean index 91d859de3..c1e1814b9 100644 --- a/StrataTest/Transform/ProcedureInlining.lean +++ b/StrataTest/Transform/ProcedureInlining.lean @@ -294,17 +294,17 @@ def Test2 := program Core; procedure f(x : bool) returns (y : bool) { if (x) { - goto end; + goto end1; } else { y := false; } - end: {} + end1: {} }; procedure h() returns () { var b_in : bool; var b_out : bool; call b_out := f(b_in); - end: {} + end1: {} }; #end @@ -313,10 +313,10 @@ def Test2Ans := program Core; procedure f(x : bool) returns (y : bool) { if (x) { - goto end; + goto end1; } else { y := false; } - end: {} + end1: {} }; procedure h() returns () { @@ -334,7 +334,7 @@ procedure h() returns () { f_end: {} b_out := f_y; } - end: {} + end1: {} }; #end From d9d5fd372831267c82648627f26ab4ba6532bb9a Mon Sep 17 00:00:00 2001 From: Josh Cohen Date: Thu, 29 Jan 2026 13:28:56 -0500 Subject: [PATCH 02/12] Fix bug with polymorphic datatypes --- Strata/DL/SMT/Encoder.lean | 4 +- .../Core/PolymorphicDatatypeTest.lean | 56 ++++++++++++++++++- .../Core/SMTEncoderDatatypeTest.lean | 4 +- 3 files changed, 59 insertions(+), 5 deletions(-) diff --git a/Strata/DL/SMT/Encoder.lean b/Strata/DL/SMT/Encoder.lean index 8a8b74e02..d4ecccd1e 100644 --- a/Strata/DL/SMT/Encoder.lean +++ b/Strata/DL/SMT/Encoder.lean @@ -197,12 +197,12 @@ def defineApp (inBinder : Bool) (tyEnc : String) (op : Op) (tEncs : List String) else defineTerm inBinder tyEnc s!"({← encodeUF f} {args})" | .datatype_op .constructor name => - -- Zero-argument constructors are constants in SMT-LIB, not function applications -- For parametric datatypes, we need to cast the constructor to the concrete type + -- This is necessary when the constructor doesn't use all type parameters if tEncs.isEmpty then defineTerm inBinder tyEnc s!"(as {name} {tyEnc})" else - defineTerm inBinder tyEnc s!"({name} {args})" + defineTerm inBinder tyEnc s!"((as {name} {tyEnc}) {args})" | .datatype_op _ _ => defineTerm inBinder tyEnc s!"({encodeOp op} {args})" | _ => diff --git a/StrataTest/Languages/Core/PolymorphicDatatypeTest.lean b/StrataTest/Languages/Core/PolymorphicDatatypeTest.lean index 04f0f907d..27d8a8887 100644 --- a/StrataTest/Languages/Core/PolymorphicDatatypeTest.lean +++ b/StrataTest/Languages/Core/PolymorphicDatatypeTest.lean @@ -176,7 +176,7 @@ assert [lValue] (((~Either..l : (arrow (Either int bool) int)) (x : (Either int #eval Core.typeCheck Options.quiet (TransM.run Inhabited.default (translateProgram eitherUsePgm)).fst --------------------------------------------------------------------- --- Test 9: Nested Polymorphic Types (Option of List) +-- Test 5: Nested Polymorphic Types (Option of List) --------------------------------------------------------------------- def nestedPolyPgm : Program := @@ -316,4 +316,58 @@ Result: ✅ pass #guard_msgs in #eval verify "cvc5" multiInstSMTPgm Inhabited.default Options.quiet + +--------------------------------------------------------------------- +-- Test 8: Multiple polymorphic arguments, constructor only needs 1 +--------------------------------------------------------------------- + +def eitherHavocPgm : Program := +#strata +program Core; + +datatype Either (a : Type, b : Type) { Left(l: a), Right(r: b) }; + +procedure TestEitherHavoc() returns () +spec { + ensures true; +} +{ + var x : Either int bool; + + x := Left(0); + havoc x; + + assume (x == Left(42)); + + assert [isLeft]: Either..isLeft(x); + assert [notRight]: !Either..isRight(x); + assert [leftVal]: Either..l(x) == 42; +}; +#end + +/-- info: true -/ +#guard_msgs in +#eval TransM.run Inhabited.default (translateProgram eitherHavocPgm) |>.snd |>.isEmpty + +/-- +info: +Obligation: isLeft +Property: assert +Result: ✅ pass + +Obligation: notRight +Property: assert +Result: ✅ pass + +Obligation: leftVal +Property: assert +Result: ✅ pass + +Obligation: TestEitherHavoc_ensures_0 +Property: assert +Result: ✅ pass +-/ +#guard_msgs in +#eval verify "cvc5" eitherHavocPgm Inhabited.default Options.quiet + end Strata.PolymorphicDatatypeTest diff --git a/StrataTest/Languages/Core/SMTEncoderDatatypeTest.lean b/StrataTest/Languages/Core/SMTEncoderDatatypeTest.lean index 4fbdf7b28..654f770ec 100644 --- a/StrataTest/Languages/Core/SMTEncoderDatatypeTest.lean +++ b/StrataTest/Languages/Core/SMTEncoderDatatypeTest.lean @@ -227,7 +227,7 @@ info: (declare-datatype TestOption (par (α) ( info: (declare-datatype TestOption (par (α) ( (None) (Some (TestOption..val α))))) -(define-fun t0 () (TestOption Int) (Some 42)) +(define-fun t0 () (TestOption Int) ((as Some (TestOption Int)) 42)) -/ #guard_msgs in #eval format <$> toSMTStringWithDatatypes @@ -240,7 +240,7 @@ info: (declare-datatype TestList (par (α) ( (Nil) (Cons (TestList..head α) (TestList..tail (TestList α)))))) (define-fun t0 () (TestList Int) (as Nil (TestList Int))) -(define-fun t1 () (TestList Int) (Cons 1 t0)) +(define-fun t1 () (TestList Int) ((as Cons (TestList Int)) 1 t0)) -/ #guard_msgs in #eval format <$> toSMTStringWithDatatypes From db996cce9015f509bcfd29d7ef28fd6f2ade175e Mon Sep 17 00:00:00 2001 From: Josh Cohen Date: Thu, 29 Jan 2026 14:37:25 -0500 Subject: [PATCH 03/12] Minor comment fix --- Strata/DL/SMT/Encoder.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Strata/DL/SMT/Encoder.lean b/Strata/DL/SMT/Encoder.lean index d4ecccd1e..e2fdae45b 100644 --- a/Strata/DL/SMT/Encoder.lean +++ b/Strata/DL/SMT/Encoder.lean @@ -197,8 +197,8 @@ def defineApp (inBinder : Bool) (tyEnc : String) (op : Op) (tEncs : List String) else defineTerm inBinder tyEnc s!"({← encodeUF f} {args})" | .datatype_op .constructor name => + -- Zero-argument constructors are constants in SMT-LIB, not function applications -- For parametric datatypes, we need to cast the constructor to the concrete type - -- This is necessary when the constructor doesn't use all type parameters if tEncs.isEmpty then defineTerm inBinder tyEnc s!"(as {name} {tyEnc})" else From d0968801bb8b9fc6e9a5e1715efd0ab8af842e7d Mon Sep 17 00:00:00 2001 From: Josh Cohen Date: Thu, 29 Jan 2026 17:23:42 -0500 Subject: [PATCH 04/12] Fix scoping and polymorphism issue Make datatypes handle type arguments appropriately in parser Remove scoping workaroudn with local/declared Some formatting fixes --- Strata/DDM/AST.lean | 15 +++++---- Strata/DDM/Elab/Core.lean | 33 ++++++++++-------- Strata/DDM/Elab/Tree.lean | 37 +++++++-------------- StrataTest/Languages/Core/ExprEvalTest.lean | 2 +- 4 files changed, 41 insertions(+), 46 deletions(-) diff --git a/Strata/DDM/AST.lean b/Strata/DDM/AST.lean index 1ed5655b9..5b01ddfdf 100644 --- a/Strata/DDM/AST.lean +++ b/Strata/DDM/AST.lean @@ -91,12 +91,14 @@ inductive TypeExprF (α : Type) where | ident (ann : α) (name : QualifiedIdent) (args : Array (TypeExprF α)) /-- A bound type variable at the given deBruijn index in the context. -/ | bvar (ann : α) (index : Nat) - /-- A reference to a global variable along with any arguments to ensure it is well-typed. - The name field stores the original type name for lookup in mutual blocks. -/ -| fvar (ann : α) (fvar : FreeVarIndex) (name : Option String) (args : Array (TypeExprF α)) /-- A polymorphic type variable (universally quantified). Used for polymorphic function type parameters -/ | tvar (ann : α) (name : String) + /-- A reference to a global variable along with any arguments to ensure it is + well-typed. The name field stores the original type name for lookup in + mutual blocks. -/ +| fvar (ann : α) (fvar : FreeVarIndex) (name : Option String) + (args : Array (TypeExprF α)) /-- A function type. -/ | arrow (ann : α) (arg : TypeExprF α) (res : TypeExprF α) deriving BEq, Inhabited, Repr @@ -106,8 +108,8 @@ namespace TypeExprF def ann {α} : TypeExprF α → α | .ident ann _ _ => ann | .bvar ann _ => ann -| .fvar ann _ _ _ => ann | .tvar ann _ => ann +| .fvar ann _ _ _ => ann | .arrow ann _ _ => ann def mkFunType {α} (n : α) (bindings : Array (String × TypeExprF α)) (res : TypeExprF α) : TypeExprF α := @@ -1910,7 +1912,7 @@ def isForward (ctx : GlobalContext) (idx : FreeVarIndex) : Bool := | some (_, _, .forward) => true | _ => false -/-- Add a symbol as defined (backward compatible with existing code). -/ +/-- Add a symbol as defined. -/ def push (ctx : GlobalContext) (v : Var) (k : GlobalKind) : GlobalContext := match ctx.define v k with | .ok ctx' => ctx' @@ -1919,7 +1921,7 @@ def push (ctx : GlobalContext) (v : Var) (k : GlobalKind) : GlobalContext := /-- Return the index of the variable with the given name. -/ def findIndex? (ctx : GlobalContext) (v : Var) : Option FreeVarIndex := ctx.nameMap.get? v -def nameOf? (ctx : GlobalContext) (idx : FreeVarIndex) : Option String := ctx.vars[idx]? |>.map (·.1) +def nameOf? (ctx : GlobalContext) (idx : FreeVarIndex) : Option String := ctx.vars[idx]? |>.map (·.fst) def kindOf! (ctx : GlobalContext) (idx : FreeVarIndex) : GlobalKind := assert! idx < ctx.vars.size @@ -2128,7 +2130,6 @@ private def addDatatypeBindings let gctx := match gctx.define datatypeName (GlobalKind.type typeParams.toList none) with | .ok gctx' => gctx' | .error msg => panic! s!"addDatatypeBindings: {msg}" - -- Get the actual index - may be from forward declaration or newly added let datatypeIndex := gctx.findIndex? datatypeName |>.getD (gctx.vars.size - 1) let datatypeType := mkDatatypeTypeRef src datatypeIndex typeParams (some datatypeName) diff --git a/Strata/DDM/Elab/Core.lean b/Strata/DDM/Elab/Core.lean index 7c4c084a9..54851ca9a 100644 --- a/Strata/DDM/Elab/Core.lean +++ b/Strata/DDM/Elab/Core.lean @@ -459,7 +459,7 @@ partial def unifyTypes return args | .bvar _ idx => let .isTrue idxP := inferInstanceAs (Decidable (idx < argLevel)) - | return panic! s!"Invalid index: idx={idx} argLevel={argLevel} expectedType={repr expectedType} inferredType={repr inferredType}" + | return panic! "Invalid index" let typeLevel := argLevel - (idx + 1) -- Verify type level is a type parameter. assert! b[typeLevel].kind.isType @@ -799,6 +799,18 @@ def translateBindingKind (tree : Tree) : ElabM BindingKind := do logInternalError argInfo.loc s!"translateArgDeclKind given invalid kind {opInfo.op.name}" return default +/-- Extract type parameter names from a bindings argument. -/ +def elabTypeParams {n} (initSize : Nat) (args : Vector Tree n) + (idx : Option (DebruijnIndex n)) : ElabM (List String) := do + let params ← elabArgIndex initSize args idx fun argLoc b => do + match b.kind with + | .type _ [] _ => pure () + | .tvar _ _ => pure () + | .type .. | .expr _ | .cat _ => + logError argLoc s!"{b.ident} must have type Type instead of {repr b.kind}." + return b.ident + pure params.toList + /-- Construct a binding from a binding spec and the arguments to an operation. -/ @@ -846,15 +858,7 @@ def evalBindingSpec pure { ident, kind } | .type b | .typeForward b => let ident := evalBindingNameIndex args b.nameIndex - let params ← elabArgIndex initSize args b.argsIndex fun argLoc b => do - match b.kind with - | .type _ [] _ => - pure () - | .tvar _ _ => - pure () - | .type .. | .expr _ | .cat _ => do - logError argLoc s!"{b.ident} must be have type Type instead of {repr b.kind}." - return b.ident + let params ← elabTypeParams initSize args b.argsIndex let value : Option TypeExpr := match b.defIndex with | none => none @@ -864,10 +868,11 @@ def evalBindingSpec some info.typeExpr | _ => panic! "Bad arg" - pure { ident, kind := .type loc params.toList value } + pure { ident, kind := .type loc params value } | .datatype b => let ident := evalBindingNameIndex args b.nameIndex - pure { ident, kind := .type loc [] none } + let params ← elabTypeParams initSize args (some b.typeParamsIndex) + pure { ident, kind := .type loc params none } | .tvar b => let ident := evalBindingNameIndex args b.nameIndex pure { ident, kind := .tvar loc ident } @@ -1057,7 +1062,9 @@ partial def runSyntaxElaborator else gctx.push datatypeName (GlobalKind.type typeParamNames.toList none) -- Add .tvar bindings for type parameters let loc := typeParamsT.info.loc - let tctx := typeParamNames.foldl (init := baseCtx.withGlobalContext gctx) fun ctx name => + -- Start with empty local bindings - don't inherit from baseCtx + -- This prevents datatype names from leaking between mutual block entries + let tctx := typeParamNames.foldl (init := TypingContext.empty gctx) fun ctx name => ctx.push { ident := name, kind := .tvar loc name } pure tctx | _, _ => continue diff --git a/Strata/DDM/Elab/Tree.lean b/Strata/DDM/Elab/Tree.lean index c614b5886..12f4782ad 100644 --- a/Strata/DDM/Elab/Tree.lean +++ b/Strata/DDM/Elab/Tree.lean @@ -185,32 +185,19 @@ inductive VarBinding | fvar (idx : FreeVarIndex) (tp : GlobalKind) protected def lookupVar (tctx : TypingContext) (var : String) : Option VarBinding := - let gctx := tctx.globalContext - -- Check if there's a forward declaration in global context - those take precedence - match gctx.findIndex? var with - | some gidx => - if gctx.isForward gidx then - -- Forward declaration - use global - some (.fvar gidx (gctx.kindOf! gidx)) - else - -- Not forward-declared, check local first for shadowing - let a := tctx.map.getD var #[] - match a.back? with - | some lvl => - assert! lvl < tctx.bindings.size - let idx := tctx.bindings.size - 1 - lvl - some (.bvar idx tctx.bindings[lvl]!.kind) - | none => - some (.fvar gidx (gctx.kindOf! gidx)) + let a := tctx.map.getD var #[] + match a.back? with + | some lvl => + assert! lvl < tctx.bindings.size + let idx := tctx.bindings.size - 1 - lvl + some (.bvar idx tctx.bindings[lvl]!.kind) | none => - -- Not in global, check local - let a := tctx.map.getD var #[] - match a.back? with - | some lvl => - assert! lvl < tctx.bindings.size - let idx := tctx.bindings.size - 1 - lvl - some (.bvar idx tctx.bindings[lvl]!.kind) - | none => none + let gctx := tctx.globalContext + match gctx.findIndex? var with + | some idx => + some (.fvar idx (gctx.kindOf! idx)) + | none => + none end TypingContext diff --git a/StrataTest/Languages/Core/ExprEvalTest.lean b/StrataTest/Languages/Core/ExprEvalTest.lean index cd6c3e9ad..22bad0114 100644 --- a/StrataTest/Languages/Core/ExprEvalTest.lean +++ b/StrataTest/Languages/Core/ExprEvalTest.lean @@ -189,7 +189,7 @@ open Lambda.LTy.Syntax -- This may take a while (~ 5min) --- #eval (checkFactoryOps false) +#eval (checkFactoryOps false) open Plausible TestGen From 4b1577ab71089c82c49eff8dc6c8a703c1725cb3 Mon Sep 17 00:00:00 2001 From: Josh Cohen Date: Thu, 29 Jan 2026 17:30:17 -0500 Subject: [PATCH 05/12] Formatting fixes --- Strata/DDM/Ion.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Strata/DDM/Ion.lean b/Strata/DDM/Ion.lean index 1fb39f8d7..7d7b55031 100644 --- a/Strata/DDM/Ion.lean +++ b/Strata/DDM/Ion.lean @@ -416,6 +416,9 @@ private protected def toIon {α} [ToIon α] (refs : SymbolIdCache) (tpe : TypeEx let args : Array (Ion SymbolId) := #[ionSymbol! "ident", ← toIon ann, v] Ion.sexp <$> a.attach.mapM_off (init := args) fun ⟨e, _⟩ => e.toIon refs + -- A polymorphic type variable with the given name. + | .tvar ann name => + return Ion.sexp #[ionSymbol! "tvar", ← toIon ann, .string name] -- A bound type variable with the given index. | .bvar ann vidx => return Ion.sexp #[ionSymbol! "bvar", ← toIon ann, .int vidx] @@ -424,9 +427,6 @@ private protected def toIon {α} [ToIon α] (refs : SymbolIdCache) (tpe : TypeEx let s ← a.attach.mapM_off (init := s) fun ⟨e, _⟩ => e.toIon refs return Ion.sexp s - -- A polymorphic type variable with the given name. - | .tvar ann name => - return Ion.sexp #[ionSymbol! "tvar", ← toIon ann, .string name] | .arrow ann l r => do return Ion.sexp #[ .symbol ionSymbol! "arrow", From 542bc0b22cc23cbece84f52708cb8d9660e17c6b Mon Sep 17 00:00:00 2001 From: Josh Cohen Date: Thu, 29 Jan 2026 17:31:41 -0500 Subject: [PATCH 06/12] Revert comment --- Strata/DL/SMT/Encoder.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Strata/DL/SMT/Encoder.lean b/Strata/DL/SMT/Encoder.lean index d4ecccd1e..e2fdae45b 100644 --- a/Strata/DL/SMT/Encoder.lean +++ b/Strata/DL/SMT/Encoder.lean @@ -197,8 +197,8 @@ def defineApp (inBinder : Bool) (tyEnc : String) (op : Op) (tEncs : List String) else defineTerm inBinder tyEnc s!"({← encodeUF f} {args})" | .datatype_op .constructor name => + -- Zero-argument constructors are constants in SMT-LIB, not function applications -- For parametric datatypes, we need to cast the constructor to the concrete type - -- This is necessary when the constructor doesn't use all type parameters if tEncs.isEmpty then defineTerm inBinder tyEnc s!"(as {name} {tyEnc})" else From e846866fa4f1e69ead4c9ab1f3b31d561a95e52d Mon Sep 17 00:00:00 2001 From: Josh Cohen Date: Thu, 29 Jan 2026 19:29:43 -0500 Subject: [PATCH 07/12] Some refactoring of Translate.lean Factor out common functionality with mutual/single datatypes Require that mutual datatypes are forward declared --- .../Core/DDMTransform/Translate.lean | 233 ++++++++---------- 1 file changed, 99 insertions(+), 134 deletions(-) diff --git a/Strata/Languages/Core/DDMTransform/Translate.lean b/Strata/Languages/Core/DDMTransform/Translate.lean index d16660d46..5a57396bd 100644 --- a/Strata/Languages/Core/DDMTransform/Translate.lean +++ b/Strata/Languages/Core/DDMTransform/Translate.lean @@ -372,8 +372,6 @@ def translateForwardTypeDecl (bindings : TransBindings) (op : Operation) : s!"translateForwardTypeDecl expects a comma separated list: {repr bargs[0]!}") op.args[1]! let md ← getOpMetaData op - -- Create a placeholder type constructor that will be replaced by the actual - -- datatype definition in a mutual block let decl := Core.Decl.type (.con { name := name, numargs := numargs }) md return (decl, { bindings with freeVars := bindings.freeVars.push decl }) @@ -1343,6 +1341,88 @@ def translateConstructorList (p : Program) (bindings : TransBindings) (arg : Arg let constructorInfos := GlobalContext.extractConstructorInfo p.dialects arg constructorInfos.mapM (translateConstructorInfo bindings) +--------------------------------------------------------------------- +-- Common helpers for datatype translation + +/-- +Extract type arguments from a datatype's optional bindings argument. +-/ +def translateDatatypeTypeArgs (bindings : TransBindings) (arg : Arg) (errorContext : String) : + TransM (List TyIdentifier × TransBindings) := + translateOption + (fun maybearg => do + match maybearg with + | none => pure ([], bindings) + | some arg => + let bargs ← checkOpArg arg q`Core.mkBindings 1 + match bargs[0]! with + | .seq _ .comma args => + let (arr, bindings) ← translateTypeBindings bindings args + return (arr.toList, bindings) + | _ => TransM.error s!"{errorContext} expects a comma separated list: {repr bargs[0]!}") + arg + +/-- +Create a placeholder LDatatype for recursive type references. +-/ +def mkPlaceholderLDatatype (name : String) (typeArgs : List TyIdentifier) : LDatatype Visibility := + { name := name + typeArgs := typeArgs + constrs := [{ name := name, args := [], testerName := "" }] + constrs_ne := by simp } + +/-- +Filter factory function declarations to extract constructor, tester, and field accessor decls +for a single datatype. +-/ +def filterDatatypeDecls (ldatatype : LDatatype Visibility) (funcDecls : List Core.Decl) : + List Core.Decl × List Core.Decl × List Core.Decl := + let constructorNames := ldatatype.constrs.map fun c => c.name.name + let testerNames := ldatatype.constrs.map fun c => c.testerName + let fieldAccessorNames := ldatatype.constrs.foldl (fun acc c => + acc ++ (c.args.map fun (fieldName, _) => ldatatype.name ++ ".." ++ fieldName.name)) [] + + let constructorDecls := funcDecls.filter fun decl => + match decl with + | .func f => constructorNames.contains f.name.name + | _ => false + + let testerDecls := funcDecls.filter fun decl => + match decl with + | .func f => testerNames.contains f.name.name + | _ => false + + let fieldAccessorDecls := funcDecls.filter fun decl => + match decl with + | .func f => fieldAccessorNames.contains f.name.name + | _ => false + + (constructorDecls, testerDecls, fieldAccessorDecls) + +/-- +Build LConstr list from TransConstructorInfo array. +-/ +def buildLConstrs (datatypeName : String) (constructors : Array TransConstructorInfo) : + List (LConstr Visibility) := + let testerPattern : Array NamePatternPart := #[.datatype, .literal "..is", .constructor] + constructors.toList.map fun constr => + let testerName := expandNamePattern testerPattern datatypeName (some constr.name.name) + { name := constr.name + args := constr.fields.toList.map fun (fieldName, fieldType) => (fieldName, fieldType) + testerName := testerName } + +/-- +Generate factory function declarations from a list of LDatatypes. +-/ +def genDatatypeFactory (ldatatypes : List (LDatatype Visibility)) : + TransM (List Core.Decl) := do + let factory ← match genBlockFactory ldatatypes (T := CoreLParams) with + | .ok f => pure f + | .error e => TransM.error s!"Failed to generate datatype factory: {e}" + return factory.toList.map fun func => Core.Decl.func func + +--------------------------------------------------------------------- + /-- Translate a datatype declaration to Boogie declarations, updating bindings appropriately. @@ -1365,31 +1445,12 @@ def translateDatatype (p : Program) (bindings : TransBindings) (op : Operation) let datatypeName ← translateIdent String op.args[0]! -- Extract type arguments (optional bindings) - let (typeArgs, bindings) ← - translateOption - (fun maybearg => - do match maybearg with - | none => pure ([], bindings) - | some arg => - let bargs ← checkOpArg arg q`Core.mkBindings 1 - let args ← - match bargs[0]! with - | .seq _ .comma args => - let (arr, bindings) ← translateTypeBindings bindings args - return (arr.toList, bindings) - | _ => TransM.error - s!"translateDatatype expects a comma separated list: {repr bargs[0]!}") - op.args[1]! + let (typeArgs, bindings) ← translateDatatypeTypeArgs bindings op.args[1]! "translateDatatype" /- Note: Add a placeholder for the datatype type BEFORE translating constructors, for recursive constructors. Replaced with actual declaration later. -/ - let placeholderLDatatype : LDatatype Visibility := - { name := datatypeName - typeArgs := typeArgs - constrs := [{ name := datatypeName, args := [], testerName := "" }] - constrs_ne := by simp } - let placeholderDecl := Core.Decl.type (.data [placeholderLDatatype]) + let placeholderDecl := Core.Decl.type (.data [mkPlaceholderLDatatype datatypeName typeArgs]) let bindingsWithPlaceholder := { bindings with freeVars := bindings.freeVars.push placeholderDecl } -- Extract constructor information (possibly recursive) @@ -1399,15 +1460,10 @@ def translateDatatype (p : Program) (bindings : TransBindings) (op : Operation) TransM.error s!"Datatype {datatypeName} must have at least one constructor" else -- Build LConstr list from TransConstructorInfo - let testerPattern : Array NamePatternPart := #[.datatype, .literal "..is", .constructor] - let lConstrs : List (LConstr Visibility) := constructors.toList.map fun constr => - let testerName := expandNamePattern testerPattern datatypeName (some constr.name.name) - { name := constr.name - args := constr.fields.toList.map fun (fieldName, fieldType) => (fieldName, fieldType) - testerName := testerName } + let lConstrs := buildLConstrs datatypeName constructors have constrs_ne : lConstrs.length != 0 := by - simp [lConstrs] + simp [lConstrs, buildLConstrs] intro heq; subst_vars; apply h; rfl let ldatatype : LDatatype Visibility := @@ -1416,57 +1472,21 @@ def translateDatatype (p : Program) (bindings : TransBindings) (op : Operation) constrs := lConstrs constrs_ne := constrs_ne } - -- Generate factory from LDatatype and convert to Core.Decl - -- (used only for bindings.freeVars, not for allDecls) - let factory ← match genBlockFactory [ldatatype] (T := CoreLParams) with - | .ok f => pure f - | .error e => TransM.error s!"Failed to generate datatype factory: {e}" - let funcDecls : List Core.Decl := factory.toList.map fun func => - Core.Decl.func func + -- Generate factory from LDatatype + let funcDecls ← genDatatypeFactory [ldatatype] -- Only includes typeDecl, factory functions generated later let md ← getOpMetaData op let typeDecl := Core.Decl.type (.data [ldatatype]) md - let allDecls := [typeDecl] - - /- - We must add to bindings.freeVars in the same order as the DDM's - `addDatatypeBindings`: type, constructors, template functions. We do NOT - include eliminators here because the DDM does not (yet) produce them. - -/ - - let constructorNames : List String := lConstrs.map fun c => c.name.name - let testerNames : List String := lConstrs.map fun c => c.testerName - - -- Extract all field accessor names across all constructors for field projections - -- Note: DDM validates that field names are unique across constructors - -- Field accessors are named as "Datatype..fieldName" - let fieldAccessorNames : List String := lConstrs.foldl (fun acc c => - acc ++ (c.args.map fun (fieldName, _) => datatypeName ++ ".." ++ fieldName.name)) [] - - -- Filter factory functions to get constructors, testers, projections - -- TODO: this could be more efficient via `LDatatype.genFunctionMaps` - let constructorDecls := funcDecls.filter fun decl => - match decl with - | .func f => constructorNames.contains f.name.name - | _ => false - - let testerDecls := funcDecls.filter fun decl => - match decl with - | .func f => testerNames.contains f.name.name - | _ => false - - let fieldAccessorDecls := funcDecls.filter fun decl => - match decl with - | .func f => fieldAccessorNames.contains f.name.name - | _ => false + -- Filter and add declarations to bindings + let (constructorDecls, testerDecls, fieldAccessorDecls) := filterDatatypeDecls ldatatype funcDecls let bindingDecls := typeDecl :: constructorDecls ++ testerDecls ++ fieldAccessorDecls let bindings := bindingDecls.foldl (fun b d => { b with freeVars := b.freeVars.push d } ) bindings - return (allDecls, bindings) + return ([typeDecl], bindings) /-- Translate a mutual block containing mutually recursive datatype definitions. @@ -1491,39 +1511,15 @@ def translateMutualBlock (p : Program) (bindings : TransBindings) (op : Operatio TransM.error "Mutual block must contain at least one datatype" else -- First pass: collect all datatype names, type args, and their indices in freeVars - -- The forward declarations should already be in bindings.freeVars + -- Forward declarations MUST already be in bindings.freeVars let mut datatypeInfos : Array (String × List TyIdentifier × Nat) := #[] let mut bindingsWithPlaceholders := bindings for dtOp in datatypeOps do let datatypeName ← translateIdent String dtOp.args[0]! - let (typeArgs, _) ← - translateOption - (fun maybearg => - do match maybearg with - | none => pure ([], bindings) - | some arg => - let bargs ← checkOpArg arg q`Core.mkBindings 1 - let args ← - match bargs[0]! with - | .seq _ .comma args => - let (arr, _) ← translateTypeBindings bindings args - return (arr.toList, bindings) - | _ => TransM.error - s!"translateMutualBlock expects a comma separated list: {repr bargs[0]!}") - dtOp.args[1]! + let (typeArgs, _) ← translateDatatypeTypeArgs bindings dtOp.args[1]! "translateMutualBlock" -- Find the index of this datatype in freeVars (from forward declaration) - -- or add a new placeholder if not forward-declared - let idx := bindingsWithPlaceholders.freeVars.size - let placeholderLDatatype : LDatatype Visibility := - { name := datatypeName - typeArgs := typeArgs - constrs := [{ name := datatypeName, args := [], testerName := "" }] - constrs_ne := by simp } - let placeholderDecl := Core.Decl.type (.data [placeholderLDatatype]) - - -- Check if there's already an entry for this datatype (from forward declaration) let existingIdx := bindings.freeVars.findIdx? fun decl => match decl with | .type t _ => t.names.contains datatypeName @@ -1531,15 +1527,12 @@ def translateMutualBlock (p : Program) (bindings : TransBindings) (op : Operatio match existingIdx with | some i => - -- Update existing entry with placeholder + let placeholderDecl := Core.Decl.type (.data [mkPlaceholderLDatatype datatypeName typeArgs]) datatypeInfos := datatypeInfos.push (datatypeName, typeArgs, i) bindingsWithPlaceholders := { bindingsWithPlaceholders with freeVars := bindingsWithPlaceholders.freeVars.set! i placeholderDecl } | none => - -- Add new placeholder - datatypeInfos := datatypeInfos.push (datatypeName, typeArgs, idx) - bindingsWithPlaceholders := { bindingsWithPlaceholders with - freeVars := bindingsWithPlaceholders.freeVars.push placeholderDecl } + TransM.error s!"Mutual datatype {datatypeName} requires a forward declaration" -- Second pass: translate all constructors with all placeholders in scope let mut ldatatypes : List (LDatatype Visibility) := [] @@ -1552,15 +1545,10 @@ def translateMutualBlock (p : Program) (bindings : TransBindings) (op : Operatio TransM.error s!"Datatype {datatypeName} must have at least one constructor" else -- Build LConstr list - let testerPattern : Array NamePatternPart := #[.datatype, .literal "..is", .constructor] - let lConstrs : List (LConstr Visibility) := constructors.toList.map fun constr => - let testerName := expandNamePattern testerPattern datatypeName (some constr.name.name) - { name := constr.name - args := constr.fields.toList.map fun (fieldName, fieldType) => (fieldName, fieldType) - testerName := testerName } + let lConstrs := buildLConstrs datatypeName constructors have constrs_ne : lConstrs.length != 0 := by - simp [lConstrs] + simp [lConstrs, buildLConstrs] intro heq; subst_vars; apply h; rfl let ldatatype : LDatatype Visibility := @@ -1572,11 +1560,7 @@ def translateMutualBlock (p : Program) (bindings : TransBindings) (op : Operatio ldatatypes := ldatatypes ++ [ldatatype] -- Generate factory functions for the ENTIRE mutual block at once - let factory ← match genBlockFactory ldatatypes (T := CoreLParams) with - | .ok f => pure f - | .error e => TransM.error s!"Failed to generate datatype factory: {e}" - let allFuncDecls : List Core.Decl := factory.toList.map fun func => - Core.Decl.func func + let allFuncDecls ← genDatatypeFactory ldatatypes -- Create the mutual TypeDecl with all datatypes let md ← getOpMetaData op @@ -1596,26 +1580,7 @@ def translateMutualBlock (p : Program) (bindings : TransBindings) (op : Operatio -- Add constructor, tester, and accessor functions for each datatype for ldatatype in ldatatypes do - let constructorNames := ldatatype.constrs.map fun c => c.name.name - let testerNames := ldatatype.constrs.map fun c => c.testerName - let fieldNames := ldatatype.constrs.foldl (fun acc c => - acc ++ (c.args.map fun (fieldName, _) => ldatatype.name ++ ".." ++ fieldName.name)) [] - - let constructorDecls := allFuncDecls.filter fun decl => - match decl with - | .func f => constructorNames.contains f.name.name - | _ => false - - let testerDecls := allFuncDecls.filter fun decl => - match decl with - | .func f => testerNames.contains f.name.name - | _ => false - - let fieldAccessorDecls := allFuncDecls.filter fun decl => - match decl with - | .func f => fieldNames.contains f.name.name - | _ => false - + let (constructorDecls, testerDecls, fieldAccessorDecls) := filterDatatypeDecls ldatatype allFuncDecls for d in constructorDecls ++ testerDecls ++ fieldAccessorDecls do finalBindings := { finalBindings with freeVars := finalBindings.freeVars.push d } From 59223fd281f685873f39b24d39bafbc0fc083c3d Mon Sep 17 00:00:00 2001 From: Josh Cohen Date: Fri, 30 Jan 2026 10:58:41 -0500 Subject: [PATCH 08/12] Some refactoring in Translate.lean --- .../Core/DDMTransform/Translate.lean | 75 +++++++------------ 1 file changed, 25 insertions(+), 50 deletions(-) diff --git a/Strata/Languages/Core/DDMTransform/Translate.lean b/Strata/Languages/Core/DDMTransform/Translate.lean index 5a57396bd..673e378d8 100644 --- a/Strata/Languages/Core/DDMTransform/Translate.lean +++ b/Strata/Languages/Core/DDMTransform/Translate.lean @@ -1438,7 +1438,7 @@ duplicates. - `op`: The `command_datatype` operation to translate -/ def translateDatatype (p : Program) (bindings : TransBindings) (op : Operation) : - TransM (Core.Decls × TransBindings) := do + TransM (Core.Decl × TransBindings) := do -- Check operation has correct name and argument count let _ ← @checkOp (Core.Decls × TransBindings) op q`Core.command_datatype 3 @@ -1475,7 +1475,6 @@ def translateDatatype (p : Program) (bindings : TransBindings) (op : Operation) -- Generate factory from LDatatype let funcDecls ← genDatatypeFactory [ldatatype] - -- Only includes typeDecl, factory functions generated later let md ← getOpMetaData op let typeDecl := Core.Decl.type (.data [ldatatype]) md @@ -1486,7 +1485,7 @@ def translateDatatype (p : Program) (bindings : TransBindings) (op : Operation) { b with freeVars := b.freeVars.push d } ) bindings - return ([typeDecl], bindings) + return (typeDecl, bindings) /-- Translate a mutual block containing mutually recursive datatype definitions. @@ -1494,7 +1493,7 @@ This collects all datatypes, creates a single TypeDecl.data with all of them, and updates the forward-declared entries in bindings.freeVars. -/ def translateMutualBlock (p : Program) (bindings : TransBindings) (op : Operation) : - TransM (Core.Decls × TransBindings) := do + TransM (Core.Decl × TransBindings) := do let _ ← @checkOp (Core.Decls × TransBindings) op q`Core.command_mutual 1 -- Extract commands from the SpacePrefixSepBy @@ -1535,29 +1534,16 @@ def translateMutualBlock (p : Program) (bindings : TransBindings) (op : Operatio TransM.error s!"Mutual datatype {datatypeName} requires a forward declaration" -- Second pass: translate all constructors with all placeholders in scope - let mut ldatatypes : List (LDatatype Visibility) := [] - - for (dtOp, (datatypeName, typeArgs, _idx)) in datatypeOps.zip datatypeInfos do - -- Extract constructor information + let ldatatypes ← (datatypeOps.zip datatypeInfos).toList.mapM fun (dtOp, (datatypeName, typeArgs, _idx)) => do let constructors ← translateConstructorList p bindingsWithPlaceholders dtOp.args[2]! - if h : constructors.size == 0 then TransM.error s!"Datatype {datatypeName} must have at least one constructor" else - -- Build LConstr list let lConstrs := buildLConstrs datatypeName constructors - have constrs_ne : lConstrs.length != 0 := by simp [lConstrs, buildLConstrs] intro heq; subst_vars; apply h; rfl - - let ldatatype : LDatatype Visibility := - { name := datatypeName - typeArgs := typeArgs - constrs := lConstrs - constrs_ne := constrs_ne } - - ldatatypes := ldatatypes ++ [ldatatype] + pure { name := datatypeName, typeArgs := typeArgs, constrs := lConstrs, constrs_ne := constrs_ne } -- Generate factory functions for the ENTIRE mutual block at once let allFuncDecls ← genDatatypeFactory ldatatypes @@ -1584,7 +1570,7 @@ def translateMutualBlock (p : Program) (bindings : TransBindings) (op : Operatio for d in constructorDecls ++ testerDecls ++ fieldAccessorDecls do finalBindings := { finalBindings with freeVars := finalBindings.freeVars.push d } - return ([mutualTypeDecl], finalBindings) + return (mutualTypeDecl, finalBindings) --------------------------------------------------------------------- @@ -1609,50 +1595,39 @@ partial def translateCoreDecls (p : Program) (bindings : TransBindings) : | 0 => return ([], bindings) | _ + 1 => let op := ops[count]! - -- Commands that produce multiple declarations let (newDecls, bindings) ← match op.name with - | q`Core.command_datatype => - translateDatatype p bindings op - | q`Core.command_mutual => - translateMutualBlock p bindings op + | q`Core.command_forward_typedecl => + -- Forward declarations do NOT produce AST nodes - they only update bindings + let (_, bindings) ← translateForwardTypeDecl bindings op + pure ([], bindings) | _ => - -- All other commands produce a single declaration - let (decls, bindings) ← + let (decl, bindings) ← match op.name with + | q`Core.command_datatype => + translateDatatype p bindings op + | q`Core.command_mutual => + translateMutualBlock p bindings op | q`Core.command_var => - let (decl, bindings) ← translateGlobalVar bindings op - pure ([decl], bindings) + translateGlobalVar bindings op | q`Core.command_constdecl => - let (decl, bindings) ← translateConstant bindings op - pure ([decl], bindings) + translateConstant bindings op | q`Core.command_typedecl => - let (decl, bindings) ← translateTypeDecl bindings op - pure ([decl], bindings) - | q`Core.command_forward_typedecl => - -- Forward declarations do NOT produce AST nodes - they only update bindings - let (_, bindings) ← translateForwardTypeDecl bindings op - pure ([], bindings) + translateTypeDecl bindings op | q`Core.command_typesynonym => - let (decl, bindings) ← translateTypeSynonym bindings op - pure ([decl], bindings) + translateTypeSynonym bindings op | q`Core.command_axiom => - let (decl, bindings) ← translateAxiom p bindings op - pure ([decl], bindings) + translateAxiom p bindings op | q`Core.command_distinct => - let (decl, bindings) ← translateDistinct p bindings op - pure ([decl], bindings) + translateDistinct p bindings op | q`Core.command_procedure => - let (decl, bindings) ← translateProcedure p bindings op - pure ([decl], bindings) + translateProcedure p bindings op | q`Core.command_fndef => - let (decl, bindings) ← translateFunction .Definition p bindings op - pure ([decl], bindings) + translateFunction .Definition p bindings op | q`Core.command_fndecl => - let (decl, bindings) ← translateFunction .Declaration p bindings op - pure ([decl], bindings) + translateFunction .Declaration p bindings op | _ => TransM.error s!"translateCoreDecls unimplemented for {repr op}" - pure (decls, bindings) + pure ([decl], bindings) let (decls, bindings) ← go (count + 1) max bindings ops return (newDecls ++ decls, bindings) From 45684291e3fd8980a62fdb5c58d4240f12e6567c Mon Sep 17 00:00:00 2001 From: Josh Cohen Date: Fri, 30 Jan 2026 11:00:22 -0500 Subject: [PATCH 09/12] Remove duplicate test file --- .../Core/Examples/DatatypeRoseTree.lean | 322 ------------------ 1 file changed, 322 deletions(-) delete mode 100644 StrataTest/Languages/Core/Examples/DatatypeRoseTree.lean diff --git a/StrataTest/Languages/Core/Examples/DatatypeRoseTree.lean b/StrataTest/Languages/Core/Examples/DatatypeRoseTree.lean deleted file mode 100644 index 92972738c..000000000 --- a/StrataTest/Languages/Core/Examples/DatatypeRoseTree.lean +++ /dev/null @@ -1,322 +0,0 @@ -/- - Copyright Strata Contributors - - SPDX-License-Identifier: Apache-2.0 OR MIT --/ - -import Strata.Languages.Core.Verifier - -/-! -# Datatype Rose Tree Integration Test - -Tests mutually recursive Rose Tree datatypes using the DDM datatype declaration syntax. -A rose tree is a tree where each node has a value and a list of children (forest). - -This requires mutually recursive types: -- RoseTree: a node with a value and a forest of children -- Forest: a list of rose trees - -Verifies: -- Parsing of mutually recursive datatype declarations -- Tester functions for both types -- Destructor functions for field access -- Type-checking and verification with mutually recursive types --/ - -namespace Strata.DatatypeRoseTreeTest - ---------------------------------------------------------------------- --- Test 1: Basic Rose Tree Datatype Declaration and Tester Functions ---------------------------------------------------------------------- - -def roseTreeTesterPgm : Program := -#strata -program Core; - -// Define mutually recursive Rose Tree and Forest datatypes using mutual block -// Forest is a list of RoseTrees -forward type RoseTree; -forward type Forest; -mutual - datatype Forest { FNil(), FCons(head: RoseTree, tail: Forest) }; - datatype RoseTree { Node(val: int, children: Forest) }; -end; - -procedure TestRoseTreeTesters() returns () -spec { - ensures true; -} -{ - var t : RoseTree; - var f : Forest; - - // Create an empty forest - f := FNil(); - - // Test that f is FNil - assert [isFNil]: Forest..isFNil(f); - - // Test that f is not FCons - assert [notFCons]: !Forest..isFCons(f); - - // Create a leaf node (node with empty forest) - t := Node(42, FNil()); - - // Test that t is Node - assert [isNode]: RoseTree..isNode(t); - - // Create a non-empty forest - f := FCons(Node(1, FNil()), FNil()); - - // Test that f is FCons - assert [isFCons]: Forest..isFCons(f); - - // Test that f is not FNil - assert [notFNil]: !Forest..isFNil(f); -}; -#end - -/-- info: true -/ -#guard_msgs in -#eval TransM.run Inhabited.default (translateProgram roseTreeTesterPgm) |>.snd |>.isEmpty - -/-- -info: -Obligation: isFNil -Property: assert -Result: ✅ pass - -Obligation: notFCons -Property: assert -Result: ✅ pass - -Obligation: isNode -Property: assert -Result: ✅ pass - -Obligation: isFCons -Property: assert -Result: ✅ pass - -Obligation: notFNil -Property: assert -Result: ✅ pass - -Obligation: TestRoseTreeTesters_ensures_0 -Property: assert -Result: ✅ pass --/ -#guard_msgs in -#eval verify "cvc5" roseTreeTesterPgm Inhabited.default Options.quiet - ---------------------------------------------------------------------- --- Test 2: Rose Tree Destructor Functions ---------------------------------------------------------------------- - -def roseTreeDestructorPgm : Program := -#strata -program Core; - -forward type RoseTree; -forward type Forest; -mutual - datatype Forest { FNil(), FCons(head: RoseTree, tail: Forest) }; - datatype RoseTree { Node(val: int, children: Forest) }; -end; - -procedure TestRoseTreeDestructor() returns () -spec { - ensures true; -} -{ - var t : RoseTree; - var f : Forest; - var v : int; - var c : Forest; - - // Create a leaf node - t := Node(42, FNil()); - - // Extract the value - v := RoseTree..val(t); - assert [valIs42]: v == 42; - - // Extract the children (should be empty forest) - c := RoseTree..children(t); - assert [childrenIsNil]: Forest..isFNil(c); - - // Create a forest with one tree - f := FCons(Node(10, FNil()), FNil()); - - // Extract the head - t := Forest..head(f); - assert [headIsNode]: RoseTree..isNode(t); - assert [headVal]: RoseTree..val(t) == 10; - - // Extract the tail - f := Forest..tail(f); - assert [tailIsNil]: Forest..isFNil(f); -}; -#end - -/-- info: true -/ -#guard_msgs in -#eval TransM.run Inhabited.default (translateProgram roseTreeDestructorPgm) |>.snd |>.isEmpty - -/-- -info: -Obligation: valIs42 -Property: assert -Result: ✅ pass - -Obligation: childrenIsNil -Property: assert -Result: ✅ pass - -Obligation: headIsNode -Property: assert -Result: ✅ pass - -Obligation: headVal -Property: assert -Result: ✅ pass - -Obligation: tailIsNil -Property: assert -Result: ✅ pass - -Obligation: TestRoseTreeDestructor_ensures_0 -Property: assert -Result: ✅ pass --/ -#guard_msgs in -#eval verify "cvc5" roseTreeDestructorPgm Inhabited.default Options.quiet - ---------------------------------------------------------------------- --- Test 3: Rose Tree Equality ---------------------------------------------------------------------- - -def roseTreeEqualityPgm : Program := -#strata -program Core; - -forward type RoseTree; -forward type Forest; -mutual - datatype Forest { FNil(), FCons(head: RoseTree, tail: Forest) }; - datatype RoseTree { Node(val: int, children: Forest) }; -end; - -procedure TestRoseTreeEquality() returns () -spec { - ensures true; -} -{ - var t1 : RoseTree; - var t2 : RoseTree; - var f1 : Forest; - var f2 : Forest; - - // Create two identical leaf nodes - t1 := Node(42, FNil()); - t2 := Node(42, FNil()); - assert [leafEquality]: t1 == t2; - - // Create two identical empty forests - f1 := FNil(); - f2 := FNil(); - assert [emptyForestEquality]: f1 == f2; - - // Create two identical non-empty forests - f1 := FCons(Node(1, FNil()), FNil()); - f2 := FCons(Node(1, FNil()), FNil()); - assert [forestEquality]: f1 == f2; -}; -#end - -/-- info: true -/ -#guard_msgs in -#eval TransM.run Inhabited.default (translateProgram roseTreeEqualityPgm) |>.snd |>.isEmpty - -/-- -info: -Obligation: leafEquality -Property: assert -Result: ✅ pass - -Obligation: emptyForestEquality -Property: assert -Result: ✅ pass - -Obligation: forestEquality -Property: assert -Result: ✅ pass - -Obligation: TestRoseTreeEquality_ensures_0 -Property: assert -Result: ✅ pass --/ -#guard_msgs in -#eval verify "cvc5" roseTreeEqualityPgm Inhabited.default Options.quiet - ---------------------------------------------------------------------- --- Test 4: Polymorphic Rose Tree ---------------------------------------------------------------------- - -def polyRoseTreeHavocPgm : Program := -#strata -program Core; - -forward type RoseTree (a : Type); -forward type Forest (a : Type); -mutual - datatype Forest (a : Type) { FNil(), FCons(head: RoseTree a, tail: Forest a) }; - datatype RoseTree (a : Type) { Node(val: a, children: Forest a) }; -end; - -procedure TestPolyRoseTreeHavoc() returns () -spec { - ensures true; -} -{ - var t : RoseTree int; - var f : Forest int; - - havoc t; - havoc f; - - assume t == Node(42, FNil()); - assume f == FCons(t, FNil()); - - assert [valIs42]: RoseTree..val(t) == 42; - assert [headIsT]: Forest..head(f) == t; - assert [headVal]: RoseTree..val(Forest..head(f)) == 42; -}; -#end - -/-- info: true -/ -#guard_msgs in -#eval TransM.run Inhabited.default (translateProgram polyRoseTreeHavocPgm) |>.snd |>.isEmpty - -/-- -info: -Obligation: valIs42 -Property: assert -Result: ✅ pass - -Obligation: headIsT -Property: assert -Result: ✅ pass - -Obligation: headVal -Property: assert -Result: ✅ pass - -Obligation: TestPolyRoseTreeHavoc_ensures_0 -Property: assert -Result: ✅ pass --/ -#guard_msgs in -#eval verify "cvc5" polyRoseTreeHavocPgm Inhabited.default Options.quiet - -end Strata.DatatypeRoseTreeTest From e008e68714bdcf61303e9b4cf035e786c1598aef Mon Sep 17 00:00:00 2001 From: Josh Cohen Date: Fri, 30 Jan 2026 11:02:51 -0500 Subject: [PATCH 10/12] Clean up test file --- .../Core/Examples/MutualDatatypes.lean | 34 +------------------ 1 file changed, 1 insertion(+), 33 deletions(-) diff --git a/StrataTest/Languages/Core/Examples/MutualDatatypes.lean b/StrataTest/Languages/Core/Examples/MutualDatatypes.lean index 5e6859a1a..e8b8365ff 100644 --- a/StrataTest/Languages/Core/Examples/MutualDatatypes.lean +++ b/StrataTest/Languages/Core/Examples/MutualDatatypes.lean @@ -10,13 +10,6 @@ import Strata.Languages.Core.Verifier # Mutual Datatype Integration Tests Tests mutually recursive datatypes using the DDM datatype declaration syntax. - -Verifies: -- Parsing of mutually recursive datatype declarations -- Tester functions for both types -- Destructor functions for field access -- Type-checking and verification with mutually recursive types -- Polymorphic mutually recursive types -/ namespace Strata.MutualDatatypeTest @@ -29,8 +22,6 @@ def roseTreeTesterPgm : Program := #strata program Core; -// Define mutually recursive Rose Tree and Forest datatypes using mutual block -// Forest is a list of RoseTrees forward type RoseTree; forward type Forest; mutual @@ -46,28 +37,15 @@ spec { var t : RoseTree; var f : Forest; - // Create an empty forest f := FNil(); - - // Test that f is FNil assert [isFNil]: Forest..isFNil(f); - - // Test that f is not FCons assert [notFCons]: !Forest..isFCons(f); - // Create a leaf node (node with empty forest) t := Node(42, FNil()); - - // Test that t is Node assert [isNode]: RoseTree..isNode(t); - // Create a non-empty forest f := FCons(Node(1, FNil()), FNil()); - - // Test that f is FCons assert [isFCons]: Forest..isFCons(f); - - // Test that f is not FNil assert [notFNil]: !Forest..isFNil(f); }; #end @@ -130,26 +108,20 @@ spec { var v : int; var c : Forest; - // Create a leaf node t := Node(42, FNil()); - // Extract the value v := RoseTree..val(t); assert [valIs42]: v == 42; - // Extract the children (should be empty forest) c := RoseTree..children(t); assert [childrenIsNil]: Forest..isFNil(c); - // Create a forest with one tree f := FCons(Node(10, FNil()), FNil()); - // Extract the head t := Forest..head(f); assert [headIsNode]: RoseTree..isNode(t); assert [headVal]: RoseTree..val(t) == 10; - // Extract the tail f := Forest..tail(f); assert [tailIsNil]: Forest..isFNil(f); }; @@ -213,17 +185,14 @@ spec { var f1 : Forest; var f2 : Forest; - // Create two identical leaf nodes t1 := Node(42, FNil()); t2 := Node(42, FNil()); assert [leafEquality]: t1 == t2; - // Create two identical empty forests f1 := FNil(); f2 := FNil(); assert [emptyForestEquality]: f1 == f2; - // Create two identical non-empty forests f1 := FCons(Node(1, FNil()), FNil()); f2 := FCons(Node(1, FNil()), FNil()); assert [forestEquality]: f1 == f2; @@ -319,8 +288,7 @@ Result: ✅ pass -- Test 5: Imperative Stmt/StmtList with Havoc (SMT verification) --------------------------------------------------------------------- -/-- Mutually recursive Stmt/StmtList modeling the Imperative dialect's - statement structure with explicit list type instead of nested List. -/ +/-- Mutually recursive Stmt/StmtList modeling Imperative.Stmt -/ def stmtListHavocPgm : Program := #strata program Core; From 8e513422f7f10fabc242d4fb6464281c2eebaea0 Mon Sep 17 00:00:00 2001 From: Josh Cohen Date: Fri, 30 Jan 2026 12:25:00 -0500 Subject: [PATCH 11/12] Add DDM mutual test, fix issue with datatypes as type parameters --- Strata/DDM/Elab/Core.lean | 14 ++- StrataTest/DDM/MutualDatatypes.lean | 140 ++++++++++++++++++++++++++++ 2 files changed, 149 insertions(+), 5 deletions(-) create mode 100644 StrataTest/DDM/MutualDatatypes.lean diff --git a/Strata/DDM/Elab/Core.lean b/Strata/DDM/Elab/Core.lean index 54851ca9a..9a924882b 100644 --- a/Strata/DDM/Elab/Core.lean +++ b/Strata/DDM/Elab/Core.lean @@ -1050,11 +1050,15 @@ partial def runSyntaxElaborator | .ofIdentInfo info => info.val | _ => panic! "Expected identifier for datatype name" let baseCtx := typeParamsT.resultContext - -- Extract type parameter names from the bindings - let typeParamNames := baseCtx.bindings.toArray.filterMap fun b => - match b.kind with - | .type _ [] _ => some b.ident - | _ => none + /- Extract type parameter names only from NEW bindings added by + typeParams, not inherited bindings (which may include datatypes from + previous commands) -/ + let inheritedCount := tctx0.bindings.size + let typeParamNames := baseCtx.bindings.toArray.extract inheritedCount baseCtx.bindings.size + |>.filterMap fun b => + match b.kind with + | .type _ [] _ => some b.ident + | _ => none -- Add the datatype name to the GlobalContext as a type let gctx := baseCtx.globalContext let gctx := diff --git a/StrataTest/DDM/MutualDatatypes.lean b/StrataTest/DDM/MutualDatatypes.lean new file mode 100644 index 000000000..4d4a2f071 --- /dev/null +++ b/StrataTest/DDM/MutualDatatypes.lean @@ -0,0 +1,140 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.DDM.Integration.Lean + +/-! +# Tests for mutual datatype blocks in DDM + +Tests that mutually recursive datatypes can be declared via forward +declarations and mutual blocks. +-/ + +#dialect +dialect TestMutual; + +metadata declareDatatype (name : Ident, typeParams : Ident, constructors : Ident); + +type int; + +category Binding; +@[declare(name, tp)] +op mkBinding (name : Ident, tp : TypeP) : Binding => @[prec(40)] name ":" tp; + +category Bindings; +@[scope(bindings)] +op mkBindings (bindings : CommaSepBy Binding) : Bindings => "(" bindings ")"; + +category Constructor; +category ConstructorList; + +@[constructor(name, fields)] +op constructor_mk (name : Ident, fields : Option (CommaSepBy Binding)) : Constructor => + name "(" fields ")"; + +@[constructorListAtom(c)] +op constructorListAtom (c : Constructor) : ConstructorList => c; + +@[constructorListPush(cl, c)] +op constructorListPush (cl : ConstructorList, c : Constructor) : ConstructorList => + cl ", " c; + +@[declareTypeForward(name, none)] +op command_forward (name : Ident) : Command => + "forward type " name ";\n"; + +@[declareDatatype(name, typeParams, constructors)] +op command_datatype (name : Ident, + typeParams : Option Bindings, + @[scopeDatatype(name, typeParams)] constructors : ConstructorList) : Command => + "datatype " name typeParams " { " constructors " };\n"; + +@[scope(commands)] +op command_mutual (commands : SpacePrefixSepBy Command) : Command => + "mutual\n" indent(2, commands) "end;\n"; + +#end + +--------------------------------------------------------------------- +-- Test 1: Basic mutual recursion (Tree/Forest) +--------------------------------------------------------------------- + +def mutualBasicPgm := +#strata +program TestMutual; +forward type Tree; +forward type Forest; +mutual + datatype Tree { Node(val: int, children: Forest) }; + datatype Forest { FNil(), FCons(head: Tree, tail: Forest) }; +end; +#end + +/-- +info: program TestMutual; +forward type Tree; +forward type Forest; +mutual + datatype Tree { (Node)(val:int, children:Forest) }; + datatype Forest { ((FNil)()), ((FCons)(head:Tree, tail:Forest)) }; +end; +-/ +#guard_msgs in +#eval IO.println mutualBasicPgm + +--------------------------------------------------------------------- +-- Test 2: Single datatype in mutual block (should not actually be used) +--------------------------------------------------------------------- + +def mutualSinglePgm := +#strata +program TestMutual; +forward type List; +mutual + datatype List { Nil(), Cons(head: int, tail: List) }; +end; +#end + +/-- +info: program TestMutual; +forward type List; +mutual + datatype List { ((Nil)()), ((Cons)(head:int, tail:List)) }; +end; +-/ +#guard_msgs in +#eval IO.println mutualSinglePgm + +--------------------------------------------------------------------- +-- Test 3: Three-way mutual recursion +--------------------------------------------------------------------- + +def mutualThreeWayPgm := +#strata +program TestMutual; +forward type A; +forward type B; +forward type C; +mutual + datatype A { MkA(toB: B) }; + datatype B { MkB(toC: C) }; + datatype C { MkC(toA: A), CBase() }; +end; +#end + +/-- +info: program TestMutual; +forward type A; +forward type B; +forward type C; +mutual + datatype A { (MkA)(toB:B) }; + datatype B { (MkB)(toC:C) }; + datatype C { ((MkC)(toA:A)), ((CBase)()) }; +end; +-/ +#guard_msgs in +#eval IO.println mutualThreeWayPgm From 52e7b086d5077e700995dbced794bf57b374a02d Mon Sep 17 00:00:00 2001 From: Josh Cohen Date: Fri, 30 Jan 2026 17:24:51 -0500 Subject: [PATCH 12/12] Change "end" label to "_exit" to avoid name clashes --- .../Core/Examples/RemoveIrrelevantAxioms.lean | 10 ++++---- StrataTest/Transform/ProcedureInlining.lean | 12 +++++----- .../BoogieToStrata/Source/StrataGenerator.cs | 4 ++-- Tools/BoogieToStrata/Tests/B.bpl | 24 +++++++++---------- 4 files changed, 25 insertions(+), 25 deletions(-) diff --git a/StrataTest/Languages/Core/Examples/RemoveIrrelevantAxioms.lean b/StrataTest/Languages/Core/Examples/RemoveIrrelevantAxioms.lean index e4ee62fcc..220aa1436 100644 --- a/StrataTest/Languages/Core/Examples/RemoveIrrelevantAxioms.lean +++ b/StrataTest/Languages/Core/Examples/RemoveIrrelevantAxioms.lean @@ -39,7 +39,7 @@ procedure P() returns () assert f(23); assert f(-(5)); } - end1 : {} + _exit : {} }; procedure Q0(x : int) returns () @@ -49,7 +49,7 @@ procedure Q0(x : int) returns () assert (x == 2); assert (x == 2); } - end1 : {} + _exit : {} }; procedure Q1(x : int) returns () @@ -59,7 +59,7 @@ procedure Q1(x : int) returns () assert (x == 2); assert (x == 2); } - end1 : {} + _exit : {} }; procedure Q2(x : int) returns () @@ -69,7 +69,7 @@ procedure Q2(x : int) returns () assert (x == 2); assert (x == 2); } - end1 : {} + _exit : {} }; procedure Q3(x : int) returns () @@ -79,7 +79,7 @@ procedure Q3(x : int) returns () assert (x == 2); assert (x == 2); } - end1 : {} + _exit : {} }; #end diff --git a/StrataTest/Transform/ProcedureInlining.lean b/StrataTest/Transform/ProcedureInlining.lean index c1e1814b9..c83b45b57 100644 --- a/StrataTest/Transform/ProcedureInlining.lean +++ b/StrataTest/Transform/ProcedureInlining.lean @@ -294,17 +294,17 @@ def Test2 := program Core; procedure f(x : bool) returns (y : bool) { if (x) { - goto end1; + goto _exit; } else { y := false; } - end1: {} + _exit: {} }; procedure h() returns () { var b_in : bool; var b_out : bool; call b_out := f(b_in); - end1: {} + _exit: {} }; #end @@ -313,10 +313,10 @@ def Test2Ans := program Core; procedure f(x : bool) returns (y : bool) { if (x) { - goto end1; + goto _exit; } else { y := false; } - end1: {} + _exit: {} }; procedure h() returns () { @@ -334,7 +334,7 @@ procedure h() returns () { f_end: {} b_out := f_y; } - end1: {} + _exit: {} }; #end diff --git a/Tools/BoogieToStrata/Source/StrataGenerator.cs b/Tools/BoogieToStrata/Source/StrataGenerator.cs index 1bd7448fe..b854f8ea3 100644 --- a/Tools/BoogieToStrata/Source/StrataGenerator.cs +++ b/Tools/BoogieToStrata/Source/StrataGenerator.cs @@ -846,7 +846,7 @@ public override Cmd VisitAssignCmd(AssignCmd node) { } public override ReturnCmd VisitReturnCmd(ReturnCmd node) { - IndentLine("goto end;"); + IndentLine("goto _exit;"); return node; } @@ -1333,7 +1333,7 @@ public override Implementation VisitImplementation(Implementation node) { } } - IndentLine("end : {}"); + IndentLine("_exit : {}"); DecIndent(); WriteLine("};"); diff --git a/Tools/BoogieToStrata/Tests/B.bpl b/Tools/BoogieToStrata/Tests/B.bpl index 00d8c37b8..0465acefb 100644 --- a/Tools/BoogieToStrata/Tests/B.bpl +++ b/Tools/BoogieToStrata/Tests/B.bpl @@ -14,13 +14,13 @@ procedure Q0() Then: h := 15; - goto end; + goto _exit; Else: assume h == 0; - goto end; + goto _exit; - end: + _exit: assert 0 <= h; return; } @@ -34,13 +34,13 @@ procedure Q1() Then: h := -15; - goto end; + goto _exit; Else: assume h == 0; - goto end; + goto _exit; - end: + _exit: h := -h; assert 0 <= h; return; @@ -54,13 +54,13 @@ procedure P0(this: ref) Then: Heap[this, N] := 15; - goto end; + goto _exit; Else: assume Heap[this, N] == 0; - goto end; + goto _exit; - end: + _exit: assert 0 <= Heap[this, N]; return; } @@ -73,13 +73,13 @@ procedure P1(this: ref) Then: Heap[this, N] := -15; - goto end; + goto _exit; Else: assume Heap[this, N] == 0; - goto end; + goto _exit; - end: + _exit: Heap[this, N] := -Heap[this, N]; assert 0 <= Heap[this, N]; return;