tweag/pirouette

Issues

• Document the “underlying implementation” of terms in the design document

  #190 opened 2 years ago by Niols
  0

• Give an overview of how to implement `LanguageBuiltins` in the design document

  #189 opened 2 years ago by Niols
  0

• Investigate whether `PrtUnorderedDefs` could be encoded as constraints in `SymEvalSt`

  #188 opened 2 years ago by Niols
  0

• Link to the transformations blog post in the DESIGN document

  #187 opened 2 years ago by Niols
  0

• Figure out `WeightedLists` and explain their use in design document

  #186 opened 2 years ago by Niols
  0

• Add a `hlint` pre-commit hook and cleanup files accordingly.

  #173 opened 2 years ago by Niols
  1

• Move or document orphan instances in `Language.Pirouette.QuasiQuoter.Internal`

  #176 opened 2 years ago by Niols
  0

• Use artifacts instead of cache to propagate test results in CI

  #164 opened 2 years ago by Niols
  0

• Linking Z3 fails on rebuild

  #160 opened 2 years ago by qaristote
  6

• Z3's logical context is leaked

  #156 opened 2 years ago by qaristote
  6

• Make `QuasiQuoter.Syntax` and `Pirouette.Term.Syntax.Pretty` compatible

  #126 opened 3 years ago by VictorCMiraldo
  1

• Translate case expressions to SystemF

  #142 opened 2 years ago by florentc
  0

• Type-level witnesses of transformations

  #148 opened 2 years ago by 0xd34df00d
  4

• Improve the surface language

  #143 opened 2 years ago by florentc
  0

• Consider simplifying monomorphisation and defunctionalisation

  #140 opened 2 years ago by facundominguez
  2

• Improve the surface language syntax

  #131 opened 2 years ago by VictorCMiraldo
  0

• How to deal with strict evaluation when arguments evaluate to bottom?

  #137 opened 2 years ago by carlhammann
  6

• Remove the need for `StateT` in the `SymEval` monad

  #138 opened 2 years ago by VictorCMiraldo
  3

• Remove the hack for translating `Bool` and make it into a transformation

  #127 opened 2 years ago by VictorCMiraldo
  1

• Transformation for removing `/\ dead . T` from the code

  #125 opened 2 years ago by VictorCMiraldo
  2

• Make `Eq` instance for `Datatype` into propositional equality

  #132 opened 2 years ago by VictorCMiraldo
  1

• Finalize the PlutusIR interface

  #122 opened 3 years ago by VictorCMiraldo
  0

• Test exhaustiveness of symbolic evaluator

  #94 opened 3 years ago by VictorCMiraldo
  6

• in `dev`: Update our READMEs

  #87 opened 3 years ago by VictorCMiraldo
  1

• Exit when counter-example is found

  #97 opened 3 years ago by serras
  2

• Understand and explore whether we really need that many monads in `SymEval`

  #112 opened 3 years ago by VictorCMiraldo
  6

• in `dev`: support as much of `PlutusIR` primitives as possible

  #88 opened 3 years ago by VictorCMiraldo
  5

• In `dev`: re-enable `ormolu` on CI and remove hlint

  #105 opened 3 years ago by VictorCMiraldo
  0

• In `dev`: Purify `pirouette` using a pure `solve` function, no more `IO` from the symbolic engine.

  #107 opened 3 years ago by VictorCMiraldo
  0

• In `dev`: Remove `Logger` and rename `LanguageSMTBranches`

  #106 opened 3 years ago by VictorCMiraldo
  2

• Bring back the TLA+ extraction.

  #57 opened 3 years ago by VictorCMiraldo
  2

• In `dev`: support `PlutusIR` type synonyms

  #101 opened 3 years ago by florentc
  1

• in `dev`: remove or re-design the executable

  #89 opened 3 years ago by VictorCMiraldo
  2

• In `dev`: Rename `MinSwap` to `IsUnityBug`

  #95 opened 3 years ago by VictorCMiraldo
  0

• Understand, document and implement a better "fuel" counter for the symbolic engine

  #90 opened 3 years ago by VictorCMiraldo
  5

• Deeper SMT embedding plan

  #81 opened 3 years ago by serras
  3

• Fix the translation of bound type variables avoiding the warning about it.

  #7 opened 3 years ago by VictorCMiraldo
  2

• Find a more idiomatic way of handling Plutus `Value`

  #13 opened 3 years ago by VictorCMiraldo
  1

• Improve our local nix and CI

  #22 opened 3 years ago by VictorCMiraldo
  1

• Improve the handling of builtins: devise a `Plutus.tla` file to be imported by the generated TLA+ code

  #38 opened 3 years ago by VictorCMiraldo
  0

• Whenever `declsUniqueNames` is disabled, we produce invalid TLA+

  #47 opened 3 years ago by VictorCMiraldo
  2

• Automatically generate the flat and pir files for `tests/integration/`

  #35 opened 3 years ago by VictorCMiraldo
  0

• Contracts of the `plutus-use-cases` folder

  #23 opened 3 years ago by GuillaumeGen
  1

• Generate type dependencies for terms declared within an inner let binding.

  #6 opened 3 years ago by VictorCMiraldo
  0

• Enable pirouette to extract a PlutusIR program's main term

  #48 opened 3 years ago by VictorCMiraldo
  0

• Replace `--with-args` and `--pull-destr` with a more flexible mechanism

  #12 opened 3 years ago by VictorCMiraldo
  0

• Deshadowing subterm is not working

  #43 opened 3 years ago by GuillaumeGen
  0

• Implement a more efficient version of `mapM expandDefs`

  #31 opened 3 years ago by VictorCMiraldo
  0

• `cfoldmapSpecialize` does not properly lift de Bruijn indices

  #25 opened 3 years ago by GuillaumeGen
  1

• Add `tla` and `tlacli` to our nix shell

  #5 opened 3 years ago by VictorCMiraldo
  0