Skip to content
New issue

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

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

Already on GitHub? Sign in to your account

Port to elpi 2.0 #708

Closed
wants to merge 14 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions Changelog.md
Original file line number Diff line number Diff line change
@@ -1,5 +1,11 @@
# Development version

### Vernacular
- `Elpi Accumulate Db Header <db>` to accumulate just the `Db` declaration
but no code added after that
- `Elpi Typecheck` is deprecated and is a no-op since `Elpi Accumulate`
performs type checking incrementally

### Build system
- Support dune workspace build with `elpi`

Expand Down
3 changes: 3 additions & 0 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -2,10 +2,12 @@ dune = dune $(1) $(DUNE_$(1)_FLAGS)

all:
$(call dune,build)
$(call dune,build) builtin-doc
.PHONY: all

build-core:
$(call dune,build) theories
$(call dune,build) builtin-doc
.PHONY: build-core

build-apps:
Expand All @@ -14,6 +16,7 @@ build-apps:

build:
$(call dune,build) -p coq-elpi @install
$(call dune,build) builtin-doc
.PHONY: build

test-core:
Expand Down
42 changes: 34 additions & 8 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -182,14 +182,39 @@ In order to load Coq-Elpi use `From elpi Require Import elpi`.
It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands).
- `Elpi Program <qname> <code>` lower level primitive letting one crate a
command/tactic with a custom preamble `<code>`.
- `From some.load.path Extra Dependency <filename> as <fname>`.
- `Elpi Accumulate [<dbname>|<qname>] [<code>|File <fname>|Db <dbname>]`
- `From some.load.path Extra Dependency <filename> as <fname>` declares `<fname>`
as a piece of code that can be accumulated via `Elpi Accumulate File`.
The content is given in the external file `<filename>` to be found in
the Coq load path `some.load.path`.
- `Elpi File <fname> <code>.` declares `<fname>`
as a piece of code that can be accumulated via `Elpi Accumulate File`.
This time the code is given in the .v file.
It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands).
- `Elpi Accumulate [<dbname>|<qname>] [<code>|File [Signature] <fname>|Db [Header] <dbname>]`
adds code to the current program (or `<dbname>` or `<qname>` if specified).
The code can be verbatim, from a file or a Db.
File names `<fname>` must have been previously declared with the above command.
File names `<fname>` must have been previously declared with
`Extra Dependency` or `Elpi File`.
Accumulating `File Signature <fname>` only adds the signautre declarations
(kinds, types, modes, type abbreviations) from `<fname>` skipping the code
(clauses/rules).
Accumulating `Db Header <dbname>`, instead of `Db <dbname>`, accumulates
only the first chunk of code associated with Db, typically the type
declaration of the predicates that live in the Db. When defining a command
or tactic it can be useful to first accumulate the Db header, then some
code (possibly calling the predicate living in the Db), and finally
accumulating the (full) Db.
Note that when a command is executed it may need to be (partially)
recompiled, e.g. if the Db was updated. In this case all the code accumulated
after the Db (but not after its header) may need to be recompiled. Hence
we recommend to accumulate Dbs last.
It understands the `#[skip="rex"]` and `#[only="rex"]` which make the command
a no op if the Coq version is matched (or not) by the given regular expression.
It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands)
It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands).
It understands the `#[local]`, `#[global]`, and `#[superglobal]` scope attributes,
although only when accumulating to a `<dbname>` (all accumulations to a program
are `#[superglobal]`). Default accumulation to db is the equivalent of `#[export]`.
See the Coq reference manual for the meaning of these scopes.
- `Elpi Typecheck [<qname>]` typechecks the current program (or `<qname>` if
specified).
It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands)
Expand All @@ -204,10 +229,9 @@ In order to load Coq-Elpi use `From elpi Require Import elpi`.
tracing for Elpi's [trace browser]().
- `Elpi Bound Steps <number>` limits the number of steps an Elpi program can
make.
- `Elpi Print <qname> [<string> <filter>*]` prints the program `<qname>` to an
HTML file named `<qname>.html` and a text file called `<qname>.txt`
(or `<string>` if provided) filtering out clauses whose file or clause-name
matches `<filter>`.
- `Elpi Print <qname> [<string> <filter>*]` prints the program `<qname>` to
a text file called `<qname>.txt` (or `<string>` if provided) filtering out
clauses whose file or clause-name matches `<filter>`.
It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands)

