diff options
| -rw-r--r-- | .circleci/config.yml | 6 | ||||
| -rw-r--r-- | .gitlab-ci.yml | 6 | ||||
| -rw-r--r-- | .travis.yml | 3 | ||||
| -rw-r--r-- | Makefile.ci | 1 | ||||
| -rw-r--r-- | dev/ci/ci-basic-overlay.sh | 6 | ||||
| -rwxr-xr-x | dev/ci/ci-elpi.sh | 10 | ||||
| -rw-r--r-- | plugins/funind/glob_termops.ml | 2 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 30 | ||||
| -rw-r--r-- | pretyping/pretyping.mli | 7 | ||||
| -rw-r--r-- | vernac/record.mli | 11 |
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 * |