Skip to content

Isolate the front end part as a library#6

Merged
KenSakayori merged 18 commits intomasterfrom
ocaml-hfl
Aug 13, 2025
Merged

Isolate the front end part as a library#6
KenSakayori merged 18 commits intomasterfrom
ocaml-hfl

Conversation

@KenSakayori
Copy link
Copy Markdown
Member

This PR adapts the code to use this library. The library is basically the codes that existed in lib/syntax. The followings are the reasons to prefer using a library:

  1. it's much easier to share the code between muhfl and rethfl (ReTHFL doesn't use this library yet).
  2. the codes in the library are better documented and arguably cleaner.

The first point is important if we were to add features (e.g. the support of ADT) to muhfl. We don't want to write the code for ADT twice, one for muhfl and the other for Rethfl. Actually, this problem has already happened multiple times in the past. For example, the code to remove disjunctoins of a nuHFL formula has been written twice. Also muhfl has a lot of redundant code (which this PR doesn't delete). I don't know why we need a yet another data type for Hflz and yet another printer for the HFlz (not for the new data type but for the original one).

It's also simply much easier to maintain the two tools. There are changes/fixes that has only been applied to muhfl and not to rethfl and vice versa. I tried to import the changes to the library as much as possible.

I believe that no one can review this PR, so I'll do a self-review, and merge it once I think it is ready.

@KenSakayori KenSakayori requested a review from Copilot August 13, 2025 09:35
@KenSakayori
Copy link
Copy Markdown
Member Author

Trying a review from Copilot, out of curiosity.

Copy link
Copy Markdown

Copilot AI left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pull Request Overview

This PR replaces the local syntax library (lib/syntax) with an external HFL library, migrating the codebase to use shared components for better maintainability across related tools (muhfl and rethfl).

Key changes include:

  • Complete removal of the local lib/syntax module and replacement with the external hfl library
  • Update of dependency management to include the new hfl library from git
  • Extensive refactoring across the codebase to use the new library's module structure and APIs

Reviewed Changes

Copilot reviewed 70 out of 71 changed files in this pull request and generated 4 comments.

Show a summary per file
File Description
muhfl.opam.template, muhfl.opam Add dependency on external hfl library
lib/syntax/* Complete removal of local syntax implementation
lib/muhfl_prover/* Update imports from Hflmc2_syntax to Hfl
lib/manipulate/* Migrate to use Hfl modules and update function calls
lib/mufu_core/* Replace Hflmc2_syntax with Hfl
lib/muhfl.ml Update parsing logic to use new library APIs

Tip: Customize your code reviews with copilot-instructions.md. Create the file or learn how to get started.

@KenSakayori KenSakayori changed the title Isolate the front end part as a library. Isolate the front end part as a library Aug 13, 2025
If I understand correctly, the rename_simple_ty thing was used to align
the variable in type with that of the function argument.
For example, it changes the type of \x. e
from
f : (y : Int -> Prop)
to
f : (x : Int -> Prop)

I don't think we rely on the variables in types because we are only
using simple types.
Hence it should be safe to remove it
@KenSakayori KenSakayori self-assigned this Aug 13, 2025
@KenSakayori KenSakayori merged commit 485cf71 into master Aug 13, 2025
4 checks passed
@KenSakayori KenSakayori deleted the ocaml-hfl branch August 13, 2025 14:49
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants