diff options
102 files changed, 937 insertions, 850 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 06a733be45..2a325f2d71 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -173,6 +173,8 @@ azure-pipelines.yml @coq/ci-maintainers /plugins/rtauto/ @PierreCorbineau # Secondary maintainer @herbelin +/user-contrib/Ltac2 @ppedrot + ########## Pretyper ########## /pretyping/ @mattam82 diff --git a/Makefile.build b/Makefile.build index 147668187f..c76c14f2de 100644 --- a/Makefile.build +++ b/Makefile.build @@ -365,7 +365,7 @@ $(COQPP): $(COQPPCMO) coqpp/coqpp_main.ml ########################################################################### # Specific rules for Uint63 ########################################################################### -kernel/uint63.ml: kernel/write_uint63.ml kernel/uint63_x86.ml kernel/uint63_amd64.ml +kernel/uint63.ml: kernel/write_uint63.ml kernel/uint63_i386_31.ml kernel/uint63_amd64_63.ml $(SHOW)'WRITE $@' $(HIDE)(cd kernel && ocaml unix.cma $(shell basename $<)) diff --git a/checker/check.ml b/checker/check.ml index c5bc59e72a..903258daef 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -51,7 +51,7 @@ let pr_path sp = type compilation_unit_name = DirPath.t type seg_univ = Univ.ContextSet.t * bool -type seg_proofs = Constr.constr option array +type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.constr option) array type library_t = { library_name : compilation_unit_name; @@ -98,9 +98,19 @@ let access_opaque_table dp i = with Not_found -> assert false in assert (i < Array.length t); - t.(i) + let (info, n, c) = t.(i) in + match c with + | None -> None + | Some c -> Some (Cooking.cook_constr info n c) -let () = Mod_checking.set_indirect_accessor access_opaque_table +let access_discharge = Cooking.cook_constr + +let indirect_accessor = { + Opaqueproof.access_proof = access_opaque_table; + Opaqueproof.access_discharge = access_discharge; +} + +let () = Mod_checking.set_indirect_accessor indirect_accessor let check_one_lib admit senv (dir,m) = let md = m.library_compiled in @@ -327,7 +337,6 @@ let intern_from_file ~intern_mode (dir, f) = let (sd:summary_disk), _, digest = marshal_in_segment f ch in let (md:library_disk), _, digest = marshal_in_segment f ch in let (opaque_csts:seg_univ option), _, udg = marshal_in_segment f ch in - let (discharging:'a option), _, _ = marshal_in_segment f ch in let (tasks:'a option), _, _ = marshal_in_segment f ch in let (table:seg_proofs option), pos, checksum = marshal_or_skip ~intern_mode f ch in @@ -340,7 +349,7 @@ let intern_from_file ~intern_mode (dir, f) = if dir <> sd.md_name then user_err ~hdr:"intern_from_file" (name_clash_message dir sd.md_name f); - if tasks <> None || discharging <> None then + if tasks <> None then user_err ~hdr:"intern_from_file" (str "The file "++str f++str " contains unfinished tasks"); if opaque_csts <> None then begin diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index ccce0bd9a7..0684623a81 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -8,13 +8,13 @@ open Environ (** {6 Checking constants } *) -let get_proof = ref (fun _ _ -> assert false) -let set_indirect_accessor f = get_proof := f - -let indirect_accessor = { - Opaqueproof.access_proof = (fun dp n -> !get_proof dp n); +let indirect_accessor = ref { + Opaqueproof.access_proof = (fun _ _ -> assert false); + Opaqueproof.access_discharge = (fun _ _ _ -> assert false); } +let set_indirect_accessor f = indirect_accessor := f + let check_constant_declaration env kn cb = Flags.if_verbose Feedback.msg_notice (str " checking cst:" ++ Constant.print kn); (* Locally set the oracle for further typechecking *) @@ -40,7 +40,7 @@ let check_constant_declaration env kn cb = let body = match cb.const_body with | Undef _ | Primitive _ -> None | Def c -> Some (Mod_subst.force_constr c) - | OpaqueDef o -> Some (Opaqueproof.force_proof indirect_accessor otab o) + | OpaqueDef o -> Some (Opaqueproof.force_proof !indirect_accessor otab o) in let () = match body with diff --git a/checker/mod_checking.mli b/checker/mod_checking.mli index dbc81c8507..7aa1f837a0 100644 --- a/checker/mod_checking.mli +++ b/checker/mod_checking.mli @@ -8,6 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -val set_indirect_accessor : (Names.DirPath.t -> int -> Constr.t option) -> unit +val set_indirect_accessor : Opaqueproof.indirect_accessor -> unit val check_module : Environ.env -> Names.ModPath.t -> Declarations.module_body -> unit diff --git a/checker/values.ml b/checker/values.ml index 031f05dd6b..4a4c8d803c 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -131,7 +131,7 @@ let v_proj = v_tuple "projection" [|v_proj_repr; v_bool|] let rec v_constr = Sum ("constr",0,[| [|Int|]; (* Rel *) - [|Fail "Var"|]; (* Var *) + [|v_id|]; (* Var *) [|Fail "Meta"|]; (* Meta *) [|Fail "Evar"|]; (* Evar *) [|v_sort|]; (* Sort *) @@ -383,6 +383,22 @@ let v_libsum = let v_lib = Tuple ("library",[|v_compiled_lib;v_libraryobjs|]) -let v_opaques = Array (Opt v_constr) +let v_ndecl = v_sum "named_declaration" 0 + [| [|v_binder_annot v_id; v_constr|]; (* LocalAssum *) + [|v_binder_annot v_id; v_constr; v_constr|] |] (* LocalDef *) + +let v_nctxt = List v_ndecl + +let v_work_list = + let v_abstr = v_pair v_instance (Array v_id) in + Tuple ("work_list", [|v_hmap v_cst v_abstr; v_hmap v_cst v_abstr|]) + +let v_abstract = + Tuple ("abstract", [| v_nctxt; v_instance; v_abs_context |]) + +let v_cooking_info = + Tuple ("cooking_info", [|v_work_list; v_abstract|]) + +let v_opaques = Array (Tuple ("opaque", [| List v_cooking_info; Int; Opt v_constr |])) let v_univopaques = Opt (Tuple ("univopaques",[|v_context_set;v_bool|])) diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 95fceb773a..fa39b41565 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -215,7 +215,7 @@ ######################################################################## # simple-io ######################################################################## -: "${simple_io_CI_REF:=dev}" +: "${simple_io_CI_REF:=master}" : "${simple_io_CI_GITURL:=https://github.com/Lysxia/coq-simple-io}" : "${simple_io_CI_ARCHIVEURL:=${simple_io_CI_GITURL}/archive}" diff --git a/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh b/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh deleted file mode 100644 index 2b4c1489ad..0000000000 --- a/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh +++ /dev/null @@ -1,13 +0,0 @@ -_OVERLAY_BRANCH=ho-matching-occ-sel - -if [ "$CI_PULL_REQUEST" = "7819" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then - - unicoq_CI_REF="PR7819-overlay" - - mtac2_CI_REF="PR7819-overlay" - mtac2_CI_GITURL=https://github.com/mattam82/Mtac2 - - equations_CI_GITURL=https://github.com/mattam82/Coq-Equations - equations_CI_REF="PR7819-overlay" - -fi diff --git a/dev/ci/user-overlays/08764-validsdp-master-parsing-decimal.sh b/dev/ci/user-overlays/08764-validsdp-master-parsing-decimal.sh deleted file mode 100644 index 67f6f8610a..0000000000 --- a/dev/ci/user-overlays/08764-validsdp-master-parsing-decimal.sh +++ /dev/null @@ -1,18 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8764" ] || [ "$CI_BRANCH" = "master-parsing-decimal" ]; then - - ltac2_CI_REF=master-parsing-decimal - ltac2_CI_GITURL=https://github.com/proux01/ltac2 - - quickchick_CI_REF=master-parsing-decimal - quickchick_CI_GITURL=https://github.com/proux01/QuickChick - - Corn_CI_REF=master-parsing-decimal - Corn_CI_GITURL=https://github.com/proux01/corn - - HoTT_CI_REF=master-parsing-decimal - HoTT_CI_GITURL=https://github.com/proux01/HoTT - - stdlib2_CI_REF=master-parsing-decimal - stdlib2_CI_GITURL=https://github.com/proux01/stdlib2 - -fi diff --git a/dev/ci/user-overlays/08817-sprop.sh b/dev/ci/user-overlays/08817-sprop.sh deleted file mode 100644 index 81e18226ed..0000000000 --- a/dev/ci/user-overlays/08817-sprop.sh +++ /dev/null @@ -1,34 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8817" ] || [ "$CI_BRANCH" = "sprop" ]; then - aac_tactics_CI_REF=sprop - aac_tactics_CI_GITURL=https://github.com/SkySkimmer/aac-tactics - - coq_dpdgraph_CI_REF=sprop - coq_dpdgraph_CI_GITURL=https://github.com/SkySkimmer/coq-dpdgraph - - coqhammer_CI_REF=sprop - coqhammer_CI_GITURL=https://github.com/SkySkimmer/coqhammer - - elpi_CI_REF=sprop - elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi - - equations_CI_REF=sprop - equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations - - ltac2_CI_REF=sprop - ltac2_CI_GITURL=https://github.com/SkySkimmer/ltac2 - - unicoq_CI_REF=sprop - unicoq_CI_GITURL=https://github.com/SkySkimmer/unicoq - - mtac2_CI_REF=sprop - mtac2_CI_GITURL=https://github.com/SkySkimmer/mtac2 - - paramcoq_CI_REF=sprop - paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq - - quickchick_CI_REF=sprop - quickchick_CI_GITURL=https://github.com/SkySkimmer/QuickChick - - relation_algebra_CI_REF=sprop - relation_algebra_CI_GITURL=https://github.com/SkySkimmer/relation-algebra -fi diff --git a/dev/ci/user-overlays/08829-proj-syntax-check.sh b/dev/ci/user-overlays/08829-proj-syntax-check.sh deleted file mode 100644 index c04621114f..0000000000 --- a/dev/ci/user-overlays/08829-proj-syntax-check.sh +++ /dev/null @@ -1,5 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8829" ] || [ "$CI_BRANCH" = "proj-syntax-check" ]; then - lambdaRust_CI_REF=proj-syntax-check - lambdaRust_CI_GITURL=https://github.com/SkySkimmer/lambda-rust - lambdaRust_CI_ARCHIVEURL=$lambdaRust_CI_GITURL/archive -fi diff --git a/dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh b/dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh deleted file mode 100644 index dc39ea5ef0..0000000000 --- a/dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh +++ /dev/null @@ -1,7 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8893" ] || [ "$CI_BRANCH" = "master+moving-evars-of-term-on-econstr" ]; then - - equations_CI_BRANCH=master+fix-evars_of_term-pr8893 - equations_CI_REF=master+fix-evars_of_term-pr8893 - equations_CI_GITURL=https://github.com/herbelin/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh b/dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh deleted file mode 100644 index 12be1b676a..0000000000 --- a/dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh +++ /dev/null @@ -1,12 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8984" ] || [ "$CI_BRANCH" = "rm-hardwired-hint-db" ]; then - - HoTT_CI_REF=rm-hardwired-hint-db - HoTT_CI_GITURL=https://github.com/vbgl/HoTT - - ltac2_CI_REF=rm-hardwired-hint-db - ltac2_CI_GITURL=https://github.com/vbgl/ltac2 - - UniMath_CI_REF=rm-hardwired-hint-db - UniMath_CI_GITURL=https://github.com/vbgl/UniMath - -fi diff --git a/dev/ci/user-overlays/08988-herbelin-master+mini-uniformizaton-parsing-printing-univ-level-sort.sh b/dev/ci/user-overlays/08988-herbelin-master+mini-uniformizaton-parsing-printing-univ-level-sort.sh deleted file mode 100644 index ae72405e6e..0000000000 --- a/dev/ci/user-overlays/08988-herbelin-master+mini-uniformizaton-parsing-printing-univ-level-sort.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8988" ] || [ "$CI_BRANCH" = "master+mini-uniformizaton-parsing-printing-univ-level-sort" ]; then - - elpi_CI_REF=coq-master+adapt-coq8988-type-internal-syntax - elpi_CI_GITURL=https://github.com/herbelin/coq-elpi - -fi diff --git a/dev/ci/user-overlays/09129-ejgallego-proof+no_global_partial.sh b/dev/ci/user-overlays/09129-ejgallego-proof+no_global_partial.sh deleted file mode 100644 index c09d1b8929..0000000000 --- a/dev/ci/user-overlays/09129-ejgallego-proof+no_global_partial.sh +++ /dev/null @@ -1,30 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9129" ] || [ "$CI_BRANCH" = "proof+no_global_partial" ]; then - - aac_tactics_CI_REF=proof+no_global_partial - aac_tactics_CI_GITURL=https://github.com/ejgallego/aac-tactics - - # coqhammer_CI_REF=proof+no_global_partial - # coqhammer_CI_GITURL=https://github.com/ejgallego/coqhammer - - elpi_CI_REF=proof+no_global_partial - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - - equations_CI_REF=proof+no_global_partial - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - ltac2_CI_REF=proof+no_global_partial - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 - - # unicoq_CI_REF=proof+no_global_partial - # unicoq_CI_GITURL=https://github.com/ejgallego/unicoq - - mtac2_CI_REF=proof+no_global_partial - mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - - paramcoq_CI_REF=proof+no_global_partial - paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq - - quickchick_CI_REF=proof+no_global_partial - quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick - -fi diff --git a/dev/ci/user-overlays/09165-ejgallego-recarg-cleanup.sh b/dev/ci/user-overlays/09165-ejgallego-recarg-cleanup.sh deleted file mode 100644 index 1e1d36d54a..0000000000 --- a/dev/ci/user-overlays/09165-ejgallego-recarg-cleanup.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9165" ] || [ "$CI_BRANCH" = "recarg-cleanup" ]; then - - elpi_CI_REF=recarg-cleanup - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - - quickchick_CI_REF=recarg-cleanup - quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick - -fi diff --git a/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh b/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh deleted file mode 100644 index 23eb24c304..0000000000 --- a/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9173" ] || [ "$CI_BRANCH" = "proofview+proof_info" ]; then - - ltac2_CI_REF=proofview+proof_info - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 - - fiat_parsers_CI_REF=proofview+proof_info - fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat - -fi diff --git a/dev/ci/user-overlays/09389-SkySkimmer-set-implicits.sh b/dev/ci/user-overlays/09389-SkySkimmer-set-implicits.sh deleted file mode 100644 index 1110157069..0000000000 --- a/dev/ci/user-overlays/09389-SkySkimmer-set-implicits.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9389" ] || [ "$CI_BRANCH" = "set-implicits" ]; then - - equations_CI_REF=set-implicits - equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations - - mtac2_CI_REF=set-implicits - mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2 - -fi diff --git a/dev/ci/user-overlays/09439-sep-variance.sh b/dev/ci/user-overlays/09439-sep-variance.sh deleted file mode 100644 index cca85a2f68..0000000000 --- a/dev/ci/user-overlays/09439-sep-variance.sh +++ /dev/null @@ -1,14 +0,0 @@ - -if [ "$CI_PULL_REQUEST" = "9439" ] || [ "$CI_BRANCH" = "sep-variance" ]; then - elpi_CI_REF=sep-variance - elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi - - equations_CI_REF=sep-variance - equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations - - mtac2_CI_REF=sep-variance - mtac2_CI_GITURL=https://github.com/SkySkimmer/mtac2 - - paramcoq_CI_REF=sep-variance - paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq -fi diff --git a/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh b/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh deleted file mode 100644 index 1af8b5430d..0000000000 --- a/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9476" ] || [ "$CI_BRANCH" = "context-constructor" ]; then - - quickchick_CI_REF=context-constructor - quickchick_CI_GITURL=https://github.com/ppedrot/QuickChick - - equations_CI_REF=context-constructor - equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/09567-ejgallego-hooks_unify.sh b/dev/ci/user-overlays/09567-ejgallego-hooks_unify.sh deleted file mode 100644 index 27ce9aca16..0000000000 --- a/dev/ci/user-overlays/09567-ejgallego-hooks_unify.sh +++ /dev/null @@ -1,12 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9567" ] || [ "$CI_BRANCH" = "hooks_unify" ]; then - - equations_CI_REF=hooks_unify - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - mtac2_CI_REF=hooks_unify - mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - - paramcoq_CI_REF=hooks_unify - paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq - -fi diff --git a/dev/ci/user-overlays/09602-gares-more-delta-in-termination-checking.sh b/dev/ci/user-overlays/09602-gares-more-delta-in-termination-checking.sh deleted file mode 100644 index 18a295cdbb..0000000000 --- a/dev/ci/user-overlays/09602-gares-more-delta-in-termination-checking.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9602" ] || [ "$CI_BRANCH" = "more-delta-in-termination-checking" ]; then - - equations_CI_REF=more-delta-in-termination-checking - equations_CI_GITURL=https://github.com/gares/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/09678-printed-by-env.sh b/dev/ci/user-overlays/09678-printed-by-env.sh deleted file mode 100644 index ccb3498764..0000000000 --- a/dev/ci/user-overlays/09678-printed-by-env.sh +++ /dev/null @@ -1,14 +0,0 @@ - -if [ "$CI_PULL_REQUEST" = "9678" ] || [ "$CI_BRANCH" = "printed-by-env" ]; then - elpi_CI_REF=printed-by-env - elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi - - equations_CI_REF=printed-by-env - equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations - - ltac2_CI_REF=printed-by-env - ltac2_CI_GITURL=https://github.com/maximedenes/ltac2 - - quickchick_CI_REF=printed-by-env - quickchick_CI_GITURL=https://github.com/maximedenes/QuickChick -fi diff --git a/dev/ci/user-overlays/09733-gares-quotations.sh b/dev/ci/user-overlays/09733-gares-quotations.sh deleted file mode 100644 index b17454fc4c..0000000000 --- a/dev/ci/user-overlays/09733-gares-quotations.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9733" ] || [ "$CI_BRANCH" = "quotations" ]; then - - ltac2_CI_REF=quotations - ltac2_CI_GITURL=https://github.com/gares/ltac2 - -fi diff --git a/dev/ci/user-overlays/09815-token-type.sh b/dev/ci/user-overlays/09815-token-type.sh deleted file mode 100644 index 4b49011de3..0000000000 --- a/dev/ci/user-overlays/09815-token-type.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9815" ] || [ "$CI_BRANCH" = "token-type" ]; then - ltac2_CI_REF=token-type - ltac2_CI_GITURL=https://github.com/proux01/ltac2 -fi diff --git a/dev/ci/user-overlays/09870-vbgl-recordops.sh b/dev/ci/user-overlays/09870-vbgl-recordops.sh deleted file mode 100644 index bb14a8c204..0000000000 --- a/dev/ci/user-overlays/09870-vbgl-recordops.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9870" ] || [ "$CI_BRANCH" = "doc-canonical" ]; then - - elpi_CI_REF=pr-9870 - elpi_CI_GITURL=https://github.com/vbgl/coq-elpi - -fi diff --git a/dev/ci/user-overlays/09895-ejgallego-require+upper.sh b/dev/ci/user-overlays/09895-ejgallego-require+upper.sh deleted file mode 100644 index 9a42c829ce..0000000000 --- a/dev/ci/user-overlays/09895-ejgallego-require+upper.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9895" ] || [ "$CI_BRANCH" = "require+upper" ]; then - - quickchick_CI_REF=require+upper - quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick - -fi diff --git a/dev/ci/user-overlays/09909-maximedenes-pretyping-rm-global.sh b/dev/ci/user-overlays/09909-maximedenes-pretyping-rm-global.sh deleted file mode 100644 index 01d3068591..0000000000 --- a/dev/ci/user-overlays/09909-maximedenes-pretyping-rm-global.sh +++ /dev/null @@ -1,21 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9909" ] || [ "$CI_BRANCH" = "pretyping-rm-global" ]; then - - elpi_CI_REF=pretyping-rm-global - elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi - - coqhammer_CI_REF=pretyping-rm-global - coqhammer_CI_GITURL=https://github.com/maximedenes/coqhammer - - equations_CI_REF=pretyping-rm-global - equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations - - ltac2_CI_REF=pretyping-rm-global - ltac2_CI_GITURL=https://github.com/maximedenes/ltac2 - - paramcoq_CI_REF=pretyping-rm-global - paramcoq_CI_GITURL=https://github.com/maximedenes/paramcoq - - mtac2_CI_REF=pretyping-rm-global - mtac2_CI_GITURL=https://github.com/maximedenes/Mtac2 - -fi diff --git a/dev/ci/user-overlays/09973-gares-elpi-2.1.sh b/dev/ci/user-overlays/09973-gares-elpi-2.1.sh deleted file mode 100644 index 9a6e25d893..0000000000 --- a/dev/ci/user-overlays/09973-gares-elpi-2.1.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9973" ] || [ "$CI_BRANCH" = "elpi-1.2" ]; then - - elpi_CI_REF=overlay-elpi1.2-coq-master - elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi - -fi diff --git a/dev/ci/user-overlays/10052-ppedrot-cleanup-logic-convert-hyp.sh b/dev/ci/user-overlays/10052-ppedrot-cleanup-logic-convert-hyp.sh deleted file mode 100644 index 9f9cc19e83..0000000000 --- a/dev/ci/user-overlays/10052-ppedrot-cleanup-logic-convert-hyp.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10052" ] || [ "$CI_BRANCH" = "cleanup-logic-convert-hyp" ]; then - - relation_algebra_CI_REF=cleanup-logic-convert-hyp - relation_algebra_CI_GITURL=https://github.com/ppedrot/relation-algebra - -fi diff --git a/dev/ci/user-overlays/10069-ppedrot-whd-for-evar-conv-no-stack.sh b/dev/ci/user-overlays/10069-ppedrot-whd-for-evar-conv-no-stack.sh deleted file mode 100644 index 0e1449f36c..0000000000 --- a/dev/ci/user-overlays/10069-ppedrot-whd-for-evar-conv-no-stack.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10069" ] || [ "$CI_BRANCH" = "whd-for-evar-conv-no-stack" ]; then - - unicoq_CI_REF=whd-for-evar-conv-no-stack - unicoq_CI_GITURL=https://github.com/ppedrot/unicoq - -fi diff --git a/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh b/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh deleted file mode 100644 index 2015935dd9..0000000000 --- a/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10076" ] || [ "$CI_BRANCH" = "canonical-disable-hint" ]; then - - elpi_CI_REF=canonical-disable-hint - elpi_CI_GITURL=https://github.com/vbgl/coq-elpi - -fi diff --git a/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh b/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh deleted file mode 100644 index 4032b1c6b5..0000000000 --- a/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10125" ] || [ "$CI_BRANCH" = "run_tactic_gen" ]; then - - paramcoq_CI_REF=run_tactic_gen - paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq - -fi diff --git a/dev/ci/user-overlays/10133-SkySkimmer-kelim.sh b/dev/ci/user-overlays/10133-SkySkimmer-kelim.sh deleted file mode 100644 index 3658e96a3a..0000000000 --- a/dev/ci/user-overlays/10133-SkySkimmer-kelim.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10133" ] || [ "$CI_BRANCH" = "kelim" ]; then - - equations_CI_REF=kelim - equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh b/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh deleted file mode 100644 index bc8aa33565..0000000000 --- a/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10135" ] || [ "$CI_BRANCH" = "detype-anonymous" ]; then - - unicoq_CI_REF=detype-anonymous - unicoq_CI_GITURL=https://github.com/maximedenes/unicoq - -fi diff --git a/dev/ci/user-overlays/10157-SkySkimmer-def-not-visible-generic-warning.sh b/dev/ci/user-overlays/10157-SkySkimmer-def-not-visible-generic-warning.sh deleted file mode 100644 index fcbeb32a58..0000000000 --- a/dev/ci/user-overlays/10157-SkySkimmer-def-not-visible-generic-warning.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10188" ] || [ "$CI_BRANCH" = "def-not-visible-remove-warning" ]; then - - elpi_CI_REF=def-not-visible-generic-warning - elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi - -fi diff --git a/dev/ci/user-overlays/10177-SkySkimmer-generalize.sh b/dev/ci/user-overlays/10177-SkySkimmer-generalize.sh deleted file mode 100644 index a89f6aca1b..0000000000 --- a/dev/ci/user-overlays/10177-SkySkimmer-generalize.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10177" ] || [ "$CI_BRANCH" = "generalize" ]; then - - quickchick_CI_REF=generalize - quickchick_CI_GITURL=https://github.com/SkySkimmer/QuickChick - -fi diff --git a/dev/ci/user-overlays/10201-ppedrot-opaque-future-cleanup.sh b/dev/ci/user-overlays/10201-ppedrot-opaque-future-cleanup.sh deleted file mode 100644 index e3bbb84bcb..0000000000 --- a/dev/ci/user-overlays/10201-ppedrot-opaque-future-cleanup.sh +++ /dev/null @@ -1,15 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10201" ] || [ "$CI_BRANCH" = "opaque-future-cleanup" ]; then - - coq_dpdgraph_CI_REF=opaque-future-cleanup - coq_dpdgraph_CI_GITURL=https://github.com/ppedrot/coq-dpdgraph - - coqhammer_CI_REF=opaque-future-cleanup - coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer - - elpi_CI_REF=opaque-future-cleanup - elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi - - paramcoq_CI_REF=opaque-future-cleanup - paramcoq_CI_GITURL=https://github.com/ppedrot/paramcoq - -fi diff --git a/dev/ci/user-overlays/10215-gares-less-ontop.sh b/dev/ci/user-overlays/10215-gares-less-ontop.sh deleted file mode 100644 index bceb5ad0e8..0000000000 --- a/dev/ci/user-overlays/10215-gares-less-ontop.sh +++ /dev/null @@ -1,15 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10215" ] || [ "$CI_BRANCH" = "custom-typing" ]; then - - equations_CI_REF=pass-less-ontop - equations_CI_GITURL=https://github.com/gares/Coq-Equations - - mtac2_CI_REF=pass-less-ontop - mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2 - - paramcoq_CI_REF=pass-less-ontop - paramcoq_CI_GITURL=https://github.com/gares/paramcoq - - quickchick_CI_REF=pass-less-ontop - quickchick_CI_GITURL=https://github.com/gares/QuickChick - -fi diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index 7fb73e447d..4c2f264a74 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -21,14 +21,14 @@ The name of your overlay file should start with a five-digit pull request number, followed by a dash, anything (for instance your GitHub nickname and the branch name), then a `.sh` extension (`[0-9]{5}-[a-zA-Z0-9-_]+.sh`). -Example: `00669-maximedenes-ssr-merge.sh` containing +Example: `10185-SkySkimmer-instance-no-bang.sh` containing ``` -#!/bin/sh +if [ "$CI_PULL_REQUEST" = "10185" ] || [ "$CI_BRANCH" = "instance-no-bang" ]; then + + quickchick_CI_REF=instance-no-bang + quickchick_CI_GITURL=https://github.com/SkySkimmer/QuickChick -if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then - mathcomp_CI_REF=ssr-merge - mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp fi ``` diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el index b89ae67a82..5f9f326750 100644 --- a/dev/tools/coqdev.el +++ b/dev/tools/coqdev.el @@ -78,11 +78,7 @@ Specifically `camldebug-command-name' and `ocamldebug-command-name'." Note that this function is executed before _Coqproject is read if it exists." (let ((dir (coqdev-default-directory))) (when dir - (unless coq-prog-args - (setq coq-prog-args - `("-coqlib" ,dir - "-topfile" ,buffer-file-name))) - (setq-local coq-prog-name (concat dir "bin/coqtop"))))) + (setq-local coq-prog-name (concat dir "_build/default/dev/shim/coqtop-prelude"))))) (add-hook 'hack-local-variables-hook #'coqdev-setup-proofgeneral) (defvar coqdev-ocamldebug-command "dune exec dev/dune-dbg" diff --git a/doc/changelog/04-tactics/10205-discriminate-HoTT.rst b/doc/changelog/04-tactics/10205-discriminate-HoTT.rst new file mode 100644 index 0000000000..bb2d2a092e --- /dev/null +++ b/doc/changelog/04-tactics/10205-discriminate-HoTT.rst @@ -0,0 +1,6 @@ +- Make the :tacn:`discriminate` tactic work together with + :flag:`Universe Polymorphism` and equality in :g:`Type`. This, + in particular, makes :tacn:`discriminate` compatible with the HoTT + library https://github.com/HoTT/HoTT. + (`#10205 <https://github.com/coq/coq/pull/10205>`_, + by Andreas Lynge, review by Pierre-Marie Pédrot and Matthieu Sozeau) diff --git a/doc/changelog/04-tactics/10318-select-only-error.rst b/doc/changelog/04-tactics/10318-select-only-error.rst new file mode 100644 index 0000000000..03ed15d948 --- /dev/null +++ b/doc/changelog/04-tactics/10318-select-only-error.rst @@ -0,0 +1,4 @@ +- The goal selector tactical ``only`` now checks that the goal range + it is given is valid instead of ignoring goals out of the focus + range. (`#10318 <https://github.com/coq/coq/pull/10318>`_, by Gaëtan + Gilbert). diff --git a/doc/changelog/05-tactic-language/10002-ltac2.rst b/doc/changelog/05-tactic-language/10002-ltac2.rst new file mode 100644 index 0000000000..6d62f11eff --- /dev/null +++ b/doc/changelog/05-tactic-language/10002-ltac2.rst @@ -0,0 +1,9 @@ +- Ltac2, a new version of the tactic language Ltac, that doesn't + preserve backward compatibility, has been integrated in the main Coq + distribution. It is still experimental, but we already recommend + users of advanced Ltac to start using it and report bugs or request + enhancements. See its documentation in the :ref:`dedicated chapter + <ltac2>` (`#10002 <https://github.com/coq/coq/pull/10002>`_, plugin + authored by Pierre-Marie Pédrot, with contributions by various + users, integration by Maxime Dénès, help on integrating / improving + the documentation by Théo Zimmermann and Jim Fehrle). diff --git a/doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst b/doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst new file mode 100644 index 0000000000..bd1c0c42e8 --- /dev/null +++ b/doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst @@ -0,0 +1,5 @@ +- Ltac2 tactic notations with “constr” arguments can specify the + interpretation scope for these arguments; + see :ref:`ltac2_notations` for details + (`#10289 <https://github.com/coq/coq/pull/10289>`_, + by Vincent Laporte). diff --git a/doc/changelog/08-tools/10245-require-command-line.rst b/doc/changelog/08-tools/10245-require-command-line.rst new file mode 100644 index 0000000000..54417077f5 --- /dev/null +++ b/doc/changelog/08-tools/10245-require-command-line.rst @@ -0,0 +1,6 @@ +- Add command line options `-require-import`, `-require-export`, + `-require-import-from` and `-require-export-from`, as well as their + shorthand, `-ri`, `-re`, `-refrom` and -`rifrom`. Deprecate + confusing command line option `-require` + (`#10245 <https://github.com/coq/coq/pull/10245>`_ + by Hugo Herbelin, review by Emilio Gallego). diff --git a/doc/plugin_tutorial/README.md b/doc/plugin_tutorial/README.md index f82edb2352..6d142a9af8 100644 --- a/doc/plugin_tutorial/README.md +++ b/doc/plugin_tutorial/README.md @@ -1,34 +1,20 @@ How to write plugins in Coq =========================== - # Working environment : merlin, tuareg (open question) + # Working environment + + In addition to installing OCaml and Coq, it can help to install several tools for development. - ## OCaml & related tools + ## Merlin These instructions use [OPAM](http://opam.ocaml.org/doc/Install.html) ```shell -opam init --root=$PWD/CIW2018 --compiler=4.06.0 -j2 -eval `opam config env --root=$PWD/CIW2018` -opam install camlp5 ocamlfind num # Coq's dependencies -opam install lablgtk # Coqide's dependencies (optional) opam install merlin # prints instructions for vim and emacs ``` - ## Coq - -```shell -git clone git@github.com:coq/coq.git -cd coq -./configure -profile devel -make -j2 -cd .. -export PATH=$PWD/coq/bin:$PATH -``` - ## This tutorial ```shell -git clone git@github.com:ybertot/plugin_tutorials.git cd plugin_tutorials/tuto0 make .merlin # run before opening .ml files in your editor make # build @@ -40,6 +26,8 @@ make # build package a ml4 file in a plugin, organize a `Makefile`, `_CoqProject` - Example of syntax to add a new toplevel command - Example of function call to print a simple message + - Example of function call to print a simple warning + - Example of function call to raise a simple error to the user - Example of syntax to add a simple tactic (that does nothing and prints a message) - To use it: @@ -54,19 +42,23 @@ make # build Require Import Tuto0.Loader. HelloWorld. ``` - # tuto1 : Ocaml to Coq communication + You can also modify and run `theories/Demo.v`. + + # tuto1 : OCaml to Coq communication Explore the memory of Coq, modify it - - Commands that take arguments: strings, symbols, expressions of the calculus of constructions + - Commands that take arguments: strings, integers, symbols, expressions of the calculus of constructions + - Examples of using environments correctly + - Examples of using state (the evar_map) correctly - Commands that interact with type-checking in Coq + - A command that checks convertibility between two terms - A command that adds a new definition or theorem - - A command that uses a name and exploits the existing definitions - or theorems + - A command that uses a name and exploits the existing definitions or theorems - A command that exploits an existing ongoing proof - A command that defines a new tactic Compilation and loading must be performed as for `tuto0`. - # tuto2 : Ocaml to Coq communication + # tuto2 : OCaml to Coq communication A more step by step introduction to writing commands - Explanation of the syntax of entries - Adding a new type to and parsing to the available choices diff --git a/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg b/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg index 5c633fe862..97689adfed 100644 --- a/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg +++ b/doc/plugin_tutorial/tuto0/src/g_tuto0.mlg @@ -5,14 +5,70 @@ DECLARE PLUGIN "tuto0_plugin" open Pp open Ltac_plugin +let tuto_warn = CWarnings.create ~name:"name" ~category:"category" + (fun _ -> strbrk Tuto0_main.message) + } +(*** Printing messages ***) + +(* + * This defines a command that prints HelloWorld. + * Note that Feedback.msg_notice can be used to print messages. + *) VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY | [ "HelloWorld" ] -> { Feedback.msg_notice (strbrk Tuto0_main.message) } END +(* + * This is a tactic version of the same thing. + *) TACTIC EXTEND hello_world_tactic | [ "hello_world" ] -> { let _ = Feedback.msg_notice (str Tuto0_main.message) in Tacticals.New.tclIDTAC } END + +(*** Printing warnings ***) + +(* + * This defines a command that prints HelloWorld as a warning. + * tuto_warn is defined at the top-level, before the command runs, + * which is standard. + *) +VERNAC COMMAND EXTEND HelloWarning CLASSIFIED AS QUERY +| [ "HelloWarning" ] -> + { + tuto_warn () + } +END + +(* + * This is a tactic version of the same thing. + *) +TACTIC EXTEND hello_warning_tactic +| [ "hello_warning" ] -> + { + let _ = tuto_warn () in + Tacticals.New.tclIDTAC + } +END + +(*** Printing errors ***) + +(* + * This defines a command that prints HelloWorld inside of an error. + * Note that CErrors.user_err can be used to raise errors to the user. + *) +VERNAC COMMAND EXTEND HelloError CLASSIFIED AS QUERY +| [ "HelloError" ] -> { CErrors.user_err (str Tuto0_main.message) } +END + +(* + * This is a tactic version of the same thing. + *) +TACTIC EXTEND hello_error_tactic +| [ "hello_error" ] -> + { let _ = CErrors.user_err (str Tuto0_main.message) in + Tacticals.New.tclIDTAC } +END diff --git a/doc/plugin_tutorial/tuto0/theories/Demo.v b/doc/plugin_tutorial/tuto0/theories/Demo.v index bdc61986af..54d5239421 100644 --- a/doc/plugin_tutorial/tuto0/theories/Demo.v +++ b/doc/plugin_tutorial/tuto0/theories/Demo.v @@ -1,8 +1,28 @@ From Tuto0 Require Import Loader. +(*** Printing messages ***) + HelloWorld. Lemma test : True. Proof. hello_world. Abort. + +(*** Printing warnings ***) + +HelloWarning. + +Lemma test : True. +Proof. +hello_warning. +Abort. + +(*** Signaling errors ***) + +Fail HelloError. + +Lemma test : True. +Proof. +Fail hello_error. +Abort. diff --git a/doc/plugin_tutorial/tuto1/_CoqProject b/doc/plugin_tutorial/tuto1/_CoqProject index 585d1360be..60f9f0a0c7 100644 --- a/doc/plugin_tutorial/tuto1/_CoqProject +++ b/doc/plugin_tutorial/tuto1/_CoqProject @@ -2,7 +2,10 @@ -I src theories/Loader.v +theories/Demo.v +src/inspector.mli +src/inspector.ml src/simple_check.mli src/simple_check.ml src/simple_declare.mli diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg index 300d62285a..0b005a2341 100644 --- a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg +++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg @@ -8,7 +8,6 @@ DECLARE PLUGIN "tuto1_plugin" theories/Loader.v *) open Ltac_plugin -open Attributes open Pp (* This module defines the types of arguments to be used in the EXTEND directives below, for example the string one. *) @@ -16,136 +15,276 @@ open Stdarg } -VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY -| [ "Hello" string(s) ] -> - { Feedback.msg_notice (strbrk "Hello " ++ str s) } -END +(*** Printing inputs ***) -(* reference is allowed as a syntactic entry, but so are all the entries - found the signature of module Prim in file coq/parsing/pcoq.mli *) +(* + * This command prints an input from the user. + * + * A list with allowable inputs can be found in interp/stdarg.mli, + * plugin/ltac/extraargs.mli, and plugin/ssr/ssrparser.mli + * (remove the wit_ prefix), but not all of these are allowable + * (unit and bool, for example, are not usable from within here). + * + * We include only some examples that are standard and useful for commands. + * Some of the omitted examples are useful for tactics. + * + * Inspector is our own file that defines a simple messaging function. + * The printing functions (pr_qualid and so on) are in printing. + * + * Some of these cases would be ambiguous if we used "What's" for each of + * these. For example, all of these are terms. We purposely disambiguate. + *) +VERNAC COMMAND EXTEND WhatIsThis CLASSIFIED AS QUERY +| [ "What's" constr(e) ] -> + { + let env = Global.env () in (* we'll explain later *) + let sigma = Evd.from_env env in (* we'll explain later *) + Inspector.print_input e (Ppconstr.pr_constr_expr env sigma) "term" + } +| [ "What" "kind" "of" "term" "is" string(s) ] -> + { Inspector.print_input s strbrk "string" } +| [ "What" "kind" "of" "term" "is" int(i) ] -> + { Inspector.print_input i Pp.int "int" } +| [ "What" "kind" "of" "term" "is" ident(id) ] -> + { Inspector.print_input id Ppconstr.pr_id "identifier" } +| [ "What" "kind" "of" "identifier" "is" reference(r) ] -> + { Inspector.print_input r Ppconstr.pr_qualid "reference" } +END -VERNAC COMMAND EXTEND HelloAgain CLASSIFIED AS QUERY -| [ "HelloAgain" reference(r)] -> -(* The function Ppconstr.pr_qualid was found by searching all mli files - for a function of type qualid -> Pp.t *) - { Feedback.msg_notice - (strbrk "Hello again " ++ Ppconstr.pr_qualid r)} +(* + * This command demonstrates basic combinators built into the DSL here. + * You can generalize this for constr_list, constr_opt, int_list, and so on. + *) +VERNAC COMMAND EXTEND WhatAreThese CLASSIFIED AS QUERY +| [ "What" "is" int_list(l) "a" "list" "of" ] -> + { + let print l = str "[" ++ Pp.prlist_with_sep (fun () -> str ";") Pp.int l ++ str "]" in + Inspector.print_input l print "int list" + } +| [ "Is" ne_int_list(l) "nonempty" ] -> + { + let print l = str "[" ++ Pp.prlist_with_sep (fun () -> str ";") Pp.int l ++ str "]" in + Inspector.print_input l print "nonempty int list" + } +| [ "And" "is" int_opt(o) "provided" ] -> + { + let print o = strbrk (if Option.has_some o then "Yes" else "No") in + Feedback.msg_notice (print o) + } END -(* According to parsing/pcoq.mli, e has type constr_expr *) -(* this type is defined in pretyping/constrexpr.ml *) -(* Question for the developers: why is the file constrexpr.ml and not - constrexpr.mli --> Easier for packing the software in components. *) -VERNAC COMMAND EXTEND TakingConstr CLASSIFIED AS QUERY -| [ "Cmd1" constr(e) ] -> - { let _ = e in Feedback.msg_notice (strbrk "Cmd1 parsed something") } + +(*** Interning terms ***) + +(* + * The next step is to make something of parsed expression. + * Interesting information in interp/constrintern.mli. + * + * When you read in constr(e), e will have type Constrexpr.constr_expr, + * which is defined in pretyping/constrexpr.ml. Your plugin + * will want a different representation. + * + * The important function is Constrintern.interp_constr_evars, + * which converts between a constr_expr and an + * (EConstr.constr, evar_map) pair. This essentially contains + * an internal representation of the term along with some state. + * For more on the state, read /dev/doc/econstr.md. + * + * NOTE ON INTERNING: Always prefer Constrintern.interp_constr_evars + * over Constrintern.interp_constr. The latter is an internal function + * not meant for external use. + * + * To get your initial environment, call Global.env (). + * To get state from that environment, call Evd.from_env on that environment. + * It is important to NEVER use the empty environment or Evd.empty; + * if you do, you will get confusing errors. + * + * NOTE ON STATE: It is important to use the evar_map that is returned to you. + * Otherwise, you may get cryptic errors later in your plugin. + * For example, you may get universe inconsistency errors. + * In general, if a function returns an evar_map to you, that's the one + * you want to thread through the rest of your command. + * + * NOTE ON STYLE: In general, it's better practice to move large + * chunks of OCaml code like this one into an .ml file. We include + * this here because it's really important to understand how to + * thread state in a plugin, and it's easier to see that if it's in the + * top-level file itself. + *) +VERNAC COMMAND EXTEND Intern CLASSIFIED AS QUERY +| [ "Intern" constr(e) ] -> + { + let env = Global.env () in (* use this; never use empty *) + let sigma = Evd.from_env env in (* use this; never use empty *) + let debug sigma = Termops.pr_evar_map ~with_univs:true None env sigma in + Feedback.msg_notice (strbrk "State before intern: " ++ debug sigma); + let (sigma, t) = Constrintern.interp_constr_evars env sigma e in + Feedback.msg_notice (strbrk "State after intern: " ++ debug sigma); + let print t = Printer.pr_econstr_env env sigma t in + Feedback.msg_notice (strbrk "Interned: " ++ print t) + } END -(* The next step is to make something of parsed expression. - Interesting information in interp/constrintern.mli *) - -(* There are several phases of transforming a parsed expression into - the final internal data-type (constr). There exists a collection of - functions that combine all the phases *) - -VERNAC COMMAND EXTEND TakingConstr2 CLASSIFIED AS QUERY -| [ "Cmd2" constr(e) ] -> - { let _ = Constrintern.interp_constr - (Global.env()) - (* Make sure you don't use Evd.empty here, as this does not - check consistency with existing universe constraints. *) - (Evd.from_env (Global.env())) e in - Feedback.msg_notice (strbrk "Cmd2 parsed something legitimate") } +(*** Defining terms ***) + +(* + * To define a term, we start similarly to our intern functionality, + * then we call another function. We define this function in + * the Simple_declare module. + * + * The line #[ poly = Attributes.polymorphic ] says that this command accepts + * polymorphic attributes. + * @SkySkimmer: Here, poly is what the result is bound to in the + * rule's code. Multiple attributes may be used separated by ;, and we have + * punning so foo is equivalent to foo = foo. + * + * The declare_definition function returns the reference + * that was defined. This reference will be present in the new environment. + * If you want to refer to it later in your plugin, you must use an + * updated environment and the constructed reference. + * + * Note since we are now defining a term, we must classify this + * as a side-effect (CLASSIFIED AS SIDEFF). + *) +VERNAC COMMAND EXTEND MyDefine CLASSIFIED AS SIDEFF +| #[ poly = Attributes.polymorphic ] [ "MyDefine" ident(i) ":=" constr(e) ] -> + { + let env = Global.env () in + let sigma = Evd.from_env env in + let (sigma, t) = Constrintern.interp_constr_evars env sigma e in + let r = Simple_declare.declare_definition ~poly i sigma t in + let print r = strbrk "Defined " ++ Printer.pr_global r ++ strbrk "." in + Feedback.msg_notice (print r) + } END -(* This is to show what happens when typing in an empty environment - with an empty evd. - Question for the developers: why does "Cmd3 (fun x : nat => x)." - raise an anomaly, not the same error as "Cmd3 (fun x : a => x)." *) - -VERNAC COMMAND EXTEND TakingConstr3 CLASSIFIED AS QUERY -| [ "Cmd3" constr(e) ] -> - { let _ = Constrintern.interp_constr Environ.empty_env - Evd.empty e in - Feedback.msg_notice - (strbrk "Cmd3 accepted something in the empty context")} +(*** Printing terms ***) + +(* + * This command takes a name and return its value. It does less + * than Print, because it fails on constructors, axioms, and inductive types. + * It signals an error to the user for unsupported terms. + * + * Simple_print contains simple_body_access, which shows how to look up + * a global reference. + *) +VERNAC COMMAND EXTEND ExamplePrint CLASSIFIED AS QUERY +| [ "MyPrint" reference(r) ] -> + { + let env = Global.env () in + let sigma = Evd.from_env env in + try + let t = Simple_print.simple_body_access (Nametab.global r) in + Feedback.msg_notice (Printer.pr_econstr_env env sigma t) + with Failure s -> + CErrors.user_err (str s) + } END -(* When adding a definition, we have to be careful that just - the operation of constructing a well-typed term may already change - the environment, at the level of universe constraints (which - are recorded in the evd component). The function - Constrintern.interp_constr ignores this side-effect, so it should - not be used here. *) - -(* Looking at the interface file interp/constrintern.ml4, I lost - some time because I did not see that the "constr" type appearing - there was "EConstr.constr" and not "Constr.constr". *) - -VERNAC COMMAND EXTEND Define1 CLASSIFIED AS SIDEFF -| #[ poly = polymorphic ] [ "Cmd4" ident(i) constr(e) ] -> - { let v = Constrintern.interp_constr (Global.env()) - (Evd.from_env (Global.env())) e in - Simple_declare.packed_declare_definition ~poly i v } +(* + * This command shows that after you define a new term, + * you can also look it up. But there's a catch! You need to actually + * refresh your environment. Otherwise, the defined term + * will not be in the environment. + * + * Using the global reference as opposed to the ID is generally + * a good idea, otherwise you might end up running into unforeseen + * problems inside of modules and sections and so on. + * + * Inside of simple_body_access, note that it uses Global.env (), + * which refreshes the environment before looking up the term. + *) +VERNAC COMMAND EXTEND DefineLookup CLASSIFIED AS SIDEFF +| #[ poly = Attributes.polymorphic ] [ "DefineLookup" ident(i) ":=" constr(e) ] -> + { + let env = Global.env () in + let sigma = Evd.from_env env in + let (sigma, t) = Constrintern.interp_constr_evars env sigma e in + let r = Simple_declare.declare_definition ~poly i sigma t in + let print r = strbrk "Defined " ++ Printer.pr_global r ++ strbrk "." in + Feedback.msg_notice (print r); + let env = Global.env () in + let sigma = Evd.from_env env in + let t = Simple_print.simple_body_access r in + let print t = strbrk "Found " ++ Printer.pr_econstr_env env sigma t in + Feedback.msg_notice (print t) + } END +(*** Checking terms ***) + +(* + * These are two commands for simple type-checking of terms. + * The bodies and explanations of the differences are in simple_check.ml. + *) + VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY -| [ "Cmd5" constr(e) ] -> - { let v = Constrintern.interp_constr (Global.env()) - (Evd.from_env (Global.env())) e in - let (_, ctx) = v in - let sigma = Evd.from_ctx ctx in - Feedback.msg_notice - (Printer.pr_econstr_env (Global.env()) sigma - (Simple_check.simple_check1 v)) } +| [ "Check1" constr(e) ] -> + { + let env = Global.env () in + let sigma = Evd.from_env env in + let (sigma, t) = Constrintern.interp_constr_evars env sigma e in + let (sigma, typ) = Simple_check.simple_check1 env sigma t in + Feedback.msg_notice (Printer.pr_econstr_env env sigma typ) + } END VERNAC COMMAND EXTEND Check2 CLASSIFIED AS QUERY -| [ "Cmd6" constr(e) ] -> - { let v = Constrintern.interp_constr (Global.env()) - (Evd.from_env (Global.env())) e in - let sigma, ty = Simple_check.simple_check2 v in - Feedback.msg_notice - (Printer.pr_econstr_env (Global.env()) sigma ty) } +| [ "Check2" constr(e) ] -> + { + let env = Global.env () in + let sigma = Evd.from_env env in + let (sigma, t) = Constrintern.interp_constr_evars env sigma e in + let typ = Simple_check.simple_check2 env sigma t in + Feedback.msg_notice (Printer.pr_econstr_env env sigma typ) + } END -VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY -| [ "Cmd7" constr(e) ] -> - { let v = Constrintern.interp_constr (Global.env()) - (Evd.from_env (Global.env())) e in - let (a, ctx) = v in - let sigma = Evd.from_ctx ctx in - Feedback.msg_notice - (Printer.pr_econstr_env (Global.env()) sigma - (Simple_check.simple_check3 v)) } -END +(*** Convertibility ***) -(* This command takes a name and return its value. It does less - than Print, because it fails on constructors, axioms, and inductive types. - This should be improved, because the error message is an anomaly. - Anomalies should never appear even when using a command outside of its - intended use. *) -VERNAC COMMAND EXTEND ExamplePrint CLASSIFIED AS QUERY -| [ "Cmd8" reference(r) ] -> - { let env = Global.env() in - let sigma = Evd.from_env env in - Feedback.msg_notice - (Printer.pr_econstr_env env sigma - (EConstr.of_constr - (Simple_print.simple_body_access (Nametab.global r)))) } +(* + * This command checks if there is a possible assignment of + * constraints in the state under which the two terms are + * convertible. + *) +VERNAC COMMAND EXTEND Convertible CLASSIFIED AS QUERY +| [ "Convertible" constr(e1) constr(e2) ] -> + { + let env = Global.env () in + let sigma = Evd.from_env env in + let (sigma, t1) = Constrintern.interp_constr_evars env sigma e1 in + let (sigma, t2) = Constrintern.interp_constr_evars env sigma e2 in + match Reductionops.infer_conv env sigma t1 t2 with + | Some _ -> + Feedback.msg_notice (strbrk "Yes :)") + | None -> + Feedback.msg_notice (strbrk "No :(") + } END +(*** Introducing terms ***) + +(* + * We can call the tactics defined in Tactics within our tactics. + * Here we call intros. + *) TACTIC EXTEND my_intro | [ "my_intro" ident(i) ] -> { Tactics.introduction i } END -(* if one write this: - VERNAC COMMAND EXTEND exploreproof CLASSIFIED AS QUERY - it gives an error message that is basically impossible to understand. *) +(*** Exploring proof state ***) +(* + * This command demonstrates exploring the proof state from within + * a command. + * + * Note that Pfedit.get_current_context gets us the environment + * and state within a proof, as opposed to the global environment + * and state. This is important within tactics. + *) VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY -| ![ proof_query ] [ "Cmd9" ] -> +| ![ proof_query ] [ "ExploreProof" ] -> { fun ~pstate -> let sigma, env = Pfedit.get_current_context pstate in let pprf = Proof.partial_proof Proof_global.(give_me_the_proof pstate) in diff --git a/doc/plugin_tutorial/tuto1/src/inspector.ml b/doc/plugin_tutorial/tuto1/src/inspector.ml new file mode 100644 index 0000000000..d37cbdb74c --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/inspector.ml @@ -0,0 +1,8 @@ +open Pp + +(* + * Inspect an input and print a feedback message explaining what it is + *) +let print_input (a : 'a) (printer : 'a -> Pp.t) (type_str : string) : unit = + let msg = printer a ++ strbrk (Printf.sprintf " is a %s." type_str) in + Feedback.msg_notice msg diff --git a/doc/plugin_tutorial/tuto1/src/inspector.mli b/doc/plugin_tutorial/tuto1/src/inspector.mli new file mode 100644 index 0000000000..52b970bbe0 --- /dev/null +++ b/doc/plugin_tutorial/tuto1/src/inspector.mli @@ -0,0 +1,4 @@ +(* + * Inspect an input and print a feedback message explaining what it is + *) +val print_input : 'a -> ('a -> Pp.t) -> string -> unit diff --git a/doc/plugin_tutorial/tuto1/src/simple_check.ml b/doc/plugin_tutorial/tuto1/src/simple_check.ml index c2f09c64e0..684864a056 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_check.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_check.ml @@ -1,32 +1,14 @@ -let simple_check1 value_with_constraints = - begin - let evalue, st = value_with_constraints in - let sigma = Evd.from_ctx st in -(* This is reverse engineered from vernacentries.ml *) -(* The point of renaming is to make sure the bound names printed by Check - can be re-used in `apply with` tactics that use bound names to - refer to arguments. *) - let j = Environ.on_judgment EConstr.of_constr - (Arguments_renaming.rename_typing (Global.env()) - (EConstr.to_constr sigma evalue)) in - let {Environ.uj_type=x}=j in x - end - -let simple_check2 value_with_constraints = - let evalue, st = value_with_constraints in - let sigma = Evd.from_ctx st in -(* This version should be preferred if bound variable names are not so - important, you want to really verify that the input is well-typed, +let simple_check1 env sigma evalue = +(* This version should be preferred if you want to really + verify that the input is well-typed, and if you want to obtain the type. *) (* Note that the output value is a pair containing a new evar_map: typing will fill out blanks in the term by add evar bindings. *) - Typing.type_of (Global.env()) sigma evalue + Typing.type_of env sigma evalue -let simple_check3 value_with_constraints = - let evalue, st = value_with_constraints in - let sigma = Evd.from_ctx st in -(* This version should be preferred if bound variable names are not so - important and you already expect the input to have been type-checked - before. Set ~lax to false if you want an anomaly to be raised in - case of a type error. Otherwise a ReTypeError exception is raised. *) - Retyping.get_type_of ~lax:true (Global.env()) sigma evalue +let simple_check2 env sigma evalue = +(* This version should be preferred if you already expect the input to + have been type-checked before. Set ~lax to false if you want an anomaly + to be raised in case of a type error. Otherwise a ReTypeError exception + is raised. *) + Retyping.get_type_of ~lax:true env sigma evalue diff --git a/doc/plugin_tutorial/tuto1/src/simple_check.mli b/doc/plugin_tutorial/tuto1/src/simple_check.mli index bcf1bf56cf..4b28ac74fe 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_check.mli +++ b/doc/plugin_tutorial/tuto1/src/simple_check.mli @@ -1,8 +1,5 @@ val simple_check1 : - EConstr.constr Evd.in_evar_universe_context -> EConstr.constr + Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.constr val simple_check2 : - EConstr.constr Evd.in_evar_universe_context -> Evd.evar_map * EConstr.constr - -val simple_check3 : - EConstr.constr Evd.in_evar_universe_context -> EConstr.constr + Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index e9b91d5a7e..1e582e6456 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -6,11 +6,9 @@ let edeclare ?hook ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps = let hook_data = Option.map (fun hook -> hook, uctx, []) hook in DeclareDef.declare_definition ident k ce ubinders imps ?hook_data -let packed_declare_definition ~poly ident value_with_constraints = - let body, ctx = value_with_constraints in - let sigma = Evd.from_ctx ctx in +let declare_definition ~poly ident sigma body = let k = (Decl_kinds.Global, poly, Decl_kinds.Definition) in let udecl = UState.default_univ_decl in - ignore (edeclare ident k ~opaque:false sigma udecl body None []) + edeclare ident k ~opaque:false sigma udecl body None [] (* But this definition cannot be undone by Reset ident *) diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.mli b/doc/plugin_tutorial/tuto1/src/simple_declare.mli index fd74e81526..c55b36742f 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.mli +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.mli @@ -1,5 +1,4 @@ open Names -open EConstr -val packed_declare_definition : - poly:bool -> Id.t -> constr Evd.in_evar_universe_context -> unit +val declare_definition : + poly:bool -> Id.t -> Evd.evar_map -> EConstr.t -> Names.GlobRef.t diff --git a/doc/plugin_tutorial/tuto1/src/simple_print.ml b/doc/plugin_tutorial/tuto1/src/simple_print.ml index 22a0163fbb..48b5f2214c 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_print.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_print.ml @@ -12,6 +12,6 @@ let simple_body_access gref = | Globnames.ConstRef cst -> let cb = Environ.lookup_constant cst (Global.env()) in match Global.body_of_constant_body Library.indirect_accessor cb with - | Some(e, _) -> e + | Some(e, _) -> EConstr.of_constr e | None -> failwith "This term has no value" diff --git a/doc/plugin_tutorial/tuto1/src/simple_print.mli b/doc/plugin_tutorial/tuto1/src/simple_print.mli index 254b56ff79..943e26acb6 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_print.mli +++ b/doc/plugin_tutorial/tuto1/src/simple_print.mli @@ -1 +1 @@ -val simple_body_access : Names.GlobRef.t -> Constr.constr +val simple_body_access : Names.GlobRef.t -> EConstr.constr diff --git a/doc/plugin_tutorial/tuto1/src/tuto1_plugin.mlpack b/doc/plugin_tutorial/tuto1/src/tuto1_plugin.mlpack index a797a509e0..9309f78cd0 100644 --- a/doc/plugin_tutorial/tuto1/src/tuto1_plugin.mlpack +++ b/doc/plugin_tutorial/tuto1/src/tuto1_plugin.mlpack @@ -1,3 +1,4 @@ +Inspector Simple_check Simple_declare Simple_print diff --git a/doc/plugin_tutorial/tuto1/theories/Demo.v b/doc/plugin_tutorial/tuto1/theories/Demo.v new file mode 100644 index 0000000000..5723e2f82e --- /dev/null +++ b/doc/plugin_tutorial/tuto1/theories/Demo.v @@ -0,0 +1,95 @@ +From Tuto1 Require Import Loader. + +(*** Printing user inputs ***) + +Definition definition := 5. +What's definition. +What kind of term is definition. +What kind of identifier is definition. + +What is 1 2 3 a list of. +What is a list of. (* no arguments = empty list *) + +Is 1 2 3 nonempty. +(* Is nonempty *) (* does not parse *) + +And is 1 provided. +And is provided. + +(*** Interning terms ***) + +Intern 3. +Intern definition. +Intern (fun (x : Prop) => x). +Intern (fun (x : Type) => x). +Intern (forall (T : Type), T). +Intern (fun (T : Type) (t : T) => t). +Intern _. +Intern (Type : Type). + +(*** Defining terms ***) + +MyDefine n := 1. +Print n. + +MyDefine f := (fun (x : Type) => x). +Print f. + +(*** Printing terms ***) + +MyPrint f. +MyPrint n. +Fail MyPrint nat. + +DefineLookup n' := 1. +DefineLookup f' := (fun (x : Type) => x). + +(*** Checking terms ***) + +Check1 3. +Check1 definition. +Check1 (fun (x : Prop) => x). +Check1 (fun (x : Type) => x). +Check1 (forall (T : Type), T). +Check1 (fun (T : Type) (t : T) => t). +Check1 _. +Check1 (Type : Type). + +Check2 3. +Check2 definition. +Check2 (fun (x : Prop) => x). +Check2 (fun (x : Type) => x). +Check2 (forall (T : Type), T). +Check2 (fun (T : Type) (t : T) => t). +Check2 _. +Check2 (Type : Type). + +(*** Convertibility ***) + +Convertible 1 1. +Convertible (fun (x : Type) => x) (fun (x : Type) => x). +Convertible Type Type. +Convertible 1 ((fun (x : nat) => x) 1). + +Convertible 1 2. +Convertible (fun (x : Type) => x) (fun (x : Prop) => x). +Convertible Type Prop. +Convertible 1 ((fun (x : nat) => x) 2). + +(*** Introducing variables ***) + +Theorem foo: + forall (T : Set) (t : T), T. +Proof. + my_intro T. my_intro t. apply t. +Qed. + +(*** Exploring proof state ***) + +Fail ExploreProof. (* not in a proof *) + +Theorem bar: + forall (T : Set) (t : T), T. +Proof. + ExploreProof. my_intro T. ExploreProof. my_intro t. ExploreProof. apply t. +Qed. diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index bdda35fcc0..48d5f4075e 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -124,11 +124,11 @@ and ``coqtop``, unless stated otherwise: :ref:`names-of-libraries` and the command Declare ML Module Section :ref:`compiled-files`. -:-Q *directory* dirpath: Add physical path *directory* to the list of +:-Q *directory* *dirpath*: Add physical path *directory* to the list of directories where |Coq| looks for a file and bind it to the logical directory *dirpath*. The subdirectory structure of *directory* is recursively available from |Coq| using absolute names (extending the - dirpath prefix) (see Section :ref:`qualified-names`).Note that only those + :n:`@dirpath` prefix) (see Section :ref:`qualified-names`). Note that only those subdirectories and files which obey the lexical conventions of what is an :n:`@ident` are taken into account. Conversely, the underlying file systems or operating systems may be more restrictive @@ -138,13 +138,13 @@ and ``coqtop``, unless stated otherwise: disallow two files differing only in the case in the same directory. .. seealso:: Section :ref:`names-of-libraries`. -:-R *directory* dirpath: Do as -Q *directory* dirpath but make the +:-R *directory* *dirpath*: Do as ``-Q`` *directory* *dirpath* but make the subdirectory structure of *directory* recursively visible so that the recursive contents of physical *directory* is available from |Coq| using short or partially qualified names. .. seealso:: Section :ref:`names-of-libraries`. -:-top dirpath: Set the toplevel module name to dirpath instead of Top. +:-top *dirpath*: Set the toplevel module name to :n:`@dirpath` instead of ``Top``. Not valid for `coqc` as the toplevel module name is inferred from the name of the output file. :-exclude-dir *directory*: Exclude any subdirectory named *directory* @@ -164,10 +164,17 @@ and ``coqtop``, unless stated otherwise: :-lv *file*, -load-vernac-source-verbose *file*: Load and execute the |Coq| script from *file.v*. Write its contents to the standard output as it is executed. -:-load-vernac-object dirpath: Load |Coq| compiled library dirpath. This - is equivalent to runningRequire dirpath. -:-require dirpath: Load |Coq| compiled library dirpath and import it. - This is equivalent to running Require Import dirpath. +:-load-vernac-object *qualid*: Load |Coq| compiled library :n:`@qualid`. This + is equivalent to running :cmd:`Require` :n:`qualid`. +:-ri *qualid*, -require-import *qualid*: Load |Coq| compiled library :n:`@qualid` and import it. + This is equivalent to running :cmd:`Require Import` :n:`@qualid`. +:-re *qualid*, -require-export *qualid*: Load |Coq| compiled library :n:`@qualid` and transitively import it. + This is equivalent to running :cmd:`Require Export` :n:`@qualid`. +:-rifrom *dirpath* *qualid*, -require-import-from *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid` and import it. + This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Import` :n:`@qualid`. +:-refrom *dirpath* *qualid*, -require-export-from *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid` and transitively import it. + This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Export` :n:`@qualid`. +:-require *qualid*: Deprecated; use ``-ri`` *qualid*. :-batch: Exit just after argument parsing. Available for ``coqtop`` only. :-compile *file.v*: Deprecated; use ``coqc`` instead. Compile file *file.v* into *file.vo*. This option implies -batch (exit just after argument parsing). It is available only @@ -193,7 +200,7 @@ and ``coqtop``, unless stated otherwise: :-emacs, -ide-slave: Start a special toplevel to communicate with a specific IDE. :-impredicative-set: Change the logical theory of |Coq| by declaring the - sort Set impredicative. + sort :g:`Set` impredicative. .. warning:: diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 5f2e911ff9..36eeff6192 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -655,6 +655,8 @@ this features has the same semantics as in Ltac1. In particular, a ``reverse`` flag can be specified to match hypotheses from the more recently introduced to the least recently introduced one. +.. _ltac2_notations: + Notations --------- @@ -679,6 +681,11 @@ The following scopes are built-in. + parses :n:`c = @term` and produces :n:`constr:(c)` + This scope can be parameterized by a list of delimiting keys of interpretation + scopes (as described in :ref:`LocalInterpretationRulesForNotations`), + describing how to interpret the parsed term. For instance, :n:`constr(A, B)` + parses :n:`c = @term` and produces :n:`constr:(c%A%B)`. + - :n:`ident`: + parses :n:`id = @ident` and produces :n:`ident:(id)` diff --git a/engine/proofview.ml b/engine/proofview.ml index c00c90e5e9..d4f6fe3aef 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -373,32 +373,24 @@ let tclTRYFOCUS i j t = tclFOCUS ~nosuchgoal:(tclUNIT ()) i j t let tclFOCUSLIST ?(nosuchgoal=tclZERO (NoSuchGoals 0)) l t = let open Proof in Comb.get >>= fun comb -> - let n = CList.length comb in - (* First, remove empty intervals, and bound the intervals to the number - of goals. *) - let sanitize (i, j) = - if i > j then None - else if i > n then None - else if j < 1 then None - else Some ((max i 1), (min j n)) - in - let l = CList.map_filter sanitize l in + let n = CList.length comb in + let ok (i, j) = 1 <= i && i <= j && j <= n in + if not (CList.for_all ok l) then nosuchgoal + else match l with - | [] -> nosuchgoal - | (mi, _) :: _ -> - (* Get the left-most goal to focus. This goal won't move, and we - will then place all the other goals to focus to the right. *) - let mi = CList.fold_left (fun m (i, _) -> min m i) mi l in - (* [CList.goto] returns a zipper, so that - [(rev left) @ sub_right = comb]. *) - let left, sub_right = CList.goto (mi-1) comb in - let p x _ = CList.exists (fun (i, j) -> i <= x + mi && x + mi <= j) l in - let sub, right = CList.partitioni p sub_right in - let mj = mi - 1 + CList.length sub in - Comb.set (CList.rev_append left (sub @ right)) >> - tclFOCUS mi mj t - - + | [] -> nosuchgoal + | (mi, _) :: _ -> + (* Get the left-most goal to focus. This goal won't move, and we + will then place all the other goals to focus to the right. *) + let mi = CList.fold_left (fun m (i, _) -> min m i) mi l in + (* [CList.goto] returns a zipper, so that + [(rev left) @ sub_right = comb]. *) + let left, sub_right = CList.goto (mi-1) comb in + let p x _ = CList.exists (fun (i, j) -> i <= x + mi && x + mi <= j) l in + let sub, right = CList.partitioni p sub_right in + let mj = mi - 1 + CList.length sub in + Comb.set (CList.rev_append left (sub @ right)) >> + tclFOCUS mi mj t (** Like {!tclFOCUS} but selects a single goal by name. *) let tclFOCUSID ?(nosuchgoal=tclZERO (NoSuchGoals 1)) id t = diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 620efbafd6..1336e3e8bf 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -202,17 +202,21 @@ let lift_univs cb subst auctx0 = let subst, auctx = discharge_abstract_universe_context subst auctx0 auctx in subst, (Polymorphic auctx) -let cook_constr { Opaqueproof.modlist ; abstract } c = +let cook_constr { Opaqueproof.modlist ; abstract } (univs, c) = let cache = RefTable.create 13 in let abstract, usubst, abs_ctx = abstract in - (* For now the STM only handles deferred computation of monomorphic - constants. The API will need to be adapted when it's not the case - anymore. *) - let () = assert (AUContext.is_empty abs_ctx) in + let ainst = Instance.of_array (Array.init univs Level.var) in + let usubst = Instance.append usubst ainst in let expmod = expmod_constr_subst cache modlist usubst in let hyps = Context.Named.map expmod abstract in let hyps = abstract_context hyps in - abstract_constant_body (expmod c) hyps + let c = abstract_constant_body (expmod c) hyps in + univs + AUContext.size abs_ctx, c + +let cook_constr infos univs c = + let fold info (univs, c) = cook_constr info (univs, c) in + let (_, c) = List.fold_right fold infos (univs, c) in + c let cook_constant { from = cb; info } = let { Opaqueproof.modlist; abstract } = info in @@ -227,7 +231,7 @@ let cook_constant { from = cb; info } = | Undef _ as x -> x | Def cs -> Def (Mod_subst.from_val (map (Mod_subst.force_constr cs))) | OpaqueDef o -> - OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:map info o) + OpaqueDef (Opaqueproof.discharge_direct_opaque info o) | Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked") in let const_hyps = diff --git a/kernel/cooking.mli b/kernel/cooking.mli index abae3880d7..934b7c6b50 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -28,7 +28,7 @@ type 'opaque result = { } val cook_constant : recipe -> Opaqueproof.opaque result -val cook_constr : Opaqueproof.cooking_info -> constr -> constr +val cook_constr : Opaqueproof.cooking_info list -> int -> constr -> constr val cook_inductive : Opaqueproof.cooking_info -> mutual_inductive_body -> Entries.mutual_inductive_entry diff --git a/kernel/dune b/kernel/dune index 5b23a705ae..4038bf5638 100644 --- a/kernel/dune +++ b/kernel/dune @@ -3,7 +3,7 @@ (synopsis "The Coq Kernel") (public_name coq.kernel) (wrapped false) - (modules (:standard \ genOpcodeFiles uint63_x86 uint63_amd64 write_uint63)) + (modules (:standard \ genOpcodeFiles uint63_i386_31 uint63_amd64_63 write_uint63)) (libraries lib byterun dynlink)) (executable @@ -14,15 +14,10 @@ (targets copcodes.ml) (action (with-stdout-to %{targets} (run ./genOpcodeFiles.exe copml)))) -(executable - (name write_uint63) - (modules write_uint63) - (libraries unix)) - (rule (targets uint63.ml) - (deps (:gen ./write_uint63.exe) uint63_x86.ml uint63_amd64.ml) - (action (run %{gen}))) + (deps (:gen-file uint63_%{ocaml-config:architecture}_%{ocaml-config:int_size}.ml)) + (action (copy# %{gen-file} %{targets}))) (documentation (package coq)) diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 1971c67c61..e18b726111 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -16,19 +16,22 @@ open Mod_subst type work_list = (Instance.t * Id.t array) Cmap.t * (Instance.t * Id.t array) Mindmap.t +type cooking_info = { + modlist : work_list; + abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t } + type indirect_accessor = { access_proof : DirPath.t -> int -> constr option; + access_discharge : cooking_info list -> int -> constr -> constr; } -type cooking_info = { - modlist : work_list; - abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t } type proofterm = (constr * Univ.ContextSet.t) Future.computation +type universes = int type opaque = | Indirect of substitution list * DirPath.t * int (* subst, lib, index *) - | Direct of cooking_info list * proofterm + | Direct of universes * cooking_info list * proofterm type opaquetab = { - opaque_val : (cooking_info list * proofterm) Int.Map.t; + opaque_val : (int * cooking_info list * proofterm) Int.Map.t; (** Actual proof terms *) opaque_len : int; (** Size of the above map *) @@ -43,14 +46,14 @@ let empty_opaquetab = { let not_here () = CErrors.user_err Pp.(str "Cannot access opaque delayed proof") -let create cu = Direct ([],cu) +let create ~univs cu = Direct (univs, [],cu) let turn_indirect dp o tab = match o with | Indirect (_,_,i) -> if not (Int.Map.mem i tab.opaque_val) then CErrors.anomaly (Pp.str "Indirect in a different table.") else CErrors.anomaly (Pp.str "Already an indirect opaque.") - | Direct (d,cu) -> + | Direct (nunivs, d, cu) -> (* Invariant: direct opaques only exist inside sections, we turn them indirect as soon as we are at toplevel. At this moment, we perform hashconsing of their contents, potentially as a future. *) @@ -61,7 +64,7 @@ let turn_indirect dp o tab = match o with in let cu = Future.chain cu hcons in let id = tab.opaque_len in - let opaque_val = Int.Map.add id (d,cu) tab.opaque_val in + let opaque_val = Int.Map.add id (nunivs, d,cu) tab.opaque_val in let opaque_dir = if DirPath.equal dp tab.opaque_dir then tab.opaque_dir else if DirPath.equal tab.opaque_dir DirPath.initial then dp @@ -74,10 +77,10 @@ let subst_opaque sub = function | Indirect (s,dp,i) -> Indirect (sub::s,dp,i) | Direct _ -> CErrors.anomaly (Pp.str "Substituting a Direct opaque.") -let discharge_direct_opaque ~cook_constr ci = function +let discharge_direct_opaque ci = function | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") - | Direct (d,cu) -> - Direct (ci::d,Future.chain cu (fun (c, u) -> cook_constr c, u)) + | Direct (n, d, cu) -> + Direct (n, ci :: d, cu) let join except cu = match except with | None -> ignore (Future.join cu) @@ -86,54 +89,61 @@ let join except cu = match except with else ignore (Future.join cu) let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function - | Direct (_,cu) -> join except cu + | Direct (_,_,cu) -> join except cu | Indirect (_,dp,i) -> if DirPath.equal dp odp then - let fp = snd (Int.Map.find i prfs) in + let (_, _, fp) = Int.Map.find i prfs in join except fp let force_proof access { opaque_val = prfs; opaque_dir = odp; _ } = function - | Direct (_,cu) -> - fst(Future.force cu) + | Direct (n, d, cu) -> + let (c, _) = Future.force cu in + access.access_discharge d n c | Indirect (l,dp,i) -> - let pt = + let c = if DirPath.equal dp odp - then Future.chain (snd (Int.Map.find i prfs)) fst + then + let (n, d, cu) = Int.Map.find i prfs in + let (c, _) = Future.force cu in + access.access_discharge d n c else match access.access_proof dp i with | None -> not_here () - | Some v -> Future.from_val v + | Some v -> v in - let c = Future.force pt in force_constr (List.fold_right subst_substituted l (from_val c)) let force_constraints _access { opaque_val = prfs; opaque_dir = odp; _ } = function - | Direct (_,cu) -> snd(Future.force cu) + | Direct (_,_,cu) -> + snd(Future.force cu) | Indirect (_,dp,i) -> if DirPath.equal dp odp - then snd (Future.force (snd (Int.Map.find i prfs))) + then + let (_, _, cu) = Int.Map.find i prfs in + snd (Future.force cu) else Univ.ContextSet.empty let get_direct_constraints = function | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") -| Direct (_, cu) -> Future.chain cu snd +| Direct (_, _, cu) -> Future.chain cu snd module FMap = Future.UUIDMap let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _ } = - let opaque_table = Array.make n None in - let disch_table = Array.make n [] in + let opaque_table = Array.make n ([], 0, None) in let f2t_map = ref FMap.empty in - let iter n (d, cu) = + let iter n (univs, d, cu) = let uid = Future.uuid cu in let () = f2t_map := FMap.add (Future.uuid cu) n !f2t_map in - if Future.is_val cu then - let (c, _) = Future.force cu in - opaque_table.(n) <- Some c - else if Future.UUIDSet.mem uid except then - disch_table.(n) <- d - else - CErrors.anomaly - Pp.(str"Proof object "++int n++str" is not checked nor to be checked") + let c = + if Future.is_val cu then + let (c, _) = Future.force cu in + Some c + else if Future.UUIDSet.mem uid except then None + else + CErrors.anomaly + Pp.(str"Proof object "++int n++str" is not checked nor to be checked") + in + opaque_table.(n) <- (d, univs, c) in let () = Int.Map.iter iter otab in - opaque_table, disch_table, !f2t_map + opaque_table, !f2t_map diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 46b0500507..6e275649cd 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -28,15 +28,23 @@ type opaque val empty_opaquetab : opaquetab (** From a [proofterm] to some [opaque]. *) -val create : proofterm -> opaque +val create : univs:int -> proofterm -> opaque (** Turn a direct [opaque] into an indirect one. It is your responsibility to hashcons the inner term beforehand. The integer is an hint of the maximum id used so far *) val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab +type work_list = (Univ.Instance.t * Id.t array) Cmap.t * + (Univ.Instance.t * Id.t array) Mindmap.t + +type cooking_info = { + modlist : work_list; + abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t } + type indirect_accessor = { access_proof : DirPath.t -> int -> constr option; + access_discharge : cooking_info list -> int -> constr -> constr; } (** When stored indirectly, opaque terms are indexed by their library dirpath and an integer index. The two functions above activate @@ -51,23 +59,11 @@ val get_direct_constraints : opaque -> Univ.ContextSet.t Future.computation val subst_opaque : substitution -> opaque -> opaque -type work_list = (Univ.Instance.t * Id.t array) Cmap.t * - (Univ.Instance.t * Id.t array) Mindmap.t - -type cooking_info = { - modlist : work_list; - abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t } - -(* The type has two caveats: - 1) cook_constr is defined after - 2) we have to store the input in the [opaque] in order to be able to - discharge it when turning a .vi into a .vo *) val discharge_direct_opaque : - cook_constr:(constr -> constr) -> cooking_info -> opaque -> opaque + cooking_info -> opaque -> opaque val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit val dump : ?except:Future.UUIDSet.t -> opaquetab -> - Constr.t option array * - cooking_info list array * + (cooking_info list * int * Constr.t option) array * int Future.UUIDMap.t diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 9f7466902d..824400b4e3 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -231,7 +231,7 @@ let check_engagement env expected_impredicative_set = type side_effect = { from_env : Declarations.structure_body CEphemeron.key; seff_constant : Constant.t; - seff_body : (Constr.t * Univ.ContextSet.t) Declarations.constant_body; + seff_body : Constr.t Declarations.constant_body; seff_role : Entries.side_effect_role; } @@ -299,11 +299,6 @@ let concat_private = SideEffects.concat let universes_of_private eff = let fold acc eff = - let acc = match eff.seff_body.const_body with - | Def _ -> acc - | OpaqueDef (_, ctx) -> ctx :: acc - | Primitive _ | Undef _ -> assert false - in match eff.seff_body.const_universes with | Monomorphic ctx -> ctx :: acc | Polymorphic _ -> acc @@ -601,7 +596,7 @@ let inline_side_effects env body side_eff = let fold (subst, var, ctx, args) (c, cb) = let (b, opaque) = match cb.const_body with | Def b -> (Mod_subst.force_constr b, false) - | OpaqueDef (b, _) -> (b, true) + | OpaqueDef b -> (b, true) | _ -> assert false in match cb.const_universes with @@ -689,13 +684,13 @@ let constant_entry_of_side_effect eff = | Polymorphic auctx -> Polymorphic_entry (Univ.AUContext.names auctx, Univ.AUContext.repr auctx) in - let pt = + let p = match cb.const_body with - | OpaqueDef (b, c) -> b, c - | Def b -> Mod_subst.force_constr b, Univ.ContextSet.empty + | OpaqueDef b -> b + | Def b -> Mod_subst.force_constr b | _ -> assert false in DefinitionEntry { - const_entry_body = Future.from_val (pt, ()); + const_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ()); const_entry_secctx = None; const_entry_feedback = None; const_entry_type = Some cb.const_type; @@ -721,11 +716,6 @@ let export_side_effects mb env (b_ctx, eff) = match cb.const_universes with | Polymorphic _ -> env | Monomorphic ctx -> - let ctx = match eff.seff_body.const_body with - | Def _ -> ctx - | OpaqueDef (_, ctx') -> Univ.ContextSet.union ctx' ctx - | Undef _ | Primitive _ -> assert false - in Environ.push_context_set ~strict:true ctx env in let rec translate_seff sl seff acc env = @@ -737,7 +727,12 @@ let export_side_effects mb env (b_ctx, eff) = let kn = eff.seff_constant in let ce = constant_entry_of_side_effect eff in let cb = Term_typing.translate_constant Term_typing.Pure env kn ce in - let cb = map_constant Future.force cb in + let map cu = + let (c, u) = Future.force cu in + let () = assert (Univ.ContextSet.is_empty u) in + c + in + let cb = map_constant map cb in let eff = { eff with seff_body = cb } in (push_seff env eff, export_eff eff) in @@ -749,9 +744,13 @@ let export_side_effects mb env (b_ctx, eff) = in translate_seff trusted seff [] env +let n_univs cb = match cb.const_universes with +| Monomorphic _ -> 0 +| Polymorphic auctx -> Univ.AUContext.size auctx + let export_private_constants ~in_section ce senv = let exported, ce = export_side_effects senv.revstruct senv.env ce in - let map (kn, cb, _) = (kn, map_constant (fun p -> Opaqueproof.create (Future.from_val p)) cb) in + let map (kn, cb, _) = (kn, map_constant (fun p -> Opaqueproof.create ~univs:(n_univs cb) (Future.from_val (p, Univ.ContextSet.empty))) cb) in let bodies = List.map map exported in let exported = List.map (fun (kn, _, r) -> (kn, r)) exported in let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in @@ -778,7 +777,7 @@ let add_constant ?role ~in_section l decl senv = Term_typing.translate_constant Term_typing.Pure senv.env kn ce in let senv = - let cb = map_constant Opaqueproof.create cb in + let cb = map_constant (fun c -> Opaqueproof.create ~univs:(n_univs cb) c) cb in add_constant_aux ~in_section senv (kn, cb) in let senv = match decl with @@ -790,7 +789,20 @@ let add_constant ?role ~in_section l decl senv = let eff = match role with | None -> empty_private_constants | Some role -> - let cb = map_constant Future.force cb in + let body, univs = match cb.const_body with + | (Primitive _ | Undef _) -> assert false + | Def c -> (Def c, cb.const_universes) + | OpaqueDef o -> + let (b, ctx) = Future.force o in + match cb.const_universes with + | Monomorphic ctx' -> + OpaqueDef b, Monomorphic (Univ.ContextSet.union ctx ctx') + | Polymorphic auctx -> + (* Upper layers enforce that there are no internal constraints *) + let () = assert (Univ.ContextSet.is_empty ctx) in + OpaqueDef b, Polymorphic auctx + in + let cb = { cb with const_body = body; const_universes = univs } in let from_env = CEphemeron.create senv.revstruct in let eff = { from_env = from_env; diff --git a/kernel/uint63_amd64.ml b/kernel/uint63_amd64_63.ml index 2d4d685775..2d4d685775 100644 --- a/kernel/uint63_amd64.ml +++ b/kernel/uint63_amd64_63.ml diff --git a/kernel/uint63_x86.ml b/kernel/uint63_i386_31.ml index fa45c90241..fa45c90241 100644 --- a/kernel/uint63_x86.ml +++ b/kernel/uint63_i386_31.ml diff --git a/kernel/write_uint63.ml b/kernel/write_uint63.ml index beb59ce205..42bb5dfbb1 100644 --- a/kernel/write_uint63.ml +++ b/kernel/write_uint63.ml @@ -31,8 +31,8 @@ let ml_file_copy input output = let write_uint63 () = ml_file_copy - (if max_int = 1073741823 (* 32-bits *) then "uint63_x86.ml" - else (* 64 bits *) "uint63_amd64.ml") + (if max_int = 1073741823 (* 32-bits *) then "uint63_i386_31.ml" + else (* 64 bits *) "uint63_amd64_63.ml") "uint63.ml" let () = write_uint63 () diff --git a/library/library.ml b/library/library.ml index e3b8511af1..1ac75d2fdc 100644 --- a/library/library.ml +++ b/library/library.ml @@ -276,11 +276,11 @@ let in_import_library : DirPath.t list * bool -> obj = (** Delayed / available tables of opaque terms *) type 'a table_status = - | ToFetch of 'a option array delayed - | Fetched of 'a option array + | ToFetch of 'a array delayed + | Fetched of 'a array let opaque_tables = - ref (LibraryMap.empty : (Constr.constr table_status) LibraryMap.t) + ref (LibraryMap.empty : ((Opaqueproof.cooking_info list * int * Constr.constr option) table_status) LibraryMap.t) let add_opaque_table dp st = opaque_tables := LibraryMap.add dp st !opaque_tables @@ -306,10 +306,14 @@ let access_table what tables dp i = let access_opaque_table dp i = let what = "opaque proofs" in - access_table what opaque_tables dp i + let (info, n, c) = access_table what opaque_tables dp i in + match c with + | None -> None + | Some c -> Some (Cooking.cook_constr info n c) let indirect_accessor = { Opaqueproof.access_proof = access_opaque_table; + Opaqueproof.access_discharge = Cooking.cook_constr; } (************************************************************************) @@ -319,8 +323,7 @@ type seg_sum = summary_disk type seg_lib = library_disk type seg_univ = (* true = vivo, false = vi *) Univ.ContextSet.t * bool -type seg_discharge = Opaqueproof.cooking_info list array -type seg_proofs = Constr.constr option array +type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.t option) array let mk_library sd md digests univs = { @@ -344,7 +347,6 @@ let intern_from_file f = let ((lmd : seg_lib delayed), digest_lmd) = in_delayed f ch in let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in let _ = System.skip_in_segment f ch in - let _ = System.skip_in_segment f ch in let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch in close_in ch; register_library_filename lsd.md_name f; @@ -527,15 +529,13 @@ let load_library_todo f = let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in let (s2 : seg_univ option), _, _ = System.marshal_in_segment f ch in - let (s3 : seg_discharge option), _, _ = System.marshal_in_segment f ch in let tasks, _, _ = System.marshal_in_segment f ch in - let (s5 : seg_proofs), _, _ = System.marshal_in_segment f ch in + let (s4 : seg_proofs), _, _ = System.marshal_in_segment f ch in close_in ch; if tasks = None then user_err ~hdr:"restart" (str"not a .vio file"); if s2 = None then user_err ~hdr:"restart" (str"not a .vio file"); - if s3 = None then user_err ~hdr:"restart" (str"not a .vio file"); if snd (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file"); - s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5 + s0, s1, Option.get s2, Option.get tasks, s4 (************************************************************************) (*s [save_library dir] ends library [dir] and save it to the disk. *) @@ -578,10 +578,10 @@ let save_library_to ?todo ~output_native_objects dir f otab = List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e) Future.UUIDSet.empty l in let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in - let opaque_table, disch_table, f2t_map = Opaqueproof.dump ~except otab in - let tasks, utab, dtab = + let opaque_table, f2t_map = Opaqueproof.dump ~except otab in + let tasks, utab = match todo with - | None -> None, None, None + | None -> None, None | Some (tasks, rcbackup) -> let tasks = List.map Stateid.(fun (r,b) -> @@ -589,8 +589,8 @@ let save_library_to ?todo ~output_native_objects dir f otab = with Not_found -> assert b; { r with uuid = -1 }, b) tasks in Some (tasks,rcbackup), - Some (Univ.ContextSet.empty,false), - Some disch_table in + Some (Univ.ContextSet.empty,false) + in let sd = { md_name = dir; md_deps = Array.of_list (current_deps ()); @@ -610,7 +610,6 @@ let save_library_to ?todo ~output_native_objects dir f otab = System.marshal_out_segment f' ch (sd : seg_sum); System.marshal_out_segment f' ch (md : seg_lib); System.marshal_out_segment f' ch (utab : seg_univ option); - System.marshal_out_segment f' ch (dtab : seg_discharge option); System.marshal_out_segment f' ch (tasks : 'tasks option); System.marshal_out_segment f' ch (opaque_table : seg_proofs); close_out ch; @@ -630,7 +629,6 @@ let save_library_raw f sum lib univs proofs = System.marshal_out_segment f ch (sum : seg_sum); System.marshal_out_segment f ch (lib : seg_lib); System.marshal_out_segment f ch (Some univs : seg_univ option); - System.marshal_out_segment f ch (None : seg_discharge option); System.marshal_out_segment f ch (None : 'tasks option); System.marshal_out_segment f ch (proofs : seg_proofs); close_out ch diff --git a/library/library.mli b/library/library.mli index 142206e2c5..727eca10cf 100644 --- a/library/library.mli +++ b/library/library.mli @@ -35,8 +35,7 @@ type seg_sum type seg_lib type seg_univ = (* all_cst, finished? *) Univ.ContextSet.t * bool -type seg_discharge = Opaqueproof.cooking_info list array -type seg_proofs = Constr.constr option array +type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.t option) array (** Open a module (or a library); if the boolean is true then it's also an export otherwise just a simple import *) @@ -51,7 +50,7 @@ val save_library_to : val load_library_todo : CUnix.physical_path - -> seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs + -> seg_sum * seg_lib * seg_univ * 'tasks * seg_proofs val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 7b286e69dc..e0a31e7dba 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -946,9 +946,9 @@ let fold_match ?(force=false) env sigma c = if dep then case_dep_scheme_kind_from_prop else case_scheme_kind_from_prop else ( - if dep - then case_dep_scheme_kind_from_type_in_prop - else case_scheme_kind_from_type) + if dep + then case_dep_scheme_kind_from_type_in_prop + else case_scheme_kind_from_type) else ((* sortc <> InProp by typing *) if dep then case_dep_scheme_kind_from_type diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index dbb0f25abf..91905d277c 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -336,14 +336,14 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_ let sigma, p = (* The resulting goal *) Evarutil.new_evar env sigma (beta (EConstr.Vars.subst1 new_rdx pred)) in let pred = EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdx_ty pred in - let elim, gl = + let elim, gl = let ((kn, i) as ind, _), unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in let sort = elimination_sort_of_goal gl in let elim, gl = pf_fresh_global (Indrec.lookup_eliminator env ind sort) gl in if dir = R2L then elim, gl else (* taken from Coq's rewrite *) let elim, _ = destConst elim in let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical elim)) in - let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r") in + let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r") in let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make2 mp l')) in mkConst c1', gl in let elim = EConstr.of_constr elim in diff --git a/proofs/refine.ml b/proofs/refine.ml index 4a9404aa96..8439156e65 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -116,9 +116,6 @@ let lift c = let make_refine_enter ~typecheck f gl = generic_refine ~typecheck (lift f) gl -let refine_one ~typecheck f = - Proofview.Goal.enter_one (make_refine_enter ~typecheck f) - let refine ~typecheck f = let f evd = let (evd,c) = f evd in (evd,((), c)) diff --git a/proofs/refine.mli b/proofs/refine.mli index b8948a92f3..93fd9d7a64 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -27,9 +27,6 @@ val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> uni raised during the interpretation of [t] are caught and result in tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *) -val refine_one : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * ('a * EConstr.t)) -> 'a tactic -(** A variant of [refine] which assumes exactly one goal under focus *) - val generic_refine : typecheck:bool -> ('a * EConstr.t) tactic -> Proofview.Goal.t -> 'a tactic (** The general version of refine. *) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 799f4a380b..557f428be9 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -129,9 +129,6 @@ let tclTHENSLASTn tac1 tac taci = tclTHENS3PARTS tac1 [||] tac taci let tclTHEN_i tac taci gls = finish_tac (thensi_tac taci (then_tac tac (start_tac gls))) -let tclTHENLASTn tac1 taci = tclTHENSLASTn tac1 tclIDTAC taci -let tclTHENFIRSTn tac1 taci = tclTHENSFIRSTn tac1 taci tclIDTAC - (* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies [tac2] to every resulting subgoals *) let tclTHEN tac1 tac2 = tclTHENS3PARTS tac1 [||] tac2 [||] @@ -253,46 +250,9 @@ let rec tclFIRST = function | [] -> tclFAIL_s "No applicable tactic." | t::rest -> tclORELSE0 t (tclFIRST rest) -let ite_gen tcal tac_if continue tac_else gl= - let success=ref false in - let tac_if0 gl= - let result=tac_if gl in - success:=true;result in - let tac_else0 e gl= - if !success then - iraise e - else - try - tac_else gl - with - e' when CErrors.noncritical e' -> iraise e in - try - tcal tac_if0 continue gl - with (* Breakpoint *) - | e when CErrors.noncritical e -> - let e = CErrors.push e in catch_failerror e; tac_else0 e gl - -(* Try the first tactic and, if it succeeds, continue with - the second one, and if it fails, use the third one *) - -let tclIFTHENELSE=ite_gen tclTHEN - -(* Idem with tclTHENS and tclTHENSV *) - -let tclIFTHENSELSE=ite_gen tclTHENS - -let tclIFTHENSVELSE=ite_gen tclTHENSV - -let tclIFTHENTRYELSEMUST tac1 tac2 gl = - tclIFTHENELSE tac1 (tclTRY tac2) tac2 gl - (* Fails if a tactic did not solve the goal *) let tclCOMPLETE tac = tclTHEN tac (tclFAIL_s "Proof is not complete.") -(* Try the first that solves the current goal *) -let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl) - - (* Iteration tacticals *) let tclDO n t = @@ -311,22 +271,7 @@ let rec tclREPEAT t g = let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t)) -(* Repeat on the first subgoal (no failure if no more subgoal) *) -let rec tclREPEAT_MAIN t g = - (tclORELSE (tclTHEN_i t (fun i -> if Int.equal i 1 then (tclREPEAT_MAIN t) else - tclIDTAC)) tclIDTAC) g - (* Change evars *) let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma} - -let tclEVARUNIVCONTEXT ctx gls = tclIDTAC {gls with sigma= Evd.set_universe_context gls.sigma ctx} - -(* Push universe context *) -let tclPUSHCONTEXT rigid ctx tac gl = - tclTHEN (tclEVARS (Evd.merge_context_set rigid (project gl) ctx)) tac gl - let tclPUSHEVARUNIVCONTEXT ctx gl = tclEVARS (Evd.merge_universe_context (project gl) ctx) gl - -let tclPUSHCONSTRAINTS cst gl = - tclEVARS (Evd.add_constraints (project gl) cst) gl diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 52cbf7658b..0f34a79c49 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -32,12 +32,8 @@ val tclIDTAC_MESSAGE : Pp.t -> tactic (** [tclEVARS sigma] changes the current evar map *) val tclEVARS : evar_map -> tactic -val tclEVARUNIVCONTEXT : UState.t -> tactic - -val tclPUSHCONTEXT : Evd.rigid -> Univ.ContextSet.t -> tactic -> tactic val tclPUSHEVARUNIVCONTEXT : UState.t -> tactic -val tclPUSHCONSTRAINTS : Univ.Constraint.t -> tactic (** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies [tac2] to every resulting subgoals *) @@ -86,16 +82,6 @@ val tclTHENSLASTn : tactic -> tactic -> tactic array -> tactic [tac2] for the remaining last subgoals (previously called tclTHENST) *) val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic -(** [tclTHENLASTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then, - applies [t1],...,[tn] on the last [n] resulting subgoals and leaves - unchanged the other subgoals *) -val tclTHENLASTn : tactic -> tactic array -> tactic - -(** [tclTHENFIRSTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then, - applies [t1],...,[tn] on the first [n] resulting subgoals and leaves - unchanged the other subgoals (previously called [tclTHENSI]) *) -val tclTHENFIRSTn : tactic -> tactic array -> tactic - (** A special exception for levels for the Fail tactic *) exception FailError of int * Pp.t Lazy.t @@ -106,9 +92,7 @@ val catch_failerror : Exninfo.iexn -> unit val tclORELSE0 : tactic -> tactic -> tactic val tclORELSE : tactic -> tactic -> tactic val tclREPEAT : tactic -> tactic -val tclREPEAT_MAIN : tactic -> tactic val tclFIRST : tactic list -> tactic -val tclSOLVE : tactic list -> tactic val tclTRY : tactic -> tactic val tclTHENTRY : tactic -> tactic -> tactic val tclCOMPLETE : tactic -> tactic @@ -118,16 +102,3 @@ val tclFAIL_lazy : int -> Pp.t Lazy.t -> tactic val tclDO : int -> tactic -> tactic val tclPROGRESS : tactic -> tactic val tclSHOWHYPS : tactic -> tactic - -(** [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then, - if it succeeds, applies [tac2] to the resulting subgoals, - and if not applies [tac3] to the initial goal [gls] *) -val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic -val tclIFTHENSELSE : tactic -> tactic list -> tactic ->tactic -val tclIFTHENSVELSE : tactic -> tactic array -> tactic ->tactic - -(** [tclIFTHENTRYELSEMUST tac1 tac2 gls] applies [tac1] then [tac2]. If [tac1] - has been successful, then [tac2] may fail. Otherwise, [tac2] must succeed. - Equivalent to [(tac1;try tac2)||tac2] *) - -val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 93031c2202..d7b4f729cb 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -81,12 +81,10 @@ let pf_type_of = pf_reduce type_of let pf_get_type_of = pf_reduce Retyping.get_type_of let pf_conv_x gl = pf_reduce test_conversion gl Reduction.CONV -let pf_conv_x_leq gl = pf_reduce test_conversion gl Reduction.CUMUL let pf_const_value = pf_reduce (fun env _ c -> EConstr.of_constr (constant_value_in env c)) let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind - let pf_hnf_type_of gls = pf_get_type_of gls %> pf_whd_all gls (* Pretty-printers *) @@ -181,14 +179,7 @@ module New = struct let pf_hnf_type_of gl t = pf_whd_all gl (pf_get_type_of gl t) - let pf_whd_all gl t = pf_apply whd_all gl t let pf_compute gl t = pf_apply compute gl t let pf_nf_evar gl t = nf_evar (project gl) t - - let pf_undefined_evars gl = - let sigma = Proofview.Goal.sigma gl in - let ev = Proofview.Goal.goal gl in - let evi = Evd.find sigma ev in - Evarutil.filtered_undefined_evars_of_evar_info sigma evi end diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 23e1e6f566..195be04986 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -64,7 +64,6 @@ val pf_unfoldn : (occurrences * evaluable_global_reference) list val pf_const_value : Goal.goal sigma -> pconstant -> constr val pf_conv_x : Goal.goal sigma -> constr -> constr -> bool -val pf_conv_x_leq : Goal.goal sigma -> constr -> constr -> bool (** {6 Pretty-printing functions (debug only). } *) val pr_gls : Goal.goal sigma -> Pp.t @@ -109,11 +108,8 @@ module New : sig val pf_hnf_constr : Proofview.Goal.t -> constr -> types val pf_hnf_type_of : Proofview.Goal.t -> constr -> types - val pf_whd_all : Proofview.Goal.t -> constr -> constr val pf_compute : Proofview.Goal.t -> constr -> constr val pf_nf_evar : Proofview.Goal.t -> constr -> constr - (** Gathers the undefined evars of the given goal. *) - val pf_undefined_evars : Proofview.Goal.t -> Evar.Set.t end diff --git a/stm/stm.ml b/stm/stm.ml index 0efea0b8e0..5baa6ce251 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1639,7 +1639,7 @@ and Slaves : sig val info_tasks : 'a tasks -> (string * float * int) list val finish_task : string -> - Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs -> + Library.seg_univ -> Library.seg_proofs -> int tasks -> int -> Library.seg_univ val cancel_worker : WorkerPool.worker_id -> unit @@ -1724,7 +1724,7 @@ end = struct (* {{{ *) str (Printexc.to_string e))); if drop then `ERROR_ADMITTED else `ERROR - let finish_task name (cst,_) d p l i = + let finish_task name (cst,_) p l i = let { Stateid.uuid = bucket }, drop = List.nth l i in let bucket_name = if bucket < 0 then (assert drop; ", no bucket") @@ -1734,7 +1734,6 @@ end = struct (* {{{ *) | `ERROR_ADMITTED -> cst, false | `OK_ADMITTED -> cst, false | `OK (po,_) -> - let discharge c = List.fold_right Cooking.cook_constr d.(bucket) c in let con = Nametab.locate_constant (Libnames.qualid_of_ident po.Proof_global.id) in @@ -1746,12 +1745,14 @@ end = struct (* {{{ *) the call to [check_task_aux] above. *) let uc = Opaqueproof.force_constraints Library.indirect_accessor (Global.opaque_tables ()) o in let uc = Univ.hcons_universe_context_set uc in + let (pr, ctx) = Option.get (Global.body_of_constant_body Library.indirect_accessor c) in (* We only manipulate monomorphic terms here. *) - let map (c, ctx) = assert (Univ.AUContext.is_empty ctx); c in - let pr = map (Option.get (Global.body_of_constant_body Library.indirect_accessor c)) in - let pr = discharge pr in + let () = assert (Univ.AUContext.is_empty ctx) in let pr = Constr.hcons pr in - p.(bucket) <- Some pr; + let (ci, univs, dummy) = p.(bucket) in + let () = assert (Option.is_empty dummy) in + let () = assert (Int.equal (Univ.AUContext.size ctx) univs) in + p.(bucket) <- ci, univs, Some pr; Univ.ContextSet.union cst uc, false let check_task name l i = @@ -2747,11 +2748,11 @@ let check_task name (tasks,rcbackup) i = with e when CErrors.noncritical e -> VCS.restore vcs; false let info_tasks (tasks,_) = Slaves.info_tasks tasks -let finish_tasks name u d p (t,rcbackup as tasks) = +let finish_tasks name u p (t,rcbackup as tasks) = RemoteCounter.restore rcbackup; let finish_task u (_,_,i) = let vcs = VCS.backup () in - let u = State.purify (Slaves.finish_task name u d p t) i in + let u = State.purify (Slaves.finish_task name u p t) i in VCS.restore vcs; u in try diff --git a/stm/stm.mli b/stm/stm.mli index 5e1e9bf5ad..86e2566539 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -167,7 +167,7 @@ type tasks val check_task : string -> tasks -> int -> bool val info_tasks : tasks -> (string * float * int) list val finish_tasks : string -> - Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs -> + Library.seg_univ -> Library.seg_proofs -> tasks -> Library.seg_univ * Library.seg_proofs (* Id of the tip of the current branch *) diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml index 0f78e0acf6..cf0c8934b0 100644 --- a/stm/vio_checking.ml +++ b/stm/vio_checking.ml @@ -12,7 +12,7 @@ open Util let check_vio (ts,f_in) = Dumpglob.noglob (); - let _, _, _, _, tasks, _ = Library.load_library_todo f_in in + let _, _, _, tasks, _ = Library.load_library_todo f_in in Stm.set_compilation_hints f_in; List.fold_left (fun acc ids -> Stm.check_task f_in tasks ids && acc) true ts @@ -29,7 +29,7 @@ let schedule_vio_checking j fs = if j < 1 then CErrors.user_err Pp.(str "The number of workers must be bigger than 0"); let jobs = ref [] in List.iter (fun long_f_dot_vio -> - let _,_,_,_, tasks, _ = Library.load_library_todo long_f_dot_vio in + let _,_,_, tasks, _ = Library.load_library_todo long_f_dot_vio in Stm.set_compilation_hints long_f_dot_vio; let infos = Stm.info_tasks tasks in let eta = List.fold_left (fun a (_,t,_) -> a +. t) 0.0 infos in diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 1170c1acd0..8ead050262 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -59,7 +59,7 @@ let build_induction_scheme_in_type dep sort ind = let sigma, pind = Evd.fresh_inductive_instance env sigma ind in let sigma, c = build_induction_scheme env sigma pind dep sort in c, Evd.evar_universe_context sigma - + let rect_scheme_kind_from_type = declare_individual_scheme_object "_rect_nodep" (fun _ x -> build_induction_scheme_in_type false InType x, Safe_typing.empty_private_constants) @@ -108,6 +108,16 @@ let sind_scheme_kind_from_prop = declare_individual_scheme_object "_sind" ~aux:"_sind_from_prop" (fun _ x -> build_induction_scheme_in_type false InSProp x, Safe_typing.empty_private_constants) +let nondep_elim_scheme from_kind to_kind = + match from_kind, to_kind with + | InProp, InProp -> ind_scheme_kind_from_prop + | InProp, InSProp -> sind_scheme_kind_from_prop + | InProp, InSet -> rec_scheme_kind_from_prop + | InProp, InType -> rect_scheme_kind_from_prop + | _ , InProp -> ind_scheme_kind_from_type + | _ , InSProp -> sind_scheme_kind_from_type + | _ , InSet -> rec_scheme_kind_from_type + | _ , InType -> rect_scheme_kind_from_type (* Case analysis *) diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli index 4472792449..f60e6c137a 100644 --- a/tactics/elimschemes.mli +++ b/tactics/elimschemes.mli @@ -33,6 +33,7 @@ val sind_dep_scheme_kind_from_type : individual scheme_kind val rec_scheme_kind_from_type : individual scheme_kind val rec_dep_scheme_kind_from_type : individual scheme_kind +val nondep_elim_scheme : Sorts.family -> Sorts.family -> individual scheme_kind (** Case analysis schemes *) diff --git a/tactics/equality.ml b/tactics/equality.ml index 51eee2a053..ec0876110b 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -352,35 +352,35 @@ let find_elim hdcncl lft2rgt dep cls ot = (is_global_exists "core.JMeq.type" hdcncl && jmeq_same_dom env sigma ot)) && not dep then - let c = + let c = match EConstr.kind sigma hdcncl with - | Ind (ind_sp,u) -> - let pr1 = + | Ind (ind_sp,u) -> + let pr1 = lookup_eliminator env ind_sp (elimination_sort_of_clause cls gl) - in + in begin match lft2rgt, cls with | Some true, None | Some false, Some _ -> - let c1 = destConstRef pr1 in + let c1 = destConstRef pr1 in let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical c1)) in - let l' = Label.of_id (add_suffix (Label.to_id l) "_r") in + let l' = Label.of_id (add_suffix (Label.to_id l) "_r") in let c1' = Global.constant_of_delta_kn (KerName.make mp l') in - begin - try - let _ = Global.lookup_constant c1' in - c1' - with Not_found -> + begin + try + let _ = Global.lookup_constant c1' in + c1' + with Not_found -> user_err ~hdr:"Equality.find_elim" (str "Cannot find rewrite principle " ++ Label.print l' ++ str ".") end - | _ -> destConstRef pr1 + | _ -> destConstRef pr1 end | _ -> (* cannot occur since we checked that we are in presence of Logic.eq or Jmeq just before *) assert false in - pf_constr_of_global (ConstRef c) + pf_constr_of_global (ConstRef c) else let scheme_name = match dep, lft2rgt, inccl with (* Non dependent case *) @@ -946,12 +946,12 @@ let build_coq_I () = pf_constr_of_global (lib_ref "core.True.I") let rec build_discriminator env sigma true_0 false_0 dirn c = function | [] -> let ind = get_type_of env sigma c in - build_selector env sigma dirn c ind true_0 false_0 + build_selector env sigma dirn c ind true_0 (fst false_0) | ((sp,cnum),argnum)::l -> let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in let newc = mkRel(cnum_nlams-argnum) in let subval = build_discriminator cnum_env sigma true_0 false_0 dirn newc l in - kont sigma subval (false_0,mkProp) + kont sigma subval false_0 (* Note: discrimination could be more clever: if some elimination is not allowed because of a large impredicative constructor in the @@ -983,25 +983,22 @@ let gen_absurdity id = absurd_term=False *) -let ind_scheme_of_eq lbeq = +let ind_scheme_of_eq lbeq to_kind = let (mib,mip) = Global.lookup_inductive (destIndRef lbeq.eq) in - let kind = inductive_sort_family mip in + let from_kind = inductive_sort_family mip in (* use ind rather than case by compatibility *) - let kind = - if kind == InProp then Elimschemes.ind_scheme_kind_from_prop - else Elimschemes.ind_scheme_kind_from_type in + let kind = Elimschemes.nondep_elim_scheme from_kind to_kind in let c, eff = find_scheme kind (destIndRef lbeq.eq) in ConstRef c, eff -let discrimination_pf e (t,t1,t2) discriminator lbeq = +let discrimination_pf e (t,t1,t2) discriminator lbeq to_kind = build_coq_I () >>= fun i -> - build_coq_False () >>= fun absurd_term -> - let eq_elim, eff = ind_scheme_of_eq lbeq in + let eq_elim, eff = ind_scheme_of_eq lbeq to_kind in Proofview.tclEFFECTS eff <*> pf_constr_of_global eq_elim >>= fun eq_elim -> Proofview.tclUNIT - (applist (eq_elim, [t;t1;mkNamedLambda (make_annot e Sorts.Relevant) t discriminator;i;t2]), absurd_term) + (applist (eq_elim, [t;t1;mkNamedLambda (make_annot e Sorts.Relevant) t discriminator;i;t2])) let eq_baseid = Id.of_string "e" @@ -1018,21 +1015,23 @@ let apply_on_clause (f,t) clause = let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = build_coq_True () >>= fun true_0 -> build_coq_False () >>= fun false_0 -> + let false_ty = Retyping.get_type_of env sigma false_0 in + let false_kind = Retyping.get_sort_family_of env sigma false_0 in let e = next_ident_away eq_baseid (vars_of_env env) in let e_env = push_named (Context.Named.Declaration.LocalAssum (make_annot e Sorts.Relevant,t)) env in let discriminator = try Proofview.tclUNIT - (build_discriminator e_env sigma true_0 false_0 dirn (mkVar e) cpath) + (build_discriminator e_env sigma true_0 (false_0,false_ty) dirn (mkVar e) cpath) with UserError _ as ex -> Proofview.tclZERO ex in discriminator >>= fun discriminator -> - discrimination_pf e (t,t1,t2) discriminator lbeq >>= fun (pf, absurd_term) -> - let pf_ty = mkArrow eqn Sorts.Relevant absurd_term in + discrimination_pf e (t,t1,t2) discriminator lbeq false_kind >>= fun pf -> + let pf_ty = mkArrow eqn Sorts.Relevant false_0 in let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in let pf = Clenvtac.clenv_value_cast_meta absurd_clause in - tclTHENS (assert_after Anonymous absurd_term) + tclTHENS (assert_after Anonymous false_0) [onLastHypId gen_absurdity; (Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf)))] let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 59fd8b37d6..81700986ea 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -43,12 +43,8 @@ let tclTHENS = Refiner.tclTHENS let tclTHENSV = Refiner.tclTHENSV let tclTHENSFIRSTn = Refiner.tclTHENSFIRSTn let tclTHENSLASTn = Refiner.tclTHENSLASTn -let tclTHENFIRSTn = Refiner.tclTHENFIRSTn -let tclTHENLASTn = Refiner.tclTHENLASTn let tclREPEAT = Refiner.tclREPEAT -let tclREPEAT_MAIN = Refiner.tclREPEAT_MAIN let tclFIRST = Refiner.tclFIRST -let tclSOLVE = Refiner.tclSOLVE let tclTRY = Refiner.tclTRY let tclCOMPLETE = Refiner.tclCOMPLETE let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE @@ -58,10 +54,6 @@ let tclDO = Refiner.tclDO let tclPROGRESS = Refiner.tclPROGRESS let tclSHOWHYPS = Refiner.tclSHOWHYPS let tclTHENTRY = Refiner.tclTHENTRY -let tclIFTHENELSE = Refiner.tclIFTHENELSE -let tclIFTHENSELSE = Refiner.tclIFTHENSELSE -let tclIFTHENSVELSE = Refiner.tclIFTHENSVELSE -let tclIFTHENTRYELSEMUST = Refiner.tclIFTHENTRYELSEMUST (************************************************************************) (* Tacticals applying on hypotheses *) diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 201b7801c3..a9ccda527f 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -31,13 +31,9 @@ val tclTHENLAST : tactic -> tactic -> tactic val tclTHENS : tactic -> tactic list -> tactic val tclTHENSV : tactic -> tactic array -> tactic val tclTHENSLASTn : tactic -> tactic -> tactic array -> tactic -val tclTHENLASTn : tactic -> tactic array -> tactic val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic -val tclTHENFIRSTn : tactic -> tactic array -> tactic val tclREPEAT : tactic -> tactic -val tclREPEAT_MAIN : tactic -> tactic val tclFIRST : tactic list -> tactic -val tclSOLVE : tactic list -> tactic val tclTRY : tactic -> tactic val tclCOMPLETE : tactic -> tactic val tclAT_LEAST_ONCE : tactic -> tactic @@ -49,11 +45,6 @@ val tclSHOWHYPS : tactic -> tactic val tclTHENTRY : tactic -> tactic -> tactic val tclMAP : ('a -> tactic) -> 'a list -> tactic -val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic -val tclIFTHENSELSE : tactic -> tactic list -> tactic -> tactic -val tclIFTHENSVELSE : tactic -> tactic array -> tactic -> tactic -val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic - (** {6 Tacticals applying to hypotheses } *) val onNthHypId : int -> (Id.t -> tactic) -> tactic diff --git a/test-suite/ltac2/notations.v b/test-suite/ltac2/notations.v new file mode 100644 index 0000000000..3d2a875e38 --- /dev/null +++ b/test-suite/ltac2/notations.v @@ -0,0 +1,24 @@ +From Ltac2 Require Import Ltac2. +From Coq Require Import ZArith String List. + +Open Scope Z_scope. + +Check 1 + 1 : Z. + +Ltac2 Notation "ex" arg(constr(nat,Z)) := arg. + +Check (1 + 1)%nat%Z = 1%nat. + +Lemma two : nat. + refine (ex (1 + 1)). +Qed. + +Import ListNotations. +Close Scope list_scope. + +Ltac2 Notation "sl" arg(constr(string,list)) := arg. + +Lemma maybe : list bool. +Proof. + refine (sl ["left" =? "right"]). +Qed. diff --git a/test-suite/success/Discriminate_HoTT.v b/test-suite/success/Discriminate_HoTT.v new file mode 100644 index 0000000000..2a5e083d56 --- /dev/null +++ b/test-suite/success/Discriminate_HoTT.v @@ -0,0 +1,89 @@ +(* -*- mode: coq; coq-prog-args: ("-noinit" "-indices-matter") -*- *) + +(* This file tests the discriminate tactic compatibility with HoTT. + The first part of the file will setup a mini HoTT environment. + Afterwards a number of tests are performed. The tests are basically + copied from the Discriminate.v test file. *) + +Unset Elimination Schemes. + +Set Universe Polymorphism. + +Declare ML Module "ltac_plugin". + +Global Set Default Proof Mode "Classic". + +Notation "x -> y" := (forall (_:x), y) (at level 99, right associativity, y at level 200). + +Cumulative Variant paths {A} (a:A) : A -> Type + := idpath : paths a a. + +Arguments idpath {A a} , [A] a. + +Scheme paths_ind := Induction for paths Sort Type. +Arguments paths_ind [A] a P f y p. + +Notation "x = y :> A" := (@paths A x y) (at level 70, y at next level, no associativity). +Notation "x = y" := (x = y :>_) (at level 70, no associativity). + +Register paths as core.identity.type. +Register idpath as core.identity.refl. +Register paths_ind as core.identity.ind. + +Definition inverse {A : Type} {x y : A} (p : x = y) : y = x + := match p with idpath => idpath end. +Arguments inverse {A x y} p : simpl nomatch. +Register inverse as core.identity.sym. + +Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := + match p, q with idpath, idpath => idpath end. +Arguments concat {A x y z} p q : simpl nomatch. +Register concat as core.identity.trans. + +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y + := match p with idpath => idpath end. +Arguments ap {A B} f {x y} p. +Register ap as core.identity.congr. + +Variant Empty : Type :=. + +Register Empty as core.False.type. + +Variant Unit : Type := tt. + +Register Unit as core.True.type. +Register tt as core.True.I. + +Variant Bool : Type := true | false. + +Inductive nat : Type := O | S (n:nat). + +(*********** Test discriminate tactic below. ***************) + +Goal O = S O -> Empty. + discriminate 1. +Qed. + +Goal forall H : O = S O, H = H. + discriminate H. +Qed. + +Goal O = S O -> Unit. +intros. discriminate H. Qed. +Goal O = S O -> Unit. +intros. Ltac g x := discriminate x. g H. Qed. + +Goal (forall x y : nat, x = y -> x = S y) -> Unit. +intros. +try discriminate (H O) || exact tt. +Qed. + +Goal (forall x y : nat, x = y -> x = S y) -> Unit. +intros. ediscriminate (H O). instantiate (1:=O). Abort. + +(* Check discriminate on types with local definitions *) + +Inductive A := B (T := Unit) (x y : Bool) (z := x). +Goal forall x y, B x true = B y false -> Empty. +discriminate. +Qed. diff --git a/test-suite/success/goal_selector.v b/test-suite/success/goal_selector.v index 0951c5c8d4..ae834e7696 100644 --- a/test-suite/success/goal_selector.v +++ b/test-suite/success/goal_selector.v @@ -13,13 +13,15 @@ Goal two false /\ two true /\ two false /\ two true /\ two true /\ two true. Proof. do 2 dup. - repeat split. - 2, 4-99, 100-3:idtac. + Fail 7:idtac. + Fail 2-1:idtac. + 1,2,4-6:idtac. 2-5:exact One. par:exact Zero. - repeat split. 3-6:swap 1 4. 1-5:swap 1 5. - 0-4:exact One. + 1-4:exact One. all:exact Zero. - repeat split. 1, 3:exact Zero. @@ -34,7 +36,7 @@ Qed. Goal True -> True. Proof. - intros y; only 1-2 : repeat idtac. + intros y. 1-1:match goal with y : _ |- _ => let x := y in idtac x end. Fail 1-1:let x := y in idtac x. 1:let x := y in idtac x. diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml index 6ddc503542..b5d1e01630 100644 --- a/tools/coq_dune.ml +++ b/tools/coq_dune.ml @@ -128,6 +128,7 @@ module Options = struct [ { enabled = false; cmd = "-debug"; } ; { enabled = false; cmd = "-native_compiler"; } ; { enabled = true; cmd = "-allow-sprop"; } + ; { enabled = true; cmd = "-w +default"; } ] let build_coq_flags () = diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index 7748134146..2e25066897 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -176,9 +176,9 @@ let compile opts copts ~echo ~f_in ~f_out = Dumpglob.noglob (); let long_f_dot_vio, long_f_dot_vo = ensure_exists_with_prefix f_in f_out ".vio" ".vo" in - let sum, lib, univs, disch, tasks, proofs = + let sum, lib, univs, tasks, proofs = Library.load_library_todo long_f_dot_vio in - let univs, proofs = Stm.finish_tasks long_f_dot_vo univs disch proofs tasks in + let univs, proofs = Stm.finish_tasks long_f_dot_vo univs proofs tasks in Library.save_library_raw long_f_dot_vo sum lib univs proofs let compile opts copts ~echo ~f_in ~f_out = diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 4ef31c73b7..9180cae389 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -184,6 +184,10 @@ let warn_deprecated_inputstate = CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.") +let warn_deprecated_simple_require = + CWarnings.create ~name:"deprecated-boot" ~category:"deprecated" + (fun () -> Pp.strbrk "The -require option is deprecated, please use -require-import instead.") + let set_inputstate opts s = warn_deprecated_inputstate (); { opts with inputstate = Some s } @@ -416,7 +420,22 @@ let parse_args ~help ~init arglist : t * string list = Flags.profile_ltac_cutoff := get_float opt (next ()); oval - |"-require" -> add_vo_require oval (next ()) None (Some false) + |"-rfrom" -> + let from = next () in add_vo_require oval (next ()) (Some from) None + + |"-require" -> + warn_deprecated_simple_require (); + add_vo_require oval (next ()) None (Some false) + + |"-require-import" | "-ri" -> add_vo_require oval (next ()) None (Some false) + + |"-require-export" | "-re" -> add_vo_require oval (next ()) None (Some true) + + |"-require-import-from" | "-rifrom" -> + let from = next () in add_vo_require oval (next ()) (Some from) (Some false) + + |"-require-export-from" | "-refrom" -> + let from = next () in add_vo_require oval (next ()) (Some from) (Some true) |"-top" -> let topname = Libnames.dirpath_of_string (next ()) in diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 29948d50b2..84d3992f5c 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -44,10 +44,23 @@ let print_usage_common co command = \n -load-ml-source f load ML file f\ \n -load-vernac-source f load Coq file f.v (Load \"f\".)\ \n -l f (idem)\ -\n -require path load Coq library path and import it (Require Import path.)\ \n -load-vernac-source-verbose f load Coq file f.v (Load Verbose \"f\".)\ \n -lv f (idem)\ -\n -load-vernac-object path load Coq library path (Require path)\ +\n -load-vernac-object lib, -r lib\ +\n load Coq library lib (Require lib)\ +\n -rfrom root lib load Coq library lib (From root Require lib.)\ +\n -require-import lib, -ri lib\ +\n load and import Coq library lib\ +\n (equivalent to Require Import lib.)\ +\n -require-export lib, -re lib\ +\n load and transitively import Coq library lib\ +\n (equivalent to Require Export lib.)\ +\n -require-import-from root lib, -rifrom lib\ +\n load and import Coq library lib\ +\n (equivalent to From root Require Import lib.)\ +\n -require-export-from root lib, -refrom lib\ +\n load and transitively import Coq library lib\ +\n (equivalent to From root Require Export lib.)\ \n\ \n -where print Coq's standard library location and exit\ \n -config, --config print Coq's configuration information and exit\ diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index da8600109e..e2bab96e20 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -1355,6 +1355,16 @@ let () = add_scope "thunk" begin function | arg -> scope_fail "thunk" arg end +let () = add_scope "constr" (fun arg -> + let delimiters = List.map (function + | SexprRec (_, { v = Some s }, []) -> s + | _ -> scope_fail "constr" arg) + arg + in + let act e = Tac2quote.of_constr ~delimiters e in + Tac2entries.ScopeRule (Extend.Aentry Pcoq.Constr.constr, act) + ) + let add_expr_scope name entry f = add_scope name begin function | [] -> Tac2entries.ScopeRule (Extend.Aentry entry, f) @@ -1382,7 +1392,6 @@ let () = add_expr_scope "assert" q_assert Tac2quote.of_assertion let () = add_expr_scope "constr_matching" q_constr_matching Tac2quote.of_constr_matching let () = add_expr_scope "goal_matching" q_goal_matching Tac2quote.of_goal_matching -let () = add_generic_scope "constr" Pcoq.Constr.constr Tac2quote.wit_constr let () = add_generic_scope "open_constr" Pcoq.Constr.constr Tac2quote.wit_open_constr let () = add_generic_scope "pattern" Pcoq.Constr.constr Tac2quote.wit_pattern diff --git a/user-contrib/Ltac2/tac2quote.ml b/user-contrib/Ltac2/tac2quote.ml index a98264745e..81442c9d6b 100644 --- a/user-contrib/Ltac2/tac2quote.ml +++ b/user-contrib/Ltac2/tac2quote.ml @@ -94,8 +94,14 @@ let of_anti f = function let of_ident {loc;v=id} = inj_wit ?loc wit_ident id -let of_constr c = +let of_constr ?delimiters c = let loc = Constrexpr_ops.constr_loc c in + let c = Option.cata + (List.fold_left (fun c d -> + CAst.make ?loc @@ Constrexpr.CDelimiters(Id.to_string d, c)) + c) + c delimiters + in inj_wit ?loc wit_constr c let of_open_constr c = diff --git a/user-contrib/Ltac2/tac2quote.mli b/user-contrib/Ltac2/tac2quote.mli index 1b03dad8ec..1c859063aa 100644 --- a/user-contrib/Ltac2/tac2quote.mli +++ b/user-contrib/Ltac2/tac2quote.mli @@ -32,7 +32,7 @@ val of_variable : Id.t CAst.t -> raw_tacexpr val of_ident : Id.t CAst.t -> raw_tacexpr -val of_constr : Constrexpr.constr_expr -> raw_tacexpr +val of_constr : ?delimiters:Id.t list -> Constrexpr.constr_expr -> raw_tacexpr val of_open_constr : Constrexpr.constr_expr -> raw_tacexpr diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index af13c873e2..8668f01053 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2694,7 +2694,7 @@ let rec interp_expr ?proof ~atts ~st c = [vernac_load] is mutually-recursive with [interp_expr] *) | VernacLoad (verbosely,fname) -> unsupported_attributes atts; - vernac_load ?proof ~verbosely ~st fname + vernac_load ~verbosely ~st fname (* Special: ?proof parameter doesn't allow for uniform pstate pop :S *) | VernacEndProof e -> @@ -2711,7 +2711,7 @@ let rec interp_expr ?proof ~atts ~st c = the way the proof mode is set there makes the task non trivial without a considerable amount of refactoring. *) -and vernac_load ?proof ~verbosely ~st fname = +and vernac_load ~verbosely ~st fname = let pstate = st.Vernacstate.proof in if there_are_pending_proofs ~pstate then CErrors.user_err Pp.(str "Load is not supported inside proofs."); @@ -2734,7 +2734,7 @@ and vernac_load ?proof ~verbosely ~st fname = try let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) pstate in let pstate = - v_mod (interp_control ?proof ~st:{ st with Vernacstate.proof = pstate }) + v_mod (interp_control ?proof:None ~st:{ st with Vernacstate.proof = pstate }) (parse_sentence proof_mode input) in load_loop ~pstate with |