Printer for terms - #14

@Gbury In the tptp file is it a typo let name id = Pretty.Normal (Dolmen_std.Id.full_name id) in, or do you plan to extend the Normal construct inside Pretty?

That's a typo, should indeed be Escape.Normal, ^^

It's corrected then.

Should we create a new package, including the external dependencies in the dolmen.opam file, or compile dolmen.export only if the dependencies are available?

Separate package, by creating a dolmen-export.opam file with the correct deps (i.e. dolmen, uucp and uutf).

@Gbury It's right. I forget it.

Should we treat this cases like that ?

| Def (id, ({term = Binder (binder, _, _)} as term)) ->
    Format.fprintf
      fmt
      "(define-%s %s %a)"
      (print_binder binder).name
      (Dolmen_std.Id.full_name id)
      print_terms
      term
| Def (id, _) -> assert false

In smtlib doesn't make sense to print a definition that is not a function nor a sort.

Smtlib's define-fun allows functions with arity 0, i.e. it allows defining constants, so no need for an assert false.

I don't think you've understood the design of the Pretty module (though that's probably my fault for not documenting it enough). The point of a Pretty.t is to factorize away the printing of single identifiers.

So in a typical control flow, you'll have a function pretty_of_builtin : builtin -> Pretty.t (Note that you called it print_builtin although it simply creates a Pretty.t, and does not actually print anything). Similarly, you'd have a function from an Id to a Pretty.t.
Afterwards, you'd write a function that actually prints terms that are applications, and in this function, you'll use the information of the Pretty.t of the head symbol to decide how to print the term. So for instance the printing functions in https://github.com/Gbury/archsat/blob/master/src/output/tptp.ml#L113

Smtlib's define-fun allows functions with arity 0, i.e. it allows defining constants, so no need for an assert false.

So, what to do with the other binders?

So, what to do with the other binders?

Well, clearly, in a lot of cases (for instance, when a forall is bound), the term cannot be printed. In such cases, instead of assert false, a custom exception such as Smtlib.Cannot_print of term should be raised I think, at least for now.

So, what to do with the other binders?

Well, clearly, in a lot of cases (for instance, when a forall is bound), the term cannot be printed. In such cases, instead of assert false, a custom exception such as Smtlib.Cannot_print of term should be raised I think, at least for now.

Yes. I will do it incrementally, first I expect to pretty print all the parsed smtlib files (some that I have generated), then we can do translations from other constructions available for instance in tptp.

@Gbury Do you have any reason for implementing the order of body ty_ret like

let fun_def ?loc id args ty_ret body =
  let t = Term.lambda args (Term.colon body ty_ret) in
  mk ?loc (Def (id, t))

instead of

let fun_def ?loc id args ty_ret body =
  let t = Term.lambda args (Term.colon ty_ret body) in
  mk ?loc (Def (id, t))

Typically, most type annotations are of the form: term: type (I think all the exmaples I know of always put the term on the left, and the type on the right). If you look at the way typed variables are handled (for instance, in quantifications), it is also in this order.

Alright.

Should we create a new bash script for testing dolmen-exports? Which testing mechanism have you in mind?

Basically, the goal of tests would be to check that parsing and printing are invers of one another, which can be divided into two distinct tests:

• For any AST, printing it, then parsing it should produce the same AST (modulo the normalization functions in Normalize)
• For any printed file, parsing it and then printing it should produce an identical file (note that the input file needs to be the result of printing some AST using the printing function, in order to not fail on basic formatting differences).

The two tests can be done at the same time, using a small ocaml program which does the following:

• take an arbitrary input in some language
• parse it, and save the AST somewhere
• print the AST to a first file
• parse that file, and check that this second AST matched the first one
• print that second AST into a second file
• check that the two produced files are identical (could be done outside the ocaml program, by using diff in the shell script)

This would then need to be run on pretty much the whole smtlib to check that there are no errors.

Additionally, it could be nice to have some quickcheck-like testing (using the same method as described in the previous comment, but using a randomly-generated AST instead of an AST coming from an input file).

@Gbury What is the plan for the printing feature?

@Gbury What is the plan for the printing feature?

The printing feature is the next big item on my todo list for dolmen, on which i'll be working once #84 is merged.

My current plan is to add printing functors, which will take a view on terms, and return printing functions. I still have a few details concerning scopes[1] and differences in spec between languages[2] to work out, but it shouldn't delay things too much. When I have working code, I'll probably open a different PR (and close this one). As for the timeline, maybe I'll get enough time to get some working code around the end of October ?

[1] : the printing function will take as first argument an environment, which will carry both a global and local state in order to accurately track scopes and potential renaming of variables/constants in order to avoid unintended shadowing.

[2] : the module taken as argument to the printing functor will expect a view functions on terms. For simplicity, this view type will be defined by Dolmen and most likely use the current types builtins. The printing of builtins is straightforward when the same language is used as input and output, but for the other cases, it can be more tricky. Basically, there are a few subtle situations:

• builtins from a source language that do not exist in the printing language. For these there are a few solutions (which will probably end up being configurable by the user of printing functions): either fail during the printing, or provide emulations (either in a prelude that will need to be printed/included from somewhere, or locally if the wrappers are small enough)
• builtins that are present in both a the source and destination languages, but which might have subtly differing semantics in the two languages (think about arithmetic operators and rounding, etc...). For that, I'll probably need to re-read the specs quite carefully and assign a very precise semantics to each of Dolmen's builtins.
• lastly for some language features which are missing in the destination language or different enough, dolmen might need some more involved manipulation on terms before printing. For instance, for datatype in a source language with mainly constructors/testers (i.e. which mainly use is#some_constructor predicates) and a destination language which mainly uses pattern matching, we'll probably want to recognize "deep" if/then/else structures that encode pattern matching using the is#constr predicates in order to print these as a single pattern matching.

This is now a bit too outdated, so i'll close this PR and open a new one when I have the time to work on printing/exporting.