Merge pull request #491 from LPCIC/new-master-rc1

New master rc1

.github/workflows/main.yml

@@ -16,7 +16,7 @@ jobs:
     strategy:
       matrix:
         coq_version:
-          - '8.17'
+          - '8.18'
         ocaml_version:
           - '4.09-flambda'
           - '4.13-flambda'

.gitignore

@@ -43,4 +43,7 @@ tests/test_glob/*.css
 
 META
 
-*.cache
+*.cache
+
+apps/coercion/src/coq_elpi_coercion_hook.ml
+.filestoinstall

Changelog.md

@@ -1,5 +1,18 @@
 # Changelog
 
+## [1.19.0] - 04/08/2023
+
+Requires Elpi 1.16.5 and Coq 8.18.
+
+### APPS
+- New `coercion` app providing `coercion` predicate
+  to program coercions (thanks @proux01).
+  This app is experimental.
+
+### API:
+- Removed option `@nonuniform!` as it disappears from Coq 8.18.
+  (c.f. https://github.com/coq/coq/pull/17716 )
+
 ## [1.18.0] - 27/07/2023
 
 Requires Elpi 1.16.5 and Coq 8.17.

Makefile

@@ -21,7 +21,7 @@ export ELPIDIR
 
 DEPS=$(ELPIDIR)/elpi.cmxa $(ELPIDIR)/elpi.cma
 
-APPS=$(addprefix apps/, derive eltac NES locker)
+APPS=$(addprefix apps/, derive eltac NES locker coercion)
 
 ifeq "$(COQ_ELPI_ALREADY_INSTALLED)" ""
 DOCDEP=build

Makefile.coq.local

@@ -1,6 +1,7 @@
 CAMLPKGS+= -package elpi,stdlib-shims
 CAMLFLAGS+= -bin-annot -g
 OCAMLWARN+=-warn-error -32
+COQEXTRAFLAGS=-bt
 
 theories/elpi.vo: $(wildcard elpi/*.elpi)
 

README.md

@@ -152,7 +152,9 @@ all the dependencies installed first (see [coq-elpi.opam](coq-elpi.opam)).
 - [Dx](https://gitlab.univ-lille.fr/samuel.hym/dx) uses elpi to generate
   an intermediate representation of Coq terms, to be later tranformed into
   C.
-
+- [Coercion](apps/coercion) enable to program coercions in Elpi.
+  It comes bundled with Coq-Elpi.
+
 ### Quick Reference
 
 In order to load Coq-Elpi use `From elpi Require Import elpi`.

_CoqProject

@@ -17,6 +17,7 @@
 -R apps/eltac/theories elpi.apps.eltac
 -R apps/eltac/tests    elpi.apps.eltac.tests
 -R apps/eltac/examples elpi.apps.eltac.examples
+-R apps/coercion/theories elpi.apps.coercion
 
 theories/elpi.v
 theories/wip/memoization.v

apps/coercion/Makefile

@@ -0,0 +1,40 @@
+# detection of coq
+ifeq "$(COQBIN)" ""
+COQBIN := $(shell which coqc >/dev/null 2>&1 && dirname `which coqc`)
+endif
+ifeq "$(COQBIN)" ""
+$(error Coq not found, make sure it is installed in your PATH or set COQBIN)
+else
+$(info Using coq found in $(COQBIN), from COQBIN or PATH)
+endif
+export COQBIN := $(COQBIN)/
+
+all: build test
+
+build: Makefile.coq
+	@$(MAKE) --no-print-directory -f Makefile.coq
+
+test: Makefile.test.coq
+	@$(MAKE) --no-print-directory -f Makefile.test.coq
+
+theories/%.vo: force
+	@$(MAKE) --no-print-directory -f Makefile.coq $@
+tests/%.vo: force build Makefile.test.coq
+	@$(MAKE) --no-print-directory -f Makefile.test.coq $@
+examples/%.vo: force build Makefile.test.coq
+	@$(MAKE) --no-print-directory -f Makefile.test.coq $@
+
+Makefile.coq Makefile.coq.conf: _CoqProject
+	@$(COQBIN)/coq_makefile -f _CoqProject -o Makefile.coq
+	@$(MAKE) --no-print-directory -f Makefile.coq .merlin
+Makefile.test.coq Makefile.test.coq.conf: _CoqProject.test
+	@$(COQBIN)/coq_makefile -f _CoqProject.test -o Makefile.test.coq
+
+clean: Makefile.coq Makefile.test.coq
+	@$(MAKE) -f Makefile.coq $@
+	@$(MAKE) -f Makefile.test.coq $@
+
+.PHONY: force all build test
+
+install:
+	@$(MAKE) -f Makefile.coq $@

apps/coercion/Makefile.coq.local

@@ -0,0 +1,3 @@
+CAMLPKGS+= -package coq-elpi.elpi
+OCAMLPATH:=../../src/:$(OCAMLPATH)
+export OCAMLPATH

apps/coercion/README.md

@@ -0,0 +1,80 @@
+# Coercion
+
+The `coercion` app enables to program Coq coercions in Elpi.
+
+This app is experimental.
+
+## The coercion predicate
+
+The `coercion` predicate lives in the database `coercion.db`
+
+```elpi
+% [coercion Ctx V Inferred Expected Res] is queried to cast V to Res
+% - [Ctx] is the context
+% - [V] is the value to be coerced
+% - [Inferred] is the type of [V]
+% - [Expected] is the type [V] should be coerced to
+% - [Res] is the result (of type [Expected])
+pred coercion i:goal-ctx, i:term, i:term, i:term, o:term.
+```
+
+By addings rules for this predicate one can recover from a type error, that is
+when `Inferred` and `Expected` are not unifiable.
+
+## Simple example of coercion
+
+This example maps `True : Prop` to `true : bool`, which is a function you
+cannot express in type theory, hence in the standard Coercion system.
+
+```coq
+From elpi.apps Require Import coercion.
+From Coq Require Import Bool.
+
+Elpi Accumulate coercion.db lp:{{
+
+coercion _ {{ True }} {{ Prop }} {{ bool }} {{ true }}.
+coercion _ {{ False }} {{ Prop }} {{ bool }} {{ false }}.
+
+}}.
+Elpi Typecheck coercion. (* checks the elpi program is OK *)
+
+Check True && False.
+```
+
+## Example of coercion with proof automation
+
+This coercion enriches `x : T` to a `{x : T | P x}` by using
+`my_solver` to prove `P x`.
+
+```coq
+From elpi.apps Require Import coercion.
+From Coq Require Import Arith ssreflect.
+
+Ltac my_solver := trivial with arith.
+
+Elpi Accumulate coercion.db lp:{{
+
+coercion _ X Ty {{ @sig lp:Ty lp:P }} Solution :- std.do! [
+  % we unfold letins since the solver is dumb and the `as` in the second
+  % example introduces a letin
+  (pi a b b1\ copy a b :- def a _ _ b, copy b b1) => copy X X1,
+  % we build the solution
+  Solution = {{ @exist lp:Ty lp:P lp:X1 _ }},
+  % we call the solver
+  coq.ltac.collect-goals Solution [G] [],
+  coq.ltac.open (coq.ltac.call-ltac1 "my_solver") G [],
+].
+
+}}.
+Elpi Typecheck coercion.
+
+Goal {x : nat | x > 0}.
+apply: 3.
+Qed.
+
+Definition ensure_pos n : {x : nat | x > 0} :=
+  match n with
+  | O => 1
+  | S x as y => y
+  end.
+```

apps/coercion/_CoqProject

@@ -0,0 +1,14 @@
+# Hack to see Coq-Elpi even if it is not installed yet
+-Q ../../theories elpi
+-I ../../src
+-docroot elpi.apps
+
+-R theories   elpi.apps
+
+src/coq_elpi_coercion_hook.mlg
+src/elpi_coercion_plugin.mlpack
+
+-I src/
+src/META.coq-elpi-coercion
+
+theories/coercion.v

apps/coercion/_CoqProject.test

@@ -0,0 +1,13 @@
+# Hack to see Coq-Elpi even if it is not installed yet
+-Q ../../theories elpi
+-I ../../src
+-docroot elpi.apps
+
+-R theories elpi.apps
+-R tests    elpi.apps.coercion.tests
+
+tests/test_coercion.v
+tests/test_coercion_open.v
+tests/test_coercion_load.v
+
+-I src

apps/coercion/src/META.coq-elpi-coercion

@@ -0,0 +1,10 @@
+
+package "plugin" (
+  directory = "."
+  requires = "coq-core.plugins.ltac coq-elpi.elpi"
+  archive(byte) = "elpi_coercion_plugin.cma"
+  archive(native) = "elpi_coercion_plugin.cmxa"
+  plugin(byte) = "elpi_coercion_plugin.cma"
+  plugin(native) = "elpi_coercion_plugin.cmxs"
+)
+directory = "."

apps/coercion/src/coq_elpi_coercion_hook.mlg

@@ -0,0 +1,58 @@
+DECLARE PLUGIN "coq-elpi-coercion.plugin"
+
+{
+
+open Elpi
+open Elpi_plugin
+open Coq_elpi_arg_syntax
+open Coq_elpi_vernacular
+
+
+let elpi_coercion_hook program env sigma ~flags v ~inferred ~expected =
+  let loc = API.Ast.Loc.initial "(unknown)" in
+  let atts = [] 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 state, qatts = atts2impl loc ~depth state atts q in
+    let state = API.State.set Coq_elpi_builtins.tactic_mode state true in
+    state, (loc, qatts), gls
+  in
+  let cprogram, _ = get_and_compile program in
+  match run ~static_check:false cprogram (`Fun query) with
+  | API.Execute.Success solution ->
+     let gls = Evar.Set.singleton goal_evar in
+     let sigma, _, _ = Coq_elpi_HOAS.solution2evd sigma solution gls in
+     if Evd.is_defined sigma goal_evar then Some (sigma, goal) else None
+  | API.Execute.NoMoreSteps
+  | API.Execute.Failure -> None
+  | exception (Coq_elpi_utils.LtacFail (level, msg)) -> None
+
+let add_coercion_hook =
+  let coercion_hook_program = Summary.ref ~name:"elpi-coercion" None in
+  let coercion_hook env sigma ~flags v ~inferred ~expected =
+    match !coercion_hook_program with
+    | None -> None
+    | Some h -> elpi_coercion_hook h env sigma ~flags v ~inferred ~expected in
+  let name = "elpi-coercion" in
+  Coercion.register_hook ~name coercion_hook;
+  let inCoercion =
+    let cache program =
+      coercion_hook_program := Some program;
+      Coercion.activate_hook ~name in
+    let open Libobject in
+    declare_object
+    @@ superglobal_object_nodischarge "ELPI-COERCION" ~cache ~subst:None in
+  fun program -> Lib.add_leaf (inCoercion program)
+
+}
+
+VERNAC COMMAND EXTEND ElpiCoercion CLASSIFIED AS SIDEFF
+| #[ atts = any_attribute ] [ "Elpi" "CoercionFallbackTactic" qualified_name(p) ] -> {
+     let () = ignore_unknown_attributes atts in
+     add_coercion_hook (snd p) }
+
+END

apps/coercion/src/elpi_coercion_plugin.mlpack

@@ -0,0 +1 @@
+Coq_elpi_coercion_hook

apps/coercion/tests/test_coercion.v

@@ -0,0 +1,34 @@
+From elpi.apps Require Import coercion.
+From Coq Require Import Bool.
+
+Elpi Accumulate coercion.db lp:{{
+
+coercion _ {{ True }} {{ Prop }} {{ bool }} {{ true }}.
+coercion _ {{ False }} {{ Prop }} {{ bool }} {{ false }}.
+
+}}.
+Elpi Typecheck coercion.
+
+Check True && False.
+
+Parameter ringType : Type.
+Parameter ringType_sort : ringType -> Type.
+Parameter natmul : forall (R : ringType) (n : nat), (ringType_sort R).
+
+Elpi Accumulate coercion.db lp:{{
+
+coercion _ N {{ nat }} {{ ringType_sort lp:R }} {{ natmul lp:R lp:N }} :-
+  coq.typecheck R {{ ringType }} ok.
+
+}}.
+Elpi Typecheck coercion.
+
+Section TestNatMul.
+
+Variable R : ringType.
+Variable n : nat.
+
+Check natmul R n : ringType_sort R.
+Check n : ringType_sort R.
+
+End TestNatMul.

apps/coercion/tests/test_coercion_load.v

@@ -0,0 +1,3 @@
+Require Import test_coercion.
+
+Check True : bool.

apps/coercion/tests/test_coercion_open.v

@@ -0,0 +1,29 @@
+From elpi.apps Require Import coercion.
+From Coq Require Import Arith ssreflect.
+
+Ltac my_solver := trivial with arith.
+
+Elpi Accumulate coercion.db lp:{{
+
+coercion _ X Ty {{ @sig lp:Ty lp:P }} Solution :- std.do! [
+  % we unfold letins since the solve is dumb
+  (pi a b b1\ copy a b :- def a _ _ b, copy b b1) => copy X X1,
+  % we build the solution
+  Solution = {{ @exist lp:Ty lp:P lp:X1 _ }},
+  % we call the solver
+  coq.ltac.collect-goals Solution [G] [],
+  coq.ltac.open (coq.ltac.call-ltac1 "my_solver") G [],
+].
+
+}}.
+Elpi Typecheck coercion.
+
+Goal {x : nat | x > 0}.
+apply: 3.
+Qed.
+
+Definition add1 n : {x : nat | x > 0} :=
+  match n with
+  | O => 1
+  | S x as y => y
+  end.

apps/coercion/theories/coercion.v

@@ -0,0 +1,25 @@
+Declare ML Module "coq-elpi-coercion.plugin".
+From elpi Require Import elpi.
+
+Elpi Db coercion.db lp:{{
+
+% predicate [coercion Ctx V Inferred Expected Res] used to add new coercion, with
+% - [Ctx] is the context
+% - [V] is the value to be coerced
+% - [Inferred] is the type of [V]
+% - [Expected] is the type [V] should be coerced to
+% - [Res] is the result (of type [Expected])
+% Be careful not to trigger coercion as this may loop.
+pred coercion i:goal-ctx, i:term, i:term, i:term, o:term.
+
+}}.
+
+Elpi Tactic coercion.
+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.