Extract local MLfix as valid Java expressions via fixK helpers by hiroshi-cl · Pull Request #20 · proof-ninja/rocq

hiroshi-cl · 2026-07-22T17:01:11Z

MLfixに対応してvalidなJavaコードが出るようにします。
相互再帰には対応していません。
参照のない変数がある場合JDK21までではコンパイルできないコードが出ます #19

hiroshi-cl · 2026-07-23T10:53:16Z


 static Function<shape, result> from_shape = s ->
-  (s instanceof Leaf) ? new Ok()
+  ((s instanceof Leaf) ? ((result) new Ok())


再帰で型が小さく推論されないようにするために補うキャスト

cedretaber · 2026-07-23T12:16:56Z

+  assert (Array.length ids = 1);
+  assert (Array.length bl = 1);
+  assert (Int.equal i 0);


user_err を使った方が良いかもしれません。
（丁寧なエラーが出せるので。）

…_fix Addresses review feedback: #20 (comment)

hiroshi-cl · 2026-07-27T16:09:38Z

+  if not (Int.equal (Array.length ids) 1 && Int.equal (Array.length bl) 1
+          && Int.equal i 0)
+  then user_err Pp.(str "Cannot handle mutually recursive definitions in Java yet.");


user_err にしました

cedretaber · 2026-07-27T17:54:00Z

-        and pp_a1 = pp_expr table env [] a1
-        and pp_a2 = pp_expr table env' [] a2 in
-        hv 0 (apply (pp_letin pp_id pp_a1 pp_a2))
+        if is_fix_head a1 then pp_expr table env args (ast_subst a1 a2)


📝
ast_subst a1 a2 で AST を代入（この場合は文字通り置換？）しているので、束縛した変数を2回使う場合、2回評価してしまうかもしれない。

let r := go l in Node r r (* go l が2回評価される *)

が、ここを let 束縛で置き換えると型推論が通らなさそうなのでやむを得ない？

難しそうだったので上にコメントだけつけておいた

cedretaber · 2026-07-27T18:01:27Z

+Extraction "java_local_fix.java"
+  rev_acc rev_pair.


fix0 は他と違う実装なので、これ用のテストが別途あってもいいかも。

https://github.com/proof-ninja/rocq/pull/20/changes#diff-33cb0ad40c65cd67b59e8b59ec7ed9d5065d451039d76cb12b724a9bea9e00a6R151-R153

cedretaber

機能的には大丈夫そうです。

The Java backend printed local MLfix as a statement sequence (var f = ...; ...; f.apply(args)), which is invalid in expression positions (lambda bodies, let RHS, function arguments). Every other MiniML construct already prints as an expression. Encode a local fix applied to K arguments as a call to a generated generic helper fixK(gen, a1, ..., aK) that ties recursion by method self-reference, so no cell arrays, unchecked casts, definite-assignment or effectively-final issues arise. Argument types ground A1..AK bottom-up and R is grounded by the target type of the expression position. Helpers are emitted on demand per arity next to the let helper (fix0 for unapplied fixes implies fix1). Scope is single (non-mutual) local recursion only, matching the pattern that actually shows up in ordinary miniML-style code. Mutual fixpoint groups (Array.length ids > 1) are not supported: the new pp_fix's invariant assertions (Array.length ids = 1, i = 0) reject them, the same way this file already treats other structurally unsupported constructs (Tmeta/Tvar'/Taxiom in pp_type, MEident/MEapply in pp_module_expr) with a bare assert rather than a bespoke error. Supporting changes needed for javac type inference: - Inline let-bound fix heads into their use sites (a fixK call in the targetless let() argument position would infer Object). - Upcast constructor expressions to their inductive interface, ((natlist) new Cons(...)), to avoid over-specialized inference such as A2 := Nil; skipped for custom inductives. Expected outputs regenerated accordingly. - Fix MLmagic and MLcase dropping the application args accumulator. Known limitations: fixK calls in positions without a target type infer R = Object (e.g. a fix application result bound by let); helper names fixN can collide with user identifiers (same caveat as let); parameterized inductives get raw-type casts. Tests: local_fix (single recursion, applied K=2 and reused let-bound fix), with a runtime driver. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

…_fix Addresses review feedback: #20 (comment)

