diff options
43 files changed, 422 insertions, 344 deletions
diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md index 3bd3342329..df9e14b178 100644 --- a/.github/PULL_REQUEST_TEMPLATE.md +++ b/.github/PULL_REQUEST_TEMPLATE.md @@ -17,3 +17,5 @@ Fixes / closes #???? <!-- (Otherwise, remove these lines.) --> - [ ] Corresponding documentation was added / updated (including any warning and error messages added / removed / modified). - [ ] Entry added in the changelog (see https://github.com/coq/coq/tree/master/doc/changelog#unreleased-changelog for details). +- [ ] Overlay pull requests (if this breaks 3rd party developments in CI, see +https://github.com/coq/coq/blob/master/dev/ci/user-overlays/README.md for details) @@ -22,6 +22,7 @@ Yves Bertot <yves.bertot@inria.fr> Yves Bertot <bertot@inria.fr> Yves Bertot <yves.bertot@inria.fr> Yves Bertot <Yves.Bertot@inria.fr> Yves Bertot <yves.bertot@inria.fr> Yves Bertot <bertot@nardis.inria.fr> Frédéric Besson <frederic.besson@inria.fr> fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7> +Frédéric Besson <frederic.besson@inria.fr> BESSON Frederic <frederic.besson@inria.fr> Siddharth Bhat <siddu.druid@gmail.com> Siddharth <siddu.druid@gmail.com> Lasse Blaauwbroek <lasse@blaauwbroek.eu> Lasse Blaauwbroek <lasse@lasse-work.localdomain> Simon Boulier <simon.boulier@ens-rennes.fr> SimonBoulier <simon.boulier@ens-rennes.fr> @@ -72,6 +73,7 @@ Vincent Gross <vgross@gforge> vgross <vgross@85f007b7-540e- Huang Guan-Shieng <huang@gforge> huang <huang@85f007b7-540e-0410-9357-904b9bb8a0f7> Hugo Herbelin <Hugo.Herbelin@inria.fr> herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> Hugo Herbelin <Hugo.Herbelin@inria.fr> Hugo Herbelin <herbelin@users.noreply.github.com> +Wolf Honore <wolfhonore@gmail.com> whonore <wolfhonore@gmail.com> Jasper Hugunin <jasperh@cs.washington.edu> Jasper Hugunin <jasper@hashplex.com> Tom Hutchinson <thutchin@gforge> thutchin <thutchin@85f007b7-540e-0410-9357-904b9bb8a0f7> Cezary Kaliszyk <cek@gforge> cek <cek@85f007b7-540e-0410-9357-904b9bb8a0f7> @@ -91,7 +93,6 @@ Larry Darryl Lee Jr. <llee454@gmail.com> llee454@gmail.com <llee454@gm Xavier Leroy <xavier.leroy@college-de-france.fr> Xavier Leroy <xavier.leroy@inria.fr> Pierre Letouzey <pierre.letouzey@inria.fr> letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> Pierre Letouzey <pierre.letouzey@inria.fr> letouzey <pierre.letouzey@inria.fr> -Xia Li-yao <lysxia@gmail.com> Lysxia <lysxia@gmail.com> Yishuai Li <yishuai@cis.upenn.edu> Yishuai Li <yishuai@upenn.edu> Assia Mahboubi <assia.mahboubi@inria.fr> amahboub <amahboub@85f007b7-540e-0410-9357-904b9bb8a0f7> Kenji Maillard <kenji.maillard@inria.fr> Kenji Maillard <kenji@maillard.blue> @@ -154,6 +155,9 @@ Laurent Théry <laurent.thery@inria.fr> Laurent Théry <thery@sophia Laurent Théry <laurent.thery@inria.fr> thery <Laurent.Thery@inria.fr> Anton Trunov <anton.a.trunov@gmail.com> Anton Trunov <anton.trunov@imdea.org> Benjamin Werner <werner@gforge> werner <werner@85f007b7-540e-0410-9357-904b9bb8a0f7> +Li-yao Xia <lysxia@gmail.com> Lysxia <lysxia@gmail.com> +Li-yao Xia <lysxia@gmail.com> Xia Li-yao <lysxia@gmail.com> +Li-yao Xia <lysxia@gmail.com> Xia Li-yao <Lysxia@users.noreply.github.com> Wang Zhuyang <hawnzug@gmail.com> hawnzug <hawnzug@gmail.com> Beta Ziliani <beta@mpi-sws.org> Beta Ziliani <bziliani@famaf.unc.edu.ar> Beta Ziliani <beta@mpi-sws.org> beta <beta@mpi-sws.org> diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index a96b93154c..361270ff32 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -643,7 +643,7 @@ reviewers, with specific requests. - [needs: benchmarking][needs-benchmarking] and [needs: testing][needs-testing] indicate the PR needs testing beyond what the test suite can handle. For example, performance benchmarking is currently performed with a different - infrastructure ([documented in the wiki][jenkins-doc]). Unless some followup + infrastructure ([documented in the wiki][Benchmarking]). Unless some followup is specifically requested, you aren't expected to do this additional testing. More generally, such labels should come with a description that should @@ -1007,7 +1007,7 @@ to prepare overlays, and propose a simplified and documented procedure. We also have a benchmarking infrastructure, which is documented [on -the wiki][jenkins-doc]. +the wiki][Benchmarking]. ##### Restarting failed jobs ##### @@ -1225,6 +1225,7 @@ can be found [on the wiki][wiki-CUDW]. [add-contributor]: https://github.com/orgs/coq/teams/contributors/members?add=true [api-doc]: https://coq.github.io/doc/master/api/ +[Benchmarking]: https://github.com/coq/coq/wiki/Benchmarking [CEP]: https://github.com/coq/ceps [check-owners]: dev/tools/check-owners-pr.sh [CI-README-developers]: dev/ci/README-developers.md @@ -1272,7 +1273,6 @@ can be found [on the wiki][wiki-CUDW]. [GitLab-coq]: https://gitlab.com/coq [GitLab-doc]: https://docs.gitlab.com/ [JasonGross-coq-tools]: https://github.com/JasonGross/coq-tools -[jenkins-doc]: https://github.com/coq/coq/wiki/Jenkins-(automated-benchmarking) [kind-documentation]: https://github.com/coq/coq/issues?q=is%3Aopen+is%3Aissue+label%3A%22kind%3A+documentation%22 [master-doc]: https://coq.github.io/doc/master/refman/ [merge-pr]: dev/tools/merge-pr.sh diff --git a/default.nix b/default.nix index f838f17d07..4700a6ed64 100644 --- a/default.nix +++ b/default.nix @@ -33,7 +33,7 @@ }: with pkgs; -with stdenv.lib; +with pkgs.lib; stdenv.mkDerivation rec { diff --git a/dev/base_include b/dev/base_include index f375a867bc..061bf1f3e1 100644 --- a/dev/base_include +++ b/dev/base_include @@ -16,7 +16,6 @@ #install_printer (* kernel_name *) ppkn;; #install_printer (* constant *) ppcon;; #install_printer (* projection *) ppproj;; -#install_printer (* cl_index *) ppclindex;; #install_printer (* recarg Rtree.t *) ppwf_paths;; #install_printer (* constr *) print_pure_constr;; #install_printer (* patch *) ppripos;; diff --git a/dev/ci/user-overlays/13912-pi8027-remove-bijint.sh b/dev/ci/user-overlays/13912-pi8027-remove-bijint.sh new file mode 100644 index 0000000000..d860cfec01 --- /dev/null +++ b/dev/ci/user-overlays/13912-pi8027-remove-bijint.sh @@ -0,0 +1 @@ +overlay elpi https://github.com/pi8027/coq-elpi coq-overlay-13912 13912 diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index 57c325f698..1697a19668 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -114,6 +114,11 @@ list of contributors between Coq revisions. Typically used with `VX.X+alpha..vX.X` to check the contributors of version `VX.X`. + Note that this script relies on `.mailmap` to merge multiple + identities. If you notice anything incorrect while using it, use + the opportunity to fix the `.mailmap` file. Same thing if you want + to have the full name of a contributor shown instead of a pseudonym. + ## For each release (preview, final, patch-level) ## - [ ] Ensure that there exists a milestone for the following version. diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix index a582a70e0a..37e39a99a9 100644 --- a/dev/nixpkgs.nix +++ b/dev/nixpkgs.nix @@ -1,4 +1,4 @@ import (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/0bbeca2ff952e6a171534793ddd0fa97c8f9546a.tar.gz"; - sha256 = "0h1y4ffvyvkqs6k2pak02pby25va7c6c1y4p8xkwlzqwswxqxvfl"; + url = "https://github.com/NixOS/nixpkgs/archive/5c7a370a208d93d458193fc05ed84ced0ba7f387.tar.gz"; + sha256 = "1jkn71xscsk4rb0agbp5saf06hy36qvy512zzh3881pkkn67i9js"; }) diff --git a/dev/tools/list-contributors.sh b/dev/tools/list-contributors.sh index c968f2e952..0b0d01c7e2 100644..100755 --- a/dev/tools/list-contributors.sh +++ b/dev/tools/list-contributors.sh @@ -1,15 +1,15 @@ #!/usr/bin/env bash # For compat with OSX which has a non-gnu sed which doesn't support -z -SED=`which gsed || which sed` +SED=`(which gsed || which sed) 2> /dev/null` if [ $# != 1 ]; then - error "usage: $0 rev0..rev1" + echo "usage: $0 rev0..rev1" exit 1 fi git shortlog -s -n --group=author --group=trailer:Co-authored-by $1 | cut -f2 | sort -k 2 | grep -v -e "coqbot" -e "^$" > contributors.tmp cat contributors.tmp | wc -l | xargs echo "Contributors:" -cat contributors.tmp | gsed -z "s/\n/, /g" +cat contributors.tmp | $SED -z "s/\n/, /g" echo rm contributors.tmp diff --git a/dev/top_printers.ml b/dev/top_printers.ml index f8fd8b3d5b..67fe7b980b 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -52,7 +52,6 @@ let ppmind kn = pp(MutInd.debug_print kn) let ppind (kn,i) = pp(MutInd.debug_print kn ++ str"," ++int i) let ppsp sp = pp(pr_path sp) let ppqualid qid = pp(pr_qualid qid) -let ppclindex cl = pp(Coercionops.pr_cl_index cl) let ppscheme k = pp (Ind_tables.pr_scheme_kind k) let prrecarg = Declareops.pp_recarg diff --git a/dev/top_printers.mli b/dev/top_printers.mli index b4b24d743a..ba7d92f907 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -29,8 +29,6 @@ val ppind : Names.inductive -> unit val ppsp : Libnames.full_path -> unit val ppqualid : Libnames.qualid -> unit -val ppclindex : Coercionops.cl_index -> unit - val ppscheme : 'a Ind_tables.scheme_kind -> unit val prrecarg : Declarations.recarg -> Pp.t diff --git a/doc/changelog/03-notations/13840-print-prim.rst b/doc/changelog/03-notations/13840-print-prim.rst new file mode 100644 index 0000000000..d6e3184662 --- /dev/null +++ b/doc/changelog/03-notations/13840-print-prim.rst @@ -0,0 +1,11 @@ +- **Changed:** + Flag :flag:`Printing Notations` no longer controls + whether strings and numbers are printed raw + (`#13840 <https://github.com/coq/coq/pull/13840>`_, + by Enrico Tassi). + +- **Added:** + Flag :flag:`Printing Raw Literals` to control whether + strings and numbers are printed raw. + (`#13840 <https://github.com/coq/coq/pull/13840>`_, + by Enrico Tassi). diff --git a/doc/changelog/07-vernac-commands-and-options/13912-remove-bijint.rst b/doc/changelog/07-vernac-commands-and-options/13912-remove-bijint.rst new file mode 100644 index 0000000000..99efda3a5b --- /dev/null +++ b/doc/changelog/07-vernac-commands-and-options/13912-remove-bijint.rst @@ -0,0 +1,5 @@ +- **Changed:** + The printing order of :cmd:`Print Classes` and :cmd:`Print Graph`, due to the + changes for the internal tables of coercion classes and coercion paths. + (`#13912 <https://github.com/coq/coq/pull/13912>`_, + by Kazuhiko Sakaguchi). diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 557ef10555..453e878a5d 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -442,6 +442,12 @@ Displaying information about notations Controls whether to use notations for printing terms wherever possible. Default is on. +.. flag:: Printing Raw Literals + + Controls whether to use string and number notations for printing terms + wherever possible (see :ref:`string-notations`). + Default is off. + .. flag:: Printing Parentheses If on, parentheses are printed even if implied by associativity and precedence diff --git a/engine/termops.ml b/engine/termops.ml index 4dc584cfa8..d60aa69ccb 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -979,69 +979,52 @@ let collapse_appl sigma c = match EConstr.kind sigma c with (* First utilities for avoiding telescope computation for subst_term *) -let prefix_application sigma eq_fun (k,c) t = +let prefix_application sigma eq_fun k l1 t = let open EConstr in - let c' = collapse_appl sigma c and t' = collapse_appl sigma t in - match EConstr.kind sigma c', EConstr.kind sigma t' with - | App (f1,cl1), App (f2,cl2) -> - let l1 = Array.length cl1 - and l2 = Array.length cl2 in + let t' = collapse_appl sigma t in + if 0 < l1 then match EConstr.kind sigma t' with + | App (f2,cl2) -> + let l2 = Array.length cl2 in if l1 <= l2 - && eq_fun sigma c' (mkApp (f2, Array.sub cl2 0 l1)) then - Some (mkApp (mkRel k, Array.sub cl2 l1 (l2 - l1))) + && eq_fun sigma k (mkApp (f2, Array.sub cl2 0 l1)) then + Some (Array.sub cl2 l1 (l2 - l1)) else None | _ -> None + else None -let my_prefix_application sigma eq_fun (k,c) by_c t = - let open EConstr in - let c' = collapse_appl sigma c and t' = collapse_appl sigma t in - match EConstr.kind sigma c', EConstr.kind sigma t' with - | App (f1,cl1), App (f2,cl2) -> - let l1 = Array.length cl1 - and l2 = Array.length cl2 in - if l1 <= l2 - && eq_fun sigma c' (mkApp (f2, Array.sub cl2 0 l1)) then - Some (mkApp ((Vars.lift k by_c), Array.sub cl2 l1 (l2 - l1))) - else - None - | _ -> None - -(* Recognizing occurrences of a given subterm in a term: [subst_term c t] - substitutes [(Rel 1)] for all occurrences of term [c] in a term [t]; - works if [c] has rels *) - -let subst_term_gen sigma eq_fun c t = - let open EConstr in - let open Vars in - let rec substrec (k,c as kc) t = - match prefix_application sigma eq_fun kc t with - | Some x -> x - | None -> - if eq_fun sigma c t then mkRel k - else - EConstr.map_with_binders sigma (fun (k,c) -> (k+1,lift 1 c)) substrec kc t +let eq_upto_lift cache c sigma k t = + let c = + try Int.Map.find k !cache + with Not_found -> + let c = EConstr.Vars.lift k c in + let () = cache := Int.Map.add k c !cache in + c in - substrec (1,c) t - -let subst_term sigma c t = subst_term_gen sigma EConstr.eq_constr c t + EConstr.eq_constr sigma c t (* Recognizing occurrences of a given subterm in a term : [replace_term c1 c2 t] substitutes [c2] for all occurrences of term [c1] in a term [t]; works if [c1] and [c2] have rels *) -let replace_term_gen sigma eq_fun c by_c in_t = - let rec substrec (k,c as kc) t = - match my_prefix_application sigma eq_fun kc by_c t with - | Some x -> x +let replace_term_gen sigma eq_fun ar by_c in_t = + let rec substrec k t = + match prefix_application sigma eq_fun k ar t with + | Some args -> EConstr.mkApp (EConstr.Vars.lift k by_c, args) | None -> - (if eq_fun sigma c t then (EConstr.Vars.lift k by_c) else - EConstr.map_with_binders sigma (fun (k,c) -> (k+1,EConstr.Vars.lift 1 c)) - substrec kc t) + (if eq_fun sigma k t then (EConstr.Vars.lift k by_c) else + EConstr.map_with_binders sigma succ substrec k t) in - substrec (0,c) in_t + substrec 0 in_t + +let replace_term sigma c byc t = + let cache = ref Int.Map.empty in + let c = collapse_appl sigma c in + let ar = Array.length (snd (decompose_app_vect sigma c)) in + let eq sigma k t = eq_upto_lift cache c sigma k t in + replace_term_gen sigma eq ar byc t -let replace_term sigma c byc t = replace_term_gen sigma EConstr.eq_constr c byc t +let subst_term sigma c t = replace_term sigma c (EConstr.mkRel 1) t let vars_of_env env = let s = Environ.ids_of_named_context_val (Environ.named_context_val env) in diff --git a/engine/termops.mli b/engine/termops.mli index 12df61e4c8..bdde2c450d 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -122,16 +122,12 @@ val pop : constr -> constr (** Substitution of an arbitrary large term. Uses equality modulo reduction of let *) -(** [subst_term_gen eq d c] replaces [d] by [Rel 1] in [c] using [eq] - as equality *) -val subst_term_gen : Evd.evar_map -> - (Evd.evar_map -> constr -> constr -> bool) -> constr -> constr -> constr - -(** [replace_term_gen eq d e c] replaces [d] by [e] in [c] using [eq] - as equality *) +(** [replace_term_gen eq arity e c] replaces matching subterms according to + [eq] by [e] in [c]. If [arity] is non-zero applications of larger length + are handled atomically. *) val replace_term_gen : - Evd.evar_map -> (Evd.evar_map -> constr -> constr -> bool) -> - constr -> constr -> constr -> constr + Evd.evar_map -> (Evd.evar_map -> int -> constr -> bool) -> + int -> constr -> constr -> constr (** [subst_term d c] replaces [d] by [Rel 1] in [c] *) val subst_term : Evd.evar_map -> constr -> constr -> constr diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 4fb7861ca6..3cabf52197 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -64,7 +64,7 @@ let print_parentheses = Notation_ops.print_parentheses (* This forces printing universe names of Type{.} *) let print_universes = Detyping.print_universes -(* This suppresses printing of primitive tokens (e.g. numeral) and notations *) +(* This suppresses printing of notations *) let print_no_symbol = ref false (* This tells to skip types if a variable has this type by default *) @@ -74,6 +74,9 @@ let print_use_implicit_types = ~key:["Printing";"Use";"Implicit";"Types"] ~value:true +(* Print primitive tokens, like strings *) +let print_raw_literal = ref false + (**********************************************************************) let hole = CAst.make @@ CHole (None, IntroAnonymous, None) @@ -434,7 +437,7 @@ let extern_record_pattern cstrsp args = (* Better to use extern_glob_constr composed with injection/retraction ?? *) let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = try - if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match; + if !Flags.in_debugger || !Flags.raw_print || !print_raw_literal then raise No_match; let (na,p,key) = uninterp_prim_token_cases_pattern pat scopes in match availability_of_entry_coercion custom InConstrEntrySomeLevel with | None -> raise No_match @@ -853,6 +856,7 @@ let same_binder_type ty nal c = (* one with no delimiter if possible) *) let extern_possible_prim_token (custom,scopes) r = + if !print_raw_literal then raise No_match; let (n,key) = uninterp_prim_token r scopes in match availability_of_entry_coercion custom InConstrEntrySomeLevel with | None -> raise No_match @@ -1261,11 +1265,12 @@ and extern_eqn inctx scopes vars {CAst.loc;v=(ids,pll,c)} = make ?loc (pll,extern inctx scopes vars c) and extern_notations inctx scopes vars nargs t = - if !Flags.raw_print || !print_no_symbol then raise No_match; + if !Flags.raw_print then raise No_match; try extern_possible_prim_token scopes t with No_match -> - let t = flatten_application t in - extern_notation inctx scopes vars t (filter_enough_applied nargs (uninterp_notations t)) + if !print_no_symbol then raise No_match; + let t = flatten_application t in + extern_notation inctx scopes vars t (filter_enough_applied nargs (uninterp_notations t)) and extern_notation inctx (custom,scopes as allscopes) vars t rules = match rules with diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 298b52f0be..bb49c8697d 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -60,6 +60,7 @@ val print_parentheses : bool ref val print_universes : bool ref val print_no_symbol : bool ref val print_projections : bool ref +val print_raw_literal : bool ref (** Customization of the global_reference printer *) val set_extern_reference : diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 1432fb9310..d31d7a03b6 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -196,8 +196,9 @@ let vm_conv_gen cv_pb env univs t1 t2 = TransparentState.full env univs t1 t2 else try - let v1 = val_of_constr env t1 in - let v2 = val_of_constr env t2 in + let sigma _ = assert false in + let v1 = val_of_constr env sigma t1 in + let v2 = val_of_constr env sigma t2 in fst (conv_val env cv_pb (nb_rel env) v1 v2 univs) with Not_found | Invalid_argument _ -> warn_bytecode_compiler_failed (); diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml index 20de4bc81b..7d3b3469b0 100644 --- a/kernel/vmbytegen.ml +++ b/kernel/vmbytegen.ml @@ -840,21 +840,21 @@ let dump_bytecodes init code fvs = prlist_with_sep (fun () -> str "; ") pp_fv_elem fvs ++ fnl ()) -let compile ~fail_on_error ?universes:(universes=0) env c = +let compile ~fail_on_error ?universes:(universes=0) env sigma c = init_fun_code (); Label.reset_label_counter (); let cont = [Kstop] in try let cenv, init_code = if Int.equal universes 0 then - let lam = lambda_of_constr ~optimize:true env c in + let lam = lambda_of_constr ~optimize:true env sigma c in let cenv = empty_comp_env () in cenv, ensure_stack_capacity (compile_lam env cenv lam 0) cont else (* We are going to generate a lambda, but merge the universe closure * with the function closure if it exists. *) - let lam = lambda_of_constr ~optimize:true env c in + let lam = lambda_of_constr ~optimize:true env sigma c in let params, body = decompose_Llam lam in let arity = Array.length params in let cenv = empty_comp_env () in @@ -896,7 +896,8 @@ let compile_constant_body ~fail_on_error env univs = function let con= Constant.make1 (Constant.canonical kn') in Some (BCalias (get_alias env con)) | _ -> - let res = compile ~fail_on_error ~universes:instance_size env body in + let sigma _ = assert false in + let res = compile ~fail_on_error ~universes:instance_size env sigma body in Option.map (fun x -> BCdefined (to_memory x)) res (* Shortcut of the previous function used during module strengthening *) diff --git a/kernel/vmbytegen.mli b/kernel/vmbytegen.mli index aef7ac3d6b..c724cad5ec 100644 --- a/kernel/vmbytegen.mli +++ b/kernel/vmbytegen.mli @@ -15,8 +15,10 @@ open Declarations open Environ (** Should only be used for monomorphic terms *) -val compile : fail_on_error:bool -> - ?universes:int -> env -> constr -> (bytecodes * bytecodes * fv) option +val compile : + fail_on_error:bool -> ?universes:int -> + env -> (existential -> constr option) -> constr -> + (bytecodes * bytecodes * fv) option (** init, fun, fv *) val compile_constant_body : fail_on_error:bool -> diff --git a/kernel/vmlambda.ml b/kernel/vmlambda.ml index 91de58b0e6..e353348ac7 100644 --- a/kernel/vmlambda.ml +++ b/kernel/vmlambda.ml @@ -591,12 +591,14 @@ struct type t = { global_env : env; + evar_body : existential -> constr option; name_rel : Name.t Vect.t; construct_tbl : (constructor, constructor_info) Hashtbl.t; } - let make env = { + let make env sigma = { global_env = env; + evar_body = sigma; name_rel = Vect.make 16 Anonymous; construct_tbl = Hashtbl.create 111 } @@ -633,9 +635,13 @@ open Renv let rec lambda_of_constr env c = match Constr.kind c with | Meta _ -> raise (Invalid_argument "Vmbytegen.lambda_of_constr: Meta") - | Evar (evk, args) -> - let args = Array.map_of_list (fun c -> lambda_of_constr env c) args in - Levar (evk, args) + | Evar (evk, args as ev) -> + begin match env.evar_body ev with + | None -> + let args = Array.map_of_list (fun c -> lambda_of_constr env c) args in + Levar (evk, args) + | Some t -> lambda_of_constr env t + end | Cast (c, _, _) -> lambda_of_constr env c @@ -774,8 +780,8 @@ let optimize_lambda lam = let lam = simplify subst_id lam in remove_let subst_id lam -let lambda_of_constr ~optimize genv c = - let env = Renv.make genv in +let lambda_of_constr ~optimize genv sigma c = + let env = Renv.make genv sigma in let ids = List.rev_map Context.Rel.Declaration.get_annot (rel_context genv) in Renv.push_rels env (Array.of_list ids); let lam = lambda_of_constr env c in diff --git a/kernel/vmlambda.mli b/kernel/vmlambda.mli index ad5f81638f..03d3393219 100644 --- a/kernel/vmlambda.mli +++ b/kernel/vmlambda.mli @@ -33,7 +33,7 @@ and fix_decl = Name.t Context.binder_annot array * lambda array * lambda array exception TooLargeInductive of Pp.t -val lambda_of_constr : optimize:bool -> env -> Constr.t -> lambda +val lambda_of_constr : optimize:bool -> env -> (existential -> constr option) -> Constr.t -> lambda val decompose_Llam : lambda -> Name.t Context.binder_annot array * lambda diff --git a/kernel/vmsymtable.ml b/kernel/vmsymtable.ml index ae0fa38571..90ee1c5378 100644 --- a/kernel/vmsymtable.ml +++ b/kernel/vmsymtable.ml @@ -144,7 +144,7 @@ let slot_for_proj_name key = ProjNameTable.add proj_name_tbl key n; n -let rec slot_for_getglobal env kn = +let rec slot_for_getglobal env sigma kn = let (cb,(_,rk)) = lookup_constant_key kn env in try key rk with NotEvaluated -> @@ -155,22 +155,22 @@ let rec slot_for_getglobal env kn = | Some code -> match Vmemitcodes.force code with | BCdefined(code,pl,fv) -> - let v = eval_to_patch env (code,pl,fv) in + let v = eval_to_patch env sigma (code,pl,fv) in set_global v - | BCalias kn' -> slot_for_getglobal env kn' + | BCalias kn' -> slot_for_getglobal env sigma kn' | BCconstant -> set_global (val_of_constant kn) in (*Pp.msgnl(str"value stored at: "++int pos);*) rk := Some (CEphemeron.create pos); pos -and slot_for_fv env fv = +and slot_for_fv env sigma fv = let fill_fv_cache cache id v_of_id env_of_id b = let v,d = match b with | None -> v_of_id id, Id.Set.empty | Some c -> - val_of_constr (env_of_id id env) c, + val_of_constr (env_of_id id env) sigma c, Environ.global_vars_set env c in build_lazy_val cache (v, d); v in let val_of_rel i = val_of_rel (nb_rel env - i) in @@ -194,11 +194,11 @@ and slot_for_fv env fv = | FVuniv_var _idu -> assert false -and eval_to_patch env (buff,pl,fv) = +and eval_to_patch env sigma (buff,pl,fv) = let slots = function | Reloc_annot a -> slot_for_annot a | Reloc_const sc -> slot_for_str_cst sc - | Reloc_getglobal kn -> slot_for_getglobal env kn + | Reloc_getglobal kn -> slot_for_getglobal env sigma kn | Reloc_proj_name p -> slot_for_proj_name p | Reloc_caml_prim op -> slot_for_caml_prim op in @@ -207,13 +207,13 @@ and eval_to_patch env (buff,pl,fv) = (* Environment should look like a closure, so free variables start at slot 2. *) let a = Array.make (Array.length fv + 2) crazy_val in a.(1) <- Obj.magic 2; - Array.iteri (fun i v -> a.(i + 2) <- slot_for_fv env v) fv; + Array.iteri (fun i v -> a.(i + 2) <- slot_for_fv env sigma v) fv; a in eval_tcode tc (get_atom_rel ()) (vm_global global_data.glob_val) vm_env -and val_of_constr env c = - match compile ~fail_on_error:true env c with - | Some v -> eval_to_patch env (to_memory v) +and val_of_constr env sigma c = + match compile ~fail_on_error:true env sigma c with + | Some v -> eval_to_patch env sigma (to_memory v) | None -> assert false let set_transparent_const _kn = () (* !?! *) diff --git a/kernel/vmsymtable.mli b/kernel/vmsymtable.mli index e480bfcec1..c6dc09d944 100644 --- a/kernel/vmsymtable.mli +++ b/kernel/vmsymtable.mli @@ -14,7 +14,7 @@ open Names open Constr open Environ -val val_of_constr : env -> constr -> Vmvalues.values +val val_of_constr : env -> (existential -> constr option) -> constr -> Vmvalues.values val set_opaque_const : Constant.t -> unit val set_transparent_const : Constant.t -> unit diff --git a/pretyping/coercionops.ml b/pretyping/coercionops.ml index ac89dfd747..274dbfd7ed 100644 --- a/pretyping/coercionops.ml +++ b/pretyping/coercionops.ml @@ -34,6 +34,31 @@ type cl_info_typ = { cl_param : int } +let cl_typ_ord t1 t2 = match t1, t2 with + | CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2 + | CL_CONST c1, CL_CONST c2 -> Constant.CanOrd.compare c1 c2 + | CL_PROJ c1, CL_PROJ c2 -> Projection.Repr.CanOrd.compare c1 c2 + | CL_IND i1, CL_IND i2 -> Ind.CanOrd.compare i1 i2 + | _ -> pervasives_compare t1 t2 (** OK *) + +let cl_typ_eq t1 t2 = Int.equal (cl_typ_ord t1 t2) 0 + +module ClTyp = struct + type t = cl_typ + let compare = cl_typ_ord +end + +module ClPairOrd = +struct + type t = cl_typ * cl_typ + let compare (i1, j1) (i2, j2) = + let c = cl_typ_ord i1 i2 in + if Int.equal c 0 then cl_typ_ord j1 j2 else c +end + +module ClTypMap = Map.Make(ClTyp) +module ClPairMap = Map.Make(ClPairOrd) + type coe_typ = GlobRef.t module CoeTypMap = GlobRef.Map_env @@ -43,6 +68,8 @@ type coe_info_typ = { coe_local : bool; coe_is_identity : bool; coe_is_projection : Projection.Repr.t option; + coe_source : cl_typ; + coe_target : cl_typ; coe_param : int; } @@ -53,88 +80,26 @@ let coe_info_typ_equal c1 c2 = c1.coe_is_projection == c2.coe_is_projection && Int.equal c1.coe_param c2.coe_param -let cl_typ_ord t1 t2 = match t1, t2 with - | CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2 - | CL_CONST c1, CL_CONST c2 -> Constant.CanOrd.compare c1 c2 - | CL_PROJ c1, CL_PROJ c2 -> Projection.Repr.CanOrd.compare c1 c2 - | CL_IND i1, CL_IND i2 -> Ind.CanOrd.compare i1 i2 - | _ -> pervasives_compare t1 t2 (** OK *) - -module ClTyp = struct - type t = cl_typ - let compare = cl_typ_ord -end - -module ClTypMap = Map.Make(ClTyp) - -let cl_typ_eq t1 t2 = Int.equal (cl_typ_ord t1 t2) 0 - type inheritance_path = coe_info_typ list -(* table des classes, des coercions et graphe d'heritage *) - -module Bijint : -sig - module Index : - sig - type t - val compare : t -> t -> int - val equal : t -> t -> bool - val print : t -> Pp.t - end - type 'a t - val empty : 'a t - val mem : cl_typ -> 'a t -> bool - val map : Index.t -> 'a t -> cl_typ * 'a - val revmap : cl_typ -> 'a t -> Index.t * 'a - val add : cl_typ -> 'a -> 'a t -> 'a t - val dom : 'a t -> cl_typ list -end -= -struct - - module Index = struct include Int let print = Pp.int end - - type 'a t = { v : (cl_typ * 'a) Int.Map.t; s : int; inv : int ClTypMap.t } - let empty = { v = Int.Map.empty; s = 0; inv = ClTypMap.empty } - let mem y b = ClTypMap.mem y b.inv - let map x b = Int.Map.find x b.v - let revmap y b = let n = ClTypMap.find y b.inv in (n, snd (Int.Map.find n b.v)) - let add x y b = - { v = Int.Map.add b.s (x,y) b.v; s = b.s+1; inv = ClTypMap.add x b.s b.inv } - let dom b = List.rev (ClTypMap.fold (fun x _ acc -> x::acc) b.inv []) -end - -type cl_index = Bijint.Index.t - let init_class_tab = - let open Bijint in + let open ClTypMap in add CL_FUN { cl_param = 0 } (add CL_SORT { cl_param = 0 } empty) let class_tab = - Summary.ref ~name:"class_tab" (init_class_tab : cl_info_typ Bijint.t) + Summary.ref ~name:"class_tab" (init_class_tab : cl_info_typ ClTypMap.t) let coercion_tab = Summary.ref ~name:"coercion_tab" (CoeTypMap.empty : coe_info_typ CoeTypMap.t) -module ClPairOrd = -struct - type t = cl_index * cl_index - let compare (i1, j1) (i2, j2) = - let c = Bijint.Index.compare i1 i2 in - if Int.equal c 0 then Bijint.Index.compare j1 j2 else c -end - -module ClPairMap = Map.Make(ClPairOrd) - let inheritance_graph = Summary.ref ~name:"inheritance_graph" (ClPairMap.empty : inheritance_path ClPairMap.t) (* ajout de nouveaux "objets" *) let add_new_class cl s = - if not (Bijint.mem cl !class_tab) then - class_tab := Bijint.add cl s !class_tab + if not (ClTypMap.mem cl !class_tab) then + class_tab := ClTypMap.add cl s !class_tab let add_new_coercion coe s = coercion_tab := CoeTypMap.add coe s !coercion_tab @@ -144,17 +109,9 @@ let add_new_path x y = (* class_info : cl_typ -> int * cl_info_typ *) -let class_info cl = Bijint.revmap cl !class_tab - -let class_exists cl = Bijint.mem cl !class_tab - -(* class_info_from_index : int -> cl_typ * cl_info_typ *) +let class_info cl = ClTypMap.find cl !class_tab -let class_info_from_index i = Bijint.map i !class_tab - -let cl_fun_index = fst(class_info CL_FUN) - -let cl_sort_index = fst(class_info CL_SORT) +let class_exists cl = ClTypMap.mem cl !class_tab let coercion_info coe = CoeTypMap.find coe !coercion_tab @@ -200,20 +157,18 @@ let subst_coe_typ subst t = subst_global_reference subst t (* class_of : Term.constr -> int *) let class_of env sigma t = - let (t, n1, i, u, args) = + let (t, n1, cl, u, args) = try let (cl, u, args) = find_class_type env sigma t in - let (i, { cl_param = n1 } ) = class_info cl in - (t, n1, i, u, args) + let { cl_param = n1 } = class_info cl in + (t, n1, cl, u, args) with Not_found -> let t = Tacred.hnf_constr env sigma t in let (cl, u, args) = find_class_type env sigma t in - let (i, { cl_param = n1 } ) = class_info cl in - (t, n1, i, u, args) + let { cl_param = n1 } = class_info cl in + (t, n1, cl, u, args) in - if Int.equal (List.length args) n1 then t, i else raise Not_found - -let inductive_class_of ind = fst (class_info (CL_IND ind)) + if Int.equal (List.length args) n1 then t, cl else raise Not_found let class_args_of env sigma c = pi3 (find_class_type env sigma c) @@ -238,26 +193,26 @@ let lookup_path_between_class (s,t) = ClPairMap.find (s,t) !inheritance_graph let lookup_path_to_fun_from_class s = - lookup_path_between_class (s,cl_fun_index) + lookup_path_between_class (s, CL_FUN) let lookup_path_to_sort_from_class s = - lookup_path_between_class (s,cl_sort_index) + lookup_path_between_class (s, CL_SORT) (* advanced path lookup *) let apply_on_class_of env sigma t cont = try let (cl,u,args) = find_class_type env sigma t in - let (i, { cl_param = n1 } ) = class_info cl in + let { cl_param = n1 } = class_info cl in if not (Int.equal (List.length args) n1) then raise Not_found; - t, cont i + t, cont cl with Not_found -> (* Is it worth to be more incremental on the delta steps? *) let t = Tacred.hnf_constr env sigma t in let (cl, u, args) = find_class_type env sigma t in - let (i, { cl_param = n1 } ) = class_info cl in + let { cl_param = n1 } = class_info cl in if not (Int.equal (List.length args) n1) then raise Not_found; - t, cont i + t, cont cl let lookup_path_between env sigma (s,t) = let (s,(t,p)) = @@ -287,25 +242,25 @@ let get_coercion_constructor env coe = | _ -> raise Not_found let lookup_pattern_path_between env (s,t) = - let i = inductive_class_of s in - let j = inductive_class_of t in - List.map (get_coercion_constructor env) (ClPairMap.find (i,j) !inheritance_graph) + List.map (get_coercion_constructor env) + (ClPairMap.find (CL_IND s, CL_IND t) !inheritance_graph) (* rajouter une coercion dans le graphe *) -let path_printer : ((cl_index * cl_index) * inheritance_path -> Pp.t) ref = +let path_printer : ((cl_typ * cl_typ) * inheritance_path -> Pp.t) ref = ref (fun _ -> str "<a class path>") let install_path_printer f = path_printer := f let print_path x = !path_printer x -let path_comparator : (Environ.env -> Evd.evar_map -> cl_index -> inheritance_path -> inheritance_path -> bool) ref = +let path_comparator : + (Environ.env -> Evd.evar_map -> cl_typ -> inheritance_path -> inheritance_path -> bool) ref = ref (fun _ _ _ _ _ -> false) let install_path_comparator f = path_comparator := f -let compare_path p q = !path_comparator p q +let compare_path env sigma cl p q = !path_comparator env sigma cl p q let warn_ambiguous_path = CWarnings.create ~name:"ambiguous-paths" ~category:"typechecker" @@ -316,29 +271,29 @@ let warn_ambiguous_path = else str" is ambiguous with existing " ++ print_path (c, q) ++ str".") l) -(* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit +(* add_coercion_in_graph : coe_index * cl_typ * cl_typ -> unit coercion,source,target *) -let different_class_params env i = - let ci = class_info_from_index i in - if (snd ci).cl_param > 0 then true - else - match fst ci with - | CL_IND i -> Environ.is_polymorphic env (GlobRef.IndRef i) - | CL_CONST c -> Environ.is_polymorphic env (GlobRef.ConstRef c) - | _ -> false +let different_class_params env ci = + if (class_info ci).cl_param > 0 then true + else + match ci with + | CL_IND i -> Environ.is_polymorphic env (GlobRef.IndRef i) + | CL_CONST c -> Environ.is_polymorphic env (GlobRef.ConstRef c) + | _ -> false -let add_coercion_in_graph env sigma (ic,source,target) = +let add_coercion_in_graph env sigma ic = let old_inheritance_graph = !inheritance_graph in - let ambig_paths = - (ref [] : ((cl_index * cl_index) * inheritance_path * inheritance_path) list ref) in + let ambig_paths : + ((cl_typ * cl_typ) * inheritance_path * inheritance_path) list ref = + ref [] in let try_add_new_path (i,j as ij) p = (* If p is a cycle, we check whether p is definitionally an identity function or not. If it is not, we report p as an ambiguous inheritance path. *) - if Bijint.Index.equal i j && not (compare_path env sigma i p []) then + if cl_typ_eq i j && not (compare_path env sigma i p []) then ambig_paths := (ij,p,[])::!ambig_paths; - if not (Bijint.Index.equal i j) || different_class_params env i then + if not (cl_typ_eq i j) || different_class_params env i then match lookup_path_between_class ij with | q -> (* p has the same source and target classes as an existing path q. We @@ -359,45 +314,36 @@ let add_coercion_in_graph env sigma (ic,source,target) = let try_add_new_path1 ij p = let _ = try_add_new_path ij p in () in - if try_add_new_path (source,target) [ic] then begin + if try_add_new_path (ic.coe_source, ic.coe_target) [ic] then begin ClPairMap.iter (fun (s,t) p -> - if not (Bijint.Index.equal s t) then begin - if Bijint.Index.equal t source then begin - try_add_new_path1 (s,target) (p@[ic]); + if not (cl_typ_eq s t) then begin + if cl_typ_eq t ic.coe_source then begin + try_add_new_path1 (s, ic.coe_target) (p@[ic]); ClPairMap.iter (fun (u,v) q -> - if not (Bijint.Index.equal u v) && Bijint.Index.equal u target then + if not (cl_typ_eq u v) && cl_typ_eq u ic.coe_target then try_add_new_path1 (s,v) (p@[ic]@q)) old_inheritance_graph end; - if Bijint.Index.equal s target then try_add_new_path1 (source,t) (ic::p) + if cl_typ_eq s ic.coe_target then + try_add_new_path1 (ic.coe_source, t) (ic::p) end) old_inheritance_graph end; match !ambig_paths with [] -> () | _ -> warn_ambiguous_path !ambig_paths -type coercion = { - coercion_type : coe_typ; - coercion_local : bool; - coercion_is_id : bool; - coercion_is_proj : Projection.Repr.t option; - coercion_source : cl_typ; - coercion_target : cl_typ; - coercion_params : int; -} - let subst_coercion subst c = let env = Global.env () in - let coe = subst_coe_typ subst c.coercion_type in - let cls = subst_cl_typ env subst c.coercion_source in - let clt = subst_cl_typ env subst c.coercion_target in - let clp = Option.Smart.map (subst_proj_repr subst) c.coercion_is_proj in - if c.coercion_type == coe && c.coercion_source == cls && - c.coercion_target == clt && c.coercion_is_proj == clp + let coe = subst_coe_typ subst c.coe_value in + let cls = subst_cl_typ env subst c.coe_source in + let clt = subst_cl_typ env subst c.coe_target in + let clp = Option.Smart.map (subst_proj_repr subst) c.coe_is_projection in + if c.coe_value == coe && c.coe_source == cls && c.coe_target == clt && + c.coe_is_projection == clp then c - else { c with coercion_type = coe; coercion_source = cls; - coercion_target = clt; coercion_is_proj = clp; } + else { c with coe_value = coe; coe_source = cls; coe_target = clt; + coe_is_projection = clp; } (* Computation of the class arity *) @@ -422,24 +368,14 @@ let add_class env sigma cl = add_new_class cl { cl_param = class_params env sigma cl } let declare_coercion env sigma c = - let () = add_class env sigma c.coercion_source in - let () = add_class env sigma c.coercion_target in - let is, _ = class_info c.coercion_source in - let it, _ = class_info c.coercion_target in - let xf = - { coe_value = c.coercion_type; - coe_local = c.coercion_local; - coe_is_identity = c.coercion_is_id; - coe_is_projection = c.coercion_is_proj; - coe_param = c.coercion_params; - } in - let () = add_new_coercion c.coercion_type xf in - add_coercion_in_graph env sigma (xf,is,it) + let () = add_class env sigma c.coe_source in + let () = add_class env sigma c.coe_target in + let () = add_new_coercion c.coe_value c in + add_coercion_in_graph env sigma c (* For printing purpose *) -let pr_cl_index = Bijint.Index.print - -let classes () = Bijint.dom !class_tab +let classes () = + List.rev (ClTypMap.fold (fun x _ acc -> x :: acc) !class_tab []) let coercions () = List.rev (CoeTypMap.fold (fun _ y acc -> y::acc) !coercion_tab []) diff --git a/pretyping/coercionops.mli b/pretyping/coercionops.mli index 073500b155..fb5621dd3a 100644 --- a/pretyping/coercionops.mli +++ b/pretyping/coercionops.mli @@ -44,12 +44,11 @@ type coe_info_typ = { coe_local : bool; coe_is_identity : bool; coe_is_projection : Projection.Repr.t option; + coe_source : cl_typ; + coe_target : cl_typ; coe_param : int; } -(** [cl_index] is the type of class keys *) -type cl_index - (** This is the type of paths from a class to another *) type inheritance_path = coe_info_typ list @@ -57,37 +56,21 @@ type inheritance_path = coe_info_typ list val class_exists : cl_typ -> bool -val class_info : cl_typ -> (cl_index * cl_info_typ) (** @raise Not_found if this type is not a class *) - -val class_info_from_index : cl_index -> cl_typ * cl_info_typ +val class_info : cl_typ -> cl_info_typ (** [find_class_type env sigma c] returns the head reference of [c], its universe instance and its arguments *) val find_class_type : env -> evar_map -> types -> cl_typ * EInstance.t * constr list (** raises [Not_found] if not convertible to a class *) -val class_of : env -> evar_map -> types -> types * cl_index - -(** raises [Not_found] if not mapped to a class *) -val inductive_class_of : inductive -> cl_index +val class_of : env -> evar_map -> types -> types * cl_typ val class_args_of : env -> evar_map -> types -> constr list -(** {6 [declare_coercion] adds a coercion in the graph of coercion paths } *) -type coercion = { - coercion_type : coe_typ; - coercion_local : bool; - coercion_is_id : bool; - coercion_is_proj : Projection.Repr.t option; - coercion_source : cl_typ; - coercion_target : cl_typ; - coercion_params : int; -} - -val subst_coercion : substitution -> coercion -> coercion +val subst_coercion : substitution -> coe_info_typ -> coe_info_typ -val declare_coercion : env -> evar_map -> coercion -> unit +val declare_coercion : env -> evar_map -> coe_info_typ -> unit (** {6 Access to coercions infos } *) val coercion_exists : coe_typ -> bool @@ -98,7 +81,7 @@ val coercion_info : coe_typ -> coe_info_typ (** @raise Not_found in the following functions when no path exists *) -val lookup_path_between_class : cl_index * cl_index -> inheritance_path +val lookup_path_between_class : cl_typ * cl_typ -> inheritance_path val lookup_path_between : env -> evar_map -> types * types -> types * types * inheritance_path val lookup_path_to_fun_from : env -> evar_map -> types -> @@ -111,16 +94,15 @@ val lookup_pattern_path_between : (**/**) (* Crade *) val install_path_printer : - ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit + ((cl_typ * cl_typ) * inheritance_path -> Pp.t) -> unit val install_path_comparator : - (env -> evar_map -> cl_index -> inheritance_path -> inheritance_path -> bool) -> unit + (env -> evar_map -> cl_typ -> inheritance_path -> inheritance_path -> bool) -> unit (**/**) (** {6 This is for printing purpose } *) val string_of_class : cl_typ -> string val pr_class : cl_typ -> Pp.t -val pr_cl_index : cl_index -> Pp.t -val inheritance_graph : unit -> ((cl_index * cl_index) * inheritance_path) list +val inheritance_graph : unit -> ((cl_typ * cl_typ) * inheritance_path) list val classes : unit -> cl_typ list val coercions : unit -> coe_info_typ list diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 2c107502f4..b19dbd46be 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -135,8 +135,9 @@ let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs = let construct_of_constr const env sigma tag typ = - let t, l = app_type env typ in - match EConstr.kind_upto sigma t with + let typ = Reductionops.clos_whd_flags CClosure.all env sigma (EConstr.of_constr typ) in + let t, l = decompose_appvect (EConstr.Unsafe.to_constr typ) in + match Constr.kind t with | Ind (ind,u) -> construct_of_constr_notnative const env tag ind u l | _ -> diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index e86a8a28c9..3ccc6ea125 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1398,7 +1398,7 @@ let understand_ltac flags env sigma lvar kind c = let (sigma, c, _) = ise_pretype_gen flags env sigma lvar kind c in (sigma, c) -let path_convertible env sigma i p q = +let path_convertible env sigma cl p q = let open Coercionops in let mkGRef ref = DAst.make @@ Glob_term.GRef(ref,None) in let mkGVar id = DAst.make @@ Glob_term.GVar(id) in @@ -1423,7 +1423,7 @@ let path_convertible env sigma i p q = p' | [] -> (* identity function for the class [i]. *) - let cl,params = class_info_from_index i in + let params = (class_info cl).cl_param in let clty = match cl with | CL_SORT -> mkGSort (Glob_term.UAnonymous {rigid=false}) @@ -1434,8 +1434,7 @@ let path_convertible env sigma i p q = | CL_PROJ p -> mkGRef (GlobRef.ConstRef (Projection.Repr.constant p)) in let names = - List.init params.cl_param - (fun n -> Id.of_string ("x" ^ string_of_int n)) + List.init params (fun n -> Id.of_string ("x" ^ string_of_int n)) in List.fold_right (fun id t -> mkGLambda (Name id, mkGHole (), t)) names @@ diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index cf6d581066..9939764069 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -78,8 +78,9 @@ let type_constructor mind mib u (ctx, typ) params = -let construct_of_constr const env tag typ = - let (t, allargs) = decompose_appvect (whd_all env typ) in +let construct_of_constr const env sigma tag typ = + let typ = Reductionops.clos_whd_flags CClosure.all env sigma (EConstr.of_constr typ) in + let t, allargs = decompose_appvect (EConstr.Unsafe.to_constr typ) in match Constr.kind t with | Ind ((mind,_ as ind), u as indu) -> let mib,mip = lookup_mind_specif env ind in @@ -92,8 +93,8 @@ let construct_of_constr const env tag typ = assert (Constr.equal t (Typeops.type_of_int env)); (mkInt (Uint63.of_int tag), t) -let construct_of_constr_const env tag typ = - fst (construct_of_constr true env tag typ) +let construct_of_constr_const env sigma tag typ = + fst (construct_of_constr true env sigma tag typ) let construct_of_constr_block = construct_of_constr false @@ -156,7 +157,7 @@ and nf_whd env sigma whd typ = let _, args = nf_args env sigma vargs t in mkApp(cfd,args) | Vconstr_const n -> - construct_of_constr_const env n typ + construct_of_constr_const env sigma n typ | Vconstr_block b -> let tag = btag b in let (tag,ofs) = @@ -165,7 +166,7 @@ and nf_whd env sigma whd typ = | Vconstr_const tag -> (tag+Obj.last_non_constant_constructor_tag, 1) | _ -> assert false else (tag, 0) in - let capp,ctyp = construct_of_constr_block env tag typ in + let capp,ctyp = construct_of_constr_block env sigma tag typ in let args = nf_bargs env sigma b ofs ctyp in mkApp(capp,args) | Vint64 i -> i |> Uint63.of_int64 |> mkInt @@ -414,9 +415,9 @@ let cbv_vm env sigma c t = if Termops.occur_meta sigma c then CErrors.user_err Pp.(str "vm_compute does not support metas."); (* This evar-normalizes terms beforehand *) - let c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in - let t = EConstr.to_constr ~abort_on_undefined_evars:false sigma t in - let v = Vmsymtable.val_of_constr env c in + let c = EConstr.Unsafe.to_constr c in + let t = EConstr.Unsafe.to_constr t in + let v = Vmsymtable.val_of_constr env (Evd.existential_opt_value0 sigma) c in EConstr.of_constr (nf_val env sigma v t) let vm_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 = diff --git a/sysinit/usage.ml b/sysinit/usage.ml index d00b916f23..5886b1c5b5 100644 --- a/sysinit/usage.ml +++ b/sysinit/usage.ml @@ -73,8 +73,6 @@ let print_usage_common co command = \n -debug debug mode (implies -bt)\ \n -xml-debug debug mode and print XML messages to/from coqide\ \n -diffs (on|off|removed) highlight differences between proof steps\ -\n -noglob do not dump globalizations\ -\n -dump-glob f dump globalizations in file f (to be used by coqdoc)\ \n -impredicative-set set sort Set impredicative\ \n -allow-sprop allow using the proof irrelevant SProp sort\ \n -disallow-sprop forbid using the proof irrelevant SProp sort\ diff --git a/tactics/tactics.ml b/tactics/tactics.ml index cbf12ac22f..67bf8d0d29 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2796,7 +2796,24 @@ let generalize_goal_gen env sigma ids i ((occs,c,b),na) t cl = let open Context.Rel.Declaration in let decls,cl = decompose_prod_n_assum sigma i cl in let dummy_prod = it_mkProd_or_LetIn mkProp decls in - let newdecls,_ = decompose_prod_n_assum sigma i (subst_term_gen sigma EConstr.eq_constr_nounivs c dummy_prod) in + let newdecls,_ = + let c = Termops.collapse_appl sigma c in + let arity = Array.length (snd (Termops.decompose_app_vect sigma c)) in + let cache = ref Int.Map.empty in + let eq sigma k t = + let c = + try Int.Map.find k !cache + with Not_found -> + let c = EConstr.Vars.lift k c in + let () = cache := Int.Map.add k c !cache in + c + in + (* We use a nounivs equality because generalize morally takes a pattern as + argument, so we have to ignore freshly generated sorts. *) + EConstr.eq_constr_nounivs sigma c t + in + decompose_prod_n_assum sigma i (replace_term_gen sigma eq arity (mkRel 1) dummy_prod) + in let cl',sigma' = subst_closed_term_occ env sigma (AtOccs occs) c (it_mkProd_or_LetIn cl newdecls) in let na = generalized_name env sigma c t ids cl' na in let r = Retyping.relevance_of_type env sigma t in diff --git a/test-suite/bugs/closed/bug_13841.v b/test-suite/bugs/closed/bug_13841.v new file mode 100644 index 0000000000..60fca8b49c --- /dev/null +++ b/test-suite/bugs/closed/bug_13841.v @@ -0,0 +1,11 @@ +Goal True. +evar (p : bool). +unify ?p true. +let v := eval vm_compute in (orb p false) in +match v with true => idtac end. +assert (orb p false = true). +vm_compute. +match goal with |- true = _ => idtac end. +easy. +easy. +Qed. diff --git a/test-suite/bugs/closed/bug_13896.v b/test-suite/bugs/closed/bug_13896.v new file mode 100644 index 0000000000..10f24d8564 --- /dev/null +++ b/test-suite/bugs/closed/bug_13896.v @@ -0,0 +1,24 @@ +Inductive type : Set := + Tptr : type -> type + | Tref : type -> type + | Trv_ref : type -> type + | Tint : type -> type -> type + | Tvoid : type + | Tarray : type -> type -> type + | Tnamed : type -> type + | Tfunction : type -> type -> type -> type + | Tbool : type + | Tmember_pointer : type -> type -> type + | Tfloat : type -> type + | Tqualified : type -> type -> type + | Tnullptr : type + | Tarch : type -> type -> type +. +Definition type_eq_dec : forall (ty1 ty2 : type), { ty1 = ty2 } + { ty1 <> ty2 }. +Proof. fix IHty1 1. decide equality. Defined. + +Goal (if type_eq_dec (Tptr Tvoid) (Tptr Tvoid) then True else False). +Proof. +timeout 1 cbn. +constructor. +Qed. diff --git a/test-suite/bugs/closed/bug_7631.v b/test-suite/bugs/closed/bug_7631.v index 93aeb83e28..14ab4de9b7 100644 --- a/test-suite/bugs/closed/bug_7631.v +++ b/test-suite/bugs/closed/bug_7631.v @@ -21,3 +21,9 @@ Definition bar (x := foo) := Eval native_compute in x. Definition barvm (x := foo) := Eval vm_compute in x. End RelContext. + +Definition bar (t:=_) (x := true : t) := Eval native_compute in x. +Definition barvm (t:=_) (x := true : t) := Eval vm_compute in x. + +Definition baz (z:nat) (t:=_ z) (x := true : t) := Eval native_compute in x. +Definition bazvm (z:nat) (t:=_ z) (x := true : t) := Eval vm_compute in x. diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 60213cab0c..cc9e745f6b 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -6,7 +6,7 @@ : nat * nat * (nat * nat) (0, 2, (2, 2)) : nat * nat * (nat * nat) -pair (pair O (S (S O))) (pair (S (S O)) O) +pair (pair 0 2) (pair 2 0) : prod (prod nat nat) (prod nat nat) << 0, 2, 4 >> : nat * nat * nat * (nat * (nat * nat)) @@ -16,8 +16,7 @@ pair (pair O (S (S O))) (pair (S (S O)) O) : nat * nat * nat * (nat * (nat * nat)) (0, 2, 4, (0, (2, 4))) : nat * nat * nat * (nat * (nat * nat)) -pair (pair (pair O (S (S O))) (S (S (S (S O))))) - (pair (S (S (S (S O)))) (pair (S (S O)) O)) +pair (pair (pair 0 2) 4) (pair 4 (pair 2 0)) : prod (prod (prod nat nat) nat) (prod nat (prod nat nat)) ETA x y : nat, Nat.add : nat -> nat -> nat @@ -174,9 +173,8 @@ forall_non_null x y z t : nat , x = y /\ z = t : nat * (nat * nat) * (nat * nat * nat) * (nat * (nat * nat)) * (nat * nat * nat) pair - (pair - (pair (pair (S (S O)) (pair (S O) O)) (pair (pair O (S (S O))) (S O))) - (pair (S O) (pair (S (S O)) O))) (pair (pair O (S O)) (S (S O))) + (pair (pair (pair 2 (pair 1 0)) (pair (pair 0 2) 1)) (pair 1 (pair 2 0))) + (pair (pair 0 1) 2) : prod (prod (prod (prod nat (prod nat nat)) (prod (prod nat nat) nat)) (prod nat (prod nat nat))) (prod (prod nat nat) nat) diff --git a/test-suite/output/primitive_tokens.out b/test-suite/output/primitive_tokens.out new file mode 100644 index 0000000000..afe9b25442 --- /dev/null +++ b/test-suite/output/primitive_tokens.out @@ -0,0 +1,61 @@ +"foo" + : string +1234 + : nat +Nat.add 1 2 + : nat +match "a" with +| "a" => true +| _ => false +end + : bool +match 1 with +| 1 => true +| _ => false +end + : bool +{| field := 7 |} + : test +String (Ascii.Ascii false true true false false true true false) + (String (Ascii.Ascii true true true true false true true false) + (String (Ascii.Ascii true true true true false true true false) + EmptyString)) + : string +S + (S + (S + (S + (S + (S + (S + (S + (S + (S + (S + (S + (S + (S + (S + (S + (S + (S + (S (S (S (S (S (S ...))))))))))))))))))))))) + : nat +Nat.add (S O) (S (S O)) + : nat +match + String (Ascii.Ascii true false false false false true true false) + EmptyString +with +| String (Ascii.Ascii true false false false false true true false) + EmptyString => true +| _ => false +end + : bool +match S O with +| S O => true +| _ => false +end + : bool +{| field := S (S (S (S (S (S (S O)))))) |} + : test diff --git a/test-suite/output/primitive_tokens.v b/test-suite/output/primitive_tokens.v new file mode 100644 index 0000000000..3207e5983f --- /dev/null +++ b/test-suite/output/primitive_tokens.v @@ -0,0 +1,23 @@ +Require Import String. + +Record test := { field : nat }. + +Open Scope string_scope. + +Unset Printing Notations. + +Check "foo". +Check 1234. +Check 1 + 2. +Check match "a" with "a" => true | _ => false end. +Check match 1 with 1 => true | _ => false end. +Check {| field := 7 |}. + +Set Printing Raw Literals. + +Check "foo". +Check 1234. +Check 1 + 2. +Check match "a" with "a" => true | _ => false end. +Check match 1 with 1 => true | _ => false end. +Check {| field := 7 |}. diff --git a/test-suite/output/relaxed_ambiguous_paths.out b/test-suite/output/relaxed_ambiguous_paths.out index ac5a09bad7..48368c7ede 100644 --- a/test-suite/output/relaxed_ambiguous_paths.out +++ b/test-suite/output/relaxed_ambiguous_paths.out @@ -3,32 +3,32 @@ Warning: New coercion path [ac; cd] : A >-> D is ambiguous with existing [ab; bd] : A >-> D. [ambiguous-paths,typechecker] [ab] : A >-> B -[ab; bd] : A >-> D [ac] : A >-> C +[ab; bd] : A >-> D [bd] : B >-> D [cd] : C >-> D File "stdin", line 26, characters 0-28: Warning: New coercion path [ab; bc] : A >-> C is ambiguous with existing [ac] : A >-> C. [ambiguous-paths,typechecker] +[ab] : A >-> B [ac] : A >-> C [ac; cd] : A >-> D -[ab] : A >-> B -[cd] : C >-> D [bc] : B >-> C [bc; cd] : B >-> D +[cd] : C >-> D [B_A] : B >-> A [C_A] : C >-> A -[D_B] : D >-> B [D_A] : D >-> A +[D_B] : D >-> B [D_C] : D >-> C [A'_A] : A' >-> A -[B_A'] : B >-> A' [B_A'; A'_A] : B >-> A -[C_A'] : C >-> A' +[B_A'] : B >-> A' [C_A'; A'_A] : C >-> A -[D_B; B_A'] : D >-> A' +[C_A'] : C >-> A' [D_A] : D >-> A +[D_B; B_A'] : D >-> A' [D_B] : D >-> B [D_C] : D >-> C File "stdin", line 121, characters 0-86: @@ -36,12 +36,12 @@ Warning: New coercion path [D_C; C_A'] : D >-> A' is ambiguous with existing [D_B; B_A'] : D >-> A'. [ambiguous-paths,typechecker] [A'_A] : A' >-> A -[B_A'] : B >-> A' [B_A'; A'_A] : B >-> A -[C_A'] : C >-> A' +[B_A'] : B >-> A' [C_A'; A'_A] : C >-> A -[D_B; B_A'] : D >-> A' +[C_A'] : C >-> A' [D_A] : D >-> A +[D_B; B_A'] : D >-> A' [D_B] : D >-> B [D_C] : D >-> C File "stdin", line 130, characters 0-47: diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index b7af66b2ee..b78bcce6db 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -26,6 +26,8 @@ let coqc_specific_usage = Usage.{ coqc specific options:\ \n -o f.vo use f.vo as the output file name\ \n -verbose compile and output the input file\ +\n -noglob do not dump globalizations\ +\n -dump-glob f dump globalizations in file f (to be used by coqdoc)\ \n -schedule-vio2vo j f1..fn run up to j instances of Coq to turn each fi.vio\ \n into fi.vo\ \n -schedule-vio-checking j f1..fn run up to j instances of Coq to check all\ diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml index 15d8ebc4b5..86b15739f9 100644 --- a/vernac/comCoercion.ml +++ b/vernac/comCoercion.ml @@ -237,24 +237,24 @@ let open_coercion i o = cache_coercion o let discharge_coercion (_, c) = - if c.coercion_local then None + if c.coe_local then None else let n = try - let ins = Lib.section_instance c.coercion_type in + let ins = Lib.section_instance c.coe_value in Array.length (snd ins) with Not_found -> 0 in let nc = { c with - coercion_params = n + c.coercion_params; - coercion_is_proj = Option.map Lib.discharge_proj_repr c.coercion_is_proj; + coe_param = n + c.coe_param; + coe_is_projection = Option.map Lib.discharge_proj_repr c.coe_is_projection; } in Some nc let classify_coercion obj = - if obj.coercion_local then Dispose else Substitute obj + if obj.coe_local then Dispose else Substitute obj -let inCoercion : coercion -> obj = +let inCoercion : coe_info_typ -> obj = declare_object {(default_object "COERCION") with open_function = simple_open open_coercion; cache_function = cache_coercion; @@ -269,13 +269,13 @@ let declare_coercion coef ?(local = false) ~isid ~src:cls ~target:clt ~params:ps | _ -> None in let c = { - coercion_type = coef; - coercion_local = local; - coercion_is_id = isid; - coercion_is_proj = isproj; - coercion_source = cls; - coercion_target = clt; - coercion_params = ps; + coe_value = coef; + coe_local = local; + coe_is_identity = isid; + coe_is_projection = isproj; + coe_source = cls; + coe_target = clt; + coe_param = ps; } in Lib.add_anonymous_leaf (inCoercion c) diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 79a0cdf8d1..ec6e3b44ba 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -976,15 +976,11 @@ open Coercionops let print_coercion_value v = Printer.pr_global v.coe_value -let print_class i = - let cl,_ = class_info_from_index i in - pr_class cl - let print_path ((i,j),p) = hov 2 ( str"[" ++ hov 0 (prlist_with_sep pr_semicolon print_coercion_value p) ++ str"] : ") ++ - print_class i ++ str" >-> " ++ print_class j + pr_class i ++ str" >-> " ++ pr_class j let _ = Coercionops.install_path_printer print_path @@ -997,25 +993,16 @@ let print_classes () = let print_coercions () = pr_sequence print_coercion_value (coercions()) -let index_of_class cl = - try - fst (class_info cl) - with Not_found -> - user_err ~hdr:"index_of_class" - (pr_class cl ++ spc() ++ str "not a defined class.") - let print_path_between cls clt = - let i = index_of_class cls in - let j = index_of_class clt in let p = try - lookup_path_between_class (i,j) + lookup_path_between_class (cls, clt) with Not_found -> user_err ~hdr:"index_cl_of_id" (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt ++ str ".") in - print_path ((i,j),p) + print_path ((cls, clt), p) let print_canonical_projections env sigma grefs = let match_proj_gref ((x,y),c) gr = diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 38ca836b32..e8d84a67a3 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1568,6 +1568,13 @@ let () = let () = declare_bool_option { optdepr = false; + optkey = ["Printing";"Raw";"Literals"]; + optread = (fun () -> !Constrextern.print_raw_literal); + optwrite = (fun b -> Constrextern.print_raw_literal := b) } + +let () = + declare_bool_option + { optdepr = false; optkey = ["Printing";"All"]; optread = (fun () -> !Flags.raw_print); optwrite = (fun b -> Flags.raw_print := b) } |