where:
Expand All @@ -220,6 +244,8 @@ where:
`lp:{{ coq.say "hello!" }}` becomes `" coq.say ""hello!"" "`).
- `<filename>` is a string containing the path of an external file, e.g.
`"this_file.elpi"`.
- `<fname>` is a qualified Coq name, eg `foo.elpi` (note that `Extra Dependency`
only allows simple identifiers).
- `<start>` and `<stop>` are numbers, e.g. `17 24`.
- `<predicate-filter>` is a regexp against which the predicate name is matched,
e.g. `"derive.*"`.
Expand Down
65 changes: 2 additions & 63 deletions _CoqProject
Original file line number Diff line number Diff line change
Expand Up @@ -57,72 +57,11 @@
-Q _build/default/apps/tc/elpi elpi.apps.tc.elpi
-Q apps/tc/examples elpi.apps.tc.examples
-Q _build/default/apps/tc/examples elpi.apps.tc.examples
-Q apps/tc/tests elpi.apps.tc.tests
-Q _build/default/apps/tc/tests elpi.apps.tc.tests
-Q apps/tc/theories elpi.apps.tc
-Q _build/default/apps/tc/theories elpi.apps.tc

# Cram tests.

-Q tests/link_order5.t elpi.test
-Q tests/checker.t elpi.test
-Q tests/query_extra_dep.t elpi.test
-Q tests/libobject_C.t elpi.test
-Q tests/link_order3.t elpi.test
-Q tests/ltac3.t elpi.test
-Q tests/synterp.t elpi.test
-Q tests/link_order6.t elpi.test
-Q tests/API2.t elpi.test
-Q tests/glob.t elpi.test
-Q tests/require_bad_order.t elpi.test
-Q tests/API_arguments.t elpi.test
-Q tests/link_order9.t elpi.test
-Q tests/API_typecheck.t elpi.test
-Q tests/link_order7.t elpi.test
-Q tests/libobject_A.t elpi.test
-Q tests/libobject_B.t elpi.test
-Q tests/vernacular1.t elpi.test
-Q tests/API_section.t elpi.test
-Q tests/tactic.t elpi.test
-Q tests/link_perf.t elpi.test
-Q tests/API_elaborate.t elpi.test
-Q tests/link_order_import3.t elpi.test
-Q tests/COQ_ELPI_ATTRIBUTES.t elpi.test
-Q tests/elaborator.t elpi.test
-Q tests/HOAS.t elpi.test
-Q tests/API_notations.t elpi.test
-Q tests/arg_HOAS.t elpi.test
-Q tests/link_order_import2.t elpi.test
-Q tests/link_order2.t elpi.test
-Q tests/link_order8.t elpi.test
-Q tests/cache_async.t elpi.test
-Q tests/API_new_pred.t elpi.test
-Q tests/quotation.t elpi.test
-Q tests/ltac2.t elpi.test
-Q tests/perf_calls.t elpi.test
-Q tests/link_order1.t elpi.test
-Q tests/link_order_import0.t elpi.test
-Q tests/ltac.t elpi.test
-Q tests/link_order4.t elpi.test
-Q tests/API_env.t elpi.test
-Q tests/toposort.t elpi.test
-Q tests/link_order_import1.t elpi.test
-Q tests/API_module.t elpi.test
-Q tests/vernacular2.t elpi.test
-Q tests/API.t elpi.test
-Q tests/ctx_cache.t elpi.test
-Q tests/API_TC_CS.t elpi.test
-Q tests/example_abs_evars.t elpi.test
-Q tests/example_curry_howard_tactics.t elpi.test
-Q tests/example_data_base.t elpi.test
-Q tests/example_fuzzer.t elpi.test
-Q tests/example_generalize.t elpi.test
-Q tests/example_import_projections.t elpi.test
-Q tests/example_record_expansion.t elpi.test
-Q tests/example_record_to_sigma.t elpi.test
-Q tests/example_reduction_surgery.t elpi.test
-Q tests/example_reflexive_tactic.t elpi.test
-Q tests/tutorial_coq_elpi_command.t elpi.test
-Q tests/tutorial_coq_elpi_HOAS.t elpi.test
-Q tests/tutorial_coq_elpi_tactic.t elpi.test
-Q tests/tutorial_elpi_lang.t elpi.test
-Q tests elpi.tests
-Q _build/default/tests elpi.tests
2 changes: 1 addition & 1 deletion apps/NES/tests/test_NES_lib.v
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ Elpi Command Make.
nes.end-path,
].
}}.
Elpi Typecheck.

Elpi Export Make.

Make Cats.And.Dogs.
Expand Down
12 changes: 6 additions & 6 deletions apps/NES/theories/NES.v
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ main _ :-
coq.say "NES: registered namespaces" NS.

}}.
Elpi Typecheck.

Elpi Export NES.Status.

Elpi Command NES.Begin.
Expand All @@ -45,7 +45,7 @@ Elpi Command NES.Begin.

}}.
#[interp] Elpi Accumulate lp:{{ main _ :- nes.begin-path. }}.
Elpi Typecheck.

