Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

SCP-2136 Inline single occurence bounded terms #3630

Closed
wants to merge 3 commits into from
Closed

Conversation

jakzale
Copy link
Contributor

@jakzale jakzale commented Jul 28, 2021

Pre-submit checklist:

  • Branch
    • Commit sequence broadly makes sense
    • Key commits have useful messages
    • Relevant tickets are mentioned in commit messages
    • Formatting, materialized Nix files, PNG optimization, etc. are updated
  • PR
    • Self-reviewed the diff
    • Useful pull request description
    • Reviewer requested

Pre-merge checklist:

  • Someone approved it
  • Commits have useful messages
  • Review clarifications made it into the code
  • History is moderately tidy; or going to squash-merge

@jakzale jakzale force-pushed the jakzale/inline branch 2 times, most recently from af17ef2 to e0a0f03 Compare August 4, 2021 23:08

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
- pedantic typechecking will typecheck between simplifier passes,
- add option for being verbose about simplifier passes,
- add option for dumping PIR to stdout before and after a pass,
- add option for specifying max number of iterations,
- add option for controlling each simplifier pass,
- run the simplifier 8 times by default.
Another attempt at inliner

The following commits are included:

- Refactor out Flat instance for PlutusIR,
- Moves Flat instance for PlutusIR to PlutusIR.Core.Instance.Flat,
- Add Plugin option to dump flat pir representation,
- Add a small tool to load and compile binary PIR.
@jakzale
Copy link
Contributor Author

jakzale commented Aug 5, 2021

@michaelpj I think you will have to take this from here.

Note that general pir compiler improvements got split into a separate PR (#3655) and should be safe to merge by now. Nevertheless, as this PR depends on that work, they are included in this PR as well.

Unfortunately, there still seems to be a bug in the floatTerm pass: compiling plutus-ledger will lead to the following output

[19 of 25] Compiling Ledger.Typed.Scripts.MonetaryPolicies ( src/Ledger/Typed/Scripts/MonetaryPolicies.hs, /home/jakub/Developer/plutus-inline/dist-newstyle/build/x86_64-linux/ghc-8.10.4.20210212/plutus-ledger-0.1.0.0/build/Ledger/Typed/Scripts/MonetaryPolicies.o, /home/jakub/Developer/plutus-inline/dist-newstyle/build/x86_64-linux/ghc-8.10.4.20210212/plutus-ledger-0.1.0.0/build/Ledger/Typed/Scripts/MonetaryPolicies.dyn_o )
  !!! rename
  !!! simplifyTerm
    !!! simplifier pass 1
      !!! unwrap cancel
      !!! beta
      !!! inline
      !!! remove dead bindings
    !!! simplifier pass 2
      !!! unwrap cancel
      !!! beta
      !!! inline
      !!! remove dead bindings
    !!! simplifier pass 3
      !!! unwrap cancel
      !!! beta
      !!! inline
      !!! remove dead bindings
    !!! simplifier pass 4
      !!! unwrap cancel
      !!! beta
      !!! inline
      !!! remove dead bindings
    !!! simplifier pass 5
      !!! unwrap cancel
      !!! beta
      !!! inline
      !!! remove dead bindings
    !!! simplifier pass 6
      !!! unwrap cancel
      !!! beta
      !!! inline
      !!! remove dead bindings
    !!! simplifier pass 7
      !!! unwrap cancel
      !!! beta
      !!! inline
      !!! remove dead bindings
    !!! simplifier pass 8
      !!! unwrap cancel
      !!! beta
      !!! inline
      !!! remove dead bindings
  !!! floatTerm
GHC Core to PLC plugin: E020:Error: Error from the PIR compiler:
            E020: Error during PIR typechecking:
            Free variable at  () :  d_25317

Also, equality does not survive renaming without marking seems to fail once in a blue moon:

cd plutus-core/
for run in {1..100}; do
  cabal run plutus-core:plutus-core-test -- --pattern "equality does not survive renaming without marking"
done

will eventually get it to fail. I am not sure if that is simply because it generates a term with no names.

@michaelpj
Copy link
Contributor

Okay, I'll take it from here.

@michaelpj michaelpj closed this Aug 5, 2021
@michaelpj
Copy link
Contributor

On the plus side, I managed to isolate and minimize the let-floating bug, now let's see if I can fix it.

@jakzale
Copy link
Contributor Author

jakzale commented Sep 4, 2021

I rebased this branch on top of #3823 and got pass pass floating let terms. Now there seems to be an issue with compiling recursive terms. (Note that this is with pedantic typechecking on):

[20 of 26] Compiling Ledger.Typed.Scripts.MonetaryPolicies ( src/Ledger/Typed/Scripts/MonetaryPolicies.hs, /home/jakub/Developer/plutus-inline/dist-newstyle/build/x86_64-linux/ghc-8.10.4.20210212/plutus-ledger-0.1.0.0/build/Ledger/Typed/Scripts/MonetaryPolicies.o, /home/jakub/Developer/plutus-inline/dist-newstyle/build/x86_64-linux/ghc-8.10.4.20210212/plutus-ledger-0.1.0.0/build/Ledger/Typed/Scripts/MonetaryPolicies.dyn_o )
  !!! rename
  !!! removeDeadBindings
  !!! simplifyTerm
    !!! simplifier pass 1
      !!! unwrap cancel
      !!! beta
      !!! inline
    !!! simplifier pass 2
      !!! unwrap cancel
      !!! beta
      !!! inline
    !!! simplifier pass 3
      !!! unwrap cancel
      !!! beta
      !!! inline
    !!! simplifier pass 4
      !!! unwrap cancel
      !!! beta
      !!! inline
    !!! simplifier pass 5
      !!! unwrap cancel
      !!! beta
      !!! inline
    !!! simplifier pass 6
      !!! unwrap cancel
      !!! beta
      !!! inline
    !!! simplifier pass 7
      !!! unwrap cancel
      !!! beta
      !!! inline
    !!! simplifier pass 8
      !!! unwrap cancel
      !!! beta
      !!! inline
  !!! floatTerm
  !!! compileNonStrictBindings
  !!! thunkRecursions
  !!! compileLets DataTypes
  !!! compileLets RecTerms
GHC Core to PLC plugin: E016:Error: Error from the PIR compiler:
            E016: Error during PIR typechecking:
            Type mismatch at <unknown> in term
              's'.
            Expected type
              '(ifix
                (lam
                  self_21843
                  (fun (type) (type))
                  (lam a_21844 (type) (fun [ self_21843 a_21843 ] a_21843))
                )
                a_0
              )',
            found type
              '(ifix
                (lam
                  self_21832
                  (fun (type) (type))
                  (lam a_21833 (type) (fun [ self_21832 a_21832 ] a_21832))
                )
                (lam
                  a_21837
                  (type)
                  (ifix
                    (lam
                      self_21838
                      (fun (type) (type))
                      (lam a_21839 (type) (fun [ self_21838 a_21838 ] a_21838))
                    )
                    a_21837
                  )
                )
              )'
Context: Compiling expr at "plutus-ledger-0.1.0.0-inplace:Ledger.Typed.Scripts.MonetaryPolicies:(53,11)-(53,105)"

@jakzale
Copy link
Contributor Author

jakzale commented Sep 4, 2021

Suspected there was something off with type inlining being disabled, but after enabling it, it made stuff worse.

Added it as a reverted commit to jakzale/inline for posterity.

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