Generate per-file top-level Java class names instead of hardcoded Main - #25
Merged
Conversation
Every generated .java file declared `class Main`, so compiling multiple extracted files together with `javac *.java` always failed with a duplicate-class error. The class name is now derived from the module id (the same one file_naming already computes), threaded from preamble into pp_struct via a ref, mirroring the existing fix_arities side channel. mono_filename's Java branch now derives its id from the target filename the same way Haskell already does, since previously it always forced the literal "Main" id for Java regardless of the requested filename. Updates all Java extraction test fixtures accordingly and adds a run-case.sh step that compiles a case's generated files together, which would have caught this bug. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Java's top-level class name needed the module id, but the shared pp_struct signature carried none, so it was smuggled in via a top_class_name ref written by preamble and read by pp_struct (mirroring fix_arities). Add Id.t as an explicit pp_struct argument instead: OCaml/Haskell/JSON/Scheme just ignore it, and Java derives the class name directly from it, removing the ordering dependency on preamble running first. Pure refactor: all java-extraction test fixtures still match byte for byte. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
hiroshi-cl
changed the title
hiroshi-cl
commented
Aug 5, 2026
Comment on lines
+537
to
+544
| match lang () with | ||
| | Haskell | Java -> | ||
| (* These backends name a top-level container (module / class) | ||
| after the file, so the file name must be a valid identifier. *) | ||
| (try Id.of_string (Filename.basename f) | ||
| with UserError _ -> | ||
| user_err Pp.(str "Extraction: provided filename is not a valid identifier")) | ||
| | Ocaml | Scheme | JSON -> default_id |
Author
There was a problem hiding this comment.
HaskellだけでなくJavaもdefault_idじゃなくてfilenameを使うようにする
hiroshi-cl
commented
Aug 5, 2026
| 's -> Id.t -> Pp.t option -> DirPath.Set.t -> unsafe_needs -> | ||
| Pp.t; | ||
| pp_struct : 's -> ml_structure -> Pp.t; | ||
| pp_struct : 's -> Id.t -> ml_structure -> Pp.t; |
Author
There was a problem hiding this comment.
pp_stuctを拡張してId.tを渡すようにする
haskellではpreambleとして処理しているがjavaではpp_structで出力する
これにより他の言語への抽出コードも変更が出ている
hiroshi-cl
marked this pull request as ready for review
August 5, 2026 16:19
cedretaber
reviewed
Aug 6, 2026
Comment on lines
+47
to
+48
| if not valid then | ||
| user_err Pp.(str "Extraction: " ++ Id.print id ++ |
There was a problem hiding this comment.
📝
invalid な名前の場合、名前を変えるのではなくエラーにする。
cedretaber
reviewed
Aug 6, 2026
| not (String.is_empty s) | ||
| && is_java_ident_start s.[0] | ||
| && String.for_all is_java_ident_part s | ||
| && not (Id.Set.mem id keywords) |
There was a problem hiding this comment.
nits な指摘
- Rocq コード内にファイル名と同じ型が定義されていると、同じ名前のクラスが2つ出てきてコンパイルが落ちそう
true / false / nullは Java のキーワードではなくリテラルなので valid な扱いとなり、しかしclass trueは javac がエラーを出す。varなども同様
There was a problem hiding this comment.
Java keyword じゃないやつも必要に応じて keywords の中に突っ込んでるから（ let とか error とか）、このへんの語も全部入れてしまっても良いかも？
Author
There was a problem hiding this comment.
確かに JLS §3.8 で reserved 以外にもBooleanLiteral (true, false), NullLiteral (null) も識別子として使えないことになってるので入れても良さそう
一方以下5つは TypeIdentifier から除外されてるけど変数とかには使えることになってそうなのでここで除外はするけどkeywordsには入れないほうが良さそう 🤔
permits
record
sealed
var
yield
cedretaber
approved these changes
Aug 6, 2026
cedretaber
left a comment
cedretaber
left a comment
There was a problem hiding this comment.
2点指摘しましたが、概ね良さそうです 🙏
（ Java のキーワードとそれ以外のリテラルとか、 var みたいな後から入ったのがどういう扱いなのかとか、よく分っていないのですが……。）
…ction true/false/null are excluded from Identifier per JLS 3.8, and permits/record/sealed/var/yield are excluded from TypeIdentifier specifically, so add them to keywords and a new restricted_type_identifiers set used by java_class_name. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
hiroshi-cl
commented
Aug 13, 2026
Comment on lines
+29
to
+31
| (* not keywords, but JLS 3.8 excludes BooleanLiteral and NullLiteral | ||
| from Identifier as well *) | ||
| "true"; "false"; "null"; |
hiroshi-cl
commented
Aug 13, 2026
Comment on lines
+42
to
+49
| (* JLS 3.8 defines a class name as a TypeIdentifier: an Identifier that is not | ||
| one of these five contextual keywords. They are deliberately kept out of | ||
| [keywords], which governs all extracted identifiers: they are perfectly | ||
| legal as variable or method names, and only forbidden as type names. *) | ||
| let restricted_type_identifiers = | ||
| List.fold_right (fun s -> Id.Set.add (Id.of_string s)) | ||
| [ "permits"; "record"; "sealed"; "var"; "yield" ] | ||
| Id.Set.empty |
cedretaber
added a commit
that referenced
this pull request
Aug 19, 2026
PR #25 changed the Java backend to name the enclosing class after the extracted file instead of the fixed "Main". Update the goldens and drivers of the three tests added on this branch (poly_list, poly_head, corelib_list) accordingly. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
cedretaber
added a commit
that referenced
this pull request
Aug 19, 2026
* Erase type variables to Object and insert casts via local type propagation (#22) Tvar previously printed as OCaml-style 'a and type applications as (t1, t2) name, so any polymorphic definition or inductive produced uncompilable Java. Following the strategy agreed for issue #22: - pp_type erases Tvar to Object and drops type arguments; generated classes stay non-generic and polymorphic constants remain static fields (class declarations lose the ('a, 'b) prefix). - The printer records declared types per pp_struct (constants from Dterm/Dfix, inductive signatures from Dind) and propagates expected types top-down and recoverable actual types bottom-up through pp_expr; a plain cast is inserted only where the two erased Java types are known and differ. Unknown types insert no cast, so monomorphic output is unchanged (all nine existing goldens are byte-identical). - Constructor field accesses in match branches are cast using the MLcase scrutinee annotation instantiated with type_subst_list, which also types the let-bound variable. New test cases: poly_list (polymorphic list reversed at nat) and poly_head (application-result, let-bound and field-access casts), extracted, compiled and run by the harness. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Add a test extracting Corelib's polymorphic list, option and prod Now that type variables are erased to valid Java, the standard Corelib types work directly, without hand-rolled monomorphic copies: list nat with Corelib's app, an option nat built by matching, and a polymorphic pair swap instantiated at nat * bool. The driver checks the values end to end. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Adapt new extraction tests to per-file class names PR #25 changed the Java backend to name the enclosing class after the extracted file instead of the fixed "Main". Update the goldens and drivers of the three tests added on this branch (poly_list, poly_head, corelib_list) accordingly. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Cast intermediate receivers when a head type runs out of arrows A polymorphic head such as poly_id : A -> A can be applied to more arguments than its type has arrows once A is instantiated to a function type. Erasure gives the intermediate result the static Java type Object, so the chain's outermost cast alone cannot save the remaining .apply calls: javac rejects them first (reported on PR #23). When the arrow spine of the head's type is exhausted with arguments remaining, cast the receiver back to Function<Object, Object> before each remaining application, and treat the chain's actual type as Object so the existing outer cast fires. Add a poly_receiver test case reproducing the report. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Document why record_ind iterates over every packet All packets of a mutual inductive block share one MutInd.t, so the Array.iter re-adds the same binding once per packet. Note that this is harmless and only avoids assumptions about the packet array's shape, lest the repeated insertion read as a bug. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
extractのファイル名をhaskellと同様クラス名に反映するようにします