search

arademaker / delphin

The Lean port of PyDelphin, a library to integrate DELPH-IN toolsets
Apache License 2.0
2 stars 2 forks source link

mrsprolog codec #4

Open arademaker opened 3 weeks ago

arademaker commented 3 weeks ago
  1. I would like to use the ideas from https://homepages.inf.ed.ac.uk/wadler/papers/prettier/prettier.pdf implemented in Lean as Format type.
  2. I would like to follow the idea of codecs from https://pydelphin.readthedocs.io/en/latest/api/delphin.codecs.html
MarcusGDaniels commented 3 weeks ago

The ToFormat typeclasses don't seem to be designed to add alternative formats. One idea is to have type tuples that combine the object with a style descriptor. If that were done, the Mrs/Basic.lean file should be done in the same way, I think.

arademaker commented 3 weeks ago

Indeed, I still need to clearly understand how to use the Prettyprinter to produce alternative formats. I am rereading the discussion at https://leanprover.zulipchat.com/#narrow/stream/419231-Lean-Together-2024/topic/A.20Pretty.20Expressive.20Printer.20-.20Sorawee.20Porncharoenwase.

arademaker commented 3 weeks ago

In this Haskell Library, the prettyprinter is illustrated with different renders

https://hackage.haskell.org/package/prettyprinter-1.7.1/docs/Prettyprinter.html