…ting MLletin over a fix-headed value used ast_subst unconditionally, which is fine when the value is a bare, unapplied MLfix (duplicating just its definition text, as in the existing rev_pair case) but silently re-executes the recursive computation itself when the value is already an application of the fix and the bound variable is reused. Detected via a minimal repro matching the pattern in PR #20 review comment #20 (comment). Raise a clear user_err for the unsafe case (applied fix result used more than once, where "more than once" also treats any use nested under a further lambda/fix as unsafe regardless of syntactic count, since such a use can be evaluated many times at runtime) instead of silently recomputing, matching this file's existing precedent of user_err over silent bad behavior (see the mutual-recursion check in pp_fix). Add test-suite/misc/java-extraction/fix_reuse.v covering both the safe (single, non-nested use) and unsafe (reused) shapes. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

MLletin over a fix-headed value uses ast_subst unconditionally. This is fine when the value is a bare, unapplied MLfix (duplicating just its definition text, as in the existing rev_pair case), but if the value is already an application of the fix (a computed result) and the let-bound variable is used more than once, the substitution duplicates the recursive computation itself, not just source text. Flagged in PR #20 review comment #20 (comment) . Not attempting a check or warning here: the underlying function is pure, so the result is still correct, just potentially recomputed; a prior attempt at detecting and erroring on this case would have made previously- extractable Rocq programs fail to extract entirely, which is worse than the duplication itself. Documenting it in place instead. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

pp_fix_helper's k=0 (fix0) and k=1 (fix1) cases had no test coverage: local_fix.v always applied its local fix to both arguments at every call site, so only fix2 was ever generated or compiled. In particular, the Int.Set.mem 0 -> add 1 rule in pp_struct (fix0's body unconditionally calls fix1, so a program using only fix0 needs fix1 emitted too, even with no direct fix1 call site) was untested and, if broken, would only surface as a javac "cannot find symbol" failure in some future unrelated change. Add fix0.v: a local fix referenced as a bare, unapplied value (from a match branch, and as a higher-order argument to a Fixpoint), which is what makes pp_fix see zero already-applied arguments and emit fix0. Verified by temporarily removing the Int.Set.mem 0 rule and confirming run-case.sh fix0 fails (missing fix1 helper) while local_fix is unaffected, then reverting. Add rev_onto to local_fix.v: a local fix applied to exactly one argument at its call site, exercising fix1 (previously never emitted either). Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

hiroshi-cl · 2026-07-28T16:27:35Z

fix0のカバレッジ追加

hiroshi-cl commented Jul 23, 2026

View reviewed changes

hiroshi-cl marked this pull request as ready for review July 23, 2026 10:54

hiroshi-cl requested a review from cedretaber July 23, 2026 11:12

cedretaber reviewed Jul 23, 2026

View reviewed changes

hiroshi-cl added a commit that referenced this pull request Jul 27, 2026

Use user_err instead of assert for unsupported mutual recursion in pp…

070c0b4

…_fix Addresses review feedback: #20 (comment)

hiroshi-cl commented Jul 27, 2026

View reviewed changes

cedretaber reviewed Jul 27, 2026

View reviewed changes

cedretaber approved these changes Jul 27, 2026

View reviewed changes

cedretaber mentioned this pull request Jul 27, 2026

5. Tvar/Tdummy/Tunknown を有効なJava型として生成する #22

Open

hiroshi-cl and others added 2 commits July 29, 2026 00:08

Use user_err instead of assert for unsupported mutual recursion in pp…

d49e4f8

…_fix Addresses review feedback: #20 (comment)

hiroshi-cl force-pushed the feat/java-simple-recursion branch from 070c0b4 to d49e4f8 Compare July 28, 2026 15:09

hiroshi-cl force-pushed the feat/java-simple-recursion branch from c7ab6a0 to d49e4f8 Compare July 28, 2026 15:42

hiroshi-cl and others added 2 commits July 29, 2026 00:53

hiroshi-cl commented Jul 28, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Extract local MLfix as valid Java expressions via fixK helpers - #20

Extract local MLfix as valid Java expressions via fixK helpers#20
hiroshi-cl wants to merge 4 commits into
java_extractionfrom
feat/java-simple-recursion

hiroshi-cl commented Jul 22, 2026 •

edited

Loading

Uh oh!

hiroshi-cl Jul 23, 2026

Uh oh!

cedretaber Jul 23, 2026

Uh oh!

hiroshi-cl Jul 27, 2026

Uh oh!

cedretaber Jul 27, 2026

Uh oh!

hiroshi-cl Jul 28, 2026

Uh oh!

hiroshi-cl Jul 28, 2026

Uh oh!

cedretaber Jul 27, 2026

Uh oh!

cedretaber left a comment

Uh oh!

hiroshi-cl Jul 28, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

hiroshi-cl commented Jul 22, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

cedretaber left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

hiroshi-cl commented Jul 22, 2026 •

edited

Loading