Struct/record type declarations with named field access in Boole

Strata/DDM/AST.lean

@@ -937,6 +937,21 @@ structure DatatypeBindingSpec (argDecls : ArgDecls) where
   functionTemplates : Array FunctionTemplate := #[]
   deriving Repr
 
+/--
+Specification for single-constructor record type declarations.
+Like `DatatypeBindingSpec` but the fields are given directly as `CommaSepBy Binding`
+rather than through a `ConstructorList`; a single constructor named `T_mk` is
+synthesized automatically.
+-/
+structure RecordBindingSpec (argDecls : ArgDecls) where
+  /-- deBrujin index of the record type name -/
+  nameIndex : DebruijnIndex argDecls.size
+  /-- deBrujin index of the field list (`CommaSepBy Binding`) -/
+  fieldsIndex : DebruijnIndex argDecls.size
+  /-- Optional list of function templates (selectors, etc.) to expand -/
+  functionTemplates : Array FunctionTemplate := #[]
+  deriving Repr
+
 /--
 Specification for declaring a single type variable.
 Creates a .tvar binding in the result context.
@@ -954,6 +969,7 @@ inductive BindingSpec (argDecls : ArgDecls) where
 | type (_ : TypeBindingSpec argDecls)
 | scopedType (_ : TypeBindingSpec argDecls)  -- Type added to global context
 | datatype (_ : DatatypeBindingSpec argDecls)
+| record (_ : RecordBindingSpec argDecls)
 | tvar (_ : TvarBindingSpec argDecls)
 deriving Repr
 
@@ -964,6 +980,7 @@ def nameIndex {argDecls} : BindingSpec argDecls → DebruijnIndex argDecls.size
 | .type v => v.nameIndex
 | .scopedType v => v.nameIndex
 | .datatype v => v.nameIndex
+| .record v => v.nameIndex
 | .tvar v => v.nameIndex
 
 end BindingSpec
@@ -1127,6 +1144,25 @@ def parseNewBindings (md : Metadata) (argDecls : ArgDecls) : Array (BindingSpec
             constructorsIndex := ⟨constructorsIndex, constructorsP⟩,
             functionTemplates
           }
