Comments (8)
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 ?
from dolmen.
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, ...).
from dolmen.
@Gbury Do you want to proceed with the port to dune before the pretty printer?
from dolmen.
That's the plan indeed, so that dolmen and the pretty-printers can be compiled (and released) separately.
from dolmen.
@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?
from dolmen.
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).
from dolmen.
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.
from dolmen.
@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.
from dolmen.
Related Issues (20)
- Additional builtins in the State? HOT 1
- Wrong check-model
- Bitvectors of size 0 should be forbidden
- Ill-typed statement on Bitvector is accepted by Dolmen HOT 1
- Expose `with_cache`? HOT 1
- Support Alt-Ergo's `cut` and `check` HOT 12
- Add authors files
- Unclear error message during model checking HOT 7
- Spec errors on the difference logic benchmarks of the SMT-LIB HOT 2
- Reject names starting with `@` and `.` outside of models
- Handling of `set-option :global-declarations`
- Handling of named terms HOT 2
- Check sat assuming HOT 2
- DIMACS variables do not appear as decls HOT 1
- Uncaught exception on buggy file
- 4.08 support broken (`List.concat_map`) HOT 10
- Quoted identifiers can be keywords HOT 12
- Warning regarding the `dolmen_type` file HOT 2
- Support non-incremental parsing from stdin HOT 1
- Handling abstract values in `(get-value)` statements HOT 8
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from dolmen.