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

API: cleanup contextual type of conversions #62

Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open
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
20 changes: 20 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
@@ -1,10 +1,30 @@
## v1.11.0 UNRELEASED

- 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
5 changes: 4 additions & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ 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 );\
exit $$RC

install:
Expand All @@ -56,6 +56,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
Loading