Elpi Export NES.Begin.

Elpi Command NES.End.
Expand All @@ -59,7 +59,7 @@ Elpi Command NES.End.

}}.
#[interp] Elpi Accumulate lp:{{ main _ :- nes.end-path. }}.
Elpi Typecheck.

Elpi Export NES.End.


Expand All @@ -74,7 +74,7 @@ Elpi Command NES.Open.

}}.
#[interp] Elpi Accumulate lp:{{ main _ :- nes.open-path. }}.
Elpi Typecheck.

Elpi Export NES.Open.

(* List the contents a namespace *)
Expand All @@ -93,7 +93,7 @@ Elpi Command NES.List.
main _ :- coq.error "usage: NES.List <DotSeparatedPath>".

}}.
Elpi Typecheck.

Elpi Export NES.List.

(* NES.List with types *)
Expand All @@ -118,5 +118,5 @@ Elpi Accumulate lp:{{
main _ :- coq.error "usage: NES.Print <DotSeparatedPath>".

}}.
Elpi Typecheck.

Elpi Export NES.Print.
1 change: 0 additions & 1 deletion apps/coercion/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,6 @@ coercion _ {{ True }} {{ Prop }} {{ bool }} {{ true }}.
coercion _ {{ False }} {{ Prop }} {{ bool }} {{ false }}.

}}.
Elpi Typecheck coercion. (* checks the elpi program is OK *)

Check True && False.
```
Expand Down
18 changes: 10 additions & 8 deletions apps/coercion/src/coq_elpi_coercion_hook.mlg
Original file line number Diff line number Diff line change
Expand Up @@ -24,23 +24,25 @@ let build_expected_type env sigma expected =
let return s g t = Some (s,g,t)

let elpi_coercion_hook program env sigma ~flags v ~inferred ~expected =
let loc = API.Ast.Loc.initial "(unknown)" in
let atts = [] in
let sigma, expected, retype = build_expected_type env sigma expected in
let sigma, goal = Evarutil.new_evar env sigma expected in
let goal_evar, _ = EConstr.destEvar sigma goal in
let query ~depth state =
let state, (loc, q), gls =
Coq_elpi_HOAS.goals2query sigma [goal_evar] loc ~main:(Coq_elpi_HOAS.Solve [v; inferred])
~in_elpi_tac_arg:Coq_elpi_arg_HOAS.in_elpi_tac_econstr ~depth state in
let query state =
let loc = Elpi.API.State.get Coq_elpi_builtins_synterp.invocation_site_loc state in
let depth = 0 in
let state, q, gls =
Coq_elpi_HOAS.solvegoals2query sigma [goal_evar] loc ~main:[v; inferred]
~in_elpi_tac_arg:Coq_elpi_arg_HOAS.in_elpi_tac_econstr ~depth ~base:() state in
let state, qatts = atts2impl loc Summary.Stage.Interp ~depth state atts q in
let state = API.State.set Coq_elpi_builtins.tactic_mode state true in
state, (loc, qatts), gls
state, qatts, gls
in
match Interp.get_and_compile program with
let loc = Loc.initial Loc.ToplevelInput in
match Interp.get_and_compile ~loc program with
| None -> None
| Some (cprogram, _) ->
match Interp.run ~static_check:false cprogram (`Fun query) with
match Interp.run ~loc cprogram (Fun (query)) with
| API.Execute.Success solution ->
let gls = Evar.Set.singleton goal_evar in
let sigma, _, _ = Coq_elpi_HOAS.solution2evd ~eta_contract_solution:false sigma solution gls in
Expand Down
2 changes: 0 additions & 2 deletions apps/coercion/tests/coercion.t/test.v
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,6 @@ coercion _ {{ True }} {{ Prop }} {{ bool }} {{ true }}.
coercion _ {{ False }} {{ Prop }} {{ bool }} {{ false }}.

}}.
Elpi Typecheck coercion.

Check True && False.

Expand All @@ -22,7 +21,6 @@ coercion _ N {{ nat }} {{ ringType_sort lp:R }} {{ natmul lp:R lp:N }} :-
coq.typecheck R {{ ringType }} ok.

}}.
Elpi Typecheck coercion.

Section TestNatMul.

Expand Down
3 changes: 1 addition & 2 deletions apps/coercion/tests/coercion_open.t/test.v
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ From Coq Require Import Arith ssreflect.

Ltac my_solver := trivial with arith.

