Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Elpi ppx #63

Draft
wants to merge 7 commits into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .travis.yml
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ env:
- OCAML_MIN=4.04.1
- OCAML_MAX=4.09.0
- PREDEPS="ocamlfind"
- DEPS="camlp5 ocamlfind ppx_deriving ppxlib re dune cmdliner ANSITerminal"
- DEPS="camlp5 ocamlfind ppx_deriving ppxlib stdcompat re dune cmdliner ANSITerminal"
- MINDEPS="camlp5 ocamlfind dune re"
- JOBS=2

Expand Down
23 changes: 23 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
@@ -1,10 +1,33 @@
## v1.11.0 UNRELEASED

- PPX:
- new, experimental, elpi.ppx to generate glue code from an ADT declaration

- Stdlib:
- triple, quadruple and quintuple data types
- char builtin

- API:
- `ContextualConversion` module is gone.
- `('a, #ctx as 'c) Conversion.t` is the only datatype describing the
conversion for type `'a` under a context `'c` which is a subclass of
the raw context `#ctx`.
- `('i, 'k, #ctx as 'c) Conversion.context` is a datatype describing
the conversion for context `'i` indexed in the host application with keys
`'k`. A context items conversion can depend on a context as well.
- `BuiltInData.nominal` for nominal constants.
- `PPX` sub module gathering private access points for the `elpi_ppx` deriver.
- Conversions for data types such as `diagnostic`, `bool`, `*_stream`
moved from `Elpi.Builtin` to `Elpi.API.BuiltInData`.

- Trace:
- json output, with messages representing the tree structure of the proof
- categorize spy points into `user` and `dev`
- improve trace_ppx, revise all trace points
- port to ppxlib
- commodity extension `[%elpi.template name args]` and
`let[@elpi.template] f = fun args -> code` attribute to perform
compile time inlining (can be used to circumvent the value restriction)

- Build system:
- cache ppx output so that it builds without ppx_deriving and trace_ppx
Expand Down
7 changes: 6 additions & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,8 @@ DUNE_OPTS=
build:
dune build $(DUNE_OPTS) @all ; RC=$$?; \
( cp -r _build/default/src/.ppcache src/ 2>/dev/null || true ); \
( echo "FLG -ppx './merlinppx.exe --as-ppx --trace_ppx-on'" >> src/.merlin );\
( echo "FLG -ppx './merlinppx.exe --as-ppx --cookie '\''elpi_trace=\"true\"'\'''" >> src/.merlin );\
( echo "FLG -ppx './pp.exe --as-ppx '" >> ppx_elpi/tests/.merlin );\
exit $$RC

install:
Expand All @@ -46,6 +47,7 @@ cleancache:

tests:
$(MAKE) build
dune runtest --diff-command 'diff -w -u'
ulimit -s $(STACK); \
tests/test.exe \
--seed $$RANDOM \
Expand All @@ -56,6 +58,9 @@ tests:
$(addprefix --name-match ,$(ONLY)) \
$(addprefix --runner , $(RUNNERS))

test-noppx:
dune build --workspace dune-workspace.noppx

git/%:
rm -rf "_build/git/elpi-$*"
mkdir -p "_build/git/elpi-$*"
Expand Down
2 changes: 2 additions & 0 deletions dune-workspace.noppx
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
(lang dune 2.0)
(context (opam (switch 4.04.0))) ; here I don't have ppxlib
15 changes: 15 additions & 0 deletions ppx_elpi/dune
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
(library
(name ppx_elpi)
(public_name elpi.ppx)
(synopsis "[@@elpi]")
(libraries re ppxlib elpi)
(preprocess (pps ppxlib.metaquot))
(ppx_runtime_libraries elpi)
(modules ppx_elpi)
(kind ppx_rewriter)
(optional)
)

(env
(dev
(flags (:standard -warn-error -A))))
Loading