diff options
41 files changed, 663 insertions, 244 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 3a762b42a..eb2797101 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -186,6 +186,10 @@ /pretyping/ @mattam82 # Secondary maintainer @gares +/pretyping/vnorm.* @maximedenes +/pretyping/nativenorm.* @maximedenes +# Secondary maintainer @ppedrot + ########## Pretty printer ########## /printing/ @herbelin diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 971a281ea..4e159ebdc 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -306,6 +306,9 @@ validate:edge+flambda: OPAM_SWITCH: edge OPAM_VARIANT: "+flambda" +ci-bedrock2: + <<: *ci-template + ci-bignums: <<: *ci-template @@ -1,6 +1,10 @@ Changes from 8.8.2 to 8.9+beta1 =============================== +Kernel + +- Mutually defined records are now supported. + Tactics - Added toplevel goal selector ! which expects a single focused goal. @@ -87,13 +91,26 @@ Changes from 8.8.0 to 8.8.1 Kernel - Fix a critical bug with cofixpoints and vm_compute/native_compute (#7333). +- Fix a critical bug with modules and algebraic universes (#7695) - Fix a critical bug with inlining of polymorphic constants (#7615). +- Fix a critical bug with universe polymorphism and vm_compute (#7723). Was + present since 8.5. Notations - Fixed unexpected collision between only-parsing and only-printing notations (issue #7462). +Windows installer + +- The Windows installer now includes external packages Ltac2 and Equations + (it included the Bignums package since 8.8+beta1). + +Many other bug fixes, documentation improvements (including fixes of +regressions due to the Sphinx migration), and user message improvements +(for details, see the 8.8.1 milestone at +https://github.com/coq/coq/milestone/13?closed=1). + Changes from 8.8+beta1 to 8.8.0 =============================== diff --git a/Makefile.ci b/Makefile.ci index 7f63157fa..fce16906c 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -8,7 +8,8 @@ ## # (see LICENSE file for the text of the license) ## ########################################################################## -CI_TARGETS=ci-bignums \ +CI_TARGETS=ci-bedrock2 \ + ci-bignums \ ci-color \ ci-compcert \ ci-coq-dpdgraph \ @@ -56,3 +56,11 @@ used, and include a complete source example leading to the bug. ## Contributing Guidelines for contributing to Coq in various ways are listed in the [contributor's guide](CONTRIBUTING.md). + +## Supporting Coq + +Help the Coq community grow and prosper by becoming a sponsor! The [Coq +Consortium](https://coq.inria.fr/consortium) can establish sponsorship contracts +or receive donations. If you want to take an active role in shaping Coq's +future, you can also become a Consortium member. If you are interested, please +get in touch! diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index a4e60744f..94e90bf4f 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1437,12 +1437,16 @@ function make_addon_equations { } function make_addons { - if [ -n "${GITLAB_CI}" ]; then + if [ -n "$GITLAB_CI" ]; then export CI_BRANCH="$CI_COMMIT_REF_NAME" - if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]] - then + if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]]; then export CI_PULL_REQUEST="${CI_BRANCH#pr-}" + else + export CI_PULL_REQUEST="" fi + else + export CI_BRANCH="" + export CI_PULL_REQUEST="" fi . /build/ci-basic-overlay.sh for overlay in /build/user-overlays/*.sh; do diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 2ebbf2cc4..28321d13e 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -148,6 +148,12 @@ : "${bignums_CI_GITURL:=https://github.com/coq/bignums}" ######################################################################## +# bedrock2 +######################################################################## +: "${bedrock2_CI_BRANCH:=master}" +: "${bedrock2_CI_GITURL:=https://github.com/mit-plv/bedrock2}" + +######################################################################## # Equations ######################################################################## : "${Equations_CI_BRANCH:=master}" diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh new file mode 100755 index 000000000..447076e09 --- /dev/null +++ b/dev/ci/ci-bedrock2.sh @@ -0,0 +1,11 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +bedrock2_CI_DIR="${CI_BUILD_DIR}/bedrock2" + +git_checkout "${bedrock2_CI_BRANCH}" "${bedrock2_CI_GITURL}" "${bedrock2_CI_DIR}" +( cd "${bedrock2_CI_DIR}" && git submodule update --init --recursive ) + +( cd "${bedrock2_CI_DIR}" && make ) diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs index 293b01f63..6166d24b7 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -81,6 +81,20 @@ Module system GH issue number: #4294 risk: ? +Module system + + component: modules, universes + summary: universe constraints for module subtyping not stored in vo files + introduced: presumably 8.2 (b3d3b56) + impacted released versions: 8.2, 8.3, 8.4 + impacted development branches: v8.5 + impacted coqchk versions: none + fixed in: v8.2 (c1d9889), v8.3 (8056d02), v8.4 (a07deb4), trunk (0cd0a3e) Mar 5, 2014, Tassi + found by: Tassi by running coqchk on the mathematical components library + exploit: requires multiple files, no test provided + GH issue number: #3243 + risk: could be exploited by mistake + Universes component: template polymorphism @@ -123,6 +137,18 @@ Primitive projections Conversion machines + component: "lazy machine" (lazy krivine abstract machine) + summary: the invariant justifying some optimization was wrong for some combination of sharing side effects + introduced: prior to V7.0 + impacted released versions: V8.0-V8.0pl4, V8.1-V8.1pl3 + impacted development branches: none + impacted coqchk versions: (eefe63d52, Barras, 20 May 2008), was in beta-development for 8.2 at this time + fixed in: master/trunk/8.2 (f13aaec57/a8b034513, 15 May 2008, Barras), v8.1 (e7611477a, 15 May 2008, Barras), v8.0 (6ed40a8bc, 29 Nov 2016, Herbelin, backport) + found by: Gonthier + exploit: by Gonthier + GH issue number: none + risk: unrealistic to be exploited by chance + component: "virtual machine" (compilation to bytecode ran by a C-interpreter) summary: collision between constructors when more than 256 constructors in a type introduced: V8.1 diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 811abd67f..ab679a71c 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -232,7 +232,7 @@ let ppenv e = pp let ppenvwithcst e = pp (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++ str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]" ++ spc() ++ - str "{" ++ Cmap_env.fold (fun a _ s -> Constant.print a ++ spc () ++ s) (Obj.magic e).env_globals.env_constants (mt ()) ++ str "}") + str "{" ++ Environ.fold_constants (fun a _ s -> Constant.print a ++ spc () ++ s) e (mt ()) ++ str "}") let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (Global.env()) x)) diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst index 2562dec46..5d9324a65 100644 --- a/doc/sphinx/credits.rst +++ b/doc/sphinx/credits.rst @@ -1393,7 +1393,7 @@ Version 8.8 is the third release of |Coq| developed on a time-based development cycle. Its development spanned 6 months from the release of |Coq| 8.7 and was based on a public roadmap. The development process was coordinated by Matthieu Sozeau. Maxime Dénès was in charge of the -release process. +release process. Théo Zimmermann is the maintainer of this release. Many power users helped to improve the design of the new features via the bug tracker, the pull request system, the |Coq| development mailing diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index c21d8d4ec..8fbd2ea4e 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -23,8 +23,9 @@ expressions. In this sense, the :cmd:`Record` construction allows defining .. _record_grammar: .. productionlist:: `sentence` - record : `record_keyword` `ident` [ `binders` ] [: `sort` ] := [ `ident` ] { [ `field` ; … ; `field` ] }. + record : `record_keyword` `record_body` with … with `record_body` record_keyword : Record | Inductive | CoInductive + record_body : `ident` [ `binders` ] [: `sort` ] := [ `ident` ] { [ `field` ; … ; `field` ] }. field : `ident` [ `binders` ] : `type` [ where `notation` ] : | `ident` [ `binders` ] [: `type` ] := `term` @@ -167,12 +168,13 @@ and the syntax `term.(@qualid` |term_1| |term_n| `)` to `@qualid` |term_1| `…` In each case, `term` is the object projected and the other arguments are the parameters of the inductive type. + .. note:: Records defined with the ``Record`` keyword are not allowed to be recursive (references to the record's name in the type of its field raises an error). To define recursive records, one can use the ``Inductive`` and ``CoInductive`` keywords, resulting in an inductive or co-inductive record. - A *caveat*, however, is that records cannot appear in mutually inductive - (or co-inductive) definitions. + Definition of mutal inductive or co-inductive records are also allowed, as long + as all of the types in the block are records. .. note:: Induction schemes are automatically generated for inductive records. Automatic generation of induction schemes for non-recursive records @@ -2226,7 +2228,7 @@ existential variable used in the same context as its context of definition is wr Check (fun x y => _) 0 1. Existential variables can be named by the user upon creation using -the syntax ``?``\ `ident`. This is useful when the existential +the syntax :n:`?[@ident]`. This is useful when the existential variable needs to be explicitly handled later in the script (e.g. with a named-goal selector, see :ref:`goal-selectors`). diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index b3088ee28..9be562d3e 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -103,7 +103,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals ~unfoc_goals hints = mat else [] in proof#buffer#insert (goal_str ~shownum:true 1 goals_cnt); - insert_xml proof#buffer (Richpp.richpp_of_pp width cur_goal); + insert_xml ~tags:[Tags.Proof.goal] proof#buffer (Richpp.richpp_of_pp width cur_goal); proof#buffer#insert "\n" in (* Insert remaining goals (no hypotheses) *) @@ -128,7 +128,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals ~unfoc_goals hints = mat ignore(proof#buffer#place_cursor ~where:(proof#buffer#end_iter#backward_to_tag_toggle (Some Tags.Proof.goal))); - ignore(proof#scroll_to_mark ~use_align:true ~yalign:0.95 `INSERT) + ignore(proof#scroll_to_mark `INSERT) let rec flatten = function | [] -> [] diff --git a/interp/declare.ml b/interp/declare.ml index e79cc6079..fcb62ac8c 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -383,13 +383,12 @@ let inInductive : inductive_obj -> obj = rebuild_function = infer_inductive_subtyping } let declare_projections univs mind = - (** FIXME: handle mutual records *) - let mind = (mind, 0) in let env = Global.env () in - let spec,_ = Inductive.lookup_mind_specif env mind in - match spec.mind_record with - | PrimRecord info -> - let _, kns, _ = info.(0) in + let mib = Environ.lookup_mind mind env in + match mib.mind_record with + | PrimRecord info -> + let iter i (_, kns, _) = + let mind = (mind, i) in let projs = Inductiveops.compute_projections env mind in Array.iter2 (fun kn (term, types) -> let id = Label.to_id (Constant.label kn) in @@ -411,10 +410,12 @@ let declare_projections univs mind = let entry = definition_entry ~types ~univs term in let kn' = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in assert (Constant.equal kn kn') - ) kns projs; - true, true - | FakeRecord -> true,false - | NotRecord -> false,false + ) kns projs + in + let () = Array.iteri iter info in + true, true + | FakeRecord -> true, false + | NotRecord -> false, false (* for initial declaration *) let declare_mind mie = diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 487385a78..3095ce148 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -217,6 +217,7 @@ type vm_env = { type comp_env = { + arity : int; (* arity of the current function, 0 if none *) nb_uni_stack : int ; (* number of universes on the stack, *) (* universes are always at the bottom. *) nb_stack : int; (* number of variables on the stack *) diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 238edc0af..de21401b3 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -159,6 +159,7 @@ type vm_env = { type comp_env = { + arity : int; (* arity of the current function, 0 if none *) nb_uni_stack : int ; (** number of universes on the stack *) nb_stack : int; (** number of variables on the stack *) in_stack : int list; (** position in the stack *) diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 881bfae19..6677db2fd 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -112,8 +112,9 @@ let push_fv d e = { let fv r = !(r.in_env) -let empty_comp_env ?(univs=0) ()= - { nb_uni_stack = univs; +let empty_comp_env ()= + { arity = 0; + nb_uni_stack = 0; nb_stack = 0; in_stack = []; nb_rec = 0; @@ -148,7 +149,8 @@ let rec add_param n sz l = if Int.equal n 0 then l else add_param (n - 1) sz (n+sz::l) let comp_env_fun ?(univs=0) arity = - { nb_uni_stack = univs ; + { arity; + nb_uni_stack = univs ; nb_stack = arity; in_stack = add_param arity 0 []; nb_rec = 0; @@ -159,7 +161,8 @@ let comp_env_fun ?(univs=0) arity = let comp_env_fix_type rfv = - { nb_uni_stack = 0; + { arity = 0; + nb_uni_stack = 0; nb_stack = 0; in_stack = []; nb_rec = 0; @@ -173,7 +176,8 @@ let comp_env_fix ndef curr_pos arity rfv = for i = ndef downto 1 do prec := Koffsetclosure (2 * (ndef - curr_pos - i)) :: !prec done; - { nb_uni_stack = 0; + { arity; + nb_uni_stack = 0; nb_stack = arity; in_stack = add_param arity 0 []; nb_rec = ndef; @@ -183,7 +187,8 @@ let comp_env_fix ndef curr_pos arity rfv = } let comp_env_cofix_type ndef rfv = - { nb_uni_stack = 0; + { arity = 0; + nb_uni_stack = 0; nb_stack = 0; in_stack = []; nb_rec = 0; @@ -197,7 +202,8 @@ let comp_env_cofix ndef arity rfv = for i = 1 to ndef do prec := Kenvacc i :: !prec done; - { nb_uni_stack = 0; + { arity; + nb_uni_stack = 0; nb_stack = arity; in_stack = add_param arity 0 []; nb_rec = ndef; @@ -249,8 +255,15 @@ let pos_rel i r sz = Kenvacc(r.offset + pos) let pos_universe_var i r sz = - if i < r.nb_uni_stack then - Kacc (sz - r.nb_stack - (r.nb_uni_stack - i)) + (* Compilation of a universe variable can happen either at toplevel (the + current closure correspond to a constant and has local universes) or in a + local closure (which has no local universes). *) + if r.nb_uni_stack != 0 then + (* Universe variables are represented by De Bruijn levels (not indices), + starting at 0. The shape of the stack will be [v1|..|vn|u1..up|arg1..argq] + with size = n + p + q, and q = r.arity. So Kacc (sz - r.arity - 1) will access + the last universe. *) + Kacc (sz - r.arity - (r.nb_uni_stack - i)) else let env = !(r.in_env) in let db = FVuniv_var i in diff --git a/kernel/clambda.ml b/kernel/clambda.ml index b722e4200..f1b6f3dff 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -814,7 +814,7 @@ let optimize_lambda lam = let lambda_of_constr ~optimize genv c = let env = Renv.make genv in - let ids = List.rev_map Context.Rel.Declaration.get_name genv.env_rel_context.env_rel_ctx in + let ids = List.rev_map Context.Rel.Declaration.get_name (rel_context genv) in Renv.push_rels env (Array.of_list ids); let lam = lambda_of_constr env c in let lam = if optimize then optimize_lambda lam else lam in diff --git a/kernel/environ.ml b/kernel/environ.ml index cc14dae5b..4ab469803 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -55,7 +55,8 @@ type globals = { env_projections : projection_body Cmap_env.t; env_inductives : mind_key Mindmap_env.t; env_modules : module_body MPmap.t; - env_modtypes : module_type_body MPmap.t} + env_modtypes : module_type_body MPmap.t; +} type stratification = { env_universes : UGraph.t; @@ -86,7 +87,7 @@ type rel_context_val = { } type env = { - env_globals : globals; (* globals = constants + inductive types + modules + module-types *) + env_globals : globals; env_named_context : named_context_val; (* section variables *) env_rel_context : rel_context_val; env_nb_rel : int; @@ -208,6 +209,9 @@ let lookup_named_val id env = let lookup_named_ctxt id ctxt = fst (Id.Map.find id ctxt.env_named_map) +let fold_constants f env acc = + Cmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.env_constants acc + (* Global constants *) let lookup_constant_key kn env = diff --git a/kernel/environ.mli b/kernel/environ.mli index deca8afde..0259dbbdd 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -46,13 +46,8 @@ type constant_key = constant_body * (link_info ref * key) type mind_key = mutual_inductive_body * link_info ref -type globals = { - env_constants : constant_key Cmap_env.t; - env_projections : projection_body Cmap_env.t; - env_inductives : mind_key Mindmap_env.t; - env_modules : module_body MPmap.t; - env_modtypes : module_type_body MPmap.t -} +type globals +(** globals = constants + projections + inductive types + modules + module-types *) type stratification = { env_universes : UGraph.t; @@ -70,7 +65,7 @@ type rel_context_val = private { } type env = private { - env_globals : globals; (* globals = constants + inductive types + modules + module-types *) + env_globals : globals; env_named_context : named_context_val; (* section variables *) env_rel_context : rel_context_val; env_nb_rel : int; @@ -175,6 +170,9 @@ val reset_with_named_context : named_context_val -> env -> env (** This removes the [n] last declarations from the rel context *) val pop_rel_context : int -> env -> env +(** Useful for printing *) +val fold_constants : (Constant.t -> constant_body -> 'a -> 'a) -> env -> 'a -> 'a + (** {5 Global constants } {6 Add entries to global environment } *) @@ -320,6 +318,7 @@ open Retroknowledge (** functions manipulating the retroknowledge @author spiwack *) val retroknowledge : (retroknowledge->'a) -> env -> 'a +[@@ocaml.deprecated "Use the record projection."] val registered : env -> field -> bool diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 74d12f3cd..1748e98a4 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1845,7 +1845,7 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml = in let auxdefs = List.fold_right get_rel_val fv_rel auxdefs in let auxdefs = List.fold_right get_named_val fv_named auxdefs in - let lvl = Context.Rel.length env.env_rel_context.env_rel_ctx in + let lvl = Context.Rel.length (rel_context env) in let fv_rel = List.map (fun (n,_) -> MLglobal (Grel (lvl-n))) fv_rel in let fv_named = List.map (fun (id,_) -> MLglobal (Gnamed id)) fv_named in let aux_name = fresh_lname Anonymous in @@ -1854,7 +1854,7 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml = and compile_rel env sigma univ auxdefs n = let open Context.Rel.Declaration in let decl = lookup_rel n env in - let n = List.length env.env_rel_context.env_rel_ctx - n in + let n = List.length (rel_context env) - n in match decl with | LocalDef (_,t,_) -> let code = lambda_of_constr env sigma t in diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 244e5e0dd..5843cd543 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -659,7 +659,7 @@ let optimize lam = let lambda_of_constr env sigma c = set_global_env env; let env = Renv.make () in - let ids = List.rev_map RelDecl.get_name !global_env.env_rel_context.env_rel_ctx in + let ids = List.rev_map RelDecl.get_name (rel_context !global_env) in Renv.push_rels env (Array.of_list ids); let lam = lambda_of_constr env sigma c in (* if Flags.vm_draw_opt () then begin diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 12c82e20d..f87ec9e02 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -897,9 +897,11 @@ let typing senv = Typeops.infer (env_of_senv senv) (** {6 Retroknowledge / native compiler } *) +[@@@ocaml.warning "-3"] (** universal lifting, used for the "get" operations mostly *) let retroknowledge f senv = Environ.retroknowledge f (env_of_senv senv) +[@@@ocaml.warning "+3"] let register field value by_clause senv = (* todo : value closed, by_clause safe, by_clause of the proper type*) @@ -918,7 +920,7 @@ let register_inline kn senv = if not (evaluable_constant kn senv.env) then CErrors.user_err Pp.(str "Register inline: an evaluable constant is expected"); let env = senv.env in - let (cb,r) = Cmap_env.find kn env.env_globals.env_constants in + let cb = lookup_constant kn env in let cb = {cb with const_inline_code = true} in let env = add_constant kn cb env in { senv with env} diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 4078a9092..aca77ccd1 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -221,6 +221,7 @@ val delta_of_senv : open Retroknowledge val retroknowledge : (retroknowledge-> 'a) -> safe_environment -> 'a +[@@ocaml.deprecated "Use the projection of Environ.env"] val register : field -> Retroknowledge.entry -> Constr.constr -> safe_transformer0 diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml index 61eb1dafd..c2bcd73ff 100644 --- a/lib/coqProject_file.ml4 +++ b/lib/coqProject_file.ml @@ -90,30 +90,50 @@ let rec post_canonize f = exception Parsing_error of string -let rec parse_string = parser - | [< '' ' | '\n' | '\t' >] -> "" - | [< 'c; s >] -> (String.make 1 c)^(parse_string s) - | [< >] -> "" -and parse_string2 = parser - | [< ''"' >] -> "" - | [< 'c; s >] -> (String.make 1 c)^(parse_string2 s) - | [< >] -> raise (Parsing_error "unterminated string") -and parse_skip_comment = parser - | [< ''\n'; s >] -> s - | [< 'c; s >] -> parse_skip_comment s - | [< >] -> [< >] -and parse_args = parser - | [< '' ' | '\n' | '\t'; s >] -> parse_args s - | [< ''#'; s >] -> parse_args (parse_skip_comment s) - | [< ''"'; str = parse_string2; s >] -> ("" ^ str) :: parse_args s - | [< 'c; str = parse_string; s >] -> ((String.make 1 c) ^ str) :: (parse_args s) - | [< >] -> [] +let buffer buf = + let ans = Buffer.contents buf in + let () = Buffer.clear buf in + ans + +let rec parse_string buf s = match Stream.next s with +| ' ' | '\n' | '\t' -> buffer buf +| c -> + let () = Buffer.add_char buf c in + parse_string buf s +| exception Stream.Failure -> buffer buf + +and parse_string2 buf s = match Stream.next s with +| '"' -> buffer buf +| c -> + let () = Buffer.add_char buf c in + parse_string2 buf s +| exception Stream.Failure -> raise (Parsing_error "unterminated string") + +and parse_skip_comment s = match Stream.next s with +| '\n' -> () +| _ -> parse_skip_comment s +| exception Stream.Failure -> () + +and parse_args buf accu s = match Stream.next s with +| ' ' | '\n' | '\t' -> parse_args buf accu s +| '#' -> + let () = parse_skip_comment s in + parse_args buf accu s +| '"' -> + let str = parse_string2 buf s in + parse_args buf (str :: accu) s +| c -> + let () = Buffer.add_char buf c in + let str = parse_string buf s in + parse_args buf (str :: accu) s +| exception Stream.Failure -> accu let parse f = let c = open_in f in - let res = parse_args (Stream.of_channel c) in + let buf = Buffer.create 64 in + let res = parse_args buf [] (Stream.of_channel c) in close_in c; - res + List.rev res ;; (* Copy from minisys.ml, since we don't see that file here *) @@ -143,7 +163,7 @@ let process_cmd_line orig_dir proj args = error "Use \"-install none\" instead of \"-no-install\"" | "-custom" :: _ -> error "Use \"-extra[-phony] target deps command\" instead of \"-custom command deps target\"" - + | ("-no-opt"|"-byte") :: r -> aux { proj with use_ocamlopt = false } r | ("-full"|"-opt") :: r -> aux { proj with use_ocamlopt = true } r | "-install" :: d :: r -> @@ -189,7 +209,7 @@ let process_cmd_line orig_dir proj args = error "Output file must be in the current directory"; if proj.makefile <> None then error "Option -o given more than once"; - aux { proj with makefile = Some file } r + aux { proj with makefile = Some file } r | v :: "=" :: def :: r -> aux { proj with defs = proj.defs @ [sourced (v,def)] } r | "-arg" :: a :: r -> diff --git a/lib/system.ml b/lib/system.ml index f109c7192..eef65a4e3 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -302,7 +302,7 @@ let with_time ~batch f x = raise e let get_toplevel_path top = - let dir = Filename.dirname Sys.argv.(0) in + let dir = Filename.dirname Sys.executable_name in let exe = if Sys.(os_type = "Win32" || os_type = "Cygwin") then ".exe" else "" in let eff = if Dynlink.is_native then ".opt" else ".byte" in dir ^ Filename.dir_sep ^ top ^ eff ^ exe diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index e9ce306e8..4ea0b30bd 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -29,11 +29,6 @@ TACTIC EXTEND protect_fv [ protect_tac map ] END -TACTIC EXTEND closed_term - [ "closed_term" constr(t) "[" ne_reference_list(l) "]" ] -> - [ closed_term t l ] -END - open Pptactic open Ppconstr diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index e4d17f250..8e0ca877a 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -96,34 +96,36 @@ let protect_tac_in map id = (****************************************************************************) -let closed_term t l = - let open Quote_plugin in +let rec closed_under sigma cset t = + try + let (gr, _) = Termops.global_of_constr sigma t in + Refset_env.mem gr cset + with Not_found -> + match EConstr.kind sigma t with + | Cast(c,_,_) -> closed_under sigma cset c + | App(f,l) -> closed_under sigma cset f && Array.for_all (closed_under sigma cset) l + | _ -> false + +let closed_term args _ = match args with +| [t; l] -> + let t = Option.get (Value.to_constr t) in + let l = List.map (fun c -> Value.cast (Genarg.topwit Stdarg.wit_ref) c) (Option.get (Value.to_list l)) in Proofview.tclEVARMAP >>= fun sigma -> - let l = List.map UnivGen.constr_of_global l in - let cs = List.fold_right Quote.ConstrSet.add l Quote.ConstrSet.empty in - if Quote.closed_under sigma cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt()) - -(* TACTIC EXTEND echo -| [ "echo" constr(t) ] -> - [ Pp.msg (Termops.print_constr t); Tacinterp.eval_tactic (TacId []) ] -END;;*) + let cs = List.fold_right Refset_env.add l Refset_env.empty in + if closed_under sigma cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt()) +| _ -> assert false -(* -let closed_term_ast l = - TacFun([Some(Id.of_string"t")], - TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term", - [Genarg.in_gen Constrarg.wit_constr (mkVar(Id.of_string"t")); - Genarg.in_gen (Genarg.wit_list Constrarg.wit_ref) l]))) -*) -let closed_term_ast l = +let closed_term_ast = let tacname = { mltac_plugin = "newring_plugin"; mltac_tactic = "closed_term"; } in + let () = Tacenv.register_ml_tactic tacname [|closed_term|] in let tacname = { mltac_name = tacname; mltac_index = 0; } in + fun l -> let l = List.map (fun gr -> ArgArg(Loc.tag gr)) l in TacFun([Name(Id.of_string"t")], TacML(Loc.tag (tacname, diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli index 0e056a472..fcd04a2e7 100644 --- a/plugins/setoid_ring/newring.mli +++ b/plugins/setoid_ring/newring.mli @@ -18,8 +18,6 @@ val protect_tac_in : string -> Id.t -> unit Proofview.tactic val protect_tac : string -> unit Proofview.tactic -val closed_term : EConstr.constr -> GlobRef.t list -> unit Proofview.tactic - val add_theory : Id.t -> constr_expr -> diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 64407f359..576073344 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -465,22 +465,21 @@ let build_branch_type env sigma dep p cs = let compute_projections env (kn, i as ind) = let open Term in let mib = Environ.lookup_mind kn env in - let indu = match mib.mind_universes with - | Monomorphic_ind _ -> mkInd ind - | Polymorphic_ind ctx -> mkIndU (ind, make_abstract_instance ctx) - | Cumulative_ind ctx -> - mkIndU (ind, make_abstract_instance (ACumulativityInfo.univ_context ctx)) + let u = match mib.mind_universes with + | Monomorphic_ind _ -> Instance.empty + | Polymorphic_ind auctx -> make_abstract_instance auctx + | Cumulative_ind acumi -> + make_abstract_instance (ACumulativityInfo.univ_context acumi) in let x = match mib.mind_record with | NotRecord | FakeRecord -> anomaly Pp.(str "Trying to build primitive projections for a non-primitive record") | PrimRecord info-> Name (pi1 (info.(i))) in - (** FIXME: handle mutual records *) - let pkt = mib.mind_packets.(0) in - let { mind_consnrealargs; mind_consnrealdecls } = pkt in + let pkt = mib.mind_packets.(i) in let { mind_nparams = nparamargs; mind_params_ctxt = params } = mib in - let rctx, _ = decompose_prod_assum (subst1 indu pkt.mind_nf_lc.(0)) in + let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((kn, mib.mind_ntypes - i - 1), u)) in + let rctx, _ = decompose_prod_assum (substl subst pkt.mind_nf_lc.(0)) in let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in let mp, dp, l = MutInd.repr3 kn in (** We build a substitution smashing the lets in the record parameters so @@ -489,6 +488,7 @@ let compute_projections env (kn, i as ind) = let indty = (* [ty] = [Ind inst] is typed in context [params] *) let inst = Context.Rel.to_extended_vect mkRel 0 paramslet in + let indu = mkIndU (ind, u) in let ty = mkApp (indu, inst) in (* [Ind inst] is typed in context [params-wo-let] *) ty @@ -498,8 +498,8 @@ let compute_projections env (kn, i as ind) = { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in { ci_ind = ind; ci_npar = nparamargs; - ci_cstr_ndecls = mind_consnrealdecls; - ci_cstr_nargs = mind_consnrealargs; + ci_cstr_ndecls = pkt.mind_consnrealdecls; + ci_cstr_nargs = pkt.mind_consnrealargs; ci_pp_info = print_info } in let len = List.length ctx in diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 7319846fb..16d003f67 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -123,7 +123,7 @@ let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs = try if const then let ctyp = type_constructor mind mib u (mip.mind_nf_lc.(0)) params in - retroknowledge Retroknowledge.get_vm_decompile_constant_info env (mkInd ind) tag, ctyp + Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (mkInd ind) tag, ctyp else raise Not_found with Not_found -> diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 14c9f49b1..bd6062824 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -79,7 +79,7 @@ let construct_of_constr const env tag typ = (* spiwack : here be a branch for specific decompilation handled by retroknowledge *) try if const then - ((retroknowledge Retroknowledge.get_vm_decompile_constant_info env (mkIndU indu) tag), + ((Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (mkIndU indu) tag), typ) (*spiwack: this may need to be changed in case there are parameters in the type which may cause a constant value to have an arity. (type_constructor seems to be all about parameters actually) diff --git a/test-suite/Makefile b/test-suite/Makefile index 32e245e36..33b402327 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -519,6 +519,7 @@ $(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG) @echo "TEST $<" $(HIDE){ \ echo $(call log_intro,$<); \ + export BIN="$(BIN)"; \ export coqc="$(coqc)"; \ export coqtop="$(coqtop)"; \ export coqdep="$(coqdep)"; \ diff --git a/test-suite/bugs/closed/7723.v b/test-suite/bugs/closed/7723.v new file mode 100644 index 000000000..216290123 --- /dev/null +++ b/test-suite/bugs/closed/7723.v @@ -0,0 +1,58 @@ +Set Universe Polymorphism. + +Module Segfault. + +Inductive decision_tree : Type := . + +Fixpoint first_satisfying_helper {A B} (f : A -> option B) (ls : list A) : option B + := match ls with + | nil => None + | cons x xs + => match f x with + | Some v => Some v + | None => first_satisfying_helper f xs + end + end. + +Axiom admit : forall {T}, T. +Definition dtree4 : option decision_tree := + match first_satisfying_helper (fun pat : nat => Some pat) (cons 0 nil) + with + | Some _ => admit + | None => admit + end +. +Definition dtree'' := Eval vm_compute in dtree4. (* segfault *) + +End Segfault. + +Module OtherExample. + +Definition bar@{i} := Type@{i}. +Definition foo@{i j} (x y z : nat) := + @id Type@{j} bar@{i}. +Eval vm_compute in foo. + +End OtherExample. + +Module LocalClosure. + +Definition bar@{i} := Type@{i}. + +Definition foo@{i j} (x y z : nat) := + @id (nat -> Type@{j}) (fun _ => Type@{i}). +Eval vm_compute in foo. + +End LocalClosure. + +Require Import Hurkens. +Polymorphic Inductive unit := tt. + +Polymorphic Definition foo := + let x := id tt in (x, x, Type). + +Lemma bad : False. + refine (TypeNeqSmallType.paradox (snd foo) _). + vm_compute. + Fail reflexivity. +Abort. diff --git a/test-suite/misc/7704.sh b/test-suite/misc/7704.sh new file mode 100755 index 000000000..0ca2c97d2 --- /dev/null +++ b/test-suite/misc/7704.sh @@ -0,0 +1,7 @@ +#!/usr/bin/env bash + +set -e + +export PATH=$BIN:$PATH + +${coqtop#"$BIN"} -compile misc/aux7704.v diff --git a/test-suite/misc/aux7704.v b/test-suite/misc/aux7704.v new file mode 100644 index 000000000..6fdcf6768 --- /dev/null +++ b/test-suite/misc/aux7704.v @@ -0,0 +1,6 @@ + +Goal True /\ True. +Proof. + split. + par:exact I. +Qed. diff --git a/test-suite/success/mutual_record.v b/test-suite/success/mutual_record.v new file mode 100644 index 000000000..77529733b --- /dev/null +++ b/test-suite/success/mutual_record.v @@ -0,0 +1,57 @@ +Module M0. + +Inductive foo (A : Type) := Foo { + foo0 : option (bar A); + foo1 : nat; + foo2 := foo1 = 0; + foo3 : foo2; +} + +with bar (A : Type) := Bar { + bar0 : A; + bar1 := 0; + bar2 : bar1 = 0; + bar3 : nat -> foo A; +}. + +End M0. + +Module M1. + +Set Primitive Projections. + +Inductive foo (A : Type) := Foo { + foo0 : option (bar A); + foo1 : nat; + foo2 := foo1 = 0; + foo3 : foo2; +} + +with bar (A : Type) := Bar { + bar0 : A; + bar1 := 0; + bar2 : bar1 = 0; + bar3 : nat -> foo A; +}. + +End M1. + +Module M2. + +Set Primitive Projections. + +CoInductive foo (A : Type) := Foo { + foo0 : option (bar A); + foo1 : nat; + foo2 := foo1 = 0; + foo3 : foo2; +} + +with bar (A : Type) := Bar { + bar0 : A; + bar1 := 0; + bar2 : bar1 = 0; + bar3 : nat -> foo A; +}. + +End M2. diff --git a/test-suite/success/vm_records.v b/test-suite/success/vm_records.v new file mode 100644 index 000000000..8a1544c8e --- /dev/null +++ b/test-suite/success/vm_records.v @@ -0,0 +1,40 @@ +Set Primitive Projections. + +Module M. + +CoInductive foo := Foo { + foo0 : foo; + foo1 : bar; +} +with bar := Bar { + bar0 : foo; + bar1 : bar; +}. + +CoFixpoint f : foo := Foo f g +with g : bar := Bar f g. + +Check (@eq_refl _ g.(bar0) <: f.(foo0).(foo0) = g.(bar0)). +Check (@eq_refl _ g <: g.(bar1).(bar0).(foo1) = g). + +End M. + +Module N. + +Inductive foo := Foo { + foo0 : option foo; + foo1 : list bar; +} +with bar := Bar { + bar0 : option bar; + bar1 : list foo; +}. + +Definition f_0 := Foo None nil. +Definition g_0 := Bar None nil. + +Definition f := Foo (Some f_0) (cons g_0 nil). + +Check (@eq_refl _ f.(foo1) <: f.(foo1) = cons g_0 nil). + +End N. diff --git a/vernac/record.ml b/vernac/record.ml index 2d7800827..7a8ce7d25 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -100,7 +100,7 @@ let binder_of_decl = function let binders_of_decls = List.map binder_of_decl -let typecheck_params_and_fields finite def id poly pl t ps nots fs = +let typecheck_params_and_fields finite def poly pl ps records = let env0 = Global.env () in let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env0 pl in let _ = @@ -117,7 +117,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters")) ps in let sigma, (impls_env, ((env1,newps), imps)) = interp_context_evars env0 sigma ps in - let sigma, typ, sort, template = match t with + let fold (sigma, template) (_, t, _, _) = match t with | Some t -> let env = EConstr.push_rel_context newps env0 in let poly = @@ -132,28 +132,36 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = match Evd.is_sort_variable sigma s' with | Some l -> let sigma = Evd.make_flexible_variable sigma ~algebraic:true l in - sigma, s, s', true + (sigma, template), (s, s') | None -> - sigma, s, s', false - else sigma, s, s', false) + (sigma, false), (s, s') + else (sigma, false), (s, s')) | _ -> user_err ?loc:(constr_loc t) (str"Sort expected.")) | None -> let uvarkind = Evd.univ_flexible_alg in let sigma, s = Evd.new_sort_variable uvarkind sigma in - sigma, EConstr.mkSort s, s, true + (sigma, template), (EConstr.mkSort s, s) in - let arity = EConstr.it_mkProd_or_LetIn typ newps in - let env_ar = EConstr.push_rel_context newps (EConstr.push_rel (LocalAssum (Name id,arity)) env0) in + let (sigma, template), typs = List.fold_left_map fold (sigma, true) records in + let arities = List.map (fun (typ, _) -> EConstr.it_mkProd_or_LetIn typ newps) typs in + let fold accu (id, _, _, _) arity = EConstr.push_rel (LocalAssum (Name id,arity)) accu in + let env_ar = EConstr.push_rel_context newps (List.fold_left2 fold env0 records arities) in let assums = List.filter is_local_assum newps in - let params = List.map (RelDecl.get_name %> Name.get_id) assums in - let ty = Inductive (params,(finite != Declarations.BiFinite)) in - let impls_env = compute_internalization_env env0 sigma ~impls:impls_env ty [id] [arity] [imps] in - let env2,sigma,impls,newfs,data = - interp_fields_evars env_ar sigma impls_env nots (binders_of_decls fs) + let impls_env = + let params = List.map (RelDecl.get_name %> Name.get_id) assums in + let ty = Inductive (params, (finite != Declarations.BiFinite)) in + let ids = List.map (fun (id, _, _, _) -> id) records in + let imps = List.map (fun _ -> imps) arities in + compute_internalization_env env0 sigma ~impls:impls_env ty ids arities imps in + let fold sigma (_, _, nots, fs) arity = + let _, sigma, impls, newfs, _ = interp_fields_evars env_ar sigma impls_env nots (binders_of_decls fs) in + (sigma, (impls, newfs)) + in + let (sigma, data) = List.fold_left2_map fold sigma records arities in let sigma = Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar sigma (Evd.from_env env_ar) in - let sigma, typ = + let fold sigma (typ, sort) (_, newfs) = let _, univ = compute_constructor_level sigma env_ar newfs in if not def && (Sorts.is_prop sort || (Sorts.is_set sort && is_impredicative_set env0)) then @@ -167,16 +175,21 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = Evd.set_eq_sort env_ar sigma Set sort, EConstr.mkSort (Sorts.sort_of_univ univ) else sigma, typ in + let (sigma, typs) = List.fold_left2_map fold sigma typs data in let sigma = Evd.minimize_universes sigma in - let newfs = List.map (EConstr.to_rel_decl sigma) newfs in let newps = List.map (EConstr.to_rel_decl sigma) newps in - let typ = EConstr.to_constr sigma typ in - let ce t = Pretyping.check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr t) in let univs = Evd.check_univ_decl ~poly sigma decl in let ubinders = Evd.universe_binders sigma in - List.iter (iter_constr ce) (List.rev newps); + let ce t = Pretyping.check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr t) in + let () = List.iter (iter_constr ce) (List.rev newps) in + let map (impls, newfs) typ = + let newfs = List.map (EConstr.to_rel_decl sigma) newfs in + let typ = EConstr.to_constr sigma typ in List.iter (iter_constr ce) (List.rev newfs); - ubinders, univs, typ, template, imps, newps, impls, newfs + (typ, impls, newfs) + in + let ans = List.map2 map data typs in + ubinders, univs, template, newps, imps, ans let degenerate_decl decl = let id = match RelDecl.get_name decl with @@ -260,9 +273,10 @@ let subst_projection fid l c = raise (NotDefinable (MissingProj (fid,List.rev !bad_projs))); c'' -let instantiate_possibly_recursive_type indu paramdecls fields = +let instantiate_possibly_recursive_type ind u ntypes paramdecls fields = let subst = List.map_i (fun i _ -> mkRel i) 1 paramdecls in - Termops.substl_rel_context (subst@[mkIndU indu]) fields + let subst' = List.init ntypes (fun i -> mkIndU ((ind, ntypes - i - 1), u)) in + Termops.substl_rel_context (subst @ subst') fields let warn_non_primitive_record = CWarnings.create ~name:"non-primitive-record" ~category:"record" @@ -280,12 +294,11 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u | Monomorphic_const_entry ctx -> Univ.Instance.empty in let paramdecls = Inductive.inductive_paramdecls (mib, u) in - let indu = indsp, u in let r = mkIndU (indsp,u) in let rp = applist (r, Context.Rel.to_extended_list mkRel 0 paramdecls) in let paramargs = Context.Rel.to_extended_list mkRel 1 paramdecls in (*def in [[params;x:rp]]*) let x = Name binder_name in - let fields = instantiate_possibly_recursive_type indu paramdecls fields in + let fields = instantiate_possibly_recursive_type (fst indsp) u mib.mind_ntypes paramdecls fields in let lifted_fields = Termops.lift_rel_context 1 fields in let primitive = if !primitive_flag then @@ -373,12 +386,9 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u open Typeclasses -let declare_structure finite ubinders univs id idbuild paramimpls params arity template - fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers = - let nparams = List.length params and nfields = List.length fields in - let args = Context.Rel.to_extended_list mkRel nfields params in - let ind = applist (mkRel (1+nparams+nfields), args) in - let type_constructor = it_mkProd_or_LetIn ind fields in + +let declare_structure finite ubinders univs paramimpls params template ?(kind=StructureComponent) ?name record_data = + let nparams = List.length params in let template, ctx = match univs with | Monomorphic_ind_entry ctx -> @@ -388,37 +398,51 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t | Cumulative_ind_entry cumi -> false, Polymorphic_const_entry (Univ.CumulativityInfo.univ_context cumi) in - let binder_name = + let binder_name = match name with - | None -> Id.of_string (Unicode.lowercase_first_char (Id.to_string id)) + | None -> + let map (id, _, _, _, _, _, _) = + Id.of_string (Unicode.lowercase_first_char (Id.to_string id)) + in + Array.map_of_list map record_data | Some n -> n in - let mie_ind = + let ntypes = List.length record_data in + let mk_block i (id, idbuild, arity, _, fields, _, _) = + let nfields = List.length fields in + let args = Context.Rel.to_extended_list mkRel nfields params in + let ind = applist (mkRel (ntypes - i + nparams + nfields), args) in + let type_constructor = it_mkProd_or_LetIn ind fields in { mind_entry_typename = id; mind_entry_arity = arity; mind_entry_template = template; mind_entry_consnames = [idbuild]; mind_entry_lc = [type_constructor] } in + let blocks = List.mapi mk_block record_data in let mie = { mind_entry_params = List.map degenerate_decl params; - mind_entry_record = Some (if !primitive_flag then Some [|binder_name|] else None); + mind_entry_record = Some (if !primitive_flag then Some binder_name else None); mind_entry_finite = finite; - mind_entry_inds = [mie_ind]; + mind_entry_inds = blocks; mind_entry_private = None; mind_entry_universes = univs; } in let mie = InferCumulativity.infer_inductive (Global.env ()) mie in - let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders [(paramimpls,[])] in - let rsp = (kn,0) in (* This is ind path of idstruc *) - let cstr = (rsp,1) in - let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name coers ubinders fieldimpls fields in - let build = ConstructRef cstr in - let poly = match ctx with | Polymorphic_const_entry _ -> true | Monomorphic_const_entry _ -> false in - let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in - Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs); - rsp + let impls = List.map (fun _ -> paramimpls, []) record_data in + let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders impls in + let map i (_, _, _, fieldimpls, fields, is_coe, coers) = + let rsp = (kn, i) in (* This is ind path of idstruc *) + let cstr = (rsp, 1) in + let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers ubinders fieldimpls fields in + let build = ConstructRef cstr in + let poly = match ctx with | Polymorphic_const_entry _ -> true | Monomorphic_const_entry _ -> false in + let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in + let () = Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs) in + rsp + in + List.mapi map record_data let implicits_of_context ctx = List.map_i (fun i name -> @@ -430,22 +454,22 @@ let implicits_of_context ctx = 1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx))) let declare_class finite def cum ubinders univs id idbuild paramimpls params arity - template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities = + template fieldimpls fields ?(kind=StructureComponent) coers priorities = let fieldimpls = (* Make the class implicit in the projections, and the params if applicable. *) let len = List.length params in let impls = implicits_of_context params in List.map (fun x -> impls @ Impargs.lift_implicits (succ len) x) fieldimpls in - let binder_name = Namegen.next_ident_away (snd id) (Termops.vars_of_env (Global.env())) in - let impl, projs = + let binder_name = Namegen.next_ident_away id (Termops.vars_of_env (Global.env())) in + let data = match fields with | [LocalAssum (Name proj_name, field) | LocalDef (Name proj_name, _, field)] when def -> let class_body = it_mkLambda_or_LetIn field params in let class_type = it_mkProd_or_LetIn arity params in let class_entry = Declare.definition_entry ~types:class_type ~univs class_body in - let cst = Declare.declare_constant (snd id) + let cst = Declare.declare_constant id (DefinitionEntry class_entry, IsDefinition Definition) in let cstu = (cst, match univs with @@ -472,7 +496,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari | Some b -> Some ((if b then Backward else Forward), List.hd priorities) | None -> None in - cref, [Name proj_name, sub, Some proj_cst] + [cref, [Name proj_name, sub, Some proj_cst]] | _ -> let univs = match univs with @@ -484,18 +508,21 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari | Monomorphic_const_entry univs -> Monomorphic_ind_entry univs in - let ind = declare_structure Declarations.BiFinite ubinders univs (snd id) idbuild paramimpls - params arity template fieldimpls fields - ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) - in + let record_data = [id, idbuild, arity, fieldimpls, fields, false, List.map (fun _ -> false) fields] in + let inds = declare_structure Declarations.BiFinite ubinders univs paramimpls + params template ~kind:Method ~name:[|binder_name|] record_data + in let coers = List.map2 (fun coe pri -> Option.map (fun b -> if b then Backward, pri else Forward, pri) coe) coers priorities in - let l = List.map3 (fun decl b y -> RelDecl.get_name decl, b, y) - (List.rev fields) coers (Recordops.lookup_projections ind) - in IndRef ind, l + let map ind = + let l = List.map3 (fun decl b y -> RelDecl.get_name decl, b, y) + (List.rev fields) coers (Recordops.lookup_projections ind) + in IndRef ind, l + in + List.map map inds in let ctx_context = List.map (fun decl -> @@ -516,16 +543,19 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari | Monomorphic_const_entry _ -> Univ.AUContext.empty, ctx_context, fields in - let k = - { cl_univs = univs; - cl_impl = impl; - cl_strict = !typeclasses_strict; - cl_unique = !typeclasses_unique; - cl_context = ctx_context; - cl_props = fields; - cl_projs = projs } - in + let map (impl, projs) = + let k = + { cl_univs = univs; + cl_impl = impl; + cl_strict = !typeclasses_strict; + cl_unique = !typeclasses_unique; + cl_context = ctx_context; + cl_props = fields; + cl_projs = projs } + in add_class k; impl + in + List.map map data let add_constant_class cst = @@ -576,39 +606,72 @@ let declare_existing_class g = open Vernacexpr -(* [fs] corresponds to fields and [ps] to parameters; [coers] is a - list telling if the corresponding fields must me declared as coercions - or subinstances. *) -let definition_structure (kind,cum,poly,finite,(is_coe,({CAst.loc;v=idstruc},pl)),ps,cfs,idbuild,s) = - let cfs,notations = List.split cfs in - let cfs,priorities = List.split cfs in - let coers,fs = List.split cfs in - let extract_name acc = function +let check_unique_names records = + let extract_name acc (((_, bnd), _), _) = match bnd with Vernacexpr.AssumExpr({CAst.v=Name id},_) -> id::acc | Vernacexpr.DefExpr ({CAst.v=Name id},_,_) -> id::acc | _ -> acc in - let allnames = idstruc::(List.fold_left extract_name [] fs) in - let () = match List.duplicates Id.equal allnames with + let allnames = + List.fold_left (fun acc (_, id, _, _, cfs, _, _) -> + id.CAst.v :: (List.fold_left extract_name acc cfs)) [] records + in + match List.duplicates Id.equal allnames with | [] -> () | id :: _ -> user_err (str "Two objects have the same name" ++ spc () ++ quote (Id.print id)) - in + +let check_priorities kind records = let isnot_class = match kind with Class false -> false | _ -> true in - if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then - user_err Pp.(str "Priorities only allowed for type class substructures"); - (* Now, younger decl in params and fields is on top *) - let pl, univs, arity, template, implpars, params, implfs, fields = + let has_priority (_, _, _, _, cfs, _, _) = + List.exists (fun ((_, pri), _) -> not (Option.is_empty pri)) cfs + in + if isnot_class && List.exists has_priority records then + user_err Pp.(str "Priorities only allowed for type class substructures") + +let extract_record_data records = + let map (is_coe, id, _, _, cfs, idbuild, s) = + let fs = List.map (fun (((_, f), _), _) -> f) cfs in + id.CAst.v, s, List.map snd cfs, fs + in + let data = List.map map records in + let pss = List.map (fun (_, _, _, ps, _, _, _) -> ps) records in + let ps = match pss with + | [] -> CErrors.anomaly (str "Empty record block") + | ps :: rem -> + let eq_local_binders bl1 bl2 = List.equal local_binder_eq bl1 bl2 in + let () = + if not (List.for_all (eq_local_binders ps) rem) then + user_err (str "Parameters should be syntactically the \ + same for each inductive type.") + in + ps + in + (** FIXME: Same issue as #7754 *) + let _, _, pl, _, _, _, _ = List.hd records in + pl, ps, data + +(* [fs] corresponds to fields and [ps] to parameters; [coers] is a + list telling if the corresponding fields must me declared as coercions + or subinstances. *) +let definition_structure kind cum poly finite records = + let () = check_unique_names records in + let () = check_priorities kind records in + let pl, ps, data = extract_record_data records in + let pl, univs, template, params, implpars, data = States.with_state_protection (fun () -> - typecheck_params_and_fields finite (kind = Class true) idstruc poly pl s ps notations fs) () in + typecheck_params_and_fields finite (kind = Class true) poly pl ps data) () in match kind with | Class def -> - let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in - declare_class finite def cum pl univs (loc,idstruc) idbuild - implpars params arity template implfs fields is_coe coers priorities + let (_, id, _, _, cfs, idbuild, _), (arity, implfs, fields) = match records, data with + | [r], [d] -> r, d + | _, _ -> CErrors.user_err (str "Mutual definitional classes are not handled") + in + let priorities = List.map (fun ((_, id), _) -> {hint_priority = id; hint_pattern = None}) cfs in + let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in + declare_class finite def cum pl univs id.CAst.v idbuild + implpars params arity template implfs fields coers priorities | _ -> - let implfs = List.map - (fun impls -> implpars @ Impargs.lift_implicits - (succ (List.length params)) impls) implfs - in + let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in + let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in let univs = match univs with | Polymorphic_const_entry univs -> @@ -619,7 +682,11 @@ let definition_structure (kind,cum,poly,finite,(is_coe,({CAst.loc;v=idstruc},pl) | Monomorphic_const_entry univs -> Monomorphic_ind_entry univs in - let ind = declare_structure finite pl univs idstruc - idbuild implpars params arity template implfs - fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) in - IndRef ind + let map (arity, implfs, fields) (is_coe, id, _, _, cfs, idbuild, _) = + let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in + let coe = List.map (fun coe -> not (Option.is_empty coe)) coers in + id.CAst.v, idbuild, arity, implfs, fields, is_coe, coe + in + let data = List.map2 map data records in + let inds = declare_structure finite pl univs implpars params template data in + List.map (fun ind -> IndRef ind) inds diff --git a/vernac/record.mli b/vernac/record.mli index f46f59c14..567f2b313 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -26,9 +26,14 @@ val declare_projections : (Name.t * bool) list * Constant.t option list val definition_structure : - inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic * - Declarations.recursivity_kind * ident_decl with_coercion * local_binder_expr list * + inductive_kind -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic -> + Declarations.recursivity_kind -> + (coercion_flag * + Names.lident * + universe_decl_expr option * + local_binder_expr list * (local_decl_expr with_instance with_priority with_notation) list * - Id.t * constr_expr option -> GlobRef.t + Id.t * constr_expr option) list -> + GlobRef.t list val declare_existing_class : GlobRef.t -> unit diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 479482095..6d1abeca1 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -263,15 +263,13 @@ let print_namespace ns = let matches mp = match match_modulepath ns mp with | Some [] -> true | _ -> false in - let constants = (Global.env ()).Environ.env_globals.Environ.env_constants in let constants_in_namespace = - Cmap_env.fold (fun c (body,_) acc -> - let kn = Constant.user c in - if matches (KerName.modpath kn) then - acc++fnl()++hov 2 (print_constant kn body) - else - acc - ) constants (str"") + Environ.fold_constants (fun c body acc -> + let kn = Constant.user c in + if matches (KerName.modpath kn) + then acc++fnl()++hov 2 (print_constant kn body) + else acc) + (Global.env ()) (str"") in (print_list Id.print ns)++str":"++fnl()++constants_in_namespace @@ -539,25 +537,36 @@ let should_treat_as_cumulative cum poly = else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.") | None -> poly && Flags.is_polymorphic_inductive_cumulativity () -let vernac_record cum k poly finite struc binders sort nameopt cfs = +let vernac_record cum k poly finite records = let is_cumulative = should_treat_as_cumulative cum poly in - let const = match nameopt with - | None -> add_prefix "Build_" (fst (snd struc)).v - | Some ({v=id} as lid) -> - Dumpglob.dump_definition lid false "constr"; id in - if Dumpglob.dump () then ( - Dumpglob.dump_definition (fst (snd struc)) false "rec"; - List.iter (fun (((_, x), _), _) -> - match x with - | Vernacexpr.AssumExpr ({loc;v=Name id}, _) -> Dumpglob.dump_definition (make ?loc id) false "proj" - | _ -> ()) cfs); - ignore(Record.definition_structure (k,is_cumulative,poly,finite,struc,binders,cfs,const,sort)) + let map ((coe, (id, pl)), binders, sort, nameopt, cfs) = + let const = match nameopt with + | None -> add_prefix "Build_" id.v + | Some lid -> + let () = Dumpglob.dump_definition lid false "constr" in + lid.v + in + let () = + if Dumpglob.dump () then + let () = Dumpglob.dump_definition id false "rec" in + let iter (((_, x), _), _) = match x with + | Vernacexpr.AssumExpr ({loc;v=Name id}, _) -> + Dumpglob.dump_definition (make ?loc id) false "proj" + | _ -> () + in + List.iter iter cfs + in + coe, id, pl, binders, cfs, const, sort + in + let records = List.map map records in + ignore(Record.definition_structure k is_cumulative poly finite records) (** When [poly] is true the type is declared polymorphic. When [lo] is true, then the type is declared private (as per the [Private] keyword). [finite] indicates whether the type is inductive, co-inductive or neither. *) let vernac_inductive ~atts cum lo finite indl = + let open Pp in if Dumpglob.dump () then List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) -> match cstrs with @@ -567,35 +576,85 @@ let vernac_inductive ~atts cum lo finite indl = Dumpglob.dump_definition lid false "constr") cstrs | _ -> () (* dumping is done by vernac_record (called below) *) ) indl; + let is_record = function + | ((_ , _ , _ , _, RecordDecl _), _) -> true + | _ -> false + in + let is_constructor = function + | ((_ , _ , _ , _, Constructors _), _) -> true + | _ -> false + in + let is_defclass = match indl with + | [ ( id , bl , c , Class _, Constructors [l]), [] ] -> Some (id, bl, c, l) + | _ -> None + in + if Option.has_some is_defclass then + (** Definitional class case *) + let (id, bl, c, l) = Option.get is_defclass in + let (coe, (lid, ce)) = l in + let coe' = if coe then Some true else None in + let f = (((coe', AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce)), None), []) in + vernac_record cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]] + else if List.for_all is_record indl then + (** Mutual record case *) + let check_kind ((_, _, _, kind, _), _) = match kind with + | Variant -> + user_err (str "The Variant keyword does not support syntax { ... }.") + | Record | Structure | Class _ | Inductive_kw | CoInductive -> () + in + let () = List.iter check_kind indl in + let check_where ((_, _, _, _, _), wh) = match wh with + | [] -> () + | _ :: _ -> + user_err (str "where clause not supported for records") + in + let () = List.iter check_where indl in + let unpack ((id, bl, c, _, decl), _) = match decl with + | RecordDecl (oc, fs) -> + (id, bl, c, oc, fs) + | Constructors _ -> assert false (** ruled out above *) + in + let ((_, _, _, kind, _), _) = List.hd indl in + let kind = match kind with Class _ -> Class false | _ -> kind in + let recordl = List.map unpack indl in + vernac_record cum kind atts.polymorphic finite recordl + else if List.for_all is_constructor indl then + (** Mutual inductive case *) + let check_kind ((_, _, _, kind, _), _) = match kind with + | (Record | Structure) -> + user_err (str "The Record keyword is for types defined using the syntax { ... }.") + | Class _ -> + user_err (str "Inductive classes not supported") + | Variant | Inductive_kw | CoInductive -> () + in + let () = List.iter check_kind indl in + let check_name ((na, _, _, _, _), _) = match na with + | (true, _) -> + user_err (str "Variant types do not handle the \"> Name\" \ + syntax, which is reserved for records. Use the \":>\" \ + syntax on constructors instead.") + | _ -> () + in + let () = List.iter check_name indl in + let unpack (((_, id) , bl, c, _, decl), ntn) = match decl with + | Constructors l -> (id, bl, c, l), ntn + | RecordDecl _ -> assert false (* ruled out above *) + in + let indl = List.map unpack indl in + let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in + ComInductive.do_mutual_inductive indl is_cumulative atts.polymorphic lo finite + else + user_err (str "Mixed record-inductive definitions are not allowed") +(* + match indl with - | [ ( _ , _ , _ ,(Record|Structure), Constructors _ ),_ ] -> - user_err Pp.(str "The Record keyword is for types defined using the syntax { ... }.") - | [ (_ , _ , _ ,Variant, RecordDecl _),_ ] -> - user_err Pp.(str "The Variant keyword does not support syntax { ... }.") - | [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] -> - vernac_record cum (match b with Class _ -> Class false | _ -> b) - atts.polymorphic finite id bl c oc fs | [ ( id , bl , c , Class _, Constructors [l]), [] ] -> let f = let (coe, ({loc;v=id}, ce)) = l in let coe' = if coe then Some true else None in (((coe', AssumExpr ((make ?loc @@ Name id), ce)), None), []) - in vernac_record cum (Class true) atts.polymorphic finite id bl c None [f] - | [ ( _ , _, _, Class _, Constructors _), [] ] -> - user_err Pp.(str "Inductive classes not supported") - | [ ( id , bl , c , Class _, _), _ :: _ ] -> - user_err Pp.(str "where clause not supported for classes") - | [ ( _ , _ , _ , _, RecordDecl _ ) , _ ] -> - user_err Pp.(str "where clause not supported for (co)inductive records") - | _ -> let unpack = function - | ( (false, id) , bl , c , _ , Constructors l ) , ntn -> ( id , bl , c , l ) , ntn - | ( (true,_),_,_,_,Constructors _),_ -> - user_err Pp.(str "Variant types do not handle the \"> Name\" syntax, which is reserved for records. Use the \":>\" syntax on constructors instead.") - | _ -> user_err Pp.(str "Cannot handle mutually (co)inductive records.") - in - let indl = List.map unpack indl in - let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in - ComInductive.do_mutual_inductive indl is_cumulative atts.polymorphic lo finite + in vernac_record cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]] + *) let vernac_fixpoint ~atts discharge l = let local = enforce_locality_exp atts.locality discharge in |