diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 35202f6b57..2ca0bb1847 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -91,10 +91,6 @@ jobs: StrataDDM/.lake StrataBoole/.lake StrataPython/.lake - - name: Verify Java testdata is up to date - run: | - StrataTestExtra/Languages/Java/regenerate-testdata.sh - git diff --exit-code StrataTestExtra/Languages/Java/testdata/ - name: Build and run strata verify run: lake exe strata verify ../Examples/SimpleProc.core.st working-directory: StrataCLI diff --git a/Scripts/JavaGenTestData.lean b/Scripts/JavaGenTestData.lean deleted file mode 100644 index 00a2e890dc..0000000000 --- a/Scripts/JavaGenTestData.lean +++ /dev/null @@ -1,79 +0,0 @@ -/- - Copyright Strata Contributors - - SPDX-License-Identifier: Apache-2.0 OR MIT --/ -import StrataDDM - -/-! -# Java test data generation helper - -Usage: - lake env lean --run Scripts/JavaGenTestData.lean javaGen - lake env lean --run Scripts/JavaGenTestData.lean print --include - -Note: Unlike the former CLI `javaGen` command, this script only loads dialects -from files — it does not support referencing preloaded dialect names directly. -This is sufficient for the testdata regeneration workflow. --/ - -open StrataDDM - -def javaGen (dialectPath packageName outputDir : String) : IO Unit := do - let fm ← mkDialectFileMap - let d ← readStrataDialectFile fm dialectPath - match StrataDDM.Java.generateDialect d packageName with - | .ok files => - StrataDDM.Java.writeJavaFiles outputDir packageName files - IO.println s!"Generated Java files for {d.name} in {outputDir}/{StrataDDM.Java.packageToPath packageName}" - | .error msg => - IO.eprintln s!"Error generating Java: {msg}" - IO.Process.exit 1 - -def printFile (includeDirs : List String) (file : String) : IO Unit := do - let fm ← mkDialectFileMap - let mut fm := fm - for dir in includeDirs do - match ← fm.addSearchPath dir |>.toBaseIO with - | .error msg => - IO.eprintln msg - IO.Process.exit 1 - | .ok fm' => fm := fm' - let ld ← fm.getLoaded - if mem : file ∈ ld.dialects then - IO.print <| ld.dialects.format file mem - return - match ← readStrataFile fm file with - | .dialect d => - let ld ← fm.getLoaded - if mem : d.name ∈ ld.dialects then - IO.print <| ld.dialects.format d.name mem - else - IO.eprintln "Internal error reading file." - IO.Process.exit 1 - | .program pgm => - IO.print <| toString pgm - -private def parseIncludeArgs (args : List String) : List String × List String := - go args [] -where - go : List String → List String → List String × List String - | "--include" :: dir :: rest, includes => go rest (dir :: includes) - | other, includes => (includes.reverse, other) - -def main (args : List String) : IO Unit := do - match args with - | "javaGen" :: dialectPath :: packageName :: outputDir :: _ => - javaGen dialectPath packageName outputDir - | "print" :: rest => - let (includeDirs, fileArgs) := parseIncludeArgs rest - match fileArgs with - | [file] => printFile includeDirs file - | _ => - IO.eprintln "Usage: ... print [--include ]... " - IO.Process.exit 1 - | _ => - IO.eprintln "Usage:" - IO.eprintln " lake env lean --run Scripts/JavaGenTestData.lean javaGen " - IO.eprintln " lake env lean --run Scripts/JavaGenTestData.lean print [--include ]... " - IO.Process.exit 1 diff --git a/Scripts/LaurelJavaGen.lean b/Scripts/LaurelJavaGen.lean new file mode 100644 index 0000000000..69e4d53131 --- /dev/null +++ b/Scripts/LaurelJavaGen.lean @@ -0,0 +1,36 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +import StrataDDM.Integration.Java.Gen +import Strata.Languages.Laurel.LaurelAST + +/-! +# Laurel Java AST Generator + +Generates Java source files for the Laurel AST types using `getIonSerializer%`. +The generated Java matches the Ion encoding format used by `getIonDeserializer%`. + +Usage: + lake exe laurelJavaGen + +Example: + lake exe laurelJavaGen org.strata.jverify.laurel ../jverify/verifier/src/main/java +-/ + +open Strata.Java + +/-- Pre-computed Java files for the Laurel `Program` type. -/ +private def laurelFiles : GeneratedFiles := getIonSerializer% Strata.Laurel.Program "___placeholder___" + +def main (args : List String) : IO Unit := do + match args with + | [package, outputDir] => + let files := laurelFiles.files.map fun (name, content) => + (name, content.replace "package ___placeholder___;" s!"package {package};") + writeJavaFiles outputDir package { files } + IO.println s!"Generated {files.size} Java files in {outputDir}" + | _ => + IO.eprintln "Usage: lake exe laurelJavaGen " + IO.Process.exit 1 diff --git a/Strata.lean b/Strata.lean index 5457e4d54a..f407171d6d 100644 --- a/Strata.lean +++ b/Strata.lean @@ -17,6 +17,7 @@ import Strata.DL.Lambda import Strata.DL.Imperative /- Utilities -/ +import Strata.Util.IonDeserializer import Strata.Util.NameProofs import Strata.Util.Sarif diff --git a/Strata/Languages/Laurel.lean b/Strata/Languages/Laurel.lean index f223ac14d0..78a2f73fda 100644 --- a/Strata/Languages/Laurel.lean +++ b/Strata/Languages/Laurel.lean @@ -12,6 +12,7 @@ import Strata.Languages.Laurel.Grammar.ConcreteToAbstractTreeTranslator import Strata.Languages.Laurel.Grammar.AbstractToConcreteTreeTranslator import Strata.Languages.Laurel.Grammar.LaurelGrammar import StrataDDM.Elab +import Strata.Util.IonDeserializer /-! ## Strata Laurel API @@ -22,6 +23,11 @@ public section namespace Strata +/-- Deserializer for the new struct-format Ion encoding of `Laurel.Program`, +generated by `getIonSerializer%`. -/ +private partial def deserializeLaurelProgram : ByteArray → Except Std.Format Laurel.Program := + getIonDeserializer% Laurel.Program + /-! ### File I/O -/ /-- @@ -64,9 +70,17 @@ def readLaurelIonFiles (bytes : ByteArray) /-- Deserialize Laurel Ion bytes and parse all files into a single combined `Laurel.Program`. + +Supports both the new struct-format (from `getIonSerializer%`) and the +legacy DDM-based format. Tries the new format first, falls back to DDM. -/ def readLaurelIonProgram (bytes : ByteArray) : IO Laurel.Program := do + -- Try new struct-format deserialization first + match deserializeLaurelProgram bytes with + | .ok program => return program + | .error _ => pure () + -- Fall back to legacy DDM path let files ← readLaurelIonFiles bytes let mut combined : Laurel.Program := { staticProcedures := [] diff --git a/Strata/Util/IonDeserializer.lean b/Strata/Util/IonDeserializer.lean new file mode 100644 index 0000000000..f820e99cec --- /dev/null +++ b/Strata/Util/IonDeserializer.lean @@ -0,0 +1,495 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +module + +public meta import Lean.Elab.Term.TermElabM +public import StrataDDM.Util.Ion +public import StrataDDM.Util.Decimal + +open Lean Meta Elab Term +open Ion + +/-! +# Generic Ion Deserializer + +`getIonDeserializer%` is a term-level elaborator that, at compile time, +inspects a Lean inductive or structure type and generates a function +`ByteArray → Except Std.Format α` that deserializes Ion binary data into +values of that type. + +## Ion encoding conventions + +- **Structures** are encoded as Ion structs whose keys match the Lean field + names. +- **Single-constructor inductives** are encoded as Ion structs with positional + field names `_0`, `_1`, … +- **Multi-constructor inductives** are encoded as Ion s-expressions + `(ConstructorName arg₁ arg₂ …)`. +- **Supported leaf types**: `Nat`, `Int`, `String`, `Bool`, `Float`, `Decimal`. +- **Container types**: `List α`, `Option α`. +- **Nested/recursive types** are supported. Recursive types require the + enclosing definition to be marked `partial`. + +## Usage + +```lean +def myDeserializer : ByteArray → Except Std.Format MyType := + getIonDeserializer% MyType +``` +-/ + +public section + +namespace Strata.Util.IonDeserializer + +def readNat (v : Ion SymbolId) : Except Std.Format Nat := + match v.app with + | .int i => if i ≥ 0 then .ok i.toNat else .error f!"Expected non-negative int, got {repr v}" + | _ => .error f!"Expected int for Nat, got {repr v}" + +def readInt (v : Ion SymbolId) : Except Std.Format Int := + match v.app with + | .int i => .ok i + | _ => .error f!"Expected int, got {repr v}" + +def readString (v : Ion SymbolId) (tbl : SymbolTable) : Except Std.Format String := + match v.app with + | .string s => .ok s + | .symbol sym => match tbl[sym]? with + | some s => .ok s + | none => .error f!"Unknown symbol id {sym.value}" + | _ => .error f!"Expected string, got {repr v}" + +def readBool (v : Ion SymbolId) : Except Std.Format Bool := + match v.app with + | .bool b => .ok b + | _ => .error f!"Expected bool, got {repr v}" + +def readFloat (v : Ion SymbolId) : Except Std.Format Float := + match v.app with + | .float f => .ok f + | .int i => .ok (Float.ofInt i) + | _ => .error f!"Expected float, got {repr v}" + +def readDecimal (v : Ion SymbolId) : Except Std.Format StrataDDM.Decimal := + match v.app with + | .decimal d => .ok d + | .int i => .ok (StrataDDM.Decimal.ofInt i) + | _ => .error f!"Expected decimal, got {repr v}" + +def readList (readElem : Ion SymbolId → SymbolTable → Except Std.Format α) + (v : Ion SymbolId) (tbl : SymbolTable) : Except Std.Format (List α) := do + let elems ← match v.app with + | .list a => .ok a + | .sexp a => .ok a + | _ => .error f!"Expected list, got {repr v}" + let mut result : List α := [] + for elem in elems.reverse do + result := (← readElem elem tbl) :: result + .ok result + +def readOption (readElem : Ion SymbolId → SymbolTable → Except Std.Format α) + (v : Ion SymbolId) (tbl : SymbolTable) : Except Std.Format (Option α) := + match v.app with + | .null _ => .ok none + | _ => (readElem v tbl).map some + +def resolveSymbol (tbl : SymbolTable) (sym : SymbolId) : Except Std.Format String := + match tbl[sym]? with + | some s => .ok s + | none => .error f!"Unknown symbol id {sym.value}" + +def lookupField (tbl : SymbolTable) (fields : Array (SymbolId × Ion SymbolId)) + (name : String) : Except Std.Format (Ion SymbolId) := do + for (sym, val) in fields do + match tbl[sym]? with + | some s => if s == name then return val + | none => pure () + .error f!"Missing field '{name}'" + +def asStruct (v : Ion SymbolId) : Except Std.Format (Array (SymbolId × Ion SymbolId)) := + match v.app with + | .struct fields => .ok fields + | _ => .error f!"Expected struct, got {repr v}" + +def asSexp (v : Ion SymbolId) : Except Std.Format (Array (Ion SymbolId)) := + match v.app with + | .sexp args => .ok args + | .list args => .ok args + | _ => .error f!"Expected sexp, got {repr v}" + +def deserializeWith {α : Type} (f : Ion SymbolId → SymbolTable → Except Std.Format α) + (bs : ByteArray) : Except Std.Format α := do + let entries ← match Ion.deserialize bs with + | .error (off, msg) => .error f!"Ion parse error at offset {off}: {msg}" + | .ok a => .ok a + if h : entries.size = 1 then + let entry := entries[0] + if h2 : entry.size = 2 then + let tbl ← match SymbolTable.ofLocalSymbolTable entry[0] with + | .error (_, msg) => .error f!"Symbol table error: {msg}" + | .ok tbl => .ok tbl + f entry[1] tbl + else + .error f!"Expected symbol table and value, got {entry.size} elements" + else + .error f!"Expected single Ion top-level value, got {entries.size}" + +end Strata.Util.IonDeserializer +end -- public section + +/-- Leaf type names that should not be treated as nested inductives. -/ +private meta def isLeafTypeName (name : Name) : Bool := + name == ``Nat || name == ``Int || name == ``String || name == ``Bool || name == ``Float || + name == ``StrataDDM.Decimal + +/-- Check if a type name refers to a non-leaf inductive or structure in the environment. -/ +private meta def isCompoundType (env : Environment) (name : Name) : Bool := + !isLeafTypeName name && + ((getStructureInfo? env name).isSome || + match env.find? name with | some (.inductInfo _) => true | _ => false) + +/-- Canonical string key for a fully-applied type expression: "Name arg1 arg2 ...". -/ +private meta partial def typeKey (t : Expr) : String := + let fn := t.getAppFn + let args := t.getAppArgs + let base := match fn.constName? with + | some n => n.toString (escape := false) + | none => "?" + if args.isEmpty then base + else s!"{base}[{",".intercalate (args.toList.map typeKey)}]" + +/-- Generate a unique reader function name for a fully-applied type. -/ +private meta def readerNameExpr (t : Expr) : Name := + Name.mkSimple s!"_ionRead_{(typeKey t).hash}" + +/-- Legacy: reader name from a bare Name (no type args). -/ +private meta def readerName (typeName : Name) : Name := + readerNameExpr (mkConst typeName) + +/-- +Generate a read expression for a value of the given type. +`valExpr` is the syntax for the Ion value to read. +Returns syntax of type `Except Std.Format T`. +-/ +private meta partial def mkValueRead (fieldType : Expr) (valExpr : TSyntax `term) : + TermElabM (TSyntax `term) := do + let fieldType' ← whnf fieldType + let name := fieldType'.getAppFn.constName? + match name with + | some ``Nat => `(Strata.Util.IonDeserializer.readNat $valExpr) + | some ``Int => `(Strata.Util.IonDeserializer.readInt $valExpr) + | some ``String => `(Strata.Util.IonDeserializer.readString $valExpr tbl) + | some ``Bool => `(Strata.Util.IonDeserializer.readBool $valExpr) + | some ``Float => `(Strata.Util.IonDeserializer.readFloat $valExpr) + | some ``StrataDDM.Decimal => `(Strata.Util.IonDeserializer.readDecimal $valExpr) + | some ``List => + let args := fieldType'.getAppArgs + if h : args.size > 0 then + let elemType := args[0] + let elemReader ← mkValueRead elemType (← `(_elemVal)) + `(Strata.Util.IonDeserializer.readList (fun _elemVal tbl => $elemReader) $valExpr tbl) + else throwError "getIonDeserializer%: List without type argument" + | some ``Option => + let args := fieldType'.getAppArgs + if h : args.size > 0 then + let elemType := args[0] + let elemReader ← mkValueRead elemType (← `(_elemVal)) + `(Strata.Util.IonDeserializer.readOption (fun _elemVal tbl => $elemReader) $valExpr tbl) + else throwError "getIonDeserializer%: Option without type argument" + | some n => + if isCompoundType (← getEnv) n then + let readerId := mkIdent (readerNameExpr fieldType') + `($readerId $valExpr tbl) + else + throwError "getIonDeserializer%: unsupported field type {fieldType'}" + | _ => throwError "getIonDeserializer%: unsupported field type {fieldType'}" + +/-- +Generate a read expression for a field accessed via `lookupField` (struct context). +Supports leaf types and nested inductive/structure types. +-/ +private meta def mkFieldRead (fieldType : Expr) (fieldNameLit : TSyntax `str) : + TermElabM (TSyntax `term) := do + let valExpr ← `(_fv) + let readExpr ← mkValueRead fieldType valExpr + `(Strata.Util.IonDeserializer.lookupField tbl fields $fieldNameLit >>= (fun _fv => $readExpr)) + +/-- +Generate a read expression for a field accessed by index (sexp context). +Supports leaf types and nested inductive/structure types. +-/ +private meta def mkIndexRead (fieldType : Expr) (idx : Nat) : + TermElabM (TSyntax `term) := do + let idxLit := quote idx + let valExpr ← `(_iv) + let readExpr ← mkValueRead fieldType valExpr + `(if h : $(idxLit) < args.size + then (fun _iv => $readExpr) args[$(idxLit)] + else .error f!"Missing argument at index {$(idxLit)}") + +private meta def getCtorFieldTypes (env : Environment) (ctorName : Name) + (typeArgs : Array Expr := #[]) : TermElabM (Nat × Nat × Array Expr) := do + let some (.ctorInfo ci) := env.find? ctorName + | throwError "getIonDeserializer%: cannot find constructor {ctorName}" + let mut ty := ci.type + for i in List.range ci.numParams do + match ty with + | .forallE _ _ b _ => + let sub := if h : i < typeArgs.size then typeArgs[i] else mkSort levelZero + ty := b.instantiate1 sub + | _ => throwError "getIonDeserializer%: unexpected type shape" + let mut result := #[] + for _ in List.range ci.numFields do + match ty with + | .forallE _ t b _ => + result := result.push t + ty := b.instantiate1 (mkSort levelZero) + | _ => throwError "getIonDeserializer%: unexpected type shape" + return (ci.numParams, ci.numFields, result) + +/-- Generate the body of a reader for a struct type. -/ +private meta def mkStructReaderBody (sinfo : StructureInfo) (typeArgs : Array Expr := #[]) : + TermElabM (TSyntax `term) := do + let env ← getEnv + let fieldNames := sinfo.fieldNames + let ctorName := sinfo.structName ++ `mk + let (_, _, fieldTypes) ← getCtorFieldTypes env ctorName typeArgs + let ctorId := mkIdent ctorName + let mut ctorArgs : Array (TSyntax `term) := #[] + for fieldName in fieldNames do + ctorArgs := ctorArgs.push (← `($(mkIdent fieldName))) + let mut body : TSyntax `term ← `(Except.ok ($ctorId $ctorArgs*)) + for i in (List.range fieldNames.size).reverse do + let fieldName := fieldNames[i]! + let fieldStr := fieldName.toString (escape := false) + let fieldLit := Syntax.mkStrLit fieldStr + let fieldType := fieldTypes[i]! + let localId := mkIdent fieldName + let readExpr ← mkFieldRead fieldType fieldLit + body ← `(Except.bind $readExpr (fun $localId => $body)) + `(Except.bind (Strata.Util.IonDeserializer.asStruct v) (fun fields => $body)) + +/-- Generate the body of a reader for a single-constructor inductive. -/ +private meta def mkSingleCtorReaderBody (ctorName : Name) (typeArgs : Array Expr := #[]) : + TermElabM (TSyntax `term) := do + let (_, numFields, fieldTypes) ← getCtorFieldTypes (← getEnv) ctorName typeArgs + let ctorId := mkIdent ctorName + let mut ctorArgs : Array (TSyntax `term) := #[] + for i in List.range numFields do + ctorArgs := ctorArgs.push (← `($(mkIdent (Name.mkSimple s!"_f{i}")))) + let mut body : TSyntax `term ← `(Except.ok ($ctorId $ctorArgs*)) + for i in (List.range numFields).reverse do + let fieldLit := Syntax.mkStrLit s!"_{i}" + let localId := mkIdent (Name.mkSimple s!"_f{i}") + let readExpr ← mkFieldRead fieldTypes[i]! fieldLit + body ← `(Except.bind $readExpr (fun $localId => $body)) + `(Except.bind (Strata.Util.IonDeserializer.asStruct v) (fun fields => $body)) + +/-- Generate the body of a reader for a multi-constructor inductive. -/ +private meta def mkMultiCtorReaderBody (typeName : Name) (ctors : List Name) + (typeArgs : Array Expr := #[]) : + TermElabM (TSyntax `term) := do + let env ← getEnv + let typeNameStr := typeName.toString + let mut body : TSyntax `term ← + `(Except.error (f!"Unknown constructor for {$(Syntax.mkStrLit typeNameStr)}" : Std.Format)) + for ctorName in ctors.reverse do + let shortName := ctorName.getString! + let ctorId := mkIdent ctorName + let (_, numFields, fieldTypes) ← getCtorFieldTypes env ctorName typeArgs + let mut ctorArgs : Array (TSyntax `term) := #[] + for i in List.range numFields do + ctorArgs := ctorArgs.push (← `($(mkIdent (Name.mkSimple s!"_a{i}")))) + let mut ctorBody : TSyntax `term ← `(Except.ok ($ctorId $ctorArgs*)) + for i in (List.range numFields).reverse do + let localId := mkIdent (Name.mkSimple s!"_a{i}") + let readExpr ← mkIndexRead fieldTypes[i]! (i + 1) + ctorBody ← `(Except.bind $readExpr (fun $localId => $ctorBody)) + let patLit := Syntax.mkStrLit shortName + body ← `(if tag == $patLit then $ctorBody else $body) + `(Except.bind (Strata.Util.IonDeserializer.asSexp v) (fun args => + if h : args.size < 1 then + Except.error (f!"Expected non-empty sexp" : Std.Format) + else + Except.bind + (match args[0].app with + | .symbol sym => Strata.Util.IonDeserializer.resolveSymbol tbl sym + | .string s => Except.ok s + | _ => Except.error (f!"Expected symbol or string tag" : Std.Format)) + (fun tag => $body))) + +/-- Generate the body of a reader function for a given (possibly applied) type. -/ +private meta def mkReaderBody (env : Environment) (typeExpr : Expr) : + TermElabM (TSyntax `term) := do + let typeName := typeExpr.getAppFn.constName?.getD Name.anonymous + let typeArgs := typeExpr.getAppArgs + if let some sinfo := getStructureInfo? env typeName then + mkStructReaderBody sinfo typeArgs + else + let some (.inductInfo indInfo) := env.find? typeName + | throwError "getIonDeserializer%: {typeName} is not an inductive or structure type" + if indInfo.ctors.length == 1 then + mkSingleCtorReaderBody indInfo.ctors.head! typeArgs + else + mkMultiCtorReaderBody typeName indInfo.ctors typeArgs + +/-- Extract fully-applied compound type expressions from a field type, looking through List/Option. -/ +private meta partial def extractCompoundExprs (env : Environment) (t : Expr) : TermElabM (Array Expr) := do + let t ← whnf t + let name := t.getAppFn.constName? + match name with + | some ``List | some ``Option => + let args := t.getAppArgs + if h : args.size > 0 then extractCompoundExprs env args[0] + else return #[] + | some n => + if isCompoundType env n then + -- Return the full applied type, and recurse into type arguments + let mut result := #[t] + for arg in t.getAppArgs do + result := result ++ (← extractCompoundExprs env arg) + return result + else return #[] + | none => return #[] + +/-- Collect all nested fully-applied type expressions reachable from a type's fields. -/ +private meta def collectNestedTypeExprs (env : Environment) (rootExpr : Expr) : + TermElabM (Array Expr) := do + let mut visited : Std.HashSet String := {} + let mut queue : Array Expr := #[rootExpr] + let mut result : Array Expr := #[] + while h : queue.size > 0 do + let typeExpr := queue[0] + queue := queue.extract 1 queue.size + let key := typeKey typeExpr + if visited.contains key then continue + visited := visited.insert key + result := result.push typeExpr + let typeName := typeExpr.getAppFn.constName?.getD Name.anonymous + let typeArgs := typeExpr.getAppArgs + let ctors := if let some sinfo := getStructureInfo? env typeName then + [sinfo.structName ++ `mk] + else match env.find? typeName with + | some (.inductInfo indInfo) => indInfo.ctors + | _ => [] + for ctorName in ctors do + let some (.ctorInfo ci) := env.find? ctorName | continue + let mut ty := ci.type + for i in List.range ci.numParams do + match ty with + | .forallE _ _ b _ => + let sub := if h2 : i < typeArgs.size then typeArgs[i] else mkSort levelZero + ty := b.instantiate1 sub + | _ => break + for _ in List.range ci.numFields do + match ty with + | .forallE _ t b _ => + for texpr in ← extractCompoundExprs env t do + let tkey := typeKey texpr + if !visited.contains tkey then queue := queue.push texpr + ty := b.instantiate1 (mkSort levelZero) + | _ => break + return result + +/-- Build a `let rec` term with multiple mutually-recursive bindings. -/ +private meta def mkMutualLetRec (bindings : Array (Ident × TSyntax `term × TSyntax `term)) + (innerBody : TSyntax `term) : TermElabM (TSyntax `term) := do + if bindings.isEmpty then return innerBody + let termSuffix := mkNode ``Lean.Parser.Termination.suffix #[mkNullNode, mkNullNode] + let mut declNodes : Array Syntax := #[] + for (fnName, type, body) in bindings do + let letIdDecl ← `(Lean.Parser.Term.letIdDecl| $fnName : $type := $body) + let letDecl := mkNode ``Lean.Parser.Term.letDecl #[letIdDecl] + let letRecDecl := mkNode ``Lean.Parser.Term.letRecDecl + #[mkNullNode, mkNullNode, letDecl, termSuffix] + declNodes := declNodes.push letRecDecl + -- Build comma-separated array: [decl0, ",", decl1, ",", decl2, ...] + let mut sepElems : Array Syntax := #[] + for i in List.range declNodes.size do + if i > 0 then sepElems := sepElems.push (mkAtom ",") + sepElems := sepElems.push declNodes[i]! + let sepArray := mkNullNode sepElems + let letRecDecls := mkNode ``Lean.Parser.Term.letRecDecls #[sepArray] + let letrec := mkNode ``Lean.Parser.Term.letrec + #[mkNullNode, letRecDecls, mkNullNode, innerBody] + return ⟨letrec⟩ + +/-- Convert a type Expr to syntax for use in type annotations. -/ +private meta partial def exprToTypeSyntax (e : Expr) : TermElabM (TSyntax `term) := do + let fn := e.getAppFn + let args := e.getAppArgs + if args.isEmpty then + if let some n := fn.constName? then + `($(mkIdent n)) + else + `(_) + else + let fnStx ← exprToTypeSyntax fn + let mut result := fnStx + for arg in args do + let argStx ← exprToTypeSyntax arg + result ← `($result $argStx) + return result + +public section + +/-- +`getIonDeserializer%` generates an Ion deserializer for the given type. +The result has type `ByteArray → Except Std.Format T`. + +Usage: `getIonDeserializer% MyType` +-/ +syntax (name := getIonDeserializerStx) "getIonDeserializer%" ident : term + +@[term_elab getIonDeserializerStx] +meta def getIonDeserializerElab : TermElab := fun stx _expectedType? => do + match stx with + | `(getIonDeserializer% $typeId) => do + let typeName ← resolveGlobalConstNoOverload typeId + let env ← getEnv + let rootExpr := Lean.mkConst typeName + let nestedTypes ← collectNestedTypeExprs env rootExpr + if nestedTypes.size <= 1 then + -- Simple case: no nested types, check for compound fields + let mut hasCompoundFields := false + let ctors := if let some sinfo := getStructureInfo? env typeName then + [sinfo.structName ++ `mk] + else match env.find? typeName with + | some (.inductInfo indInfo) => indInfo.ctors + | _ => [] + for ctorName in ctors do + if let some (.ctorInfo ci) := env.find? ctorName then + let mut ty := ci.type + for _ in List.range ci.numParams do + match ty with | .forallE _ _ b _ => ty := b.instantiate1 (mkSort levelZero) | _ => break + for _ in List.range ci.numFields do + match ty with + | .forallE _ t b _ => + if let some n := t.getAppFn.constName? then + if isCompoundType env n then hasCompoundFields := true + ty := b.instantiate1 (mkSort levelZero) + | _ => break + if !hasCompoundFields then + let readerBody ← mkReaderBody env rootExpr + let resultStx ← `(Strata.Util.IonDeserializer.deserializeWith (fun v tbl => $readerBody)) + return ← elabTerm resultStx _expectedType? + -- Nested/recursive types: generate a single mutual let rec block + let rootReaderId := mkIdent (readerNameExpr rootExpr) + let mut bindings : Array (Ident × TSyntax `term × TSyntax `term) := #[] + for typeExpr in nestedTypes do + let readerId := mkIdent (readerNameExpr typeExpr) + let body ← mkReaderBody env typeExpr + let typeStx ← exprToTypeSyntax typeExpr + let readerType ← `(Ion SymbolId → SymbolTable → Except Std.Format $typeStx) + let readerBody ← `(fun v tbl => $body) + bindings := bindings.push (readerId, readerType, readerBody) + let innerExpr ← `(Strata.Util.IonDeserializer.deserializeWith $rootReaderId) + let finalExpr ← mkMutualLetRec bindings innerExpr + elabTerm finalExpr _expectedType? + | _ => throwUnsupportedSyntax + +end diff --git a/StrataCLI/StrataMainLib.lean b/StrataCLI/StrataMainLib.lean index c7604c82b7..65731e58d5 100644 --- a/StrataCLI/StrataMainLib.lean +++ b/StrataCLI/StrataMainLib.lean @@ -9,7 +9,6 @@ import Lean.Parser.Extension import Strata.Cli.Framework import Strata.Cli.VerifyOptions import Strata.Backends.CBMC.GOTO.CoreToGOTOPipeline -import StrataDDM.Integration.Java.Gen import Strata.Languages.Core.Verifier import Strata.Languages.Core.SarifOutput import Strata.Languages.C_Simp.Verify @@ -148,27 +147,6 @@ def diffCommand : Command where exitFailure "Cannot compare dialect def with another dialect/program." -def javaGenCommand : Command where - name := "javaGen" - args := [ "dialect", "package", "output-dir" ] - flags := [includeFlag] - help := "Generate Java source files from a DDM dialect definition. Accepts a dialect name (e.g. Laurel) or a dialect file path." - callback := fun v pflags => do - let fm ← pflags.buildDialectFileMap - let ld ← fm.getLoaded - let d ← if mem : v[0] ∈ ld.dialects then - pure ld.dialects[v[0]] - else - match ← StrataDDM.readStrataFile fm v[0] with - | .dialect d => pure d - | .program _ => exitFailure "Expected a dialect file, not a program file." - match StrataDDM.Java.generateDialect d v[1] with - | .ok files => - StrataDDM.Java.writeJavaFiles v[2] v[1] files - IO.println s!"Generated Java files for {d.name} in {v[2]}/{StrataDDM.Java.packageToPath v[1]}" - | .error msg => - exitFailure s!"Error generating Java: {msg}" - def laurelAnalyzeBinaryCommand : Command where name := "laurelAnalyzeBinary" args := [] @@ -542,8 +520,6 @@ def commandGroups : List CommandGroup := [ { name := "Core" commands := [verifyCommand, transformCommand, checkCommand, toIonCommand, printCommand, diffCommand] commonFlags := [includeFlag] }, - { name := "Code Generation" - commands := [javaGenCommand] }, { name := "Python" commands := [StrataPython.Cli.pyAnalyzeLaurelCommand, StrataPython.Cli.pyResolveOverloadsCommand, diff --git a/StrataDDM/StrataDDM/Integration/Java/Gen.lean b/StrataDDM/StrataDDM/Integration/Java/Gen.lean index 7698781ddf..50f605dd70 100644 --- a/StrataDDM/StrataDDM/Integration/Java/Gen.lean +++ b/StrataDDM/StrataDDM/Integration/Java/Gen.lean @@ -5,32 +5,58 @@ -/ module -public import StrataDDM.AST -import StrataDDM.Ion -import StrataDDM.Integration.Categories +public meta import Lean.Elab.Term.TermElabM +public meta import Init.Data.String.Legacy +public import StrataDDM.Util.Decimal -namespace StrataDDM.Java +open Lean Meta Elab Term -open StrataDDM (Dialect OpDecl ArgDecl ArgDeclKind QualifiedIdent SyntaxCat) -open StrataDDM.Integration (primitiveCategories forbiddenCategories abstractCategories) +/-! +# Java Code Generator for Lean Types -/-! # Java Code Generator for DDM Dialects +`getIonSerializer%` is a term-level elaborator that inspects Lean inductive and +structure types at compile time and generates Java source code consisting of: -Generates Java source files from DDM dialect definitions: -- Sealed interfaces for categories, with operator records as nested types -- Non-sealed stub interfaces for abstract categories (e.g., Init.Expr) -- Generated `toIon` methods on each record for serialization -- Static factory methods for ergonomic AST construction -- Slim Ion serializer with helper methods (no reflection) +- A sealed interface hierarchy mirroring the Lean type +- Records for each constructor / structure +- Ion serialization methods using the same format as `getIonDeserializer%` -All names are disambiguated to avoid collisions with Java reserved words, -base classes (Node, SourceRange, IonSerializer), and each other. +## Ion encoding conventions (matching `getIonDeserializer%`) + +| Lean type | Ion encoding | +|-----------|-------------| +| Structures | Ion struct with field names as keys | +| Single-constructor inductives | Ion struct with positional keys `_0`, `_1`, … | +| Multi-constructor inductives | Ion sexp `(ConstructorName arg₁ arg₂ …)` | + +## Supported leaf types + +`Nat`, `Int`, `Float`, `String`, `Bool`, `Decimal` + +## Container types + +`List α` → `java.util.List`, `Option α` → nullable `T` -/ +namespace Strata.Java + +/-! ## All generated Java source files. -/ + +public structure GeneratedFiles where + files : Array (String × String) -- (filename, content) + deriving Inhabited + +public def writeJavaFiles (baseDir : System.FilePath) (package : String) + (files : GeneratedFiles) : IO Unit := do + let parts := package.splitOn "." + let dir := parts.foldl (init := baseDir) (· / ·) + IO.FS.createDirAll dir + for (filename, content) in files.files do + IO.FS.writeFile (dir / filename) content + /-! ## Name Utilities -/ -def javaReservedWords : Std.HashSet String := Std.HashSet.ofList [ - -- Reserved keywords +private meta def javaReservedWords : Std.HashSet String := Std.HashSet.ofList [ "abstract", "assert", "boolean", "break", "byte", "case", "catch", "char", "class", "const", "continue", "default", "do", "double", "else", "enum", "extends", "final", "finally", "float", "for", "goto", "if", "implements", @@ -38,25 +64,19 @@ def javaReservedWords : Std.HashSet String := Std.HashSet.ofList [ "package", "private", "protected", "public", "return", "short", "static", "strictfp", "super", "switch", "synchronized", "this", "throw", "throws", "transient", "try", "void", "volatile", "while", - -- Contextual keywords (restricted in some contexts) "exports", "module", "open", "opens", "permits", "provides", "record", "sealed", "to", "transitive", "uses", "var", "when", "with", "yield", - -- Literals (cannot be used as identifiers) - "true", "false", "null", - -- Underscore (Java 9+) - "_", - -- Common java.lang classes that would cause ambiguity - "String", "Object", "Integer", "Boolean", "Long", "Double", "Float", "Character", "Byte", "Short" + "true", "false", "null", "_", + "String", "Object", "Integer", "Boolean", "Long", "Double", "Float", + "Character", "Byte", "Short" ] -def escapeJavaName (name : String) : String := - -- Remove invalid characters (like ?) +private meta def escapeJavaName (name : String) : String := let cleaned := String.ofList (name.toList.filter (fun c => c.isAlphanum || c == '_')) let cleaned := if cleaned.isEmpty then "field" else cleaned - -- Add suffix if reserved word if javaReservedWords.contains cleaned then cleaned ++ "_" else cleaned -def toPascalCase (s : String) : String := +private meta def toPascalCase (s : String) : String := s.splitOn "_" |>.filter (!·.isEmpty) |>.map (fun part => match part.toList with @@ -64,388 +84,412 @@ def toPascalCase (s : String) : String := | c :: cs => .ofList (c.toUpper :: cs)) |> String.intercalate "" -/-- Generate unique name by adding suffix if collision detected -/ -partial def disambiguate (base : String) (usedNames : Std.HashSet String) : String × Std.HashSet String := - let rec findUnused (n : Nat) : String := - let suffix := if n == 0 then "" else if n == 1 then "_" else s!"_{n}" - let candidate := base ++ suffix - if usedNames.contains candidate.toLower then findUnused (n + 1) else candidate - let name := findUnused 0 - (name, usedNames.insert name.toLower) - -/-! ## Type Mapping -/ - -inductive JavaType where - | simple (name : String) (boxed : Option String := none) - | array (elem : JavaType) - | optional (elem : JavaType) - | list (elem : JavaType) - deriving Inhabited - -mutual -def JavaType.toJava : JavaType → String - | .simple name _ => name - | .array elem => elem.toJava ++ "[]" - | .optional elem => s!"java.util.Optional<{elem.toJavaBoxed}>" - | .list elem => s!"java.util.List<{elem.toJavaBoxed}>" - -def JavaType.toJavaBoxed : JavaType → String - | .simple _ (some boxed) => boxed - | t => t.toJava -end - -/-- Maps a primitive Init category to its Java type. -/ -def primitiveJavaType (qid : QualifiedIdent) : JavaType := - match qid with - | q`Init.Ident => .simple "java.lang.String" - | q`Init.Num => .simple "java.math.BigInteger" - | q`Init.Decimal => .simple "java.math.BigDecimal" - | q`Init.Str => .simple "java.lang.String" - | q`Init.ByteArray => .array (.simple "byte" (some "java.lang.Byte")) - | q`Init.Bool => .simple "boolean" (some "java.lang.Boolean") - | _ => panic! s!"Not a primitive category: {qid.dialect}.{qid.name}" - -/-- Maps an abstract Init category to its Java interface name. -/ -def abstractJavaName (qid : QualifiedIdent) : String := - match qid with - | q`Init.Expr => "Expr" - | q`Init.Type => "Type_" - | q`Init.TypeP => "TypeP" - | _ => panic! s!"Not an abstract category: {qid.dialect}.{qid.name}" - -partial def syntaxCatToJavaType (cat : SyntaxCat) : JavaType := - if forbiddenCategories.contains cat.name then - panic! s!"{cat.name.dialect}.{cat.name.name} is internal DDM machinery" - else if primitiveCategories.contains cat.name then - primitiveJavaType cat.name - else if abstractCategories.contains cat.name then - .simple (abstractJavaName cat.name) - else match cat.name with - | q`Init.Option => - match cat.args[0]? with - | some inner => .optional (syntaxCatToJavaType inner) - | none => panic! "Init.Option requires a type argument" - | _ => - if (SepFormat.fromCategoryName? cat.name).isSome then - match cat.args[0]? with - | some inner => .list (syntaxCatToJavaType inner) - | none => panic! "List category requires a type argument" - else match cat.name with - | ⟨"Init", _⟩ => panic! s!"Unknown Init category: {cat.name.name}" - | ⟨_, name⟩ => .simple (escapeJavaName (toPascalCase name)) - -def argDeclKindToJavaType : ArgDeclKind → JavaType - | .type _ => .simple "Expr" - | .cat c => syntaxCatToJavaType c - -/-- Extract the QualifiedIdent for categories that need Java interfaces, or none for primitives. -/ -partial def syntaxCatToQualifiedName (cat : SyntaxCat) : Option QualifiedIdent := - if primitiveCategories.contains cat.name then none - else if abstractCategories.contains cat.name then some cat.name - else if SepFormat.isParametricCategory cat.name then - cat.args[0]?.bind syntaxCatToQualifiedName - else match cat.name with - | ⟨"Init", _⟩ => none - | qid => some qid - -/-! ## Serialization Code Generation -/ - -/-- Maps a primitive Init category to its serializer method name, or none for non-primitives. -/ -def primitiveSerializerMethod (qid : QualifiedIdent) : Option String := - match qid with - | q`Init.Ident => some "serializeIdent" - | q`Init.Str => some "serializeStrlit" - | q`Init.Num => some "serializeNum" - | q`Init.Decimal => some "serializeDecimal" - | q`Init.Bool => some "serializeBool" - | q`Init.ByteArray => some "serializeBytes" - | _ => .none - -/-- Get the serializer method reference for a SyntaxCat's inner type (used in Option/List). -/ -def serializerFnRef (c : SyntaxCat) : String := - match primitiveSerializerMethod c.name with - | some method => s!"$s::{method}" - | none => "$s::serialize" - -/-- Generate the serialization expression for a single field. -/ -def serializeFieldExpr (kind : ArgDeclKind) (fieldName : String) : String := - match kind with - | .type _ => s!"$s.serialize({fieldName})" - | .cat c => - match primitiveSerializerMethod c.name with - | some method => s!"$s.{method}({fieldName})" - | none => - if abstractCategories.contains c.name then s!"$s.serialize({fieldName})" - else match c.name with - | q`Init.Option => - let inner := c.args[0]! - s!"$s.serializeOption({fieldName}, {serializerFnRef inner})" - | _ => - if let some sep := SepFormat.fromCategoryName? c.name then - let inner := c.args[0]! - s!"$s.serializeSeq({fieldName}, \"{sep.toIonName}\", {serializerFnRef inner})" - else s!"$s.serialize({fieldName})" - -/-! ## Java Structures -/ - -structure JavaField where +/-! ## Leaf type detection and mapping -/ + +private meta def isLeafTypeName (name : Name) : Bool := + name == ``Nat || name == ``Int || name == ``String || name == ``Bool || name == ``Float || + name == ``StrataDDM.Decimal + +private meta def leafJavaType (name : Name) : Option String := + match name with + | ``Nat => some "long" + | ``Int => some "long" + | ``Float => some "double" + | ``String => some "java.lang.String" + | ``Bool => some "boolean" + | ``StrataDDM.Decimal => some "java.math.BigDecimal" + | _ => none + +private meta def leafSerializeExpr (name : Name) (accessor : String) : Option String := + match name with + | ``Nat => some s!"ion.newInt({accessor})" + | ``Int => some s!"ion.newInt({accessor})" + | ``Float => some s!"ion.newFloat({accessor})" + | ``String => some s!"ion.newString({accessor})" + | ``Bool => some s!"ion.newBool({accessor})" + | ``StrataDDM.Decimal => some s!"ion.newDecimal({accessor})" + | _ => none + +/-! ## Type info extraction -/ + +private inductive FieldTypeInfo where + | leaf (name : Name) + | compound (name : Name) (typeArgs : Array FieldTypeInfo) + | typeParam (paramName : String) -- type parameter; generates a Java generic + | list (elem : FieldTypeInfo) + | option (elem : FieldTypeInfo) + +private structure JavaFieldInfo where name : String - type : JavaType - -/-- A nested record within a category interface. -/ -structure JavaCategoryRecord where - name : String - operationName : QualifiedIdent - fields : Array JavaField - argDecls : Array ArgDecl -- original DDM arg declarations for toIon generation - -/-- All generated Java source files for a dialect. -/ -public structure GeneratedFiles where - sourceRange : String - node : String - categories : Array (String × String) -- (filename, content) - stubs : Array (String × String) -- (filename, content) for stub interfaces - builders : String × String -- (filename, content) - serializer : String - deriving Inhabited - -/-- Mapping from DDM names to disambiguated Java identifiers. -/ -structure NameAssignments where - categories : Std.HashMap QualifiedIdent String - /-- Maps (category, opName) to the nested record name within that category -/ - operators : Std.HashMap (QualifiedIdent × String) String - stubs : Std.HashMap QualifiedIdent String - builders : String - -/-! ## Code Generation -/ - -def argDeclToJavaField (decl : ArgDecl) : JavaField := - { name := escapeJavaName decl.ident, type := argDeclKindToJavaType decl.kind } - -def JavaField.toParam (f : JavaField) : String := - s!"{f.type.toJava} {f.name}" - -/-- Group operators by their target category, preserving declaration order. -/ -def groupOpsByCategory (d : Dialect) : Std.HashMap QualifiedIdent (Array OpDecl) := - d.declarations.foldl (init := {}) fun acc decl => - match decl with - | .op op => acc.alter op.category (fun ops? => some ((ops?.getD #[]).push op)) - | _ => acc - -def templatePackage := "com.strata.template" - -def sourceRangeTemplate : String := include_str "templates/SourceRange.java" -def nodeTemplate : String := include_str "templates/Node.java" -def serializerTemplate : String := include_str "templates/IonSerializer.java" - -def generateSourceRange (package : String) : String := - sourceRangeTemplate.replace templatePackage package - -def generateNodeInterface (package : String) (categories : List String) : String := - let base := nodeTemplate.replace templatePackage package - if categories.isEmpty then base - else - let permits := " permits " ++ String.intercalate ", " categories - base.replace "sealed interface Node" s!"sealed interface Node{permits}" - -/-- Generate non-sealed stub interface for a category with no operators -/ -def generateStubInterface (package : String) (name : String) : String × String := - (s!"{name}.java", s!"package {package};\n\npublic non-sealed interface {name} extends Node \{}\n") - -def generateSerializer (package : String) : String := - serializerTemplate.replace templatePackage package - -/-- Generate a nested record definition within a category interface. -/ -def generateRecord (catName : String) (r : JavaCategoryRecord) : String := - let params := ", ".intercalate (r.fields.toList.map JavaField.toParam) - let opName := s!"{r.operationName.dialect}.{r.operationName.name}" - let fieldSerializations := r.argDecls.toList.map fun arg => - let fieldName := escapeJavaName arg.ident - s!" sexp.add({serializeFieldExpr arg.kind (fieldName ++ "()")});" - let toIonBody := "\n".intercalate - (s!" var sexp = $s.newOp(\"{opName}\", sourceRange());" - :: fieldSerializations ++ [" return sexp;"]) - s!" public record {r.name}( - SourceRange sourceRange{if r.fields.isEmpty then "" else ",\n " ++ params} - ) implements {catName} \{ - @Override - public java.lang.String operationName() \{ return \"{opName}\"; } - + typeInfo : FieldTypeInfo + +private meta instance : Inhabited JavaFieldInfo := ⟨{ name := "", typeInfo := .leaf `unknown }⟩ + +private structure CtorInfo' where + name : Name + shortName : String + fields : Array JavaFieldInfo + +private meta instance : Inhabited CtorInfo' := ⟨{ name := `unknown, shortName := "", fields := #[] }⟩ + +private inductive TypeShape where + | struct (name : Name) (javaName : String) (fields : Array JavaFieldInfo) (typeParams : Array String := #[]) + | singleCtor (name : Name) (javaName : String) (ctor : CtorInfo') (typeParams : Array String := #[]) + | multiCtor (name : Name) (javaName : String) (ctors : Array CtorInfo') (typeParams : Array String := #[]) + +private meta def isCompoundType (env : Environment) (name : Name) : Bool := + !isLeafTypeName name && + ((getStructureInfo? env name).isSome || + match env.find? name with | some (.inductInfo _) => true | _ => false) + +/-- Extract Java type parameter name from a tagged level, if it is one. -/ +private meta def extractTypeParamName : Level → Option String + | .param n => + let s := n.toString (escape := false) + if s.startsWith "__javaTypeParam_" then some (s.drop "__javaTypeParam_".length).toString + else none + | _ => none + +private meta partial def classifyFieldType (env : Environment) (ty : Expr) + (paramNames : Array String := #[]) : MetaM FieldTypeInfo := do + let ty ← whnf ty + -- Strip optParam/autoParam wrappers (fields with default values) + let ty := match ty.getAppFn.constName? with + | some ``optParam => + let args := ty.getAppArgs + if h : args.size > 0 then args[0] else ty + | some ``autoParam => + let args := ty.getAppArgs + if h : args.size > 0 then args[0] else ty + | _ => ty + let name := ty.getAppFn.constName? + match name with + | some ``List => + let args := ty.getAppArgs + if h : args.size > 0 then return .list (← classifyFieldType env args[0] paramNames) + else return .leaf `unknown + | some ``Option => + let args := ty.getAppArgs + if h : args.size > 0 then return .option (← classifyFieldType env args[0] paramNames) + else return .leaf `unknown + | some n => + if isCompoundType env n then + -- Collect type arguments as FieldTypeInfo + let args := ty.getAppArgs + let numParams := match env.find? n with + | some (.inductInfo indInfo) => indInfo.numParams + | _ => args.size + let typeArgs ← args[:numParams].toArray.mapM (classifyFieldType env · paramNames) + return .compound n typeArgs + else return .leaf n + | none => + -- Check for tagged type parameter sorts + if let .sort level := ty then + if let some pName := extractTypeParamName level then + return .typeParam pName + if ty.isSort || ty.isFVar then return .typeParam "T" + return .leaf `unknown + +private meta def extractCtorFields (env : Environment) (ctorName : Name) + (fieldNames? : Option (Array Name) := none) : MetaM (Array String × Array JavaFieldInfo) := do + let some (.ctorInfo ci) := env.find? ctorName + | throwError "Cannot find constructor {ctorName}" + let mut ty := ci.type + -- Collect parameter names and substitute with unique level-tagged sorts + let mut paramNames : Array String := #[] + for _ in List.range ci.numParams do + match ty with + | .forallE n dom b _ => + let pName := n.toString (escape := false) + let jName := toPascalCase pName + paramNames := paramNames.push jName + -- Use a tagged sort as placeholder; only substitute Type-valued params + let placeholder := if dom.isSort then + mkSort (mkLevelParam (Name.mkStr .anonymous s!"__javaTypeParam_{jName}")) + else + mkSort levelZero + ty := b.instantiate1 placeholder + | _ => break + let mut fields := #[] + for i in List.range ci.numFields do + match ty with + | .forallE n t b _ => + let typeInfo ← classifyFieldType env t paramNames + let name := match fieldNames? with + | some names => names[i]!.toString (escape := false) + | none => + let s := n.toString (escape := false) + if s.startsWith "_" && s.length > 1 then s!"field{i}" else s + fields := fields.push { name, typeInfo } + ty := b.instantiate1 (mkSort levelZero) + | _ => break + return (paramNames, fields) + +private meta def analyzeType (env : Environment) (typeName : Name) : MetaM TypeShape := do + let javaName := escapeJavaName (toPascalCase (typeName.getString!)) + if let some sinfo := getStructureInfo? env typeName then + let (paramNames, fields) ← extractCtorFields env (sinfo.structName ++ `mk) (some sinfo.fieldNames) + return .struct typeName javaName fields paramNames + let some (.inductInfo indInfo) := env.find? typeName + | throwError "{typeName} is not an inductive or structure type" + let mut typeParams : Array String := #[] + let mut ctors : Array CtorInfo' := #[] + for ctorName in indInfo.ctors do + let (paramNames, fields) ← extractCtorFields env ctorName + typeParams := paramNames + ctors := ctors.push { name := ctorName, shortName := ctorName.getString!, fields } + if ctors.size == 1 then + return .singleCtor typeName javaName ctors[0]! typeParams + return .multiCtor typeName javaName ctors typeParams + +private meta partial def extractCompoundNamesFromExpr (env : Environment) (t : Expr) : MetaM (Array Name) := do + let t ← whnf t + -- Strip optParam/autoParam wrappers + let t := match t.getAppFn.constName? with + | some ``optParam => + let args := t.getAppArgs + if h : args.size > 0 then args[0] else t + | some ``autoParam => + let args := t.getAppArgs + if h : args.size > 0 then args[0] else t + | _ => t + let name := t.getAppFn.constName? + match name with + | some ``List | some ``Option => + let args := t.getAppArgs + if h : args.size > 0 then extractCompoundNamesFromExpr env args[0] + else return #[] + | some n => + let mut result := #[] + if isCompoundType env n then result := result.push n + -- Also recurse into type arguments to find nested compound types + for arg in t.getAppArgs do + result := result ++ (← extractCompoundNamesFromExpr env arg) + return result + | none => return #[] + +private meta def collectNestedTypes (env : Environment) (rootName : Name) : MetaM (Array Name) := do + let mut visited : Std.HashSet Name := {} + let mut queue := #[rootName] + let mut result := #[] + while h : queue.size > 0 do + let name := queue[0] + queue := queue.extract 1 queue.size + if visited.contains name then continue + visited := visited.insert name + result := result.push name + let ctors := if let some sinfo := getStructureInfo? env name then + [sinfo.structName ++ `mk] + else match env.find? name with + | some (.inductInfo indInfo) => indInfo.ctors + | _ => [] + for ctorName in ctors do + let some (.ctorInfo ci) := env.find? ctorName | continue + let mut ty := ci.type + for _ in List.range ci.numParams do + match ty with + | .forallE _ _ b _ => ty := b.instantiate1 (mkSort levelZero) + | _ => break + for _ in List.range ci.numFields do + match ty with + | .forallE _ t b _ => + for n in ← extractCompoundNamesFromExpr env t do + if !visited.contains n then queue := queue.push n + ty := b.instantiate1 (mkSort levelZero) + | _ => break + return result + +/-! ## Java Code Generation -/ + +private meta partial def javaTypeForInfo : FieldTypeInfo → String + | .leaf name => (leafJavaType name).getD "java.lang.Object" + | .compound name typeArgs => + let base := escapeJavaName (toPascalCase (name.getString!)) + if typeArgs.isEmpty then base + else s!"{base}<{", ".intercalate (typeArgs.toList.map javaBoxedTypeForInfo)}>" + | .typeParam paramName => paramName + | .list elem => s!"java.util.List<{javaBoxedTypeForInfo elem}>" + | .option elem => javaBoxedTypeForInfo elem +where + javaBoxedTypeForInfo : FieldTypeInfo → String + | .leaf ``Nat | .leaf ``Int => "Long" + | .leaf ``Float => "Double" + | .leaf ``Bool => "Boolean" + | .leaf ``StrataDDM.Decimal => "java.math.BigDecimal" + | .leaf ``String => "java.lang.String" + | other => javaTypeForInfo other + +private meta def javaTypeFor (f : JavaFieldInfo) : String := javaTypeForInfo f.typeInfo + +private meta partial def serializeExprForInfo (ti : FieldTypeInfo) (accessor : String) : String := + match ti with + | .leaf name => (leafSerializeExpr name accessor).getD "ion.newNull()" + | .compound _ _ => s!"{accessor}.toIon(ion)" + | .typeParam _ => s!"{accessor}.toIon(ion)" + | .list _ => + -- List serialization requires multiple statements; handled by toIon body generators. + -- This branch is used for inner elements of containers (e.g., Option (List T)). + s!"{accessor}.toIon(ion)" + | .option elem => + let inner := serializeExprForInfo elem accessor + s!"({accessor} != null ? {inner} : ion.newNull())" + +private meta def serializeExprFor (f : JavaFieldInfo) (accessor : String) : String := + serializeExprForInfo f.typeInfo accessor + +private meta def recordParams (fields : Array JavaFieldInfo) : String := + ", ".intercalate (fields.toList.map fun f => s!"{javaTypeFor f} {escapeJavaName f.name}") + +private meta def typeParamDecl (typeParams : Array String) : String := + if typeParams.isEmpty then "" + else s!"<{", ".intercalate (typeParams.toList.map fun p => s!"{p} extends ToIon")}>" + +private meta def typeParamUse (typeParams : Array String) : String := + if typeParams.isEmpty then "" + else s!"<{", ".intercalate typeParams.toList}>" + +/-- Generate the toIon method body for a struct (Ion struct with field name keys). -/ +private meta def structToIonBody (fields : Array JavaFieldInfo) : String := + let fieldLines := (List.range fields.size).flatMap fun i => + let f := fields[i]! + let accessor := s!"{escapeJavaName f.name}()" + match f.typeInfo with + | .list elem => + let inner := serializeExprForInfo elem "e" + [s!" var _l_{escapeJavaName f.name} = ion.newEmptyList();", + s!" for (var e : {accessor}) _l_{escapeJavaName f.name}.add({inner});", + s!" s.put(\"{f.name}\", _l_{escapeJavaName f.name});"] + | _ => + [s!" s.put(\"{f.name}\", {serializeExprFor f accessor});"] + s!" var s = ion.newEmptyStruct();\n{"\n".intercalate fieldLines}\n return s;" + +/-- Generate the toIon method body for a single-ctor inductive (Ion struct with _0, _1, ... keys). -/ +private meta def singleCtorToIonBody (fields : Array JavaFieldInfo) : String := + let fieldLines := (List.range fields.size).flatMap fun i => + let f := fields[i]! + let accessor := s!"{escapeJavaName f.name}()" + match f.typeInfo with + | .list elem => + let inner := serializeExprForInfo elem "e" + [s!" var _l{i} = ion.newEmptyList();", + s!" for (var e : {accessor}) _l{i}.add({inner});", + s!" s.put(\"_{i}\", _l{i});"] + | _ => + [s!" s.put(\"_{i}\", {serializeExprFor f accessor});"] + s!" var s = ion.newEmptyStruct();\n{"\n".intercalate fieldLines}\n return s;" + +private meta def multiCtorToIonBody (shortName : String) (fields : Array JavaFieldInfo) : String := + let fieldLines := (List.range fields.size).flatMap fun i => + let f := fields[i]! + let accessor := s!"{escapeJavaName f.name}()" + match f.typeInfo with + | .list elem => + let inner := serializeExprForInfo elem "e" + [s!" var _l{i} = ion.newEmptyList();", + s!" for (var e : {accessor}) _l{i}.add({inner});", + s!" sexp.add(_l{i});"] + | _ => + [s!" sexp.add({serializeExprFor f accessor});"] + s!" var sexp = ion.newEmptySexp();\n sexp.add(ion.newSymbol(\"{shortName}\"));\n{"\n".intercalate fieldLines}\n return sexp;" + +private meta def generateRecord (interfaceName : String) (recordName : String) + (fields : Array JavaFieldInfo) (toIonBody : String) (tpDecl : String := "") : String := + let params := recordParams fields + s!" public record {recordName}{tpDecl}({params}) implements {interfaceName} \{ @Override - public com.amazon.ion.IonSexp toIon(IonSerializer $s) \{ + public com.amazon.ion.IonValue toIon(com.amazon.ion.IonSystem ion) \{ {toIonBody} } }" -/-- Generate a category file with sealed interface and nested records. -/ -def generateCategoryFile (package : String) (catName : String) (records : Array JavaCategoryRecord) : String := - let permits := if records.isEmpty then "" - else " permits " ++ ", ".intercalate (records.toList.map fun r => s!"{catName}.{r.name}") - let body := "\n\n".intercalate (records.toList.map (generateRecord catName)) - s!"package {package}; - -public sealed interface {catName} extends Node{permits} \{ -{body} +private meta def generateTypeFile (package : String) (shape : TypeShape) : String := + match shape with + | .struct _ javaName fields typeParams => + let toIon := structToIonBody fields + let params := recordParams fields + let tpDecl := typeParamDecl typeParams + s!"package {package}; + +public record {javaName}{tpDecl}({params}) implements ToIon \{ + public com.amazon.ion.IonValue toIon(com.amazon.ion.IonSystem ion) \{ +{toIon} + } +} +" + | .singleCtor _ javaName ctor typeParams => + let toIon := singleCtorToIonBody ctor.fields + let params := recordParams ctor.fields + let tpDecl := typeParamDecl typeParams + s!"package {package}; + +public record {javaName}{tpDecl}({params}) implements ToIon \{ + public com.amazon.ion.IonValue toIon(com.amazon.ion.IonSystem ion) \{ +{toIon} + } +} +" + | .multiCtor _ javaName ctors typeParams => + let tpDecl := typeParamDecl typeParams + let tpUse := typeParamUse typeParams + let recordDefs := ctors.toList.map fun ctor => + let recName := escapeJavaName (toPascalCase ctor.shortName) + let toIon := multiCtorToIonBody ctor.shortName ctor.fields + generateRecord (s!"{javaName}{tpUse}") recName ctor.fields toIon tpDecl + let permits := ", ".intercalate (ctors.toList.map fun ctor => + s!"{javaName}.{escapeJavaName (toPascalCase ctor.shortName)}") + s!"package {package}; + +public sealed interface {javaName}{tpDecl} extends ToIon permits {permits} \{ + com.amazon.ion.IonValue toIon(com.amazon.ion.IonSystem ion); + +{"\n\n".intercalate recordDefs} } " -/-- Assign unique Java names to all generated types. - Operator names are scoped within their category (nested records). -/ -def assignAllNames (d : Dialect) : NameAssignments := - let baseNames : Std.HashSet String := Std.HashSet.ofList ["node", "sourcerange", "ionserializer"] - - -- Collect unique categories and referenced types - let init : Array QualifiedIdent × Std.HashSet QualifiedIdent := (#[], {}) - let (cats, refs) := d.declarations.foldl (init := init) fun (cats, refs) decl => - match decl with - | .op op => - let cats := if cats.contains op.category then cats else cats.push op.category - let refs := op.argDecls.toArray.foldl (init := refs) fun refs arg => - match arg.kind with - | .type _ => refs.insert q`Init.Expr - | .cat c => match syntaxCatToQualifiedName c with - | some qid => refs.insert qid - | none => refs - (cats, refs) - | _ => (cats, refs) - - -- All QualifiedIdents that need Java names (categories + refs) - let allQids := cats ++ refs.toArray.filter (!cats.contains ·) - - -- Count name occurrences to detect collisions across categories - let nameCounts : Std.HashMap String Nat := allQids.foldl (init := {}) fun m qid => - m.alter qid.name (fun v => some (v.getD 0 + 1)) - - -- Assign Java names, prefixing with dialect when there's a collision - let assignName (used : Std.HashSet String) (qid : QualifiedIdent) : String × Std.HashSet String := - let base := if nameCounts.getD qid.name 0 > 1 - then escapeJavaName (toPascalCase s!"{qid.dialect}_{qid.name}") - else escapeJavaName (toPascalCase qid.name) - disambiguate base used - - -- Assign category names (top-level, must be globally unique) - let catInit : Std.HashMap QualifiedIdent String × Std.HashSet String := ({}, baseNames) - let (categoryNames, used) := cats.foldl (init := catInit) fun (map, used) cat => - let (name, newUsed) := assignName used cat - (map.insert cat name, newUsed) - - -- Assign operator names (nested within category, must be unique within category + not collide with category name) - let opsByCategory := groupOpsByCategory d - - let operatorNames := opsByCategory.toList.foldl (init := ({})) fun opNames (cat, ops) => - let catName := categoryNames[cat]! - -- Within each category, operator names must be unique and not collide with the category name - let localUsed : Std.HashSet String := Std.HashSet.ofList [catName.toLower] - let (opNames, _) := ops.foldl (init := (opNames, localUsed)) fun (opNames, localUsed) op => - let base := escapeJavaName (toPascalCase op.name) - -- For single-op categories where the op name matches the category, use "Of" - let base := if ops.size == 1 && base.toLower == catName.toLower then "Of" else base - let (name, newLocalUsed) := disambiguate base localUsed - (opNames.insert (op.category, op.name) name, newLocalUsed) - opNames - - -- Assign stub names (referenced types not in this dialect's categories) - let stubInit : Std.HashMap QualifiedIdent String × Std.HashSet String := ({}, used) - let (stubNames, used) := refs.toArray.foldl (init := stubInit) fun (map, used) ref => - if categoryNames.contains ref then (map, used) - else - let (name, newUsed) := assignName used ref - (map.insert ref name, newUsed) - - let (buildersName, _) := disambiguate (escapeJavaName (toPascalCase d.name)) used - - { categories := categoryNames, operators := operatorNames, stubs := stubNames, builders := buildersName } - -def generateBuilders (package : String) (dialectName : String) (d : Dialect) (names : NameAssignments) : String := - let methods (op : OpDecl) := - let (ps, as, checks) := op.argDecls.toArray - |>.foldl (init := (#[], #[], #[])) fun (ps, as, checks) decl => - let name := escapeJavaName decl.ident - let cat := decl.kind.categoryOf.name - if cat == q`Init.Num then - (ps.push s!"long {name}", - as.push s!"java.math.BigInteger.valueOf({name})", - checks.push s!"if ({name} < 0) throw new IllegalArgumentException(\"{name} must be non-negative\");") - else if cat == q`Init.Decimal then - (ps.push s!"double {name}", - as.push s!"java.math.BigDecimal.valueOf({name})", - checks) - else - let t := (argDeclKindToJavaType decl.kind).toJava - (ps.push s!"{t} {name}", as.push name, checks) - let methodName := escapeJavaName op.name - let returnType := names.categories[op.category]! - let recordName := s!"{returnType}.{names.operators[(op.category, op.name)]!}" - let checksStr := if checks.isEmpty then "" else " ".intercalate checks.toList ++ " " - let argsStr := if as.isEmpty then "" else ", " ++ ", ".intercalate as.toList - let paramsStr := ", ".intercalate ps.toList - let srParams := if ps.isEmpty then "SourceRange sourceRange" else s!"SourceRange sourceRange, {paramsStr}" - let withSR := s!" public static {returnType} {methodName}({srParams}) \{ {checksStr}return new {recordName}(sourceRange{argsStr}); }" - let withoutSR := s!" public static {returnType} {methodName}({paramsStr}) \{ {checksStr}return new {recordName}(SourceRange.NONE{argsStr}); }" - s!"{withSR}\n{withoutSR}" - let allMethods := d.declarations.filterMap fun | .op op => some (methods op) | _ => none - s!"package {package};\n\npublic class {dialectName} \{\n{"\n\n".intercalate allMethods.toList}\n}\n" - -public def generateDialect (d : Dialect) (package : String) : Except String GeneratedFiles := do - let names := assignAllNames d - - -- Check for unsupported declarations - for decl in d.declarations do - match decl with - | .type t => throw s!"type declaration '{t.name}' is not supported in Java generation" - | .function f => throw s!"function declaration '{f.name}' is not supported in Java generation" - | _ => pure () - - -- Group operators by category (preserving declaration order) - let opsByCategory := groupOpsByCategory d - - -- Generate category files (sealed interface + nested records) - let categoryFiles := opsByCategory.toList.map fun (cat, ops) => - let catName := names.categories[cat]! - let records := ops.map fun op => - let recName := names.operators[(op.category, op.name)]! - { name := recName - operationName := ⟨d.name, op.name⟩ - fields := op.argDecls.toArray.map argDeclToJavaField - argDecls := op.argDecls.toArray : JavaCategoryRecord } - (s!"{catName}.java", generateCategoryFile package catName records) - - -- Stub interfaces for referenced types without operators - let stubFiles := names.stubs.toList.map fun (_, name) => - generateStubInterface package name - - -- All type names for Node permits clause - let allTypeNames := categoryFiles.map (·.1.dropEnd 5 |>.toString) - ++ stubFiles.map (·.1.dropEnd 5 |>.toString) - - return { - sourceRange := generateSourceRange package - node := generateNodeInterface package allTypeNames - categories := categoryFiles.toArray - stubs := stubFiles.toArray - builders := (s!"{names.builders}.java", generateBuilders package names.builders d names) - serializer := generateSerializer package - } - -/-! ## File Output -/ - -public def packageToPath (package : String) : System.FilePath := - let parts := package.splitOn "." - ⟨String.intercalate "/" parts⟩ - -public def writeJavaFiles (baseDir : System.FilePath) (package : String) (files : GeneratedFiles) : IO Unit := do - let dir := baseDir / packageToPath package - IO.FS.createDirAll dir - - IO.FS.writeFile (dir / "SourceRange.java") files.sourceRange - IO.FS.writeFile (dir / "Node.java") files.node - IO.FS.writeFile (dir / "IonSerializer.java") files.serializer - IO.FS.writeFile (dir / files.builders.1) files.builders.2 - - for (filename, content) in files.categories do - IO.FS.writeFile (dir / filename) content +private meta def generateForType (env : Environment) (package : String) (rootName : Name) : + MetaM GeneratedFiles := do + let nestedTypes ← collectNestedTypes env rootName + let mut files := #[] + -- Emit the ToIon interface used by type-parameter fields + let toIonInterface := s!"package {package};\n\npublic interface ToIon \{\n com.amazon.ion.IonValue toIon(com.amazon.ion.IonSystem ion);\n}\n" + files := files.push ("ToIon.java", toIonInterface) + for typeName in nestedTypes do + let shape ← analyzeType env typeName + let javaName := match shape with + | .struct _ n _ _ | .singleCtor _ n _ _ | .multiCtor _ n _ _ => n + let content := generateTypeFile package shape + files := files.push (s!"{javaName}.java", content) + return { files } + +/-! ## Elaborator -/ + +public section + +/-- +`getIonSerializer%` generates Java source files for a Lean type. +The result has type `Strata.Java.GeneratedFiles`. + +Usage: `getIonSerializer% MyType "com.example.pkg"` +-/ +syntax (name := getIonSerializerStx) "getIonSerializer%" ident str : term + +@[term_elab getIonSerializerStx] +meta def getIonSerializerElab : TermElab := fun stx _expectedType? => do + match stx with + | `(getIonSerializer% $typeId $pkgStr) => do + let typeName ← resolveGlobalConstNoOverload typeId + let env ← getEnv + let package := pkgStr.getString + let result ← generateForType env package typeName + let filesArr ← result.files.mapM fun (name, content) => do + let nameLit : TSyntax `str := ⟨Syntax.mkStrLit name⟩ + let contentLit : TSyntax `str := ⟨Syntax.mkStrLit content⟩ + `(($nameLit, $contentLit)) + let arrStx ← `(#[$[$filesArr],*]) + let resultStx ← `(Strata.Java.GeneratedFiles.mk $arrStx) + elabTerm resultStx _expectedType? + | _ => throwUnsupportedSyntax - for (filename, content) in files.stubs do - IO.FS.writeFile (dir / filename) content +end -end StrataDDM.Java +end Strata.Java diff --git a/StrataDDM/StrataDDM/Integration/Java/templates/IonSerializer.java b/StrataDDM/StrataDDM/Integration/Java/templates/IonSerializer.java deleted file mode 100644 index 11dd708656..0000000000 --- a/StrataDDM/StrataDDM/Integration/Java/templates/IonSerializer.java +++ /dev/null @@ -1,82 +0,0 @@ -package com.strata.template; - -import com.amazon.ion.*; -import com.amazon.ion.system.*; - -public class IonSerializer { - private final IonSystem ion; - - public IonSerializer(IonSystem ion) { - this.ion = ion; - } - - /** Serialize a node as a top-level command (no "op" wrapper). */ - public IonValue serializeCommand(Node node) { - return node.toIon(this); - } - - /** Serialize a node as an argument (with "op" wrapper). */ - public IonValue serialize(Node node) { - IonSexp sexp = ion.newEmptySexp(); - sexp.add(ion.newSymbol("op")); - sexp.add(node.toIon(this)); - return sexp; - } - - /** Create an s-expression with operation name and source range. */ - public IonSexp newOp(java.lang.String opName, SourceRange sr) { - IonSexp sexp = ion.newEmptySexp(); - sexp.add(ion.newSymbol(opName)); - if (sr.start() == 0 && sr.stop() == 0) { - sexp.add(ion.newNull()); - } else { - IonSexp range = ion.newEmptySexp(); - range.add(ion.newInt(sr.start())); - range.add(ion.newInt(sr.stop())); - sexp.add(range); - } - return sexp; - } - - private IonSexp newTagged(String symbol, IonValue value) { - IonSexp sexp = ion.newEmptySexp(); - sexp.add(ion.newSymbol(symbol)); - sexp.add(ion.newNull()); - sexp.add(value); - return sexp; - } - - public IonValue serializeIdent(java.lang.String s) { return newTagged("ident", ion.newString(s)); } - public IonValue serializeStrlit(java.lang.String s) { return newTagged("strlit", ion.newString(s)); } - public IonValue serializeNum(java.math.BigInteger n) { return newTagged("num", ion.newInt(n)); } - public IonValue serializeDecimal(java.math.BigDecimal d) { return newTagged("decimal", ion.newDecimal(d)); } - public IonValue serializeBytes(byte[] bytes) { return newTagged("bytes", ion.newBlob(bytes)); } - - public IonValue serializeBool(boolean b) { - IonSexp inner = ion.newEmptySexp(); - inner.add(ion.newSymbol(b ? "Init.boolTrue" : "Init.boolFalse")); - inner.add(ion.newNull()); - IonSexp sexp = ion.newEmptySexp(); - sexp.add(ion.newSymbol("op")); - sexp.add(inner); - return sexp; - } - - public IonValue serializeOption(java.util.Optional opt, java.util.function.Function f) { - IonSexp sexp = ion.newEmptySexp(); - sexp.add(ion.newSymbol("option")); - sexp.add(ion.newNull()); - opt.ifPresent(v -> sexp.add(f.apply(v))); - return sexp; - } - - public IonValue serializeSeq(java.util.List list, java.lang.String sepType, java.util.function.Function f) { - IonSexp sexp = ion.newEmptySexp(); - sexp.add(ion.newSymbol(sepType)); - sexp.add(ion.newNull()); - for (T item : list) { - sexp.add(f.apply(item)); - } - return sexp; - } -} diff --git a/StrataDDM/StrataDDM/Integration/Java/templates/Node.java b/StrataDDM/StrataDDM/Integration/Java/templates/Node.java deleted file mode 100644 index ca639c7937..0000000000 --- a/StrataDDM/StrataDDM/Integration/Java/templates/Node.java +++ /dev/null @@ -1,9 +0,0 @@ -package com.strata.template; - -import com.amazon.ion.IonSexp; - -public sealed interface Node { - SourceRange sourceRange(); - java.lang.String operationName(); - IonSexp toIon(IonSerializer $s); -} diff --git a/StrataDDM/StrataDDM/Integration/Java/templates/SourceRange.java b/StrataDDM/StrataDDM/Integration/Java/templates/SourceRange.java deleted file mode 100644 index e993a1ff92..0000000000 --- a/StrataDDM/StrataDDM/Integration/Java/templates/SourceRange.java +++ /dev/null @@ -1,5 +0,0 @@ -package com.strata.template; - -public record SourceRange(long start, long stop) { - public static final SourceRange NONE = new SourceRange(0, 0); -} diff --git a/StrataTest/Util/IonDeserializer.lean b/StrataTest/Util/IonDeserializer.lean new file mode 100644 index 0000000000..867810bafd --- /dev/null +++ b/StrataTest/Util/IonDeserializer.lean @@ -0,0 +1,144 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +module + +import Strata.Util.IonDeserializer + +-- Test structure +structure Point where + x : Nat + y : Nat +deriving Repr, BEq + +-- Verify the elaborator produces a well-typed function +def deserializePoint : ByteArray → Except Std.Format Point := + getIonDeserializer% Point + +-- Test multi-constructor inductive +inductive Color where + | red + | green + | blue +deriving Repr, BEq + +def deserializeColor : ByteArray → Except Std.Format Color := + getIonDeserializer% Color + +-- Test inductive with fields +inductive Shape where + | circle (radius : Nat) + | rect (width : Nat) (height : Nat) +deriving Repr, BEq + +def deserializeShape : ByteArray → Except Std.Format Shape := + getIonDeserializer% Shape + +-- Test structure with String and Bool +structure Person where + name : String + age : Nat + active : Bool +deriving Repr, BEq + +def deserializePerson : ByteArray → Except Std.Format Person := + getIonDeserializer% Person + +-- Test structure with Int +structure Offset where + dx : Int + dy : Int +deriving Repr, BEq + +def deserializeOffset : ByteArray → Except Std.Format Offset := + getIonDeserializer% Offset + +-- Test structure with Float +structure Measurement where + value : Float + tolerance : Float +deriving Repr, BEq + +def deserializeMeasurement : ByteArray → Except Std.Format Measurement := + getIonDeserializer% Measurement + +-- Test nested structure (non-recursive) +structure Line where + start : Point + stop : Point +deriving Repr, BEq + +def deserializeLine : ByteArray → Except Std.Format Line := + getIonDeserializer% Line + +-- Test recursive type +inductive Tree where + | leaf (value : Nat) + | node (left : Tree) (right : Tree) +deriving Repr, BEq + +partial def deserializeTree : ByteArray → Except Std.Format Tree := + getIonDeserializer% Tree + +-- Verify type signatures +#check (deserializePoint : ByteArray → Except Std.Format Point) +#check (deserializeColor : ByteArray → Except Std.Format Color) +#check (deserializeShape : ByteArray → Except Std.Format Shape) +#check (deserializePerson : ByteArray → Except Std.Format Person) +#check (deserializeOffset : ByteArray → Except Std.Format Offset) +#check (deserializeMeasurement : ByteArray → Except Std.Format Measurement) +#check (deserializeLine : ByteArray → Except Std.Format Line) +#check (deserializeTree : ByteArray → Except Std.Format Tree) + +-- Test structure with List fields +structure Polygon where + vertices : List Point +deriving Repr, BEq + +partial def deserializePolygon : ByteArray → Except Std.Format Polygon := + getIonDeserializer% Polygon + +#check (deserializePolygon : ByteArray → Except Std.Format Polygon) + +-- Test structure with Option fields +structure Config where + name : String + timeout : Option Nat +deriving Repr, BEq + +def deserializeConfig : ByteArray → Except Std.Format Config := + getIonDeserializer% Config + +#check (deserializeConfig : ByteArray → Except Std.Format Config) + +-- Test structure with Decimal fields +structure Price where + amount : StrataDDM.Decimal +deriving Repr, BEq + +def deserializePrice : ByteArray → Except Std.Format Price := + getIonDeserializer% Price + +#check (deserializePrice : ByteArray → Except Std.Format Price) + +-- Test structure with List of leaf types +structure Numbers where + values : List Nat +deriving Repr, BEq + +def deserializeNumbers : ByteArray → Except Std.Format Numbers := + getIonDeserializer% Numbers + +#check (deserializeNumbers : ByteArray → Except Std.Format Numbers) + +-- Test structure with Option of compound type +structure MaybeLine where + line : Option Line +deriving Repr, BEq + +partial def deserializeMaybeLine : ByteArray → Except Std.Format MaybeLine := + getIonDeserializer% MaybeLine + +#check (deserializeMaybeLine : ByteArray → Except Std.Format MaybeLine) diff --git a/StrataTestExtra/Languages/Java/TestGen.lean b/StrataTestExtra/Languages/Java/TestGen.lean index 8ce4ca3dbc..e46ce2de65 100644 --- a/StrataTestExtra/Languages/Java/TestGen.lean +++ b/StrataTestExtra/Languages/Java/TestGen.lean @@ -5,421 +5,272 @@ -/ module -public import Lean.Elab.Command -public meta import StrataDDM.BuiltinDialects.Init -public meta import StrataDDM.Integration.Java -public meta import StrataDDM.Integration.Lean.Env -meta import StrataDDM.Integration.Lean.HashCommands -- For #load_dialect -public meta import StrataDDM.Ion -import Strata.Languages.Core.DDMTransform.Grammar -- Loads Strata Core dialect into env +public meta import Lean.Elab.Command +public meta import StrataDDM.Integration.Java.Gen +public meta import Strata.Util.IonDeserializer -namespace StrataDDM.Java.Test +open Strata.Java -open StrataDDM.Java +namespace Strata.Java.Test meta def check (s sub : String) : Bool := (s.splitOn sub).length > 1 --- Test 1: Basic dialect with 2 operators — nested records in category file -#eval do - let testDialect : StrataDDM.Dialect := { - name := "Test" - imports := #[] - declarations := #[ - .syncat { name := "Expr", argNames := #[] }, - .op { - name := "literal" - argDecls := .ofArray #[ - { ident := "value", kind := .cat (.atom .none ⟨"Init", "Num"⟩) } - ] - category := ⟨"Test", "Expr"⟩ - syntaxDef := .std #[] 0 - }, - .op { - name := "add" - argDecls := .ofArray #[ - { ident := "lhs", kind := .cat (.atom .none ⟨"Test", "Expr"⟩) }, - { ident := "rhs", kind := .cat (.atom .none ⟨"Test", "Expr"⟩) } - ] - category := ⟨"Test", "Expr"⟩ - syntaxDef := .std #[] 0 - } - ] - } - let files := (generateDialect testDialect "com.test").toOption.get! - -- One category file containing the interface and both records - assert! files.categories.size = 1 - assert! files.categories.any (fun c => check c.2 "sealed interface Expr") - assert! files.categories.any (fun c => check c.2 "record Literal") - assert! files.categories.any (fun c => check c.2 "record Add") - -- Records have toIon methods - assert! files.categories.any (fun c => check c.2 "toIon") - pure () - --- Test 2: Reserved word escaping for fields -#eval do - let testDialect : StrataDDM.Dialect := { - name := "Reserved" - imports := #[] - declarations := #[ - .syncat { name := "Stmt", argNames := #[] }, - .op { - name := "int" - argDecls := .ofArray #[ - { ident := "public", kind := .cat (.atom .none ⟨"Init", "Ident"⟩) } - ] - category := ⟨"Reserved", "Stmt"⟩ - syntaxDef := .std #[] 0 - } - ] - } - let files := (generateDialect testDialect "com.test").toOption.get! - -- Single-op category where op name "int" (PascalCase "Int") doesn't match category "Stmt" - assert! files.categories.any (fun c => check c.2 "record Int") - assert! files.categories.any (fun c => check c.2 "public_") - pure () - --- Test 3: Name collision (single-op, operator name matches category name) → uses "Of" -#eval do - let testDialect : StrataDDM.Dialect := { - name := "Collision" - imports := #[] - declarations := #[ - .syncat { name := "expr", argNames := #[] }, - .op { - name := "Expr" - argDecls := .ofArray #[] - category := ⟨"Collision", "expr"⟩ - syntaxDef := .std #[] 0 - } - ] - } - let files := (generateDialect testDialect "com.test").toOption.get! - -- Single-op category: operator gets "Of" since it collides with category name - assert! files.categories.any (fun c => check c.2 "sealed interface Expr") - assert! files.categories.any (fun c => check c.2 "record Of") - pure () - --- Test 4: Duplicate operator names across categories — nested so no global collision -#eval do - let testDialect : StrataDDM.Dialect := { - name := "Dup" - imports := #[] - declarations := #[ - .syncat { name := "A", argNames := #[] }, - .syncat { name := "B", argNames := #[] }, - .op { name := "foo", argDecls := .ofArray #[], category := ⟨"Dup", "A"⟩, syntaxDef := .std #[] 0 }, - .op { name := "foo", argDecls := .ofArray #[], category := ⟨"Dup", "B"⟩, syntaxDef := .std #[] 0 }, - .op { name := "class", argDecls := .ofArray #[], category := ⟨"Dup", "A"⟩, syntaxDef := .std #[] 0 }, - .op { name := "class_", argDecls := .ofArray #[], category := ⟨"Dup", "B"⟩, syntaxDef := .std #[] 0 } - ] - } - let files := (generateDialect testDialect "com.test").toOption.get! - -- Both categories should have their operators as nested records - assert! files.categories.size = 2 - -- A has Foo and Class (class is reserved but Class after PascalCase is not) - assert! files.categories.any (fun c => check c.2 "record Foo" && check c.2 "interface A") - assert! files.categories.any (fun c => check c.2 "record Class" && check c.2 "interface A") - pure () - --- Test 5: Category name collides with base class -#eval do - let testDialect : StrataDDM.Dialect := { - name := "Base" - imports := #[] - declarations := #[ - .syncat { name := "Node", argNames := #[] }, - .op { name := "leaf", argDecls := .ofArray #[], category := ⟨"Base", "Node"⟩, syntaxDef := .std #[] 0 } - ] - } - let files := (generateDialect testDialect "com.test").toOption.get! - -- Category "Node" collides with base class, should be disambiguated - let allNames := #["Node.java", "SourceRange.java"] ++ files.categories.map Prod.fst - assert! allNames.toList.eraseDups.length == allNames.size - pure () - --- Test 6: Snake_case to PascalCase conversion -#eval do - let testDialect : StrataDDM.Dialect := { - name := "Snake" - imports := #[] - declarations := #[ - .syncat { name := "my_category", argNames := #[] }, - .op { - name := "my_operator" - argDecls := .ofArray #[] - category := ⟨"Snake", "my_category"⟩ - syntaxDef := .std #[] 0 - } - ] - } - let files := (generateDialect testDialect "com.test").toOption.get! - assert! files.categories.any (fun c => c.1 == "MyCategory.java") - assert! files.categories.any (fun c => check c.2 "record MyOperator") - pure () - --- Test 7: All DDM types map correctly -#eval! do - let testDialect : StrataDDM.Dialect := { - name := "Types" - imports := #[] - declarations := #[ - .syncat { name := "Node", argNames := #[] }, - .op { - name := "allTypes" - argDecls := .ofArray #[ - { ident := "ident", kind := .cat (.atom .none ⟨"Init", "Ident"⟩) }, - { ident := "num", kind := .cat (.atom .none ⟨"Init", "Num"⟩) }, - { ident := "dec", kind := .cat (.atom .none ⟨"Init", "Decimal"⟩) }, - { ident := "str", kind := .cat (.atom .none ⟨"Init", "Str"⟩) }, - { ident := "b", kind := .cat (.atom .none ⟨"Init", "Bool"⟩) }, - { ident := "bytes", kind := .cat (.atom .none ⟨"Init", "ByteArray"⟩) }, - { ident := "opt", kind := .cat ⟨.none, ⟨"Init", "Option"⟩, #[.atom .none ⟨"Init", "Num"⟩]⟩ }, - { ident := "seq", kind := .cat ⟨.none, ⟨"Init", "Seq"⟩, #[.atom .none ⟨"Init", "Ident"⟩]⟩ } - ] - category := ⟨"Types", "Node"⟩ - syntaxDef := .std #[] 0 - } - ] - } - let files := (generateDialect testDialect "com.test").toOption.get! - let catContent := files.categories[0]!.2 - assert! check catContent "java.lang.String ident" - assert! check catContent "java.math.BigInteger num" - assert! check catContent "java.math.BigDecimal dec" - assert! check catContent "java.lang.String str" - assert! check catContent "boolean b" - assert! check catContent "byte[] bytes" - assert! check catContent "java.util.Optional opt" - assert! check catContent "java.util.List seq" - -- Verify toIon uses correct serializers for Ident vs Str - assert! check catContent "serializeIdent(ident())" - assert! check catContent "serializeStrlit(str())" - assert! check catContent "serializeNum(num())" - assert! check catContent "serializeBool(b())" - pure () - --- Test 8: FQN usage (no imports that could conflict) -#eval! do - let testDialect : StrataDDM.Dialect := { - name := "FQN" - imports := #[] - declarations := #[ - .syncat { name := "Node", argNames := #[] }, - .op { - name := "test" - argDecls := .ofArray #[] - category := ⟨"FQN", "Node"⟩ - syntaxDef := .std #[] 0 - } - ] - } - let files := (generateDialect testDialect "com.test").toOption.get! - let catContent := files.categories[0]!.2 - assert! check catContent "java.lang.String operationName()" - pure () - --- Test 9: Stub interfaces for referenced-but-empty categories -#eval do - let testDialect : StrataDDM.Dialect := { - name := "Stub" - imports := #[] - declarations := #[ - .syncat { name := "Stmt", argNames := #[] }, - .op { - name := "eval" - argDecls := .ofArray #[ - { ident := "e", kind := .cat (.atom .none ⟨"Init", "Expr"⟩) } - ] - category := ⟨"Stub", "Stmt"⟩ - syntaxDef := .std #[] 0 - } - ] - } - let files := (generateDialect testDialect "com.test").toOption.get! - assert! files.categories.any (fun c => check c.2 "sealed interface Stmt") - assert! files.stubs.any (fun s => check s.2 "non-sealed interface Expr") - pure () - --- Test 10: Core dialect returns error (has type/function declarations not yet supported) -elab "#testCoreError" : command => do - let env ← Lean.getEnv - let state := StrataDDM.dialectExt.getState env - let some core := state.loaded.dialects["Core"]? - | Lean.logError "Core dialect not found"; return - match generateDialect core "com.strata.core" with - | .error msg => - if !(check msg "type declaration" || check msg "function declaration") then - Lean.logError s!"Expected error about type/function declaration, got: {msg}" - | .ok _ => Lean.logError "Expected error for Core dialect" - -#testCoreError - --- Test 11: Cross-dialect name collision (A.Num vs B.Num) -#eval do - let testDialect : StrataDDM.Dialect := { - name := "A" - imports := #[] - declarations := #[ - .syncat { name := "Num", argNames := #[] }, - .op { - name := "lit" - argDecls := .ofArray #[ - { ident := "a", kind := .cat (.atom .none ⟨"A", "Num"⟩) }, - { ident := "b", kind := .cat (.atom .none ⟨"B", "Num"⟩) } - ] - category := ⟨"A", "Num"⟩ - syntaxDef := .std #[] 0 - } - ] - } - let files := (generateDialect testDialect "com.test").toOption.get! - -- Category for A.Num + stub for B.Num - assert! files.categories.size = 1 - assert! files.stubs.size = 1 - let allNames := files.categories.map Prod.fst ++ files.stubs.map Prod.fst - assert! allNames.any (fun n => (n.splitOn "A").length > 1) - assert! allNames.any (fun n => (n.splitOn "B").length > 1) - pure () - --- Test 12: Generated Java compiles (requires javac) -#load_dialect "StrataTestExtra/Languages/Java/testdata/Simple.dialect.st" - +-- Test types +structure Point where + x : Nat + y : Nat +deriving Repr, BEq + +inductive Color where + | red + | green + | blue +deriving Repr, BEq + +inductive Shape where + | circle (radius : Nat) + | rect (width : Nat) (height : Nat) +deriving Repr, BEq + +structure Person where + name : String + age : Nat + active : Bool +deriving Repr, BEq + +structure Line where + start : Point + stop : Point +deriving Repr, BEq + +inductive Tree where + | leaf (value : Nat) + | node (left : Tree) (right : Tree) +deriving Repr, BEq + +-- Test 1: Structure generates a record with field-name-keyed Ion struct +elab "#testPoint" : command => do + let files := getIonSerializer% Point "com.test" + let some (_, content) := files.files.find? (·.1 == "Point.java") + | Lean.logError "Expected Point.java"; return + if !check content "public record Point(" then Lean.logError "Missing record Point"; return + if !check content "long x" then Lean.logError "Missing long x"; return + if !check content "long y" then Lean.logError "Missing long y"; return + if !check content "toIon" then Lean.logError "Missing toIon"; return + if !check content "s.put(\"x\"" then Lean.logError "Missing s.put(\"x\""; return + if !check content "s.put(\"y\"" then Lean.logError "Missing s.put(\"y\""; return + +#testPoint + +-- Test 2: Multi-constructor inductive generates sealed interface with records +elab "#testColor" : command => do + let files := getIonSerializer% Color "com.test" + let some (_, content) := files.files.find? (·.1 == "Color.java") + | Lean.logError "Expected Color.java"; return + if !check content "sealed interface Color" then Lean.logError "Missing sealed interface"; return + if !check content "record Red" then Lean.logError "Missing record Red"; return + if !check content "record Green" then Lean.logError "Missing record Green"; return + if !check content "record Blue" then Lean.logError "Missing record Blue"; return + if !check content "newSymbol(\"red\")" then Lean.logError "Missing newSymbol red"; return + if !check content "newSymbol(\"green\")" then Lean.logError "Missing newSymbol green"; return + if !check content "newSymbol(\"blue\")" then Lean.logError "Missing newSymbol blue"; return + +#testColor + +-- Test 3: Multi-constructor inductive with fields +elab "#testShape" : command => do + let files := getIonSerializer% Shape "com.test" + let some (_, content) := files.files.find? (·.1 == "Shape.java") + | Lean.logError "Expected Shape.java"; return + if !check content "sealed interface Shape" then Lean.logError "Missing sealed interface"; return + if !check content "record Circle(long radius)" then Lean.logError "Missing Circle record"; return + if !check content "record Rect(long width, long height)" then Lean.logError "Missing Rect record"; return + if !check content "newSymbol(\"circle\")" then Lean.logError "Missing newSymbol circle"; return + if !check content "newSymbol(\"rect\")" then Lean.logError "Missing newSymbol rect"; return + +#testShape + +-- Test 4: Structure with String and Bool fields +elab "#testPerson" : command => do + let files := getIonSerializer% Person "com.test" + let some (_, content) := files.files.find? (·.1 == "Person.java") + | Lean.logError "Expected Person.java"; return + if !check content "java.lang.String name" then Lean.logError "Missing String name"; return + if !check content "long age" then Lean.logError "Missing long age"; return + if !check content "boolean active" then Lean.logError "Missing boolean active"; return + if !check content "newString(name())" then Lean.logError "Missing newString"; return + if !check content "newInt(age())" then Lean.logError "Missing newInt"; return + if !check content "newBool(active())" then Lean.logError "Missing newBool"; return + +#testPerson + +-- Test 5: Nested structure generates files for both types +elab "#testLine" : command => do + let files := getIonSerializer% Line "com.test" + if !files.files.any (fun f => f.1 == "Line.java") then Lean.logError "Missing Line.java"; return + if !files.files.any (fun f => f.1 == "Point.java") then Lean.logError "Missing Point.java"; return + for (fname, content) in files.files do + if fname == "Line.java" then + if !check content "Point start" then Lean.logError "Missing Point start"; return + if !check content "Point stop" then Lean.logError "Missing Point stop"; return + if !check content "start().toIon(ion)" then Lean.logError "Missing start().toIon"; return + if !check content "stop().toIon(ion)" then Lean.logError "Missing stop().toIon"; return + +#testLine + +-- Test 6: Recursive type generates files +elab "#testTree" : command => do + let files := getIonSerializer% Tree "com.test" + let some (_, content) := files.files.find? (·.1 == "Tree.java") + | Lean.logError "Expected Tree.java"; return + if !check content "sealed interface Tree" then Lean.logError "Missing sealed interface"; return + if !check content "record Leaf(long value)" then Lean.logError "Missing Leaf record"; return + if !check content "record Node(Tree left, Tree right)" then Lean.logError "Missing Node record"; return + if !check content "left().toIon(ion)" then Lean.logError "Missing left().toIon"; return + if !check content "right().toIon(ion)" then Lean.logError "Missing right().toIon"; return + +#testTree + +-- Test 7: Package name appears in generated files +elab "#testPackage" : command => do + let files := getIonSerializer% Point "com.example.mypackage" + let (_, content) := files.files[0]! + if !check content "package com.example.mypackage;" then Lean.logError "Missing package"; return + +#testPackage + +-- Test 8: writeJavaFiles writes to correct directory +elab "#testWriteFiles" : command => do + let dir : System.FilePath := "/tmp/strata-java-test-write" + if ← dir.pathExists then IO.FS.removeDirAll dir + let files : GeneratedFiles := { files := #[("Test.java", "package com.test;\npublic record Test() {}\n")] } + writeJavaFiles dir "com.test" files + let path := dir / "com" / "test" / "Test.java" + if !(← path.pathExists) then + Lean.logError "Expected file not found" + IO.FS.removeDirAll dir + +#testWriteFiles + +-- Test 9: Generated Java compiles (requires javac + ion-java jar) elab "#testCompile" : command => do let javacCheck ← IO.Process.output { cmd := "javac", args := #["--version"] } if javacCheck.exitCode != 0 then - Lean.logError "Test 12 failed: javac not found" + Lean.logWarning "Test skipped: javac not found" return - let env ← Lean.getEnv - let state := StrataDDM.dialectExt.getState env - let some simple := state.loaded.dialects["Simple"]? - | Lean.logError "Simple dialect not found"; return - let files := (generateDialect simple "com.test").toOption.get! - let jarPath := "StrataTestExtra/Languages/Java/testdata/ion-java-1.11.11.jar" if !(← System.FilePath.pathExists jarPath) then - Lean.logError s!"Test 12 failed: ion-java jar not found at {jarPath}" + Lean.logWarning s!"Test skipped: ion-java jar not found at {jarPath}" return - IO.FS.withTempDir fun dir => do - writeJavaFiles dir "com.test" files + let dir : System.FilePath := "/tmp/strata-java-test-compile" + if ← dir.pathExists then IO.FS.removeDirAll dir - let fileNames := #["SourceRange.java", "Node.java", "IonSerializer.java", files.builders.1] - ++ files.categories.map Prod.fst - ++ files.stubs.map Prod.fst - let pkgDir := (dir / "com" / "test").toString - let filePaths := fileNames.map fun f => pkgDir ++ "/" ++ f + let shapeFiles := getIonSerializer% Shape "com.test" + let lineFiles := getIonSerializer% Line "com.test" - let result ← IO.Process.output { - cmd := "javac" - args := #["-cp", jarPath] ++ filePaths - } + let mut allFiles : Std.HashMap String String := {} + for (name, content) in shapeFiles.files do allFiles := allFiles.insert name content + for (name, content) in lineFiles.files do allFiles := allFiles.insert name content + + let pkgDir := dir / "com" / "test" + IO.FS.createDirAll pkgDir + let mut filePaths : Array String := #[] + for (name, content) in allFiles do + let path := pkgDir / name + IO.FS.writeFile path content + filePaths := filePaths.push path.toString + + let result ← IO.Process.output { + cmd := "javac" + args := #["-cp", s!"{jarPath}:{dir}"] ++ filePaths + } + + if result.exitCode != 0 then + Lean.throwError s!"javac failed:\n{result.stderr}" - if result.exitCode != 0 then - Lean.throwError s!"javac failed:\n{result.stderr}" + IO.FS.removeDirAll dir #testCompile --- Test 13: Roundtrip - verify Lean can read Java-generated Ion --- Depends on testdata/comprehensive.ion +-- Test 10: Roundtrip - Java serializes Ion, Lean deserializes it elab "#testRoundtrip" : command => do - let env ← Lean.getEnv - let state := StrataDDM.dialectExt.getState env - let some simple := state.loaded.dialects["Simple"]? - | Lean.logError "Simple dialect not found"; return - let dm := StrataDDM.DialectMap.ofList! [StrataDDM.initDialect, simple] - let ionBytes ← IO.FS.readBinFile "StrataTestExtra/Languages/Java/testdata/comprehensive.ion" - match StrataDDM.Program.fromIon dm "Simple" ionBytes with - | .error e => Lean.logError s!"Roundtrip test failed: {e}" - | .ok prog => - if prog.commands.size != 1 then Lean.logError "Expected 1 command"; return - let cmd := prog.commands[0]! - if cmd.name != (⟨"Simple", "block"⟩ : StrataDDM.QualifiedIdent) then Lean.logError "Expected block command"; return - if let .seq _ _ stmts := cmd.args[0]! then - if stmts.size != 4 then Lean.logError s!"Expected 4 statements, got {stmts.size}" - -- Verify print's msg arg is strlit (not ident) — catches Init.Str serialization bug - if stmts.size < 2 then Lean.logError "Expected at least 2 statements"; return - match stmts[1]! with - | .op op => - if op.name != ⟨"Simple", "print"⟩ then Lean.logError s!"Expected print, got {op.name}" - else match op.args[0]! with - | .strlit _ s => if s != "hello" then Lean.logError s!"Expected 'hello', got '{s}'" - | .ident _ s => Lean.logError s!"print msg is ident '{s}', expected strlit" - | _ => Lean.logError "Expected strlit arg for print" - | _ => Lean.logError "Expected op for stmts[1]" - else Lean.logError "Expected seq argument" + let javacCheck ← IO.Process.output { cmd := "javac", args := #["--version"] } + if javacCheck.exitCode != 0 then + Lean.logWarning "Roundtrip test skipped: javac not found" + return -#testRoundtrip + let jarPath := "StrataTestExtra/Languages/Java/testdata/ion-java-1.11.11.jar" + if !(← System.FilePath.pathExists jarPath) then + Lean.logWarning s!"Roundtrip test skipped: ion-java jar not found at {jarPath}" + return --- Test 14: Roundtrip with fromIonFiles - verify Lean can read Java-generated Ion array format --- Depends on testdata/comprehensive-files.ion -elab "#testRoundtripFiles" : command => do - let env ← Lean.getEnv - let state := StrataDDM.dialectExt.getState env - let some simple := state.loaded.dialects["Simple"]? - | Lean.logError "Simple dialect not found"; return - let dm := StrataDDM.DialectMap.ofList! [StrataDDM.initDialect, simple] - let ionBytes ← IO.FS.readBinFile "StrataTestExtra/Languages/Java/testdata/comprehensive-files.ion" - match StrataDDM.Program.filesFromIon dm ionBytes with - | .error e => Lean.logError s!"Roundtrip files test failed: {e}" - | .ok files => - if files.length != 2 then - Lean.logError s!"Expected 2 files, got {files.length}" - return - - let file1 := files[0]! - if file1.filePath != "file1.st" then - Lean.logError s!"File 1: Expected path 'file1.st', got '{file1.filePath}'" - return - if file1.program.commands.size != 1 then - Lean.logError s!"File 1: Expected 1 command, got {file1.program.commands.size}" - return - let cmd1 := file1.program.commands[0]! - if cmd1.name != (⟨"Simple", "block"⟩ : StrataDDM.QualifiedIdent) then - Lean.logError "File 1: Expected block command"; return - if let .seq _ _ stmts := cmd1.args[0]! then - if stmts.size != 2 then - Lean.logError s!"File 1: Expected 2 statements, got {stmts.size}" - return - else - Lean.logError "File 1: Expected seq argument"; return - - let file2 := files[1]! - if file2.filePath != "file2.st" then - Lean.logError s!"File 2: Expected path 'file2.st', got '{file2.filePath}'" - return - if file2.program.commands.size != 1 then - Lean.logError s!"File 2: Expected 1 command, got {file2.program.commands.size}" - return - let cmd2 := file2.program.commands[0]! - if cmd2.name != (⟨"Simple", "block"⟩ : StrataDDM.QualifiedIdent) then - Lean.logError "File 2: Expected block command"; return - if let .seq _ _ stmts := cmd2.args[0]! then - if stmts.size != 3 then - Lean.logError s!"File 2: Expected 3 statements, got {stmts.size}" - return - else - Lean.logError "File 2: Expected seq argument"; return - -#testRoundtripFiles - --- Test 15: javaGen works on preloaded dialects via CLI -elab "#testJavaGenPreloaded" : command => do - IO.FS.withTempDir fun parentDir => do - let dir := parentDir / "javagen-output" - let result ← IO.Process.output { - cmd := "lake" - args := #["exe", "strata", "javaGen", "Laurel", "com.test.laurel", dir.toString] - cwd := "StrataCLI" + let dir : System.FilePath := "/tmp/strata-java-roundtrip" + if ← dir.pathExists then IO.FS.removeDirAll dir + + let pointFiles := getIonSerializer% Point "com.test" + let pkgDir := dir / "com" / "test" + IO.FS.createDirAll pkgDir + for (name, content) in pointFiles.files do + IO.FS.writeFile (pkgDir / name) content + + let driverContent := " +import com.test.*; +import com.amazon.ion.*; +import com.amazon.ion.system.*; +import java.io.*; + +public class RoundtripTest { + public static void main(String[] args) throws Exception { + var ionSystem = IonSystemBuilder.standard().build(); + var point = new Point(42, 7); + var ionValue = point.toIon(ionSystem); + + try (var out = new FileOutputStream(args[0])) { + var writer = IonBinaryWriterBuilder.standard().build(out); + ionValue.writeTo(writer); + writer.close(); + } } - if result.exitCode != 0 then - Lean.throwError s!"javaGen on preloaded Laurel dialect failed:\n{result.stdout}\n{result.stderr}" - -- Verify some expected files exist (now one file per category) - let pkgDir := (dir / "com" / "test" / "laurel").toString - for expected in #["Node.java", "StmtExpr.java", "Procedure.java", "Parameter.java"] do - if !(← System.FilePath.pathExists (pkgDir ++ "/" ++ expected)) then - Lean.throwError s!"Expected file {expected} not found in {pkgDir}" +} +" + IO.FS.writeFile (dir / "RoundtripTest.java") driverContent -#testJavaGenPreloaded + let mut javaPaths : Array String := #[(dir / "RoundtripTest.java").toString] + for (name, _) in pointFiles.files do + javaPaths := javaPaths.push (pkgDir / name).toString + + let compileResult ← IO.Process.output { + cmd := "javac" + args := #["-cp", s!"{jarPath}:{dir}"] ++ javaPaths + } + if compileResult.exitCode != 0 then + Lean.logError s!"Roundtrip compile failed:\n{compileResult.stderr}" + IO.FS.removeDirAll dir + return + + let ionFile := dir / "point.ion" + let runResult ← IO.Process.output { + cmd := "java" + args := #["-cp", s!"{jarPath}:{dir}", "RoundtripTest", ionFile.toString] + } + if runResult.exitCode != 0 then + Lean.logError s!"Roundtrip run failed:\n{runResult.stderr}" + IO.FS.removeDirAll dir + return + + let ionBytes ← IO.FS.readBinFile ionFile + let deserializePoint : ByteArray → Except Std.Format Point := getIonDeserializer% Point + match deserializePoint ionBytes with + | .ok point => + if point.x != 42 || point.y != 7 then + Lean.logError s!"Roundtrip mismatch: expected (42, 7), got ({point.x}, {point.y})" + | .error e => + Lean.logError s!"Roundtrip deserialization failed: {e}" + + IO.FS.removeDirAll dir + +#testRoundtrip -end StrataDDM.Java.Test +end Strata.Java.Test diff --git a/StrataTestExtra/Languages/Java/regenerate-testdata.sh b/StrataTestExtra/Languages/Java/regenerate-testdata.sh deleted file mode 100755 index 1e7eda03dd..0000000000 --- a/StrataTestExtra/Languages/Java/regenerate-testdata.sh +++ /dev/null @@ -1,34 +0,0 @@ -#!/bin/bash -# Regenerate Java roundtrip test data -set -e -cd "$(dirname "$0")" - -STRATA_ROOT="$(cd ../../.. && pwd)" -TESTDATA="testdata" -GEN_DIR="testdata/generated" -JAR="testdata/ion-java-1.11.11.jar" - -# Download ion-java if needed -if [ ! -f "$JAR" ]; then - echo "=== Downloading ion-java ===" - curl -sLo "$JAR" "https://github.com/amazon-ion/ion-java/releases/download/v1.11.11/ion-java-1.11.11.jar" -fi - -echo "=== Generating Java classes from dialect ===" -(cd "$STRATA_ROOT" && ./StrataCLI/.lake/build/bin/strata javaGen "$STRATA_ROOT/StrataTestExtra/Languages/Java/$TESTDATA/Simple.dialect.st" com.strata.simple "$STRATA_ROOT/StrataTestExtra/Languages/Java/$GEN_DIR") - -echo "=== Compiling Java ===" -javac -cp "$JAR" $GEN_DIR/com/strata/simple/*.java $TESTDATA/GenerateTestData.java - -echo "=== Generating test data ===" -java -cp "$JAR:$GEN_DIR:$TESTDATA" GenerateTestData "$TESTDATA/comprehensive.ion" "$TESTDATA/comprehensive-files.ion" - -echo "=== Cleaning up ===" -rm -rf "$GEN_DIR" -rm -f $TESTDATA/*.class - -echo "=== Verifying with Lean ===" -(cd "$STRATA_ROOT" && ./StrataCLI/.lake/build/bin/strata print --include "$STRATA_ROOT/StrataTestExtra/Languages/Java/$TESTDATA" "$STRATA_ROOT/StrataTestExtra/Languages/Java/$TESTDATA/comprehensive.ion" 2>&1 | tail -1) - -echo "" -echo "Done! Regenerated $TESTDATA/comprehensive.ion and $TESTDATA/comprehensive-files.ion" diff --git a/StrataTestExtra/Languages/Java/testdata/GenerateTestData.java b/StrataTestExtra/Languages/Java/testdata/GenerateTestData.java deleted file mode 100644 index 395ac4c74c..0000000000 --- a/StrataTestExtra/Languages/Java/testdata/GenerateTestData.java +++ /dev/null @@ -1,87 +0,0 @@ -import static com.strata.simple.Simple.*; -import com.strata.simple.*; -import com.amazon.ion.*; -import com.amazon.ion.system.*; -import java.io.*; -import java.util.*; - -/** Generates comprehensive.ion covering all DDM types. */ -public class GenerateTestData { - public static void main(String[] args) throws Exception { - var ion = IonSystemBuilder.standard().build(); - var serializer = new IonSerializer(ion); - generateSingleProgram(ion, serializer, args[0]); - - if (args.length > 1) { - generateMultipleFiles(ion, serializer, args[1]); - } - } - - private static void generateSingleProgram(IonSystem ion, IonSerializer serializer, String outPath) throws Exception { - - // AST covering: Num, Str, Ident, Bool, Decimal, ByteArray, Option, Seq, nesting - Node ast = block(List.of( - assign("x", add(num(1), neg(num(2)))), - print("hello"), - ifStmt(true, data(new byte[]{0x01, (byte)0xFF}), Optional.of(decimal(3.14))), - ifStmt(false, block(List.of()), Optional.empty()))); - - IonList program = ion.newEmptyList(); - IonSexp header = ion.newEmptySexp(); - header.add(ion.newSymbol("program")); - header.add(ion.newString("Simple")); - program.add(header); - program.add(serializer.serializeCommand(ast)); - - try (var out = new FileOutputStream(outPath)) { - var writer = IonBinaryWriterBuilder.standard().build(out); - program.writeTo(writer); - writer.close(); - } - System.out.println("Generated: " + outPath); - } - - private static void generateMultipleFiles(IonSystem ion, IonSerializer serializer, String outPath) throws Exception { - Node ast1 = block(List.of( - assign("x", num(42)), - print("first file"))); - - IonList program1 = ion.newEmptyList(); - IonSexp header1 = ion.newEmptySexp(); - header1.add(ion.newSymbol("program")); - header1.add(ion.newString("Simple")); - program1.add(header1); - program1.add(serializer.serializeCommand(ast1)); - - Node ast2 = block(List.of( - assign("y", add(num(1), num(2))), - print("second file"), - ifStmt(true, block(List.of()), Optional.empty()))); - - IonList program2 = ion.newEmptyList(); - IonSexp header2 = ion.newEmptySexp(); - header2.add(ion.newSymbol("program")); - header2.add(ion.newString("Simple")); - program2.add(header2); - program2.add(serializer.serializeCommand(ast2)); - - IonList files = ion.newEmptyList(); - - IonStruct file1 = ion.newEmptyStruct(); - file1.put("filePath", ion.newString("file1.st")); - file1.put("program", program1); - files.add(file1); - - IonStruct file2 = ion.newEmptyStruct(); - file2.put("filePath", ion.newString("file2.st")); - file2.put("program", program2); - files.add(file2); - - try (var out = new FileOutputStream(outPath)) { - var writer = IonBinaryWriterBuilder.standard().build(out); - files.writeTo(writer); - writer.close(); - } - System.out.println("Generated: " + outPath); - } -} diff --git a/StrataTestExtra/Languages/Java/testdata/README.md b/StrataTestExtra/Languages/Java/testdata/README.md index 35dc36f4e2..96f21188a1 100644 --- a/StrataTestExtra/Languages/Java/testdata/README.md +++ b/StrataTestExtra/Languages/Java/testdata/README.md @@ -1,27 +1,19 @@ # Java Roundtrip Test Data -`comprehensive.ion` is a Java-generated Ion file that tests all DDM types. +The Java code generator uses the `getIonSerializer%` elaborator to generate +Java source files from Lean types. The generated Java code produces Ion data +in the same format that `getIonDeserializer%` expects. -## To regenerate +## Test approach -From this directory: +The roundtrip test in `TestGen.lean`: +1. Generates Java source files for Lean types using `getIonSerializer%` +2. Compiles the Java code with `javac` +3. Runs the Java code to produce Ion binary data +4. Deserializes the Ion data back into Lean values using `getIonDeserializer%` +5. Verifies the round-tripped values match the originals -```bash -./regenerate-testdata.sh -``` +## Requirements -This will: -1. Generate Java classes from `Simple.dialect.st` -2. Build and run `GenerateTestData.java` to produce `comprehensive.ion` -3. Clean up generated classes -4. Verify the output with Lean - -## What's tested - -The test file covers all DDM types in a single AST: -- Num, Str, Ident -- Bool (true and false) -- Decimal, ByteArray -- Option (some and none) -- Seq (with items and empty) -- Nested operations (3 levels deep) +- `javac` (Java 17+) +- `ion-java-1.11.11.jar` in this directory (downloaded automatically by CI) diff --git a/StrataTestExtra/Languages/Java/testdata/Simple.dialect.st b/StrataTestExtra/Languages/Java/testdata/Simple.dialect.st deleted file mode 100644 index b4d3e7ea2c..0000000000 --- a/StrataTestExtra/Languages/Java/testdata/Simple.dialect.st +++ /dev/null @@ -1,15 +0,0 @@ -dialect Simple; - -category Expr; -op num (value : Num) : Simple.Expr => value; -op add (left : Simple.Expr, right : Simple.Expr) : Simple.Expr => left "+" right; -op neg (inner : Simple.Expr) : Simple.Expr => "-" inner; - -category Stmt; -op print (msg : Str) : Simple.Stmt => "print" msg; -op assign (name : Ident, value : Simple.Expr) : Simple.Stmt => name ":=" value; -op block (stmts : Seq Simple.Stmt) : Simple.Stmt => "{" stmts "}"; -op ifStmt (cond : Bool, thenBranch : Simple.Stmt, elseBranch : Option Simple.Stmt) : Simple.Stmt => - "if" cond "then" thenBranch elseBranch; -op data (bytes : ByteArray) : Simple.Stmt => "data" bytes; -op decimal (value : Decimal) : Simple.Stmt => "decimal" value; diff --git a/StrataTestExtra/Languages/Java/testdata/comprehensive-files.ion b/StrataTestExtra/Languages/Java/testdata/comprehensive-files.ion deleted file mode 100644 index c688b9e87c..0000000000 Binary files a/StrataTestExtra/Languages/Java/testdata/comprehensive-files.ion and /dev/null differ diff --git a/StrataTestExtra/Languages/Java/testdata/comprehensive.ion b/StrataTestExtra/Languages/Java/testdata/comprehensive.ion deleted file mode 100644 index 202ea8bd93..0000000000 Binary files a/StrataTestExtra/Languages/Java/testdata/comprehensive.ion and /dev/null differ diff --git a/lakefile.toml b/lakefile.toml index b0837ea7ed..d88577051b 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -48,3 +48,7 @@ root = "Scripts.CheckImports" name = "ImportStats" root = "Scripts.ImportStats" + +[[lean_exe]] +name = "laurelJavaGen" +root = "Scripts.LaurelJavaGen"