+        | { dialect := _, name := "declareRecord" } => do
+          let args := attr.args
+          if args.size < 2 then
+            newBindingErr "declareRecord expects at least 2 arguments (name, fields)."
+            return none
+          let .catbvar nameIndex := args[0]!
+            | newBindingErr "declareRecord: invalid name index"; return none
+          let .catbvar fieldsIndex := args[1]!
+            | newBindingErr "declareRecord: invalid fields index"; return none
+          let .isTrue nameP := decideProp (nameIndex < argDecls.size)
+            | return panic! "Invalid name index"
+          let .isTrue fieldsP := decideProp (fieldsIndex < argDecls.size)
+            | return panic! "Invalid fields index"
+          let functionTemplates ← parseFunctionTemplates (args.extract 2 args.size)
+          some <$> .record <$> pure {
+            nameIndex := ⟨nameIndex, nameP⟩,
+            fieldsIndex := ⟨fieldsIndex, fieldsP⟩,
+            functionTemplates
+          }
         | q`StrataDDL.declareTVar => do
           let #[.catbvar nameIndex] := attr.args
             | newBindingErr "declareTVar expects 1 argument."; return none
@@ -1758,6 +1794,9 @@ partial def resolveBindingIndices { argDecls : ArgDecls } (m : DialectMap) (src
             | a => panic! s!"Expected ident for type param {repr a}"
         foldOverArgAtLevel m addBinding #[] argDecls args b.typeParamsIndex.toLevel
     some <| .type params.toList none
+  | .record _ =>
+    -- Records have no type params; constructor/selectors are handled in addRecordBindings.
+    some <| .type [] none
   | .tvar _ =>
     -- tvar bindings are local only, not added to GlobalContext
     none
@@ -1805,7 +1844,7 @@ private def getConstructorListPushAnnotation (opDecl : OpDecl) : Option (Nat ×
 The accumulator is `Except String ...` because `foldOverArgBindingSpecs` fixes the
 fold's accumulator type; wrapping in `Except` lets us propagate errors through
 the fold without changing its generic signature. -/
-private def extractFieldsFromBindings (dialects : DialectMap) (arg : Arg)
+def extractFieldsFromBindings (dialects : DialectMap) (arg : Arg)
     : Except String (Array (String × TypeExpr)) :=
   -- We thread `Except` through the accumulator rather than changing
   -- `foldOverArgBindingSpecs`, which is used broadly with plain accumulators.
@@ -2139,6 +2178,35 @@ FreeVarIndex values are consistent with this order.
 this adds entries for: `Option` (type), `None` (constructor), `Some` (constructor),
 `Option..isNone` (tester), `Option..isSome` (tester).
 -/
+private def addRecordBindings
+    (dialects : DialectMap)
+    (gctx : GlobalContext)
+    (src : SourceRange)
+    (dialectName : DialectName)
+    (preRegistered : Bool)
+    {argDecls : ArgDecls}
+    (b : RecordBindingSpec argDecls)
+    (args : Vector Arg argDecls.size)
+    : Except String GlobalContext := do
+  let recordName :=
+    match args[b.nameIndex.toLevel] with
+    | .ident _ e => e
+    | a => panic! s!"Expected ident for record name {repr a}"
+  -- Step 1: Register the record type (no type parameters).
+  let k := GlobalKind.type [] none
+  let gctx ← gctx.defineChecked recordName k preRegistered
+  let recordIndex := gctx.findIndex? recordName |>.getD (gctx.vars.size - 1)
+  let recordType := mkDatatypeTypeRef src recordIndex #[]
+  -- Step 2: Extract fields from the CommaSepBy Binding argument and
+  -- synthesize a single constructor named `recordName ++ "_mk"`.
+  let fieldsArg := args[b.fieldsIndex.toLevel]
+  let fields ← extractFieldsFromBindings dialects fieldsArg
+  let ctorInfo : Array ConstructorInfo := #[{ name := recordName ++ "_mk", fields }]
+  -- Step 3: Expand function templates (field selectors etc.).
+  let (gctx, _) := expandFunctionTemplates dialectName src
+    recordName recordType ctorInfo b.functionTemplates gctx
+  return gctx
+
 private def addDatatypeBindings
     (dialects : DialectMap)
     (gctx : GlobalContext)
@@ -2190,7 +2258,7 @@ private def preRegisterType (dialects : DialectMap) (acc : Except String GlobalC
     {argDecls} (b : BindingSpec argDecls) (args : Vector Arg argDecls.size) : Except String GlobalContext := do
   let gctx ← acc
   match b with
-  | .datatype _ | .type _ =>
+  | .datatype _ | .record _ | .type _ =>
     let name :=
           match args[b.nameIndex.toLevel] with
           | .ident _ e => e
@@ -2212,6 +2280,8 @@ private def addBinding (dialects : DialectMap) (dialectName : DialectName) (preR
   match b with
   | .datatype datatypeSpec =>
     addDatatypeBindings dialects gctx l dialectName preRegistered datatypeSpec args
+  | .record recordSpec =>
+    addRecordBindings dialects gctx l dialectName preRegistered recordSpec args
   | _ =>
     let name : Var :=
           match args[b.nameIndex.toLevel] with

Strata/DDM/Elab/Core.lean

@@ -942,6 +942,33 @@ def evalBindingSpec
     | .error e =>
       logError loc e
       pure <| .empty gctx
+  | .record b =>
+    let nameInfo := args[b.nameIndex.toLevel].info
+    let (_, ident) ←
+        match nameInfo with
+        | .ofIdentInfo i =>
+          pure (i.loc, i.val)
+        | _ =>
+          logInternalError nameInfo.loc s!"Expected ident"
+          return tctx
+    assert! tctx.bindings.size = 0
+    let gctx := tctx.globalContext
+    let gctx := gctx.ensureDefined ident (.type [] none)
+    let dialects := (← read).dialects
+    let fieldsArg := args[b.fieldsIndex.toLevel]
+    match extractFieldsFromBindings dialects fieldsArg.arg with
+    | .ok fields =>
+      let recordIndex := gctx.findIndex? ident |>.getD (gctx.vars.size - 1)
+      let recordType := mkDatatypeTypeRef loc recordIndex #[]
+      let ctorInfo : Array ConstructorInfo := #[{ name := ident ++ "_mk", fields }]
+      let (gctx, errors) := gctx.expandFunctionTemplates
+        dialectName loc ident recordType ctorInfo
+        b.functionTemplates
+      errors.forM (logError loc)
+      pure <| .empty gctx
+    | .error e =>
+      logError loc e
+      pure <| .empty gctx
   | .tvar b =>
     let ident := evalBindingNameIndex args b.nameIndex
     pure <| tctx.push { ident, kind := .tvar loc ident }
@@ -1666,7 +1693,29 @@ partial def elabExpr (tctx : TypingContext) (stx : Syntax) : ElabM Tree := do
     let einfo : ElabInfo := { loc := loc, inputCtx := tctx }
     let name := elabIdent stx[0]
     let some binding := tctx.lookupVar name
-      | logError loc s!"Unknown expr identifier {name}"
+      | -- Desugar dot notation: "base.field" → T..field(base)
+        -- A single dot (not "..") separates the variable from the field name.
+        let dotParts := name.splitOn ".."
+        let parts := name.splitOn "."
+        if parts.length == 2 && dotParts.length == 1 then
+          let baseName := parts[0]!
+          let fieldName := parts[1]!
+          if let some baseBinding := tctx.lookupVar baseName then
+            let typeExprOpt : Option TypeExpr := match baseBinding with
+              | .bvar _ (.expr tp) => some tp
+              | .fvar _ (.expr tp) => some tp
+              | _ => none
+            if let some (.fvar _ typeIdx _) := typeExprOpt then
+              if let some typeName := tctx.globalContext.nameOf? typeIdx then
+                let selectorName := typeName ++ ".." ++ fieldName
+                if let some selectorIdx := tctx.globalContext.findIndex? selectorName then
+                  let baseExpr : Expr := match baseBinding with
+                    | .bvar idx _ => .bvar loc idx
+                    | .fvar idx _ => .fvar loc idx
+                  let appExpr : Expr := .app loc (.fvar loc selectorIdx) (.expr baseExpr)
+                  let info : ExprInfo := { toElabInfo := einfo, expr := appExpr }
+                  return .node (.ofExprInfo info) #[]
+        logError loc s!"Unknown expr identifier {name}"
         return default
     match binding with
     | .bvar idx k => do

Strata/DDM/Integration/Lean/ToExpr.lean

@@ -399,6 +399,17 @@ protected def toExpr {argDecls} (b : DatatypeBindingSpec argDecls) (argDeclsExpr
 
 end DatatypeBindingSpec
 
+namespace RecordBindingSpec
+
+protected def toExpr {argDecls} (b : RecordBindingSpec argDecls) (argDeclsExpr : Lean.Expr) : Lean.Expr :=
+  astExpr! mk
+    argDeclsExpr
+    (toExpr b.nameIndex)
+    (toExpr b.fieldsIndex)
+    (toExpr b.functionTemplates)
+
+end RecordBindingSpec
+
 namespace TvarBindingSpec
 
 protected def toExpr {argDecls} (b : TvarBindingSpec argDecls) (argDeclsExpr : Lean.Expr) : Lean.Expr :=
@@ -423,6 +434,7 @@ private def toExpr {argDecls} (bi : BindingSpec argDecls) (argDeclsExpr : Lean.E
   | .type b => astExpr! type argDeclsExpr (b.toExpr argDeclsExpr)
   | .scopedType b => astExpr! scopedType argDeclsExpr (b.toExpr argDeclsExpr)
   | .datatype b => astExpr! datatype argDeclsExpr (b.toExpr argDeclsExpr)
+  | .record b => astExpr! record argDeclsExpr (b.toExpr argDeclsExpr)
   | .tvar b => astExpr! tvar argDeclsExpr (b.toExpr argDeclsExpr)
 
 end BindingSpec

Strata/Languages/Boole/Grammar.lean

@@ -89,6 +89,15 @@ op for_down_to_by_statement (v : MonoBind, init : Expr, limit : Expr,
   @[scope(v)] body : Block) : Statement =>
   "for " v " := " init " downto " limit step invs body;
 
+// Record/struct type declaration: `type T := { f1: A, f2: B };`
+// Desugars to a single-constructor datatype `T_mk(f1: A, f2: B)` with
+// field selectors `T..f1(val)`, `T..f2(val)` etc.
+@[declareRecord(name, fields,
+    perField([.datatype, .literal "..", .field], [.datatype], .fieldType),
+    perField([.datatype, .literal "..", .field, .literal "!"], [.datatype], .fieldType))]
+op struct_decl (name : Ident, fields : CommaSepBy Binding) : Command =>
+  "type " name " := " "{" fields "}" ";\n";
+
 category Program;
 op prog (commands : SpacePrefixSepBy Command) : Program =>
   commands;

Strata/Languages/Boole/Verify.lean

@@ -233,18 +233,6 @@ private def toCoreMonoBind (b : BooleDDM.MonoBind SourceRange) : TranslateM (Cor
   match b with
   | .mono_bind_mk _ ⟨_, n⟩ ty => return (mkIdent n, ← toCoreMonoType ty)
 
-def toCoreTypedUn (m : SourceRange) (ty : Boole.Type) (op : String) (a : Core.Expression.Expr) : TranslateM Core.Expression.Expr := do
-  let .int _ := ty
-    | throwAt m s!"Unsupported typed operator type: {repr ty}"
-  let iop : Core.Expression.Expr := .op () ⟨s!"Int.{op}", ()⟩ none
-  return .app () iop a
-
-def toCoreTypedBin (m : SourceRange) (ty : Boole.Type) (op : String) (a b : Core.Expression.Expr) : TranslateM Core.Expression.Expr := do
-  let .int _ := ty
-    | throwAt m s!"Unsupported typed operator type: {repr ty}"
-  let iop : Core.Expression.Expr := .op () ⟨s!"Int.{op}", ()⟩ none
-  return mkCoreApp iop [a, b]
-
 private def bvWidth (m : SourceRange) (ty : Boole.Type) : TranslateM Nat :=
   match ty with
   | .bv1 _  => return 1
@@ -262,6 +250,20 @@ private def toCoreBvBin (m : SourceRange) (ty : Boole.Type) (op : String) (a b :
   let n ← bvWidth m ty
   return mkCoreApp (.op () ⟨s!"Bv{n}.{op}", ()⟩ none) [a, b]
 
+def toCoreTypedUn (m : SourceRange) (ty : Boole.Type) (op : String) (a : Core.Expression.Expr) : TranslateM Core.Expression.Expr := do
+  match ty with
+  | .int _ =>
+    let iop : Core.Expression.Expr := .op () ⟨s!"Int.{op}", ()⟩ none
+    return .app () iop a
+  | _ => toCoreBvUn m ty op a
+
+def toCoreTypedBin (m : SourceRange) (ty : Boole.Type) (op : String) (a b : Core.Expression.Expr) : TranslateM Core.Expression.Expr := do
+  match ty with
+  | .int _ =>
+    let iop : Core.Expression.Expr := .op () ⟨s!"Int.{op}", ()⟩ none
+    return mkCoreApp iop [a, b]
+  | _ => toCoreBvBin m ty op a b
+
 private def toCoreExtensionalEq
     (m : SourceRange)
     (ty : Boole.Type)
@@ -373,9 +375,21 @@ def toCoreExpr (e : Boole.Expr) : TranslateM Core.Expression.Expr := do
   | .bvand  m ty a b => toCoreBvBin m ty "And"  (← toCoreExpr a) (← toCoreExpr b)
   | .bvor   m ty a b => toCoreBvBin m ty "Or"   (← toCoreExpr a) (← toCoreExpr b)
   | .bvxor  m ty a b => toCoreBvBin m ty "Xor"  (← toCoreExpr a) (← toCoreExpr b)
-  | .bvshl  m ty a b => toCoreBvBin m ty "Shl"  (← toCoreExpr a) (← toCoreExpr b)
+  | .bvshl  m ty a b =>
+      match ty with
+      | .int _ => do
+          -- Integer << n encoded as multiplication by 2^n; n must be a literal.
+          let n ← match b with
+            | .natToInt _ ⟨_, n⟩ => pure n
+            | _ => throwAt m "Integer << requires a constant (literal) shift amount"
+          toCoreTypedBin m ty "Mul" (← toCoreExpr a) (.intConst () (Int.ofNat (1 <<< n)))
+      | _ => toCoreBvBin m ty "Shl" (← toCoreExpr a) (← toCoreExpr b)
   | .bvushr m ty a b => toCoreBvBin m ty "UShr" (← toCoreExpr a) (← toCoreExpr b)
   | .bvsshr m ty a b => toCoreBvBin m ty "SShr" (← toCoreExpr a) (← toCoreExpr b)
+  | .bvult  m ty a b => toCoreBvBin m ty "ULt"  (← toCoreExpr a) (← toCoreExpr b)
+  | .bvule  m ty a b => toCoreBvBin m ty "ULe"  (← toCoreExpr a) (← toCoreExpr b)
+  | .bvugt  m ty a b => toCoreBvBin m ty "UGt"  (← toCoreExpr a) (← toCoreExpr b)
+  | .bvuge  m ty a b => toCoreBvBin m ty "UGe"  (← toCoreExpr a) (← toCoreExpr b)
   | .old _ _ a =>
       return oldifyExpr (← get).currentInoutNames (← toCoreExpr a)
   | _ => throw (.fromMessage s!"Unsupported expression: {repr e}")
@@ -747,6 +761,7 @@ private def registerCommandSymbols (cmd : BooleDDM.Command SourceRange) : List B
   -- Procedure names are referenced by call statements directly and are not Expr.fvar symbols.
   | .boole_procedure _ _ _ _ _ _ _ | .command_procedure _ _ _ _ _ _ => []
   | .command_datatypes _ ⟨_, decls⟩ => decls.toList.map (fun _ => false)
+  | .struct_decl _ _ _ => [false]
   | .command_block _ _ => []
   | .command_axiom _ _ _ => []
   | .command_distinct _ _ _ => []
@@ -886,6 +901,20 @@ def toCoreDecls (cmd : BooleDDM.Command SourceRange) : TranslateM (List Core.Dec
     } .empty]
   | .command_datatypes _ ⟨_, decls⟩ =>
     return [.type (.data (← decls.toList.mapM toCoreDatatypeDecl)) .empty]
+  | .struct_decl m ⟨_, tname⟩ ⟨_, fields⟩ =>
+    -- Desugar `type T := { f1: A, f2: B }` to a single-constructor datatype.
+    -- DDM registration (type + selectors) is handled by @[declareRecord].
+    let args ← fields.toList.mapM toCoreBinding
+    let ctorName := tname ++ "_mk"
+    let constr : Lambda.LConstr Unit := {
+      name := mkIdent ctorName
+      args := args
+      testerName := s!"{tname}..is{ctorName}"
+    }
+    return [.type (.data [{ name := tname
+                            typeArgs := []
+                            constrs := [constr]
+                            constrs_ne := by simp }]) .empty]
 
 /-- Render a `Boole.Program` to a format object using the provided `GlobalContext` and
 `DialectMap`. These should come from the originating `Strata.Program` (i.e. `env.globalContext`

Strata/Languages/Core/DDMTransform/Grammar.lean

@@ -39,6 +39,12 @@ constructors : Ident, testerTemplate : FunctionTemplate,
 accessorTemplate : FunctionTemplate,
 unsafeAccessorTemplate : FunctionTemplate);
 
+// Declare metadata for single-constructor record types (field list variant).
+// Unlike declareDatatype, the constructor is synthesized as `name ++ "_mk"`.
+metadata declareRecord (name : Ident, fields : Ident,
+accessorTemplate : FunctionTemplate,
+unsafeAccessorTemplate : FunctionTemplate);
+
 type bool;
 type int;
 type string;
@@ -187,6 +193,10 @@ fn bvslt (tp : Type, a : tp, b : tp) : bool => @[prec(20), leftassoc] a " <s " b
 fn bvsle (tp : Type, a : tp, b : tp) : bool => @[prec(20), leftassoc] a " <=s " b;
 fn bvsgt (tp : Type, a : tp, b : tp) : bool => @[prec(20), leftassoc] a " >s " b;
 fn bvsge (tp : Type, a : tp, b : tp) : bool => @[prec(20), leftassoc] a " >=s " b;
+fn bvult (tp : Type, a : tp, b : tp) : bool => @[prec(20), leftassoc] a " <u " b;
+fn bvule (tp : Type, a : tp, b : tp) : bool => @[prec(20), leftassoc] a " <=u " b;
+fn bvugt (tp : Type, a : tp, b : tp) : bool => @[prec(20), leftassoc] a " >u " b;
+fn bvuge (tp : Type, a : tp, b : tp) : bool => @[prec(20), leftassoc] a " >=u " b;
 
 fn bvconcat8 (a : bv8, b : bv8) : bv16 => "bvconcat{8}{8}" "(" a ", " b ")";
 fn bvconcat16 (a : bv16, b : bv16) : bv32 => "bvconcat{16}{16}" "(" a ", " b ")";