Elpi Accumulate coercion.db lp:{{
Elpi Accumulate coercion lp:{{

coercion _ X Ty {{ @sig lp:Ty lp:P }} Solution :- std.do! [
% we unfold letins since the solve is dumb
Expand All @@ -17,7 +17,6 @@ coercion _ X Ty {{ @sig lp:Ty lp:P }} Solution :- std.do! [
].

}}.
Elpi Typecheck coercion.

Goal {x : nat | x > 0}.
apply: 3.
Expand Down
3 changes: 2 additions & 1 deletion apps/coercion/theories/coercion.v
Original file line number Diff line number Diff line change
Expand Up @@ -15,11 +15,12 @@ pred coercion i:goal-ctx, i:term, i:term, i:term, o:term.
}}.

Elpi Tactic coercion.
Elpi Accumulate Db Header coercion.db.
Elpi Accumulate lp:{{

solve (goal Ctx _ Ty Sol [trm V, trm VTy]) _ :- coercion Ctx V VTy Ty Sol.

}}.
Elpi Accumulate Db coercion.db.
Elpi Typecheck.

Elpi CoercionFallbackTactic coercion.
1 change: 0 additions & 1 deletion apps/cs/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,6 @@ cs _ {{ sort lp:Sol }} {{ nat }} :-
Sol = {{ Build_S nat }}.

}}.
Elpi Typecheck canonical_solution.

Check eq_refl _ : (sort _) = nat.
```
20 changes: 11 additions & 9 deletions apps/cs/src/coq_elpi_cs_hook.mlg
Original file line number Diff line number Diff line change
Expand Up @@ -8,27 +8,29 @@ open Coq_elpi_arg_syntax
open Coq_elpi_vernacular

let elpi_cs_hook program env sigma ((proji, u), params1, c1) (t2, args2) =
let loc = API.Ast.Loc.initial "(unknown)" in
let atts = [] in
let rhs = Reductionops.Stack.zip sigma (t2, Reductionops.Stack.append_app_list args2 Reductionops.Stack.empty) in
let sigma, (goal_ty, _) = Evarutil.new_type_evar env sigma Evd.UnivRigid in
let sigma, goal = Evarutil.new_evar env sigma goal_ty in
let goal_evar, _ = EConstr.destEvar sigma goal in
let nparams = Structures.Structure.projection_nparams proji in
let query ~depth state =
let state, (loc, q), gls =
let query state =
let loc = Elpi.API.State.get Coq_elpi_builtins_synterp.invocation_site_loc state in
let state, q, gls =
let lhs = match params1 with
| Some params1 -> EConstr.mkApp (EConstr.mkConstU (proji, u), Array.of_list params1)
| None -> EConstr.mkConstU (proji, u) in
Coq_elpi_HOAS.goals2query sigma [goal_evar] loc ~main:(Coq_elpi_HOAS.Solve [lhs; rhs])
~in_elpi_tac_arg:Coq_elpi_arg_HOAS.in_elpi_tac_econstr ~depth state in
let state, qatts = atts2impl loc Summary.Stage.Interp ~depth state atts q in
Coq_elpi_HOAS.solvegoals2query sigma [goal_evar] loc ~main:[lhs; rhs]
~in_elpi_tac_arg:Coq_elpi_arg_HOAS.in_elpi_tac_econstr ~depth:0 ~base:() state in
let state, qatts = atts2impl loc Summary.Stage.Interp ~depth:0 state atts q in
let state = API.State.set Coq_elpi_builtins.tactic_mode state true in
state, (loc, qatts), gls
in match Interp.get_and_compile program with
state, qatts, gls
in
let loc = Loc.initial Loc.ToplevelInput in
match Interp.get_and_compile ~loc program with
| None -> None
| Some (cprogram, _) ->
begin match Interp.run ~static_check:false cprogram (`Fun query) with
begin match Interp.run ~loc cprogram (Fun query) with
| API.Execute.Success solution ->
let gls = Evar.Set.singleton goal_evar in
let sigma, _, _ = Coq_elpi_HOAS.solution2evd ~eta_contract_solution:false sigma solution gls in
Expand Down
1 change: 0 additions & 1 deletion apps/cs/tests/cs.t.disabled_broken_8.19/test.v
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,6 @@ Elpi Accumulate canonical_solution lp:{{
cs _ {{ sort lp:T }} {{ @id lp:T }} {{ Build_S lp:T (@id lp:T) }}.

}}.
Elpi Typecheck canonical_solution.

Check 1.
Check eq_refl _ : (sort nat _) = @id nat.
Expand Down
1 change: 0 additions & 1 deletion apps/cs/theories/cs.v
Original file line number Diff line number Diff line change
Expand Up @@ -24,5 +24,4 @@ solve (goal Ctx _ _Ty Sol [trm Proj, trm Rhs]) _ :-
true.

}}.
Elpi Typecheck canonical_solution.
Elpi CS canonical_solution.
Loading
Loading