Switch to dune ?

[Gbury]

Providing printers for terms needs to correctly handle unicode[1] in the general case. Thus it adds uutf and uucp as dependencies, however people may not need or want those dependencies in a parser library[2].

The simple answer is to provide another package (kind of a sub-package) that provides the export functionalities, and which can depend on uutf and uucp while the main package does not need them.

However, correctly handling multiple packages is quite a pain to deal with when using ocamlbuild and manual makefiles for installation, so switching to dune would probably ease that a lot (once the switch done), so here it goes: dolmen should probably switch to dune.

If anyone is motivated to do the switch, please do so and create a PR ! Else I'll have a look sometime soon.

cc @anmaped

[1] : handling unicode primarily means detecting unicode characters in order to know what to do with them in languages that do not support unicode. This require a unicode-aware handling of identifiers strings, if only to replace unicode characters by appropriate ASCII characters.

[2]: though if dolmen one day parses unicode-aware languages (such as Coq ?), a unicode-ware lexer might be needed...

[anmaped]

The simple answer is to provide another package (kind of a sub-package) that provides the export functionalities, and which can depend on uutf and uucp while the main package does not need them.

It's a reasonable choice for now.

However, correctly handling multiple packages is quite a pain to deal with when using ocamlbuild and manual makefiles for installation, so switching to dune would probably ease that a lot (once the switch done), so here it goes: dolmen should probably switch to dune.

Do you have an idea of the shape of that prettyprinter package ?
Is the idea to use a Dolmen package and a Dolmen_prettyprint package ?

[Gbury]

Do you have an idea of the shape of that prettyprinter package ?
Is the idea to use a Dolmen package and a Dolmen_prettyprint package ?

Yes, the exact name of the subpackage is yet to be decided though (something like Dolmen.export, Dolmen.print, Dolmen.pp, ...).

[anmaped]

@Gbury Do you want to proceed with the port to dune before the pretty printer?

[Gbury]

That's the plan indeed, so that dolmen and the pretty-printers can be compiled (and released) separately.

[anmaped]

@Gbury Alright. I will do it these days.

I'm also interested in pretty printing Statements/Terms to Coq (assuming at least lambdas and non interpreted functions). Do you think is doable? Do you see some problems beforehand?

What do you think about including parameterized unrolling of recursive definitions in Dolmen?

[Gbury]

Thanks a lot ! Don't hesitate to ask if you have any problem.

Concerning printing to Coq, it is clearly possible. However, the only guarantee that will be given is that the printed term is syntaxically correct, but not correctly typed or typable.
For instance, quantification of variables without explicit type annotations is possible in the untyped terms of dolmen, and will be printable in Coq, but Coq will likely reject such terms.

About parmeterized unrolling of recursive definitions, it's definitely possible but I'd say it's preferable to do such transformations on a typed AST (Dolmen only has an untyped AST currently, see the #4 for discussions on including a typechecker to dolmen).

[Gbury]

Note that if you want some command line tool that can read some tptp or smtlib file, and print equivalent Coq axioms, https://github.com/Gbury/archsat can reliably do so for you (only for first-order though), and ensures that the produced file is correctly typed.

[anmaped]

@Gbury I attach the small config file for dune.

(ocamllex
 (modules lexiCNF lexZf lexTptp lexSmtlib lexDimacs)
)

(menhir
 (flags (--infer --explain))
 (modules parseiCNF parseZf parseTptp parseSmtlib parseDimacs)
)

(library
  (name            dolmen)
  (public_name     dolmen)
  (modules

; Standard implementation
Id
Term
Normalize
Statement
ParseLocation

; Interfaces
Lex_intf
Parse_intf
Location_intf

Id_intf
Term_intf
Stmt_intf
Language_intf


; Dimacs language
Dimacs
LexDimacs
ParseDimacs
Ast_dimacs

; iCNF language
ICNF
LexiCNF
ParseiCNF
Ast_iCNF

; Smtlib language
Smtlib
LexSmtlib
ParseSmtlib
Ast_smtlib

; Zf language
Zf
LexZf
ParseZf
Ast_zf

; Tptp language
Tptp
LexTptp
ParseTptp
Ast_tptp

; Languages classes
Logic

; Helper modules
Misc
Transformer

  )
  (libraries       MenhirLib)
)

(include_subdirs unqualified)

However, I'm not able to compile it due to a bug in the current version 1.2.1 (ocaml/dune#1372).

I will try to compile dune 1.4.