Merge PR #6767: [ci] add elpi

10 files changed, 67 insertions, 15 deletions

diff --git a/.circleci/config.yml b/.circleci/config.yml
index 9b0cc2119..441d89d42 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -191,7 +191,7 @@ jobs:
     environment:
       <<: *envvars
       EXTRA_PACKAGES: *coqide-packages
-      EXTRA_OPAM: "ocamlgraph"
+      EXTRA_OPAM: "ocamlgraph ppx_tools_versioned ppx_deriving ocaml-migrate-parsetree"
 
   opam-boot-32bit:
     <<: *opam-boot-template
@@ -286,6 +286,9 @@ jobs:
       <<: *ci-template-vars
       EXTRA_PACKAGES: "time python autoconf automake"
 
+  elpi:
+    <<: *ci-template
+
   equations:
     <<: *ci-template
 
@@ -369,6 +372,7 @@ workflows:
       - compcert: *req-main
       - coq-dpdgraph: *req-main
       - coquelicot: *req-main
+      - elpi: *req-main
       - equations: *req-main
       - geocoq: *req-main
       - fiat-crypto: *req-main
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 6b52870ce..5dd376079 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -285,6 +285,12 @@ ci-coquelicot:
     <<: *ci-template-vars
     EXTRA_PACKAGES: "$TIMING_PACKAGES autoconf"
 
+ci-elpi:
+  <<: *ci-template
+  variables:
+    <<: *ci-template-vars
+    EXTRA_OPAM: "ppx_tools_versioned ppx_deriving ocaml-migrate-parsetree"
+
 ci-equations:
   <<: *ci-template
 
diff --git a/.travis.yml b/.travis.yml
index 19e7075f2..f4f01d2f0 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -76,6 +76,9 @@ matrix:
       - TEST_TARGET="ci-coquelicot"
     - if: NOT (type = pull_request)
       env:
+      - TEST_TARGET="ci-elpi" EXTRA_OPAM="ppx_tools_versioned ppx_deriving ocaml-migrate-parsetree"
+    - if: NOT (type = pull_request)
+      env:
       - TEST_TARGET="ci-equations"
     - if: NOT (type = pull_request)
       env:
diff --git a/Makefile.ci b/Makefile.ci
index 80fbd7bbe..4e92264d6 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -5,6 +5,7 @@ CI_TARGETS=ci-bignums \
     ci-coquelicot \
     ci-corn \
     ci-cpdt \
+    ci-elpi \
     ci-equations \
     ci-fiat-crypto \
     ci-fiat-parsers \
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 784da6f97..48e01e9e9 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -144,3 +144,9 @@
 ########################################################################
 : "${Equations_CI_BRANCH:=8.8+alpha}"
 : "${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations.git}"
