Skip to content

Commit

Permalink
API: only one conversion type indexed by a context object
Browse files Browse the repository at this point in the history
  • Loading branch information
gares committed Apr 30, 2020
1 parent f867d18 commit 95fa267
Show file tree
Hide file tree
Showing 28 changed files with 1,885 additions and 3,184 deletions.
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
2 changes: 1 addition & 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 Down
Loading

0 comments on commit 95fa267

Please sign in to comment.