objectionary/normalizer

Command Line Normalizer of 𝜑-calculus Expressions

Normalizer for 𝜑-calculus

Command line normalizer of 𝜑-calculus expressions (as produced by the EO compiler).

Consult the project documentation for more details.

normalizer's Issues

Improve files generated by bnfc

• Par.y:

  • Support start and end positions
    • Like in the blog
    • OR, use a patched bnfc
  • Improve error messages using position information

• Abs.hs

  • Include custom code (see happy docs)
    • instance Plated Object (see Plated) (related to #18)
  • Use Text instead of String
  • (?) Use Bytes Integer

• Print.hs

  • Pretty-print Bytes

Add rule feature: global vertex counter

This is used in Yegor's rule 1.

Use the same BNFC version

• Make the version of BNFC fixed for devs so that changes to grammar don't produce larger than necessary diffs (like this one).

BNFC 2.9.6 doesn't exist on Hackage. The latest version is 2.9.5.

It also doesn't exist in our current resolver.

normalizer/stack.yaml

Line 1 in c1b2a13

resolver: nightly-2023-12-14

https://www.stackage.org/nightly-2023-12-14

However, I see comments that some files were generated by bnfc 2.9.6.

normalizer/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Abs.hs

Line 1 in c1b2a13

-- File generated by the BNF Converter (bnfc 2.9.6).

normalizer/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs

Line 1 in c1b2a13

-- File generated by the BNF Converter (bnfc 2.9.6).

Document usage of the normalizer

• Add examples with and without --chain
• Document user-defined rules (all existing features)

Add option to limit the number of results

Allow to set how many different answers to show.

Add rule condition: presence/absence of an attribute

These are used in Yegor's rules 1, 2, 3, 8, 11, for example.

Implement test generation

• Implement test generation (e.g. hedgehog + hspec)

Add unit tests

• 5 unit tests for each rule

Support all Yegor's rules as user-defined

The rules are being implemented in eo-phi-normalizer/test/eo/phi/rules/yegor.yaml:

• Rule 1
  • requires #55, #56, #57, #58. Implemented in #105
• Rule 2
  • requires #55. Implemented in #112
• Rule 3
  • requires #55
• Rule 4
  • requires #57. Implemented in #99
• Rule 5
  • ⚠️ implemented, but does not work properly (needs to be updated)
• Rule 6
  • ⚠️ implemented, but does not work properly due to questionable normal form condition
• Rule 7
  • ⚠️ implemented without vertex attribute, but does not work properly (updates to $\xi$, $\sigma$ and $\rho$ attributes
• Rule 8
  • requires #55
• Rule 9 (implemented in a slightly different form, but equivalent)
• Rule 10
  • requires #56. Implemented in #80
• Rule 11
  • requires #55
• Rule 12
  • Implemented in #109

deployment to hackage.haskell.org is not configured

Let's configure and make sure we deploy the package on every new tag (or by request)

Format files before a commit

• enable "editor.formatOnSave": true in .vscode/settings.json
• add a pre-commit hook for fourmolu

Add ruleset feature: program patterns

Related to #51

• Support patterns
• Support pattern imports so that patterns can be reused across rule sets

Implement pre-defined rules from Yegor's paper

• Implement rules from Yegor's paper
  
  • R1 (#9)
  • R2
  • R3
  • R4
  • R5
  • R6 (#9)
  • R7
  • R8
  • R9
  • R10
  • R11
  • R12

Document other internal representations of Java programs

• decide on the format of the documentation
• provide the documentation in this repo

Content

• Document how these representations can be mapped to EO

Output a rule index for each normalization step

• Add option for normalizer to print what rule was applied at each step
• Possibly show/highlight which part is matched and what substitution we get

Add integration test files

Superseded by #93

• Decide on tests layout
  • Probably, YAML-based
• Add sample tests in ./integration-tests

Add rule condition: (in)equality of attributes

This is used in Yegor's rules 1 and 10, for example.

Collect examples of user-defined functions

• Provide specifications of necessary user-defined functions in the YAML format
  • Define a function as a rewrite rule - similar to the current rules - link
  • State the conditions when this function is applicable
• Provide at least one unit test for each function
  • input PHI
  • output PHI
• Provide priority for each function - how important it is

Check formatting in CI

• fail CI when the formatting fails

Support integration into a Maven plugin

Support integration into a Maven plugin.

UPD

The plugin will run a command like this.

normalizer evaluate --rules rules.yaml --input-file phi/input.phi --output-file phi/output.phi

So, we already support this integration.

[meeting] [joint] 11.01.2024

Notes

1. Expecting publishing all intermediate steps in the benchmark CI (java -> EO -> phi -> normalization) (and some of their optimizations, opl). (objectionary/benchmark#16)
2. Waiting for the actual Java program examples that result in the use of rho. (objectionary/opeo-maven-plugin#68)
   • Additionally, asked for similar examples with the use of sigma and nu.
3. The EO team wishes to reuse the custom rule system to write optimizations. (#45)
   • several patterns in conditions to match;
   • combine objects, resolve naming conflicts;
   • access attributes after renaming;
4. In jump elimination paper, there are uses of quantifiers. There is a need to think of possibility of supporting them. (objectionary/opeo-maven-plugin#72)
5. Several EO files (e.g. four) should not be treated as different "universes", but rather as a single program (glued out of these files). We do not need to worry about decomposing the normalized program back into classes, we can output a single large file. (#46)
6. For the first iteration, normalization team focuses on the draft rules, afterwards moves more towards custom rules. (#11)

TODO

1. Provide JEO and OPEO papers (objectionary/jeo-maven-plugin#405, objectionary/opeo-maven-plugin#67).
2. Test custom rules (#34)
3. Provide more rules (#35, #36)
4. @deemp creates an issue about ci failure (#27)
5. Prepare milestones using GitHub Milestones (#37, objectionary/proof#7)
6. Draft a paper (#38)
7. Once the first version of normalizer is on hackage, need to integrate into a maven plugin (#2, #39).

Run confluence tests with user-defined rules

• Run confluence tests with user-defined rules

Fix pipeline

• Fix parsing error (blocked on objectionary/eo#2769)
• Ignore diff exit code
• remove the trailing newline in the normalize-phi output

Add rule feature: attribute (re)naming utilities

Based on some prior conversations, there appears to be a request for attribute name manipulation:

• create fresh attribute name (using existing attributes name as a suggested/preferred name)
• rename existing attribute

Add rule feature: reference to global object bindings

This is used in Yegor's rules 1 and 4, for example.

Implement confluence tests

• Decide on the test format
• Implement confluence tests

Draft a paper

• What is the research question?
• Global contribution?
• Look at the context
  • state-of-the-art imperative systems
  • rewrite systems

Add Nix script to run pipeline

• Add a Nix script let devs run a pipeline reproducibly locally

Create milestones

• Create milestones using GitHub Milestones
• Populate them

[meeting] [joint] 28.12.2023

Terms

1. VTX - "vertex" (see grammar)

• rename VTX to VERTEX (objectionary/eo#2768)

3. n - "normal form" (see paper)
   

Rules

• Yegor provides examples for rho, nu (v?) (https://github.com/yegor256/phi-paper/issues/1)
• Yegor adds dot notation in R8 (https://github.com/yegor256/phi-paper/issues/2)
• Improve pattern-matching in rules (https://github.com/yegor256/phi-paper/issues/2)

Normalizer

• Add mode 1 - apply pre-defined rules (#12)
• Add mode 2 - apply user-defined rules (#12)
  • Develop a language for rules (#11)
  • Develop a format for rules description (YAML?) (#11)

GH Actions

• Yegor provides a repro of suggested integration tests workflow (#3)

Add ruleset feature: conflict resolution rules

• support conflict resolution rules

• support importing these rules

  conflicts:
  - not_allowed
  - conflict_resolution_1.yaml

Get specifications of user-defined functions

1. Get use cases

@maxonfjvipon, @yegor256

• Create a PR against the normalizer repo - use the branch https://github.com/objectionary/normalizer/tree/51-collect-examples-of-user-defined-functions
• Provide use cases for user-defined functions
  • Describe functions in any convenient format
    • Example - #65 (comment)
    • Plain English is also OK
  • (Ideally) For each function:
    • Comment on its purpose and/or use cases
    • Provide examples of input and output
    • State the conditions when the function is applicable

2. Extract individual functions

@deemp, @aabounegm, @fizruk

• Describe proposal process
  • #247
• Extract individual functions from the use cases
• Provide specifications of user-defined functions in a YAML file (#236)
• Define each function as a rewrite rule - similar to the current rules - link
• Provide at least one unit test for each function
  • input PHI program
  • output PHI program
• Assign identifiers to functions
• Create issues for all functions (we need a separate thread of comments for each function)
• Link all issues here
• Ask @maxonfjvipon, @yegor256 to confirm we've specified the functions correctly
• Ask them to prioritize the functions by importance

3. Implement

@aabounegm, @fizruk

• Create new issue(s) to track implementation of the functions
• Implement functions in the order of importance

Potential features

• #65
• several patterns in conditions to match
• combine objects
  • resolve naming conflicts
• renaming
  • #59
  • access attributes after renaming
  • rename all occurences
  • "escape analysis"
• #67
• Support optional unwrapping of a rule result
  • if a result has other functions, unwrap them

[meeting] [joint] 18.01.24

• objectionary/proof#9
• #50
• #51
• objectionary/opeo-maven-plugin#96
• Release the first version of the normalizer (#2)
• (Optional) #52

Dependency Dashboard

This issue lists Renovate updates and detected dependencies. Read the Dependency Dashboard docs to learn more.

Open

These updates have all been created already. Click a checkbox below to force a retry/rebase of any.

• chore(deps): update dependency eolang to v0.21.1
• chore(deps): update dependency pre-commit to v3.8.0

Detected dependencies

github-actions

.github/workflows/ghc.yml

• actions/checkout v4
• haskell-actions/run-fourmolu v10
• haskell-actions/hlint-setup v2
• haskell-actions/hlint-run v2
• actions/checkout v4
• actions/cache v4
• freckle/stack-action v5
• actions/cache v4
• actions/checkout v4
• actions/cache v4
• freckle/stack-action v5
• actions/cache v4
• actions/setup-node v4
• actions/setup-java v4
• actions/cache v4
• actions/cache v4
• baptiste0928/cargo-install v3.1.1
• actions/upload-artifact v4
• actions/checkout v4
• freckle/stack-action v5
• actions/download-artifact v4
• jontze/action-mdbook v3
• JamesIves/github-pages-deploy-action v4

.github/workflows/release.yml

• actions/checkout v4
• freckle/stack-action v4
• haskell-actions/hackage-publish v1

npm

package.json

• eolang ^0.21.0
• prettier ^3.2.5

pip_requirements

requirements.txt

• pre-commit ==3.7.1

---

• Check this box to trigger a request for Renovate to run again on this repository

Support multiple EO files in the pipeline

For now, we run the pipeline on a single file.

normalizer/pipeline.sh

Lines 9 to 13 in b43f6e3

	cat > app.eo <<EOT
	[args] > app
	QQ.io.stdout > @
	"Hello, world!\n"
	EOT

Several EO files (e.g. four) should not be treated as different "universes", but rather as a single program (glued out of these files)

• More specifically, we should form a program with top-level attributes named as these files and work with it.

Alternatively, run normalizer on multiple test files

Describe a generalized normalizer

Describe a framework for normalization of terms given an arbitrary term rewriting system.

• benefits
• estimated amount of work
• input format
  • examples
• output format
  • examples
• literature
• approach

Support minimal $\varphi$-calculus as user-defined rules

Requires #60.

Different braces in grammar

I found inconsistency between canonical phi-calculus grammar (on the pic) and grammar in https://github.com/objectionary/normalizer/blob/master/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf.
Rules program, formation and application must have different braces

Add rule feature: support locator substitution

This is required to allow user-defined rules to specify minimal $\varphi$-calculus rules.

Provide tools for coding user-defined rules

Related to #288.

Try Rascal.

• generate a VS Code extension for the DSL

Implement CLI options for rule sets

• Add CLI option to choose rule sets

• --rules default - apply pre-defined rules

• --rules user --file ruleset1 --file ruleset2 - apply user-defined rules from given files

Depends on #4, #11

Rewrite rules using `lens`

Examples

relative to https://github.com/objectionary/normalizer/blob/b296cddce619a692a08f5571055772ee731c8cd2/eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs

lens

isNu :: Binding -> Bool
isNu (AlphaBinding VTX _) = True
isNu (EmptyBinding VTX) = True
isNu _ = False

instance Plated Object
instance Plated Binding

count :: (a -> Bool) -> [a] -> Int
count = (length .) . filter

countNus :: Object -> Int
countNus = getSum . go
 where
  go t =
    Sum ((\case Formation bindings -> count isNu bindings; _ -> 0) t)
      <> foldMapOf plate go t

pad :: [Char] -> [Char]
pad s = (if even (length s) then "" else "0") ++ s

insertDashes :: [Char] -> [Char]
insertDashes s
  | length s <= 2 = s ++ "-"
  | otherwise =
      let go = \case
            [] -> []
            [x] -> [x]
            [x, y] -> [x, y, '-']
            (x : y : xs) -> x : y : '-' : go xs
       in go s

insertNus :: Object -> Object
insertNus o =
  evalState
    ( rewriteM
        ( \case
            Formation bindings | not (any isNu bindings) -> do
              nus <- get
              id += 1
              pure $ Just (Formation $ AlphaBinding VTX (Formation [DeltaBinding (Bytes $ insertDashes $ pad $ showHex nus "")]) : bindings)
            _ -> pure Nothing
        )
        o
    )
    (countNus o)

N.B.: insertNus hangs indefinitely (see comment).

generic-lens

  finalBindings <-
    if not $ any isNu normalizedBindings
      then do
        nus <- gets totalNuCount
-        modify (\c -> c{totalNuCount = totalNuCount c + 1})
+       #totalNuCount += 1

integration tests are missing

Tasks

• Use test files (depends on #13 )
• Create a reproduction of the Pipeline (see below) in this repo in a ./pipeline directory (@yegor256)
  • provide necessary java files
  • provide a bash script that runs the suggested pipeline
• Build the package with stack

Pipeline

The pipeline would be the following:

First, start with the /tmp/test/app.eo file:

[args] > app
  QQ.io.stdout > @
    "Hello, world!\n"

Then, compile it via eoc and execute:

$ npm -g install eolang
$ cd /tmp/test
$ eoc dataize app
EO objects registered in .eoc/eo-foreign.json
Assembling into .eoc
EO program assembled in .eoc
EO program verified in .eoc
Java sources generated in .eoc/generated-sources
Java .class files compiled into .eoc
Executable JAR created at .eoc/eoc.jar
Hello, world!

---
[1]

Then, generate the .phi file:

$ eoc phi
EO objects registered in .eoc/eo-foreign.json
Assembling into .eoc
EO program assembled in .eoc
XMIR files converted into PHI files at .eoc

It will be generated in .eoc/phi/app.phi.

Then, normalize it and replace the .eoc/phi/app.phi file with new content (overwrite it!).

Then, generate XMIR from the app.phi file:

$ eoc unhpi
PHI files converted into XMIR files at .eoc/unphi

There should be new .eoc/unphi/app.xmir file generated.

Then, replace .eoc/2-optimize/app.xmir with this new file:

$ cp .eoc/unphi/app.xmir .eoc/2-optimize/app.xmir

Then, create a new EO file:

$ eoc print
XMIR files converted into EO files at .eoc/print

The .eoc/print/app.eo should be generated.

Copy it to app.eo (overwrite the existing one!):

$ cp .eoc/print/app.eo app.eo

Then, execute:

$ eoc clean
$ eoc dataize app
Hello, world!

Expect the Hello, world! output, as in the previous execution. If they match, your test passes.

Rename VTX -> Vertex

• Rename VTX -> Vertex in the grammar and other places following objectionary/eo#2768 (comment)

Implement a user-defined rules language

• Develop a format for rules description
  • possibly YAML-based
• Develop an initial version of user-defined rules language
• Implement tests

Example

rules:
  - name: Rule 6
    description: "Accessing an α-binding"
    pattern: |
      ⟦ ?a ↦ ?n, ?B ⟧.?a
    result: |
      ?n(ρ ↦ ?B)
    when:
      - nf: [ "?n" ]

Run integration tests in GH Actions

• cache dependencies (e.g., via cache-nix-action) on Linux and MacOS
  • we cache via dedicated actions
• set up separate job(s) for Windows
  • dedicated actions work also for Windows

Extend the user-defined rules language

Depends on #11.

Features:

• several patterns in conditions to match
• combine objects, resolve naming conflicts
• access attributes after renaming

Several patterns in conditions to match

Example:

TODO

Several patterns in conditions to match

Example:

TODO

Access attributes after renaming

Example:

TODO

Test against EO compiler

Related to #69 .

• Test the two evaluations:
  • Simply using EO compiler and running the resulting program
  • Converting EO program to $\varphi$-term, then using normalizer, then converting back to EO program, and then using EO compiler, then running the resulting program

[meeting] [internal] [phi] 10.01.2024

What we can learn from this project

• get expertise in optimizing compilers
• get to know various internal representations of languages

TODO

• Implement the rules (even if they're broken) (#4)
• Formalize confluence or find an example for lack of it (objectionary/proof#6)
• Guide the implementation of JEO, OPEO
  • Study the existing documentation (objectionary/jeo-maven-plugin#405, objectionary/opeo-maven-plugin#67)
  • Request and study the additional documentation (objectionary/opeo-maven-plugin#73)
  • Devise a specification of JEO, OPEO (objectionary/opeo-maven-plugin#66)
  • Provide examples of Java programs translated to EO (objectionary/opeo-maven-plugin#68)
• Document other internal representations of Java programs (#32)

Meetings

There'll be separate meetings dedicated to (1) phi-calculus, (2) normalizer formalization, (3) normalizer implementation

Fix grammar

• Fix Bytes definition (see EO grammar)