+
+########################################################################
+# Elpi
+########################################################################
+: "${Elpi_CI_BRANCH:=coq-master}"
+: "${Elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi.git}"
diff --git a/dev/ci/ci-elpi.sh b/dev/ci/ci-elpi.sh
new file mode 100755
index 000000000..c44e0a655
--- /dev/null
+++ b/dev/ci/ci-elpi.sh
@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+Elpi_CI_DIR=${CI_BUILD_DIR}/elpi
+
+git_checkout ${Elpi_CI_BRANCH} ${Elpi_CI_GITURL} ${Elpi_CI_DIR}
+
+( cd ${Elpi_CI_DIR} && make && make install )
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index b4ca1073c..41eb48657 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -562,7 +562,7 @@ let resolve_and_replace_implicits ?(flags=Pretyping.all_and_fail_flags) ?(expect
   (* we first (pseudo) understand [rt] and get back the computed evar_map *)
   (* FIXME : JF (30/03/2017) I'm not completely sure to have split understand as needed. 
 If someone knows how to prevent solved existantial removal in  understand, please do not hesitate to change the computation of [ctx] here *) 
-  let ctx,_ = Pretyping.ise_pretype_gen flags env sigma Glob_ops.empty_lvar expected_type rt in
+  let ctx,_,_ = Pretyping.ise_pretype_gen flags env sigma Glob_ops.empty_lvar expected_type rt in
   let ctx, f = Evarutil.nf_evars_and_universes ctx in
 
   (* then we map [rt] to replace the implicit holes by their values *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 8809558ff..6700748eb 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -378,10 +378,10 @@ let check_evars_are_solved env current_sigma init_sigma =
   let frozen = frozen_and_pending_holes (init_sigma, current_sigma) in
   check_evars_are_solved env current_sigma frozen
 
-let process_inference_flags flags env initial_sigma (sigma,c) =
+let process_inference_flags flags env initial_sigma (sigma,c,cty) =
   let sigma = solve_remaining_evars flags env sigma initial_sigma in
   let c = if flags.expand_evars then nf_evar sigma c else c in
-  sigma,c
+  sigma,c,cty
 
 let adjust_evar_source evdref na c =
   match na, kind !evdref c with
@@ -1173,15 +1173,18 @@ let ise_pretype_gen flags env sigma lvar kind c =
   let env = make_env env sigma in
   let evdref = ref sigma in
   let k0 = Context.Rel.length (rel_context env) in
-  let c' = match kind with
+  let c', c'_ty = match kind with
     | WithoutTypeConstraint ->
-        (pretype k0 flags.use_typeclasses empty_tycon env evdref lvar c).uj_val
+        let j = pretype k0 flags.use_typeclasses empty_tycon env evdref lvar c in
+        j.uj_val, j.uj_type
     | OfType exptyp ->
-	(pretype k0 flags.use_typeclasses (mk_tycon exptyp) env evdref lvar c).uj_val
+        let j = pretype k0 flags.use_typeclasses (mk_tycon exptyp) env evdref lvar c in
+        j.uj_val, j.uj_type
     | IsType ->
-	(pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c).utj_val 
+        let tj = pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c in
+        tj.utj_val, mkSort tj.utj_type
   in
-  process_inference_flags flags env.ExtraEnv.env sigma (!evdref,c')
+  process_inference_flags flags env.ExtraEnv.env sigma (!evdref,c',c'_ty)
 
 let default_inference_flags fail = {
   use_typeclasses = true;
@@ -1201,7 +1204,7 @@ let all_and_fail_flags = default_inference_flags true
 let all_no_fail_flags = default_inference_flags false
 
 let ise_pretype_gen_ctx flags env sigma lvar kind c =
-  let evd, c = ise_pretype_gen flags env sigma lvar kind c in
+  let evd, c, _ = ise_pretype_gen flags env sigma lvar kind c in
   let evd, f = Evarutil.nf_evars_and_universes evd in
     f (EConstr.Unsafe.to_constr c), Evd.evar_universe_context evd
 
@@ -1213,12 +1216,15 @@ let understand
     env sigma c =
   ise_pretype_gen_ctx flags env sigma empty_lvar expected_type c
 
-let understand_tcc ?(flags=all_no_fail_flags) env sigma ?(expected_type=WithoutTypeConstraint) c =
-  let (sigma, c) = ise_pretype_gen flags env sigma empty_lvar expected_type c in
-  (sigma, c)
+let understand_tcc_ty ?(flags=all_no_fail_flags) env sigma ?(expected_type=WithoutTypeConstraint) c =
+  ise_pretype_gen flags env sigma empty_lvar expected_type c
+
+let understand_tcc ?flags env sigma ?expected_type c =
+  let sigma, c, _ = understand_tcc_ty ?flags env sigma ?expected_type c in
+  sigma, c
 
 let understand_ltac flags env sigma lvar kind c =
-  let (sigma, c) = ise_pretype_gen flags env sigma lvar kind c in
+  let (sigma, c, _) = ise_pretype_gen flags env sigma lvar kind c in
   (sigma, c)
 
 let pretype k0 resolve_tc typcon env evdref lvar t =
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index fe10be9e7..864768fe5 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -58,6 +58,11 @@ val all_and_fail_flags : inference_flags
 val understand_tcc : ?flags:inference_flags -> env -> evar_map ->
   ?expected_type:typing_constraint -> glob_constr -> evar_map * constr
 
+(** As [understand_tcc] but also returns the type of the elaborated term.
+    The [expand_evars] flag is not applied to the type (only to the term). *)
+val understand_tcc_ty : ?flags:inference_flags -> env -> evar_map ->
+  ?expected_type:typing_constraint -> glob_constr -> evar_map * constr * types
+
 (** More general entry point with evars from ltac *)
 
 (** Generic call to the interpreter from glob_constr to constr
@@ -116,7 +121,7 @@ val pretype_type :
 
 val ise_pretype_gen :
   inference_flags -> env -> evar_map ->
-  ltac_var_map -> typing_constraint -> glob_constr -> evar_map * constr
+  ltac_var_map -> typing_constraint -> glob_constr -> evar_map * constr * types
 
 (**/**)
 
diff --git a/vernac/record.mli b/vernac/record.mli
index e632e7bbf..e0a4b8fdd 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -13,6 +13,17 @@ open Globnames
 
 val primitive_flag : bool ref
 
+val declare_projections :
+  inductive ->
+  Entries.constant_universes_entry ->
+  ?kind:Decl_kinds.definition_object_kind ->
+  Id.t ->
+  bool list ->
+  Universes.universe_binders ->
+  Impargs.manual_implicits list ->
+  Context.Rel.t ->
+    (Name.t * bool) list * Constant.t option list
+
 val definition_structure :
   inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic *
   Declarations.recursivity_kind * ident_decl with_coercion * local_binder_expr list *