diff options
67 files changed, 808 insertions, 617 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 536bd0af76..1be10f91d0 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -244,6 +244,9 @@ build:base+32bit: variables: OPAM_VARIANT: "+32bit" COQ_EXTRA_CONF: "-native-compiler yes" + only: &full-ci + variables: + - $FULL_CI == "true" build:edge+flambda: extends: .build-template @@ -317,6 +320,7 @@ pkg:opam: COQ_VERSION: "8.10" OPAM_SWITCH: "edge" OPAM_VARIANT: "+flambda" + only: *full-ci .nix-template: image: nixorg/nix:latest # Minimal NixOS image which doesn't even contain git @@ -448,6 +452,7 @@ test-suite:base+32bit: - build:base+32bit variables: OPAM_VARIANT: "+32bit" + only: *full-ci test-suite:edge+flambda: extends: .test-suite-template @@ -456,6 +461,7 @@ test-suite:edge+flambda: variables: OPAM_SWITCH: edge OPAM_VARIANT: "+flambda" + only: *full-ci test-suite:egde:dune:dev: stage: test @@ -498,6 +504,7 @@ test-suite:edge+trunk+make: - test-suite/logs expire_in: 1 week allow_failure: true + only: *full-ci test-suite:edge+trunk+dune: stage: test @@ -526,6 +533,7 @@ test-suite:edge+trunk+dune: - _build/default/test-suite/logs expire_in: 1 week allow_failure: true + only: *full-ci test-suite:base+async: extends: .test-suite-template @@ -550,6 +558,7 @@ validate:base+32bit: - build:base+32bit variables: OPAM_VARIANT: "+32bit" + only: *full-ci validate:edge+flambda: extends: .validate-template @@ -558,6 +567,7 @@ validate:edge+flambda: variables: OPAM_SWITCH: edge OPAM_VARIANT: "+flambda" + only: *full-ci validate:quick: extends: .validate-template diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index e811c116b6..f0e17909c1 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -169,7 +169,7 @@ People are generally happy to help and very reactive. ["Watching" this repository](https://github.com/coq/coq/subscription) can result in a very large number of notifications. We advise that if -you do, either [confifure your mailbox](https://blog.github.com/2017-07-18-managing-large-numbers-of-github-notifications/#prioritize-the-notifications-you-receive) +you do, either [configure your mailbox](https://blog.github.com/2017-07-18-managing-large-numbers-of-github-notifications/#prioritize-the-notifications-you-receive) to handle incoming notifications efficiently, or you read your notifications within a web browser. You can configure how you receive notifications in [your GitHub settings](https://github.com/settings/notifications), @@ -154,6 +154,7 @@ of the Coq Proof assistant during the indicated time: Matthias Puech (INRIA-Bologna, 2008-2011) Yann Régis-Gianas (INRIA-PPS then IRIF, 2009-now) Clément Renard (INRIA, 2001-2004) + Talia Ringer (University of Washington, 2019) Claudio Sacerdoti Coen (INRIA, 2004-2005) Amokrane Saïbi (INRIA, 1993-1998) Vincent Semeria (2018) @@ -170,7 +171,6 @@ of the Coq Proof assistant during the indicated time: Nickolai Zeldovich (MIT 2014-2016) Théo Zimmermann (ORCID: https://orcid.org/0000-0002-3580-8806, INRIA-PPS then IRIF, 2015-now) - Talia Ringer (UW, 2019) *************************************************************************** INRIA refers to: diff --git a/checker/check.ml b/checker/check.ml index 76f40dbac2..c5bc59e72a 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -50,6 +50,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 library_t = { @@ -90,7 +91,6 @@ let register_loaded_library m = (* Map from library names to table of opaque terms *) let opaque_tables = ref LibraryMap.empty -let opaque_univ_tables = ref LibraryMap.empty let access_opaque_table dp i = let t = @@ -326,7 +326,7 @@ let intern_from_file ~intern_mode (dir, f) = let ch = System.with_magic_number_check raw_intern_library f in 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:'a option), _, udg = 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 = @@ -345,7 +345,7 @@ let intern_from_file ~intern_mode (dir, f) = (str "The file "++str f++str " contains unfinished tasks"); if opaque_csts <> None then begin Flags.if_verbose chk_pp (str " (was a vio file) "); - Option.iter (fun (_,_,b) -> if not b then + Option.iter (fun (_,b) -> if not b then user_err ~hdr:"intern_from_file" (str "The file "++str f++str " is still a .vio")) opaque_csts; @@ -363,13 +363,9 @@ let intern_from_file ~intern_mode (dir, f) = with e -> Flags.if_verbose chk_pp (str" failed!]" ++ fnl ()); raise e in depgraph := LibraryMap.add sd.md_name sd.md_deps !depgraph; Option.iter (fun table -> opaque_tables := LibraryMap.add sd.md_name table !opaque_tables) table; - Option.iter (fun (opaque_csts,_,_) -> - opaque_univ_tables := - LibraryMap.add sd.md_name opaque_csts !opaque_univ_tables) - opaque_csts; let extra_cst = Option.default Univ.ContextSet.empty - (Option.map (fun (_,cs,_) -> cs) opaque_csts) in + (Option.map (fun (cs,_) -> cs) opaque_csts) in mk_library sd md f table digest extra_cst let get_deps (dir, f) = diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index 4f4527ca12..b66e198234 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -75,8 +75,7 @@ let check_arity env ar1 ar2 = match ar1, ar2 with (* template_level is inferred by indtypes, so functor application can produce a smaller one *) | (RegularArity _ | TemplateArity _), _ -> false -let check_kelim k1 k2 = - List.for_all (fun x -> List.mem_f Sorts.family_equal x k2) k1 +let check_kelim k1 k2 = Sorts.family_leq k1 k2 (* Use [eq_ind_chk] because when we rebuild the recargs we have lost the knowledge of who is the canonical version. diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 1cf07e7cc7..ccce0bd9a7 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -13,7 +13,6 @@ let set_indirect_accessor f = get_proof := f let indirect_accessor = { Opaqueproof.access_proof = (fun dp n -> !get_proof dp n); - Opaqueproof.access_constraints = (fun _ _ -> assert false); } let check_constant_declaration env kn cb = @@ -24,19 +23,19 @@ let check_constant_declaration env kn cb = (* [env'] contains De Bruijn universe variables *) let poly, env' = match cb.const_universes with - | Monomorphic ctx -> false, push_context_set ~strict:true ctx env + | Monomorphic ctx -> false, env | Polymorphic auctx -> let ctx = Univ.AUContext.repr auctx in let env = push_context ~strict:false ctx env in true, env in + let ty = cb.const_type in + let _ = infer_type env' ty in let env' = match cb.const_private_poly_univs, (cb.const_body, poly) with | None, _ -> env' | Some local, (OpaqueDef _, true) -> push_subgraph local env' | Some _, _ -> assert false in - let ty = cb.const_type in - let _ = infer_type env' ty in let otab = Environ.opaque_tables env in let body = match cb.const_body with | Undef _ | Primitive _ -> None diff --git a/checker/values.ml b/checker/values.ml index 4b651cafb6..031f05dd6b 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -257,7 +257,7 @@ let v_one_ind = v_tuple "one_inductive_body" Array v_constr; Int; Int; - List v_sortfam; + v_sortfam; Array (v_pair v_rctxt v_constr); Array Int; Array Int; @@ -385,4 +385,4 @@ let v_lib = let v_opaques = Array (Opt v_constr) let v_univopaques = - Opt (Tuple ("univopaques",[|Array (Opt v_context_set);v_context_set;v_bool|])) + Opt (Tuple ("univopaques",[|v_context_set;v_bool|])) diff --git a/dev/base_include b/dev/base_include index b214959bad..f764eaf4f5 100644 --- a/dev/base_include +++ b/dev/base_include @@ -185,7 +185,7 @@ open Declareops;; let constbody_of_string s = let b = Global.lookup_constant (Nametab.locate_constant (qualid_of_string s)) in - Option.get (Global.body_of_constant_body b);; + Option.get (Global.body_of_constant_body Library.indirect_accessor b);; (* Get the current goal *) (* diff --git a/dev/ci/user-overlays/10133-SkySkimmer-kelim.sh b/dev/ci/user-overlays/10133-SkySkimmer-kelim.sh new file mode 100644 index 0000000000..3658e96a3a --- /dev/null +++ b/dev/ci/user-overlays/10133-SkySkimmer-kelim.sh @@ -0,0 +1,6 @@ +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/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex index dd3908c25f..601d52ddda 100644 --- a/dev/v8-syntax/syntax-v8.tex +++ b/dev/v8-syntax/syntax-v8.tex @@ -1167,7 +1167,6 @@ $$ \nlsep \TERM{Show}~\OPT{\NT{num}} \nlsep \TERM{Show}~\TERM{Implicit}~\TERM{Arguments}~\OPT{\NT{num}} \nlsep \TERM{Show}~\TERM{Node} -\nlsep \TERM{Show}~\TERM{Script} \nlsep \TERM{Show}~\TERM{Existentials} \nlsep \TERM{Show}~\TERM{Tree} \nlsep \TERM{Show}~\TERM{Conjecture} diff --git a/doc/changelog/02-specification-language/10049-bidi-app.rst b/doc/changelog/02-specification-language/10049-bidi-app.rst new file mode 100644 index 0000000000..79678c5242 --- /dev/null +++ b/doc/changelog/02-specification-language/10049-bidi-app.rst @@ -0,0 +1,6 @@ +- New annotation in `Arguments` for bidirectionality hints: it is now possible + to tell type inference to use type information from the context once the `n` + first arguments of an application are known. The syntax is: + `Arguments foo x y & z`. + `#10049 <https://github.com/coq/coq/pull/10049>`_, by Maxime Dénès with + help from Enrico Tassi diff --git a/doc/changelog/07-commands-and-options/10277-no-show-script.rst b/doc/changelog/07-commands-and-options/10277-no-show-script.rst new file mode 100644 index 0000000000..7fdeb632b4 --- /dev/null +++ b/doc/changelog/07-commands-and-options/10277-no-show-script.rst @@ -0,0 +1,2 @@ +- Remove ``Show Script`` command (deprecated since 8.10) + (`#10277 <https://github.com/coq/coq/pull/10277>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/12-misc/10019-PG-proof-diffs.rst b/doc/changelog/12-misc/10019-PG-proof-diffs.rst new file mode 100644 index 0000000000..b2d191be26 --- /dev/null +++ b/doc/changelog/12-misc/10019-PG-proof-diffs.rst @@ -0,0 +1,3 @@ +- Proof General can now display Coq-generated diffs between proof steps + in color. (`#10019 <https://github.com/coq/coq/pull/10019>`_ and (in Proof General) + `#421 <https://github.com/ProofGeneral/PG/pull/421>`_, by Jim Fehrle). diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg index 1d0aca1caf..75251d8e33 100644 --- a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg +++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg @@ -94,9 +94,9 @@ VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY { let v = Constrintern.interp_constr (Global.env()) (Evd.from_env (Global.env())) e in let (_, ctx) = v in - let evd = Evd.from_ctx ctx in + let sigma = Evd.from_ctx ctx in Feedback.msg_notice - (Printer.pr_econstr_env (Global.env()) evd + (Printer.pr_econstr_env (Global.env()) sigma (Simple_check.simple_check1 v)) } END @@ -104,9 +104,9 @@ 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 evd, ty = Simple_check.simple_check2 v in + let sigma, ty = Simple_check.simple_check2 v in Feedback.msg_notice - (Printer.pr_econstr_env (Global.env()) evd ty) } + (Printer.pr_econstr_env (Global.env()) sigma ty) } END VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY @@ -114,9 +114,9 @@ VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY { let v = Constrintern.interp_constr (Global.env()) (Evd.from_env (Global.env())) e in let (a, ctx) = v in - let evd = Evd.from_ctx ctx in + let sigma = Evd.from_ctx ctx in Feedback.msg_notice - (Printer.pr_econstr_env (Global.env()) evd + (Printer.pr_econstr_env (Global.env()) sigma (Simple_check.simple_check3 v)) } END @@ -128,9 +128,9 @@ END VERNAC COMMAND EXTEND ExamplePrint CLASSIFIED AS QUERY | [ "Cmd8" reference(r) ] -> { let env = Global.env() in - let evd = Evd.from_env env in + let sigma = Evd.from_env env in Feedback.msg_notice - (Printer.pr_econstr_env env evd + (Printer.pr_econstr_env env sigma (EConstr.of_constr (Simple_print.simple_body_access (Nametab.global r)))) } END diff --git a/doc/plugin_tutorial/tuto1/src/simple_check.ml b/doc/plugin_tutorial/tuto1/src/simple_check.ml index 2949adde73..c2f09c64e0 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_check.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_check.ml @@ -1,32 +1,32 @@ let simple_check1 value_with_constraints = begin let evalue, st = value_with_constraints in - let evd = Evd.from_ctx st 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 evd evalue)) in + (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 evd = Evd.from_ctx st 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, 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()) evd evalue + Typing.type_of (Global.env()) sigma evalue let simple_check3 value_with_constraints = let evalue, st = value_with_constraints in - let evd = Evd.from_ctx st 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()) evd evalue + Retyping.get_type_of ~lax:true (Global.env()) sigma evalue diff --git a/doc/plugin_tutorial/tuto3/src/construction_game.ml b/doc/plugin_tutorial/tuto3/src/construction_game.ml index 663113d012..2a2acb6001 100644 --- a/doc/plugin_tutorial/tuto3/src/construction_game.ml +++ b/doc/plugin_tutorial/tuto3/src/construction_game.ml @@ -3,15 +3,15 @@ open Context let find_reference = Coqlib.find_reference [@ocaml.warning "-3"] -let example_sort evd = +let example_sort sigma = (* creating a new sort requires that universes should be recorded in the evd datastructure, so this datastructure also needs to be passed around. *) - let evd, s = Evd.new_sort_variable Evd.univ_rigid evd in + let sigma, s = Evd.new_sort_variable Evd.univ_rigid sigma in let new_type = EConstr.mkSort s in - evd, new_type + sigma, new_type -let c_one evd = +let c_one sigma = (* In the general case, global references may refer to universe polymorphic objects, and their universe has to be made afresh when creating an instance. *) let gr_S = @@ -19,129 +19,129 @@ let c_one evd = (* the long name of "S" was found with the command "About S." *) let gr_O = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in - let evd, c_O = Evarutil.new_global evd gr_O in - let evd, c_S = Evarutil.new_global evd gr_S in + let sigma, c_O = Evarutil.new_global sigma gr_O in + let sigma, c_S = Evarutil.new_global sigma gr_S in (* Here is the construction of a new term by applying functions to argument. *) - evd, EConstr.mkApp (c_S, [| c_O |]) + sigma, EConstr.mkApp (c_S, [| c_O |]) -let dangling_identity env evd = +let dangling_identity env sigma = (* I call this a dangling identity, because it is not polymorph, but the type on which it applies is left unspecified, as it is represented by an existential variable. The declaration for this existential variable needs to be added in the evd datastructure. *) - let evd, type_type = example_sort evd in - let evd, arg_type = Evarutil.new_evar env evd type_type in + let sigma, type_type = example_sort sigma in + let sigma, arg_type = Evarutil.new_evar env sigma type_type in (* Notice the use of a De Bruijn index for the inner occurrence of the bound variable. *) - evd, EConstr.mkLambda(nameR (Names.Id.of_string "x"), arg_type, + sigma, EConstr.mkLambda(nameR (Names.Id.of_string "x"), arg_type, EConstr.mkRel 1) -let dangling_identity2 env evd = +let dangling_identity2 env sigma = (* This example uses directly a function that produces an evar that is meant to be a type. *) - let evd, (arg_type, type_type) = - Evarutil.new_type_evar env evd Evd.univ_rigid in - evd, EConstr.mkLambda(nameR (Names.Id.of_string "x"), arg_type, + let sigma, (arg_type, type_type) = + Evarutil.new_type_evar env sigma Evd.univ_rigid in + sigma, EConstr.mkLambda(nameR (Names.Id.of_string "x"), arg_type, EConstr.mkRel 1) let example_sort_app_lambda () = let env = Global.env () in - let evd = Evd.from_env env in - let evd, c_v = c_one evd in + let sigma = Evd.from_env env in + let sigma, c_v = c_one sigma in (* dangling_identity and dangling_identity2 can be used interchangeably here *) - let evd, c_f = dangling_identity2 env evd in + let sigma, c_f = dangling_identity2 env sigma in let c_1 = EConstr.mkApp (c_f, [| c_v |]) in let _ = Feedback.msg_notice - (Printer.pr_econstr_env env evd c_1) in + (Printer.pr_econstr_env env sigma c_1) in (* type verification happens here. Type verification will update existential variable information in the evd part. *) - let evd, the_type = Typing.type_of env evd c_1 in + let sigma, the_type = Typing.type_of env sigma c_1 in (* At display time, you will notice that the system knows about the existential variable being instantiated to the "nat" type, even though c_1 still contains the meta-variable. *) Feedback.msg_notice - ((Printer.pr_econstr_env env evd c_1) ++ + ((Printer.pr_econstr_env env sigma c_1) ++ str " has type " ++ - (Printer.pr_econstr_env env evd the_type)) + (Printer.pr_econstr_env env sigma the_type)) -let c_S evd = +let c_S sigma = let gr = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in - Evarutil.new_global evd gr + Evarutil.new_global sigma gr -let c_O evd = +let c_O sigma = let gr = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in - Evarutil.new_global evd gr + Evarutil.new_global sigma gr -let c_E evd = +let c_E sigma = let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "EvenNat" in - Evarutil.new_global evd gr + Evarutil.new_global sigma gr -let c_D evd = +let c_D sigma = let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "tuto_div2" in - Evarutil.new_global evd gr + Evarutil.new_global sigma gr -let c_Q evd = +let c_Q sigma = let gr = find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq" in - Evarutil.new_global evd gr + Evarutil.new_global sigma gr -let c_R evd = +let c_R sigma = let gr = find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq_refl" in - Evarutil.new_global evd gr + Evarutil.new_global sigma gr -let c_N evd = +let c_N sigma = let gr = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "nat" in - Evarutil.new_global evd gr + Evarutil.new_global sigma gr -let c_C evd = +let c_C sigma = let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "C" in - Evarutil.new_global evd gr + Evarutil.new_global sigma gr -let c_F evd = +let c_F sigma = let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "S_ev" in - Evarutil.new_global evd gr + Evarutil.new_global sigma gr -let c_P evd = +let c_P sigma = let gr = find_reference "Tuto3" ["Tuto3"; "Data"] "s_half_proof" in - Evarutil.new_global evd gr + Evarutil.new_global sigma gr (* If c_S was universe polymorphic, we should have created a new constant at each iteration of buildup. *) -let mk_nat evd n = - let evd, c_S = c_S evd in - let evd, c_O = c_O evd in +let mk_nat sigma n = + let sigma, c_S = c_S sigma in + let sigma, c_O = c_O sigma in let rec buildup = function | 0 -> c_O | n -> EConstr.mkApp (c_S, [| buildup (n - 1) |]) in - if n <= 0 then evd, c_O else evd, buildup n + if n <= 0 then sigma, c_O else sigma, buildup n let example_classes n = let env = Global.env () in - let evd = Evd.from_env env in - let evd, c_n = mk_nat evd n in - let evd, n_half = mk_nat evd (n / 2) in - let evd, c_N = c_N evd in - let evd, c_div = c_D evd in - let evd, c_even = c_E evd in - let evd, c_Q = c_Q evd in - let evd, c_R = c_R evd in + let sigma = Evd.from_env env in + let sigma, c_n = mk_nat sigma n in + let sigma, n_half = mk_nat sigma (n / 2) in + let sigma, c_N = c_N sigma in + let sigma, c_div = c_D sigma in + let sigma, c_even = c_E sigma in + let sigma, c_Q = c_Q sigma in + let sigma, c_R = c_R sigma in let arg_type = EConstr.mkApp (c_even, [| c_n |]) in - let evd0 = evd in - let evd, instance = Evarutil.new_evar env evd arg_type in + let sigma0 = sigma in + let sigma, instance = Evarutil.new_evar env sigma arg_type in let c_half = EConstr.mkApp (c_div, [|c_n; instance|]) in - let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd c_half) in - let evd, the_type = Typing.type_of env evd c_half in - let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd c_half) in + let _ = Feedback.msg_notice (Printer.pr_econstr_env env sigma c_half) in + let sigma, the_type = Typing.type_of env sigma c_half in + let _ = Feedback.msg_notice (Printer.pr_econstr_env env sigma c_half) in let proved_equality = EConstr.mkCast(EConstr.mkApp (c_R, [| c_N; c_half |]), Constr.DEFAULTcast, EConstr.mkApp (c_Q, [| c_N; c_half; n_half|])) in (* This is where we force the system to compute with type classes. *) (* Question to coq developers: why do we pass two evd arguments to - solve_remaining_evars? Is the choice of evd0 relevant here? *) - let evd = Pretyping.solve_remaining_evars - (Pretyping.default_inference_flags true) env evd ~initial:evd0 in - let evd, final_type = Typing.type_of env evd proved_equality in - Feedback.msg_notice (Printer.pr_econstr_env env evd proved_equality) + solve_remaining_evars? Is the choice of sigma0 relevant here? *) + let sigma = Pretyping.solve_remaining_evars + (Pretyping.default_inference_flags true) env sigma ~initial:sigma0 in + let sigma, final_type = Typing.type_of env sigma proved_equality in + Feedback.msg_notice (Printer.pr_econstr_env env sigma proved_equality) (* This function, together with definitions in Data.v, shows how to trigger automatic proofs at the time of typechecking, based on @@ -152,36 +152,36 @@ let example_classes n = *) let example_canonical n = let env = Global.env () in - let evd = Evd.from_env env in + let sigma = Evd.from_env env in (* Construct a natural representation of this integer. *) - let evd, c_n = mk_nat evd n in + let sigma, c_n = mk_nat sigma n in (* terms for "nat", "eq", "S_ev", "eq_refl", "C" *) - let evd, c_N = c_N evd in - let evd, c_F = c_F evd in - let evd, c_R = c_R evd in - let evd, c_C = c_C evd in - let evd, c_P = c_P evd in + let sigma, c_N = c_N sigma in + let sigma, c_F = c_F sigma in + let sigma, c_R = c_R sigma in + let sigma, c_C = c_C sigma in + let sigma, c_P = c_P sigma in (* the last argument of C *) let refl_term = EConstr.mkApp (c_R, [|c_N; c_n |]) in (* Now we build two existential variables, for the value of the half and for the "S_ev" structure that triggers the proof search. *) - let evd, ev1 = Evarutil.new_evar env evd c_N in + let sigma, ev1 = Evarutil.new_evar env sigma c_N in (* This is the type for the second existential variable *) let csev = EConstr.mkApp (c_F, [| ev1 |]) in - let evd, ev2 = Evarutil.new_evar env evd csev in + let sigma, ev2 = Evarutil.new_evar env sigma csev in (* Now we build the C structure. *) let test_term = EConstr.mkApp (c_C, [| c_n; ev1; ev2; refl_term |]) in (* Type-checking this term will compute values for the existential variables *) - let evd, final_type = Typing.type_of env evd test_term in + let sigma, final_type = Typing.type_of env sigma test_term in (* The computed type has two parameters, the second one is the proof. *) - let value = match EConstr.kind evd final_type with + let value = match EConstr.kind sigma final_type with | Constr.App(_, [| _; the_half |]) -> the_half | _ -> failwith "expecting the whole type to be \"cmp _ the_half\"" in - let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd value) in + let _ = Feedback.msg_notice (Printer.pr_econstr_env env sigma value) in (* I wish for a nicer way to get the value of ev2 in the evar_map *) - let prf_struct = EConstr.of_constr (EConstr.to_constr evd ev2) in + let prf_struct = EConstr.of_constr (EConstr.to_constr sigma ev2) in let the_prf = EConstr.mkApp (c_P, [| ev1; prf_struct |]) in - let evd, the_statement = Typing.type_of env evd the_prf in + let sigma, the_statement = Typing.type_of env sigma the_prf in Feedback.msg_notice - (Printer.pr_econstr_env env evd the_prf ++ str " has type " ++ - Printer.pr_econstr_env env evd the_statement) + (Printer.pr_econstr_env env sigma the_prf ++ str " has type " ++ + Printer.pr_econstr_env env sigma the_statement) diff --git a/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg b/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg index f4d9e7fd5b..14b8eb5f07 100644 --- a/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg +++ b/doc/plugin_tutorial/tuto3/src/g_tuto3.mlg @@ -14,13 +14,13 @@ open Stdarg VERNAC COMMAND EXTEND ShowTypeConstruction CLASSIFIED AS QUERY | [ "Tuto3_1" ] -> { let env = Global.env () in - let evd = Evd.from_env env in - let evd, s = Evd.new_sort_variable Evd.univ_rigid evd in + let sigma = Evd.from_env env in + let sigma, s = Evd.new_sort_variable Evd.univ_rigid sigma in let new_type_2 = EConstr.mkSort s in - let evd, _ = + let sigma, _ = Typing.type_of (Global.env()) (Evd.from_env (Global.env())) new_type_2 in Feedback.msg_notice - (Printer.pr_econstr_env env evd new_type_2) } + (Printer.pr_econstr_env env sigma new_type_2) } END VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY diff --git a/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml index 2d541087ce..796a65f40d 100644 --- a/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml +++ b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml @@ -65,10 +65,10 @@ let package i = Goal.enter begin fun gl -> and return the value a. *) (* Remark by Maxime: look for destApp combinator. *) -let unpack_type evd term = +let unpack_type sigma term = let report () = CErrors.user_err (Pp.str "expecting a packed type") in - match EConstr.kind evd term with + match EConstr.kind sigma term with | Constr.App (_, [| ty |]) -> ty | _ -> report () @@ -76,19 +76,19 @@ let unpack_type evd term = A -> pack B -> C and return A, B, C but it is not used in the current version of our tactic. It is kept as an example. *) -let two_lambda_pattern evd term = +let two_lambda_pattern sigma term = let report () = CErrors.user_err (Pp.str "expecting two nested implications") in (* Note that pattern-matching is always done through the EConstr.kind function, which only provides one-level deep patterns. *) - match EConstr.kind evd term with + match EConstr.kind sigma term with (* Here we recognize the outer implication *) | Constr.Prod (_, ty1, l1) -> (* Here we recognize the inner implication *) - (match EConstr.kind evd l1 with + (match EConstr.kind sigma l1 with | Constr.Prod (n2, packed_ty2, deep_conclusion) -> (* Here we recognized that the second type is an application *) - ty1, unpack_type evd packed_ty2, deep_conclusion + ty1, unpack_type sigma packed_ty2, deep_conclusion | _ -> report ()) | _ -> report () @@ -104,22 +104,22 @@ let get_type_of_hyp env id = let repackage i h_hyps_id = Goal.enter begin fun gl -> let env = Goal.env gl in - let evd = Tacmach.New.project gl in + let sigma = Tacmach.New.project gl in let concl = Tacmach.New.pf_concl gl in let (ty1 : EConstr.t) = get_type_of_hyp env i in let (packed_ty2 : EConstr.t) = get_type_of_hyp env h_hyps_id in - let ty2 = unpack_type evd packed_ty2 in + let ty2 = unpack_type sigma packed_ty2 in let new_packed_type = EConstr.mkApp (c_P (), [| ty1; ty2 |]) in let open EConstr in let new_packed_value = mkApp (c_R (), [| ty1; ty2; mkVar i; mkApp (c_U (), [| ty2; mkVar h_hyps_id|]) |]) in - Refine.refine ~typecheck:true begin fun evd -> - let evd, new_goal = Evarutil.new_evar env evd + Refine.refine ~typecheck:true begin fun sigma -> + let sigma, new_goal = Evarutil.new_evar env sigma (mkArrowR (mkApp(c_H (), [| new_packed_type |])) (Vars.lift 1 concl)) in - evd, mkApp (new_goal, + sigma, mkApp (new_goal, [|mkApp(c_M (), [|new_packed_type; new_packed_value |]) |]) end end diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index c1af4d067f..8c5ad785e4 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2448,3 +2448,45 @@ types and functions of a :g:`Uint63` module. Said module is not produced by extraction. Instead, it has to be provided by the user (if they want to compile or execute the extracted code). For instance, an implementation of this module can be taken from the kernel of Coq. + +Bidirectionality hints +---------------------- + +When type-checking an application, Coq normally does not use information from +the context to infer the types of the arguments. It only checks after the fact +that the type inferred for the application is coherent with the expected type. +Bidirectionality hints make it possible to specify that after type-checking the +first arguments of an application, typing information should be propagated from +the context to help inferring the types of the remaining arguments. + +.. cmd:: Arguments @qualid {* @ident__1 } & {* @ident__2} + :name: Arguments (bidirectionality hints) + + This commands tells the typechecking algorithm, when type-checking + applications of :n:`@qualid`, to first type-check the arguments in + :n:`@ident__1` and then propagate information from the typing context to + type-check the remaining arguments (in :n:`@ident__2`). + +.. example:: + + In a context where a coercion was declared from ``bool`` to ``nat``: + + .. coqtop:: in reset + + Definition b2n (b : bool) := if b then 1 else 0. + Coercion b2n : bool >-> nat. + + Coq cannot automatically coerce existential statements over ``bool`` to + statements over ``nat``, because the need for inserting a coercion is known + only from the expected type of a subterm: + + .. coqtop:: all + + Fail Check (ex_intro _ true _ : exists n : nat, n > 0). + + However, a suitable bidirectionality hint makes the example work: + + .. coqtop:: all + + Arguments ex_intro _ _ & _ _. + Check (ex_intro _ true _ : exists n : nat, n > 0). diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 3f966755ca..0cff987a27 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -535,19 +535,6 @@ Requesting information eexists ?[n]. Show n. - .. cmdv:: Show Script - :name: Show Script - - Displays the whole list of tactics applied from the - beginning of the current proof. This tactics script may contain some - holes (subgoals not yet proved). They are printed under the form - - ``<Your Tactic Text here>``. - - .. deprecated:: 8.10 - - Please use a text editor. - .. cmdv:: Show Proof :name: Show Proof @@ -705,9 +692,10 @@ command in CoqIDE. You can change the background colors shown for diffs from th lets you control other attributes of the highlights, such as the foreground color, bold, italic, underline and strikeout. -Note: As of this writing (August 2018), Proof General will need minor changes -to be able to show diffs correctly. We hope it will support this feature soon. -See https://github.com/ProofGeneral/PG/issues/381 for the current status. +As of June 2019, Proof General can also display Coq-generated proof diffs automatically. +Please see the PG documentation section +"`Showing Proof Diffs" <https://proofgeneral.github.io/doc/master/userman/Coq-Proof-General#Showing-Proof-Diffs>`_) +for details. How diffs are calculated ```````````````````````` diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index b0bafb7930..7f68f24c22 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -126,7 +126,6 @@ let commands = [ "Show Intros"; "Show Programs"; "Show Proof"; - "Show Script"; "Show Tree";*) "Structure"; "Syntactic Definition"; @@ -221,7 +220,6 @@ let state_preserving = [ "Show Intro"; "Show Intros"; "Show Proof"; - "Show Script"; "Show Tree"; "Test Printing If"; diff --git a/interp/declare.ml b/interp/declare.ml index b3595b2dae..cc6f29f756 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -53,6 +53,13 @@ let load_constant i ((sp,kn), obj) = Nametab.push (Nametab.Until i) sp (ConstRef con); add_constant_kind con obj.cst_kind +let cooking_info segment = + let modlist = replacement_context () in + let { abstr_ctx = hyps; abstr_subst = subst; abstr_uctx = uctx } = segment in + let named_ctx = List.map fst hyps in + let abstract = (named_ctx, subst, uctx) in + { Opaqueproof.modlist; abstract } + (* Opening means making the name without its module qualification available *) let open_constant i ((sp,kn), obj) = (* Never open a local definition *) @@ -89,13 +96,10 @@ let cache_constant ((sp,kn), obj) = let discharge_constant ((sp, kn), obj) = let con = Constant.make1 kn in let from = Global.lookup_constant con in - let modlist = replacement_context () in - let { abstr_ctx = hyps; abstr_subst = subst; abstr_uctx = uctx } = section_segment_of_constant con in - let abstract = (named_of_variable_context hyps, subst, uctx) in - let new_decl = { from; info = { Opaqueproof.modlist; abstract } } in + let info = cooking_info (section_segment_of_constant con) in (* This is a hack: when leaving a section, we lose the constant definition, so we have to store it in the libobject to be able to retrieve it after. *) - Some { obj with cst_decl = Some new_decl; } + Some { obj with cst_decl = Some { from; info } } (* Hack to reduce the size of .vo: we keep only what load/open needs *) let dummy_constant cst = { @@ -312,9 +316,8 @@ let cache_inductive ((sp,kn),mie) = let discharge_inductive ((sp,kn),mie) = let mind = Global.mind_of_delta_kn kn in let mie = Global.lookup_mind mind in - let repl = replacement_context () in - let info = section_segment_of_mutual_inductive mind in - Some (Discharge.process_inductive info repl mie) + let info = cooking_info (section_segment_of_mutual_inductive mind) in + Some (Cooking.cook_inductive info mie) let dummy_one_inductive_entry mie = { mind_entry_typename = mie.mind_entry_typename; diff --git a/interp/discharge.ml b/interp/discharge.ml deleted file mode 100644 index 1efd13adb1..0000000000 --- a/interp/discharge.ml +++ /dev/null @@ -1,118 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Util -open Term -open Constr -open Vars -open Declarations -open Cooking -open Entries - -(********************************) -(* Discharging mutual inductive *) - -(* Replace - - Var(y1)..Var(yq):C1..Cq |- Ij:Bj - Var(y1)..Var(yq):C1..Cq; I1..Ip:B1..Bp |- ci : Ti - - by - - |- Ij: (y1..yq:C1..Cq)Bj - I1..Ip:(B1 y1..yq)..(Bp y1..yq) |- ci : (y1..yq:C1..Cq)Ti[Ij:=(Ij y1..yq)] -*) - -let abstract_inductive decls nparamdecls inds = - let ntyp = List.length inds in - let ndecls = Context.Named.length decls in - let args = Context.Named.to_instance mkVar (List.rev decls) in - let args = Array.of_list args in - let subs = List.init ntyp (fun k -> lift ndecls (mkApp(mkRel (k+1),args))) in - let inds' = - List.map - (function (tname,arity,template,cnames,lc) -> - let lc' = List.map (substl subs) lc in - let lc'' = List.map (fun b -> Termops.it_mkNamedProd_wo_LetIn b decls) lc' in - let arity' = Termops.it_mkNamedProd_wo_LetIn arity decls in - (tname,arity',template,cnames,lc'')) - inds in - let nparamdecls' = nparamdecls + Array.length args in -(* To be sure to be the same as before, should probably be moved to process_inductive *) - let params' = let (_,arity,_,_,_) = List.hd inds' in - let (params,_) = decompose_prod_n_assum nparamdecls' arity in - params - in - let ind'' = - List.map - (fun (a,arity,template,c,lc) -> - let _, short_arity = decompose_prod_n_assum nparamdecls' arity in - let shortlc = - List.map (fun c -> snd (decompose_prod_n_assum nparamdecls' c)) lc in - { mind_entry_typename = a; - mind_entry_arity = short_arity; - mind_entry_template = template; - mind_entry_consnames = c; - mind_entry_lc = shortlc }) - inds' - in (params',ind'') - -let refresh_polymorphic_type_of_inductive (_,mip) = - match mip.mind_arity with - | RegularArity s -> s.mind_user_arity, false - | TemplateArity ar -> - let ctx = List.rev mip.mind_arity_ctxt in - mkArity (List.rev ctx, Sorts.sort_of_univ ar.template_level), true - -let process_inductive info modlist mib = - let section_decls = Lib.named_of_variable_context info.Lib.abstr_ctx in - let nparamdecls = Context.Rel.length mib.mind_params_ctxt in - let subst, ind_univs = - match mib.mind_universes with - | Monomorphic ctx -> Univ.empty_level_subst, Monomorphic_entry ctx - | Polymorphic auctx -> - let subst, auctx = Lib.discharge_abstract_universe_context info auctx in - let nas = Univ.AUContext.names auctx in - let auctx = Univ.AUContext.repr auctx in - subst, Polymorphic_entry (nas, auctx) - in - let variance = match mib.mind_variance with - | None -> None - | Some _ -> Some (InferCumulativity.dummy_variance ind_univs) - in - let discharge c = Vars.subst_univs_level_constr subst (expmod_constr modlist c) in - let inds = - Array.map_to_list - (fun mip -> - let ty, template = refresh_polymorphic_type_of_inductive (mib,mip) in - let arity = discharge ty in - let lc = Array.map discharge mip.mind_user_lc in - (mip.mind_typename, - arity, template, - Array.to_list mip.mind_consnames, - Array.to_list lc)) - mib.mind_packets in - let section_decls' = Context.Named.map discharge section_decls in - let (params',inds') = abstract_inductive section_decls' nparamdecls inds in - let record = match mib.mind_record with - | PrimRecord info -> - Some (Some (Array.map (fun (x,_,_,_) -> x) info)) - | FakeRecord -> Some None - | NotRecord -> None - in - { mind_entry_record = record; - mind_entry_finite = mib.mind_finite; - mind_entry_params = params'; - mind_entry_inds = inds'; - mind_entry_private = mib.mind_private; - mind_entry_variance = variance; - mind_entry_universes = ind_univs - } - diff --git a/interp/discharge.mli b/interp/discharge.mli deleted file mode 100644 index f7408937cf..0000000000 --- a/interp/discharge.mli +++ /dev/null @@ -1,16 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Declarations -open Entries -open Opaqueproof - -val process_inductive : - Lib.abstr_info -> work_list -> mutual_inductive_body -> mutual_inductive_entry diff --git a/interp/interp.mllib b/interp/interp.mllib index 1262dbb181..b65a171ef9 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -16,5 +16,4 @@ Implicit_quantifiers Constrintern Modintern Constrextern -Discharge Declare diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 13851319cd..620efbafd6 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -165,25 +165,33 @@ type 'opaque result = { cook_context : Constr.named_context option; } -let on_body ml hy f = function - | Undef _ as x -> x - | Def cs -> Def (Mod_subst.from_val (f (Mod_subst.force_constr cs))) - | OpaqueDef o -> - OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:f - { Opaqueproof.modlist = ml; abstract = hy } o) - | Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked") - let expmod_constr_subst cache modlist subst c = let subst = Univ.make_instance_subst subst in let c = expmod_constr cache modlist c in Vars.subst_univs_level_constr subst c -let cook_constr { Opaqueproof.modlist ; abstract = (vars, subst, _) } c = - let cache = RefTable.create 13 in - let expmod = expmod_constr_subst cache modlist subst in - let hyps = Context.Named.map expmod vars in - let hyps = abstract_context hyps in - abstract_constant_body (expmod c) hyps +let discharge_abstract_universe_context subst abs_ctx auctx = + (** Given a named instance [subst := u₀ ... uₙ₋₁] together with an abstract + context [auctx0 := 0 ... n - 1 |= C{0, ..., n - 1}] of the same length, + and another abstract context relative to the former context + [auctx := 0 ... m - 1 |= C'{u₀, ..., uₙ₋₁, 0, ..., m - 1}], + construct the lifted abstract universe context + [0 ... n - 1 n ... n + m - 1 |= + C{0, ... n - 1} ∪ + C'{0, ..., n - 1, n, ..., n + m - 1} ] + together with the instance + [u₀ ... uₙ₋₁ Var(0) ... Var (m - 1)]. + *) + if (Univ.Instance.is_empty subst) then + (** Still need to take the union for the constraints between globals *) + subst, (AUContext.union abs_ctx auctx) + else + let open Univ in + let ainst = make_abstract_instance auctx in + let subst = Instance.append subst ainst in + let substf = make_instance_subst subst in + let auctx = Univ.subst_univs_level_abstract_universe_context substf auctx in + subst, (AUContext.union abs_ctx auctx) let lift_univs cb subst auctx0 = match cb.const_universes with @@ -191,26 +199,20 @@ let lift_univs cb subst auctx0 = assert (AUContext.is_empty auctx0); subst, (Monomorphic ctx) | Polymorphic auctx -> - (** Given a named instance [subst := u₀ ... uₙ₋₁] together with an abstract - context [auctx0 := 0 ... n - 1 |= C{0, ..., n - 1}] of the same length, - and another abstract context relative to the former context - [auctx := 0 ... m - 1 |= C'{u₀, ..., uₙ₋₁, 0, ..., m - 1}], - construct the lifted abstract universe context - [0 ... n - 1 n ... n + m - 1 |= - C{0, ... n - 1} ∪ - C'{0, ..., n - 1, n, ..., n + m - 1} ] - together with the instance - [u₀ ... uₙ₋₁ Var(0) ... Var (m - 1)]. - *) - if (Univ.Instance.is_empty subst) then - (** Still need to take the union for the constraints between globals *) - subst, (Polymorphic (AUContext.union auctx0 auctx)) - else - let ainst = Univ.make_abstract_instance auctx in - let subst = Instance.append subst ainst in - let substf = Univ.make_instance_subst subst in - let auctx' = Univ.subst_univs_level_abstract_universe_context substf auctx in - subst, (Polymorphic (AUContext.union auctx0 auctx')) + let subst, auctx = discharge_abstract_universe_context subst auctx0 auctx in + subst, (Polymorphic auctx) + +let cook_constr { Opaqueproof.modlist ; abstract } 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 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 cook_constant { from = cb; info } = let { Opaqueproof.modlist; abstract } = info in @@ -221,9 +223,12 @@ let cook_constant { from = cb; info } = let hyps0 = Context.Named.map expmod abstract in let hyps = abstract_context hyps0 in let map c = abstract_constant_body (expmod c) hyps in - let body = on_body modlist (hyps0, usubst, abs_ctx) - map - cb.const_body + let body = match cb.const_body with + | 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) + | Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked") in let const_hyps = Context.Named.fold_outside (fun decl hyps -> @@ -248,4 +253,115 @@ let cook_constant { from = cb; info } = (* let cook_constant_key = CProfile.declare_profile "cook_constant" *) (* let cook_constant = CProfile.profile2 cook_constant_key cook_constant *) +(********************************) +(* Discharging mutual inductive *) + +(* Replace + + Var(y1)..Var(yq):C1..Cq |- Ij:Bj + Var(y1)..Var(yq):C1..Cq; I1..Ip:B1..Bp |- ci : Ti + + by + + |- Ij: (y1..yq:C1..Cq)Bj + I1..Ip:(B1 y1..yq)..(Bp y1..yq) |- ci : (y1..yq:C1..Cq)Ti[Ij:=(Ij y1..yq)] +*) + +let it_mkNamedProd_wo_LetIn b d = + List.fold_left (fun c d -> mkNamedProd_wo_LetIn d c) b d + +let abstract_inductive decls nparamdecls inds = + let open Entries in + let ntyp = List.length inds in + let ndecls = Context.Named.length decls in + let args = Context.Named.to_instance mkVar (List.rev decls) in + let args = Array.of_list args in + let subs = List.init ntyp (fun k -> lift ndecls (mkApp(mkRel (k+1),args))) in + let inds' = + List.map + (function (tname,arity,template,cnames,lc) -> + let lc' = List.map (Vars.substl subs) lc in + let lc'' = List.map (fun b -> it_mkNamedProd_wo_LetIn b decls) lc' in + let arity' = it_mkNamedProd_wo_LetIn arity decls in + (tname,arity',template,cnames,lc'')) + inds in + let nparamdecls' = nparamdecls + Array.length args in +(* To be sure to be the same as before, should probably be moved to cook_inductive *) + let params' = let (_,arity,_,_,_) = List.hd inds' in + let (params,_) = decompose_prod_n_assum nparamdecls' arity in + params + in + let ind'' = + List.map + (fun (a,arity,template,c,lc) -> + let _, short_arity = decompose_prod_n_assum nparamdecls' arity in + let shortlc = + List.map (fun c -> snd (decompose_prod_n_assum nparamdecls' c)) lc in + { mind_entry_typename = a; + mind_entry_arity = short_arity; + mind_entry_template = template; + mind_entry_consnames = c; + mind_entry_lc = shortlc }) + inds' + in (params',ind'') + +let refresh_polymorphic_type_of_inductive (_,mip) = + match mip.mind_arity with + | RegularArity s -> s.mind_user_arity, false + | TemplateArity ar -> + let ctx = List.rev mip.mind_arity_ctxt in + mkArity (List.rev ctx, Sorts.sort_of_univ ar.template_level), true + +let dummy_variance = let open Entries in function + | Monomorphic_entry _ -> assert false + | Polymorphic_entry (_,uctx) -> Array.make (Univ.UContext.size uctx) Univ.Variance.Irrelevant + +let cook_inductive { Opaqueproof.modlist; abstract } mib = + let open Entries in + let (section_decls, subst, abs_uctx) = abstract in + let nparamdecls = Context.Rel.length mib.mind_params_ctxt in + let subst, ind_univs = + match mib.mind_universes with + | Monomorphic ctx -> Univ.empty_level_subst, Monomorphic_entry ctx + | Polymorphic auctx -> + let subst, auctx = discharge_abstract_universe_context subst abs_uctx auctx in + let subst = Univ.make_instance_subst subst in + let nas = Univ.AUContext.names auctx in + let auctx = Univ.AUContext.repr auctx in + subst, Polymorphic_entry (nas, auctx) + in + let variance = match mib.mind_variance with + | None -> None + | Some _ -> Some (dummy_variance ind_univs) + in + let cache = RefTable.create 13 in + let discharge c = Vars.subst_univs_level_constr subst (expmod_constr cache modlist c) in + let inds = + Array.map_to_list + (fun mip -> + let ty, template = refresh_polymorphic_type_of_inductive (mib,mip) in + let arity = discharge ty in + let lc = Array.map discharge mip.mind_user_lc in + (mip.mind_typename, + arity, template, + Array.to_list mip.mind_consnames, + Array.to_list lc)) + mib.mind_packets in + let section_decls' = Context.Named.map discharge section_decls in + let (params',inds') = abstract_inductive section_decls' nparamdecls inds in + let record = match mib.mind_record with + | PrimRecord info -> + Some (Some (Array.map (fun (x,_,_,_) -> x) info)) + | FakeRecord -> Some None + | NotRecord -> None + in + { mind_entry_record = record; + mind_entry_finite = mib.mind_finite; + mind_entry_params = params'; + mind_entry_inds = inds'; + mind_entry_private = mib.mind_private; + mind_entry_variance = variance; + mind_entry_universes = ind_univs + } + let expmod_constr modlist c = expmod_constr (RefTable.create 13) modlist c diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 024eed1285..abae3880d7 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -30,6 +30,9 @@ type 'opaque result = { val cook_constant : recipe -> Opaqueproof.opaque result val cook_constr : Opaqueproof.cooking_info -> constr -> constr +val cook_inductive : + Opaqueproof.cooking_info -> mutual_inductive_body -> Entries.mutual_inductive_entry + (** {6 Utility functions used in module [Discharge]. } *) val expmod_constr : Opaqueproof.work_list -> constr -> constr diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 860d19fe26..388b4f14bf 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -165,7 +165,7 @@ type one_inductive_body = { mind_nrealdecls : int; (** Length of realargs context (with let, no params) *) - mind_kelim : Sorts.family list; (** List of allowed elimination sorts *) + mind_kelim : Sorts.family; (** Highest allowed elimination sort *) mind_nf_lc : (rel_context * types) array; (** Head normalized constructor types so that their conclusion exposes the inductive type *) diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index 4e6e595331..65298938fa 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -232,18 +232,9 @@ let check_record data = (* - all_sorts in case of small, unitary Prop (not smashed) *) (* - logical_sorts in case of large, unitary Prop (smashed) *) -let all_sorts = [InSProp;InProp;InSet;InType] -let small_sorts = [InSProp;InProp;InSet] -let logical_sorts = [InSProp;InProp] -let sprop_sorts = [InSProp] - let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_;ind_has_relevant_arg=_} = - if not ind_squashed then all_sorts - else match Sorts.family (Sorts.sort_of_univ ind_univ) with - | InType -> assert false - | InSet -> small_sorts - | InProp -> logical_sorts - | InSProp -> sprop_sorts + if not ind_squashed then InType + else Sorts.family (Sorts.sort_of_univ ind_univ) (* Returns the list [x_1, ..., x_n] of levels contributing to template polymorphism. The elements x_k is None if the k-th parameter (starting diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli index ad51af66a2..ef2c30b76a 100644 --- a/kernel/indTyping.mli +++ b/kernel/indTyping.mli @@ -22,7 +22,7 @@ open Declarations - for each inductive, (arity * constructors) (with params) * (indices * splayed constructor types) (both without params) - * allowed eliminations + * top allowed elimination *) val typecheck_inductive : env -> mutual_inductive_entry -> env @@ -31,5 +31,5 @@ val typecheck_inductive : env -> mutual_inductive_entry -> * Constr.rel_context * ((inductive_arity * Constr.types array) * (Constr.rel_context * (Constr.rel_context * Constr.types) array) * - Sorts.family list) + Sorts.family) array diff --git a/kernel/inductive.ml b/kernel/inductive.ml index ca7086a3e4..beff8f4421 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -289,7 +289,7 @@ let get_instantiated_arity (_ind,u) (mib,mip) params = let sign, s = mind_arity mip in full_inductive_instantiate mib u params sign, s -let elim_sorts (_,mip) = mip.mind_kelim +let elim_sort (_,mip) = mip.mind_kelim let is_private (mib,_) = mib.mind_private = Some true let is_primitive_record (mib,_) = @@ -305,12 +305,12 @@ let build_dependent_inductive ind (_,mip) params = @ Context.Rel.to_extended_list mkRel 0 realargs) (* This exception is local *) -exception LocalArity of (Sorts.family list * Sorts.family * Sorts.family * arity_error) option +exception LocalArity of (Sorts.family * Sorts.family * Sorts.family * arity_error) option let check_allowed_sort ksort specif = - if not (CList.exists (Sorts.family_equal ksort) (elim_sorts specif)) then + if not (Sorts.family_leq ksort (elim_sort specif)) then let s = inductive_sort_family (snd specif) in - raise (LocalArity (Some(elim_sorts specif, ksort,s,error_elim_explain ksort s))) + raise (LocalArity (Some(elim_sort specif, ksort,s,error_elim_explain ksort s))) let is_correct_arity env c pj ind specif params = let arsign,_ = get_instantiated_arity ind specif params in diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 997a620742..f705cdf646 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -52,7 +52,7 @@ val type_of_inductive : env -> mind_specif puniverses -> types val type_of_inductive_knowing_parameters : env -> ?polyprop:bool -> mind_specif puniverses -> types Lazy.t array -> types -val elim_sorts : mind_specif -> Sorts.family list +val elim_sort : mind_specif -> Sorts.family val is_private : mind_specif -> bool val is_primitive_record : mind_specif -> bool diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 0ff27eb4ea..1971c67c61 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -18,7 +18,6 @@ type work_list = (Instance.t * Id.t array) Cmap.t * type indirect_accessor = { access_proof : DirPath.t -> int -> constr option; - access_constraints : DirPath.t -> int -> Univ.ContextSet.t option; } type cooking_info = { @@ -107,14 +106,12 @@ let force_proof access { opaque_val = prfs; opaque_dir = odp; _ } = function 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 +let force_constraints _access { opaque_val = prfs; opaque_dir = odp; _ } = function | Direct (_,cu) -> snd(Future.force cu) | Indirect (_,dp,i) -> if DirPath.equal dp odp then snd (Future.force (snd (Int.Map.find i prfs))) - else match access.access_constraints dp i with - | None -> Univ.ContextSet.empty - | Some u -> u + else Univ.ContextSet.empty let get_direct_constraints = function | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") @@ -124,15 +121,13 @@ 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 univ_table = Array.make n None in let disch_table = Array.make n [] in let f2t_map = ref FMap.empty in let iter n (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, u) = Future.force cu in - let () = univ_table.(n) <- Some u in + let (c, _) = Future.force cu in opaque_table.(n) <- Some c else if Future.UUIDSet.mem uid except then disch_table.(n) <- d @@ -141,4 +136,4 @@ let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _ Pp.(str"Proof object "++int n++str" is not checked nor to be checked") in let () = Int.Map.iter iter otab in - opaque_table, univ_table, disch_table, !f2t_map + opaque_table, disch_table, !f2t_map diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 4646206e55..46b0500507 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -37,7 +37,6 @@ val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab type indirect_accessor = { access_proof : DirPath.t -> int -> constr option; - access_constraints : DirPath.t -> int -> Univ.ContextSet.t option; } (** When stored indirectly, opaque terms are indexed by their library dirpath and an integer index. The two functions above activate @@ -70,6 +69,5 @@ val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit val dump : ?except:Future.UUIDSet.t -> opaquetab -> Constr.t option array * - Univ.ContextSet.t option array * cooking_info list array * int Future.UUIDMap.t diff --git a/kernel/sorts.ml b/kernel/sorts.ml index 09c98ca1bc..b5a929697e 100644 --- a/kernel/sorts.ml +++ b/kernel/sorts.ml @@ -91,6 +91,8 @@ let family_compare a b = match a,b with let family_equal = (==) +let family_leq a b = family_compare a b <= 0 + open Hashset.Combine let hash = function @@ -101,11 +103,6 @@ let hash = function let h = Univ.Universe.hash u in combinesmall 2 h -module List = struct - let mem = List.memq - let intersect l l' = CList.intersect family_equal l l' -end - module Hsorts = Hashcons.Make( struct diff --git a/kernel/sorts.mli b/kernel/sorts.mli index c49728b146..3769e31465 100644 --- a/kernel/sorts.mli +++ b/kernel/sorts.mli @@ -37,11 +37,7 @@ val hcons : t -> t val family_compare : family -> family -> int val family_equal : family -> family -> bool - -module List : sig - val mem : family -> family list -> bool - val intersect : family list -> family list -> family list -end +val family_leq : family -> family -> bool val univ_of_sort : t -> Univ.Universe.t val sort_of_univ : Univ.Universe.t -> t diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 088dd98db8..f984088f47 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -115,16 +115,8 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = } (** Definition [c] is opaque (Qed), non polymorphic and with a specified type, - so we delay the typing and hash consing of its body. - Remark: when the universe quantification is given explicitly, we could - delay even in the polymorphic case. *) + so we delay the typing and hash consing of its body. *) -(** Definition is opaque (Qed) and non polymorphic with known type, so we delay -the typing and hash consing of its body. - -TODO: if the universe quantification is given explicitly, we could delay even in -the polymorphic case - *) | DefinitionEntry ({ const_entry_type = Some typ; const_entry_opaque = true; const_entry_universes = Monomorphic_entry univs; _ } as c) -> @@ -165,16 +157,59 @@ the polymorphic case cook_context = c.const_entry_secctx; } + (** Similar case for polymorphic entries. TODO: also delay type-checking of + the body. *) + + | DefinitionEntry ({ const_entry_type = Some typ; + const_entry_opaque = true; + const_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) -> + let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in + let env = push_context ~strict:false uctx env in + let tj = Typeops.infer_type env typ in + let sbst, auctx = Univ.abstract_universes nas uctx in + let usubst = Univ.make_instance_subst sbst in + let (def, private_univs) = + let (body, ctx), side_eff = Future.join body in + let body, ctx = match trust with + | Pure -> body, ctx + | SideEffects handle -> + let body, ctx', _ = handle env body side_eff in + body, Univ.ContextSet.union ctx ctx' + in + (** [ctx] must contain local universes, such that it has no impact + on the rest of the graph (up to transitivity). *) + let env = push_subgraph ctx env in + let private_univs = on_snd (Univ.subst_univs_level_constraints usubst) ctx in + let j = Typeops.infer env body in + let _ = Typeops.judge_of_cast env j DEFAULTcast tj in + let def = Vars.subst_univs_level_constr usubst j.uj_val in + def, private_univs + in + let def = OpaqueDef (Future.from_val (def, Univ.ContextSet.empty)) in + let typ = Vars.subst_univs_level_constr usubst tj.utj_val in + feedback_completion_typecheck feedback_id; + { + Cooking.cook_body = def; + cook_type = typ; + cook_universes = Polymorphic auctx; + cook_private_univs = Some private_univs; + cook_relevance = Sorts.relevance_of_sort tj.utj_type; + cook_inline = c.const_entry_inline_code; + cook_context = c.const_entry_secctx; + } + (** Other definitions have to be processed immediately. *) | DefinitionEntry c -> - let { const_entry_type = typ; const_entry_opaque = opaque ; _ } = c in + let { const_entry_type = typ; _ } = c in let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in - let (body, ctx), side_eff = Future.join body in + (* Opaque constants must be provided with a non-empty const_entry_type, + and thus should have been treated above. *) + let () = assert (not c.const_entry_opaque) in let body, ctx = match trust with - | Pure -> body, ctx - | SideEffects handle -> - let body, ctx', _ = handle env body side_eff in - body, Univ.ContextSet.union ctx ctx' + | Pure -> + let (body, ctx), () = Future.join body in + body, ctx + | SideEffects _ -> assert false in let env, usubst, univs, private_univs = match c.const_entry_universes with | Monomorphic_entry univs -> @@ -188,9 +223,6 @@ the polymorphic case let sbst, auctx = Univ.abstract_universes nas uctx in let sbst = Univ.make_instance_subst sbst in let env, local = - if opaque then - push_subgraph ctx env, Some (on_snd (Univ.subst_univs_level_constraints sbst) ctx) - else if Univ.ContextSet.is_empty ctx then env, None else CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.") in @@ -206,10 +238,7 @@ the polymorphic case Vars.subst_univs_level_constr usubst tj.utj_val in let def = Vars.subst_univs_level_constr usubst j.uj_val in - let def = - if opaque then OpaqueDef (Future.from_val (def, Univ.ContextSet.empty)) - else Def (Mod_subst.from_val def) - in + let def = Def (Mod_subst.from_val def) in feedback_completion_typecheck feedback_id; { Cooking.cook_body = def; diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index c45fe1cf00..857e4fabf7 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -49,7 +49,7 @@ type ('constr, 'types) ptype_error = | BadAssumption of ('constr, 'types) punsafe_judgment | ReferenceVariables of Id.t * 'constr | ElimArity of pinductive * 'constr * ('constr, 'types) punsafe_judgment - * (Sorts.family list * Sorts.family * Sorts.family * arity_error) option + * (Sorts.family * Sorts.family * Sorts.family * arity_error) option | CaseNotInductive of ('constr, 'types) punsafe_judgment | WrongCaseInfo of pinductive * case_info | NumberBranches of ('constr, 'types) punsafe_judgment * int diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 88165a4f07..8e25236851 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -50,7 +50,7 @@ type ('constr, 'types) ptype_error = | BadAssumption of ('constr, 'types) punsafe_judgment | ReferenceVariables of Id.t * 'constr | ElimArity of pinductive * 'constr * ('constr, 'types) punsafe_judgment - * (Sorts.family list * Sorts.family * Sorts.family * arity_error) option + * (Sorts.family * Sorts.family * Sorts.family * arity_error) option | CaseNotInductive of ('constr, 'types) punsafe_judgment | WrongCaseInfo of pinductive * case_info | NumberBranches of ('constr, 'types) punsafe_judgment * int @@ -104,7 +104,7 @@ val error_reference_variables : env -> Id.t -> constr -> 'a val error_elim_arity : env -> pinductive -> constr -> unsafe_judgment -> - (Sorts.family list * Sorts.family * Sorts.family * arity_error) option -> 'a + (Sorts.family * Sorts.family * Sorts.family * arity_error) option -> 'a val error_case_not_inductive : env -> unsafe_judgment -> 'a diff --git a/library/lib.ml b/library/lib.ml index 4be288ed20..daa41eca65 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -474,9 +474,6 @@ let extract_hyps (secs,ohyps) = let instance_from_variable_context = List.map fst %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list -let named_of_variable_context = - List.map fst - let name_instance inst = (* FIXME: this should probably be done at an upper level, by storing the name information in the section data structure. *) diff --git a/library/lib.mli b/library/lib.mli index 5da76961a6..c19c3bf7fa 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -168,7 +168,6 @@ type abstr_info = private { } val instance_from_variable_context : variable_context -> Id.t array -val named_of_variable_context : variable_context -> Constr.named_context val section_segment_of_constant : Constant.t -> abstr_info val section_segment_of_mutual_inductive: MutInd.t -> abstr_info diff --git a/library/library.ml b/library/library.ml index 039124635e..e3b8511af1 100644 --- a/library/library.ml +++ b/library/library.ml @@ -281,13 +281,9 @@ type 'a table_status = let opaque_tables = ref (LibraryMap.empty : (Constr.constr table_status) LibraryMap.t) -let univ_tables = - ref (LibraryMap.empty : (Univ.ContextSet.t table_status) LibraryMap.t) let add_opaque_table dp st = opaque_tables := LibraryMap.add dp st !opaque_tables -let add_univ_table dp st = - univ_tables := LibraryMap.add dp st !univ_tables let access_table what tables dp i = let t = match LibraryMap.find dp !tables with @@ -312,15 +308,8 @@ let access_opaque_table dp i = let what = "opaque proofs" in access_table what opaque_tables dp i -let access_univ_table dp i = - try - let what = "universe contexts of opaque proofs" in - access_table what univ_tables dp i - with Not_found -> None - let indirect_accessor = { Opaqueproof.access_proof = access_opaque_table; - Opaqueproof.access_constraints = access_univ_table; } (************************************************************************) @@ -329,7 +318,7 @@ let indirect_accessor = { type seg_sum = summary_disk type seg_lib = library_disk type seg_univ = (* true = vivo, false = vi *) - Univ.ContextSet.t option array * Univ.ContextSet.t * bool + Univ.ContextSet.t * bool type seg_discharge = Opaqueproof.cooking_info list array type seg_proofs = Constr.constr option array @@ -363,11 +352,9 @@ let intern_from_file f = let open Safe_typing in match univs with | None -> mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty - | Some (utab,uall,true) -> - add_univ_table lsd.md_name (Fetched utab); + | Some (uall,true) -> mk_library lsd lmd (Dvivo (digest_lmd,digest_u)) uall - | Some (utab,_,false) -> - add_univ_table lsd.md_name (Fetched utab); + | Some (_,false) -> mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty module DPMap = Map.Make(DirPath) @@ -547,7 +534,7 @@ let load_library_todo f = 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 pi3 (Option.get s2) 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 (************************************************************************) @@ -591,7 +578,7 @@ 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, univ_table, disch_table, f2t_map = Opaqueproof.dump ~except otab in + let opaque_table, disch_table, f2t_map = Opaqueproof.dump ~except otab in let tasks, utab, dtab = match todo with | None -> None, None, None @@ -602,7 +589,7 @@ 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_table,Univ.ContextSet.empty,false), + Some (Univ.ContextSet.empty,false), Some disch_table in let sd = { md_name = dir; diff --git a/library/library.mli b/library/library.mli index 2c0673c3b1..142206e2c5 100644 --- a/library/library.mli +++ b/library/library.mli @@ -33,8 +33,8 @@ val require_library_from_dirpath (** Segments of a library *) type seg_sum type seg_lib -type seg_univ = (* cst, all_cst, finished? *) - Univ.ContextSet.t option array * Univ.ContextSet.t * bool +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 diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 216be3797b..de1b592337 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1489,8 +1489,6 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation } ) )) pstate in - (* (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *) -(* Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); *) let _ = Flags.silently (fun () -> Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:opacity ~idopt:None) () in () (* Pp.msgnl (fun _ _ -> str "eqn finished"); *) diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index aeceeb4e50..8e7b045b8e 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -153,9 +153,11 @@ let decl_constant na univs c = let open Constr in let vars = CVars.universes_of_constr c in let univs = UState.restrict_universe_context univs vars in - let univs = Monomorphic_entry univs in + let () = Declare.declare_universe_context false univs in + let types = (Typeops.infer (Global.env ()) c).uj_type in + let univs = Monomorphic_entry Univ.ContextSet.empty in mkConst(declare_constant (Id.of_string na) - (DefinitionEntry (definition_entry ~opaque:true ~univs c), + (DefinitionEntry (definition_entry ~opaque:true ~types ~univs c), IsProof Lemma)) (* Calling a global tactic *) diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 7615a17514..1c488a6974 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -84,7 +84,7 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = let () = if Option.is_empty projs then check_privacy_block mib in let () = - if not (Sorts.List.mem kind (elim_sorts specif)) then + if not (Sorts.family_leq kind (elim_sort specif)) then raise (RecursionSchemeError (env, NotAllowedCaseAnalysis (false, fst (UnivGen.fresh_sort_in_family kind), pind))) @@ -557,8 +557,8 @@ let weaken_sort_scheme env evd set sort npars term ty = let check_arities env listdepkind = let _ = List.fold_left (fun ln (((_,ni as mind),u),mibi,mipi,dep,kind) -> - let kelim = elim_sorts (mibi,mipi) in - if not (Sorts.List.mem kind kelim) then raise + let kelim = elim_sort (mibi,mipi) in + if not (Sorts.family_leq kind kelim) then raise (RecursionSchemeError (env, NotAllowedCaseAnalysis (true, fst (UnivGen.fresh_sort_in_family kind),(mind,u)))) else if Int.List.mem ni ln then raise diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index b1c98da2c7..12a7859b88 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -255,10 +255,13 @@ let inductive_has_local_defs env ind = let l2 = mib.mind_nparams + mip.mind_nrealargs in not (Int.equal l1 l2) -let allowed_sorts env (kn,i as ind) = +let top_allowed_sort env (kn,i as ind) = let (mib,mip) = Inductive.lookup_mind_specif env ind in mip.mind_kelim +let sorts_below top = + List.filter (fun s -> Sorts.family_leq s top) Sorts.[InSProp;InProp;InSet;InType] + let has_dependent_elim mib = match mib.mind_record with | PrimRecord _ -> mib.mind_finite == BiFinite diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index cfc650938e..aacbecf6c7 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -141,7 +141,9 @@ val constructor_nrealdecls_env : env -> constructor -> int val constructor_has_local_defs : env -> constructor -> bool val inductive_has_local_defs : env -> inductive -> bool -val allowed_sorts : env -> inductive -> Sorts.family list +val sorts_below : Sorts.family -> Sorts.family list + +val top_allowed_sort : env -> inductive -> Sorts.family (** (Co)Inductive records with primitive projections do not have eta-conversion, hence no dependent elimination. *) diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index a9e2b0ea8f..25e56602a5 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -107,7 +107,7 @@ val error_ill_typed_rec_body : val error_elim_arity : ?loc:Loc.t -> env -> Evd.evar_map -> pinductive -> constr -> - unsafe_judgment -> (Sorts.family list * Sorts.family * Sorts.family * arity_error) option -> 'b + unsafe_judgment -> (Sorts.family * Sorts.family * Sorts.family * arity_error) option -> 'b val error_not_a_type : ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index f2b8671a48..c7b657f96c 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -52,6 +52,18 @@ type typing_constraint = OfType of types | IsType | WithoutTypeConstraint let (!!) env = GlobEnv.env env +let bidi_hints = + Summary.ref (GlobRef.Map.empty : int GlobRef.Map.t) ~name:"bidirectionalityhints" + +let add_bidirectionality_hint gr n = + bidi_hints := GlobRef.Map.add gr n !bidi_hints + +let get_bidirectionality_hint gr = + GlobRef.Map.find_opt gr !bidi_hints + +let clear_bidirectionality_hint gr = + bidi_hints := GlobRef.Map.remove gr !bidi_hints + (************************************************************************) (* This concerns Cases *) open Inductive @@ -635,24 +647,36 @@ let rec pretype ~program_mode ~poly resolve_tc (tycon : type_constraint) (env : let sigma, fj = pretype empty_tycon env sigma f in let floc = loc_of_glob_constr f in let length = List.length args in + let nargs_before_bidi = + (* if `f` is a global, we retrieve bidirectionality hints *) + try + let (gr,_) = destRef sigma fj.uj_val in + Option.default length @@ GlobRef.Map.find_opt gr !bidi_hints + with DestKO -> + length + in let candargs = - (* Bidirectional typechecking hint: - parameters of a constructor are completely determined - by a typing constraint *) + (* Bidirectional typechecking hint: + parameters of a constructor are completely determined + by a typing constraint *) + (* This bidirectionality machinery is the one of `Program` for + constructors and is orthogonal to bidirectionality hints. However, we + could probably factorize both by providing default bidirectionality hints + for constructors corresponding to their number of parameters. *) if program_mode && length > 0 && isConstruct sigma fj.uj_val then - match tycon with - | None -> [] - | Some ty -> + match tycon with + | None -> [] + | Some ty -> let ((ind, i), u) = destConstruct sigma fj.uj_val in let npars = inductive_nparams !!env ind in - if Int.equal npars 0 then [] - else - try - let IndType (indf, args) = find_rectype !!env sigma ty in - let ((ind',u'),pars) = dest_ind_family indf in - if eq_ind ind ind' then List.map EConstr.of_constr pars - else (* Let the usual code throw an error *) [] - with Not_found -> [] + if Int.equal npars 0 then [] + else + try + let IndType (indf, args) = find_rectype !!env sigma ty in + let ((ind',u'),pars) = dest_ind_family indf in + if eq_ind ind ind' then List.map EConstr.of_constr pars + else (* Let the usual code throw an error *) [] + with Not_found -> [] else [] in let app_f = @@ -662,20 +686,29 @@ let rec pretype ~program_mode ~poly resolve_tc (tycon : type_constraint) (env : let p = Projection.make p false in let npars = Projection.npars p in fun n -> - if n == npars + 1 then fun _ v -> mkProj (p, v) + if Int.equal n npars then fun _ v -> mkProj (p, v) else fun f v -> applist (f, [v]) | _ -> fun _ f v -> applist (f, [v]) in - let rec apply_rec env sigma n resj candargs = function - | [] -> sigma, resj + let rec apply_rec env sigma n resj candargs bidiargs = function + | [] -> sigma, resj, List.rev bidiargs | c::rest -> + let bidi = n >= nargs_before_bidi in let argloc = loc_of_glob_constr c in let sigma, resj = Coercion.inh_app_fun ~program_mode resolve_tc !!env sigma resj in let resty = whd_all !!env sigma resj.uj_type in match EConstr.kind sigma resty with | Prod (na,c1,c2) -> let tycon = Some c1 in - let sigma, hj = pretype tycon env sigma c in + let (sigma, hj), bidiargs = + if bidi && Option.has_some tycon then + (* We want to get some typing information from the context before + typing the argument, so we replace it by an existential + variable *) + let sigma, c_hole = new_evar env sigma ~src:(loc,Evar_kinds.InternalHole) c1 in + (sigma, make_judge c_hole c1), (c_hole, c) :: bidiargs + else pretype tycon env sigma c, bidiargs + in let sigma, candargs, ujval = match candargs with | [] -> sigma, [], j_val hj @@ -687,30 +720,45 @@ let rec pretype ~program_mode ~poly resolve_tc (tycon : type_constraint) (env : sigma, args, nf_evar sigma (j_val hj) end in - let sigma, ujval = adjust_evar_source sigma na.binder_name ujval in - let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in - let j = { uj_val = value; uj_type = typ } in - apply_rec env sigma (n+1) j candargs rest - | _ -> - let sigma, hj = pretype empty_tycon env sigma c in - error_cant_apply_not_functional - ?loc:(Loc.merge_opt floc argloc) !!env sigma resj [|hj|] + let sigma, ujval = adjust_evar_source sigma na.binder_name ujval in + let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in + let j = { uj_val = value; uj_type = typ } in + apply_rec env sigma (n+1) j candargs bidiargs rest + | _ -> + let sigma, hj = pretype empty_tycon env sigma c in + error_cant_apply_not_functional + ?loc:(Loc.merge_opt floc argloc) !!env sigma resj [|hj|] in - let sigma, resj = apply_rec env sigma 1 fj candargs args in + let sigma, resj, bidiargs = apply_rec env sigma 0 fj candargs [] args in let sigma, resj = match EConstr.kind sigma resj.uj_val with | App (f,args) -> - if Termops.is_template_polymorphic_ind !!env sigma f then - (* Special case for inductive type applications that must be - refreshed right away. *) - let c = mkApp (f, args) in - let sigma, c = Evarsolve.refresh_universes (Some true) !!env sigma c in - let t = Retyping.get_type_of !!env sigma c in - sigma, make_judge c (* use this for keeping evars: resj.uj_val *) t - else sigma, resj + if Termops.is_template_polymorphic_ind !!env sigma f then + (* Special case for inductive type applications that must be + refreshed right away. *) + let c = mkApp (f, args) in + let sigma, c = Evarsolve.refresh_universes (Some true) !!env sigma c in + let t = Retyping.get_type_of !!env sigma c in + sigma, make_judge c (* use this for keeping evars: resj.uj_val *) t + else sigma, resj | _ -> sigma, resj in - inh_conv_coerce_to_tycon ?loc env sigma resj tycon + let sigma, t = inh_conv_coerce_to_tycon ?loc env sigma resj tycon in + let refine_arg sigma (newarg,origarg) = + (* Refine an argument (originally `origarg`) represented by an evar + (`newarg`) to use typing information from the context *) + (* Recover the expected type of the argument *) + let ty = Retyping.get_type_of !!env sigma newarg in + (* Type the argument using this expected type *) + let sigma, j = pretype (Some ty) env sigma origarg in + (* Unify the (possibly refined) existential variable with the + (typechecked) original value *) + Evarconv.unify_delay !!env sigma newarg (j_val j) + in + (* We now refine any arguments whose typing was delayed for + bidirectionality *) + let sigma = List.fold_left refine_arg sigma bidiargs in + (sigma, t) | GLambda(name,bk,c1,c2) -> let sigma, tycon' = diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 1037cf6cc5..c0a95e73c6 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -14,12 +14,22 @@ into elementary ones, insertion of coercions and resolution of implicit arguments. *) +open Names open Environ open Evd open EConstr open Glob_term open Ltac_pretype +val add_bidirectionality_hint : GlobRef.t -> int -> unit +(** A bidirectionality hint `n` for a global `g` tells the pretyper to use + typing information from the context after typing the `n` for arguments of an + application of `g`. *) + +val get_bidirectionality_hint : GlobRef.t -> int option + +val clear_bidirectionality_hint : GlobRef.t -> unit + val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map -> glob_level -> Univ.Level.t diff --git a/pretyping/typing.ml b/pretyping/typing.ml index be71f44a5e..00c52e7665 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -117,12 +117,12 @@ let check_branch_types env sigma (ind,u) cj (lfj,explft) = sigma lfj explft let max_sort l = - if Sorts.List.mem InType l then InType else - if Sorts.List.mem InSet l then InSet else InProp + if List.mem_f Sorts.family_equal InType l then InType else + if List.mem_f Sorts.family_equal InSet l then InSet else InProp let is_correct_arity env sigma c pj ind specif params = let arsign = make_arity_signature env sigma true (make_ind_family (ind,params)) in - let allowed_sorts = elim_sorts specif in + let allowed_sorts = sorts_below (elim_sort specif) in let error () = Pretype_errors.error_elim_arity env sigma ind c pj None in let rec srec env sigma pt ar = let pt' = whd_all env sigma pt in @@ -135,7 +135,7 @@ let is_correct_arity env sigma c pj ind specif params = end | Sort s, [] -> let s = ESorts.kind sigma s in - if not (Sorts.List.mem (Sorts.family s) allowed_sorts) + if not (List.mem_f Sorts.family_equal (Sorts.family s) allowed_sorts) then error () else sigma, s | Evar (ev,_), [] -> @@ -199,13 +199,13 @@ let check_type_fixpoint ?loc env sigma lna lar vdefj = (* FIXME: might depend on the level of actual parameters!*) let check_allowed_sort env sigma ind c p = let specif = lookup_mind_specif env (fst ind) in - let sorts = elim_sorts specif in + let sorts = elim_sort specif in let pj = Retyping.get_judgment_of env sigma p in let _, s = splay_prod env sigma pj.uj_type in let ksort = match EConstr.kind sigma s with | Sort s -> Sorts.family (ESorts.kind sigma s) | _ -> error_elim_arity env sigma ind c pj None in - if not (List.exists ((==) ksort) sorts) then + if not (Sorts.family_leq ksort sorts) then let s = inductive_sort_family (snd specif) in error_elim_arity env sigma ind c pj (Some(sorts,ksort,s,Type_errors.error_elim_explain ksort s)) diff --git a/printing/prettyp.ml b/printing/prettyp.ml index fca33a24bf..f55bfb504f 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -304,6 +304,12 @@ let print_inductive_argument_scopes = print_args_data_of_inductive_ids Notation.find_arguments_scope (Option.has_some) print_argument_scopes +let print_bidi_hints gr = + match Pretyping.get_bidirectionality_hint gr with + | None -> [] + | Some nargs -> + [str "Using typing information from context after typing the " ++ int nargs ++ str " first arguments"] + (*********************) (* "Locate" commands *) @@ -841,7 +847,8 @@ let print_about_any ?loc env sigma k udecl = print_name_infos ref @ (if Pp.ismt rb then [] else [rb]) @ print_opacity ref @ - [hov 0 (str "Expands to: " ++ pr_located_qualid k)]) + print_bidi_hints ref @ + [hov 0 (str "Expands to: " ++ pr_located_qualid k)]) | Syntactic kn -> let () = match Syntax_def.search_syntactic_definition kn with | [],Notation_term.NRef ref -> Dumpglob.add_glob ?loc ref diff --git a/stm/stm.ml b/stm/stm.ml index e32b6c9f1c..b2bfa552b4 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1060,99 +1060,6 @@ end = struct (* {{{ *) end (* }}} *) -(* indentation code for Show Script, initially contributed - * by D. de Rauglaudre. Should be moved away. - *) - -module ShowScript = struct - -let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) = - (* ng1 : number of goals remaining at the current level (before cmd) - ngl1 : stack of previous levels with their remaining goals - ng : number of goals after the execution of cmd - beginend : special indentation stack for { } *) - let ngprev = List.fold_left (+) ng1 ngl1 in - let new_ngl = - if ng > ngprev then - (* We've branched *) - (ng - ngprev + 1, ng1 - 1 :: ngl1) - else if ng < ngprev then - (* A subgoal have been solved. Let's compute the new current level - by discarding all levels with 0 remaining goals. *) - let rec loop = function - | (0, ng2::ngl2) -> loop (ng2,ngl2) - | p -> p - in loop (ng1-1, ngl1) - else - (* Standard case, same goal number as before *) - (ng1, ngl1) - in - (* When a subgoal have been solved, separate this block by an empty line *) - let new_nl = (ng < ngprev) - in - (* Indentation depth *) - let ind = List.length ngl1 - in - (* Some special handling of bullets and { }, to get a nicer display *) - let pred n = max 0 (n-1) in - let ind, nl, new_beginend = match Vernacprop.under_control cmd with - | VernacSubproof _ -> pred ind, nl, (pred ind)::beginend - | VernacEndSubproof -> List.hd beginend, false, List.tl beginend - | VernacBullet _ -> pred ind, nl, beginend - | _ -> ind, nl, beginend - in - let pp = Pp.( - (if nl then fnl () else mt ()) ++ - (hov (ind+1) (str (String.make ind ' ') ++ Ppvernac.pr_vernac cmd))) - in - (new_ngl, new_nl, new_beginend, pp :: ppl) - -let get_script prf = - let branch, test = - match prf with - | None -> VCS.Branch.master, fun _ -> true - | Some name -> VCS.current_branch (),fun nl -> nl=[] || List.mem name nl in - let rec find acc id = - if Stateid.equal id Stateid.initial || - Stateid.equal id Stateid.dummy then acc else - let view = VCS.visit id in - match view.step with - | `Fork((_,_,_,ns), _) when test ns -> acc - | `Qed (qed, proof) -> find [qed.qast.expr, (VCS.get_info id).n_goals] proof - | `Sideff (ReplayCommand x,_) -> - find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next - | `Sideff (CherryPickEnv, id) -> find acc id - | `Cmd {cast = x; ctac} when ctac -> (* skip non-tactics *) - find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next - | `Cmd _ -> find acc view.next - | `Alias (id,_) -> find acc id - | `Fork _ -> find acc view.next - in - find [] (VCS.get_branch_pos branch) - -let warn_show_script_deprecated = - CWarnings.create ~name:"deprecated-show-script" ~category:"deprecated" - (fun () -> Pp.str "The “Show Script” command is deprecated.") - -let show_script ?proof () = - warn_show_script_deprecated (); - try - let prf = - try match proof with - | None -> Some (PG_compat.get_current_proof_name ()) - | Some (p,_) -> Some (p.Proof_global.id) - with PG_compat.NoCurrentProof -> None - in - let cmds = get_script prf in - let _,_,_,indented_cmds = - List.fold_left indent_script_item ((1,[]),false,[],[]) cmds - in - let indented_cmds = List.rev (indented_cmds) in - msg_notice Pp.(v 0 (prlist_with_sep fnl (fun x -> x) indented_cmds)) - with Vcs_aux.Expired -> () - -end - (* Wrapper for Vernacentries.interp to set the feedback id *) (* It is currently called 19 times, this number should be certainly reduced... *) @@ -1172,21 +1079,17 @@ let stm_vernac_interp ?proof ?route id st { verbose; expr } : Vernacstate.t = | VernacAbortAll | VernacAbort _ -> true | _ -> false in - let aux_interp st expr = - (* XXX unsupported attributes *) - let cmd = Vernacprop.under_control expr in - if is_filtered_command cmd then - (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st) - else - match cmd with - | VernacShow ShowScript -> ShowScript.show_script (); st (* XX we are ignoring control here *) - | _ -> - stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr); - try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st expr - with e -> - let e = CErrors.push e in - Exninfo.iraise Hooks.(call_process_error_once e) - in aux_interp st expr + (* XXX unsupported attributes *) + let cmd = Vernacprop.under_control expr in + if is_filtered_command cmd then + (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st) + else begin + stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr); + try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st expr + with e -> + let e = CErrors.push e in + Exninfo.iraise Hooks.(call_process_error_once e) + end (****************************** CRUFT *****************************************) (******************************************************************************) @@ -1819,15 +1722,15 @@ end = struct (* {{{ *) str (Printexc.to_string e))); if drop then `ERROR_ADMITTED else `ERROR - let finish_task name (u,cst,_) d p l i = + let finish_task name (cst,_) d p l i = let { Stateid.uuid = bucket }, drop = List.nth l i in let bucket_name = if bucket < 0 then (assert drop; ", no bucket") else Printf.sprintf ", bucket %d" bucket in match check_task_aux bucket_name name l i with | `ERROR -> exit 1 - | `ERROR_ADMITTED -> u, cst, false - | `OK_ADMITTED -> u, cst, false + | `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 = @@ -1846,9 +1749,8 @@ end = struct (* {{{ *) let pr = map (Option.get (Global.body_of_constant_body Library.indirect_accessor c)) in let pr = discharge pr in let pr = Constr.hcons pr in - u.(bucket) <- Some uc; p.(bucket) <- Some pr; - u, Univ.ContextSet.union cst uc, false + Univ.ContextSet.union cst uc, false let check_task name l i = match check_task_aux "" name l i with @@ -2851,8 +2753,8 @@ let finish_tasks name u d p (t,rcbackup as tasks) = VCS.restore vcs; u in try - let u, a, _ = List.fold_left finish_task u (info_tasks tasks) in - (u,a,true), p + let a, _ = List.fold_left finish_task u (info_tasks tasks) in + (a,true), p with e -> let e = CErrors.push e in msg_warning (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e); diff --git a/tactics/equality.ml b/tactics/equality.ml index 45a4799ea1..51eee2a053 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -735,7 +735,7 @@ let find_positions env sigma ~keep_proofs ~no_discr t1 t2 = let project env sorts posn t1 t2 = let ty1 = get_type_of env sigma t1 in let s = get_sort_family_of ~truncation_style:true env sigma ty1 in - if Sorts.List.mem s sorts + if List.mem_f Sorts.family_equal s sorts then [(List.rev posn,t1,t2)] else [] in let rec findrec sorts posn t1 t2 = @@ -746,7 +746,7 @@ let find_positions env sigma ~keep_proofs ~no_discr t1 t2 = when Int.equal (List.length args1) (constructor_nallargs env sp1) -> let sorts' = - Sorts.List.intersect sorts (allowed_sorts env (fst sp1)) + CList.intersect Sorts.family_equal sorts (sorts_below (top_allowed_sort env (fst sp1))) in (* both sides are fully applied constructors, so either we descend, or we can discriminate here. *) @@ -762,7 +762,7 @@ let find_positions env sigma ~keep_proofs ~no_discr t1 t2 = List.flatten (List.map2_i (fun i -> findrec sorts' ((sp1,adjust i)::posn)) 0 rargs1 rargs2) - else if Sorts.List.mem InType sorts' && not no_discr + else if List.mem_f Sorts.family_equal InType sorts' && not no_discr then (* see build_discriminator *) raise (DiscrFound (List.rev posn,sp1,sp2)) else diff --git a/test-suite/Makefile b/test-suite/Makefile index 94011447d7..552d007f85 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -561,7 +561,6 @@ $(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG) export coqc="$(coqc)"; \ export coqtop="$(coqc)"; \ export coqdep="$(coqdep)"; \ - export coqtopbyte="$(coqtopbyte)"; \ "$<" 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ diff --git a/test-suite/misc/printers.sh b/test-suite/misc/printers.sh index ef3f056d89..f659fce680 100755 --- a/test-suite/misc/printers.sh +++ b/test-suite/misc/printers.sh @@ -1,2 +1,8 @@ #!/bin/sh -if printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | grep -E "Error|Unbound" ; then exit 1; else exit 0; fi + +command -v "${BIN}coqtop.byte" || { echo "Missing coqtop.byte"; exit 1; } + +f=$(mktemp) +printf 'Drop. #use"include";; #quit;;\n' | "${BIN}coqtop.byte" -q 2>&1 | tee "$f" + +if grep -q -E "Error|Unbound" "$f"; then exit 1; fi diff --git a/test-suite/success/BidirectionalityHints.v b/test-suite/success/BidirectionalityHints.v new file mode 100644 index 0000000000..284cdc871b --- /dev/null +++ b/test-suite/success/BidirectionalityHints.v @@ -0,0 +1,114 @@ +From Coq Require Import Utf8. +Set Default Proof Using "Type". + +Module SimpleExamples. + +Axiom c : bool -> nat. +Coercion c : bool >-> nat. +Inductive Boxed A := Box (a : A). +Arguments Box {A} & a. +Check Box true : Boxed nat. + +(* Here we check that there is no regression due e.g. to refining arguments + in the wrong order *) +Axiom f : forall b : bool, (if b then bool else nat) -> Type. +Check f true true : Type. +Arguments f & _ _. +Check f true true : Type. + +End SimpleExamples. + +Module Issue7910. + +Local Set Universe Polymorphism. + +(** Telescopes *) +Inductive tele : Type := + | TeleO : tele + | TeleS {X} (binder : X → tele) : tele. + +Arguments TeleS {_} _. + +(** The telescope version of Coq's function type *) +Fixpoint tele_fun (TT : tele) (T : Type) : Type := + match TT with + | TeleO => T + | TeleS b => ∀ x, tele_fun (b x) T + end. + +Notation "TT -t> A" := + (tele_fun TT A) (at level 99, A at level 200, right associativity). + +(** An eliminator for elements of [tele_fun]. + We use a [fix] because, for some reason, that makes stuff print nicer + in the proofs in iris:bi/lib/telescopes.v *) +Definition tele_fold {X Y} {TT : tele} (step : ∀ {A : Type}, (A → Y) → Y) (base : X → Y) + : (TT -t> X) → Y := + (fix rec {TT} : (TT -t> X) → Y := + match TT as TT return (TT -t> X) → Y with + | TeleO => λ x : X, base x + | TeleS b => λ f, step (λ x, rec (f x)) + end) TT. +Arguments tele_fold {_ _ !_} _ _ _ /. + +(** A sigma-like type for an "element" of a telescope, i.e. the data it + takes to get a [T] from a [TT -t> T]. *) +Inductive tele_arg : tele → Type := +| TargO : tele_arg TeleO +(* the [x] is the only relevant data here *) +| TargS {X} {binder} (x : X) : tele_arg (binder x) → tele_arg (TeleS binder). + +Definition tele_app {TT : tele} {T} (f : TT -t> T) : tele_arg TT → T := + λ a, (fix rec {TT} (a : tele_arg TT) : (TT -t> T) → T := + match a in tele_arg TT return (TT -t> T) → T with + | TargO => λ t : T, t + | TargS x a => λ f, rec a (f x) + end) TT a f. +Arguments tele_app {!_ _} & _ !_ /. + +Coercion tele_arg : tele >-> Sortclass. +Coercion tele_app : tele_fun >-> Funclass. + +(** Operate below [tele_fun]s with argument telescope [TT]. *) +Fixpoint tele_bind {U} {TT : tele} : (TT → U) → TT -t> U := + match TT as TT return (TT → U) → TT -t> U with + | TeleO => λ F, F TargO + | @TeleS X b => λ (F : TeleS b → U) (x : X), (* b x -t> U *) + tele_bind (λ a, F (TargS x a)) + end. +Arguments tele_bind {_ !_} _ /. + +(** Telescopic quantifiers *) +Definition tforall {TT : tele} (Ψ : TT → Prop) : Prop := + tele_fold (λ (T : Type) (b : T → Prop), ∀ x : T, b x) (λ x, x) (tele_bind Ψ). +Arguments tforall {!_} _ /. +Definition texist {TT : tele} (Ψ : TT → Prop) : Prop := + tele_fold ex (λ x, x) (tele_bind Ψ). +Arguments texist {!_} _ /. + +Notation "'∀..' x .. y , P" := (tforall (λ x, .. (tforall (λ y, P)) .. )) + (at level 200, x binder, y binder, right associativity, + format "∀.. x .. y , P"). +Notation "'∃..' x .. y , P" := (texist (λ x, .. (texist (λ y, P)) .. )) + (at level 200, x binder, y binder, right associativity, + format "∃.. x .. y , P"). + +(** The actual test case *) +Definition test {TT : tele} (t : TT → Prop) : Prop := + ∀.. x, t x ∧ t x. + +Notation "'[TEST' x .. z , P ']'" := + (test (TT:=(TeleS (fun x => .. (TeleS (fun z => TeleO)) ..))) + (tele_app (λ x, .. (λ z, P) ..))) + (x binder, z binder). +Notation "'[TEST2' x .. z , P ']'" := + (test (TT:=(TeleS (fun x => .. (TeleS (fun z => TeleO)) ..))) + (tele_app (TT:=(TeleS (fun x => .. (TeleS (fun z => TeleO)) ..))) + (λ x, .. (λ z, P) ..))) + (x binder, z binder). + +Check [TEST (x y : nat), x = y]. + +Check [TEST2 (x y : nat), x = y]. + +End Issue7910. diff --git a/test-suite/vio/section.v b/test-suite/vio/section.v new file mode 100644 index 0000000000..0e7722516a --- /dev/null +++ b/test-suite/vio/section.v @@ -0,0 +1,12 @@ +Section Foo. + Variable A : Type. + + Definition bla := A. + + Variable B : bla. + + Lemma blu : {X:Type & X}. + Proof using A B. + exists bla;exact B. + Qed. +End Foo. diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 528829f3a5..5aec5cac2c 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -331,8 +331,8 @@ let build_beq_scheme mode kn = eff := Safe_typing.concat_private eff' !eff done; (Array.init nb_ind (fun i -> - let kelim = Inductive.elim_sorts (mib,mib.mind_packets.(i)) in - if not (Sorts.List.mem InSet kelim) then + let kelim = Inductive.elim_sort (mib,mib.mind_packets.(i)) in + if not (Sorts.family_leq InSet kelim) then raise (NonSingletonProp (kn,i)); let fix = match mib.mind_finite with | CoFinite -> diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg index ecc7d3ff88..ea35ea782d 100644 --- a/vernac/g_proofs.mlg +++ b/vernac/g_proofs.mlg @@ -88,7 +88,6 @@ GRAMMAR EXTEND Gram | IDENT "Show" -> { VernacShow (ShowGoal OpenSubgoals) } | IDENT "Show"; n = natural -> { VernacShow (ShowGoal (NthGoal n)) } | IDENT "Show"; id = ident -> { VernacShow (ShowGoal (GoalId id)) } - | IDENT "Show"; IDENT "Script" -> { VernacShow ShowScript } | IDENT "Show"; IDENT "Existentials" -> { VernacShow ShowExistentials } | IDENT "Show"; IDENT "Universes" -> { VernacShow ShowUniverses } | IDENT "Show"; IDENT "Conjectures" -> { VernacShow ShowProofNames } diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 7c8c2b10ab..5eec8aed1e 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -752,6 +752,7 @@ GRAMMAR EXTEND Gram mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> { l } ] -> { let mods = match mods with None -> [] | Some l -> List.flatten l in let slash_position = ref None in + let ampersand_position = ref None in let rec parse_args i = function | [] -> [] | `Id x :: args -> x :: parse_args (i+1) args @@ -760,10 +761,15 @@ GRAMMAR EXTEND Gram (slash_position := Some i; parse_args i args) else user_err Pp.(str "The \"/\" modifier can occur only once") + | `Ampersand :: args -> + if Option.is_empty !ampersand_position then + (ampersand_position := Some i; parse_args i args) + else + user_err Pp.(str "The \"&\" modifier can occur only once") in let args = parse_args 0 (List.flatten args) in let more_implicits = Option.default [] more_implicits in - VernacArguments (qid, args, more_implicits, !slash_position, mods) } + VernacArguments (qid, args, more_implicits, !slash_position, !ampersand_position, mods) } | IDENT "Implicit"; "Type"; bl = reserv_list -> { VernacReserve bl } @@ -785,6 +791,7 @@ GRAMMAR EXTEND Gram | IDENT "default"; IDENT "implicits" -> { [`DefaultImplicits] } | IDENT "clear"; IDENT "implicits" -> { [`ClearImplicits] } | IDENT "clear"; IDENT "scopes" -> { [`ClearScopes] } + | IDENT "clear"; IDENT "bidirectionality"; IDENT "hint" -> { [`ClearBidiHint] } | IDENT "rename" -> { [`Rename] } | IDENT "assert" -> { [`Assert] } | IDENT "extra"; IDENT "scopes" -> { [`ExtraScopes] } @@ -810,6 +817,7 @@ GRAMMAR EXTEND Gram notation_scope=notation_scope; implicit_status = NotImplicit}] } | "/" -> { [`Slash] } + | "&" -> { [`Ampersand] } | "("; items = LIST1 argument_spec; ")"; sc = OPT scope -> { let f x = match sc, x with | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x diff --git a/vernac/himsg.ml b/vernac/himsg.ml index b2382ce6fc..a1f7835cbe 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -219,6 +219,7 @@ let explain_elim_arity env sigma ind c pj okinds = let pc = pr_leconstr_env env sigma c in let msg = match okinds with | Some(sorts,kp,ki,explanation) -> + let sorts = Inductiveops.sorts_below sorts in let pki = Sorts.pr_sort_family ki in let pkp = Sorts.pr_sort_family kp in let explanation = match explanation with diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 6ac259b1fe..de7d2fd49a 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -216,11 +216,11 @@ let declare_one_case_analysis_scheme ind = else if not (Inductiveops.has_dependent_elim mib) then case_scheme_kind_from_type else case_dep_scheme_kind_from_type in - let kelim = elim_sorts (mib,mip) in + let kelim = elim_sort (mib,mip) in (* in case the inductive has a type elimination, generates only one induction scheme, the other ones share the same code with the appropriate type *) - if Sorts.List.mem InType kelim then + if Sorts.family_leq InType kelim then ignore (define_individual_scheme dep UserAutomaticRequest None ind) (* Induction/recursion schemes *) @@ -248,16 +248,17 @@ let declare_one_induction_scheme ind = let kind = inductive_sort_family mip in let from_prop = kind == InProp in let depelim = Inductiveops.has_dependent_elim mib in - let kelim = elim_sorts (mib,mip) in + let kelim = Inductiveops.sorts_below (elim_sort (mib,mip)) in let kelim = if Global.sprop_allowed () then kelim else List.filter (fun s -> s <> InSProp) kelim in let elims = List.map_filter (fun (sort,kind) -> - if Sorts.List.mem sort kelim then Some kind else None) + if List.mem_f Sorts.family_equal sort kelim then Some kind else None) (if from_prop then kinds_from_prop else if depelim then kinds_from_type - else nondep_kinds_from_type) in + else nondep_kinds_from_type) + in List.iter (fun kind -> ignore (define_individual_scheme kind UserAutomaticRequest None ind)) elims diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 2e97a169cc..535a0fa02c 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -628,7 +628,6 @@ open Pputils let pr_showable = function | ShowGoal n -> keyword "Show" ++ pr_goal_reference n | ShowProof -> keyword "Show Proof" - | ShowScript -> keyword "Show Script" | ShowExistentials -> keyword "Show Existentials" | ShowUniverses -> keyword "Show Universes" | ShowProofNames -> keyword "Show Conjectures" @@ -1047,7 +1046,7 @@ open Pputils | Some Flags.Current -> [SetOnlyParsing] | Some v -> [SetCompatVersion v])) ) - | VernacArguments (q, args, more_implicits, nargs, mods) -> + | VernacArguments (q, args, more_implicits, nargs, nargs_before_bidi, mods) -> return ( hov 2 ( keyword "Arguments" ++ spc() ++ @@ -1058,22 +1057,23 @@ open Pputils | Impargs.Implicit -> str "[" ++ x ++ str "]" | Impargs.MaximallyImplicit -> str "{" ++ x ++ str "}" | Impargs.NotImplicit -> x in - let rec print_arguments n l = - match n, l with - | Some 0, l -> spc () ++ str"/" ++ print_arguments None l - | _, [] -> mt() - | n, { name = id; recarg_like = k; + let rec print_arguments n nbidi l = + match n, nbidi, l with + | Some 0, _, l -> spc () ++ str"/" ++ print_arguments None nbidi l + | _, Some 0, l -> spc () ++ str"|" ++ print_arguments n None l + | _, _, [] -> mt() + | n, nbidi, { name = id; recarg_like = k; notation_scope = s; implicit_status = imp } :: tl -> spc() ++ pr_br imp (pr_if k (str"!") ++ Name.print id ++ pr_s s) ++ - print_arguments (Option.map pred n) tl + print_arguments (Option.map pred n) (Option.map pred nbidi) tl in let rec print_implicits = function | [] -> mt () | (name, impl) :: rest -> spc() ++ pr_br impl (Name.print name) ++ print_implicits rest in - print_arguments nargs args ++ + print_arguments nargs nargs_before_bidi args ++ if not (List.is_empty more_implicits) then prlist (fun l -> str"," ++ print_implicits l) more_implicits else (mt ()) ++ @@ -1086,7 +1086,8 @@ open Pputils | `Assert -> keyword "assert" | `ExtraScopes -> keyword "extra scopes" | `ClearImplicits -> keyword "clear implicits" - | `ClearScopes -> keyword "clear scopes") + | `ClearScopes -> keyword "clear scopes" + | `ClearBidiHint -> keyword "clear bidirectionality hint") mods) ) | VernacReserve bl -> diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 5ae572541e..337cb233a2 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1204,6 +1204,36 @@ let vernac_syntactic_definition ~module_local lid x y = Dumpglob.dump_definition lid false "syndef"; Metasyntax.add_syntactic_definition (Global.env()) lid.v x module_local y +let cache_bidi_hints (_name, (gr, ohint)) = + match ohint with + | None -> Pretyping.clear_bidirectionality_hint gr + | Some nargs -> Pretyping.add_bidirectionality_hint gr nargs + +let load_bidi_hints _ r = + cache_bidi_hints r + +let subst_bidi_hints (subst, (gr, ohint as orig)) = + let gr' = subst_global_reference subst gr in + if gr == gr' then orig else (gr', ohint) + +let discharge_bidi_hints (_name, (gr, ohint)) = + if isVarRef gr && Lib.is_in_section gr then None + else + let vars = Lib.variable_section_segment_of_reference gr in + let n = List.length vars in + Some (gr, Option.map ((+) n) ohint) + +let inBidiHints = + let open Libobject in + declare_object { (default_object "BIDIRECTIONALITY-HINTS" ) with + load_function = load_bidi_hints; + cache_function = cache_bidi_hints; + classify_function = (fun o -> Substitute o); + subst_function = subst_bidi_hints; + discharge_function = discharge_bidi_hints; + } + + let warn_arguments_assert = CWarnings.create ~name:"arguments-assert" ~category:"vernacular" (fun sr -> @@ -1216,7 +1246,7 @@ let warn_arguments_assert = (* [nargs_for_red] is the number of arguments required to trigger reduction, [args] is the main list of arguments statuses, [more_implicits] is a list of extra lists of implicit statuses *) -let vernac_arguments ~section_local reference args more_implicits nargs_for_red flags = +let vernac_arguments ~section_local reference args more_implicits nargs_for_red nargs_before_bidi flags = let env = Global.env () in let sigma = Evd.from_env env in let assert_flag = List.mem `Assert flags in @@ -1227,6 +1257,7 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red let default_implicits_flag = List.mem `DefaultImplicits flags in let never_unfold_flag = List.mem `ReductionNeverUnfold flags in let nomatch_flag = List.mem `ReductionDontExposeCase flags in + let clear_bidi_hint = List.mem `ClearBidiHint flags in let err_incompat x y = user_err Pp.(str ("Options \""^x^"\" and \""^y^"\" are incompatible.")) in @@ -1285,6 +1316,9 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red if Option.cata (fun n -> n > num_args) false nargs_for_red then user_err Pp.(str "The \"/\" modifier should be put before any extra scope."); + if Option.cata (fun n -> n > num_args) false nargs_before_bidi then + user_err Pp.(str "The \"&\" modifier should be put before any extra scope."); + let scopes_specified = List.exists Option.has_some scopes in if scopes_specified && clear_scopes_flag then @@ -1396,6 +1430,12 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red let red_modifiers_specified = Option.has_some red_behavior in + let bidi_hint_specified = Option.has_some nargs_before_bidi in + + if bidi_hint_specified && clear_bidi_hint then + err_incompat "clear bidirectionality hint" "&"; + + (* Actions *) if renaming_specified then begin @@ -1428,10 +1468,26 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red strbrk "are relevant for constants only.") end; + if bidi_hint_specified then begin + let n = Option.get nargs_before_bidi in + if section_local then + Pretyping.add_bidirectionality_hint sr n + else + Lib.add_anonymous_leaf (inBidiHints (sr, Some n)) + end; + + if clear_bidi_hint then begin + if section_local then + Pretyping.clear_bidirectionality_hint sr + else + Lib.add_anonymous_leaf (inBidiHints (sr, None)) + end; + if not (renaming_specified || implicits_specified || scopes_specified || - red_modifiers_specified) && (List.is_empty flags) then + red_modifiers_specified || + bidi_hint_specified) && (List.is_empty flags) then warn_arguments_assert sr let default_env () = { @@ -2113,7 +2169,6 @@ let vernac_show ~pstate = begin function | ShowProof -> show_proof ~pstate | ShowMatch id -> show_match id - | ShowScript -> assert false (* Only the stm knows the script *) | _ -> user_err (str "This command requires an open proof.") end @@ -2134,7 +2189,6 @@ let vernac_show ~pstate = | ShowIntros all -> show_intro ~pstate all | ShowProof -> show_proof ~pstate:(Some pstate) | ShowMatch id -> show_match id - | ShowScript -> assert false (* Only the stm knows the script *) end let vernac_check_guard ~pstate = @@ -2437,8 +2491,8 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option = | VernacSyntacticDefinition (id,c,b) -> with_module_locality ~atts vernac_syntactic_definition id c b; pstate - | VernacArguments (qid, args, more_implicits, nargs, flags) -> - with_section_locality ~atts vernac_arguments qid args more_implicits nargs flags; + | VernacArguments (qid, args, more_implicits, nargs, nargs_before_bidi, flags) -> + with_section_locality ~atts vernac_arguments qid args more_implicits nargs nargs_before_bidi flags; pstate | VernacReserve bl -> unsupported_attributes atts; diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index f946e0596e..b8946fad23 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -81,7 +81,6 @@ type locatable = type showable = | ShowGoal of goal_reference | ShowProof - | ShowScript | ShowExistentials | ShowUniverses | ShowProofNames @@ -362,8 +361,9 @@ type nonrec vernac_expr = vernac_argument_status list (* Main arguments status list *) * (Name.t * Impargs.implicit_kind) list list (* Extra implicit status lists *) * int option (* Number of args to trigger reduction *) * + int option (* Number of args before bidirectional typing *) * [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename | - `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes | + `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes | `ClearBidiHint | `DefaultImplicits ] list | VernacReserve of simple_binder list | VernacGeneralizable of (lident list) option |