From e49ad6b976d2509f60db9e49eb6e48a4845def51 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 30 Dec 2018 17:43:19 +0100 Subject: [PATCH 01/10] build using dune (fix #20) --- .travis.yml | 20 +- Makefile | 194 +++---- Makefile.common | 34 -- README.md | 6 +- dune | 7 + dune-project | 2 + elpi.install | 96 ++++ elpi.opam | 12 +- elpi_REPL.ml | 11 +- elpi_REPL_config.mli | 5 - src/Makefile | 102 ---- builtin.elpi => src/builtin.elpi | 3 +- src/dune | 50 ++ elpi-checker.elpi => src/elpi-checker.elpi | 0 src/elpi.ml | 2 + src/elpi.mli | 4 - {utils => src}/elpi2html.elpi | 0 src/elpi_API.ml | 10 +- src/elpi_compiler.ml | 2 +- .../elpi_quoted_syntax.elpi | 0 tests/Makefile | 43 -- tests/suite/suite.ml | 20 +- tests/suite/suite.mli | 2 +- tests/test.ml | 24 +- trace/dune | 18 + {src => trace}/elpi_trace.ml | 28 +- {src => trace}/elpi_trace.mli | 3 + trace_ppx.ml => trace/trace_ppx.ml | 4 +- utils/mathpartir.sty | 492 ------------------ 29 files changed, 319 insertions(+), 875 deletions(-) delete mode 100644 Makefile.common create mode 100644 dune create mode 100644 dune-project create mode 100644 elpi.install delete mode 100644 elpi_REPL_config.mli delete mode 100644 src/Makefile rename builtin.elpi => src/builtin.elpi (99%) create mode 100644 src/dune rename elpi-checker.elpi => src/elpi-checker.elpi (100%) create mode 100644 src/elpi.ml delete mode 100644 src/elpi.mli rename {utils => src}/elpi2html.elpi (100%) rename elpi_quoted_syntax.elpi => src/elpi_quoted_syntax.elpi (100%) delete mode 100644 tests/Makefile create mode 100644 trace/dune rename {src => trace}/elpi_trace.ml (90%) rename {src => trace}/elpi_trace.mli (93%) rename trace_ppx.ml => trace/trace_ppx.ml (97%) delete mode 100644 utils/mathpartir.sty diff --git a/.travis.yml b/.travis.yml index 0811c0459..cb39e161e 100644 --- a/.travis.yml +++ b/.travis.yml @@ -43,9 +43,8 @@ matrix: - eval $(opam env) - opam install -j $JOBS -y $PREDEPS - opam install -j $JOBS -y $DEPS - - make - - make -C tests run - - make byte + - dune build + - make tests - env: TEST="linux build $OCAML_MAX" os: linux @@ -66,9 +65,8 @@ matrix: - eval $(opam env) - opam install -j $JOBS -y $PREDEPS - opam install -j $JOBS -y $DEPS - - make - - make -C tests run - - make byte + - dune build + - make tests - env: TEST="osx build $OCAML_MIN" os: osx @@ -85,9 +83,8 @@ matrix: - eval $(opam env) - opam install -j $JOBS -y $PREDEPS - opam install -j $JOBS -y $DEPS - - make - - make -C tests run - - make byte + - dune build + - make tests - env: TEST="osx build $OCAML_MAX" os: osx @@ -104,9 +101,8 @@ matrix: - eval $(opam env) - opam install -j $JOBS -y $PREDEPS - opam install -j $JOBS -y $DEPS - - make - - make -C tests run - - make byte + - dune build + - make tests - env: TEST="linux opam package installation" os: linux diff --git a/Makefile b/Makefile index a12e5aac1..cf69ab8dc 100644 --- a/Makefile +++ b/Makefile @@ -1,133 +1,65 @@ -# Commands: -# make -- to compile elpi -# make install -- to install elpi using findlib -# make install-bin BIN=path -- to install the elpi REPL in $BIN -# make uninstall -- to remove elpi using findlib -# make uninstall-bin BIN=path -- to remove the elpi REPL in $BIN -# ... BYTE=yes -- to compile/install/remove byte code -# -# make git/V -- to compile elpi.git.V out of git's commit/branch/tag V -# such binary is then picked up automatically by the bench -# system as an elpi like runner -# make runners -- foreach git tag runner-V, do something like make git/V - -BASE=$(shell pwd) -include Makefile.common - -all: check-ocaml-ver elpi$(EXE) builtin.elpi - -byte: - $(H)$(MAKE) BYTE=1 all - -trace_ppx: trace_ppx.ml - $(H)$(call pp,OCAMLOPT,-o,$@) - $(H)ocamlfind ocamlopt \ - -package ppx_tools_versioned \ - -package ppx_tools_versioned.metaquot_404 \ - -package ocaml-migrate-parsetree.driver-main \ - -c $< - $(H)ocamlfind ocamlopt \ - -package ppx_tools_versioned \ - -package ppx_tools_versioned.metaquot_404 \ - -package ocaml-migrate-parsetree \ - -predicates custom_ppx,ppx_driver \ - -linkpkg -linkall \ - trace_ppx.cmx \ - `ocamlfind query -predicates native \ - ocaml-migrate-parsetree.driver-main -a-format` \ - -o $@ - $(H)cp .merlin.in .merlin - $(H)echo "FLG -ppx '$(shell pwd)/trace_ppx --as-ppx'" >> .merlin +help: + @echo 'Known targets:' + @echo + @echo ' build builds elpi' + @echo ' .merlin builds a .merlin' + @echo + @echo ' tests runs the entire test suite' + @echo ' tests ONLY=rex runs only tests matching rex' + @echo + @echo ' git/treeish checkout treeish and build elpi.git.treeish' + @echo + +INSTALL=_build/install/default +BUILD=_build/default +SHELL:=/bin/bash +TIMEOUT=60.0 +RUNNERS=\ + $(shell pwd)/$(INSTALL)/bin/elpi \ + $(addprefix $(shell pwd)/,$(wildcard elpi.git.*)) \ + $(shell if type tjsim >/dev/null 2>&1; then type -P tjsim; else echo; fi) +TIME=--time $(shell if type -P gtime >/dev/null 2>&1; then type -P gtime; else echo /usr/bin/time; fi) +STACK=32768 + +# this is to work around https://github.com/ocaml/dune/issues/1212 +.merlin: + @dune build .merlin + @for ppx in `ls $$PWD/_build/default/.ppx/*/ppx.exe`; do\ + if $$ppx --print-transformations | grep trace; then\ + echo PKG ppx_deriving.std ppx_deriving.runtime >> .merlin;\ + echo FLG -ppx \"$$ppx --as-ppx\" >> .merlin;\ + echo PKG ppx_deriving.std ppx_deriving.runtime >> src/.merlin;\ + echo FLG -ppx \"$$ppx --as-ppx\" >> src/.merlin;\ + fi;\ + done + +build: + dune build @install + $(MAKE) .merlin + + +tests: + dune build $(INSTALL)/bin/elpi + dune build $(BUILD)/tests/test.exe + ulimit -s $(STACK); \ + $(BUILD)/tests/test.exe \ + --seed $$RANDOM \ + --timeout $(TIMEOUT) \ + $(TIME) \ + --sources=$$PWD/tests/sources/ \ + --plot=$$PWD/tests/plot \ + $(addprefix --name-match ,$(ONLY)) \ + $(addprefix --runner , $(RUNNERS)) git/%: - $(H)rm -rf "$$PWD/elpi-$*" - $(H)mkdir "elpi-$*" - $(H)git clone -l . "elpi-$*" - $(H)cd "elpi-$*" && git checkout "$*" && make - $(H)cp "elpi-$*/elpi" "elpi.git.$*" - $(H)rm -rf "$$PWD/elpi-$*" - -runners: - $(H)true $(foreach t,$(shell git branch --list 'runner*' | cut -c 3-),\ - && $(MAKE) git/$(t) && \ - mv elpi.git.$(t) elpi.git.$(t:runner-%=%)) - -clean: - $(H)rm -f $(addprefix src/, $(TRASH)) - $(H)rm -f $(TRASH) - $(H)rm -f trace_ppx.cmx elpi_REPL_config.ml - $(H)rm -f elpi.git.* trace_ppx elpi elpi.byte - $(H)rm -f src/.depends src/.depends.parser - $(H)rm -f src/.depends.byte src/.depends.parser.byte - $(H)rm -rf findlib/ - -dist: - $(H)git archive --format=tar --prefix=elpi-$(V)/ HEAD . \ - | gzip > ../elpi-$(V).tgz - -# compilation of elpi - -OC_OPTIONS = -linkpkg $(OCAMLOPTIONS) $(FLAGS) - -ELPI_LIBS = \ - elpi_quoted_syntax.elpi elpi-checker.elpi \ - utils/elpi2html.elpi - -ELPI_DIST = \ - $(addprefix src/,elpi_API.cmi elpi_API.mli elpi_builtin.cmi elpi_builtin.mli elpi.cmi) - -ELPI_DIST_OPT = \ - $(addprefix src/,elpi.cma elpi.cmxa elpi.a elpi_builtin.cmti elpi_API.cmti elpi_API.cmx elpi_API.cmo elpi_builtin.cmo elpi_builtin.cmx) - -elpi$(EXE): elpi_REPL.ml elpi_REPL_config.$(CMX) findlib/elpi/META - $(H)$(call pp,$(OCNAME),-package elpi elpi_REPL_config.$(CMX) -o $@,$<) - $(H)$(OC) $(OC_OPTIONS) -package elpi elpi_REPL_config.$(CMX) -o $@ $< - -elpi_REPL_config.$(CMX): elpi_REPL_config.ml elpi_REPL_config.cmi - $(H)$(call pp,$(OCNAME),-c, $<) - $(H)$(OC) $(OC_OPTIONS) -c $< - -elpi_REPL_config.cmi: elpi_REPL_config.mli - $(H)$(call pp,$(OCNAME),-c, $<) - $(H)$(OC) $(OC_OPTIONS) -c $< - -builtin.elpi: elpi$(EXE) - $(H)echo '%% File generated by elpi -document-builtins, do not edit' > $@ - $(H)./elpi -document-builtins >> $@ - -elpi_REPL_config.ml: - $(H)echo 'let install_dir = "$(shell ocamlfind printconf destdir)/elpi"' > $@ - -src/%: | trace_ppx - $(H)$(MAKE) --no-print-directory -C src/ $* - -src/elpi.$(CMXA): $(wildcard src/*.ml) $(wildcard src/*.mli) -findlib/elpi/META: src/elpi.$(CMXA) Makefile - $(H)rm -rf findlib/; mkdir findlib - $(H)$(MAKE) --no-print-directory -C src/ elpi.cmi # needed by ELPI_DIST - $(H)ocamlfind install -destdir $(BASE)/findlib -patch-archives \ - elpi META $(ELPI_DIST) $(ELPI_LIBS) \ - -optional $(ELPI_DIST_OPT) - -install: - $(H)ocamlfind install -patch-archives \ - elpi META $(ELPI_DIST) $(ELPI_LIBS) \ - -optional $(ELPI_DIST_OPT) elpi elpi.byte -install-bin: - $(H)cp elpi$(EXE) $(BIN) - -uninstall: - $(H)ocamlfind remove elpi -uninstall-bin: - $(H)rm -f $(BIN)/elpi$(EXE) - - -# required OCaml package -check-ocaml-ver: - $(H)ocamlfind query camlp5 > /dev/null - $(H)ocamlfind query ppx_tools_versioned > /dev/null - $(H)ocamlfind query ppx_deriving > /dev/null - $(H)ocamlfind query ocaml-migrate-parsetree.driver-main > /dev/null - $(H)ocamlfind query re.str > /dev/null - -.NOTPARALLEL: + rm -rf "$$PWD/elpi-$*" + mkdir "elpi-$*" + git clone -l . "elpi-$*" + cd "elpi-$*" && git checkout "$*" + cd "elpi-$*" && \ + if [ -f dune ]; then dune build --root . @install; else make; fi + cp "elpi-$*/elpi" "elpi.git.$*" || \ + cp "elpi-$*/$(INSTALL)/bin/elpi" "elpi.git.$*" + rm -rf "$$PWD/elpi-$*" + +.PHONY: tests help .merlin diff --git a/Makefile.common b/Makefile.common deleted file mode 100644 index 7e3b242ab..000000000 --- a/Makefile.common +++ /dev/null @@ -1,34 +0,0 @@ -# We expect the user to define BASE to the root of the repo - -V=$(shell git describe --tags) -PP=camlp5o -I . -I +camlp5 -PARSE=pa_extend.cmo pa_lexer.cmo -FLAGS=-I $(shell camlp5 -where) -w +a -OCAMLOPTIONS= -g -bin-annot -OD=ocamlfind ocamldep - -ifeq "$(BYTE)" "" -CMX=cmx -CMXA=cmxa -EXE= -OC=ocamlfind ocamlopt -DEPS=.depends .depends.parser -OCNAME=OCAMLOPT -OOPAQUE= -else -CMX=cmo -CMXA=cma -EXE=.byte -OC=ocamlfind ocamlc -DEPS=.depends.byte .depends.parser.byte -OCNAME=OCAMLC -OOPAQUE= -endif - -ifeq "$(findstring install,$(MAKECMDGOALS))$(findstring uninstall,$(MAKECMDGOALS))" "" -OCAMLPATH:=$(BASE)/findlib:$(OCAMLPATH) -export OCAMLPATH -endif -H=@ -pp = printf '$(1) %-26s %s\n' "$(3)" "$(2)" -TRASH=*.cmo *.cma *.cmx *.cmxa *.cmi *.o *.a *.cmt *.cmti diff --git a/README.md b/README.md index b6bb180d2..29de900fe 100644 --- a/README.md +++ b/README.md @@ -27,8 +27,7 @@ you can type ``` opam pin add elpi https://github.com/LPCIC/elpi.git ``` -You can also clone this repository and type `make`. The build requirements -are listed at the end of the [Makefile](Makefile) +You can also clone this repository and type `dune build`. ### Syntax highlight in Visual studio code @@ -79,7 +78,7 @@ by Miller and Nadathur is highly recommended and covers standard λProlog. The extensions to λProlog implemented in ELPI are described in the [ELPI](ELPI.md) file, built-in predicates are documented in -[builtin](builtin.elpi). +[builtin](src/builtin.elpi). There is a [short paper](https://hal.inria.fr/hal-01176856/) describing the implementation of the interpreter, in particular how it deals with @@ -167,3 +166,4 @@ The programming language has the following features Most of these feature come with λProlog. Constraints and propagation rules are novel in ELPI. + diff --git a/dune b/dune new file mode 100644 index 000000000..6e308ec29 --- /dev/null +++ b/dune @@ -0,0 +1,7 @@ +(executable + (name elpi_REPL) + (public_name elpi) + (libraries elpi) + (modules elpi_REPL) +) + diff --git a/dune-project b/dune-project new file mode 100644 index 000000000..bb48ee3e8 --- /dev/null +++ b/dune-project @@ -0,0 +1,2 @@ +(lang dune 1.6) +(name "elpi") diff --git a/elpi.install b/elpi.install new file mode 100644 index 000000000..eac261bef --- /dev/null +++ b/elpi.install @@ -0,0 +1,96 @@ +lib: [ + "_build/install/default/lib/elpi/.private/elpi__Elpi_ast.cmi" {".private/elpi__Elpi_ast.cmi"} + "_build/install/default/lib/elpi/.private/elpi__Elpi_compiler.cmi" {".private/elpi__Elpi_compiler.cmi"} + "_build/install/default/lib/elpi/.private/elpi__Elpi_data.cmi" {".private/elpi__Elpi_data.cmi"} + "_build/install/default/lib/elpi/.private/elpi__Elpi_parser.cmi" {".private/elpi__Elpi_parser.cmi"} + "_build/install/default/lib/elpi/.private/elpi__Elpi_ptmap.cmi" {".private/elpi__Elpi_ptmap.cmi"} + "_build/install/default/lib/elpi/.private/elpi__Elpi_runtime_trace_off.cmi" {".private/elpi__Elpi_runtime_trace_off.cmi"} + "_build/install/default/lib/elpi/.private/elpi__Elpi_runtime_trace_on.cmi" {".private/elpi__Elpi_runtime_trace_on.cmi"} + "_build/install/default/lib/elpi/.private/elpi__Elpi_util.cmi" {".private/elpi__Elpi_util.cmi"} + "_build/install/default/lib/elpi/META" {"META"} + "_build/install/default/lib/elpi/builtin.elpi" + "_build/install/default/lib/elpi/dune-package" {"dune-package"} + "_build/install/default/lib/elpi/elpi-checker.elpi" + "_build/install/default/lib/elpi/elpi.a" {"elpi.a"} + "_build/install/default/lib/elpi/elpi.cma" {"elpi.cma"} + "_build/install/default/lib/elpi/elpi.cmi" {"elpi.cmi"} + "_build/install/default/lib/elpi/elpi.cmt" {"elpi.cmt"} + "_build/install/default/lib/elpi/elpi.cmx" {"elpi.cmx"} + "_build/install/default/lib/elpi/elpi.cmxa" {"elpi.cmxa"} + "_build/install/default/lib/elpi/elpi.cmxs" {"elpi.cmxs"} + "_build/install/default/lib/elpi/elpi.ml" {"elpi.ml"} + "_build/install/default/lib/elpi/elpi2html.elpi" + "_build/install/default/lib/elpi/elpi_API.ml" {"elpi_API.ml"} + "_build/install/default/lib/elpi/elpi_API.mli" {"elpi_API.mli"} + "_build/install/default/lib/elpi/elpi__.cmi" {"elpi__.cmi"} + "_build/install/default/lib/elpi/elpi__.cmt" {"elpi__.cmt"} + "_build/install/default/lib/elpi/elpi__.cmx" {"elpi__.cmx"} + "_build/install/default/lib/elpi/elpi__.ml" {"elpi__.ml"} + "_build/install/default/lib/elpi/elpi__Elpi_API.cmi" {"elpi__Elpi_API.cmi"} + "_build/install/default/lib/elpi/elpi__Elpi_API.cmt" {"elpi__Elpi_API.cmt"} + "_build/install/default/lib/elpi/elpi__Elpi_API.cmti" {"elpi__Elpi_API.cmti"} + "_build/install/default/lib/elpi/elpi__Elpi_API.cmx" {"elpi__Elpi_API.cmx"} + "_build/install/default/lib/elpi/elpi__Elpi_ast.cmt" {"elpi__Elpi_ast.cmt"} + "_build/install/default/lib/elpi/elpi__Elpi_ast.cmti" {"elpi__Elpi_ast.cmti"} + "_build/install/default/lib/elpi/elpi__Elpi_ast.cmx" {"elpi__Elpi_ast.cmx"} + "_build/install/default/lib/elpi/elpi__Elpi_builtin.cmi" {"elpi__Elpi_builtin.cmi"} + "_build/install/default/lib/elpi/elpi__Elpi_builtin.cmt" {"elpi__Elpi_builtin.cmt"} + "_build/install/default/lib/elpi/elpi__Elpi_builtin.cmti" {"elpi__Elpi_builtin.cmti"} + "_build/install/default/lib/elpi/elpi__Elpi_builtin.cmx" {"elpi__Elpi_builtin.cmx"} + "_build/install/default/lib/elpi/elpi__Elpi_compiler.cmt" {"elpi__Elpi_compiler.cmt"} + "_build/install/default/lib/elpi/elpi__Elpi_compiler.cmti" {"elpi__Elpi_compiler.cmti"} + "_build/install/default/lib/elpi/elpi__Elpi_compiler.cmx" {"elpi__Elpi_compiler.cmx"} + "_build/install/default/lib/elpi/elpi__Elpi_data.cmt" {"elpi__Elpi_data.cmt"} + "_build/install/default/lib/elpi/elpi__Elpi_data.cmx" {"elpi__Elpi_data.cmx"} + "_build/install/default/lib/elpi/elpi__Elpi_parser.cmt" {"elpi__Elpi_parser.cmt"} + "_build/install/default/lib/elpi/elpi__Elpi_parser.cmti" {"elpi__Elpi_parser.cmti"} + "_build/install/default/lib/elpi/elpi__Elpi_parser.cmx" {"elpi__Elpi_parser.cmx"} + "_build/install/default/lib/elpi/elpi__Elpi_ptmap.cmt" {"elpi__Elpi_ptmap.cmt"} + "_build/install/default/lib/elpi/elpi__Elpi_ptmap.cmti" {"elpi__Elpi_ptmap.cmti"} + "_build/install/default/lib/elpi/elpi__Elpi_ptmap.cmx" {"elpi__Elpi_ptmap.cmx"} + "_build/install/default/lib/elpi/elpi__Elpi_runtime_trace_off.cmt" {"elpi__Elpi_runtime_trace_off.cmt"} + "_build/install/default/lib/elpi/elpi__Elpi_runtime_trace_off.cmti" {"elpi__Elpi_runtime_trace_off.cmti"} + "_build/install/default/lib/elpi/elpi__Elpi_runtime_trace_off.cmx" {"elpi__Elpi_runtime_trace_off.cmx"} + "_build/install/default/lib/elpi/elpi__Elpi_runtime_trace_on.cmt" {"elpi__Elpi_runtime_trace_on.cmt"} + "_build/install/default/lib/elpi/elpi__Elpi_runtime_trace_on.cmti" {"elpi__Elpi_runtime_trace_on.cmti"} + "_build/install/default/lib/elpi/elpi__Elpi_runtime_trace_on.cmx" {"elpi__Elpi_runtime_trace_on.cmx"} + "_build/install/default/lib/elpi/elpi__Elpi_util.cmt" {"elpi__Elpi_util.cmt"} + "_build/install/default/lib/elpi/elpi__Elpi_util.cmti" {"elpi__Elpi_util.cmti"} + "_build/install/default/lib/elpi/elpi__Elpi_util.cmx" {"elpi__Elpi_util.cmx"} + "_build/install/default/lib/elpi/elpi_ast.ml" {"elpi_ast.ml"} + "_build/install/default/lib/elpi/elpi_ast.mli" {"elpi_ast.mli"} + "_build/install/default/lib/elpi/elpi_builtin.ml" {"elpi_builtin.ml"} + "_build/install/default/lib/elpi/elpi_builtin.mli" {"elpi_builtin.mli"} + "_build/install/default/lib/elpi/elpi_compiler.ml" {"elpi_compiler.ml"} + "_build/install/default/lib/elpi/elpi_compiler.mli" {"elpi_compiler.mli"} + "_build/install/default/lib/elpi/elpi_data.ml" {"elpi_data.ml"} + "_build/install/default/lib/elpi/elpi_parser.ml" {"elpi_parser.ml"} + "_build/install/default/lib/elpi/elpi_parser.mli" {"elpi_parser.mli"} + "_build/install/default/lib/elpi/elpi_ptmap.ml" {"elpi_ptmap.ml"} + "_build/install/default/lib/elpi/elpi_ptmap.mli" {"elpi_ptmap.mli"} + "_build/install/default/lib/elpi/elpi_quoted_syntax.elpi" + "_build/install/default/lib/elpi/elpi_runtime_trace_off.ml" {"elpi_runtime_trace_off.ml"} + "_build/install/default/lib/elpi/elpi_runtime_trace_off.mli" {"elpi_runtime_trace_off.mli"} + "_build/install/default/lib/elpi/elpi_runtime_trace_on.ml" {"elpi_runtime_trace_on.ml"} + "_build/install/default/lib/elpi/elpi_runtime_trace_on.mli" {"elpi_runtime_trace_on.mli"} + "_build/install/default/lib/elpi/elpi_trace/elpi_trace.a" {"elpi_trace/elpi_trace.a"} + "_build/install/default/lib/elpi/elpi_trace/elpi_trace.cma" {"elpi_trace/elpi_trace.cma"} + "_build/install/default/lib/elpi/elpi_trace/elpi_trace.cmi" {"elpi_trace/elpi_trace.cmi"} + "_build/install/default/lib/elpi/elpi_trace/elpi_trace.cmt" {"elpi_trace/elpi_trace.cmt"} + "_build/install/default/lib/elpi/elpi_trace/elpi_trace.cmti" {"elpi_trace/elpi_trace.cmti"} + "_build/install/default/lib/elpi/elpi_trace/elpi_trace.cmx" {"elpi_trace/elpi_trace.cmx"} + "_build/install/default/lib/elpi/elpi_trace/elpi_trace.cmxa" {"elpi_trace/elpi_trace.cmxa"} + "_build/install/default/lib/elpi/elpi_trace/elpi_trace.cmxs" {"elpi_trace/elpi_trace.cmxs"} + "_build/install/default/lib/elpi/elpi_trace/elpi_trace.ml" {"elpi_trace/elpi_trace.ml"} + "_build/install/default/lib/elpi/elpi_trace/elpi_trace.mli" {"elpi_trace/elpi_trace.mli"} + "_build/install/default/lib/elpi/elpi_util.ml" {"elpi_util.ml"} + "_build/install/default/lib/elpi/elpi_util.mli" {"elpi_util.mli"} + "_build/install/default/lib/elpi/opam" {"opam"} +] +bin: [ + "_build/install/default/bin/elpi" {"elpi"} +] +doc: [ + "_build/install/default/doc/elpi/LICENSE" + "_build/install/default/doc/elpi/README.md" +] diff --git a/elpi.opam b/elpi.opam index 86ad68592..784c45c90 100644 --- a/elpi.opam +++ b/elpi.opam @@ -8,11 +8,13 @@ doc: "https://github.com/LPCIC/elpi" dev-repo: "git+https://github.com/LPCIC/elpi.git" bug-reports: "https://github.com/LPCIC/elpi/issues" -build: [ [ make ] [ make "byte" ] ] -run-test: [ make "-C" "tests" "run" "RUNNERS=../elpi" ] +build: [ + [ "dune" "subst" {pinned} ] + [ "dune" "build" "-p" name "-j" jobs ] +] +run-test: [ make "tests" ] install: [ - [ make "install" ] - [ make "install-bin" "BIN=%{bin}%" ] + [ "dune" "install" "-p" name ] ] depends: [ @@ -25,7 +27,7 @@ depends: [ "re" {>= "1.7.2"} "ANSITerminal" {with-test} "cmdliner" {with-test} - "dune" {with-test} + "dune" {build} "conf-time" {with-test} ] synopsis: "ELPI - Embeddable λProlog Interpreter" diff --git a/elpi_REPL.ml b/elpi_REPL.ml index af782329c..738a6165a 100644 --- a/elpi_REPL.ml +++ b/elpi_REPL.ml @@ -12,6 +12,7 @@ let _ = Gc.set tweaked_control ;; *) +open Elpi module Str = Re.Str @@ -55,7 +56,6 @@ let usage = "\nMain options:\n" ^ "\t-test runs the query \"main\"\n" ^ "\t-exec pred runs the query \"pred ARGS\"\n" ^ - "\t-where print system wide installation path then exit\n" ^ "\t-D var Define variable (conditional compilation)\n" ^ "\t-document-builtins Print documentation for built-in predicates\n" ^ "\t-no-tc don't typecheck the program\n" ^ @@ -88,8 +88,6 @@ let _ = let print_accumulated_files = ref false in let vars = ref Elpi_API.Compile.(default_flags.defined_variables) in - if List.mem "-where" (Array.to_list Sys.argv) then begin - Printf.printf "%s\n" Elpi_REPL_config.install_dir; exit 0 end; let rec aux = function | [] -> [] | "-delay-problems-outside-pattern-fragment" :: rest -> delay_outside_fragment := true; aux rest @@ -115,7 +113,12 @@ let _ = let v = try Sys.getenv "TJPATH" with Not_found -> "" in let tjpath = Str.split (Str.regexp ":") v in List.flatten (List.map (fun x -> ["-I";x]) tjpath) in - let installpath = [ "-I"; Elpi_REPL_config.install_dir ] in + let installpath = + let v = try Sys.getenv "OCAMLPATH" with Not_found -> "" in + let ocamlpath = + (Filename.dirname Sys.executable_name ^ "/../lib") :: + Str.split (Str.regexp ":") v in + List.flatten (List.map (fun x -> ["-I";x^"/elpi/"]) ocamlpath) in let execpath = ["-I"; Filename.dirname (Sys.executable_name)] in let opts = Array.to_list Sys.argv @ tjpath @ installpath @ execpath in let pheader, argv = Elpi_API.Setup.init ~builtins:Elpi_builtin.std_builtins opts ~basedir:cwd in diff --git a/elpi_REPL_config.mli b/elpi_REPL_config.mli deleted file mode 100644 index 9d93c1627..000000000 --- a/elpi_REPL_config.mli +++ /dev/null @@ -1,5 +0,0 @@ -(* elpi: embedded lambda prolog interpreter *) -(* license: GNU Lesser General Public License Version 2.1 or later *) -(* ------------------------------------------------------------------------- *) - -val install_dir : string diff --git a/src/Makefile b/src/Makefile deleted file mode 100644 index a20bf78e1..000000000 --- a/src/Makefile +++ /dev/null @@ -1,102 +0,0 @@ -# Overview of the build process: -# - trace_ppx defines [%spy] and [%trace] used _only_ in elpi_runtime.ml -# - elpi_runtime.ml is compiled twice -# - with -for-pack Elpi_runtime_trace_off and passing --off to trace_ppx, -# then it is immediately packed to elpi_runtime_trace_off.cm[x]o -# - with -for-pack Elpi_runtime_trace_on and passing --on to trace_ppx, -# then it is immediately packed to elpi_runtime_trace_on.cm[x]o -# - both runtimes are linked, and elpi_API.ml switches between the two -# using first class modules -# - elpi_parser.ml uses camlp5 syntax extensions for describing extensible -# grammars and lexers - -BASE=$(shell pwd)/.. -include ../Makefile.common - -# Compilation with trace_ppx and -pack -ELPI_PACKED_COMPONENTS = \ - elpi_runtime_trace_on.$(CMX) elpi_runtime_trace_off.$(CMX) - -# Compilation with camlp5 preprocessing -ELPI_P5_COMPONENTS = elpi_parser.$(CMX) - -# All files linked in the .cma -ELPI_COMPONENTS = \ - elpi_util.$(CMX) \ - elpi_trace.$(CMX) \ - elpi_ast.$(CMX) $(ELPI_P5_COMPONENTS) elpi_ptmap.$(CMX) \ - elpi_data.$(CMX) \ - $(ELPI_PACKED_COMPONENTS) elpi_compiler.$(CMX) \ - elpi_API.$(CMX) elpi_builtin.$(CMX) - -# Standard compilation -ELPI_EASY_COMPONENTS = \ - $(filter-out $(ELPI_PACKED_COMPONENTS), \ - $(filter-out $(ELPI_P5_COMPONENTS), $(ELPI_COMPONENTS))) - -elpi.$(CMXA): $(ELPI_COMPONENTS) - $(H)$(call pp,$(OCNAME),-a -o $@,*.$(CMX)) - $(H)$(OC) $(OC_OPTIONS) -o $@ -a $(ELPI_COMPONENTS) - -elpi_runtime_trace_on.$(CMX) elpi_runtime_trace_off.$(CMX) : elpi_runtime.ml elpi_runtime.cmi ../trace_ppx - $(H)$(call pp,$(OCNAME),-c -ppx 'trace_ppx --on' -for-pack -w -55,$<) - $(H)$(OC) $(OCAMLOPTIONS) \ - -package camlp5,ppx_deriving.std \ - -ppx '../trace_ppx --as-ppx --on' -w -55 \ - -for-pack Elpi_runtime_trace_on \ - -c $< - $(H)$(OC) $(OCAMLOPTIONS) \ - -pack elpi_runtime.$(CMX) -o elpi_runtime_trace_on.$(CMX) - $(H)rm elpi_runtime.$(CMX) - $(H)$(call pp,$(OCNAME),-c -ppx 'trace_ppx --off' -for-pack -w +55,$<) - $(H)$(OC) $(OCAMLOPTIONS) \ - -package camlp5,ppx_deriving.std \ - -ppx '../trace_ppx --as-ppx --off' -w +55 -warn-error +55 \ - -for-pack Elpi_runtime_trace_off \ - -c $< - $(H)$(OC) $(OCAMLOPTIONS) \ - -pack elpi_runtime.$(CMX) -o elpi_runtime_trace_off.$(CMX) - $(H)rm elpi_runtime.$(CMX) - -$(ELPI_EASY_COMPONENTS) : %.$(CMX): %.ml - $(H)$(call pp,$(OCNAME),-c,$<) - $(H)$(OC) $(OCAMLOPTIONS) \ - -package camlp5,ppx_deriving.std,re.str \ - -c $< - -elpi_API.cmi: elpi_API.mli - $(H)$(call pp,$(OCNAME),$(OOPAQUE) -c,$<) - $(H)$(OC) $(OCAMLOPTIONS) -package camlp5 $(OOPAQUE) -c $< -elpi_builtin.cmi: elpi_builtin.mli - $(H)$(call pp,$(OCNAME),$(OOPAQUE) -c,$<) - $(H)$(OC) $(OCAMLOPTIONS) -package camlp5 $(OOPAQUE) -c $< -%.cmi: %.mli - $(H)$(call pp,$(OCNAME),-c,$<) - $(H)$(OC) $(OCAMLOPTIONS) -package camlp5 -c $< - -elpi_parser.$(CMX): elpi_parser.ml elpi_parser.cmi elpi_ast.$(CMX) elpi_ast.cmi - $(H)$(call pp,$(OCNAME),-c -pp camlp5o,$<) - $(H)$(OC) $(OCAMLOPTIONS) -pp '$(PP) $(PARSE)' -package re.str $(FLAGS) -w -27 -o $@ -c $< - -# dependencies -include $(DEPS) - -.depends: $(filter-out elpi_parser.ml, $(wildcard *.ml *.mli)) - $(H)$(call pp,OCAMLDEP,-native,$@) - $(H)$(OD) -native $^ > $@ -.depends.parser: elpi_parser.ml - $(H)$(call pp,OCAMLDEP,-native,$@) - $(H)$(OD) -native -pp '$(PP) $(PARSE)' $< > $@ -.depends.byte: $(filter-out elpi_parser.ml, $(wildcard *.ml *.mli)) - $(H)$(call pp,OCAMLDEP,,$@) - $(H)$(OD) $^ > $@ -.depends.parser.byte: elpi_parser.ml - $(H)$(call pp,OCAMLDEP,,$@) - $(H)$(OD) -pp '$(PP) $(PARSE)' $< > $@ -# Not detected by ocamldep -elpi_runtime_trace_on.$(CMX) : elpi_util.$(CMX) elpi_data.$(CMX) elpi_ptmap.$(CMX) elpi_parser.$(CMX) elpi_ast.$(CMX) elpi_trace.$(CMX) elpi_runtime.cmi -elpi_runtime_trace_off.$(CMX) : elpi_util.$(CMX) elpi_data.$(CMX) elpi_ptmap.$(CMX) elpi_parser.$(CMX) elpi_ast.$(CMX) elpi_trace.$(CMX) elpi_runtime.cmi -elpi_API.$(CMX): elpi_runtime_trace_on.$(CMX) elpi_runtime_trace_off.$(CMX) -elpi_compiler.$(CMX): elpi_runtime_trace_on.$(CMX) elpi_runtime_trace_off.$(CMX) - -.NOTPARALLEL: diff --git a/builtin.elpi b/src/builtin.elpi similarity index 99% rename from builtin.elpi rename to src/builtin.elpi index f3e035593..f2f7dd9ae 100644 --- a/builtin.elpi +++ b/src/builtin.elpi @@ -1,5 +1,4 @@ -%% File generated by elpi -document-builtins, do not edit - +% File generated by elpi -document-builtins, do not edit % == Core builtins ===================================== diff --git a/src/dune b/src/dune new file mode 100644 index 000000000..e12bf567f --- /dev/null +++ b/src/dune @@ -0,0 +1,50 @@ +(library + (name elpi) + (public_name elpi) + (preprocess (per_module + ((pps ppx_deriving.std) elpi_API elpi_util elpi_ast elpi_data elpi_compiler) + ((pps ppx_deriving.std trace_ppx --trace_ppx-on) elpi_runtime_trace_on) + ((pps ppx_deriving.std trace_ppx --trace_ppx-off) elpi_runtime_trace_off) + ((action (system "camlp5o -I . -I +camlp5 pa_extend.cmo pa_lexer.cmo %{input-file}")) elpi_parser) + )) + (libraries re.str camlp5.gramlib unix) + (flags -linkall) + (modules elpi elpi_util elpi_parser elpi_ast elpi_compiler elpi_data elpi_ptmap elpi_builtin elpi_API elpi_runtime_trace_on elpi_runtime_trace_off) + (private_modules elpi_util elpi_parser elpi_ast elpi_compiler elpi_data elpi_ptmap elpi_runtime_trace_on elpi_runtime_trace_off) +) + +(rule + (targets elpi_runtime_trace_on.ml) + (deps elpi_runtime.ml) + (action (copy# %{deps} %{targets})) +) +(rule + (targets elpi_runtime_trace_on.mli) + (deps elpi_runtime.mli) + (action (copy# %{deps} %{targets})) +) + +(rule + (targets elpi_runtime_trace_off.ml) + (deps elpi_runtime.ml) + (action (copy# %{deps} %{targets})) +) +(rule + (targets elpi_runtime_trace_off.mli) + (deps elpi_runtime.mli) + (action (copy# %{deps} %{targets})) +) + +(install + (section lib) + (files builtin.elpi elpi-checker.elpi elpi_quoted_syntax.elpi elpi2html.elpi) +) + +(rule + (targets builtin.elpi) + (mode promote) + (action (with-stdout-to %{targets} + (progn + (echo "% File generated by elpi -document-builtins, do not edit") + (run elpi -document-builtins)))) +) diff --git a/elpi-checker.elpi b/src/elpi-checker.elpi similarity index 100% rename from elpi-checker.elpi rename to src/elpi-checker.elpi diff --git a/src/elpi.ml b/src/elpi.ml new file mode 100644 index 000000000..93e7659e3 --- /dev/null +++ b/src/elpi.ml @@ -0,0 +1,2 @@ +module Elpi_API = Elpi_API +module Elpi_builtin = Elpi_builtin diff --git a/src/elpi.mli b/src/elpi.mli deleted file mode 100644 index 0739863ab..000000000 --- a/src/elpi.mli +++ /dev/null @@ -1,4 +0,0 @@ -(* elpi: embedded lambda prolog interpreter *) -(* license: GNU Lesser General Public License Version 2.1 or later *) -(* ------------------------------------------------------------------------- *) - diff --git a/utils/elpi2html.elpi b/src/elpi2html.elpi similarity index 100% rename from utils/elpi2html.elpi rename to src/elpi2html.elpi diff --git a/src/elpi_API.ml b/src/elpi_API.ml index 9c685592c..d311a99b5 100644 --- a/src/elpi_API.ml +++ b/src/elpi_API.ml @@ -2,13 +2,13 @@ (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) -module type Runtime = module type of Elpi_runtime_trace_off.Elpi_runtime +module type Runtime = module type of Elpi_runtime_trace_off -let r = ref (module Elpi_runtime_trace_off.Elpi_runtime : Runtime) +let r = ref (module Elpi_runtime_trace_off : Runtime) let set_runtime = function - | true -> r := (module Elpi_runtime_trace_on.Elpi_runtime : Runtime) - | false -> r := (module Elpi_runtime_trace_off.Elpi_runtime : Runtime) + | true -> r := (module Elpi_runtime_trace_on : Runtime) + | false -> r := (module Elpi_runtime_trace_off : Runtime) let set_trace argv = let args = Elpi_trace.parse_argv argv in @@ -739,4 +739,4 @@ module RawPp = struct R.Pp.ppterm depth [] 0 Elpi_data.empty_env fmt t let show_term = Elpi_data.show_term end -end \ No newline at end of file +end diff --git a/src/elpi_compiler.ml b/src/elpi_compiler.ml index 54a9eee10..88c45d8ff 100644 --- a/src/elpi_compiler.ml +++ b/src/elpi_compiler.ml @@ -6,7 +6,7 @@ open Elpi_util module Ast = Elpi_ast module F = Ast.Func -module R = Elpi_runtime_trace_off.Elpi_runtime +module R = Elpi_runtime_trace_off type flags = { defined_variables : StrSet.t; diff --git a/elpi_quoted_syntax.elpi b/src/elpi_quoted_syntax.elpi similarity index 100% rename from elpi_quoted_syntax.elpi rename to src/elpi_quoted_syntax.elpi diff --git a/tests/Makefile b/tests/Makefile deleted file mode 100644 index 4a6073682..000000000 --- a/tests/Makefile +++ /dev/null @@ -1,43 +0,0 @@ -SHELL:=/bin/bash -TIMEOUT=60.0 -RUNNERS=$(shell type -P ../elpi $(wildcard ../elpi.*)) $(shell if type tjsim >/dev/null 2>&1; then type -P tjsim; else echo; fi) -TIME=--time $(shell if type -P gtime >/dev/null 2>&1; then type -P gtime; else echo /usr/bin/time; fi) -BUILD=_build/default/ -STACK=32768 - -help: - @echo 'Known targets:' - @echo - @echo ' build build the test utility' - @echo ' man manpage of the test utility' - @echo - @echo ' run runs the entire test suite' - @echo ' run ONLY=rex runs only tests matching rex' - @echo - @echo ' clean purges _build _log and plots' - @echo - @echo 'Known runners:' - @echo - @echo ' ' $(RUNNERS) - - -build: .merlin - @dune build ./test.exe - -man: build - @$(BUILD)test.exe --help - -run: build - ulimit -s $(STACK); $(BUILD)test.exe \ - --seed $$RANDOM \ - --timeout $(TIMEOUT) \ - $(TIME) \ - $(addprefix --name-match ,$(ONLY)) \ - $(addprefix --runner , $(RUNNERS)) - -.merlin: dune - @dune build .merlin - -clean: - rm -rf _log _build data.csv data.csv.dat data.csv.svg data.csv.plot - diff --git a/tests/suite/suite.ml b/tests/suite/suite.ml index 5d4a0dd2c..ee9ea9314 100644 --- a/tests/suite/suite.ml +++ b/tests/suite/suite.ml @@ -86,7 +86,7 @@ type 'a output = | Done of 'a type run = - executable:string -> timetool:string -> timeout:float -> env:string array -> + executable:string -> timetool:string -> timeout:float -> env:string array -> sources:string -> Test.t -> result output (* Some tests are only for teyjus/elpi *) @@ -104,7 +104,7 @@ let declare ~applicable ~run = type job = { executable : string; test : Test.t; - run : timeout:float -> env:string array -> result output; + run : timeout:float -> env:string array -> sources:string -> result output; } let (||>) l f = List.(concat (map f l)) @@ -247,18 +247,18 @@ let () = Runner.declare if is_elpi executable && source_elpi <> None then Runner.Can_run_it else Runner.Not_for_me end - ~run:begin fun ~executable ~timetool ~timeout ~env test -> + ~run:begin fun ~executable ~timetool ~timeout ~env ~sources test -> let source = match test.Test.source_elpi with Some x -> x | _ -> assert false in if not (Sys.file_exists executable) then Runner.Skipped - else if not (Sys.file_exists ("sources/"^source)) then Runner.Skipped + else if not (Sys.file_exists (sources^source)) then Runner.Skipped else let log = Util.open_log ~executable test in Util.write log (Printf.sprintf "executable: %s\n" executable); let { Test.expectation; input; outside_llam ; _ } = test in - let input = Util.option_map (fun x -> "sources/"^x) input in - let args = ["-test";"-no-tc";"-I";"sources";source] in + let input = Util.option_map (fun x -> sources^x) input in + let args = ["-test";"-no-tc";"-I";sources;source] in let args = if outside_llam then "-delay-problems-outside-pattern-fragment"::args else args in @@ -301,16 +301,16 @@ let is_tjsim = if is_tjsim executable && source_teyjus <> None then Runner.Can_run_it else Runner.Not_for_me end - ~run:begin fun ~executable ~timetool ~timeout ~env test -> + ~run:begin fun ~executable ~timetool ~timeout ~env ~sources test -> let source = - match test.Test.source_teyjus with Some x -> "sources/"^x | _ -> assert false in + match test.Test.source_teyjus with Some x -> sources^x | _ -> assert false in if not (Sys.file_exists executable) then Runner.Skipped else if not (Sys.file_exists source) then Runner.Skipped else let log = Util.open_log ~executable test in let { Test.expectation; input; _ } = test in - let input = Util.option_map (fun x -> "sources/"^x) input in + let input = Util.option_map (fun x -> sources^x) input in let tjcc = Filename.dirname executable ^ "/tjcc" in let tjlink = Filename.dirname executable ^ "/tjlink" in @@ -328,7 +328,7 @@ let is_tjsim = Unix.chdir old; dir, modname in - List.iter (fun x -> ignore (do1 tjcc ("sources/"^x))) + List.iter (fun x -> ignore (do1 tjcc (sources^x))) test.Test.deps_teyjus; let _ = do1 tjcc source in diff --git a/tests/suite/suite.mli b/tests/suite/suite.mli index f367fdda7..77cce627b 100644 --- a/tests/suite/suite.mli +++ b/tests/suite/suite.mli @@ -63,7 +63,7 @@ type 'a output = type job = { executable : string; test : Test.t; - run : timeout:float -> env:string array -> result output; + run : timeout:float -> env:string array -> sources:string -> result output; } val jobs : timetool:string -> executables:string list -> Test.t -> job list diff --git a/tests/test.ml b/tests/test.ml index 36b137773..b2b72cf98 100644 --- a/tests/test.ml +++ b/tests/test.ml @@ -51,7 +51,7 @@ let print_summary ~total ~ok ~ko ~skipped = end -let run timeout _seed env { Runner.run; test; executable } = +let run timeout _seed sources env { Runner.run; test; executable } = let { Test.name; description; _ } = test in let print = Printer.print ~executable:(Filename.basename executable) ~name ~description in @@ -59,7 +59,7 @@ let run timeout _seed env { Runner.run; test; executable } = print 0.0 0.0 0 `RUNNING; ANSITerminal.move_bol (); - let rc = match run ~timeout ~env with + let rc = match run ~timeout ~env ~sources with | Runner.Skipped -> print 0.0 0.0 0 `SKIPPED; None | Runner.Done ({ Runner.rc; _ } as x) -> begin match rc with @@ -75,7 +75,7 @@ let run timeout _seed env { Runner.run; test; executable } = ANSITerminal.printf [] "\n%!"; rc -let print_csv results = +let print_csv plot results = let oc = open_out "data.csv" in results |> List.iter (function @@ -89,12 +89,12 @@ let print_csv results = end | None -> ()); close_out oc; - ignore(Sys.command "./plot data.csv"); + ignore(Sys.command (plot ^ " data.csv")); ignore(Sys.command "gnuplot data.csv.plot") ;; -let main timeout executables namef timetool seed = +let main sources plot timeout executables namef timetool seed = Random.init seed; let filter_name = let rex = Str.regexp (".*"^namef) in @@ -107,7 +107,7 @@ let main timeout executables namef timetool seed = tests |> List.map (Suite.Runner.jobs ~timetool ~executables) |> List.concat in let results = - List.map (run timeout seed env) jobs in + List.map (run timeout seed sources env) jobs in let total, ok, ko, skipped = let skip, rest = List.partition (function None -> true | _ -> false) results in @@ -117,7 +117,7 @@ let main timeout executables namef timetool seed = | _ -> false) rest in List.(length jobs, length ok, length ko, length skip) in Printer.print_summary ~total ~ok ~ko ~skipped; - if List.length executables > 1 then print_csv results; + if List.length executables > 1 then print_csv plot results; if ko = 0 then exit 0 else exit 1 open Cmdliner @@ -138,6 +138,14 @@ let timeout = let doc = "Uses $(docv) as the timeout (in seconds)." in Arg.(value & opt float 30.0 & info ["timeout"] ~docv:"FLOAT" ~doc) +let src = + let doc = "Looks for the sources in $(docv)." in + Arg.(value & opt dir "sources/" & info ["sources"] ~docv:"DIR" ~doc) + +let plot = + let doc = "Path for the plot utility is $(docv)." in + Arg.(value & opt non_dir_file "./plot" & info ["plot"] ~docv:"PATH" ~doc) + let mem = let doc = "Uses $(docv) as the tool to measure memory." in Arg.(value & opt non_dir_file "/usr/bin/time" & info ["time"] ~docv:"PATH" ~doc) @@ -152,4 +160,4 @@ let info = ;; let () = - Term.exit @@ Term.eval (Term.(const main $ timeout $ runners $ namef $ mem $ seed), info) + Term.exit @@ Term.eval (Term.(const main $ src $ plot $ timeout $ runners $ namef $ mem $ seed), info) diff --git a/trace/dune b/trace/dune new file mode 100644 index 000000000..7bffffe0e --- /dev/null +++ b/trace/dune @@ -0,0 +1,18 @@ +(library + (name trace_ppx) + ; (public_name trace_ppx) + (libraries ppx_tools_versioned ocaml-migrate-parsetree) + (preprocess (pps ppx_tools_versioned.metaquot_404)) + (flags -open Ast_404) + (kind ppx_rewriter) + (ppx_runtime_libraries elpi.elpi_trace) + (modules trace_ppx) +) + +(library + (name elpi_trace) + (public_name elpi.elpi_trace) + ; (public_name trace_ppx.runtime) + (libraries re) + (modules elpi_trace) +) diff --git a/src/elpi_trace.ml b/trace/elpi_trace.ml similarity index 90% rename from src/elpi_trace.ml rename to trace/elpi_trace.ml index 85feb776f..66066dcf9 100644 --- a/src/elpi_trace.ml +++ b/trace/elpi_trace.ml @@ -3,9 +3,15 @@ (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) -open Elpi_util module F = Format +let err_fmt = ref F.err_formatter +let set_formatter x = err_fmt := x +let eprintf x = F.fprintf !err_fmt x +let set_formatter_maxcols i = F.pp_set_margin !err_fmt i +let set_formatter_maxbox i = F.pp_set_max_boxes !err_fmt i + +module StrMap = Map.Make(String) module Str = Re.Str let debug = ref false @@ -33,7 +39,7 @@ let perf_stack = ref [{name = "main"; self = 0.0; progeny = StrMap.empty }] let collect_perf_enter n = if !collect_perf then match !perf_stack with - | { progeny } :: _ when StrMap.mem n progeny -> + | { progeny; _ } :: _ when StrMap.mem n progeny -> perf_stack := StrMap.find n progeny :: !perf_stack | _ -> perf_stack := { name = n; self = 0.0; progeny = StrMap.empty } :: !perf_stack @@ -41,25 +47,25 @@ let collect_perf_enter n = let rec merge m1 m2 = StrMap.fold (fun _ ({ name; self; progeny } as v) m -> try - let { self = t; progeny = p } = StrMap.find name m in + let { self = t; progeny = p; _ } = StrMap.find name m in StrMap.add name { name; self = self +. t; progeny = merge progeny p } m with Not_found -> StrMap.add name v m) m1 m2 let collect_perf_exit time = if !collect_perf then match !perf_stack with - | { name = n1 } as top :: ({ name = n2} as prev) :: rest when n1 = n2 -> + | { name = n1; _ } as top :: ({ name = n2; _ } as prev) :: rest when n1 = n2 -> perf_stack := { name = n2; self = prev.self; progeny = merge top.progeny prev.progeny } :: rest - | top :: ({ progeny } as prev) :: rest -> + | top :: ({ progeny; _ } as prev) :: rest -> let top = { top with self = top.self +. time } in perf_stack := { prev with progeny = StrMap.add top.name top progeny } :: rest | _ -> assert false let rec print_tree hot { name; self; progeny } indent = let tprogeny, (phot, thot) = - StrMap.fold (fun n { self } (x,(_,m as top)) -> + StrMap.fold (fun n { self; _ } (x,(_,m as top)) -> x +. self, (if self > m then (n,self) else top)) progeny (0.0,("",0.0)) in let phot = @@ -73,7 +79,7 @@ let rec print_tree hot { name; self; progeny } indent = let print_perf () = while List.length !perf_stack > 1 do collect_perf_exit 0.0; done; match !perf_stack with - | [ { progeny } ] -> + | [ { progeny; _ } ] -> eprintf " %-20s %s %6s %6s\n" "name" String.(make 20 ' ' ) "total" "self"; eprintf "%s\n" (String.make 80 '-'); @@ -163,14 +169,14 @@ let pr_exn f = printers := f :: !printers exception TREC_CALL of Obj.t * Obj.t (* ('a -> 'b) * 'a *) -let print_exit k tailcall e time = +let print_exit tailcall e time = if not !trace_noprint then eprintf "%s}}} %s (%.3fs)\n%!" (make_indent ()) (if tailcall then "->" else pr_exc e) time let exit k tailcall ?(e=OK) time = if condition k then begin - print_exit k tailcall e time; + print_exit tailcall e time; collect_perf_exit time; end; decr level @@ -233,10 +239,10 @@ let parse_argv argv = only_pred := pname :: !only_pred; aux rest; | "-trace-maxbox" :: num :: rest -> - set_formatters_maxbox (int_of_string num); + set_formatter_maxbox (int_of_string num); aux rest | "-trace-maxcols" :: num :: rest -> - set_formatters_maxcols (int_of_string num); + set_formatter_maxcols (int_of_string num); aux rest | "-perf-on" :: rest -> collect_perf := true; on := true; trace_noprint := true; aux rest diff --git a/src/elpi_trace.mli b/trace/elpi_trace.mli similarity index 93% rename from src/elpi_trace.mli rename to trace/elpi_trace.mli index a20ae8c50..58e806a59 100644 --- a/src/elpi_trace.mli +++ b/trace/elpi_trace.mli @@ -25,3 +25,6 @@ val get_cur_step : string -> int val parse_argv : string list -> string list val usage: string + +(* prints here *) +val set_formatter : Format.formatter -> unit diff --git a/trace_ppx.ml b/trace/trace_ppx.ml similarity index 97% rename from trace_ppx.ml rename to trace/trace_ppx.ml index ac2884d05..b6f20a250 100644 --- a/trace_ppx.ml +++ b/trace/trace_ppx.ml @@ -74,8 +74,8 @@ let tcall hd args = let enabled = ref false let args = [ - "--on",Arg.Set enabled,"Enable trace" ; - "--off",Arg.Clear enabled,"Disable trace" ; + "--trace_ppx-on",Arg.Set enabled,"Enable trace_ppx" ; + "--trace_ppx-off",Arg.Clear enabled,"Disable trace_ppx" ; ] let reset_args () = enabled := false diff --git a/utils/mathpartir.sty b/utils/mathpartir.sty deleted file mode 100644 index 6cc0f99fe..000000000 --- a/utils/mathpartir.sty +++ /dev/null @@ -1,492 +0,0 @@ -% Mathpartir --- Math Paragraph for Typesetting Inference Rules -% -% Copyright (C) 2001, 2002, 2003, 2004, 2005, 2015 Didier R�my -% -% Author : Didier Remy -% Version : 1.3.0 -% Bug Reports : to author -% Web Site : http://pauillac.inria.fr/~remy/latex/ -% -% Mathpartir is free software; you can redistribute it and/or modify -% it under the terms of the GNU General Public License as published by -% the Free Software Foundation; either version 2, or (at your option) -% any later version. -% -% Mathpartir is distributed in the hope that it will be useful, -% but WITHOUT ANY WARRANTY; without even the implied warranty of -% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -% GNU General Public License for more details -% (http://pauillac.inria.fr/~remy/license/GPL). -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% File mathpartir.sty (LaTeX macros) -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\NeedsTeXFormat{LaTeX2e} -\ProvidesPackage{mathpartir} - [2005/12/20 version 1.2.0 Math Paragraph for Typesetting Inference Rules] - -%% - -%% Identification -%% Preliminary declarations - -\RequirePackage {keyval} - -%% Options -%% More declarations - -%% PART I: Typesetting maths in paragraphe mode - -%% \newdimen \mpr@tmpdim -%% Dimens are a precious ressource. Uses seems to be local. -\let \mpr@tmpdim \@tempdima - -% To ensure hevea \hva compatibility, \hva should expands to nothing -% in mathpar or in inferrule -\let \mpr@hva \empty - -%% normal paragraph parametters, should rather be taken dynamically -\def \mpr@savepar {% - \edef \MathparNormalpar - {\noexpand \lineskiplimit \the\lineskiplimit - \noexpand \lineskip \the\lineskip}% - } - -\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em} -\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em} -\def \mpr@lineskip {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em} -\let \MathparLineskip \mpr@lineskip -\def \mpr@paroptions {\MathparLineskip} -\let \mpr@prebindings \relax - -\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em - -\def \mpr@goodbreakand - {\hskip -\mpr@andskip \penalty -1000\hskip \mpr@andskip} -\def \mpr@and {\hskip \mpr@andskip} -\def \mpr@andcr {\penalty 50\mpr@and} -\def \mpr@cr {\penalty -10000\mpr@and} -\def \mpr@cr {\penalty -10000\vadjust{\vbox{aaa}}\mpr@and} -\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10} - -\def \mpr@bindings {% - \let \and \mpr@andcr - \let \par \mpr@andcr - \let \\\mpr@cr - \let \eqno \mpr@eqno - \let \hva \mpr@hva - } -\let \MathparBindings \mpr@bindings - -% \@ifundefined {ignorespacesafterend} -% {\def \ignorespacesafterend {\aftergroup \ignorespaces} - -\newenvironment{mathpar}[1][] - {$$\mpr@savepar \parskip 0em \hsize \linewidth \centering - \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else - \noindent $\displaystyle\fi - \MathparBindings} - {\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend} - -\newenvironment{mathparpagebreakable}[1][] - {\begingroup - \par - \mpr@savepar \parskip 0em \hsize \linewidth \centering - \mpr@prebindings \mpr@paroptions #1% - \vskip \abovedisplayskip \vskip -\lineskip% - \ifmmode \else $\displaystyle\fi - \MathparBindings - } - {\unskip - \ifmmode $\fi \par\endgroup - \vskip \belowdisplayskip - \noindent - \ignorespacesafterend} - -% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum -% \wd0 < \hsize $$\box0$$\else \bmathpar #1\emathpar \fi} - -%%% HOV BOXES - -\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip - \vbox \bgroup \tabskip 0em \let \\ \cr - \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup - \egroup} - -\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize - \box0\else \mathvbox {#1}\fi} - - -%% Part II -- operations on lists - -\newtoks \mpr@lista -\newtoks \mpr@listb - -\long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter -{#2}\edef #2{\the \mpr@lista \the \mpr@listb}} - -\long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter -{#2}\edef #2{\the \mpr@listb\the\mpr@lista}} - -\long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb -\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}} - -\def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2} -\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}} - -\def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2} -\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}} - -\def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}% - \mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the - \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty - \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop - \mpr@flatten \mpr@all \mpr@to \mpr@one - \expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof - \mpr@all \mpr@stripend - \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi - \ifx 1\mpr@isempty - \repeat -} - -\def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty - \def \\##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp} - -%% Part III -- Type inference rules - -\newif \if@premisse -\newbox \mpr@hlist -\newbox \mpr@vlist -\newif \ifmpr@center \mpr@centertrue -\def \mpr@vskip {} -\def \mpr@htovlist {% - \setbox \mpr@hlist - \hbox {\strut - \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi - \unhbox \mpr@hlist}% - \setbox \mpr@vlist - \vbox {\if@premisse - \box \mpr@hlist - \ifx \mpr@vskip \empty \else - \hrule height 0em depth \mpr@vskip width 0em - \fi - \unvbox \mpr@vlist - \else - \unvbox \mpr@vlist - \ifx \mpr@vskip \empty \else - \hrule height 0em depth \mpr@vskip width 0em - \fi - \box \mpr@hlist - \fi}% -} -% OLD version -% \def \mpr@htovlist {% -% \setbox \mpr@hlist -% \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}% -% \setbox \mpr@vlist -% \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist -% \else \unvbox \mpr@vlist \box \mpr@hlist -% \fi}% -% } - -\def \mpr@item #1{$\displaystyle #1$} -\def \mpr@sep{2em} -\def \mpr@blank { } -\def \mpr@hovbox #1#2{\hbox - \bgroup - \ifx #1T\@premissetrue - \else \ifx #1B\@premissefalse - \else - \PackageError{mathpartir} - {Premisse orientation should either be T or B} - {Fatal error in Package}% - \fi \fi - \def \@test {#2}\ifx \@test \mpr@blank\else - \setbox \mpr@hlist \hbox {}% - \setbox \mpr@vlist \vbox {}% - \if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi - \let \@hvlist \empty \let \@rev \empty - \mpr@tmpdim 0em - \expandafter \mpr@makelist #2\mpr@to \mpr@flat - \if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi - \def \\##1{% - \def \@test {##1}\ifx \@test \empty - \mpr@htovlist - \mpr@tmpdim 0em %%% last bug fix not extensively checked - \else - \setbox0 \hbox{\mpr@item {##1}}\relax - \advance \mpr@tmpdim by \wd0 - %\mpr@tmpdim 1.02\mpr@tmpdim - \ifnum \mpr@tmpdim < \hsize - \ifnum \wd\mpr@hlist > 0 - \if@premisse - \setbox \mpr@hlist - \hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}% - \else - \setbox \mpr@hlist - \hbox {\unhbox \mpr@hlist \hskip \mpr@sep \unhbox0}% - \fi - \else - \setbox \mpr@hlist \hbox {\unhbox0}% - \fi - \else - \ifnum \wd \mpr@hlist > 0 - \mpr@htovlist - \mpr@tmpdim \wd0 - \fi - \setbox \mpr@hlist \hbox {\unhbox0}% - \fi - \advance \mpr@tmpdim by \mpr@sep - \fi - }% - \@rev - \mpr@htovlist - \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist - \fi - \egroup -} - -%%% INFERENCE RULES - -\@ifundefined{@@over}{% - \let\@@over\over % fallback if amsmath is not loaded - \let\@@overwithdelims\overwithdelims - \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims - \let\@@above\above \let\@@abovewithdelims\abovewithdelims - }{} - -%% The default - -\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em - $\displaystyle {#1\mpr@over #2}$}} -\def \mpr@@nofraction #1#2{\hbox {\advance \hsize by -0.5em - $\displaystyle {#1\@@atop #2}$}} - -\let \mpr@fraction \mpr@@fraction - -%% A generic solution to arrow - -\def \mpr@@fractionaboveskip {0ex} -\def \mpr@@fractionbelowskip {0.22ex} - -\def \mpr@make@fraction #1#2#3#4#5{\hbox {% - \def \mpr@tail{#1}% - \def \mpr@body{#2}% - \def \mpr@head{#3}% - \setbox1=\hbox{$#4$}\setbox2=\hbox{$#5$}% - \setbox3=\hbox{$\mkern -3mu\mpr@body\mkern -3mu$}% - \dimen0\ht3\advance\dimen0 by \dp3\relax - \dimen0 0.5\dimen0\relax - \advance \dimen0 by \mpr@@fractionaboveskip - \setbox1=\hbox {\raise \dimen0 \box1}\relax - \dimen0 -\dimen0\advance \dimen0 \mpr@@fractionaboveskip\dimen0 -\dimen0 - \advance \dimen0 by \mpr@@fractionbelowskip - \setbox2=\hbox {\lower \dimen0 \box2}\relax - \setbox0=\hbox {$\displaystyle {\box1 \atop \box2}$}% - \dimen0=\wd0\box0 - \box0 \hskip -\dimen0\relax - \hbox to \dimen0 {$%\color{blue} - \mathrel{\mpr@tail}\joinrel - \xleaders\hbox{\copy3}\hfil\joinrel\mathrel{\mpr@head}% - $}}} - -%% Old stuff should be removed in next version -\def \mpr@@nothing #1#2 - {$\lower 0.01pt \mpr@@nofraction {#1}{#2}$} -\def \mpr@@reduce #1#2{\hbox - {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}} -\def \mpr@@rewrite #1#2#3{\hbox - {$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}} -\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}} - -\def \mpr@empty {} -\def \mpr@inferrule - {\bgroup - \ifnum \linewidth<\hsize \hsize \linewidth\fi - \mpr@rulelineskip - \let \and \qquad - \let \hva \mpr@hva - \let \@rulename \mpr@empty - \let \@rule@options \mpr@empty - \let \mpr@over \@@over - \mpr@inferrule@} -\newcommand {\mpr@inferrule@}[3][] - {\everymath={\displaystyle}% - \def \@test {#2}\ifx \empty \@test - \setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}% - \else - \def \@test {#3}\ifx \empty \@test - \setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}% - \else - \setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}% - \fi \fi - \def \@test {#1}\ifx \@test\empty \box0 - \else \vbox -%%% Suggestion de Francois pour les etiquettes longues -%%% {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi - {\hbox {\DefTirName {#1}}\box0}\fi - \egroup} - -\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}} - -% They are two forms -% \inferrule [label]{[premisses}{conclusions} -% or -% \inferrule* [options]{[premisses}{conclusions} -% -% Premisses and conclusions are lists of elements separated by \\ -% Each \\ produces a break, attempting horizontal breaks if possible, -% and vertical breaks if needed. -% -% An empty element obtained by \\\\ produces a vertical break in all cases. -% -% The former rule is aligned on the fraction bar. -% The optional label appears on top of the rule -% The second form to be used in a derivation tree is aligned on the last -% line of its conclusion -% -% The second form can be parameterized, using the key=val interface. The -% folloiwng keys are recognized: -% -% width set the width of the rule to val -% narrower set the width of the rule to val\hsize -% before execute val at the beginning/left -% lab put a label [Val] on top of the rule -% lskip add negative skip on the right -% left put a left label [Val] -% Left put a left label [Val], ignoring its width -% right put a right label [Val] -% Right put a right label [Val], ignoring its width -% leftskip skip negative space on the left-hand side -% rightskip skip negative space on the right-hand side -% vdots lift the rule by val and fill vertical space with dots -% after execute val at the end/right -% -% Note that most options must come in this order to avoid strange -% typesetting (in particular leftskip must preceed left and Left and -% rightskip must follow Right or right; vdots must come last -% or be only followed by rightskip. -% - -%% Keys that make sence in all kinds of rules -\def \mprset #1{\setkeys{mprset}{#1}} -\define@key {mprset}{andskip}[]{\mpr@andskip=#1} -\define@key {mprset}{lineskip}[]{\lineskip=#1} -\define@key {mprset}{lessskip}[]{\lineskip=0.5\lineskip} -\define@key {mprset}{flushleft}[]{\mpr@centerfalse} -\define@key {mprset}{center}[]{\mpr@centertrue} -\define@key {mprset}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite} -\define@key {mprset}{atop}[]{\let \mpr@fraction \mpr@@nofraction} -\define@key {mprset}{myfraction}[]{\let \mpr@fraction #1} -\define@key {mprset}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}} -% To be documented. -\define@key {mprset}{defaultfraction}[]{\let \mpr@fraction \mpr@@fraction} -\define@key {mprset}{sep}{\def\mpr@sep{#1}} -\define@key {mprset}{fractionaboveskip}{\def\mpr@@fractionaboveskip{#1}} -\define@key {mprset}{fractionbelowskip}{\def\mpr@@fractionbelowskip{#1}} -\define@key {mprset}{style}[1]{\def\TirNameStyle{#1}def} -\define@key {mprset}{rightstyle}[1]{\def\RightTirNameStyle{#1}} -\define@key {mprset}{leftstyle}[1]{\def\LeftTirNameStyle{#1}} -\define@key {mprset}{vskip}[1]{\def \mpr@vskip{#1}} - -\newbox \mpr@right -\define@key {mpr}{flushleft}[]{\mpr@centerfalse} -\define@key {mpr}{center}[]{\mpr@centertrue} -\define@key {mpr}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite} -\define@key {mpr}{myfraction}[]{\let \mpr@fraction #1} -\define@key {mpr}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}} -\define@key {mpr}{width}{\hsize #1} -\define@key {mpr}{sep}{\def\mpr@sep{#1}} -\define@key {mpr}{before}{#1} -\define@key {mpr}{lab}{\let \DefTirName \LabTirName \def \mpr@rulename {#1}} -\define@key {mpr}{Lab}{\let \DefTirName \LabTirName \def \mpr@rulename {#1}} -\define@key {mpr}{style}[1]{\def\TirNameStyle{#1}def} -\define@key {mpr}{rightstyle}[1]{\def\RightTirNameStyle{#1}} -\define@key {mpr}{leftstyle}[1]{\def\LeftTirNameStyle{#1}} -\define@key {mpr}{vskip}[1]{\def \mpr@vskip{#1}} -\define@key {mpr}{narrower}{\hsize #1\hsize} -\define@key {mpr}{leftskip}{\hskip -#1} -\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce} -\define@key {mpr}{rightskip} - {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}} -\define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax - \advance \hsize by -\wd0\box0} - -\define@key {mpr}{left}{\setbox0 \hbox {$\LeftTirName {#1}\;$}\relax - \advance \hsize by -\wd0\box0} -\define@key {mpr}{Left}{\llap{$\LeftTirName {#1}\;$}} -\define@key {mpr}{right} - {\setbox0 \hbox {$\;\RightTirName {#1}$}\relax \advance \hsize by -\wd0 - \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}} -\define@key {mpr}{RIGHT} - {\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0 - \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}} -\define@key {mpr}{Right} - {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\RightTirName {#1}$}}} -\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}} -\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}} -\define@key {mpr}{vcenter}[]{\mpr@vcentertrue} - -\newif \ifmpr@vcenter \mpr@vcenterfalse -\newcommand \mpr@inferstar@ [3][]{\begingroup - \setbox0 \hbox - {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax - \setbox \mpr@right \hbox{}% - \setkeys{mpr}{#1}% - $\ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else - \mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi - \box \mpr@right \mpr@vdots$ - \ifmpr@vcenter \aftergroup \mpr@vcentertrue \fi} - \ifmpr@vcenter - \box0 - \else - \setbox1 \hbox {\strut} - \@tempdima \dp0 \advance \@tempdima by -\dp1 - \raise \@tempdima \box0 - \fi - \endgroup} - -\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}} -\newcommand \mpr@err@skipargs[3][]{} -\def \mpr@inferstar*{\ifmmode - \let \@do \mpr@inferstar@ - \else - \let \@do \mpr@err@skipargs - \PackageError {mathpartir} - {\string\inferrule* can only be used in math mode}{}% - \fi \@do} - - -%%% Exports - -% Envirnonment mathpar - -\let \inferrule \mpr@infer - -% make a short name \infer is not already defined -\@ifundefined {infer}{\let \infer \mpr@infer}{} - -\def \TirNameStyle #1{\small \textsc{#1}} -\def \LeftTirNameStyle #1{\TirNameStyle {#1}} -\def \RightTirNameStyle #1{\TirNameStyle {#1}} - -\def \lefttir@name #1{\hbox {\small \LeftTirNameStyle{#1}}} -\def \righttir@name #1{\hbox {\small \RightTirNameStyle{#1}}} -\let \TirName \lefttir@name -\let \LeftTirName \lefttir@name -\let \DefTirName \lefttir@name -\let \LabTirName \lefttir@name -\let \RightTirName \righttir@name - -%%% Other Exports - -% \let \listcons \mpr@cons -% \let \listsnoc \mpr@snoc -% \let \listhead \mpr@head -% \let \listmake \mpr@makelist - - - - -\endinput From f1bb626582b49bce3ece23825bde1edb94aa980a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 19 Jun 2019 18:01:41 +0200 Subject: [PATCH 02/10] improving dune files --- elpi.install | 96 ---------------------------------------------------- src/dune | 25 +++----------- 2 files changed, 4 insertions(+), 117 deletions(-) delete mode 100644 elpi.install diff --git a/elpi.install b/elpi.install deleted file mode 100644 index eac261bef..000000000 --- a/elpi.install +++ /dev/null @@ -1,96 +0,0 @@ -lib: [ - "_build/install/default/lib/elpi/.private/elpi__Elpi_ast.cmi" {".private/elpi__Elpi_ast.cmi"} - "_build/install/default/lib/elpi/.private/elpi__Elpi_compiler.cmi" {".private/elpi__Elpi_compiler.cmi"} - "_build/install/default/lib/elpi/.private/elpi__Elpi_data.cmi" {".private/elpi__Elpi_data.cmi"} - "_build/install/default/lib/elpi/.private/elpi__Elpi_parser.cmi" {".private/elpi__Elpi_parser.cmi"} - "_build/install/default/lib/elpi/.private/elpi__Elpi_ptmap.cmi" {".private/elpi__Elpi_ptmap.cmi"} - "_build/install/default/lib/elpi/.private/elpi__Elpi_runtime_trace_off.cmi" {".private/elpi__Elpi_runtime_trace_off.cmi"} - "_build/install/default/lib/elpi/.private/elpi__Elpi_runtime_trace_on.cmi" {".private/elpi__Elpi_runtime_trace_on.cmi"} - "_build/install/default/lib/elpi/.private/elpi__Elpi_util.cmi" {".private/elpi__Elpi_util.cmi"} - "_build/install/default/lib/elpi/META" {"META"} - "_build/install/default/lib/elpi/builtin.elpi" - "_build/install/default/lib/elpi/dune-package" {"dune-package"} - "_build/install/default/lib/elpi/elpi-checker.elpi" - "_build/install/default/lib/elpi/elpi.a" {"elpi.a"} - "_build/install/default/lib/elpi/elpi.cma" {"elpi.cma"} - "_build/install/default/lib/elpi/elpi.cmi" {"elpi.cmi"} - "_build/install/default/lib/elpi/elpi.cmt" {"elpi.cmt"} - "_build/install/default/lib/elpi/elpi.cmx" {"elpi.cmx"} - "_build/install/default/lib/elpi/elpi.cmxa" {"elpi.cmxa"} - "_build/install/default/lib/elpi/elpi.cmxs" {"elpi.cmxs"} - "_build/install/default/lib/elpi/elpi.ml" {"elpi.ml"} - "_build/install/default/lib/elpi/elpi2html.elpi" - "_build/install/default/lib/elpi/elpi_API.ml" {"elpi_API.ml"} - "_build/install/default/lib/elpi/elpi_API.mli" {"elpi_API.mli"} - "_build/install/default/lib/elpi/elpi__.cmi" {"elpi__.cmi"} - "_build/install/default/lib/elpi/elpi__.cmt" {"elpi__.cmt"} - "_build/install/default/lib/elpi/elpi__.cmx" {"elpi__.cmx"} - "_build/install/default/lib/elpi/elpi__.ml" {"elpi__.ml"} - "_build/install/default/lib/elpi/elpi__Elpi_API.cmi" {"elpi__Elpi_API.cmi"} - "_build/install/default/lib/elpi/elpi__Elpi_API.cmt" {"elpi__Elpi_API.cmt"} - "_build/install/default/lib/elpi/elpi__Elpi_API.cmti" {"elpi__Elpi_API.cmti"} - "_build/install/default/lib/elpi/elpi__Elpi_API.cmx" {"elpi__Elpi_API.cmx"} - "_build/install/default/lib/elpi/elpi__Elpi_ast.cmt" {"elpi__Elpi_ast.cmt"} - "_build/install/default/lib/elpi/elpi__Elpi_ast.cmti" {"elpi__Elpi_ast.cmti"} - "_build/install/default/lib/elpi/elpi__Elpi_ast.cmx" {"elpi__Elpi_ast.cmx"} - "_build/install/default/lib/elpi/elpi__Elpi_builtin.cmi" {"elpi__Elpi_builtin.cmi"} - "_build/install/default/lib/elpi/elpi__Elpi_builtin.cmt" {"elpi__Elpi_builtin.cmt"} - "_build/install/default/lib/elpi/elpi__Elpi_builtin.cmti" {"elpi__Elpi_builtin.cmti"} - "_build/install/default/lib/elpi/elpi__Elpi_builtin.cmx" {"elpi__Elpi_builtin.cmx"} - "_build/install/default/lib/elpi/elpi__Elpi_compiler.cmt" {"elpi__Elpi_compiler.cmt"} - "_build/install/default/lib/elpi/elpi__Elpi_compiler.cmti" {"elpi__Elpi_compiler.cmti"} - "_build/install/default/lib/elpi/elpi__Elpi_compiler.cmx" {"elpi__Elpi_compiler.cmx"} - "_build/install/default/lib/elpi/elpi__Elpi_data.cmt" {"elpi__Elpi_data.cmt"} - "_build/install/default/lib/elpi/elpi__Elpi_data.cmx" {"elpi__Elpi_data.cmx"} - "_build/install/default/lib/elpi/elpi__Elpi_parser.cmt" {"elpi__Elpi_parser.cmt"} - "_build/install/default/lib/elpi/elpi__Elpi_parser.cmti" {"elpi__Elpi_parser.cmti"} - "_build/install/default/lib/elpi/elpi__Elpi_parser.cmx" {"elpi__Elpi_parser.cmx"} - "_build/install/default/lib/elpi/elpi__Elpi_ptmap.cmt" {"elpi__Elpi_ptmap.cmt"} - "_build/install/default/lib/elpi/elpi__Elpi_ptmap.cmti" {"elpi__Elpi_ptmap.cmti"} - "_build/install/default/lib/elpi/elpi__Elpi_ptmap.cmx" {"elpi__Elpi_ptmap.cmx"} - "_build/install/default/lib/elpi/elpi__Elpi_runtime_trace_off.cmt" {"elpi__Elpi_runtime_trace_off.cmt"} - "_build/install/default/lib/elpi/elpi__Elpi_runtime_trace_off.cmti" {"elpi__Elpi_runtime_trace_off.cmti"} - "_build/install/default/lib/elpi/elpi__Elpi_runtime_trace_off.cmx" {"elpi__Elpi_runtime_trace_off.cmx"} - "_build/install/default/lib/elpi/elpi__Elpi_runtime_trace_on.cmt" {"elpi__Elpi_runtime_trace_on.cmt"} - "_build/install/default/lib/elpi/elpi__Elpi_runtime_trace_on.cmti" {"elpi__Elpi_runtime_trace_on.cmti"} - "_build/install/default/lib/elpi/elpi__Elpi_runtime_trace_on.cmx" {"elpi__Elpi_runtime_trace_on.cmx"} - "_build/install/default/lib/elpi/elpi__Elpi_util.cmt" {"elpi__Elpi_util.cmt"} - "_build/install/default/lib/elpi/elpi__Elpi_util.cmti" {"elpi__Elpi_util.cmti"} - "_build/install/default/lib/elpi/elpi__Elpi_util.cmx" {"elpi__Elpi_util.cmx"} - "_build/install/default/lib/elpi/elpi_ast.ml" {"elpi_ast.ml"} - "_build/install/default/lib/elpi/elpi_ast.mli" {"elpi_ast.mli"} - "_build/install/default/lib/elpi/elpi_builtin.ml" {"elpi_builtin.ml"} - "_build/install/default/lib/elpi/elpi_builtin.mli" {"elpi_builtin.mli"} - "_build/install/default/lib/elpi/elpi_compiler.ml" {"elpi_compiler.ml"} - "_build/install/default/lib/elpi/elpi_compiler.mli" {"elpi_compiler.mli"} - "_build/install/default/lib/elpi/elpi_data.ml" {"elpi_data.ml"} - "_build/install/default/lib/elpi/elpi_parser.ml" {"elpi_parser.ml"} - "_build/install/default/lib/elpi/elpi_parser.mli" {"elpi_parser.mli"} - "_build/install/default/lib/elpi/elpi_ptmap.ml" {"elpi_ptmap.ml"} - "_build/install/default/lib/elpi/elpi_ptmap.mli" {"elpi_ptmap.mli"} - "_build/install/default/lib/elpi/elpi_quoted_syntax.elpi" - "_build/install/default/lib/elpi/elpi_runtime_trace_off.ml" {"elpi_runtime_trace_off.ml"} - "_build/install/default/lib/elpi/elpi_runtime_trace_off.mli" {"elpi_runtime_trace_off.mli"} - "_build/install/default/lib/elpi/elpi_runtime_trace_on.ml" {"elpi_runtime_trace_on.ml"} - "_build/install/default/lib/elpi/elpi_runtime_trace_on.mli" {"elpi_runtime_trace_on.mli"} - "_build/install/default/lib/elpi/elpi_trace/elpi_trace.a" {"elpi_trace/elpi_trace.a"} - "_build/install/default/lib/elpi/elpi_trace/elpi_trace.cma" {"elpi_trace/elpi_trace.cma"} - "_build/install/default/lib/elpi/elpi_trace/elpi_trace.cmi" {"elpi_trace/elpi_trace.cmi"} - "_build/install/default/lib/elpi/elpi_trace/elpi_trace.cmt" {"elpi_trace/elpi_trace.cmt"} - "_build/install/default/lib/elpi/elpi_trace/elpi_trace.cmti" {"elpi_trace/elpi_trace.cmti"} - "_build/install/default/lib/elpi/elpi_trace/elpi_trace.cmx" {"elpi_trace/elpi_trace.cmx"} - "_build/install/default/lib/elpi/elpi_trace/elpi_trace.cmxa" {"elpi_trace/elpi_trace.cmxa"} - "_build/install/default/lib/elpi/elpi_trace/elpi_trace.cmxs" {"elpi_trace/elpi_trace.cmxs"} - "_build/install/default/lib/elpi/elpi_trace/elpi_trace.ml" {"elpi_trace/elpi_trace.ml"} - "_build/install/default/lib/elpi/elpi_trace/elpi_trace.mli" {"elpi_trace/elpi_trace.mli"} - "_build/install/default/lib/elpi/elpi_util.ml" {"elpi_util.ml"} - "_build/install/default/lib/elpi/elpi_util.mli" {"elpi_util.mli"} - "_build/install/default/lib/elpi/opam" {"opam"} -] -bin: [ - "_build/install/default/bin/elpi" {"elpi"} -] -doc: [ - "_build/install/default/doc/elpi/LICENSE" - "_build/install/default/doc/elpi/README.md" -] diff --git a/src/dune b/src/dune index e12bf567f..d99aaa4ae 100644 --- a/src/dune +++ b/src/dune @@ -13,27 +13,10 @@ (private_modules elpi_util elpi_parser elpi_ast elpi_compiler elpi_data elpi_ptmap elpi_runtime_trace_on elpi_runtime_trace_off) ) -(rule - (targets elpi_runtime_trace_on.ml) - (deps elpi_runtime.ml) - (action (copy# %{deps} %{targets})) -) -(rule - (targets elpi_runtime_trace_on.mli) - (deps elpi_runtime.mli) - (action (copy# %{deps} %{targets})) -) - -(rule - (targets elpi_runtime_trace_off.ml) - (deps elpi_runtime.ml) - (action (copy# %{deps} %{targets})) -) -(rule - (targets elpi_runtime_trace_off.mli) - (deps elpi_runtime.mli) - (action (copy# %{deps} %{targets})) -) +(rule (copy# elpi_runtime.ml elpi_runtime_trace_on.ml)) +(rule (copy# elpi_runtime.ml elpi_runtime_trace_off.ml)) +(rule (copy# elpi_runtime.mli elpi_runtime_trace_on.mli)) +(rule (copy# elpi_runtime.mli elpi_runtime_trace_off.mli)) (install (section lib) From fff217da59a861955add84e8e257e87d8da407c6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 20 Jun 2019 11:29:37 +0200 Subject: [PATCH 03/10] rename files since packing is now made by dune --- Makefile | 17 +- elpi.opam | 4 +- elpi_REPL.ml | 76 ++--- src/{elpi_API.ml => API.ml} | 306 +++++++++--------- src/{elpi_API.mli => API.mli} | 2 +- src/{elpi_ast.ml => ast.ml} | 7 +- src/{elpi_ast.mli => ast.mli} | 8 +- src/builtin.elpi | 2 +- src/{elpi_builtin.ml => builtin.ml} | 12 +- src/{elpi_builtin.mli => builtin.mli} | 14 +- src/{elpi_compiler.ml => compiler.ml} | 44 ++- src/{elpi_compiler.mli => compiler.mli} | 20 +- src/{elpi_data.ml => data.ml} | 23 +- src/dune | 22 +- src/elpi-checker.elpi | 2 +- ...ed_syntax.elpi => elpi-quoted_syntax.elpi} | 0 src/elpi.ml | 4 +- src/elpi2html.elpi | 2 +- src/{elpi_parser.ml => parser.ml} | 8 +- src/{elpi_parser.mli => parser.mli} | 4 +- src/{elpi_ptmap.ml => ptmap.ml} | 2 +- src/{elpi_ptmap.mli => ptmap.mli} | 0 src/{elpi_runtime.ml => runtime.ml} | 102 +++--- src/{elpi_runtime.mli => runtime.mli} | 4 +- src/{elpi_util.ml => util.ml} | 0 src/{elpi_util.mli => util.mli} | 0 26 files changed, 346 insertions(+), 339 deletions(-) rename src/{elpi_API.ml => API.ml} (67%) rename src/{elpi_API.mli => API.mli} (99%) rename src/{elpi_ast.ml => ast.ml} (99%) rename src/{elpi_ast.mli => ast.mli} (97%) rename src/{elpi_builtin.ml => builtin.ml} (98%) rename src/{elpi_builtin.mli => builtin.mli} (71%) rename src/{elpi_compiler.ml => compiler.ml} (98%) rename src/{elpi_compiler.mli => compiler.mli} (71%) rename src/{elpi_data.ml => data.ml} (98%) rename src/{elpi_quoted_syntax.elpi => elpi-quoted_syntax.elpi} (100%) rename src/{elpi_parser.ml => parser.ml} (99%) rename src/{elpi_parser.mli => parser.mli} (98%) rename src/{elpi_ptmap.ml => ptmap.ml} (99%) rename src/{elpi_ptmap.mli => ptmap.mli} (100%) rename src/{elpi_runtime.ml => runtime.ml} (97%) rename src/{elpi_runtime.mli => runtime.mli} (97%) rename src/{elpi_util.ml => util.ml} (100%) rename src/{elpi_util.mli => util.mli} (100%) diff --git a/Makefile b/Makefile index cf69ab8dc..f1bca872a 100644 --- a/Makefile +++ b/Makefile @@ -2,7 +2,10 @@ help: @echo 'Known targets:' @echo @echo ' build builds elpi' - @echo ' .merlin builds a .merlin' + @echo ' install install elpi' + @echo ' clean remove build artifacts' + @echo + @echo ' .merlin builds a .merlin file' @echo @echo ' tests runs the entire test suite' @echo ' tests ONLY=rex runs only tests matching rex' @@ -25,7 +28,7 @@ STACK=32768 .merlin: @dune build .merlin @for ppx in `ls $$PWD/_build/default/.ppx/*/ppx.exe`; do\ - if $$ppx --print-transformations | grep trace; then\ + if $$ppx --print-transformations | grep -q trace; then\ echo PKG ppx_deriving.std ppx_deriving.runtime >> .merlin;\ echo FLG -ppx \"$$ppx --as-ppx\" >> .merlin;\ echo PKG ppx_deriving.std ppx_deriving.runtime >> src/.merlin;\ @@ -34,9 +37,15 @@ STACK=32768 done build: + @$(MAKE) --no-print-directory .merlin dune build @install - $(MAKE) .merlin + @$(MAKE) --no-print-directory .merlin + +install: + dune install +clean: + rm -rf _build tests: dune build $(INSTALL)/bin/elpi @@ -62,4 +71,4 @@ git/%: cp "elpi-$*/$(INSTALL)/bin/elpi" "elpi.git.$*" rm -rf "$$PWD/elpi-$*" -.PHONY: tests help .merlin +.PHONY: tests help .merlin install build clean diff --git a/elpi.opam b/elpi.opam index 784c45c90..417c3b10f 100644 --- a/elpi.opam +++ b/elpi.opam @@ -13,9 +13,7 @@ build: [ [ "dune" "build" "-p" name "-j" jobs ] ] run-test: [ make "tests" ] -install: [ - [ "dune" "install" "-p" name ] -] +install: [ make "install" ] depends: [ "ocaml" {>= "4.04.0"} diff --git a/elpi_REPL.ml b/elpi_REPL.ml index 738a6165a..e038caaa9 100644 --- a/elpi_REPL.ml +++ b/elpi_REPL.ml @@ -17,20 +17,20 @@ open Elpi module Str = Re.Str let print_solution time = function -| Elpi_API.Execute.NoMoreSteps -> +| API.Execute.NoMoreSteps -> Format.eprintf "Interrupted (no more steps)@\n%!" -| Elpi_API.Execute.Failure -> Format.eprintf "Failure@\n%!" -| Elpi_API.Execute.Success { - Elpi_API.Data.assignments; constraints; state; _ } -> +| API.Execute.Failure -> Format.eprintf "Failure@\n%!" +| API.Execute.Success { + API.Data.assignments; constraints; state; _ } -> Format.eprintf "@\nSuccess:@\n%!" ; - Elpi_API.Data.StrMap.iter (fun name v -> + API.Data.StrMap.iter (fun name v -> Format.eprintf " @[%s = %a@]@\n%!" name - Elpi_API.Pp.term v) assignments; + API.Pp.term v) assignments; Format.eprintf "@\nTime: %5.3f@\n%!" time; Format.eprintf "@\nConstraints:@\n%a@\n%!" - Elpi_API.Pp.constraints constraints; + API.Pp.constraints constraints; Format.eprintf "@\nState:@\n%a@\n%!" - Elpi_API.Pp.state state; + API.Pp.state state; ;; let more () = @@ -61,7 +61,7 @@ let usage = "\t-no-tc don't typecheck the program\n" ^ "\t-delay-problems-outside-pattern-fragment (deprecated, for Teyjus\n" ^ "\t compatibility)\n" ^ - Elpi_API.Setup.usage ^ + API.Setup.usage ^ "\nDebug options (for debugging Elpi, not your program):\n" ^ "\t-print-accumulated-files prints files loaded via accumulate\n" ^ "\t-print-ast prints files as parsed, then exit\n" ^ @@ -71,8 +71,8 @@ let usage = (* For testing purposes we declare an identity quotation *) let _ = - Elpi_API.Quotation.register_named_quotation ~name:"elpi" - Elpi_API.Quotation.lp + API.Quotation.register_named_quotation ~name:"elpi" + API.Quotation.lp let _ = let test = ref false in @@ -87,7 +87,7 @@ let _ = let print_passes = ref false in let print_accumulated_files = ref false in let vars = - ref Elpi_API.Compile.(default_flags.defined_variables) in + ref API.Compile.(default_flags.defined_variables) in let rec aux = function | [] -> [] | "-delay-problems-outside-pattern-fragment" :: rest -> delay_outside_fragment := true; aux rest @@ -101,7 +101,7 @@ let _ = | "-no-tc" :: rest -> typecheck := false; aux rest | "-document-builtins" :: rest -> doc_builtins := true; aux rest | "-D" :: var :: rest -> - vars := Elpi_API.Compile.StrSet.add var !vars; + vars := API.Compile.StrSet.add var !vars; aux rest | ("-h" | "--help") :: _ -> Printf.eprintf "%s" usage; exit 0 | "--" :: rest -> args := rest; [] @@ -121,74 +121,74 @@ let _ = List.flatten (List.map (fun x -> ["-I";x^"/elpi/"]) ocamlpath) in let execpath = ["-I"; Filename.dirname (Sys.executable_name)] in let opts = Array.to_list Sys.argv @ tjpath @ installpath @ execpath in - let pheader, argv = Elpi_API.Setup.init ~builtins:Elpi_builtin.std_builtins opts ~basedir:cwd in + let pheader, argv = API.Setup.init ~builtins:Builtin.std_builtins opts ~basedir:cwd in let filenames = aux (List.tl argv) in set_terminal_width (); if !doc_builtins then begin - Elpi_API.BuiltIn.document Format.std_formatter - Elpi_builtin.std_declarations; + API.BuiltIn.document Format.std_formatter + Builtin.std_declarations; exit 0; end; let p = - try Elpi_API.Parse.program + try API.Parse.program ~print_accumulated_files:!print_accumulated_files filenames - with Elpi_API.Parse.ParseError(loc,err) -> - Printf.eprintf "%s: %s\n" (Elpi_API.Ast.Loc.show loc) err; + with API.Parse.ParseError(loc,err) -> + Printf.eprintf "%s: %s\n" (API.Ast.Loc.show loc) err; exit 1; in if !print_ast then begin - Format.eprintf "%a" Elpi_API.Pp.Ast.program p; + Format.eprintf "%a" API.Pp.Ast.program p; exit 0; end; let g = - if !test then Elpi_API.Parse.goal (Elpi_API.Ast.Loc.initial "(-test)") "main." + if !test then API.Parse.goal (API.Ast.Loc.initial "(-test)") "main." else if !exec <> "" then - begin Elpi_API.Parse.goal - (Elpi_API.Ast.Loc.initial "(-exec)") + begin API.Parse.goal + (API.Ast.Loc.initial "(-exec)") (Printf.sprintf "%s [%s]." !exec String.(concat ", " (List.map (Printf.sprintf "\"%s\"") !args))) end else begin Printf.printf "goal> %!"; let strm = Stream.of_channel stdin in - try Elpi_API.Parse.goal_from_stream (Elpi_API.Ast.Loc.initial "(stdin)") strm - with Elpi_API.Parse.ParseError(loc,err) -> - Printf.eprintf "%s: %s\n" (Elpi_API.Ast.Loc.show loc) err; + try API.Parse.goal_from_stream (API.Ast.Loc.initial "(stdin)") strm + with API.Parse.ParseError(loc,err) -> + Printf.eprintf "%s: %s\n" (API.Ast.Loc.show loc) err; exit 1; end in let flags = { - Elpi_API.Compile.default_flags with - Elpi_API.Compile.defined_variables = !vars; - Elpi_API.Compile.print_passes = !print_passes; + API.Compile.default_flags with + API.Compile.defined_variables = !vars; + API.Compile.print_passes = !print_passes; } in - let prog = Elpi_API.Compile.program ~flags pheader [p] in - let query = Elpi_API.Compile.query prog g in + let prog = API.Compile.program ~flags pheader [p] in + let query = API.Compile.query prog g in if !typecheck then begin - if not (Elpi_API.Compile.static_check ~flags pheader query) then + if not (API.Compile.static_check ~flags pheader query) then Format.eprintf "Type error\n"; end; if !print_lprolog then begin - Elpi_API.Pp.query Format.std_formatter query; + API.Pp.query Format.std_formatter query; exit 0; end; - let exec = Elpi_API.Compile.link query in + let exec = API.Compile.link query in if !print_passes then begin exit 0; end; if not !batch then - Elpi_API.Execute.loop + API.Execute.loop ~delay_outside_fragment:!delay_outside_fragment ~more ~pp:print_solution exec else begin Gc.compact (); if let t0 = Unix.gettimeofday () in - let b = Elpi_API.Execute.once + let b = API.Execute.once ~delay_outside_fragment:!delay_outside_fragment exec in let t1 = Unix.gettimeofday () in match b with - | Elpi_API.Execute.Success _ -> print_solution (t1 -. t0) b; true - | (Elpi_API.Execute.Failure | Elpi_API.Execute.NoMoreSteps) -> false + | API.Execute.Success _ -> print_solution (t1 -. t0) b; true + | (API.Execute.Failure | API.Execute.NoMoreSteps) -> false then exit 0 else exit 1 end diff --git a/src/elpi_API.ml b/src/API.ml similarity index 67% rename from src/elpi_API.ml rename to src/API.ml index d311a99b5..5e6755d02 100644 --- a/src/elpi_API.ml +++ b/src/API.ml @@ -2,13 +2,13 @@ (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) -module type Runtime = module type of Elpi_runtime_trace_off +module type Runtime = module type of Runtime_trace_off -let r = ref (module Elpi_runtime_trace_off : Runtime) +let r = ref (module Runtime_trace_off : Runtime) let set_runtime = function - | true -> r := (module Elpi_runtime_trace_on : Runtime) - | false -> r := (module Elpi_runtime_trace_off : Runtime) + | true -> r := (module Runtime_trace_on : Runtime) + | false -> r := (module Runtime_trace_off : Runtime) let set_trace argv = let args = Elpi_trace.parse_argv argv in @@ -17,8 +17,8 @@ let set_trace argv = module Setup = struct -type builtins = string * Elpi_data.BuiltInPredicate.declaration list -type program_header = Elpi_ast.Program.t +type builtins = string * Data.BuiltInPredicate.declaration list +type program_header = Ast.Program.t let init ~builtins:(fname,decls) ~basedir:cwd argv = let new_argv = set_trace argv in @@ -30,84 +30,88 @@ let init ~builtins:(fname,decls) ~basedir:cwd argv = in aux [] [] new_argv in - Elpi_parser.init ~lp_syntax:Elpi_parser.lp_gramext ~paths ~cwd (); + Parser.init ~lp_syntax:Parser.lp_gramext ~paths ~cwd (); (* This is a bit ugly, since builtins are global but could be made * program specific *) List.iter (function - | Elpi_data.BuiltInPredicate.MLCode (p,_) -> Elpi_data.BuiltInPredicate.register p - | Elpi_data.BuiltInPredicate.MLData _ -> () - | Elpi_data.BuiltInPredicate.LPCode _ -> () - | Elpi_data.BuiltInPredicate.LPDoc _ -> ()) decls; + | Data.BuiltInPredicate.MLCode (p,_) -> Data.BuiltInPredicate.register p + | Data.BuiltInPredicate.MLData _ -> () + | Data.BuiltInPredicate.LPCode _ -> () + | Data.BuiltInPredicate.LPDoc _ -> ()) decls; (* This is a bit ugly, since we print and then parse... *) let b = Buffer.create 1024 in let fmt = Format.formatter_of_buffer b in - Elpi_data.BuiltInPredicate.document fmt decls; + Data.BuiltInPredicate.document fmt decls; Format.pp_print_flush fmt (); let text = Buffer.contents b in let strm = Stream.of_string text in - let loc = Elpi_util.Loc.initial fname in + let loc = Util.Loc.initial fname in let header = try - Elpi_parser.parse_program_from_stream + Parser.parse_program_from_stream ~print_accumulated_files:false loc strm - with Elpi_parser.ParseError(loc,msg) -> + with Parser.ParseError(loc,msg) -> List.iteri (fun i s -> Printf.eprintf "%4d: %s\n" (i+1) s) (Re.Str.(split_delim (regexp_string "\n") text)); Printf.eprintf "Excerpt of %s:\n%s\n" fname - (String.sub text loc.Elpi_util.Loc.line_starts_at - Elpi_util.Loc.(loc.source_stop - loc.line_starts_at)); - Elpi_util.anomaly ~loc msg + (String.sub text loc.Util.Loc.line_starts_at + Util.Loc.(loc.source_stop - loc.line_starts_at)); + Util.anomaly ~loc msg in header, new_argv let trace args = match set_trace args with | [] -> () - | l -> Elpi_util.error ("Elpi_API.trace got unknown arguments: " ^ (String.concat " " l)) + | l -> Util.error ("Elpi_API.trace got unknown arguments: " ^ (String.concat " " l)) let usage = "\nParsing options:\n" ^ "\t-I PATH search for accumulated files in PATH\n" ^ Elpi_trace.usage -let set_warn = Elpi_util.set_warn -let set_error = Elpi_util.set_error -let set_anomaly = Elpi_util.set_anomaly -let set_type_error = Elpi_util.set_type_error -let set_std_formatter = Elpi_util.set_std_formatter -let set_err_formatter = Elpi_util.set_err_formatter +let set_warn = Util.set_warn +let set_error = Util.set_error +let set_anomaly = Util.set_anomaly +let set_type_error = Util.set_type_error +let set_std_formatter = Util.set_std_formatter +let set_err_formatter = Util.set_err_formatter end +module EA = Ast + module Ast = struct - type program = Elpi_ast.Program.t - type query = Elpi_ast.Goal.t - module Loc = Elpi_util.Loc + type program = Ast.Program.t + type query = Ast.Goal.t + module Loc = Util.Loc end module Parse = struct let program ?(print_accumulated_files=false) = - Elpi_parser.parse_program ~print_accumulated_files + Parser.parse_program ~print_accumulated_files let program_from_stream ?(print_accumulated_files=false) = - Elpi_parser.parse_program_from_stream ~print_accumulated_files - let goal loc s = Elpi_parser.parse_goal ~loc s - let goal_from_stream loc s = Elpi_parser.parse_goal_from_stream ~loc s - exception ParseError = Elpi_parser.ParseError + Parser.parse_program_from_stream ~print_accumulated_files + let goal loc s = Parser.parse_goal ~loc s + let goal_from_stream loc s = Parser.parse_goal_from_stream ~loc s + exception ParseError = Parser.ParseError end +module ED = Data + module Data = struct - type term = Elpi_data.term - type constraints = Elpi_data.constraints - type state = Elpi_data.State.t - module StrMap = Elpi_util.StrMap - type 'a solution = 'a Elpi_data.solution = { + type term = Data.term + type constraints = Data.constraints + type state = Data.State.t + module StrMap = Util.StrMap + type 'a solution = 'a Data.solution = { assignments : term StrMap.t; constraints : constraints; state : state; output : 'a; } - type hyp = Elpi_data.clause_src = { + type hyp = Data.clause_src = { hdepth : int; hsrc : term } @@ -116,34 +120,34 @@ end module Compile = struct - type program = Elpi_compiler.program - type 'a query = 'a Elpi_compiler.query - type 'a executable = 'a Elpi_data.executable + type program = Compiler.program + type 'a query = 'a Compiler.query + type 'a executable = 'a ED.executable let program ~flags header l = - Elpi_compiler.program_of_ast ~flags (header @ List.flatten l) - let query = Elpi_compiler.query_of_ast + Compiler.program_of_ast ~flags (header @ List.flatten l) + let query = Compiler.query_of_ast let static_check header ?checker ?flags p = let module R = (val !r) in let open R in - let checker = Elpi_util.option_map List.flatten checker in - Elpi_compiler.static_check header ~exec:(execute_once ~delay_outside_fragment:false) ?checker ?flags p + let checker = Util.option_map List.flatten checker in + Compiler.static_check header ~exec:(execute_once ~delay_outside_fragment:false) ?checker ?flags p - module StrSet = Elpi_util.StrSet + module StrSet = Util.StrSet - type flags = Elpi_compiler.flags = { + type flags = Compiler.flags = { defined_variables : StrSet.t; allow_untyped_builtin : bool; print_passes : bool; } - let default_flags = Elpi_compiler.default_flags - let link x = Elpi_compiler.executable_of_query x + let default_flags = Compiler.default_flags + let link x = Compiler.executable_of_query x let dummy_header = [] end module Execute = struct - type 'a outcome = 'a Elpi_data.outcome = + type 'a outcome = 'a ED.outcome = Success of 'a Data.solution | Failure | NoMoreSteps let once ?max_steps ?delay_outside_fragment p = let module R = (val !r) in let open R in @@ -161,29 +165,29 @@ module Pp = struct let constraints f c = let module R = (val !r) in let open R in - Elpi_util.pplist ~boxed:true R.pp_stuck_goal "" f c + Util.pplist ~boxed:true R.pp_stuck_goal "" f c - let state = Elpi_data.State.pp + let state = ED.State.pp let query f c = let module R = (val !r) in let open R in - Elpi_compiler.pp_query (fun ~depth -> R.Pp.uppterm depth [] 0 [||]) f c + Compiler.pp_query (fun ~depth -> R.Pp.uppterm depth [] 0 [||]) f c module Ast = struct - let program = Elpi_ast.Program.pp + let program = EA.Program.pp end end (****************************************************************************) module Conversion = struct - type extra_goals = Elpi_data.extra_goals - include Elpi_data.Conversion + type extra_goals = ED.extra_goals + include ED.Conversion end module RawOpaqueData = struct - include Elpi_util.CData - include Elpi_data.C + include Util.CData + include ED.C type name = string type doc = string @@ -203,24 +207,24 @@ module RawOpaqueData = struct = let ty = Conversion.TyName name in let embed ~depth:_ _ _ state x = - state, Elpi_data.Term.CData (cin x), [] in + state, ED.Term.CData (cin x), [] in let readback ~depth _ _ state t = let module R = (val !r) in let open R in match R.deref_head ~depth t with - | Elpi_data.Term.CData c when isc c -> state, cout c - | Elpi_data.Term.Const i as t when i < 0 -> - begin try state, Elpi_data.Constants.Map.find i constants + | ED.Term.CData c when isc c -> state, cout c + | ED.Term.Const i as t when i < 0 -> + begin try state, ED.Constants.Map.find i constants with Not_found -> raise (Conversion.TypeErr(ty,depth,t)) end | t -> raise (Conversion.TypeErr(ty,depth,t)) in let pp_doc fmt () = if doc <> "" then begin - Elpi_data.BuiltInPredicate.pp_comment fmt ("% " ^ doc); + ED.BuiltInPredicate.pp_comment fmt ("% " ^ doc); Format.fprintf fmt "@\n"; end; (* TODO: use typeabbrv *) Format.fprintf fmt "@[macro %s :- ctype \"%s\".@]@\n@\n" name c; - Elpi_data.Constants.Map.iter (fun c _ -> - Format.fprintf fmt "@[type %a %s.@]@\n" Elpi_data.Constants.pp c name) + ED.Constants.Map.iter (fun c _ -> + Format.fprintf fmt "@[type %a %s.@]@\n" ED.Constants.pp c name) constants in { Conversion.embed; readback; ty; pp_doc; pp = (fun fmt x -> pp fmt (cin x)) } @@ -231,8 +235,8 @@ module RawOpaqueData = struct else "@" in let constants = List.fold_right (fun (n,v) -> - Elpi_data.Constants.Map.add (Elpi_data.Constants.from_stringc n) v) - constants Elpi_data.Constants.Map.empty in + ED.Constants.Map.add (ED.Constants.from_stringc n) v) + constants ED.Constants.Map.empty in conversion_of_cdata ~name:(prefix^name) ?doc ~constants cd let declare { name; doc; pp; eq; hash; hconsed; constants; } = @@ -269,10 +273,10 @@ end module BuiltInData = struct - let int = RawOpaqueData.conversion_of_cdata ~name:"int" Elpi_data.C.int - let float = RawOpaqueData.conversion_of_cdata ~name:"float" Elpi_data.C.float - let string = RawOpaqueData.conversion_of_cdata ~name:"string" Elpi_data.C.string - let loc = RawOpaqueData.conversion_of_cdata ~name:"loc" Elpi_data.C.loc + let int = RawOpaqueData.conversion_of_cdata ~name:"int" ED.C.int + let float = RawOpaqueData.conversion_of_cdata ~name:"float" ED.C.float + let string = RawOpaqueData.conversion_of_cdata ~name:"string" ED.C.string + let loc = RawOpaqueData.conversion_of_cdata ~name:"loc" ED.C.loc let poly ty = let embed ~depth:_ _ _ state x = state, x, [] in let readback ~depth _ _ state t = state, t in @@ -311,7 +315,7 @@ module BuiltInData = struct (lp_list_to_list ~depth t) in let pp fmt l = - Format.fprintf fmt "[%a]" (Elpi_util.pplist d.pp ~boxed:true "; ") l in + Format.fprintf fmt "[%a]" (Util.pplist d.pp ~boxed:true "; ") l in { Conversion.embed; readback; ty = TyApp ("list",d.ty,[]); pp; @@ -321,7 +325,7 @@ module BuiltInData = struct end module Elpi = struct - type uvarHandle = Arg of string | Ref of Elpi_data.uvar_body + type uvarHandle = Arg of string | Ref of ED.uvar_body [@@deriving show] type t = { @@ -342,47 +346,47 @@ module Elpi = struct let compilation_is_over ~args k = match k.handle with | Ref _ -> assert false - | Arg s -> { k with handle = Ref (Elpi_util.StrMap.find s args) } + | Arg s -> { k with handle = Ref (Util.StrMap.find s args) } (* This is to hide to the client the fact that Args change representation after compilation *) - let uvk = Elpi_data.State.declare ~name:"elpi:uvk" ~pp:(Elpi_util.StrMap.pp pp) + let uvk = ED.State.declare ~name:"elpi:uvk" ~pp:(Util.StrMap.pp pp) ~compilation_is_over:(fun ~args x -> - Some (Elpi_util.StrMap.map (compilation_is_over ~args) x)) - ~init:(fun () -> Elpi_util.StrMap.empty) + Some (Util.StrMap.map (compilation_is_over ~args) x)) + ~init:(fun () -> Util.StrMap.empty) let fresh_name = let i = ref 0 in fun () -> incr i; Printf.sprintf "_uvk_%d_" !i let alloc_Elpi name lvl state = - if Elpi_data.State.get Elpi_compiler.while_compiling state then - let state, _arg = Elpi_compiler.mk_Arg ~name ~args:[] state in + if ED.State.get Compiler.while_compiling state then + let state, _arg = Compiler.mk_Arg ~name ~args:[] state in state, { lvl; handle = Arg name } else - state, { lvl; handle = Ref (Elpi_data.oref Elpi_data.Constants.dummy) } + state, { lvl; handle = Ref (ED.oref ED.Constants.dummy) } let make ?name ~lvl state = match name with | None -> alloc_Elpi (fresh_name ()) lvl state | Some name -> - try state, Elpi_util.StrMap.find name (Elpi_data.State.get uvk state) + try state, Util.StrMap.find name (ED.State.get uvk state) with Not_found -> let state, k = alloc_Elpi name lvl state in - Elpi_data.State.update uvk state (Elpi_util.StrMap.add name k), k + ED.State.update uvk state (Util.StrMap.add name k), k let get ~name state = - try Some (Elpi_util.StrMap.find name (Elpi_data.State.get uvk state)) + try Some (Util.StrMap.find name (ED.State.get uvk state)) with Not_found -> None end module RawData = struct - type constant = Elpi_data.Term.constant - type builtin = Elpi_data.Term.constant - type uvar_body = Elpi_data.Term.uvar_body - type term = Elpi_data.Term.term + type constant = ED.Term.constant + type builtin = ED.Term.constant + type uvar_body = ED.Term.uvar_body + type term = ED.Term.term type view = (* Pure subterms *) | Const of constant (* global constant or a bound var *) @@ -401,45 +405,45 @@ module RawData = struct let look ~depth t = let module R = (val !r) in let open R in match R.deref_head ~depth t with - | Elpi_data.Term.Arg _ | Elpi_data.Term.AppArg _ -> assert false - | Elpi_data.Term.UVar(ub,lvl,nargs) -> - let args = Elpi_data.Term.Constants.mkinterval 0 nargs 0 in + | ED.Term.Arg _ | ED.Term.AppArg _ -> assert false + | ED.Term.UVar(ub,lvl,nargs) -> + let args = ED.Term.Constants.mkinterval 0 nargs 0 in UnifVar ({ lvl; handle = Ref ub},args) - | Elpi_data.Term.AppUVar(ub,lvl,args) -> + | ED.Term.AppUVar(ub,lvl,args) -> UnifVar ({ lvl; handle = Ref ub},args) | x -> Obj.magic x (* HACK: view is a "subtype" of Term.term *) let kool = function - | UnifVar({ lvl; handle = Ref ub},args) -> Elpi_data.Term.AppUVar(ub,lvl,args) + | UnifVar({ lvl; handle = Ref ub},args) -> ED.Term.AppUVar(ub,lvl,args) | UnifVar({ lvl; handle = Arg _},_) -> assert false | x -> Obj.magic x [@@ inline] - let mkConst = Elpi_data.Term.mkConst - let mkLam = Elpi_data.Term.mkLam - let mkApp = Elpi_data.Term.mkApp - let mkCons = Elpi_data.Term.mkCons - let mkNil = Elpi_data.Term.mkNil - let mkDiscard = Elpi_data.Term.mkDiscard - let mkBuiltin = Elpi_data.Term.mkBuiltin - let mkCData = Elpi_data.Term.mkCData - let mkAppL = Elpi_data.Term.mkAppL - let mkAppS = Elpi_data.Term.mkAppS - let mkAppSL = Elpi_data.Term.mkAppSL + let mkConst = ED.Term.mkConst + let mkLam = ED.Term.mkLam + let mkApp = ED.Term.mkApp + let mkCons = ED.Term.mkCons + let mkNil = ED.Term.mkNil + let mkDiscard = ED.Term.mkDiscard + let mkBuiltin = ED.Term.mkBuiltin + let mkCData = ED.Term.mkCData + let mkAppL = ED.Term.mkAppL + let mkAppS = ED.Term.mkAppS + let mkAppSL = ED.Term.mkAppSL - let mkGlobalS s = Elpi_data.Term.Constants.from_string s - let mkBuiltinS s args = mkBuiltin (Elpi_data.BuiltInPredicate.from_builtin_name s) args + let mkGlobalS s = ED.Term.Constants.from_string s + let mkBuiltinS s args = mkBuiltin (ED.BuiltInPredicate.from_builtin_name s) args let mkGlobal i = - if i >= 0 then Elpi_util.anomaly "mkGlobal: got a bound variable"; + if i >= 0 then Util.anomaly "mkGlobal: got a bound variable"; mkConst i let mkBound i = - if i < 0 then Elpi_util.anomaly "mkBound: got a global constant"; + if i < 0 then Util.anomaly "mkBound: got a global constant"; mkConst i - module Constants = Elpi_data.Term.Constants + module Constants = ED.Term.Constants - let of_term = Elpi_data.of_term + let of_term = ED.of_term let of_hyps x = x @@ -454,18 +458,18 @@ module RawData = struct goal : int * term } - type constraints = Elpi_data.constraints + type constraints = Data.constraints - let constraints = Elpi_util.map_filter (function - | { Elpi_data.kind = Constraint { cdepth; conclusion; context } } -> + let constraints = Util.map_filter (function + | { ED.kind = Constraint { cdepth; conclusion; context } } -> Some { context ; goal = (cdepth, conclusion) } | _ -> None) let no_constraints = [] let mkUnifVar { Elpi.handle; lvl } ~args state = match handle with - | Elpi.Ref ub -> Elpi_data.Term.mkAppUVar ub lvl args - | Elpi.Arg name -> Elpi_compiler.get_Arg state ~name ~args + | Elpi.Ref ub -> ED.Term.mkAppUVar ub lvl args + | Elpi.Arg name -> Compiler.get_Arg state ~name ~args end @@ -483,7 +487,7 @@ module FlexibleData = struct (* Bijective map between elpi UVar and host equivalent *) module Map = functor(T : Host) -> struct - open Elpi_util + open Util module H2E = Map.Make(T) @@ -539,8 +543,8 @@ module FlexibleData = struct let module R = (val !r) in let open R in let get_val {Elpi.lvl; handle} = match handle with - | Elpi.Ref { Elpi_data.Term.contents = ub } - when ub != Elpi_data.Term.Constants.dummy -> + | Elpi.Ref { ED.Term.contents = ub } + when ub != ED.Term.Constants.dummy -> Some (lvl, R.deref_head ~depth:lvl ub) | Elpi.Ref _ -> None | Elpi.Arg _ -> None in @@ -549,7 +553,7 @@ module FlexibleData = struct let pp fmt (m : t) = Format.fprintf fmt "" let show m = Format.asprintf "%a" pp m - let uvmap = Elpi_data.State.declare ~name:"elpi:uvm" ~pp + let uvmap = ED.State.declare ~name:"elpi:uvm" ~pp ~compilation_is_over:(fun ~args { h2e; e2h_compile; e2h_run } -> let h2e = H2E.map (Elpi.compilation_is_over ~args) h2e in let e2h_run = @@ -581,18 +585,18 @@ module AlgebraicData = struct type name = string type doc = string - include Elpi_data.BuiltInPredicate.ADT + include ED.BuiltInPredicate.ADT let declare x = let look ~depth t = let module R = (val !r) in R.deref_head ~depth t in - Elpi_data.BuiltInPredicate.adt + ED.BuiltInPredicate.adt ~look ~alloc:FlexibleData.Elpi.make ~mkUnifVar:RawData.mkUnifVar x end module BuiltInPredicate = struct - include Elpi_data.BuiltInPredicate - exception No_clause = Elpi_data.No_clause + include ED.BuiltInPredicate + exception No_clause = ED.No_clause module Notation = struct @@ -606,17 +610,17 @@ module BuiltInPredicate = struct end module BuiltIn = struct - include Elpi_data.BuiltInPredicate + include ED.BuiltInPredicate let declare ~file_name l = file_name, l end module Query = struct - include Elpi_data.Query - let compile = Elpi_compiler.query_of_data + include ED.Query + let compile = Compiler.query_of_data end module State = struct - include Elpi_data.State + include ED.State (* From now on, we pretend there is no difference between terms at compilation time and terms at execution time (in the API) *) let declare ~name ~pp ~init = @@ -626,22 +630,22 @@ end module RawQuery = struct - let mk_Arg = Elpi_compiler.mk_Arg - let is_Arg = Elpi_compiler.is_Arg - let compile = Elpi_compiler.query_of_term + let mk_Arg = Compiler.mk_Arg + let is_Arg = Compiler.is_Arg + let compile = Compiler.query_of_term end module Quotation = struct - include Elpi_compiler + include Compiler let declare_backtick ~name f = - Elpi_data.CustomFunctorCompilation.declare_backtick_compilation name - (fun s x -> f s (Elpi_ast.Func.show x)) + ED.CustomFunctorCompilation.declare_backtick_compilation name + (fun s x -> f s (EA.Func.show x)) let declare_singlequote ~name f = - Elpi_data.CustomFunctorCompilation.declare_singlequote_compilation name - (fun s x -> f s (Elpi_ast.Func.show x)) + ED.CustomFunctorCompilation.declare_singlequote_compilation name + (fun s x -> f s (EA.Func.show x)) - let term_at ~depth x = Elpi_compiler.term_of_ast ~depth x + let term_at ~depth x = Compiler.term_of_ast ~depth x end @@ -657,22 +661,22 @@ module Utils = struct let get_assignment { Elpi.handle } = match handle with | Elpi.Arg _ -> assert false - | Elpi.Ref { Elpi_data.contents = r } -> - if r == Elpi_data.Constants.dummy then None + | Elpi.Ref { ED.contents = r } -> + if r == ED.Constants.dummy then None else Some r let move ~from ~to_ t = let module R = (val !r) in let open R in R.hmove ~from ~to_ ?avoid:None t - let error = Elpi_util.error - let type_error = Elpi_util.type_error - let anomaly = Elpi_util.anomaly - let warn = Elpi_util.warn + let error = Util.error + let type_error = Util.type_error + let anomaly = Util.anomaly + let warn = Util.warn let clause_of_term ?name ?graft ~depth loc term = - let open Elpi_ast in - let module Data = Elpi_data.Term in + let open EA in + let module Data = ED.Term in let module R = (val !r) in let open R in let rec aux d ctx t = match R.deref_head ~depth:d t with @@ -680,10 +684,10 @@ module Utils = struct error "program_of_term: the term is not closed" | Data.Const i when i < 0 -> Term.mkCon (Data.Constants.show i) - | Data.Const i -> Elpi_util.IntMap.find i ctx + | Data.Const i -> Util.IntMap.find i ctx | Data.Lam t -> let s = "x" ^ string_of_int d in - let ctx = Elpi_util.IntMap.add d (Term.mkCon s) ctx in + let ctx = Util.IntMap.add d (Term.mkCon s) ctx in Term.mkLam s (aux (d+1) ctx t) | Data.App(c,x,xs) -> let c = aux d ctx (Data.Constants.mkConst c) in @@ -714,7 +718,7 @@ module Utils = struct [Program.Clause { Clause.loc = loc; attributes; - body = aux depth Elpi_util.IntMap.empty term; + body = aux depth Util.IntMap.empty term; }] let map_acc_embed = BuiltInData.map_acc_embed @@ -725,18 +729,18 @@ end module RawPp = struct let term depth fmt t = let module R = (val !r) in let open R in - R.Pp.uppterm depth [] 0 Elpi_data.empty_env fmt t + R.Pp.uppterm depth [] 0 ED.empty_env fmt t let constraint_ f c = let module R = (val !r) in let open R in R.pp_stuck_goal f c - let list = Elpi_util.pplist + let list = Util.pplist module Debug = struct let term depth fmt t = let module R = (val !r) in let open R in - R.Pp.ppterm depth [] 0 Elpi_data.empty_env fmt t - let show_term = Elpi_data.show_term + R.Pp.ppterm depth [] 0 ED.empty_env fmt t + let show_term = ED.show_term end end diff --git a/src/elpi_API.mli b/src/API.mli similarity index 99% rename from src/elpi_API.mli rename to src/API.mli index 39b6774db..ba5707bf6 100644 --- a/src/elpi_API.mli +++ b/src/API.mli @@ -872,7 +872,7 @@ module Quotation : sig (** The anti-quotation to lambda Prolog *) val lp : quotation - (** See elpi_quoted_syntax.elpi (EXPERIMENTAL, used by elpi-checker) *) + (** See elpi-quoted_syntax.elpi (EXPERIMENTAL, used by elpi-checker) *) val quote_syntax : 'a Compile.query -> Data.term list * Data.term (** To implement the string_to_term built-in (AVOID, makes little sense diff --git a/src/elpi_ast.ml b/src/ast.ml similarity index 99% rename from src/elpi_ast.ml rename to src/ast.ml index 1d9e9a195..c8833c70b 100644 --- a/src/elpi_ast.ml +++ b/src/ast.ml @@ -2,7 +2,7 @@ (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) -open Elpi_util +open Util module Func = struct @@ -59,7 +59,7 @@ module Term = struct | Const of Func.t | App of t * t list | Lam of Func.t * t - | CData of Elpi_util.CData.t + | CData of CData.t | Quoted of quote and quote = { data : string; loc : Loc.t; kind : string option } [@@deriving show, eq] @@ -225,8 +225,7 @@ module Goal = struct type t = Loc.t * Term.t [@@deriving show] end - -open Elpi_util + module Fmt = Format let { CData.cin = in_float; isc = is_float; cout = out_float } as cfloat = diff --git a/src/elpi_ast.mli b/src/ast.mli similarity index 97% rename from src/elpi_ast.mli rename to src/ast.mli index a6ebbe436..77ff60ad0 100644 --- a/src/elpi_ast.mli +++ b/src/ast.mli @@ -2,7 +2,7 @@ (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) -open Elpi_util +open Util (* Prolog functors *) module Func : sig @@ -42,7 +42,7 @@ module Term : sig | Const of Func.t | App of t * t list | Lam of Func.t * t - | CData of Elpi_util.CData.t + | CData of CData.t | Quoted of quote and quote = { data : string; loc : Loc.t; kind : string option } @@ -62,7 +62,7 @@ module Term : sig val mkFreshUVar : unit -> t val mkFreshName : unit -> t val mkLam : string -> t -> t - val mkC : Elpi_util.CData.t -> t + val mkC : CData.t -> t end module Clause : sig @@ -227,7 +227,7 @@ end (* These are declared here for convenience *) -open Elpi_util.CData +open CData val cfloat : float cdata val cint : int cdata diff --git a/src/builtin.elpi b/src/builtin.elpi index f2f7dd9ae..a9c2fcdf5 100644 --- a/src/builtin.elpi +++ b/src/builtin.elpi @@ -270,7 +270,7 @@ external pred rex_match i:string, i:string. external pred rex_replace i:string, i:string, i:string, o:string. % [quote_syntax FileName QueryText QuotedProgram QuotedQuery] quotes the -% program from FileName and the QueryText. See elpi_quoted_syntax.elpi for +% program from FileName and the QueryText. See elpi-quoted_syntax.elpi for % the syntax tree external pred quote_syntax i:string, i:string, o:list A, o:A. diff --git a/src/elpi_builtin.ml b/src/builtin.ml similarity index 98% rename from src/elpi_builtin.ml rename to src/builtin.ml index ad9d0f645..fce2623bb 100644 --- a/src/elpi_builtin.ml +++ b/src/builtin.ml @@ -2,7 +2,7 @@ (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) -open Elpi_API +open API open RawData open Constants open Utils @@ -214,7 +214,7 @@ let bool = AlgebraicData.declare { let pair a b = let open AlgebraicData in declare { ty = TyApp ("pair",a.Conversion.ty,[b.Conversion.ty]); doc = "Pair: the constructor is pr, since ',' is for conjunction"; - pp = (fun fmt o -> Format.fprintf fmt "%a" (Elpi_util.pp_pair a.Conversion.pp b.Conversion.pp) o); + pp = (fun fmt o -> Format.fprintf fmt "%a" (Util.pp_pair a.Conversion.pp b.Conversion.pp) o); constructors = [ K("pr","",A(a,A(b,N)), B (fun a b -> (a,b)), @@ -225,7 +225,7 @@ let pair a b = let open AlgebraicData in declare { let option a = let open AlgebraicData in declare { ty = TyApp("option",a.Conversion.ty,[]); doc = "The option type (aka Maybe)"; - pp = (fun fmt o -> Format.fprintf fmt "%a" (Elpi_util.pp_option a.Conversion.pp) o); + pp = (fun fmt o -> Format.fprintf fmt "%a" (Util.pp_option a.Conversion.pp) o); constructors = [ K("none","",N, B None, @@ -686,14 +686,14 @@ let elpi_builtins = let open BuiltIn in let open BuiltInData in [ Out(list (poly "A"), "QuotedProgram", Out(poly "A", "QuotedQuery", Easy ("quotes the program from FileName and the QueryText. "^ - "See elpi_quoted_syntax.elpi for the syntax tree"))))), + "See elpi-quoted_syntax.elpi for the syntax tree"))))), (fun f s _ _ ~depth -> let ap = Parse.program [f] in let loc = Ast.Loc.initial "(quote_syntax)" in let aq = Parse.goal loc s in let p = - Elpi_API.Compile.(program ~flags:default_flags dummy_header [ap]) in - let q = Elpi_API.Compile.query p aq in + API.Compile.(program ~flags:default_flags dummy_header [ap]) in + let q = API.Compile.query p aq in let qp, qq = Quotation.quote_syntax q in !: qp +! qq)), DocAbove); diff --git a/src/elpi_builtin.mli b/src/builtin.mli similarity index 71% rename from src/elpi_builtin.mli rename to src/builtin.mli index 64f44c229..17c6a44bb 100644 --- a/src/elpi_builtin.mli +++ b/src/builtin.mli @@ -4,7 +4,7 @@ (* This module provides all the built-in predicates and evaluable constants. *) -open Elpi_API.BuiltIn +open API.BuiltIn (* Builtins that are part of the language, like "is" or "!" *) val core_builtins : declaration list @@ -26,13 +26,13 @@ val elpi_stdlib : declaration list (* All the above, to be used as a sane default in Setup.init *) val std_declarations : declaration list -val std_builtins : Elpi_API.Setup.builtins +val std_builtins : API.Setup.builtins (* Type descriptors for built-in predicates *) -val pair : 'a Elpi_API.Conversion.t -> 'b Elpi_API.Conversion.t -> ('a * 'b) Elpi_API.Conversion.t -val option : 'a Elpi_API.Conversion.t -> 'a option Elpi_API.Conversion.t -val bool : bool Elpi_API.Conversion.t +val pair : 'a API.Conversion.t -> 'b API.Conversion.t -> ('a * 'b) API.Conversion.t +val option : 'a API.Conversion.t -> 'a option API.Conversion.t +val bool : bool API.Conversion.t (* The string is the "file name" *) -val in_stream : (in_channel * string) Elpi_API.Conversion.t -val out_stream : (out_channel * string) Elpi_API.Conversion.t +val in_stream : (in_channel * string) API.Conversion.t +val out_stream : (out_channel * string) API.Conversion.t diff --git a/src/elpi_compiler.ml b/src/compiler.ml similarity index 98% rename from src/elpi_compiler.ml rename to src/compiler.ml index 88c45d8ff..c6f8393ba 100644 --- a/src/elpi_compiler.ml +++ b/src/compiler.ml @@ -2,11 +2,9 @@ (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) -open Elpi_util -module Ast = Elpi_ast +open Util module F = Ast.Func - -module R = Elpi_runtime_trace_off +module R = Runtime_trace_off type flags = { defined_variables : StrSet.t; @@ -63,7 +61,7 @@ and 'a shorthand = { end -open Elpi_data +open Data module C = Constants module Structured = struct @@ -165,7 +163,7 @@ type 'a query = 'a WithMain.query module Executable = struct (* All that is needed in order to execute, and nothing more *) -type 'a executable = 'a Elpi_data.executable = { +type 'a executable = 'a Data.executable = { (* the lambda-Prolog program: an indexed list of clauses *) compiled_program : prolog_prog; (* chr rules *) @@ -389,7 +387,7 @@ module ToDBL : sig (* Exported to compile the query *) val preterm_of_ast : depth:int -> macro_declaration -> State.t -> - Loc.t * Elpi_ast.Term.t -> State.t * preterm + Loc.t * Ast.Term.t -> State.t * preterm val preterm_of_function : depth:int -> macro_declaration -> State.t -> (State.t -> State.t * (Loc.t * term)) -> @@ -568,14 +566,14 @@ let preterm_of_ast loc ~depth:arg_lvl macro state ast = option_get ~err:"No default quotation" !default_quotation in let state = set_mtm state (Some { macros = macro}) in begin try unquote ~depth:lvl state loc data - with Elpi_parser.ParseError(loc,msg) -> error ~loc msg end + with Parser.ParseError(loc,msg) -> error ~loc msg end | Ast.Term.Quoted { Ast.Term.data; kind = Some name; loc } -> let unquote = try StrMap.find name !named_quotations with Not_found -> anomaly ("No '"^name^"' quotation") in let state = set_mtm state (Some { macros = macro}) in begin try unquote ~depth:lvl state loc data - with Elpi_parser.ParseError(loc,msg) -> error ~loc msg end + with Parser.ParseError(loc,msg) -> error ~loc msg end | Ast.Term.App (Ast.Term.Quoted _,_) -> type_error ~loc "Applied quotation" in @@ -584,7 +582,7 @@ let preterm_of_ast loc ~depth:arg_lvl macro state ast = ;; let lp ~depth state loc s = - let loc, ast = Elpi_parser.parse_goal ~loc s in + let loc, ast = Parser.parse_goal ~loc s in let macros = match get_mtm state with | None -> F.Map.empty @@ -1073,7 +1071,7 @@ end = struct (* {{{ *) let argmap = ref argmap in let mk_Arg n = - let m, (x,_) = Elpi_data.mk_Arg n !argmap in + let m, (x,_) = Data.mk_Arg n !argmap in argmap := m; x in @@ -1312,7 +1310,7 @@ let program_of_ast ~flags:({ print_passes } as flags) p = if print_passes then Format.eprintf "== AST ================@\n@[%a@]@\n" - Elpi_ast.Program.pp p; + Ast.Program.pp p; let p = RecoverStructure.run ~flags p in @@ -1596,7 +1594,7 @@ let run (List.map (compile_clause modes initial_depth) (filter_if flags.defined_variables ifexpr clauses)) in { - Elpi_data.compiled_program = prolog_program; + Data.compiled_program = prolog_program; chr; initial_depth; initial_goal; @@ -1643,7 +1641,7 @@ let pp_query pp fmt { ;; (**************************************************************************** - Quotation (for static checkers, see elpi_quoted_syntax.elpi) + Quotation (for static checkers, see elpi-quoted_syntax.elpi) ****************************************************************************) let constc = C.from_stringc "const" @@ -1666,7 +1664,7 @@ let mkQCon ~on_type ?(amap=empty_amap) c = try mkConst (C.Map.find c amap.c2i) with Not_found -> let a = if on_type then tconstc else constc in - if c < 0 then App(a,Elpi_data.C.of_string (C.show c),[]) + if c < 0 then App(a,Data.C.of_string (C.show c),[]) else mkConst (c + amap.nargs) let quote_preterm ?(on_type=false) { term; amap } = @@ -1674,13 +1672,13 @@ let quote_preterm ?(on_type=false) { term; amap } = let mkQCon = mkQCon ~on_type ~amap in let rec aux depth term = match term with | Const n when on_type && C.show n = "string" -> - App(C.ctypec, Elpi_data.C.of_string "string",[]) + App(C.ctypec, Data.C.of_string "string",[]) | Const n when on_type && C.show n = "int" -> - App(C.ctypec, Elpi_data.C.of_string "int",[]) + App(C.ctypec, Data.C.of_string "int",[]) | Const n when on_type && C.show n = "float" -> - App(C.ctypec, Elpi_data.C.of_string "float",[]) + App(C.ctypec, Data.C.of_string "float",[]) | App(c,CData s,[]) - when on_type && c == C.ctypec && Elpi_data.C.is_string s -> term + when on_type && c == C.ctypec && Data.C.is_string s -> term | App(c,s,[t]) when on_type && c == C.arrowc -> App(arrowc,aux depth s,[aux depth t]) | Const n when on_type && C.show n = "prop" -> term @@ -1724,7 +1722,7 @@ let close_w_binder binder t { nargs } = let sorted_names_of_argmap argmap = IntMap.bindings argmap.i2n |> List.map snd |> - List.map Elpi_data.C.of_string + List.map Data.C.of_string let quote_loc ?id loc = let source_name = @@ -1750,9 +1748,9 @@ let quote_syntax { WithMain.clauses; query } = clist, q let default_checker () = - try Elpi_parser.parse_program + try Parser.parse_program ~print_accumulated_files:false ["elpi-checker.elpi"] - with Elpi_parser.ParseError(loc,err) -> error ~loc err + with Parser.ParseError(loc,err) -> error ~loc err let static_check header ?(exec=R.execute_once ~delay_outside_fragment:false) ?(checker=default_checker ()) ?(flags=default_flags) @@ -1769,7 +1767,7 @@ let static_check header program_of_ast ~flags:{ flags with allow_untyped_builtin = true } (header @ checker) in - let loc = Elpi_util.Loc.initial "(static_check)" in + let loc = Loc.initial "(static_check)" in let query = query_of_term checker (fun ~depth state -> assert(depth=0); diff --git a/src/elpi_compiler.mli b/src/compiler.mli similarity index 71% rename from src/elpi_compiler.mli rename to src/compiler.mli index 8ccfcbe0b..fd6920629 100644 --- a/src/elpi_compiler.mli +++ b/src/compiler.mli @@ -2,8 +2,8 @@ (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) -open Elpi_util -open Elpi_data +open Util +open Data type flags = { defined_variables : StrSet.t; @@ -16,8 +16,8 @@ type program type 'a query (* Flags are threaded *) -val program_of_ast : flags:flags -> Elpi_ast.Program.t -> program -val query_of_ast : program -> Elpi_ast.Goal.t -> unit query +val program_of_ast : flags:flags -> Ast.Program.t -> program +val query_of_ast : program -> Ast.Goal.t -> unit query val query_of_term : program -> (depth:int -> State.t -> State.t * (Loc.t * term)) -> unit query val query_of_data : @@ -25,9 +25,9 @@ val query_of_data : val pp_query : (depth:int -> Format.formatter -> term -> unit) -> Format.formatter -> 'a query -> unit -val executable_of_query : 'a query -> 'a Elpi_data.executable +val executable_of_query : 'a query -> 'a executable -val term_of_ast : depth:int -> Loc.t * Elpi_ast.Term.t -> term +val term_of_ast : depth:int -> Loc.t * Ast.Term.t -> term type quotation = depth:int -> State.t -> Loc.t -> string -> State.t * term val set_default_quotation : quotation -> unit @@ -42,13 +42,13 @@ val mk_Arg : State.t * term val get_Arg : State.t -> name:string -> args:term list -> term -(* Quotes the program and the query, see elpi_quoted_syntax.elpi *) +(* Quotes the program and the query, see elpi-quoted_syntax.elpi *) val quote_syntax : 'a query -> term list * term (* false means a type error was found *) -val static_check : Elpi_ast.Program.t -> (* header *) - ?exec:(?max_steps:int -> unit Elpi_data.executable -> unit Elpi_data.outcome) -> - ?checker:Elpi_ast.Program.t -> +val static_check : Ast.Program.t -> (* header *) + ?exec:(?max_steps:int -> unit executable -> unit outcome) -> + ?checker:Ast.Program.t -> ?flags:flags -> 'a query -> bool diff --git a/src/elpi_data.ml b/src/data.ml similarity index 98% rename from src/elpi_data.ml rename to src/data.ml index 5e76a424b..5731eae0e 100644 --- a/src/elpi_data.ml +++ b/src/data.ml @@ -5,8 +5,8 @@ (* Internal term representation *) module Fmt = Format -module F = Elpi_ast.Func -open Elpi_util +module F = Ast.Func +open Util (****************************************************************************** Terms: data type definition and printing @@ -98,20 +98,20 @@ and prolog_prog = { src : clause_src list; (* hypothetical context in original form, for CHR *) index : index; } -and index = second_lvl_idx Elpi_ptmap.t +and index = second_lvl_idx Ptmap.t and second_lvl_idx = | TwoLevelIndex of { mode : mode; argno : int; all_clauses : clause list; (* when the query is flexible *) flex_arg_clauses : clause list; (* when the query is rigid but arg_id ha nothing *) - arg_idx : clause list Elpi_ptmap.t; (* when the query is rigid (includes in each binding flex_arg_clauses) *) + arg_idx : clause list Ptmap.t; (* when the query is rigid (includes in each binding flex_arg_clauses) *) } | BitHash of { mode : mode; args : int list; time : int; (* time is used to recover the total order *) - args_idx : (clause * int) list Elpi_ptmap.t; (* clause, insertion time *) + args_idx : (clause * int) list Ptmap.t; (* clause, insertion time *) } and clause = { depth : int; @@ -143,24 +143,24 @@ let mkAppArg i args = AppArg(i,args) [@@inline] module C = struct let { CData.cin = in_int; isc = is_int; cout = out_int } as int = - Elpi_ast.cint + Ast.cint let is_int = is_int let to_int = out_int let of_int x = CData (in_int x) let { CData.cin = in_float; isc = is_float; cout = out_float } as float = - Elpi_ast.cfloat + Ast.cfloat let is_float = is_float let to_float = out_float let of_float x = CData (in_float x) let { CData.cin = in_string; isc = is_string; cout = out_string } as string = - Elpi_ast.cstring + Ast.cstring let is_string = is_string let to_string x = out_string x let of_string x = CData (in_string x) - let loc = Elpi_ast.cloc + let loc = Ast.cloc let is_loc = loc.CData.isc let to_loc = loc.CData.cout let of_loc x = CData (loc.CData.cin x) @@ -582,7 +582,7 @@ type clause_w_info = { } [@@ deriving show] -type macro_declaration = (Elpi_ast.Term.t * Loc.t) F.Map.t +type macro_declaration = (Ast.Term.t * Loc.t) F.Map.t [@@ deriving show] (* This is paired with a pre-stack term, i.e. a stack term where args are @@ -851,7 +851,7 @@ and embed : type a. fun ~depth hyps constraints state t -> let rec aux l state = match l with - | [] -> Elpi_util.type_error + | [] -> type_error ("Pattern matching failure embedding: " ^ Conversion.show_ty_ast ty ^ Format.asprintf ": %a" pp t) | (kname, CK(args,_,matcher)) :: rest -> let ok = adt_embed_args ty adt kname ~depth hyps constraints args [] in @@ -901,7 +901,6 @@ let compile_matcher : type bs b m ms t. (bs,b,ms,m,t) constructor_arguments -> ( | MS f -> f let compile_constructors ty self l = - let open Elpi_util in let names = List.fold_right (fun (K(name,_,_,_,_)) -> StrSet.add name) l StrSet.empty in if StrSet.cardinal names <> List.length l then diff --git a/src/dune b/src/dune index d99aaa4ae..b4a0aecf1 100644 --- a/src/dune +++ b/src/dune @@ -2,25 +2,25 @@ (name elpi) (public_name elpi) (preprocess (per_module - ((pps ppx_deriving.std) elpi_API elpi_util elpi_ast elpi_data elpi_compiler) - ((pps ppx_deriving.std trace_ppx --trace_ppx-on) elpi_runtime_trace_on) - ((pps ppx_deriving.std trace_ppx --trace_ppx-off) elpi_runtime_trace_off) - ((action (system "camlp5o -I . -I +camlp5 pa_extend.cmo pa_lexer.cmo %{input-file}")) elpi_parser) + ((pps ppx_deriving.std) API util ast data compiler) + ((pps ppx_deriving.std trace_ppx --trace_ppx-on) runtime_trace_on) + ((pps ppx_deriving.std trace_ppx --trace_ppx-off) runtime_trace_off) + ((action (system "camlp5o -I . -I +camlp5 pa_extend.cmo pa_lexer.cmo %{input-file}")) parser) )) (libraries re.str camlp5.gramlib unix) (flags -linkall) - (modules elpi elpi_util elpi_parser elpi_ast elpi_compiler elpi_data elpi_ptmap elpi_builtin elpi_API elpi_runtime_trace_on elpi_runtime_trace_off) - (private_modules elpi_util elpi_parser elpi_ast elpi_compiler elpi_data elpi_ptmap elpi_runtime_trace_on elpi_runtime_trace_off) + (modules elpi util parser ast compiler data ptmap builtin API runtime_trace_on runtime_trace_off) + (private_modules util parser ast compiler data ptmap runtime_trace_on runtime_trace_off) ) -(rule (copy# elpi_runtime.ml elpi_runtime_trace_on.ml)) -(rule (copy# elpi_runtime.ml elpi_runtime_trace_off.ml)) -(rule (copy# elpi_runtime.mli elpi_runtime_trace_on.mli)) -(rule (copy# elpi_runtime.mli elpi_runtime_trace_off.mli)) +(rule (copy# runtime.ml runtime_trace_on.ml)) +(rule (copy# runtime.ml runtime_trace_off.ml)) +(rule (copy# runtime.mli runtime_trace_on.mli)) +(rule (copy# runtime.mli runtime_trace_off.mli)) (install (section lib) - (files builtin.elpi elpi-checker.elpi elpi_quoted_syntax.elpi elpi2html.elpi) + (files builtin.elpi elpi-checker.elpi elpi-quoted_syntax.elpi elpi2html.elpi) ) (rule diff --git a/src/elpi-checker.elpi b/src/elpi-checker.elpi index 2d3e469de..8a4cbf3f1 100644 --- a/src/elpi-checker.elpi +++ b/src/elpi-checker.elpi @@ -3,7 +3,7 @@ /* ------------------------------------------------------------------------- */ % Simple type checker for lambda-Prolog programs -accumulate elpi_quoted_syntax. +accumulate elpi-quoted_syntax. % --------- HOAS or programs ------------------------------------------------ diff --git a/src/elpi_quoted_syntax.elpi b/src/elpi-quoted_syntax.elpi similarity index 100% rename from src/elpi_quoted_syntax.elpi rename to src/elpi-quoted_syntax.elpi diff --git a/src/elpi.ml b/src/elpi.ml index 93e7659e3..8c7b887f5 100644 --- a/src/elpi.ml +++ b/src/elpi.ml @@ -1,2 +1,2 @@ -module Elpi_API = Elpi_API -module Elpi_builtin = Elpi_builtin +module API = API +module Builtin = Builtin diff --git a/src/elpi2html.elpi b/src/elpi2html.elpi index c23abb425..e6bd87359 100644 --- a/src/elpi2html.elpi +++ b/src/elpi2html.elpi @@ -2,7 +2,7 @@ /* license: GNU Lesser General Public License Version 2.1 or later */ /* ------------------------------------------------------------------------- */ -accumulate elpi_quoted_syntax. +accumulate elpi-quoted_syntax. shorten std.{spy, rev, exists}. diff --git a/src/elpi_parser.ml b/src/parser.ml similarity index 99% rename from src/elpi_parser.ml rename to src/parser.ml index 8ef13664b..d3da28f6b 100644 --- a/src/elpi_parser.ml +++ b/src/parser.ml @@ -2,9 +2,9 @@ (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) -module U = Elpi_util +module U = Util module Loc = U.Loc -open Elpi_ast +open Ast open Term module Str = Re.Str @@ -471,7 +471,7 @@ let desugar_multi_binder loc = function let names = List.map (function | Const x -> Func.show x | (App _ | Lam _ | CData _ | Quoted _) -> - Elpi_util.error "multi binder syntax") rev_rest in + U.error "multi binder syntax") rev_rest in let body = mkApp (of_ploc loc) [binder;last] in List.fold_left (fun bo name -> mkApp (of_ploc loc) [binder;mkLam name bo]) body names | (App _ | Const _ | Lam _ | CData _ | Quoted _) as t -> t @@ -488,7 +488,7 @@ let desugar_macro loc = function let names = List.map (function | Const x -> Func.show x | (App _ | Lam _ | CData _ | Quoted _) -> - Elpi_util.error ~loc "macro binder syntax") args in + U.error ~loc "macro binder syntax") args in name, List.fold_right mkLam names body | (App _ | Const _ | Lam _ | CData _ | Quoted _) as x -> raise (Stream.Error ("Illformed macro:" ^ show x)) diff --git a/src/elpi_parser.mli b/src/parser.mli similarity index 98% rename from src/elpi_parser.mli rename to src/parser.mli index 37705e457..5e3747feb 100644 --- a/src/elpi_parser.mli +++ b/src/parser.mli @@ -2,8 +2,8 @@ (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) -open Elpi_util -open Elpi_ast +open Util +open Ast type fixity = Infixl | Infixr | Infix | Prefix | Prefixr | Postfix | Postfixl diff --git a/src/elpi_ptmap.ml b/src/ptmap.ml similarity index 99% rename from src/elpi_ptmap.ml rename to src/ptmap.ml index 5cf27cdb6..0a5becc6f 100644 --- a/src/elpi_ptmap.ml +++ b/src/ptmap.ml @@ -225,7 +225,7 @@ let to_list s = let pp f fmt m = let l = to_list m in - Elpi_util.(pplist (pp_pair Int.pp f) " " fmt l) + Util.(pplist (pp_pair Int.pp f) " " fmt l) let show f m = let b = Buffer.create 20 in diff --git a/src/elpi_ptmap.mli b/src/ptmap.mli similarity index 100% rename from src/elpi_ptmap.mli rename to src/ptmap.mli diff --git a/src/elpi_runtime.ml b/src/runtime.ml similarity index 97% rename from src/elpi_runtime.ml rename to src/runtime.ml index b76102b47..2f5a6e3b7 100644 --- a/src/elpi_runtime.ml +++ b/src/runtime.ml @@ -3,10 +3,10 @@ (* ------------------------------------------------------------------------- *) module Fmt = Format -module F = Elpi_ast.Func -open Elpi_util -open Elpi_data -module C = Elpi_data.Constants +module F = Ast.Func +open Util +open Data +module C = Constants (* Dereferencing an UVar(r,args) when !!r != dummy requires a function of this kind. The pretty printer needs one but will only be defined @@ -37,10 +37,10 @@ let do_app_deref = ref (fun ?avoid ~from ~to_ _ _ -> assert false);; let m = ref [];; let n = ref 0;; -let min_prec = Elpi_parser.min_precedence -let appl_prec = Elpi_parser.appl_precedence -let lam_prec = Elpi_parser.lam_precedence -let inf_prec = Elpi_parser.inf_precedence +let min_prec = Parser.min_precedence +let appl_prec = Parser.appl_precedence +let lam_prec = Parser.lam_precedence +let inf_prec = Parser.inf_precedence let xppterm ~nice ?(min_prec=min_prec) depth0 names argsdepth env f t = let pp_app f pphd pparg ?pplastarg (hd,args) = @@ -117,7 +117,7 @@ let xppterm ~nice ?(min_prec=min_prec) depth0 names argsdepth env f t = | (Cons _ | Nil) -> let prefix,last = flat_cons_to_list depth [] t in Fmt.fprintf f "[" ; - pplist ~boxed:true (aux Elpi_parser.list_element_prec depth) ", " f prefix ; + pplist ~boxed:true (aux Parser.list_element_prec depth) ", " f prefix ; if last != Nil then begin Fmt.fprintf f " | " ; aux prec 1 f last @@ -127,25 +127,25 @@ let xppterm ~nice ?(min_prec=min_prec) depth0 names argsdepth env f t = | App (hd,x,xs) -> (try let assoc,hdlvl = - Elpi_parser.precedence_of (F.from_string (C.show hd)) in + Parser.precedence_of (F.from_string (C.show hd)) in with_parens hdlvl (fun _ -> match assoc with - Elpi_parser.Infix when List.length xs = 1 -> + Parser.Infix when List.length xs = 1 -> Fmt.fprintf f "@[%a@ %a@ %a@]" (aux (hdlvl+1) depth) x ppconstant hd (aux (hdlvl+1) depth) (List.hd xs) - | Elpi_parser.Infixl when List.length xs = 1 -> + | Parser.Infixl when List.length xs = 1 -> Fmt.fprintf f "@[%a@ %a@ %a@]" (aux hdlvl depth) x ppconstant hd (aux (hdlvl+1) depth) (List.hd xs) - | Elpi_parser.Infixr when List.length xs = 1 -> + | Parser.Infixr when List.length xs = 1 -> Fmt.fprintf f "@[%a@ %a@ %a@]" (aux (hdlvl+1) depth) x ppconstant hd (aux hdlvl depth) (List.hd xs) - | Elpi_parser.Prefix when xs = [] -> + | Parser.Prefix when xs = [] -> Fmt.fprintf f "@[%a@ %a@]" ppconstant hd (aux hdlvl depth) x - | Elpi_parser.Postfix when xs = [] -> + | Parser.Postfix when xs = [] -> Fmt.fprintf f "@[%a@ %a@]" (aux hdlvl depth) x ppconstant hd | _ -> @@ -1722,8 +1722,8 @@ let mustbevariablec = min_int (* uvar or uvar t or uvar l t *) let ppclause f ~depth hd { args = args; hyps = hyps; } = Fmt.fprintf f "@[%s %a :- %a.@]" (C.show hd) - (pplist (uppterm ~min_prec:(Elpi_parser.appl_precedence+1) depth [] depth empty_env) " ") args - (pplist (uppterm ~min_prec:(Elpi_parser.appl_precedence+1) depth [] depth empty_env) ", ") hyps + (pplist (uppterm ~min_prec:(Parser.appl_precedence+1) depth [] depth empty_env) " ") args + (pplist (uppterm ~min_prec:(Parser.appl_precedence+1) depth [] depth empty_env) ", ") hyps let tail_opt = function | [] -> [] @@ -1850,75 +1850,75 @@ let hash_clause_arg_list = hash_arg_list false let hash_goal_arg_list = hash_arg_list true let add1clause ~depth m (predicate,clause) = - match Elpi_ptmap.find predicate m with + match Ptmap.find predicate m with | TwoLevelIndex { all_clauses; argno; mode; flex_arg_clauses; arg_idx } -> (* X matches both rigid and flexible terms *) begin match classify_clause_argno ~depth argno mode clause.args with | Variable -> - Elpi_ptmap.add predicate (TwoLevelIndex { + Ptmap.add predicate (TwoLevelIndex { argno; mode; all_clauses = clause :: all_clauses; flex_arg_clauses = clause :: flex_arg_clauses; - arg_idx = Elpi_ptmap.map (fun l_rev -> clause :: l_rev) arg_idx; + arg_idx = Ptmap.map (fun l_rev -> clause :: l_rev) arg_idx; }) m | MustBeVariable -> (* uvar matches only flexible terms (or itself at the meta level) *) let l_rev = - try Elpi_ptmap.find mustbevariablec arg_idx + try Ptmap.find mustbevariablec arg_idx with Not_found -> flex_arg_clauses in - Elpi_ptmap.add predicate (TwoLevelIndex { + Ptmap.add predicate (TwoLevelIndex { argno; mode; all_clauses = clause :: all_clauses; flex_arg_clauses; - arg_idx = Elpi_ptmap.add mustbevariablec (clause::l_rev) arg_idx; + arg_idx = Ptmap.add mustbevariablec (clause::l_rev) arg_idx; }) m | Rigid (arg_hd,matching) -> (* a rigid term matches flexible terms only in unification mode *) let l_rev = - try Elpi_ptmap.find arg_hd arg_idx + try Ptmap.find arg_hd arg_idx with Not_found -> flex_arg_clauses in let all_clauses = if matching then all_clauses else clause :: all_clauses in - Elpi_ptmap.add predicate (TwoLevelIndex { + Ptmap.add predicate (TwoLevelIndex { argno; mode; all_clauses; flex_arg_clauses; - arg_idx = Elpi_ptmap.add arg_hd (clause::l_rev) arg_idx; + arg_idx = Ptmap.add arg_hd (clause::l_rev) arg_idx; }) m end | BitHash { mode; args; time; args_idx } -> let hash = hash_clause_arg_list predicate ~depth clause.args mode args in let clauses = - try Elpi_ptmap.find hash args_idx + try Ptmap.find hash args_idx with Not_found -> [] in - Elpi_ptmap.add predicate (BitHash { + Ptmap.add predicate (BitHash { mode; args; time = time + 1; - args_idx = Elpi_ptmap.add hash ((clause,time) :: clauses) args_idx + args_idx = Ptmap.add hash ((clause,time) :: clauses) args_idx }) m | exception Not_found -> match classify_clause_argno ~depth 0 [] clause.args with | Variable -> - Elpi_ptmap.add predicate (TwoLevelIndex { + Ptmap.add predicate (TwoLevelIndex { argno = 0; mode = []; all_clauses = [clause]; flex_arg_clauses = [clause]; - arg_idx =Elpi_ptmap.empty; + arg_idx =Ptmap.empty; }) m | MustBeVariable -> - Elpi_ptmap.add predicate (TwoLevelIndex { + Ptmap.add predicate (TwoLevelIndex { argno = 0;mode = []; all_clauses = [clause]; flex_arg_clauses = []; - arg_idx = Elpi_ptmap.add mustbevariablec [clause] Elpi_ptmap.empty; + arg_idx = Ptmap.add mustbevariablec [clause] Ptmap.empty; }) m | Rigid (arg_hd,matching) -> let all_clauses = if matching then [] else [clause] in - Elpi_ptmap.add predicate (TwoLevelIndex { + Ptmap.add predicate (TwoLevelIndex { argno = 0;mode = []; all_clauses; flex_arg_clauses = []; - arg_idx = Elpi_ptmap.add arg_hd [clause] Elpi_ptmap.empty; + arg_idx = Ptmap.add arg_hd [clause] Ptmap.empty; }) m let add_clauses ~depth clauses p = @@ -1929,20 +1929,20 @@ let make_index ~depth ~indexing p = let m = Constants.Map.fold (fun predicate (mode, indexing) m -> match indexing with | Hash args -> - Elpi_ptmap.add predicate (BitHash { + Ptmap.add predicate (BitHash { args; mode; time = min_int; - args_idx = Elpi_ptmap.empty; + args_idx = Ptmap.empty; }) m | MapOn argno -> - Elpi_ptmap.add predicate (TwoLevelIndex { + Ptmap.add predicate (TwoLevelIndex { argno; mode; all_clauses = []; flex_arg_clauses = []; - arg_idx = Elpi_ptmap.empty; - }) m) indexing Elpi_ptmap.empty in + arg_idx = Ptmap.empty; + }) m) indexing Ptmap.empty in let p = List.rev p in { index = add_clauses ~depth p m; src = [] } @@ -2001,17 +2001,17 @@ let get_clauses ~depth goal { index = m } = let predicate, goal = predicate_of_goal ~depth goal in let rc = try - match Elpi_ptmap.find predicate m with + match Ptmap.find predicate m with | TwoLevelIndex { all_clauses; argno; mode; flex_arg_clauses; arg_idx } -> begin match classify_goal_argno ~depth argno goal with | Variable -> all_clauses | Rigid arg_hd -> - try Elpi_ptmap.find arg_hd arg_idx + try Ptmap.find arg_hd arg_idx with Not_found -> flex_arg_clauses end | BitHash { args; mode; args_idx } -> let hash = hash_goal_args ~depth mode args goal in - let cl = List.flatten (Elpi_ptmap.find_unifiables hash args_idx) in + let cl = List.flatten (Ptmap.find_unifiables hash args_idx) in List.(map fst (sort (fun (_,cl1) (_,cl2) -> cl2 - cl1) cl)) with Not_found -> [] in @@ -2222,7 +2222,7 @@ let rec claux1 ?loc get_mode vars depth hyps ts lts lcs t = let clausify { index } ~depth t = let get_mode x = - match Elpi_ptmap.find x index with + match Ptmap.find x index with | TwoLevelIndex { mode } -> mode | BitHash { mode } -> mode | exception Not_found -> [] in @@ -2712,7 +2712,7 @@ let exect_builtin_predicate c ~depth idx args = gs ;; -let match_head { Elpi_data.conclusion = x; cdepth } p = +let match_head { conclusion = x; cdepth } p = match deref_head ~depth:cdepth x with | Const x -> x == p | App(x,_,_) -> x == p @@ -2740,7 +2740,7 @@ let try_fire_rule rule (constraints as orig_constraints) = (* Goals are lifted at different depths to avoid collisions *) let max_depth,constraints = List.fold_left (fun (md,res) c -> - let md = md + c.Elpi_data.cdepth in + let md = md + c.cdepth in md, (md,c)::res) (0,[]) constraints in max_depth, List.rev constraints @@ -2748,7 +2748,7 @@ let try_fire_rule rule (constraints as orig_constraints) = let constraints_depts, constraints_contexts, constraints_goals = List.fold_right - (fun (dto,{Elpi_data.context = c; cdepth = d; conclusion = g}) + (fun (dto,{context = c; cdepth = d; conclusion = g}) (ds, ctxs, gs) -> (dto,d,d) :: ds, (dto,d,c) :: ctxs, (dto,d,g) :: gs) constraints ([],[],[]) in @@ -2761,7 +2761,7 @@ let try_fire_rule rule (constraints as orig_constraints) = (pats_to_match @ pats_to_remove) ([],[],[]) in let match_eigen i m (dto,d,eigen) pat = - match_goal i max_depth env m (dto,d,Elpi_data.C.of_int eigen) pat in + match_goal i max_depth env m (dto,d,Data.C.of_int eigen) pat in let match_conclusion i m g pat = match_goal i max_depth env m g pat in let match_context i m ctx pctx = @@ -2837,7 +2837,7 @@ let try_fire_rule rule (constraints as orig_constraints) = | Some { CHR.eigen; context; conclusion } -> let eigen = match full_deref ~adepth:max_depth env ~depth:max_depth eigen with - | CData x when Elpi_data.C.is_int x -> Elpi_data.C.to_int x + | CData x when Data.C.is_int x -> Data.C.to_int x | Discard -> max_depth | _ -> error "eigen not resolving to an integer" in let conclusion = @@ -3208,7 +3208,7 @@ let mk_outcome search get_cs assignments = let execute_once ?max_steps ?delay_outside_fragment exec = auxsg := []; let { search; get } = make_runtime ?max_steps ?delay_outside_fragment exec in - fst (mk_outcome search (fun () -> get CS.Ugly.delayed, get CS.state, exec.query_arguments) exec.Elpi_data.assignments) + fst (mk_outcome search (fun () -> get CS.Ugly.delayed, get CS.state, exec.query_arguments) exec.assignments) ;; let execute_loop ?delay_outside_fragment exec ~more ~pp = @@ -3216,7 +3216,7 @@ let execute_loop ?delay_outside_fragment exec ~more ~pp = let k = ref noalts in let do_with_infos f = let time0 = Unix.gettimeofday() in - let o, alts = mk_outcome f (fun () -> get CS.Ugly.delayed, get CS.state, exec.query_arguments) exec.Elpi_data.assignments in + let o, alts = mk_outcome f (fun () -> get CS.Ugly.delayed, get CS.state, exec.query_arguments) exec.assignments in let time1 = Unix.gettimeofday() in k := alts; pp (time1 -. time0) o in diff --git a/src/elpi_runtime.mli b/src/runtime.mli similarity index 97% rename from src/elpi_runtime.mli rename to src/runtime.mli index fa86c5167..d4ee03351 100644 --- a/src/elpi_runtime.mli +++ b/src/runtime.mli @@ -2,7 +2,7 @@ (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) -open Elpi_data +open Data module Pp : sig val ppterm : @@ -47,7 +47,7 @@ val make_index : (* used by the compiler *) val clausify1 : - loc:Elpi_util.Loc.t -> + loc:Util.Loc.t -> mode Constants.Map.t -> (* for caching it in the clause *) nargs:int -> depth:int -> term -> (constant * clause) * clause_src * int diff --git a/src/elpi_util.ml b/src/util.ml similarity index 100% rename from src/elpi_util.ml rename to src/util.ml diff --git a/src/elpi_util.mli b/src/util.mli similarity index 100% rename from src/elpi_util.mli rename to src/util.mli From 796734aff1f067353a29f912a5878a11314744a3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 20 Jun 2019 13:32:53 +0200 Subject: [PATCH 04/10] update changelog --- Changelog.md | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/Changelog.md b/Changelog.md index 0289e1dc3..26bb1da1b 100644 --- a/Changelog.md +++ b/Changelog.md @@ -1,3 +1,20 @@ +## Version 1.4 (June 2019) + +Elpi 1.4 requires OCaml 4.04 or newer + +- Sources and build: Switch to dune, with a little make base wrapper. + As a result of dune wrapping the library all sources are renamed from + `elpi_x.ml` to `x.ml`, and each module `Elpi_X` is now available as `Elpi.X`. + In particular clients must now use `Elpi.API` and `Elpi.Builtin`. + +- FFI: + - `Conversion.TypeErr` now carries the depth at which the error is found, so + that the term payload can be correctly printed. + - Built in predicates are allowed to raise TypeErr in their body + - `BuiltInPredicate.Full` now returns a list of `extra_goals`, exactly as + `Conversion.embed` does making conversion code easy to call in the body + of a predicate. + ## Version 1.3 (June 2019) Elpi 1.3 requires OCaml 4.04 or newer From 6e4511d4594022f706100822548b9e5f711b3cbc Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 20 Jun 2019 13:33:48 +0200 Subject: [PATCH 05/10] update gitignore --- .gitignore | 23 +---------------------- 1 file changed, 1 insertion(+), 22 deletions(-) diff --git a/.gitignore b/.gitignore index eed2ad092..15729f455 100644 --- a/.gitignore +++ b/.gitignore @@ -1,30 +1,9 @@ -*.o -*.cmx -*.cmo -*.cmi -*.a -*.cmxa -*.cmt -*.cmti -*.cma -*.lp -*.lpo - -findlib - *~ .*.swp -.depends -.depends.parser -.depends.byte -.depends.parser.byte - -./elpi ./elpi.* -trace_ppx +elpi.install .merlin -elpi_REPL_config.ml data.csv data.csv.dat From d68b80f2aeed7fb399abf30861da3331afdece60 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 20 Jun 2019 14:01:41 +0200 Subject: [PATCH 06/10] bump max ocaml version --- .travis.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.travis.yml b/.travis.yml index cb39e161e..b240143c1 100644 --- a/.travis.yml +++ b/.travis.yml @@ -4,7 +4,7 @@ language: c env: global: - OCAML_MIN=4.04.0 - - OCAML_MAX=4.07.1 + - OCAML_MAX=4.08.0 - PREDEPS="ocamlfind" - DEPS="camlp5 ocamlfind ppx_tools_versioned ppx_deriving ocaml-migrate-parsetree re dune cmdliner ANSITerminal" - JOBS=2 From 7acc529ac552076bf535020cfc7182d36c09ed92 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 20 Jun 2019 14:06:12 +0200 Subject: [PATCH 07/10] update build instructions --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 29de900fe..93c527246 100644 --- a/README.md +++ b/README.md @@ -27,7 +27,7 @@ you can type ``` opam pin add elpi https://github.com/LPCIC/elpi.git ``` -You can also clone this repository and type `dune build`. +You can also clone this repository and type `make build`. ### Syntax highlight in Visual studio code From dcad17f05d4e6918b49935c0e50881ce627f518a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 20 Jun 2019 14:08:23 +0200 Subject: [PATCH 08/10] update doc --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 93c527246..fb595d71d 100644 --- a/README.md +++ b/README.md @@ -101,8 +101,8 @@ The easiest way of embedding ELPI is by linking it using [findlib](http://projects.camlcity.org/projects/findlib.html) as in `ocamlfind opt -package elpi mycode.ml -o myprogram`. The API the host application can use to drive ELPI is documented in the -[elpi_API.mli](src/elpi_API.mli) file. The -[elpi_builtin.ml](src/elpi_builtin.ml) file contains example of +[API.mli](src/API.mli) file. The +[Builtin.ml](src/builtin.ml) file contains example of (basic) built-in predicates declaration via ELPI's FFI. The [command line](elpi_REPL.ml) interface to ELPI is a very simple From f8380c86e9c4f1a55b2bba4b04883938ef707ddc Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 20 Jun 2019 14:09:22 +0200 Subject: [PATCH 09/10] .merlin.in not needed anymore --- .merlin.in | 7 ------- 1 file changed, 7 deletions(-) delete mode 100644 .merlin.in diff --git a/.merlin.in b/.merlin.in deleted file mode 100644 index de2efa523..000000000 --- a/.merlin.in +++ /dev/null @@ -1,7 +0,0 @@ -S src/ -B src/ -PKG ppx_deriving.std ppx_deriving.runtime -PKG camlp5 -PKG re -PKG ocaml-migrate-parsetree -PKG ppx_tools_versioned.metaquot_403 From bce943879465cc7df45a8ef671bbf13eb5cc5352 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 20 Jun 2019 14:23:52 +0200 Subject: [PATCH 10/10] use dune to wrap trace_ppx and its runtime --- src/API.ml | 6 +++--- src/builtin.ml | 2 +- src/dune | 4 ++-- trace/dune | 11 +++++------ trace/{elpi_trace.ml => runtime.ml} | 0 trace/{elpi_trace.mli => runtime.mli} | 0 trace/trace.ml | 1 + trace/trace_ppx.ml | 20 ++++++++++---------- 8 files changed, 22 insertions(+), 22 deletions(-) rename trace/{elpi_trace.ml => runtime.ml} (100%) rename trace/{elpi_trace.mli => runtime.mli} (100%) create mode 100644 trace/trace.ml diff --git a/src/API.ml b/src/API.ml index 5e6755d02..f967450b8 100644 --- a/src/API.ml +++ b/src/API.ml @@ -11,8 +11,8 @@ let set_runtime = function | false -> r := (module Runtime_trace_off : Runtime) let set_trace argv = - let args = Elpi_trace.parse_argv argv in - set_runtime !Elpi_trace.debug; + let args = Trace.Runtime.parse_argv argv in + set_runtime !Trace.Runtime.debug; args module Setup = struct @@ -69,7 +69,7 @@ let trace args = let usage = "\nParsing options:\n" ^ "\t-I PATH search for accumulated files in PATH\n" ^ - Elpi_trace.usage + Trace.Runtime.usage let set_warn = Util.set_warn let set_error = Util.set_error diff --git a/src/builtin.ml b/src/builtin.ml index fce2623bb..f44210171 100644 --- a/src/builtin.ml +++ b/src/builtin.ml @@ -654,7 +654,7 @@ let elpi_builtins = let open BuiltIn in let open BuiltInData in [ In (string,"Name", Out(int, "Value", Easy "reads the Value of a trace point Name")), - (fun s _ ~depth:_ -> !:(Elpi_trace.get_cur_step s))), + (fun s _ ~depth:_ -> !:(Trace.Runtime.get_cur_step s))), DocAbove); diff --git a/src/dune b/src/dune index b4a0aecf1..83cc9271f 100644 --- a/src/dune +++ b/src/dune @@ -3,8 +3,8 @@ (public_name elpi) (preprocess (per_module ((pps ppx_deriving.std) API util ast data compiler) - ((pps ppx_deriving.std trace_ppx --trace_ppx-on) runtime_trace_on) - ((pps ppx_deriving.std trace_ppx --trace_ppx-off) runtime_trace_off) + ((pps ppx_deriving.std elpi.trace_ppx --trace_ppx-on) runtime_trace_on) + ((pps ppx_deriving.std elpi.trace_ppx --trace_ppx-off) runtime_trace_off) ((action (system "camlp5o -I . -I +camlp5 pa_extend.cmo pa_lexer.cmo %{input-file}")) parser) )) (libraries re.str camlp5.gramlib unix) diff --git a/trace/dune b/trace/dune index 7bffffe0e..481cd13d7 100644 --- a/trace/dune +++ b/trace/dune @@ -1,18 +1,17 @@ (library (name trace_ppx) - ; (public_name trace_ppx) + (public_name elpi.trace_ppx) (libraries ppx_tools_versioned ocaml-migrate-parsetree) (preprocess (pps ppx_tools_versioned.metaquot_404)) (flags -open Ast_404) (kind ppx_rewriter) - (ppx_runtime_libraries elpi.elpi_trace) + (ppx_runtime_libraries elpi.trace) (modules trace_ppx) ) (library - (name elpi_trace) - (public_name elpi.elpi_trace) - ; (public_name trace_ppx.runtime) + (name trace) + (public_name elpi.trace) (libraries re) - (modules elpi_trace) + (modules trace runtime) ) diff --git a/trace/elpi_trace.ml b/trace/runtime.ml similarity index 100% rename from trace/elpi_trace.ml rename to trace/runtime.ml diff --git a/trace/elpi_trace.mli b/trace/runtime.mli similarity index 100% rename from trace/elpi_trace.mli rename to trace/runtime.mli diff --git a/trace/trace.ml b/trace/trace.ml new file mode 100644 index 000000000..202062009 --- /dev/null +++ b/trace/trace.ml @@ -0,0 +1 @@ +module Runtime = Runtime diff --git a/trace/trace_ppx.ml b/trace/trace_ppx.ml index b6f20a250..27fa3de26 100644 --- a/trace/trace_ppx.ml +++ b/trace/trace_ppx.ml @@ -29,34 +29,34 @@ open Longident let trace name ppfun body = [%expr let wall_clock = Unix.gettimeofday () in - Elpi_trace.enter [%e name] [%e ppfun]; + Trace.Runtime.enter [%e name] [%e ppfun]; try let rc = [%e body] in let elapsed = Unix.gettimeofday () -. wall_clock in - Elpi_trace.exit [%e name] false elapsed; + Trace.Runtime.exit [%e name] false elapsed; rc with - | Elpi_trace.TREC_CALL(f,x) -> + | Trace.Runtime.TREC_CALL(f,x) -> let elapsed = Unix.gettimeofday () -. wall_clock in - Elpi_trace.exit [%e name] true elapsed; + Trace.Runtime.exit [%e name] true elapsed; Obj.obj f (Obj.obj x) | e -> let elapsed = Unix.gettimeofday () -. wall_clock in - Elpi_trace.exit [%e name] false elapsed; + Trace.Runtime.exit [%e name] false elapsed; raise e ] let spy name pp data = - [%expr Elpi_trace.print [%e name] [%e pp] [%e data]] + [%expr Trace.Runtime.print [%e name] [%e pp] [%e data]] let spyif name cond pp data = - [%expr if [%e cond] then Elpi_trace.print [%e name] [%e pp] [%e data]] + [%expr if [%e cond] then Trace.Runtime.print [%e name] [%e pp] [%e data]] let log name key data = - [%expr Elpi_trace.log [%e name] [%e key] [%e data]] + [%expr Trace.Runtime.log [%e name] [%e key] [%e data]] let cur_pred name = - [%expr Elpi_trace.cur_pred [%e name]] + [%expr Trace.Runtime.cur_pred [%e name]] let rec mkapp f = function | [] -> f @@ -69,7 +69,7 @@ let tcall hd args = match List.rev rest with | [] -> assert false | f::a -> [%expr Obj.repr [%e mkapp f a]] in - [%expr raise (Elpi_trace.TREC_CALL ([%e papp], Obj.repr [%e last]))] + [%expr raise (Trace.Runtime.TREC_CALL ([%e papp], Obj.repr [%e last]))] let enabled = ref false