diff options
100 files changed, 2193 insertions, 1519 deletions
diff --git a/Makefile.build b/Makefile.build index eed3c2813a..526a8c5831 100644 --- a/Makefile.build +++ b/Makefile.build @@ -401,6 +401,12 @@ kernel/uint63.ml: kernel/uint63_$(OCAML_INT_SIZE).ml rm -f $@ && cp $< $@ && chmod a-w $@ ########################################################################### +# Specific rules for Float64 +########################################################################### +kernel/float64.ml: kernel/float64_$(OCAML_INT_SIZE).ml + rm -f $@ && cp $< $@ && chmod a-w $@ + +########################################################################### # Main targets (coqtop.opt, coqtop.byte) ########################################################################### diff --git a/Makefile.make b/Makefile.make index 51d6d1c3c1..34f5707ae8 100644 --- a/Makefile.make +++ b/Makefile.make @@ -107,7 +107,7 @@ GRAMMLIFILES := $(addsuffix .mli, $(GRAMFILES)) GENGRAMMLFILES := $(GRAMMLFILES) gramlib/.pack/gramlib.ml # why is gramlib.ml not in GRAMMLFILES? GENMLGFILES:= $(MLGFILES:.mlg=.ml) -GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) $(GENGRAMMLFILES) ide/coqide/coqide_os_specific.ml kernel/vmopcodes.ml kernel/uint63.ml +GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) $(GENGRAMMLFILES) ide/coqide/coqide_os_specific.ml kernel/vmopcodes.ml kernel/uint63.ml kernel/float64.ml GENMLIFILES:=$(GRAMMLIFILES) GENHFILES:=kernel/byterun/coq_instruct.h kernel/byterun/coq_jumptbl.h GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) kernel/genOpcodeFiles.exe diff --git a/dev/ci/user-overlays/13166-herbelin-master+fixes13165-missing-impargs-defined-fields.sh b/dev/ci/user-overlays/13166-herbelin-master+fixes13165-missing-impargs-defined-fields.sh new file mode 100644 index 0000000000..7d55cf6883 --- /dev/null +++ b/dev/ci/user-overlays/13166-herbelin-master+fixes13165-missing-impargs-defined-fields.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "13166" ] || [ "$CI_BRANCH" = "master+fixes13165-missing-impargs-defined-fields" ]; then + + elpi_CI_REF=coq-master+adapt-coq-pr13166-impargs-record-fields + elpi_CI_GITURL=https://github.com/herbelin/coq-elpi + +fi diff --git a/dev/doc/changes.md b/dev/doc/changes.md index fb5d7cc244..6a6318f97a 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1,22 +1,35 @@ ## Changes between Coq 8.12 and Coq 8.13 -- Tactic language: TacGeneric now takes an argument to tell if it - comes from a notation. Use `None` if not and `Some foo` to tell to - print such TacGeneric surrounded with `foo:( )`. - ### Code formatting - The automatic code formatting tool `ocamlformat` has been disabled and its git hook removed. If desired, automatic formatting can be achieved by calling the `fmt` target of the dune build system. -### Pp library +### ML API + +Abstract syntax of tactic: + +- TacGeneric now takes an argument to tell if it comes from a + notation. Use `None` if not and `Some foo` to tell to print such + TacGeneric surrounded with `foo:( )`. + +Printing functions: - `Pp.h` does not take a `int` argument anymore (the argument was not used). In general, where `h n` for `n` non zero was used, `hv n` was instead intended. If cancelling the breaking role of cuts in the box was intended, turn `h n c` into `h c`. +Grammar entries: + +- `Prim.pattern_identref` is deprecated, use `Prim.pattern_ident` + which now returns a located identifier. + +Generic arguments: + +- Generic arguments: `wit_var` is deprecated, use `wit_hyp`. + ## Changes between Coq 8.11 and Coq 8.12 ### Code formatting diff --git a/doc/changelog/02-specification-language/13166-master+fixes13165-missing-impargs-defined-fields.rst b/doc/changelog/02-specification-language/13166-master+fixes13165-missing-impargs-defined-fields.rst new file mode 100644 index 0000000000..006989e6b3 --- /dev/null +++ b/doc/changelog/02-specification-language/13166-master+fixes13165-missing-impargs-defined-fields.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Implicit arguments taken into account in defined fields of a record type declaration + (`#13166 <https://github.com/coq/coq/pull/13166>`_, + fixes `#13165 <https://github.com/coq/coq/issues/13165>`_, + by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/12648-zify-int63.rst b/doc/changelog/04-tactics/12648-zify-int63.rst new file mode 100644 index 0000000000..ec7a1273e4 --- /dev/null +++ b/doc/changelog/04-tactics/12648-zify-int63.rst @@ -0,0 +1,3 @@ +- **Added:** + The :tacn:`zify` tactic provides support for primitive integers (module :g:`ZifyInt63`). + (`#12648 <https://github.com/coq/coq/pull/12648>`_, by Frédéric Besson). diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index ba5bac6489..b3a33ffeea 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -283,14 +283,19 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. .. tacn:: zify :name: zify - This tactic is internally called by :tacn:`lia` to support additional types e.g., :g:`nat`, :g:`positive` and :g:`N`. - By requiring the module ``ZifyBool``, the boolean type :g:`bool` and some comparison operators are also supported. + This tactic is internally called by :tacn:`lia` to support additional types, e.g., :g:`nat`, :g:`positive` and :g:`N`. + Additional support is provided by the following modules: + + + For boolean operators (e.g., :g:`Nat.leb`), require the module :g:`ZifyBool`. + + For comparison operators (e.g., :g:`Z.compare`), require the module :g:`ZifyComparison`. + + For native 63 bit integers, require the module :g:`ZifyInt63`. + :tacn:`zify` can also be extended by rebinding the tactics `Zify.zify_pre_hook` and `Zify.zify_post_hook` that are respectively run in the first and the last steps of :tacn:`zify`. + To support :g:`Z.div` and :g:`Z.modulo`: ``Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations``. + To support :g:`Z.quot` and :g:`Z.rem`: ``Ltac Zify.zify_post_hook ::= Z.quot_rem_to_equations``. - + To support :g:`Z.div`, :g:`Z.modulo`, :g:`Z.quot`, and :g:`Z.rem`: ``Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations``. + + To support :g:`Z.div`, :g:`Z.modulo`, :g:`Z.quot` and :g:`Z.rem`: either ``Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations`` or ``Ltac Zify.zify_convert_to_euclidean_division_equations_flag ::= constr:(true)``. The :tacn:`zify` tactic can be extended with new types and operators by declaring and registering new typeclass instances using the following commands. The typeclass declarations can be found in the module ``ZifyClasses`` and the default instances can be found in the module ``ZifyInst``. diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index 4cdfba146a..39b154de8d 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -13,7 +13,7 @@ Inductive types .. prodn:: inductive_definition ::= {? > } @ident_decl {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations } constructors_or_record ::= {? %| } {+| @constructor } - | {? @ident } %{ {*; @record_field } %} + | {? @ident } %{ {*; @record_field } {? ; } %} constructor ::= @ident {* @binder } {? @of_type } This command defines one or more diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst index cd44d06e67..b2099b8636 100644 --- a/doc/sphinx/language/core/records.rst +++ b/doc/sphinx/language/core/records.rst @@ -18,12 +18,12 @@ expressions. In this sense, the :cmd:`Record` construction allows defining .. insertprodn record_definition field_def .. prodn:: - record_definition ::= {? > } @ident_decl {* @binder } {? : @type } {? @ident } %{ {*; @record_field } %} {? @decl_notations } + record_definition ::= {? > } @ident_decl {* @binder } {? : @type } {? @ident } %{ {*; @record_field } {? ; } %} {? @decl_notations } record_field ::= {* #[ {*, @attribute } ] } @name {? @field_body } {? %| @natural } {? @decl_notations } field_body ::= {* @binder } @of_type | {* @binder } @of_type := @term | {* @binder } := @term - term_record ::= %{%| {* @field_def } %|%} + term_record ::= %{%| {*; @field_def } {? ; } %|%} field_def ::= @qualid {* @binder } := @term diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index f722ddda79..edd93f2266 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -878,6 +878,11 @@ Controlling the effect of proof editing commands proved before starting the previous proof) and Coq will switch back to the proof of the previous assertion. +.. flag:: Printing Goal Names + + When turned on, the name of the goal is printed in interactive + proof mode, which can be useful in cases of cross references + between goals. Controlling memory usage ------------------------ diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index f39c50238a..4d2972ef8f 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -50,6 +50,7 @@ theories/micromega/ZCoeff.v theories/micromega/ZMicromega.v theories/micromega/ZifyInst.v theories/micromega/ZifyBool.v +theories/micromega/ZifyInt63.v theories/micromega/ZifyComparison.v theories/micromega/ZifyClasses.v theories/micromega/ZifyPow.v diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index a9f9c805d8..1e9be8dded 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -396,8 +396,8 @@ operconstr0: [ (* @Zimmi48: This rule is a hack, according to Hugo, and should not be shown in the manual. *) | DELETE "{" binder_constr "}" | REPLACE "{|" record_declaration bar_cbrace -| WITH "{|" LIST0 field_def bar_cbrace -| MOVETO term_record "{|" LIST0 field_def bar_cbrace +| WITH "{|" LIST0 field_def SEP ";" OPT ";" bar_cbrace +| MOVETO term_record "{|" LIST0 field_def SEP ";" OPT ";" bar_cbrace | MOVETO term_generalizing "`{" operconstr200 "}" | MOVETO term_generalizing "`(" operconstr200 ")" | MOVETO term_ltac "ltac" ":" "(" tactic_expr5 ")" @@ -585,7 +585,7 @@ constructor_list_or_record_decl: [ record_fields: [ | REPLACE record_field ";" record_fields -| WITH LIST0 record_field SEP ";" +| WITH LIST0 record_field SEP ";" OPT ";" | DELETE record_field | DELETE (* empty *) ] diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 067050b4f5..73641976e3 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1740,11 +1740,11 @@ simple_tactic: [ | "zify_elim_let" (* micromega plugin *) | "nsatz_compute" constr (* nsatz plugin *) | "omega" (* omega plugin *) -| "rtauto" | "protect_fv" string "in" ident (* ring plugin *) | "protect_fv" string (* ring plugin *) | "ring_lookup" tactic0 "[" LIST0 constr "]" LIST1 constr (* ring plugin *) | "field_lookup" tactic "[" LIST0 constr "]" LIST1 constr (* ring plugin *) +| "rtauto" ] mlname: [ diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index cbef29fb39..61befe9f1f 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -539,7 +539,7 @@ variant_definition: [ ] record_definition: [ -| OPT ">" ident_decl LIST0 binder OPT [ ":" type ] OPT ident "{" LIST0 record_field SEP ";" "}" OPT decl_notations +| OPT ">" ident_decl LIST0 binder OPT [ ":" type ] OPT ident "{" LIST0 record_field SEP ";" OPT ";" "}" OPT decl_notations ] record_field: [ @@ -553,7 +553,7 @@ field_body: [ ] term_record: [ -| "{|" LIST0 field_def "|}" +| "{|" LIST0 field_def SEP ";" OPT ";" "|}" ] field_def: [ @@ -566,7 +566,7 @@ inductive_definition: [ constructors_or_record: [ | OPT "|" LIST1 constructor SEP "|" -| OPT ident "{" LIST0 record_field SEP ";" "}" +| OPT ident "{" LIST0 record_field SEP ";" OPT ";" "}" ] constructor: [ diff --git a/gramlib/.merlin.in b/gramlib/.merlin.in new file mode 100644 index 0000000000..cf828efdb7 --- /dev/null +++ b/gramlib/.merlin.in @@ -0,0 +1,3 @@ +FLG -open Gramlib + +REC diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index c98e05370e..d14d156ffc 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -108,7 +108,7 @@ and constr_expr_r = * constr_expr * constr_expr | CHole of Evar_kinds.t option * Namegen.intro_pattern_naming_expr * Genarg.raw_generic_argument option | CPatVar of Pattern.patvar - | CEvar of Glob_term.existential_name * (Id.t * constr_expr) list + | CEvar of Glob_term.existential_name CAst.t * (lident * constr_expr) list | CSort of Glob_term.glob_sort | CCast of constr_expr * constr_expr Glob_term.cast_type | CNotation of notation_with_optional_scope option * notation * constr_notation_substitution diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index ce8e7d3c2c..7075d082ee 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -156,7 +156,7 @@ let rec constr_expr_eq e1 e2 = | CPatVar i1, CPatVar i2 -> Id.equal i1 i2 | CEvar (id1, c1), CEvar (id2, c2) -> - Id.equal id1 id2 && List.equal instance_eq c1 c2 + Id.equal id1.CAst.v id2.CAst.v && List.equal instance_eq c1 c2 | CSort s1, CSort s2 -> Glob_ops.glob_sort_eq s1 s2 | CCast(t1,c1), CCast(t2,c2) -> @@ -235,7 +235,7 @@ and constr_notation_substitution_eq (e1, el1, b1, bl1) (e2, el2, b2, bl2) = List.equal (List.equal local_binder_eq) bl1 bl2 and instance_eq (x1,c1) (x2,c2) = - Id.equal x1 x2 && constr_expr_eq c1 c2 + Id.equal x1.CAst.v x2.CAst.v && constr_expr_eq c1 c2 and cast_expr_eq c1 c2 = match c1, c2 with | CastConv t1, CastConv t2 diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 167ea3ecdf..7bf1c58148 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -978,7 +978,7 @@ let rec extern inctx ?impargs scopes vars r = if !print_meta_as_hole then CHole (None, IntroAnonymous, None) else (match kind with | Evar_kinds.SecondOrderPatVar n -> CPatVar n - | Evar_kinds.FirstOrderPatVar n -> CEvar (n,[])) + | Evar_kinds.FirstOrderPatVar n -> CEvar (CAst.make n,[])) | GApp (f,args) -> (match DAst.get f with @@ -1103,7 +1103,7 @@ let rec extern inctx ?impargs scopes vars r = | GFloat f -> extern_float f (snd scopes) | GArray(u,t,def,ty) -> - CArray(u,Array.map (extern inctx scopes vars) t, extern inctx scopes vars def, extern_typ scopes vars ty) + CArray(extern_universes u,Array.map (extern inctx scopes vars) t, extern inctx scopes vars def, extern_typ scopes vars ty) in insert_entry_coercion coercion (CAst.make ?loc c) @@ -1391,7 +1391,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with | None -> Id.of_string "__" | Some id -> id in - GEvar (id,List.map (on_snd (glob_of_pat avoid env sigma)) l) + GEvar (CAst.make id,List.map (fun (id,c) -> (CAst.make id, glob_of_pat avoid env sigma c)) l) | PRel n -> let id = try match lookup_name_of_rel n env with | Name id -> id diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 48fb4a4a5d..959b61a3d7 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2188,7 +2188,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = GPatVar (Evar_kinds.SecondOrderPatVar n) | CEvar (n, []) when pattern_mode -> DAst.make ?loc @@ - GPatVar (Evar_kinds.FirstOrderPatVar n) + GPatVar (Evar_kinds.FirstOrderPatVar n.CAst.v) (* end *) (* Parsing existential variables *) | CEvar (n, l) -> diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 343f85be03..70be55f843 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -40,8 +40,10 @@ let wit_int_or_var = let wit_ident = make0 "ident" -let wit_var = - make0 ~dyn:(val_tag (topwit wit_ident)) "var" +let wit_hyp = + make0 ~dyn:(val_tag (topwit wit_ident)) "hyp" + +let wit_var = wit_hyp let wit_ref = make0 "ref" diff --git a/interp/stdarg.mli b/interp/stdarg.mli index 3ae8b7d73f..bd34af5543 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -37,7 +37,10 @@ val wit_int_or_var : (int or_var, int or_var, int) genarg_type val wit_ident : Id.t uniform_genarg_type +val wit_hyp : (lident, lident, Id.t) genarg_type + val wit_var : (lident, lident, Id.t) genarg_type +[@@ocaml.deprecated "Use Stdarg.wit_hyp"] val wit_ref : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type diff --git a/kernel/dune b/kernel/dune index ce6fdc03df..bd663974da 100644 --- a/kernel/dune +++ b/kernel/dune @@ -3,7 +3,7 @@ (synopsis "The Coq Kernel") (public_name coq.kernel) (wrapped false) - (modules (:standard \ genOpcodeFiles uint63_31 uint63_63)) + (modules (:standard \ genOpcodeFiles uint63_31 uint63_63 float64_31 float64_63)) (libraries lib byterun dynlink)) (executable @@ -19,6 +19,11 @@ (deps (:gen-file uint63_%{ocaml-config:int_size}.ml)) (action (copy# %{gen-file} %{targets}))) +(rule + (targets float64.ml) + (deps (:gen-file float64_%{ocaml-config:int_size}.ml)) + (action (copy# %{gen-file} %{targets}))) + (documentation (package coq)) diff --git a/kernel/float64_31.ml b/kernel/float64_31.ml new file mode 100644 index 0000000000..09b28e6cf0 --- /dev/null +++ b/kernel/float64_31.ml @@ -0,0 +1,35 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +include Float64_common + +external mul : float -> float -> float = "coq_fmul_byte" "coq_fmul" +[@@unboxed] [@@noalloc] + +external add : float -> float -> float = "coq_fadd_byte" "coq_fadd" +[@@unboxed] [@@noalloc] + +external sub : float -> float -> float = "coq_fsub_byte" "coq_fsub" +[@@unboxed] [@@noalloc] + +external div : float -> float -> float = "coq_fdiv_byte" "coq_fdiv" +[@@unboxed] [@@noalloc] + +external sqrt : float -> float = "coq_fsqrt_byte" "coq_fsqrt" +[@@unboxed] [@@noalloc] + +(*** Test at runtime that no harmful double rounding seems to + be performed with an intermediate 80 bits representation (x87). *) +let () = + let b = ldexp 1. 53 in + let s = add 1. (ldexp 1. (-52)) in + if add b s <= b || add b 1. <> b || ldexp 1. (-1074) <= 0. then + failwith "Detected non IEEE-754 compliant architecture (or wrong \ + rounding mode). Use of Float is thus unsafe." diff --git a/kernel/float64_63.ml b/kernel/float64_63.ml new file mode 100644 index 0000000000..0025531cb1 --- /dev/null +++ b/kernel/float64_63.ml @@ -0,0 +1,35 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +include Float64_common + +let mul (x : float) (y : float) : float = x *. y +[@@ocaml.inline always] + +let add (x : float) (y : float) : float = x +. y +[@@ocaml.inline always] + +let sub (x : float) (y : float) : float = x -. y +[@@ocaml.inline always] + +let div (x : float) (y : float) : float = x /. y +[@@ocaml.inline always] + +let sqrt (x : float) : float = sqrt x +[@@ocaml.inline always] + +(*** Test at runtime that no harmful double rounding seems to + be performed with an intermediate 80 bits representation (x87). *) +let () = + let b = ldexp 1. 53 in + let s = add 1. (ldexp 1. (-52)) in + if add b s <= b || add b 1. <> b || ldexp 1. (-1074) <= 0. then + failwith "Detected non IEEE-754 compliant architecture (or wrong \ + rounding mode). Use of Float is thus unsafe." diff --git a/kernel/float64.ml b/kernel/float64_common.ml index 76005a3dc6..2991a20b49 100644 --- a/kernel/float64.ml +++ b/kernel/float64_common.ml @@ -88,21 +88,6 @@ let classify x = | FP_nan -> NaN [@@ocaml.inline always] -external mul : float -> float -> float = "coq_fmul_byte" "coq_fmul" -[@@unboxed] [@@noalloc] - -external add : float -> float -> float = "coq_fadd_byte" "coq_fadd" -[@@unboxed] [@@noalloc] - -external sub : float -> float -> float = "coq_fsub_byte" "coq_fsub" -[@@unboxed] [@@noalloc] - -external div : float -> float -> float = "coq_fdiv_byte" "coq_fdiv" -[@@unboxed] [@@noalloc] - -external sqrt : float -> float = "coq_fsqrt_byte" "coq_fsqrt" -[@@unboxed] [@@noalloc] - let of_int63 x = Uint63.to_float x [@@ocaml.inline always] @@ -157,12 +142,3 @@ let total_compare f1 f2 = let is_float64 t = Obj.tag t = Obj.double_tag [@@ocaml.inline always] - -(*** Test at runtime that no harmful double rounding seems to - be performed with an intermediate 80 bits representation (x87). *) -let () = - let b = ldexp 1. 53 in - let s = add 1. (ldexp 1. (-52)) in - if add b s <= b || add b 1. <> b || ldexp 1. (-1074) <= 0. then - failwith "Detected non IEEE-754 compliant architecture (or wrong \ - rounding mode). Use of Float is thus unsafe." diff --git a/kernel/float64_common.mli b/kernel/float64_common.mli new file mode 100644 index 0000000000..4fb1c114a5 --- /dev/null +++ b/kernel/float64_common.mli @@ -0,0 +1,95 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** [t] is currently implemented by OCaml's [float] type. + +Beware: NaNs have a sign and a payload, while they should be +indistinguishable from Coq's perspective. *) +type t = float + +(** Test functions for special values to avoid calling [classify] *) +val is_nan : t -> bool +val is_infinity : t -> bool +val is_neg_infinity : t -> bool + +val of_string : string -> t + +(** Print a float exactly as an hexadecimal value (exact decimal + * printing would be possible but sometimes requires more than 700 + * digits). *) +val to_hex_string : t -> string + +(** Print a float as a decimal value. The printing is not exact (the + * real value printed is not always the given floating-point value), + * however printing is precise enough that forall float [f], + * [of_string (to_decimal_string f) = f]. *) +val to_string : t -> string + +val compile : t -> string + +val of_float : float -> t + +(** Return [true] for "-", [false] for "+". *) +val sign : t -> bool + +val opp : t -> t +val abs : t -> t + +type float_comparison = FEq | FLt | FGt | FNotComparable + +val eq : t -> t -> bool + +val lt : t -> t -> bool + +val le : t -> t -> bool + +(** The IEEE 754 float comparison. + * NotComparable is returned if there is a NaN in the arguments *) +val compare : t -> t -> float_comparison +[@@ocaml.inline always] + +type float_class = + | PNormal | NNormal | PSubn | NSubn | PZero | NZero | PInf | NInf | NaN + +val classify : t -> float_class +[@@ocaml.inline always] + +(** Link with integers *) +val of_int63 : Uint63.t -> t +[@@ocaml.inline always] + +val normfr_mantissa : t -> Uint63.t +[@@ocaml.inline always] + +(** Shifted exponent extraction *) +val eshift : int + +val frshiftexp : t -> t * Uint63.t (* float remainder, shifted exponent *) +[@@ocaml.inline always] + +val ldshiftexp : t -> Uint63.t -> t +[@@ocaml.inline always] + +val next_up : t -> t + +val next_down : t -> t + +(** Return true if two floats are equal. + * All NaN values are considered equal. *) +val equal : t -> t -> bool +[@@ocaml.inline always] + +val hash : t -> int + +(** Total order relation over float values. Behaves like [Pervasives.compare].*) +val total_compare : t -> t -> int + +val is_float64 : Obj.t -> bool +[@@ocaml.inline always] diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index d4d7150222..5b2a7bd9c2 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -2,6 +2,7 @@ Names TransparentState Uint63 Parray +Float64_common Float64 Univ UGraph diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 5873d1f502..c7b866179b 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -80,12 +80,11 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = let j = Typeops.infer env' c in assert (j.uj_val == c); (* relevances should already be correct here *) let typ = cb.const_type in - let cst' = Reduction.infer_conv_leq env' (Environ.universes env') - j.uj_type typ in + let cst' = Reduction.infer_conv_leq env' j.uj_type typ in j.uj_val, cst' | Def cs -> let c' = Mod_subst.force_constr cs in - c, Reduction.infer_conv env' (Environ.universes env') c c' + c, Reduction.infer_conv env' c c' | Primitive _ -> error_incorrect_with_constraint lab in @@ -103,12 +102,11 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = let j = Typeops.infer env' c in assert (j.uj_val == c); (* relevances should already be correct here *) let typ = cb.const_type in - let cst' = Reduction.infer_conv_leq env' (Environ.universes env') - j.uj_type typ in + let cst' = Reduction.infer_conv_leq env' j.uj_type typ in cst' | Def cs -> let c' = Mod_subst.force_constr cs in - let cst' = Reduction.infer_conv env' (Environ.universes env') c c' in + let cst' = Reduction.infer_conv env' c c' in cst' | Primitive _ -> error_incorrect_with_constraint lab diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 01e9550ec5..fc6afb79d4 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -176,7 +176,7 @@ let native_conv cv_pb sigma env t1 t2 = else Constr.eq_constr_univs univs t1 t2 in if not b then - let univs = (univs, checked_universes) in + let state = (univs, checked_universes) in let t1 = Term.it_mkLambda_or_LetIn t1 (Environ.rel_context env) in let t2 = Term.it_mkLambda_or_LetIn t2 (Environ.rel_context env) in - let _ = native_conv_gen cv_pb sigma env univs t1 t2 in () + let _ = native_conv_gen cv_pb sigma env state t1 t2 in () diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 7c6b869b4a..96bf370342 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -189,7 +189,7 @@ type 'a kernel_conversion_function = env -> 'a -> 'a -> unit (* functions of this type can be called from outside the kernel *) type 'a extended_conversion_function = ?l2r:bool -> ?reds:TransparentState.t -> env -> - ?evars:((existential->constr option) * UGraph.t) -> + ?evars:(existential->constr option) -> 'a -> 'a -> unit exception NotConvertible @@ -210,9 +210,6 @@ type conv_pb = let is_cumul = function CUMUL -> true | CONV -> false type 'a universe_compare = { - (* used in reduction *) - compare_graph : 'a -> UGraph.t; - (* Might raise NotConvertible *) compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a; compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; @@ -224,7 +221,7 @@ type 'a universe_state = 'a * 'a universe_compare type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b -type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t +type 'a infer_conversion_function = env -> 'a -> 'a -> Univ.Constraint.t let sort_cmp_universes env pb s0 s1 (u, check) = (check.compare_sorts env pb s0 s1 u, check) @@ -765,9 +762,8 @@ and convert_list l2r infos lft1 lft2 v1 v2 cuniv = match v1, v2 with convert_list l2r infos lft1 lft2 v1 v2 cuniv | _, _ -> raise NotConvertible -let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 = +let clos_gen_conv trans cv_pb l2r evars env graph univs t1 t2 = let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in - let graph = (snd univs).compare_graph (fst univs) in let infos = create_clos_infos ~univs:graph ~evars reds env in let infos = { cnv_inf = infos; @@ -815,8 +811,7 @@ let check_inductive_instances cv_pb variance u1 u2 univs = else raise NotConvertible let checked_universes = - { compare_graph = (fun x -> x); - compare_sorts = checked_sort_cmp_universes; + { compare_sorts = checked_sort_cmp_universes; compare_instances = check_convert_instances; compare_cumul_instances = check_inductive_instances; } @@ -878,8 +873,7 @@ let infer_inductive_instances cv_pb variance u1 u2 (univs,csts') = (univs, Univ.Constraint.union csts csts') let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare = - { compare_graph = (fun (x,_) -> x); - compare_sorts = infer_cmp_universes; + { compare_sorts = infer_cmp_universes; compare_instances = infer_convert_instances; compare_cumul_instances = infer_inductive_instances; } @@ -890,12 +884,12 @@ let gen_conv cv_pb l2r reds env evars univs t1 t2 = in if b then () else - let _ = clos_gen_conv reds cv_pb l2r evars env (univs, checked_universes) t1 t2 in + let _ = clos_gen_conv reds cv_pb l2r evars env univs (univs, checked_universes) t1 t2 in () (* Profiling *) -let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=(fun _->None), universes env) = - let evars, univs = evars in +let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=(fun _->None)) = + let univs = Environ.universes env in if Flags.profile then let fconv_universes_key = CProfile.declare_profile "trans_fconv_universes" in CProfile.profile8 fconv_universes_key gen_conv cv_pb l2r reds env evars univs @@ -906,35 +900,37 @@ let conv = gen_conv CONV let conv_leq = gen_conv CUMUL let generic_conv cv_pb ~l2r evars reds env univs t1 t2 = + let graph = Environ.universes env in let (s, _) = - clos_gen_conv reds cv_pb l2r evars env univs t1 t2 + clos_gen_conv reds cv_pb l2r evars env graph univs t1 t2 in s -let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 = +let infer_conv_universes cv_pb l2r evars reds env t1 t2 = + let univs = Environ.universes env in let b, cstrs = if cv_pb == CUMUL then Constr.leq_constr_univs_infer univs t1 t2 else Constr.eq_constr_univs_infer univs t1 t2 in if b then cstrs else - let univs = ((univs, Univ.Constraint.empty), inferred_universes) in - let ((_,cstrs), _) = clos_gen_conv reds cv_pb l2r evars env univs t1 t2 in + let state = ((univs, Univ.Constraint.empty), inferred_universes) in + let ((_,cstrs), _) = clos_gen_conv reds cv_pb l2r evars env univs state t1 t2 in cstrs (* Profiling *) let infer_conv_universes = if Flags.profile then let infer_conv_universes_key = CProfile.declare_profile "infer_conv_universes" in - CProfile.profile8 infer_conv_universes_key infer_conv_universes + CProfile.profile7 infer_conv_universes_key infer_conv_universes else infer_conv_universes let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full) - env univs t1 t2 = - infer_conv_universes CONV l2r evars ts env univs t1 t2 + env t1 t2 = + infer_conv_universes CONV l2r evars ts env t1 t2 let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full) - env univs t1 t2 = - infer_conv_universes CUMUL l2r evars ts env univs t1 t2 + env t1 t2 = + infer_conv_universes CUMUL l2r evars ts env t1 t2 let default_conv cv_pb ?l2r:_ env t1 t2 = gen_conv cv_pb env t1 t2 diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 4ae3838691..7d32596f74 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -31,14 +31,12 @@ exception NotConvertible type 'a kernel_conversion_function = env -> 'a -> 'a -> unit type 'a extended_conversion_function = ?l2r:bool -> ?reds:TransparentState.t -> env -> - ?evars:((existential->constr option) * UGraph.t) -> + ?evars:(existential->constr option) -> 'a -> 'a -> unit type conv_pb = CONV | CUMUL type 'a universe_compare = { - compare_graph : 'a -> UGraph.t; (* used for case inversion in reduction *) - (* Might raise NotConvertible *) compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a; compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; @@ -50,7 +48,7 @@ type 'a universe_state = 'a * 'a universe_compare type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b -type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t +type 'a infer_conversion_function = env -> 'a -> 'a -> Univ.Constraint.t val get_cumulativity_constraints : conv_pb -> Univ.Variance.t array -> Univ.Instance.t -> Univ.Instance.t -> Univ.Constraint.t diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 28baa82666..76a1c190be 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -85,7 +85,7 @@ let make_labmap mp list = let check_conv_error error why cst poly f env a1 a2 = try - let cst' = f env (Environ.universes env) a1 a2 in + let cst' = f env a1 a2 in if poly then if Constraint.is_empty cst' then cst else error (IncompatiblePolymorphism (env, a1, a2)) diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 87a5666fcc..d381e55dd6 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -111,7 +111,7 @@ val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t (** {6 Miscellaneous. } *) (** Check that hyps are included in env and fails with error otherwise *) -val check_hyps_inclusion : env -> ?evars:((existential->constr option) * UGraph.t) -> +val check_hyps_inclusion : env -> ?evars:(existential->constr option) -> GlobRef.t -> Constr.named_context -> unit (** Types for primitives *) diff --git a/kernel/vconv.ml b/kernel/vconv.ml index cc2c2c0b4b..948195797e 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -211,5 +211,5 @@ let vm_conv cv_pb env t1 t2 = else Constr.eq_constr_univs univs t1 t2 in if not b then - let univs = (univs, checked_universes) in - let _ = vm_conv_gen cv_pb env univs t1 t2 in () + let state = (univs, checked_universes) in + let _ = vm_conv_gen cv_pb env state t1 t2 in () diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 1ec83c496a..644493a010 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -154,7 +154,7 @@ GRAMMAR EXTEND Gram | "10" LEFTA [ f = operconstr; args = LIST1 appl_arg -> { CAst.make ~loc @@ CApp((None,f),args) } | "@"; f = global; i = univ_instance; args = LIST0 NEXT -> { CAst.make ~loc @@ CAppExpl((None,f,i),args) } - | "@"; lid = pattern_identref; args = LIST1 identref -> + | "@"; lid = pattern_ident; args = LIST1 identref -> { let { CAst.loc = locid; v = id } = lid in let args = List.map (fun x -> CAst.make @@ CRef (qualid_of_ident ?loc:x.CAst.loc x.CAst.v, None), None) args in CAst.make ~loc @@ CApp((None, CAst.make ?loc:locid @@ CPatVar id),args) } ] @@ -252,7 +252,7 @@ GRAMMAR EXTEND Gram | "cofix"; c = cofix_decls -> { let (id,dcls) = c in CAst.make ~loc @@ CCoFix (id,dcls) } ] ] ; appl_arg: - [ [ test_lpar_id_coloneq; "("; id = ident; ":="; c = lconstr; ")" -> { (c,Some (CAst.make ~loc @@ ExplByName id)) } + [ [ test_lpar_id_coloneq; "("; id = identref; ":="; c = lconstr; ")" -> { (c,Some (CAst.make ?loc:id.CAst.loc @@ ExplByName id.CAst.v)) } | c=operconstr LEVEL "9" -> { (c,None) } ] ] ; atomic_constr: @@ -261,12 +261,12 @@ GRAMMAR EXTEND Gram | n = NUMBER-> { CAst.make ~loc @@ CPrim (Numeral (NumTok.SPlus,n)) } | s = string -> { CAst.make ~loc @@ CPrim (String s) } | "_" -> { CAst.make ~loc @@ CHole (None, IntroAnonymous, None) } - | "?"; "["; id = ident; "]" -> { CAst.make ~loc @@ CHole (None, IntroIdentifier id, None) } - | "?"; "["; id = pattern_ident; "]" -> { CAst.make ~loc @@ CHole (None, IntroFresh id, None) } + | "?"; "["; id = identref; "]" -> { CAst.make ~loc @@ CHole (None, IntroIdentifier id.CAst.v, None) } + | "?"; "["; id = pattern_ident; "]" -> { CAst.make ~loc @@ CHole (None, IntroFresh id.CAst.v, None) } | id = pattern_ident; inst = evar_instance -> { CAst.make ~loc @@ CEvar(id,inst) } ] ] ; inst: - [ [ id = ident; ":="; c = lconstr -> { (id,c) } ] ] + [ [ id = identref; ":="; c = lconstr -> { (id,c) } ] ] ; evar_instance: [ [ "@{"; l = LIST1 inst SEP ";"; "}" -> { l } diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg index 270662b824..1701830cd2 100644 --- a/parsing/g_prim.mlg +++ b/parsing/g_prim.mlg @@ -45,9 +45,9 @@ let test_minus_nat = GRAMMAR EXTEND Gram GLOBAL: - bignat bigint natural integer identref name ident var preident + bignat bigint natural integer identref name ident hyp preident fullyqualid qualid reference dirpath ne_lstring - ne_string string lstring pattern_ident pattern_identref by_notation + ne_string string lstring pattern_ident by_notation smart_global bar_cbrace strategy_level; preident: [ [ s = IDENT -> { s } ] ] @@ -56,17 +56,14 @@ GRAMMAR EXTEND Gram [ [ s = IDENT -> { Id.of_string s } ] ] ; pattern_ident: - [ [ LEFTQMARK; id = ident -> { id } ] ] - ; - pattern_identref: - [ [ id = pattern_ident -> { CAst.make ~loc id } ] ] - ; - var: (* as identref, but interpret as a term identifier in ltac *) - [ [ id = ident -> { CAst.make ~loc id } ] ] + [ [ LEFTQMARK; id = ident -> { CAst.make ~loc id } ] ] ; identref: [ [ id = ident -> { CAst.make ~loc id } ] ] ; + hyp: (* as identref, but interpreted as an hypothesis in tactic notations *) + [ [ id = identref -> { id } ] ] + ; field: [ [ s = FIELD -> { Id.of_string s } ] ] ; diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 723f08413e..996aa0925c 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -279,14 +279,15 @@ module Prim = let strategy_level = Entry.create "strategy_level" (* parsed like ident but interpreted as a term *) - let var = Entry.create "var" + let hyp = Entry.create "hyp" + let var = hyp let name = Entry.create "name" let identref = Entry.create "identref" let univ_decl = Entry.create "univ_decl" let ident_decl = Entry.create "ident_decl" let pattern_ident = Entry.create "pattern_ident" - let pattern_identref = Entry.create "pattern_identref" + let pattern_identref = pattern_ident (* To remove in 8.14 *) (* A synonym of ident - maybe ident will be located one day *) let base_ident = Entry.create "base_ident" @@ -504,7 +505,7 @@ let () = Grammar.register0 wit_string (Prim.string); Grammar.register0 wit_pre_ident (Prim.preident); Grammar.register0 wit_ident (Prim.ident); - Grammar.register0 wit_var (Prim.var); + Grammar.register0 wit_hyp (Prim.hyp); Grammar.register0 wit_ref (Prim.reference); Grammar.register0 wit_smart_global (Prim.smart_global); Grammar.register0 wit_sort_family (Constr.sort_family); diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index ae9a7423c2..8e60bbf504 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -156,8 +156,8 @@ module Prim : val identref : lident Entry.t val univ_decl : universe_decl_expr Entry.t val ident_decl : ident_decl Entry.t - val pattern_ident : Id.t Entry.t - val pattern_identref : lident Entry.t + val pattern_ident : lident Entry.t + val pattern_identref : lident Entry.t [@@ocaml.deprecated "Use Prim.pattern_identref"] val base_ident : Id.t Entry.t val bignat : string Entry.t val natural : int Entry.t @@ -173,7 +173,8 @@ module Prim : val dirpath : DirPath.t Entry.t val ne_string : string Entry.t val ne_lstring : lstring Entry.t - val var : lident Entry.t + val hyp : lident Entry.t + val var : lident Entry.t [@@ocaml.deprecated "Use Prim.hyp"] val bar_cbrace : unit Entry.t val strategy_level : Conv_oracle.level Entry.t end diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg index f1f538ab39..b7ac71181a 100644 --- a/plugins/ltac/coretactics.mlg +++ b/plugins/ltac/coretactics.mlg @@ -20,8 +20,6 @@ open Tacarg open Names open Logic -let wit_hyp = wit_var - } DECLARE PLUGIN "ltac_plugin" diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg index 863c4d37d8..ad4374dba3 100644 --- a/plugins/ltac/extraargs.mlg +++ b/plugins/ltac/extraargs.mlg @@ -47,7 +47,7 @@ let () = let () = let register name entry = Tacentries.register_tactic_notation_entry name entry in - register "hyp" wit_var; + register "hyp" wit_hyp; register "simple_intropattern" wit_simple_intropattern; register "integer" wit_integer; register "reference" wit_ref; @@ -140,7 +140,7 @@ ARGUMENT EXTEND occurrences GLOB_PRINTED BY { pr_occurrences } | [ ne_integer_list(l) ] -> { ArgArg l } -| [ var(id) ] -> { ArgVar id } +| [ hyp(id) ] -> { ArgVar id } END { diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 4f20e5a800..a2a47c0bf4 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -33,8 +33,6 @@ open Proofview.Notations open Attributes open Vernacextend -let wit_hyp = wit_var - } DECLARE PLUGIN "ltac_plugin" @@ -450,7 +448,7 @@ END (* Subst *) TACTIC EXTEND subst -| [ "subst" ne_var_list(l) ] -> { subst l } +| [ "subst" ne_hyp_list(l) ] -> { subst l } | [ "subst" ] -> { subst_all () } END diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index 2e72ceae5a..44472a1995 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -18,8 +18,6 @@ open Pcoq.Constr open Pltac open Hints -let wit_hyp = wit_var - } DECLARE PLUGIN "ltac_plugin" diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg index 8d197e6056..8c2e633be5 100644 --- a/plugins/ltac/g_class.mlg +++ b/plugins/ltac/g_class.mlg @@ -31,12 +31,12 @@ let set_transparency cl b = } VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings CLASSIFIED AS SIDEFF -| [ "Typeclasses" "Transparent" reference_list(cl) ] -> { +| [ "Typeclasses" "Transparent" ne_reference_list(cl) ] -> { set_transparency cl true } END VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings CLASSIFIED AS SIDEFF -| [ "Typeclasses" "Opaque" reference_list(cl) ] -> { +| [ "Typeclasses" "Opaque" ne_reference_list(cl) ] -> { set_transparency cl false } END @@ -77,7 +77,7 @@ END (* true = All transparent, false = Opaque if possible *) VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF - | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) integer_opt(depth) ] -> { + | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) natural_opt(depth) ] -> { set_typeclasses_debug d; Option.iter set_typeclasses_strategy s; set_typeclasses_depth depth @@ -87,11 +87,13 @@ END (** Compatibility: typeclasses eauto has 8.5 and 8.6 modes *) TACTIC EXTEND typeclasses_eauto | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) "with" ne_preident_list(l) ] -> - { typeclasses_eauto ~strategy:Bfs ~depth:d l } + { typeclasses_eauto ~depth:d ~strategy:Bfs l } | [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] -> { typeclasses_eauto ~depth:d l } + | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) ] -> { + typeclasses_eauto ~depth:d ~strategy:Bfs ~only_classes:true [Class_tactics.typeclasses_db] } | [ "typeclasses" "eauto" int_or_var_opt(d) ] -> { - typeclasses_eauto ~only_classes:true ~depth:d [Class_tactics.typeclasses_db] } + typeclasses_eauto ~depth:d ~only_classes:true [Class_tactics.typeclasses_db] } END TACTIC EXTEND head_of_constr diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index fc24475a62..6bf330c830 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -111,6 +111,8 @@ END VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF STATE program | [ "Solve" "Obligations" "of" ident(name) "with" tactic(t) ] -> { try_solve_obligations (Some name) (Some (Tacinterp.interp t)) } +| [ "Solve" "Obligations" "of" ident(name) ] -> + { try_solve_obligations (Some name) None } | [ "Solve" "Obligations" "with" tactic(t) ] -> { try_solve_obligations None (Some (Tacinterp.interp t)) } | [ "Solve" "Obligations" ] -> diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 8331927cda..ee94fd565a 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -29,8 +29,6 @@ open Pvernac.Vernac_ open Pltac open Vernacextend -let wit_hyp = wit_var - } DECLARE PLUGIN "ltac_plugin" diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index e51b1f051d..c186a83a5c 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -280,7 +280,7 @@ GRAMMAR EXTEND Gram | "[="; tc = intropatterns; "]" -> { IntroInjection tc } ] ] ; naming_intropattern: - [ [ prefix = pattern_ident -> { IntroFresh prefix } + [ [ prefix = pattern_ident -> { IntroFresh prefix.CAst.v } | "?" -> { IntroAnonymous } | id = ident -> { IntroIdentifier id } ] ] ; diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index cbb53497d3..fe896f9351 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1323,7 +1323,7 @@ let () = register_basic_print0 wit_smart_global (pr_or_by_notation pr_qualid) (pr_or_var (pr_located pr_global)) pr_global; register_basic_print0 wit_ident pr_id pr_id pr_id; - register_basic_print0 wit_var pr_lident pr_lident pr_id; + register_basic_print0 wit_hyp pr_lident pr_lident pr_id; register_print0 wit_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env [@warning "-3"]; register_print0 wit_simple_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env; Genprint.register_print0 diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index f7037176d2..ee28229cb7 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -161,8 +161,8 @@ let coerce_var_to_ident fresh env sigma v = match out_gen (topwit wit_intro_pattern) v with | { CAst.v=IntroNaming (IntroIdentifier id)} -> id | _ -> fail () - else if has_type v (topwit wit_var) then - out_gen (topwit wit_var) v + else if has_type v (topwit wit_hyp) then + out_gen (topwit wit_hyp) v else match Value.to_constr v with | None -> fail () | Some c -> @@ -184,8 +184,8 @@ let id_of_name = function | Some (IntroNaming (IntroIdentifier id)) -> id | Some _ -> fail () | None -> - if has_type v (topwit wit_var) then - out_gen (topwit wit_var) v + if has_type v (topwit wit_hyp) then + out_gen (topwit wit_hyp) v else match Value.to_constr v with | None -> fail () @@ -222,8 +222,8 @@ let coerce_to_intro_pattern sigma v = match is_intro_pattern v with | Some pat -> pat | None -> - if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in + if has_type v (topwit wit_hyp) then + let id = out_gen (topwit wit_hyp) v in IntroNaming (IntroIdentifier id) else match Value.to_constr v with | Some c when isVar sigma c -> @@ -259,8 +259,8 @@ let coerce_to_constr env v = ([], c) else if has_type v (topwit wit_constr_under_binders) then out_gen (topwit wit_constr_under_binders) v - else if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in + else if has_type v (topwit wit_hyp) then + let id = out_gen (topwit wit_hyp) v in (try [], constr_of_id env id with Not_found -> fail ()) else fail () @@ -282,8 +282,8 @@ let coerce_to_evaluable_ref env sigma v = | Some (IntroNaming (IntroIdentifier id)) when is_variable env id -> EvalVarRef id | Some _ -> fail () | None -> - if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in + if has_type v (topwit wit_hyp) then + let id = out_gen (topwit wit_hyp) v in if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id else fail () else if has_type v (topwit wit_ref) then @@ -328,8 +328,8 @@ let coerce_to_hyp env sigma v = | Some (IntroNaming (IntroIdentifier id)) when is_variable env id -> id | Some _ -> fail () | None -> - if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in + if has_type v (topwit wit_hyp) then + let id = out_gen (topwit wit_hyp) v in if is_variable env id then id else fail () else match Value.to_constr v with | Some c when isVar sigma c -> destVar sigma c @@ -360,8 +360,8 @@ let coerce_to_quantified_hypothesis sigma v = | Some (IntroNaming (IntroIdentifier id)) -> NamedHyp id | Some _ -> raise (CannotCoerceTo "a quantified hypothesis") | None -> - if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in + if has_type v (topwit wit_hyp) then + let id = out_gen (topwit wit_hyp) v in NamedHyp id else if has_type v (topwit wit_int) then AnonHyp (out_gen (topwit wit_int) v) diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index f0ca813b08..d58a76fe13 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -219,7 +219,9 @@ let interp_prod_item = function | None -> if String.Map.mem s !entry_names then String.Map.find s !entry_names else begin match ArgT.name s with - | None -> user_err Pp.(str ("Unknown entry "^s^".")) + | None -> + if s = "var" then user_err Pp.(str ("var is deprecated, use hyp.")) (* to remove in 8.14 *) + else user_err Pp.(str ("Unknown entry "^s^".")) | Some arg -> arg end | Some n -> diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index dea216045e..9c3b05fdf1 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -835,7 +835,7 @@ let () = Genintern.register_intern0 wit_ref (lift intern_global_reference); Genintern.register_intern0 wit_pre_ident (fun ist c -> (ist,c)); Genintern.register_intern0 wit_ident intern_ident'; - Genintern.register_intern0 wit_var (lift intern_hyp); + Genintern.register_intern0 wit_hyp (lift intern_hyp); Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg); Genintern.register_intern0 wit_ltac (lift intern_ltac); Genintern.register_intern0 wit_quant_hyp (lift intern_quantified_hypothesis); diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index eaeae50254..12bfb4d09e 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -971,8 +971,8 @@ let interp_destruction_arg ist gl arg = match v with | {v=IntroNaming (IntroIdentifier id)} -> try_cast_id id | _ -> error () - else if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in + else if has_type v (topwit wit_hyp) then + let id = out_gen (topwit wit_hyp) v in try_cast_id id else if has_type v (topwit wit_int) then keep,ElimOnAnonHyp (out_gen (topwit wit_int) v) @@ -1238,7 +1238,7 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t = | ArgVar {loc;v=id} -> let v = try Id.Map.find id ist.lfun - with Not_found -> in_gen (topwit wit_var) id + with Not_found -> in_gen (topwit wit_hyp) id in let open Ftactic in force_vrec ist v >>= begin fun v -> @@ -1529,7 +1529,7 @@ and interp_genarg ist x : Val.t Ftactic.t = let open Ftactic.Notations in (* Ad-hoc handling of some types. *) let tag = genarg_tag x in - if argument_type_eq tag (unquote (topwit (wit_list wit_var))) then + if argument_type_eq tag (unquote (topwit (wit_list wit_hyp))) then interp_genarg_var_list ist x else if argument_type_eq tag (unquote (topwit (wit_list wit_constr))) then interp_genarg_constr_list ist x @@ -1573,9 +1573,9 @@ and interp_genarg_var_list ist x = Ftactic.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let lc = Genarg.out_gen (glbwit (wit_list wit_var)) x in + let lc = Genarg.out_gen (glbwit (wit_list wit_hyp)) x in let lc = interp_hyp_list ist env sigma lc in - let lc = in_list (val_tag wit_var) lc in + let lc = in_list (val_tag wit_hyp) lc in Ftactic.return lc end @@ -2096,7 +2096,7 @@ let () = register_interp0 wit_ref (lift interp_reference); register_interp0 wit_pre_ident (lift interp_pre_ident); register_interp0 wit_ident (lift interp_ident); - register_interp0 wit_var (lift interp_hyp); + register_interp0 wit_hyp (lift interp_hyp); register_interp0 wit_intropattern (lifts interp_intro_pattern) [@warning "-3"]; register_interp0 wit_simple_intropattern (lifts interp_intro_pattern); register_interp0 wit_clause_dft_concl (lift interp_clause); diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index fd869b225f..ec44ae4698 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -282,7 +282,7 @@ let () = Genintern.register_subst0 wit_smart_global subst_global_reference; Genintern.register_subst0 wit_pre_ident (fun _ v -> v); Genintern.register_subst0 wit_ident (fun _ v -> v); - Genintern.register_subst0 wit_var (fun _ v -> v); + Genintern.register_subst0 wit_hyp (fun _ v -> v); Genintern.register_subst0 wit_intropattern subst_intro_pattern [@warning "-3"]; Genintern.register_subst0 wit_simple_intropattern subst_intro_pattern; Genintern.register_subst0 wit_tactic subst_tactic; diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index d2c49c4432..542b99075d 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -134,166 +134,161 @@ let selecti s m = *) (** - * MODULE END: M - *) -module M = struct - (** * Initialization : a large amount of Caml symbols are derived from * ZMicromega.v *) - let constr_of_ref str = - EConstr.of_constr - (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref str)) - - let coq_and = lazy (constr_of_ref "core.and.type") - let coq_or = lazy (constr_of_ref "core.or.type") - let coq_not = lazy (constr_of_ref "core.not.type") - let coq_iff = lazy (constr_of_ref "core.iff.type") - let coq_True = lazy (constr_of_ref "core.True.type") - let coq_False = lazy (constr_of_ref "core.False.type") - let coq_bool = lazy (constr_of_ref "core.bool.type") - let coq_true = lazy (constr_of_ref "core.bool.true") - let coq_false = lazy (constr_of_ref "core.bool.false") - let coq_andb = lazy (constr_of_ref "core.bool.andb") - let coq_orb = lazy (constr_of_ref "core.bool.orb") - let coq_implb = lazy (constr_of_ref "core.bool.implb") - let coq_eqb = lazy (constr_of_ref "core.bool.eqb") - let coq_negb = lazy (constr_of_ref "core.bool.negb") - let coq_cons = lazy (constr_of_ref "core.list.cons") - let coq_nil = lazy (constr_of_ref "core.list.nil") - let coq_list = lazy (constr_of_ref "core.list.type") - let coq_O = lazy (constr_of_ref "num.nat.O") - let coq_S = lazy (constr_of_ref "num.nat.S") - let coq_nat = lazy (constr_of_ref "num.nat.type") - let coq_unit = lazy (constr_of_ref "core.unit.type") - - (* let coq_option = lazy (init_constant "option")*) - let coq_None = lazy (constr_of_ref "core.option.None") - let coq_tt = lazy (constr_of_ref "core.unit.tt") - let coq_Inl = lazy (constr_of_ref "core.sum.inl") - let coq_Inr = lazy (constr_of_ref "core.sum.inr") - let coq_N0 = lazy (constr_of_ref "num.N.N0") - let coq_Npos = lazy (constr_of_ref "num.N.Npos") - let coq_xH = lazy (constr_of_ref "num.pos.xH") - let coq_xO = lazy (constr_of_ref "num.pos.xO") - let coq_xI = lazy (constr_of_ref "num.pos.xI") - let coq_Z = lazy (constr_of_ref "num.Z.type") - let coq_ZERO = lazy (constr_of_ref "num.Z.Z0") - let coq_POS = lazy (constr_of_ref "num.Z.Zpos") - let coq_NEG = lazy (constr_of_ref "num.Z.Zneg") - let coq_Q = lazy (constr_of_ref "rat.Q.type") - let coq_Qmake = lazy (constr_of_ref "rat.Q.Qmake") - let coq_R = lazy (constr_of_ref "reals.R.type") - let coq_Rcst = lazy (constr_of_ref "micromega.Rcst.type") - let coq_C0 = lazy (constr_of_ref "micromega.Rcst.C0") - let coq_C1 = lazy (constr_of_ref "micromega.Rcst.C1") - let coq_CQ = lazy (constr_of_ref "micromega.Rcst.CQ") - let coq_CZ = lazy (constr_of_ref "micromega.Rcst.CZ") - let coq_CPlus = lazy (constr_of_ref "micromega.Rcst.CPlus") - let coq_CMinus = lazy (constr_of_ref "micromega.Rcst.CMinus") - let coq_CMult = lazy (constr_of_ref "micromega.Rcst.CMult") - let coq_CPow = lazy (constr_of_ref "micromega.Rcst.CPow") - let coq_CInv = lazy (constr_of_ref "micromega.Rcst.CInv") - let coq_COpp = lazy (constr_of_ref "micromega.Rcst.COpp") - let coq_R0 = lazy (constr_of_ref "reals.R.R0") - let coq_R1 = lazy (constr_of_ref "reals.R.R1") - let coq_proofTerm = lazy (constr_of_ref "micromega.ZArithProof.type") - let coq_doneProof = lazy (constr_of_ref "micromega.ZArithProof.DoneProof") - let coq_ratProof = lazy (constr_of_ref "micromega.ZArithProof.RatProof") - let coq_cutProof = lazy (constr_of_ref "micromega.ZArithProof.CutProof") - let coq_enumProof = lazy (constr_of_ref "micromega.ZArithProof.EnumProof") - let coq_ExProof = lazy (constr_of_ref "micromega.ZArithProof.ExProof") - let coq_IsProp = lazy (constr_of_ref "micromega.kind.isProp") - let coq_IsBool = lazy (constr_of_ref "micromega.kind.isBool") - let coq_Zgt = lazy (constr_of_ref "num.Z.gt") - let coq_Zge = lazy (constr_of_ref "num.Z.ge") - let coq_Zle = lazy (constr_of_ref "num.Z.le") - let coq_Zlt = lazy (constr_of_ref "num.Z.lt") - let coq_Zgtb = lazy (constr_of_ref "num.Z.gtb") - let coq_Zgeb = lazy (constr_of_ref "num.Z.geb") - let coq_Zleb = lazy (constr_of_ref "num.Z.leb") - let coq_Zltb = lazy (constr_of_ref "num.Z.ltb") - let coq_Zeqb = lazy (constr_of_ref "num.Z.eqb") - let coq_eq = lazy (constr_of_ref "core.eq.type") - let coq_Zplus = lazy (constr_of_ref "num.Z.add") - let coq_Zminus = lazy (constr_of_ref "num.Z.sub") - let coq_Zopp = lazy (constr_of_ref "num.Z.opp") - let coq_Zmult = lazy (constr_of_ref "num.Z.mul") - let coq_Zpower = lazy (constr_of_ref "num.Z.pow") - let coq_Qle = lazy (constr_of_ref "rat.Q.Qle") - let coq_Qlt = lazy (constr_of_ref "rat.Q.Qlt") - let coq_Qeq = lazy (constr_of_ref "rat.Q.Qeq") - let coq_Qplus = lazy (constr_of_ref "rat.Q.Qplus") - let coq_Qminus = lazy (constr_of_ref "rat.Q.Qminus") - let coq_Qopp = lazy (constr_of_ref "rat.Q.Qopp") - let coq_Qmult = lazy (constr_of_ref "rat.Q.Qmult") - let coq_Qpower = lazy (constr_of_ref "rat.Q.Qpower") - let coq_Rgt = lazy (constr_of_ref "reals.R.Rgt") - let coq_Rge = lazy (constr_of_ref "reals.R.Rge") - let coq_Rle = lazy (constr_of_ref "reals.R.Rle") - let coq_Rlt = lazy (constr_of_ref "reals.R.Rlt") - let coq_Rplus = lazy (constr_of_ref "reals.R.Rplus") - let coq_Rminus = lazy (constr_of_ref "reals.R.Rminus") - let coq_Ropp = lazy (constr_of_ref "reals.R.Ropp") - let coq_Rmult = lazy (constr_of_ref "reals.R.Rmult") - let coq_Rinv = lazy (constr_of_ref "reals.R.Rinv") - let coq_Rpower = lazy (constr_of_ref "reals.R.pow") - let coq_powerZR = lazy (constr_of_ref "reals.R.powerRZ") - let coq_IZR = lazy (constr_of_ref "reals.R.IZR") - let coq_IQR = lazy (constr_of_ref "reals.R.Q2R") - let coq_PEX = lazy (constr_of_ref "micromega.PExpr.PEX") - let coq_PEc = lazy (constr_of_ref "micromega.PExpr.PEc") - let coq_PEadd = lazy (constr_of_ref "micromega.PExpr.PEadd") - let coq_PEopp = lazy (constr_of_ref "micromega.PExpr.PEopp") - let coq_PEmul = lazy (constr_of_ref "micromega.PExpr.PEmul") - let coq_PEsub = lazy (constr_of_ref "micromega.PExpr.PEsub") - let coq_PEpow = lazy (constr_of_ref "micromega.PExpr.PEpow") - let coq_PX = lazy (constr_of_ref "micromega.Pol.PX") - let coq_Pc = lazy (constr_of_ref "micromega.Pol.Pc") - let coq_Pinj = lazy (constr_of_ref "micromega.Pol.Pinj") - let coq_OpEq = lazy (constr_of_ref "micromega.Op2.OpEq") - let coq_OpNEq = lazy (constr_of_ref "micromega.Op2.OpNEq") - let coq_OpLe = lazy (constr_of_ref "micromega.Op2.OpLe") - let coq_OpLt = lazy (constr_of_ref "micromega.Op2.OpLt") - let coq_OpGe = lazy (constr_of_ref "micromega.Op2.OpGe") - let coq_OpGt = lazy (constr_of_ref "micromega.Op2.OpGt") - let coq_PsatzIn = lazy (constr_of_ref "micromega.Psatz.PsatzIn") - let coq_PsatzSquare = lazy (constr_of_ref "micromega.Psatz.PsatzSquare") - let coq_PsatzMulE = lazy (constr_of_ref "micromega.Psatz.PsatzMulE") - let coq_PsatzMultC = lazy (constr_of_ref "micromega.Psatz.PsatzMulC") - let coq_PsatzAdd = lazy (constr_of_ref "micromega.Psatz.PsatzAdd") - let coq_PsatzC = lazy (constr_of_ref "micromega.Psatz.PsatzC") - let coq_PsatzZ = lazy (constr_of_ref "micromega.Psatz.PsatzZ") - - (* let coq_GT = lazy (m_constant "GT")*) - - let coq_DeclaredConstant = - lazy (constr_of_ref "micromega.DeclaredConstant.type") - - let coq_TT = lazy (constr_of_ref "micromega.GFormula.TT") - let coq_FF = lazy (constr_of_ref "micromega.GFormula.FF") - let coq_AND = lazy (constr_of_ref "micromega.GFormula.AND") - let coq_OR = lazy (constr_of_ref "micromega.GFormula.OR") - let coq_NOT = lazy (constr_of_ref "micromega.GFormula.NOT") - let coq_Atom = lazy (constr_of_ref "micromega.GFormula.A") - let coq_X = lazy (constr_of_ref "micromega.GFormula.X") - let coq_IMPL = lazy (constr_of_ref "micromega.GFormula.IMPL") - let coq_IFF = lazy (constr_of_ref "micromega.GFormula.IFF") - let coq_EQ = lazy (constr_of_ref "micromega.GFormula.EQ") - let coq_Formula = lazy (constr_of_ref "micromega.BFormula.type") - let coq_eKind = lazy (constr_of_ref "micromega.eKind") - - (** +let constr_of_ref str = + EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref str)) + +let coq_and = lazy (constr_of_ref "core.and.type") +let coq_or = lazy (constr_of_ref "core.or.type") +let coq_not = lazy (constr_of_ref "core.not.type") +let coq_iff = lazy (constr_of_ref "core.iff.type") +let coq_True = lazy (constr_of_ref "core.True.type") +let coq_False = lazy (constr_of_ref "core.False.type") +let coq_bool = lazy (constr_of_ref "core.bool.type") +let coq_true = lazy (constr_of_ref "core.bool.true") +let coq_false = lazy (constr_of_ref "core.bool.false") +let coq_andb = lazy (constr_of_ref "core.bool.andb") +let coq_orb = lazy (constr_of_ref "core.bool.orb") +let coq_implb = lazy (constr_of_ref "core.bool.implb") +let coq_eqb = lazy (constr_of_ref "core.bool.eqb") +let coq_negb = lazy (constr_of_ref "core.bool.negb") +let coq_cons = lazy (constr_of_ref "core.list.cons") +let coq_nil = lazy (constr_of_ref "core.list.nil") +let coq_list = lazy (constr_of_ref "core.list.type") +let coq_O = lazy (constr_of_ref "num.nat.O") +let coq_S = lazy (constr_of_ref "num.nat.S") +let coq_nat = lazy (constr_of_ref "num.nat.type") +let coq_unit = lazy (constr_of_ref "core.unit.type") + +(* let coq_option = lazy (init_constant "option")*) +let coq_None = lazy (constr_of_ref "core.option.None") +let coq_tt = lazy (constr_of_ref "core.unit.tt") +let coq_Inl = lazy (constr_of_ref "core.sum.inl") +let coq_Inr = lazy (constr_of_ref "core.sum.inr") +let coq_N0 = lazy (constr_of_ref "num.N.N0") +let coq_Npos = lazy (constr_of_ref "num.N.Npos") +let coq_xH = lazy (constr_of_ref "num.pos.xH") +let coq_xO = lazy (constr_of_ref "num.pos.xO") +let coq_xI = lazy (constr_of_ref "num.pos.xI") +let coq_Z = lazy (constr_of_ref "num.Z.type") +let coq_ZERO = lazy (constr_of_ref "num.Z.Z0") +let coq_POS = lazy (constr_of_ref "num.Z.Zpos") +let coq_NEG = lazy (constr_of_ref "num.Z.Zneg") +let coq_Q = lazy (constr_of_ref "rat.Q.type") +let coq_Qmake = lazy (constr_of_ref "rat.Q.Qmake") +let coq_R = lazy (constr_of_ref "reals.R.type") +let coq_Rcst = lazy (constr_of_ref "micromega.Rcst.type") +let coq_C0 = lazy (constr_of_ref "micromega.Rcst.C0") +let coq_C1 = lazy (constr_of_ref "micromega.Rcst.C1") +let coq_CQ = lazy (constr_of_ref "micromega.Rcst.CQ") +let coq_CZ = lazy (constr_of_ref "micromega.Rcst.CZ") +let coq_CPlus = lazy (constr_of_ref "micromega.Rcst.CPlus") +let coq_CMinus = lazy (constr_of_ref "micromega.Rcst.CMinus") +let coq_CMult = lazy (constr_of_ref "micromega.Rcst.CMult") +let coq_CPow = lazy (constr_of_ref "micromega.Rcst.CPow") +let coq_CInv = lazy (constr_of_ref "micromega.Rcst.CInv") +let coq_COpp = lazy (constr_of_ref "micromega.Rcst.COpp") +let coq_R0 = lazy (constr_of_ref "reals.R.R0") +let coq_R1 = lazy (constr_of_ref "reals.R.R1") +let coq_proofTerm = lazy (constr_of_ref "micromega.ZArithProof.type") +let coq_doneProof = lazy (constr_of_ref "micromega.ZArithProof.DoneProof") +let coq_ratProof = lazy (constr_of_ref "micromega.ZArithProof.RatProof") +let coq_cutProof = lazy (constr_of_ref "micromega.ZArithProof.CutProof") +let coq_enumProof = lazy (constr_of_ref "micromega.ZArithProof.EnumProof") +let coq_ExProof = lazy (constr_of_ref "micromega.ZArithProof.ExProof") +let coq_IsProp = lazy (constr_of_ref "micromega.kind.isProp") +let coq_IsBool = lazy (constr_of_ref "micromega.kind.isBool") +let coq_Zgt = lazy (constr_of_ref "num.Z.gt") +let coq_Zge = lazy (constr_of_ref "num.Z.ge") +let coq_Zle = lazy (constr_of_ref "num.Z.le") +let coq_Zlt = lazy (constr_of_ref "num.Z.lt") +let coq_Zgtb = lazy (constr_of_ref "num.Z.gtb") +let coq_Zgeb = lazy (constr_of_ref "num.Z.geb") +let coq_Zleb = lazy (constr_of_ref "num.Z.leb") +let coq_Zltb = lazy (constr_of_ref "num.Z.ltb") +let coq_Zeqb = lazy (constr_of_ref "num.Z.eqb") +let coq_eq = lazy (constr_of_ref "core.eq.type") +let coq_Zplus = lazy (constr_of_ref "num.Z.add") +let coq_Zminus = lazy (constr_of_ref "num.Z.sub") +let coq_Zopp = lazy (constr_of_ref "num.Z.opp") +let coq_Zmult = lazy (constr_of_ref "num.Z.mul") +let coq_Zpower = lazy (constr_of_ref "num.Z.pow") +let coq_Qle = lazy (constr_of_ref "rat.Q.Qle") +let coq_Qlt = lazy (constr_of_ref "rat.Q.Qlt") +let coq_Qeq = lazy (constr_of_ref "rat.Q.Qeq") +let coq_Qplus = lazy (constr_of_ref "rat.Q.Qplus") +let coq_Qminus = lazy (constr_of_ref "rat.Q.Qminus") +let coq_Qopp = lazy (constr_of_ref "rat.Q.Qopp") +let coq_Qmult = lazy (constr_of_ref "rat.Q.Qmult") +let coq_Qpower = lazy (constr_of_ref "rat.Q.Qpower") +let coq_Rgt = lazy (constr_of_ref "reals.R.Rgt") +let coq_Rge = lazy (constr_of_ref "reals.R.Rge") +let coq_Rle = lazy (constr_of_ref "reals.R.Rle") +let coq_Rlt = lazy (constr_of_ref "reals.R.Rlt") +let coq_Rplus = lazy (constr_of_ref "reals.R.Rplus") +let coq_Rminus = lazy (constr_of_ref "reals.R.Rminus") +let coq_Ropp = lazy (constr_of_ref "reals.R.Ropp") +let coq_Rmult = lazy (constr_of_ref "reals.R.Rmult") +let coq_Rinv = lazy (constr_of_ref "reals.R.Rinv") +let coq_Rpower = lazy (constr_of_ref "reals.R.pow") +let coq_powerZR = lazy (constr_of_ref "reals.R.powerRZ") +let coq_IZR = lazy (constr_of_ref "reals.R.IZR") +let coq_IQR = lazy (constr_of_ref "reals.R.Q2R") +let coq_PEX = lazy (constr_of_ref "micromega.PExpr.PEX") +let coq_PEc = lazy (constr_of_ref "micromega.PExpr.PEc") +let coq_PEadd = lazy (constr_of_ref "micromega.PExpr.PEadd") +let coq_PEopp = lazy (constr_of_ref "micromega.PExpr.PEopp") +let coq_PEmul = lazy (constr_of_ref "micromega.PExpr.PEmul") +let coq_PEsub = lazy (constr_of_ref "micromega.PExpr.PEsub") +let coq_PEpow = lazy (constr_of_ref "micromega.PExpr.PEpow") +let coq_PX = lazy (constr_of_ref "micromega.Pol.PX") +let coq_Pc = lazy (constr_of_ref "micromega.Pol.Pc") +let coq_Pinj = lazy (constr_of_ref "micromega.Pol.Pinj") +let coq_OpEq = lazy (constr_of_ref "micromega.Op2.OpEq") +let coq_OpNEq = lazy (constr_of_ref "micromega.Op2.OpNEq") +let coq_OpLe = lazy (constr_of_ref "micromega.Op2.OpLe") +let coq_OpLt = lazy (constr_of_ref "micromega.Op2.OpLt") +let coq_OpGe = lazy (constr_of_ref "micromega.Op2.OpGe") +let coq_OpGt = lazy (constr_of_ref "micromega.Op2.OpGt") +let coq_PsatzIn = lazy (constr_of_ref "micromega.Psatz.PsatzIn") +let coq_PsatzSquare = lazy (constr_of_ref "micromega.Psatz.PsatzSquare") +let coq_PsatzMulE = lazy (constr_of_ref "micromega.Psatz.PsatzMulE") +let coq_PsatzMultC = lazy (constr_of_ref "micromega.Psatz.PsatzMulC") +let coq_PsatzAdd = lazy (constr_of_ref "micromega.Psatz.PsatzAdd") +let coq_PsatzC = lazy (constr_of_ref "micromega.Psatz.PsatzC") +let coq_PsatzZ = lazy (constr_of_ref "micromega.Psatz.PsatzZ") + +(* let coq_GT = lazy (m_constant "GT")*) + +let coq_DeclaredConstant = + lazy (constr_of_ref "micromega.DeclaredConstant.type") + +let coq_TT = lazy (constr_of_ref "micromega.GFormula.TT") +let coq_FF = lazy (constr_of_ref "micromega.GFormula.FF") +let coq_AND = lazy (constr_of_ref "micromega.GFormula.AND") +let coq_OR = lazy (constr_of_ref "micromega.GFormula.OR") +let coq_NOT = lazy (constr_of_ref "micromega.GFormula.NOT") +let coq_Atom = lazy (constr_of_ref "micromega.GFormula.A") +let coq_X = lazy (constr_of_ref "micromega.GFormula.X") +let coq_IMPL = lazy (constr_of_ref "micromega.GFormula.IMPL") +let coq_IFF = lazy (constr_of_ref "micromega.GFormula.IFF") +let coq_EQ = lazy (constr_of_ref "micromega.GFormula.EQ") +let coq_Formula = lazy (constr_of_ref "micromega.BFormula.type") +let coq_eKind = lazy (constr_of_ref "micromega.eKind") + +(** * Initialization : a few Caml symbols are derived from other libraries; * QMicromega, ZArithRing, RingMicromega. *) - let coq_QWitness = lazy (constr_of_ref "micromega.QWitness.type") - let coq_Build = lazy (constr_of_ref "micromega.Formula.Build_Formula") - let coq_Cstr = lazy (constr_of_ref "micromega.Formula.type") +let coq_QWitness = lazy (constr_of_ref "micromega.QWitness.type") +let coq_Build = lazy (constr_of_ref "micromega.Formula.Build_Formula") +let coq_Cstr = lazy (constr_of_ref "micromega.Formula.type") - (** +(** * Parsing and dumping : transformation functions between Caml and Coq * data-structures. * @@ -302,1048 +297,1018 @@ module M = struct * pp_* functions pretty-print Coq terms. *) - exception ParseError +exception ParseError - (* A simple but useful getter function *) +(* A simple but useful getter function *) - let get_left_construct sigma term = - match EConstr.kind sigma term with - | Construct ((_, i), _) -> (i, [||]) - | App (l, rst) -> ( - match EConstr.kind sigma l with - | Construct ((_, i), _) -> (i, rst) - | _ -> raise ParseError ) - | _ -> raise ParseError +let get_left_construct sigma term = + match EConstr.kind sigma term with + | Construct ((_, i), _) -> (i, [||]) + | App (l, rst) -> ( + match EConstr.kind sigma l with + | Construct ((_, i), _) -> (i, rst) + | _ -> raise ParseError ) + | _ -> raise ParseError - (* Access the Micromega module *) +(* Access the Micromega module *) - (* parse/dump/print from numbers up to expressions and formulas *) +(* parse/dump/print from numbers up to expressions and formulas *) - let rec parse_nat sigma term = - let i, c = get_left_construct sigma term in - match i with - | 1 -> Mc.O - | 2 -> Mc.S (parse_nat sigma c.(0)) - | i -> raise ParseError +let rec parse_nat sigma term = + let i, c = get_left_construct sigma term in + match i with + | 1 -> Mc.O + | 2 -> Mc.S (parse_nat sigma c.(0)) + | i -> raise ParseError - let pp_nat o n = Printf.fprintf o "%i" (CoqToCaml.nat n) +let pp_nat o n = Printf.fprintf o "%i" (CoqToCaml.nat n) - let rec dump_nat x = - match x with - | Mc.O -> Lazy.force coq_O - | Mc.S p -> EConstr.mkApp (Lazy.force coq_S, [|dump_nat p|]) +let rec dump_nat x = + match x with + | Mc.O -> Lazy.force coq_O + | Mc.S p -> EConstr.mkApp (Lazy.force coq_S, [|dump_nat p|]) - let rec parse_positive sigma term = - let i, c = get_left_construct sigma term in - match i with - | 1 -> Mc.XI (parse_positive sigma c.(0)) - | 2 -> Mc.XO (parse_positive sigma c.(0)) - | 3 -> Mc.XH - | i -> raise ParseError +let rec parse_positive sigma term = + let i, c = get_left_construct sigma term in + match i with + | 1 -> Mc.XI (parse_positive sigma c.(0)) + | 2 -> Mc.XO (parse_positive sigma c.(0)) + | 3 -> Mc.XH + | i -> raise ParseError - let rec dump_positive x = - match x with - | Mc.XH -> Lazy.force coq_xH - | Mc.XO p -> EConstr.mkApp (Lazy.force coq_xO, [|dump_positive p|]) - | Mc.XI p -> EConstr.mkApp (Lazy.force coq_xI, [|dump_positive p|]) +let rec dump_positive x = + match x with + | Mc.XH -> Lazy.force coq_xH + | Mc.XO p -> EConstr.mkApp (Lazy.force coq_xO, [|dump_positive p|]) + | Mc.XI p -> EConstr.mkApp (Lazy.force coq_xI, [|dump_positive p|]) - let pp_positive o x = Printf.fprintf o "%i" (CoqToCaml.positive x) +let pp_positive o x = Printf.fprintf o "%i" (CoqToCaml.positive x) - let dump_n x = - match x with - | Mc.N0 -> Lazy.force coq_N0 - | Mc.Npos p -> EConstr.mkApp (Lazy.force coq_Npos, [|dump_positive p|]) +let dump_n x = + match x with + | Mc.N0 -> Lazy.force coq_N0 + | Mc.Npos p -> EConstr.mkApp (Lazy.force coq_Npos, [|dump_positive p|]) - (** [is_ground_term env sigma term] holds if the term [term] +(** [is_ground_term env sigma term] holds if the term [term] is an instance of the typeclass [DeclConstant.GT term] i.e. built from user-defined constants and functions. NB: This mechanism can be used to customise the reification process to decide what to consider as a constant (see [parse_constant]) *) - let is_declared_term env evd t = - match EConstr.kind evd t with - | Const _ | Construct _ -> ( - (* Restrict typeclass resolution to trivial cases *) - let typ = Retyping.get_type_of env evd t in - try - ignore - (Typeclasses.resolve_one_typeclass env evd - (EConstr.mkApp (Lazy.force coq_DeclaredConstant, [|typ; t|]))); - true - with Not_found -> false ) - | _ -> false - - let rec is_ground_term env evd term = - match EConstr.kind evd term with - | App (c, args) -> - is_declared_term env evd c && Array.for_all (is_ground_term env evd) args - | Const _ | Construct _ -> is_declared_term env evd term - | _ -> false - - let parse_z sigma term = - let i, c = get_left_construct sigma term in - match i with - | 1 -> Mc.Z0 - | 2 -> Mc.Zpos (parse_positive sigma c.(0)) - | 3 -> Mc.Zneg (parse_positive sigma c.(0)) - | i -> raise ParseError - - let dump_z x = - match x with - | Mc.Z0 -> Lazy.force coq_ZERO - | Mc.Zpos p -> EConstr.mkApp (Lazy.force coq_POS, [|dump_positive p|]) - | Mc.Zneg p -> EConstr.mkApp (Lazy.force coq_NEG, [|dump_positive p|]) - - let pp_z o x = - Printf.fprintf o "%s" (NumCompat.Z.to_string (CoqToCaml.z_big_int x)) - - let dump_q q = +let is_declared_term env evd t = + match EConstr.kind evd t with + | Const _ | Construct _ -> ( + (* Restrict typeclass resolution to trivial cases *) + let typ = Retyping.get_type_of env evd t in + try + ignore + (Typeclasses.resolve_one_typeclass env evd + (EConstr.mkApp (Lazy.force coq_DeclaredConstant, [|typ; t|]))); + true + with Not_found -> false ) + | _ -> false + +let rec is_ground_term env evd term = + match EConstr.kind evd term with + | App (c, args) -> + is_declared_term env evd c && Array.for_all (is_ground_term env evd) args + | Const _ | Construct _ -> is_declared_term env evd term + | _ -> false + +let parse_z sigma term = + let i, c = get_left_construct sigma term in + match i with + | 1 -> Mc.Z0 + | 2 -> Mc.Zpos (parse_positive sigma c.(0)) + | 3 -> Mc.Zneg (parse_positive sigma c.(0)) + | i -> raise ParseError + +let dump_z x = + match x with + | Mc.Z0 -> Lazy.force coq_ZERO + | Mc.Zpos p -> EConstr.mkApp (Lazy.force coq_POS, [|dump_positive p|]) + | Mc.Zneg p -> EConstr.mkApp (Lazy.force coq_NEG, [|dump_positive p|]) + +let pp_z o x = + Printf.fprintf o "%s" (NumCompat.Z.to_string (CoqToCaml.z_big_int x)) + +let dump_q q = + EConstr.mkApp + ( Lazy.force coq_Qmake + , [|dump_z q.Micromega.qnum; dump_positive q.Micromega.qden|] ) + +let parse_q sigma term = + match EConstr.kind sigma term with + | App (c, args) -> + if EConstr.eq_constr sigma c (Lazy.force coq_Qmake) then + {Mc.qnum = parse_z sigma args.(0); Mc.qden = parse_positive sigma args.(1)} + else raise ParseError + | _ -> raise ParseError + +let rec pp_Rcst o cst = + match cst with + | Mc.C0 -> output_string o "C0" + | Mc.C1 -> output_string o "C1" + | Mc.CQ q -> output_string o "CQ _" + | Mc.CZ z -> pp_z o z + | Mc.CPlus (x, y) -> Printf.fprintf o "(%a + %a)" pp_Rcst x pp_Rcst y + | Mc.CMinus (x, y) -> Printf.fprintf o "(%a - %a)" pp_Rcst x pp_Rcst y + | Mc.CMult (x, y) -> Printf.fprintf o "(%a * %a)" pp_Rcst x pp_Rcst y + | Mc.CPow (x, y) -> Printf.fprintf o "(%a ^ _)" pp_Rcst x + | Mc.CInv t -> Printf.fprintf o "(/ %a)" pp_Rcst t + | Mc.COpp t -> Printf.fprintf o "(- %a)" pp_Rcst t + +let rec dump_Rcst cst = + match cst with + | Mc.C0 -> Lazy.force coq_C0 + | Mc.C1 -> Lazy.force coq_C1 + | Mc.CQ q -> EConstr.mkApp (Lazy.force coq_CQ, [|dump_q q|]) + | Mc.CZ z -> EConstr.mkApp (Lazy.force coq_CZ, [|dump_z z|]) + | Mc.CPlus (x, y) -> + EConstr.mkApp (Lazy.force coq_CPlus, [|dump_Rcst x; dump_Rcst y|]) + | Mc.CMinus (x, y) -> + EConstr.mkApp (Lazy.force coq_CMinus, [|dump_Rcst x; dump_Rcst y|]) + | Mc.CMult (x, y) -> + EConstr.mkApp (Lazy.force coq_CMult, [|dump_Rcst x; dump_Rcst y|]) + | Mc.CPow (x, y) -> EConstr.mkApp - ( Lazy.force coq_Qmake - , [|dump_z q.Micromega.qnum; dump_positive q.Micromega.qden|] ) - - let parse_q sigma term = - match EConstr.kind sigma term with - | App (c, args) -> - if EConstr.eq_constr sigma c (Lazy.force coq_Qmake) then - { Mc.qnum = parse_z sigma args.(0) - ; Mc.qden = parse_positive sigma args.(1) } - else raise ParseError - | _ -> raise ParseError + ( Lazy.force coq_CPow + , [| dump_Rcst x + ; ( match y with + | Mc.Inl z -> + EConstr.mkApp + ( Lazy.force coq_Inl + , [|Lazy.force coq_Z; Lazy.force coq_nat; dump_z z|] ) + | Mc.Inr n -> + EConstr.mkApp + ( Lazy.force coq_Inr + , [|Lazy.force coq_Z; Lazy.force coq_nat; dump_nat n|] ) ) |] ) + | Mc.CInv t -> EConstr.mkApp (Lazy.force coq_CInv, [|dump_Rcst t|]) + | Mc.COpp t -> EConstr.mkApp (Lazy.force coq_COpp, [|dump_Rcst t|]) + +let rec dump_list typ dump_elt l = + match l with + | [] -> EConstr.mkApp (Lazy.force coq_nil, [|typ|]) + | e :: l -> + EConstr.mkApp + (Lazy.force coq_cons, [|typ; dump_elt e; dump_list typ dump_elt l|]) - let rec pp_Rcst o cst = - match cst with - | Mc.C0 -> output_string o "C0" - | Mc.C1 -> output_string o "C1" - | Mc.CQ q -> output_string o "CQ _" - | Mc.CZ z -> pp_z o z - | Mc.CPlus (x, y) -> Printf.fprintf o "(%a + %a)" pp_Rcst x pp_Rcst y - | Mc.CMinus (x, y) -> Printf.fprintf o "(%a - %a)" pp_Rcst x pp_Rcst y - | Mc.CMult (x, y) -> Printf.fprintf o "(%a * %a)" pp_Rcst x pp_Rcst y - | Mc.CPow (x, y) -> Printf.fprintf o "(%a ^ _)" pp_Rcst x - | Mc.CInv t -> Printf.fprintf o "(/ %a)" pp_Rcst t - | Mc.COpp t -> Printf.fprintf o "(- %a)" pp_Rcst t - - let rec dump_Rcst cst = - match cst with - | Mc.C0 -> Lazy.force coq_C0 - | Mc.C1 -> Lazy.force coq_C1 - | Mc.CQ q -> EConstr.mkApp (Lazy.force coq_CQ, [|dump_q q|]) - | Mc.CZ z -> EConstr.mkApp (Lazy.force coq_CZ, [|dump_z z|]) - | Mc.CPlus (x, y) -> - EConstr.mkApp (Lazy.force coq_CPlus, [|dump_Rcst x; dump_Rcst y|]) - | Mc.CMinus (x, y) -> - EConstr.mkApp (Lazy.force coq_CMinus, [|dump_Rcst x; dump_Rcst y|]) - | Mc.CMult (x, y) -> - EConstr.mkApp (Lazy.force coq_CMult, [|dump_Rcst x; dump_Rcst y|]) - | Mc.CPow (x, y) -> - EConstr.mkApp - ( Lazy.force coq_CPow - , [| dump_Rcst x - ; ( match y with - | Mc.Inl z -> - EConstr.mkApp - ( Lazy.force coq_Inl - , [|Lazy.force coq_Z; Lazy.force coq_nat; dump_z z|] ) - | Mc.Inr n -> - EConstr.mkApp - ( Lazy.force coq_Inr - , [|Lazy.force coq_Z; Lazy.force coq_nat; dump_nat n|] ) ) |] - ) - | Mc.CInv t -> EConstr.mkApp (Lazy.force coq_CInv, [|dump_Rcst t|]) - | Mc.COpp t -> EConstr.mkApp (Lazy.force coq_COpp, [|dump_Rcst t|]) - - let rec dump_list typ dump_elt l = +let pp_list op cl elt o l = + let rec _pp o l = match l with - | [] -> EConstr.mkApp (Lazy.force coq_nil, [|typ|]) - | e :: l -> - EConstr.mkApp - (Lazy.force coq_cons, [|typ; dump_elt e; dump_list typ dump_elt l|]) - - let pp_list op cl elt o l = - let rec _pp o l = - match l with - | [] -> () - | [e] -> Printf.fprintf o "%a" elt e - | e :: l -> Printf.fprintf o "%a ,%a" elt e _pp l - in - Printf.fprintf o "%s%a%s" op _pp l cl + | [] -> () + | [e] -> Printf.fprintf o "%a" elt e + | e :: l -> Printf.fprintf o "%a ,%a" elt e _pp l + in + Printf.fprintf o "%s%a%s" op _pp l cl - let dump_var = dump_positive +let dump_var = dump_positive - let dump_expr typ dump_z e = - let rec dump_expr e = - match e with - | Mc.PEX n -> EConstr.mkApp (Lazy.force coq_PEX, [|typ; dump_var n|]) - | Mc.PEc z -> EConstr.mkApp (Lazy.force coq_PEc, [|typ; dump_z z|]) - | Mc.PEadd (e1, e2) -> - EConstr.mkApp (Lazy.force coq_PEadd, [|typ; dump_expr e1; dump_expr e2|]) - | Mc.PEsub (e1, e2) -> - EConstr.mkApp (Lazy.force coq_PEsub, [|typ; dump_expr e1; dump_expr e2|]) - | Mc.PEopp e -> EConstr.mkApp (Lazy.force coq_PEopp, [|typ; dump_expr e|]) - | Mc.PEmul (e1, e2) -> - EConstr.mkApp (Lazy.force coq_PEmul, [|typ; dump_expr e1; dump_expr e2|]) - | Mc.PEpow (e, n) -> - EConstr.mkApp (Lazy.force coq_PEpow, [|typ; dump_expr e; dump_n n|]) - in - dump_expr e +let dump_expr typ dump_z e = + let rec dump_expr e = + match e with + | Mc.PEX n -> EConstr.mkApp (Lazy.force coq_PEX, [|typ; dump_var n|]) + | Mc.PEc z -> EConstr.mkApp (Lazy.force coq_PEc, [|typ; dump_z z|]) + | Mc.PEadd (e1, e2) -> + EConstr.mkApp (Lazy.force coq_PEadd, [|typ; dump_expr e1; dump_expr e2|]) + | Mc.PEsub (e1, e2) -> + EConstr.mkApp (Lazy.force coq_PEsub, [|typ; dump_expr e1; dump_expr e2|]) + | Mc.PEopp e -> EConstr.mkApp (Lazy.force coq_PEopp, [|typ; dump_expr e|]) + | Mc.PEmul (e1, e2) -> + EConstr.mkApp (Lazy.force coq_PEmul, [|typ; dump_expr e1; dump_expr e2|]) + | Mc.PEpow (e, n) -> + EConstr.mkApp (Lazy.force coq_PEpow, [|typ; dump_expr e; dump_n n|]) + in + dump_expr e - let dump_pol typ dump_c e = - let rec dump_pol e = - match e with - | Mc.Pc n -> EConstr.mkApp (Lazy.force coq_Pc, [|typ; dump_c n|]) - | Mc.Pinj (p, pol) -> - EConstr.mkApp - (Lazy.force coq_Pinj, [|typ; dump_positive p; dump_pol pol|]) - | Mc.PX (pol1, p, pol2) -> - EConstr.mkApp - ( Lazy.force coq_PX - , [|typ; dump_pol pol1; dump_positive p; dump_pol pol2|] ) - in - dump_pol e - - let pp_pol pp_c o e = - let rec pp_pol o e = - match e with - | Mc.Pc n -> Printf.fprintf o "Pc %a" pp_c n - | Mc.Pinj (p, pol) -> - Printf.fprintf o "Pinj(%a,%a)" pp_positive p pp_pol pol - | Mc.PX (pol1, p, pol2) -> - Printf.fprintf o "PX(%a,%a,%a)" pp_pol pol1 pp_positive p pp_pol pol2 - in - pp_pol o e - - (* let pp_clause pp_c o (f: 'cst clause) = - List.iter (fun ((p,_),(t,_)) -> Printf.fprintf o "(%a @%a)" (pp_pol pp_c) p Tag.pp t) f *) - - let pp_clause_tag o (f : 'cst clause) = - List.iter (fun ((p, _), (t, _)) -> Printf.fprintf o "(_ @%a)" Tag.pp t) f - - (* let pp_cnf pp_c o (f:'cst cnf) = - List.iter (fun l -> Printf.fprintf o "[%a]" (pp_clause pp_c) l) f *) - - let pp_cnf_tag o (f : 'cst cnf) = - List.iter (fun l -> Printf.fprintf o "[%a]" pp_clause_tag l) f - - let dump_psatz typ dump_z e = - let z = Lazy.force typ in - let rec dump_cone e = - match e with - | Mc.PsatzIn n -> EConstr.mkApp (Lazy.force coq_PsatzIn, [|z; dump_nat n|]) - | Mc.PsatzMulC (e, c) -> - EConstr.mkApp - (Lazy.force coq_PsatzMultC, [|z; dump_pol z dump_z e; dump_cone c|]) - | Mc.PsatzSquare e -> - EConstr.mkApp (Lazy.force coq_PsatzSquare, [|z; dump_pol z dump_z e|]) - | Mc.PsatzAdd (e1, e2) -> - EConstr.mkApp - (Lazy.force coq_PsatzAdd, [|z; dump_cone e1; dump_cone e2|]) - | Mc.PsatzMulE (e1, e2) -> - EConstr.mkApp - (Lazy.force coq_PsatzMulE, [|z; dump_cone e1; dump_cone e2|]) - | Mc.PsatzC p -> EConstr.mkApp (Lazy.force coq_PsatzC, [|z; dump_z p|]) - | Mc.PsatzZ -> EConstr.mkApp (Lazy.force coq_PsatzZ, [|z|]) - in - dump_cone e - - let pp_psatz pp_z o e = - let rec pp_cone o e = - match e with - | Mc.PsatzIn n -> Printf.fprintf o "(In %a)%%nat" pp_nat n - | Mc.PsatzMulC (e, c) -> - Printf.fprintf o "( %a [*] %a)" (pp_pol pp_z) e pp_cone c - | Mc.PsatzSquare e -> Printf.fprintf o "(%a^2)" (pp_pol pp_z) e - | Mc.PsatzAdd (e1, e2) -> - Printf.fprintf o "(%a [+] %a)" pp_cone e1 pp_cone e2 - | Mc.PsatzMulE (e1, e2) -> - Printf.fprintf o "(%a [*] %a)" pp_cone e1 pp_cone e2 - | Mc.PsatzC p -> Printf.fprintf o "(%a)%%positive" pp_z p - | Mc.PsatzZ -> Printf.fprintf o "0" - in - pp_cone o e +let dump_pol typ dump_c e = + let rec dump_pol e = + match e with + | Mc.Pc n -> EConstr.mkApp (Lazy.force coq_Pc, [|typ; dump_c n|]) + | Mc.Pinj (p, pol) -> + EConstr.mkApp (Lazy.force coq_Pinj, [|typ; dump_positive p; dump_pol pol|]) + | Mc.PX (pol1, p, pol2) -> + EConstr.mkApp + ( Lazy.force coq_PX + , [|typ; dump_pol pol1; dump_positive p; dump_pol pol2|] ) + in + dump_pol e - let dump_op = function - | Mc.OpEq -> Lazy.force coq_OpEq - | Mc.OpNEq -> Lazy.force coq_OpNEq - | Mc.OpLe -> Lazy.force coq_OpLe - | Mc.OpGe -> Lazy.force coq_OpGe - | Mc.OpGt -> Lazy.force coq_OpGt - | Mc.OpLt -> Lazy.force coq_OpLt +let pp_pol pp_c o e = + let rec pp_pol o e = + match e with + | Mc.Pc n -> Printf.fprintf o "Pc %a" pp_c n + | Mc.Pinj (p, pol) -> + Printf.fprintf o "Pinj(%a,%a)" pp_positive p pp_pol pol + | Mc.PX (pol1, p, pol2) -> + Printf.fprintf o "PX(%a,%a,%a)" pp_pol pol1 pp_positive p pp_pol pol2 + in + pp_pol o e - let dump_cstr typ dump_constant {Mc.flhs = e1; Mc.fop = o; Mc.frhs = e2} = - EConstr.mkApp - ( Lazy.force coq_Build - , [| typ - ; dump_expr typ dump_constant e1 - ; dump_op o - ; dump_expr typ dump_constant e2 |] ) +(* let pp_clause pp_c o (f: 'cst clause) = + List.iter (fun ((p,_),(t,_)) -> Printf.fprintf o "(%a @%a)" (pp_pol pp_c) p Tag.pp t) f *) - let assoc_const sigma x l = - try - snd - (List.find (fun (x', y) -> EConstr.eq_constr sigma x (Lazy.force x')) l) - with Not_found -> raise ParseError - - let zop_table_prop = - [ (coq_Zgt, Mc.OpGt) - ; (coq_Zge, Mc.OpGe) - ; (coq_Zlt, Mc.OpLt) - ; (coq_Zle, Mc.OpLe) ] - - let zop_table_bool = - [ (coq_Zgtb, Mc.OpGt) - ; (coq_Zgeb, Mc.OpGe) - ; (coq_Zltb, Mc.OpLt) - ; (coq_Zleb, Mc.OpLe) - ; (coq_Zeqb, Mc.OpEq) ] - - let rop_table_prop = - [ (coq_Rgt, Mc.OpGt) - ; (coq_Rge, Mc.OpGe) - ; (coq_Rlt, Mc.OpLt) - ; (coq_Rle, Mc.OpLe) ] - - let rop_table_bool = [] - - let qop_table_prop = - [(coq_Qlt, Mc.OpLt); (coq_Qle, Mc.OpLe); (coq_Qeq, Mc.OpEq)] - - let qop_table_bool = [] - - type gl = {env : Environ.env; sigma : Evd.evar_map} - - let is_convertible gl t1 t2 = Reductionops.is_conv gl.env gl.sigma t1 t2 - - let parse_operator table_prop table_bool has_equality typ gl k (op, args) = - let sigma = gl.sigma in - match args with - | [|a1; a2|] -> - ( assoc_const sigma op - (match k with Mc.IsProp -> table_prop | Mc.IsBool -> table_bool) - , a1 - , a2 ) - | [|ty; a1; a2|] -> - if - has_equality - && EConstr.eq_constr sigma op (Lazy.force coq_eq) - && is_convertible gl ty (Lazy.force typ) - then (Mc.OpEq, args.(1), args.(2)) - else raise ParseError - | _ -> raise ParseError +let pp_clause_tag o (f : 'cst clause) = + List.iter (fun ((p, _), (t, _)) -> Printf.fprintf o "(_ @%a)" Tag.pp t) f - let parse_zop = parse_operator zop_table_prop zop_table_bool true coq_Z - let parse_rop = parse_operator rop_table_prop [] true coq_R - let parse_qop = parse_operator qop_table_prop [] false coq_R +(* let pp_cnf pp_c o (f:'cst cnf) = + List.iter (fun l -> Printf.fprintf o "[%a]" (pp_clause pp_c) l) f *) - type 'a op = - | Binop of ('a Mc.pExpr -> 'a Mc.pExpr -> 'a Mc.pExpr) - | Opp - | Power - | Ukn of string +let pp_cnf_tag o (f : 'cst cnf) = + List.iter (fun l -> Printf.fprintf o "[%a]" pp_clause_tag l) f - let assoc_ops sigma x l = - try - snd - (List.find (fun (x', y) -> EConstr.eq_constr sigma x (Lazy.force x')) l) - with Not_found -> Ukn "Oups" +let dump_psatz typ dump_z e = + let z = Lazy.force typ in + let rec dump_cone e = + match e with + | Mc.PsatzIn n -> EConstr.mkApp (Lazy.force coq_PsatzIn, [|z; dump_nat n|]) + | Mc.PsatzMulC (e, c) -> + EConstr.mkApp + (Lazy.force coq_PsatzMultC, [|z; dump_pol z dump_z e; dump_cone c|]) + | Mc.PsatzSquare e -> + EConstr.mkApp (Lazy.force coq_PsatzSquare, [|z; dump_pol z dump_z e|]) + | Mc.PsatzAdd (e1, e2) -> + EConstr.mkApp (Lazy.force coq_PsatzAdd, [|z; dump_cone e1; dump_cone e2|]) + | Mc.PsatzMulE (e1, e2) -> + EConstr.mkApp (Lazy.force coq_PsatzMulE, [|z; dump_cone e1; dump_cone e2|]) + | Mc.PsatzC p -> EConstr.mkApp (Lazy.force coq_PsatzC, [|z; dump_z p|]) + | Mc.PsatzZ -> EConstr.mkApp (Lazy.force coq_PsatzZ, [|z|]) + in + dump_cone e - (** +let pp_psatz pp_z o e = + let rec pp_cone o e = + match e with + | Mc.PsatzIn n -> Printf.fprintf o "(In %a)%%nat" pp_nat n + | Mc.PsatzMulC (e, c) -> + Printf.fprintf o "( %a [*] %a)" (pp_pol pp_z) e pp_cone c + | Mc.PsatzSquare e -> Printf.fprintf o "(%a^2)" (pp_pol pp_z) e + | Mc.PsatzAdd (e1, e2) -> + Printf.fprintf o "(%a [+] %a)" pp_cone e1 pp_cone e2 + | Mc.PsatzMulE (e1, e2) -> + Printf.fprintf o "(%a [*] %a)" pp_cone e1 pp_cone e2 + | Mc.PsatzC p -> Printf.fprintf o "(%a)%%positive" pp_z p + | Mc.PsatzZ -> Printf.fprintf o "0" + in + pp_cone o e + +let dump_op = function + | Mc.OpEq -> Lazy.force coq_OpEq + | Mc.OpNEq -> Lazy.force coq_OpNEq + | Mc.OpLe -> Lazy.force coq_OpLe + | Mc.OpGe -> Lazy.force coq_OpGe + | Mc.OpGt -> Lazy.force coq_OpGt + | Mc.OpLt -> Lazy.force coq_OpLt + +let dump_cstr typ dump_constant {Mc.flhs = e1; Mc.fop = o; Mc.frhs = e2} = + EConstr.mkApp + ( Lazy.force coq_Build + , [| typ + ; dump_expr typ dump_constant e1 + ; dump_op o + ; dump_expr typ dump_constant e2 |] ) + +let assoc_const sigma x l = + try + snd (List.find (fun (x', y) -> EConstr.eq_constr sigma x (Lazy.force x')) l) + with Not_found -> raise ParseError + +let zop_table_prop = + [ (coq_Zgt, Mc.OpGt) + ; (coq_Zge, Mc.OpGe) + ; (coq_Zlt, Mc.OpLt) + ; (coq_Zle, Mc.OpLe) ] + +let zop_table_bool = + [ (coq_Zgtb, Mc.OpGt) + ; (coq_Zgeb, Mc.OpGe) + ; (coq_Zltb, Mc.OpLt) + ; (coq_Zleb, Mc.OpLe) + ; (coq_Zeqb, Mc.OpEq) ] + +let rop_table_prop = + [ (coq_Rgt, Mc.OpGt) + ; (coq_Rge, Mc.OpGe) + ; (coq_Rlt, Mc.OpLt) + ; (coq_Rle, Mc.OpLe) ] + +let rop_table_bool = [] +let qop_table_prop = [(coq_Qlt, Mc.OpLt); (coq_Qle, Mc.OpLe); (coq_Qeq, Mc.OpEq)] +let qop_table_bool = [] + +type gl = Environ.env * Evd.evar_map + +let is_convertible env sigma t1 t2 = Reductionops.is_conv env sigma t1 t2 + +let parse_operator table_prop table_bool has_equality typ (env, sigma) k + (op, args) = + match args with + | [|a1; a2|] -> + ( assoc_const sigma op + (match k with Mc.IsProp -> table_prop | Mc.IsBool -> table_bool) + , a1 + , a2 ) + | [|ty; a1; a2|] -> + if + has_equality + && EConstr.eq_constr sigma op (Lazy.force coq_eq) + && is_convertible env sigma ty (Lazy.force typ) + then (Mc.OpEq, args.(1), args.(2)) + else raise ParseError + | _ -> raise ParseError + +let parse_zop = parse_operator zop_table_prop zop_table_bool true coq_Z +let parse_rop = parse_operator rop_table_prop [] true coq_R +let parse_qop = parse_operator qop_table_prop [] false coq_R + +type 'a op = + | Binop of ('a Mc.pExpr -> 'a Mc.pExpr -> 'a Mc.pExpr) + | Opp + | Power + | Ukn of string + +let assoc_ops sigma x l = + try + snd (List.find (fun (x', y) -> EConstr.eq_constr sigma x (Lazy.force x')) l) + with Not_found -> Ukn "Oups" + +(** * MODULE: Env is for environment. *) - module Env = struct - type t = - { vars : (EConstr.t * Mc.kind) list - ; (* The list represents a mapping from EConstr.t to indexes. *) - gl : gl - (* The evar_map may be updated due to unification of universes *) } - - let empty gl = {vars = []; gl} - - (** [eq_constr gl x y] returns an updated [gl] if x and y can be unified *) - let eq_constr gl x y = - let evd = gl.sigma in - match EConstr.eq_constr_universes_proj gl.env evd x y with - | Some csts -> ( - let csts = - UnivProblem.to_constraints ~force_weak:false (Evd.universes evd) csts - in - match Evd.add_constraints evd csts with - | evd -> Some {gl with sigma = evd} - | exception Univ.UniverseInconsistency _ -> None ) - | None -> None - - let compute_rank_add env v is_prop = - let rec _add gl vars n v = - match vars with - | [] -> (gl, [(v, is_prop)], n) - | (e, b) :: l -> ( - match eq_constr gl e v with - | Some gl' -> (gl', vars, n) - | None -> - let gl, l', n = _add gl l (n + 1) v in - (gl, (e, b) :: l', n) ) - in - let gl', vars', n = _add env.gl env.vars 1 v in - ({vars = vars'; gl = gl'}, CamlToCoq.positive n) - - let get_rank env v = - let gl = env.gl in - let rec _get_rank env n = - match env with - | [] -> raise (Invalid_argument "get_rank") - | (e, _) :: l -> ( - match eq_constr gl e v with Some _ -> n | None -> _get_rank l (n + 1) - ) - in - _get_rank env.vars 1 - - let elements env = env.vars - - (* let string_of_env gl env = - let rec string_of_env i env acc = - match env with - | [] -> acc - | e::env -> string_of_env (i+1) env - (IMap.add i - (Pp.string_of_ppcmds - (Printer.pr_econstr_env gl.env gl.sigma e)) acc) in - string_of_env 1 env IMap.empty - *) - let pp gl env = - let ppl = - List.mapi - (fun i (e, _) -> - Pp.str "x" - ++ Pp.int (i + 1) - ++ Pp.str ":" - ++ Printer.pr_econstr_env gl.env gl.sigma e) - env +module Env = struct + type t = + { vars : (EConstr.t * Mc.kind) list + ; (* The list represents a mapping from EConstr.t to indexes. *) + gl : gl (* The evar_map may be updated due to unification of universes *) + } + + let empty gl = {vars = []; gl} + + (** [eq_constr gl x y] returns an updated [gl] if x and y can be unified *) + let eq_constr (env, sigma) x y = + match EConstr.eq_constr_universes_proj env sigma x y with + | Some csts -> ( + let csts = + UnivProblem.to_constraints ~force_weak:false (Evd.universes sigma) csts in - List.fold_right (fun e p -> e ++ Pp.str " ; " ++ p) ppl (Pp.str "\n") - end + match Evd.add_constraints sigma csts with + | sigma -> Some (env, sigma) + | exception Univ.UniverseInconsistency _ -> None ) + | None -> None + + let compute_rank_add env v is_prop = + let rec _add gl vars n v = + match vars with + | [] -> (gl, [(v, is_prop)], n) + | (e, b) :: l -> ( + match eq_constr gl e v with + | Some gl' -> (gl', vars, n) + | None -> + let gl, l', n = _add gl l (n + 1) v in + (gl, (e, b) :: l', n) ) + in + let gl', vars', n = _add env.gl env.vars 1 v in + ({vars = vars'; gl = gl'}, CamlToCoq.positive n) + + let get_rank env v = + let gl = env.gl in + let rec _get_rank env n = + match env with + | [] -> raise (Invalid_argument "get_rank") + | (e, _) :: l -> ( + match eq_constr gl e v with Some _ -> n | None -> _get_rank l (n + 1) ) + in + _get_rank env.vars 1 + + let elements env = env.vars + + (* let string_of_env gl env = + let rec string_of_env i env acc = + match env with + | [] -> acc + | e::env -> string_of_env (i+1) env + (IMap.add i + (Pp.string_of_ppcmds + (Printer.pr_econstr_env gl.env gl.sigma e)) acc) in + string_of_env 1 env IMap.empty + *) + let pp (genv, sigma) env = + let ppl = + List.mapi + (fun i (e, _) -> + Pp.str "x" + ++ Pp.int (i + 1) + ++ Pp.str ":" + ++ Printer.pr_econstr_env genv sigma e) + env + in + List.fold_right (fun e p -> e ++ Pp.str " ; " ++ p) ppl (Pp.str "\n") +end - (* MODULE END: Env *) +(* MODULE END: Env *) - (** +(** * This is the big generic function for expression parsers. *) - let parse_expr gl parse_constant parse_exp ops_spec env term = - if debug then - Feedback.msg_debug - (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env gl.env gl.sigma term); - let parse_variable env term = - let env, n = Env.compute_rank_add env term Mc.IsBool in - (Mc.PEX n, env) +let parse_expr (genv, sigma) parse_constant parse_exp ops_spec env term = + if debug then + Feedback.msg_debug + (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env genv sigma term); + let parse_variable env term = + let env, n = Env.compute_rank_add env term Mc.IsBool in + (Mc.PEX n, env) + in + let rec parse_expr env term = + let combine env op (t1, t2) = + let expr1, env = parse_expr env t1 in + let expr2, env = parse_expr env t2 in + (op expr1 expr2, env) in - let rec parse_expr env term = - let combine env op (t1, t2) = - let expr1, env = parse_expr env t1 in - let expr2, env = parse_expr env t2 in - (op expr1 expr2, env) - in - try (Mc.PEc (parse_constant gl term), env) - with ParseError -> ( - match EConstr.kind gl.sigma term with - | App (t, args) -> ( - match EConstr.kind gl.sigma t with - | Const c -> ( - match assoc_ops gl.sigma t ops_spec with - | Binop f -> combine env f (args.(0), args.(1)) - | Opp -> + try (Mc.PEc (parse_constant (genv, sigma) term), env) + with ParseError -> ( + match EConstr.kind sigma term with + | App (t, args) -> ( + match EConstr.kind sigma t with + | Const c -> ( + match assoc_ops sigma t ops_spec with + | Binop f -> combine env f (args.(0), args.(1)) + | Opp -> + let expr, env = parse_expr env args.(0) in + (Mc.PEopp expr, env) + | Power -> ( + try let expr, env = parse_expr env args.(0) in - (Mc.PEopp expr, env) - | Power -> ( - try - let expr, env = parse_expr env args.(0) in - let power = parse_exp expr args.(1) in - (power, env) - with ParseError -> - (* if the exponent is a variable *) - let env, n = Env.compute_rank_add env term Mc.IsBool in - (Mc.PEX n, env) ) - | Ukn s -> - if debug then ( - Printf.printf "unknown op: %s\n" s; - flush stdout ); + let power = parse_exp expr args.(1) in + (power, env) + with ParseError -> + (* if the exponent is a variable *) let env, n = Env.compute_rank_add env term Mc.IsBool in (Mc.PEX n, env) ) - | _ -> parse_variable env term ) + | Ukn s -> + if debug then ( + Printf.printf "unknown op: %s\n" s; + flush stdout ); + let env, n = Env.compute_rank_add env term Mc.IsBool in + (Mc.PEX n, env) ) | _ -> parse_variable env term ) - in - parse_expr env term - - let zop_spec = - [ (coq_Zplus, Binop (fun x y -> Mc.PEadd (x, y))) - ; (coq_Zminus, Binop (fun x y -> Mc.PEsub (x, y))) - ; (coq_Zmult, Binop (fun x y -> Mc.PEmul (x, y))) - ; (coq_Zopp, Opp) - ; (coq_Zpower, Power) ] - - let qop_spec = - [ (coq_Qplus, Binop (fun x y -> Mc.PEadd (x, y))) - ; (coq_Qminus, Binop (fun x y -> Mc.PEsub (x, y))) - ; (coq_Qmult, Binop (fun x y -> Mc.PEmul (x, y))) - ; (coq_Qopp, Opp) - ; (coq_Qpower, Power) ] - - let rop_spec = - [ (coq_Rplus, Binop (fun x y -> Mc.PEadd (x, y))) - ; (coq_Rminus, Binop (fun x y -> Mc.PEsub (x, y))) - ; (coq_Rmult, Binop (fun x y -> Mc.PEmul (x, y))) - ; (coq_Ropp, Opp) - ; (coq_Rpower, Power) ] - - let parse_constant parse gl t = parse gl.sigma t - - (** [parse_more_constant parse gl t] returns the reification of term [t]. + | _ -> parse_variable env term ) + in + parse_expr env term + +let zop_spec = + [ (coq_Zplus, Binop (fun x y -> Mc.PEadd (x, y))) + ; (coq_Zminus, Binop (fun x y -> Mc.PEsub (x, y))) + ; (coq_Zmult, Binop (fun x y -> Mc.PEmul (x, y))) + ; (coq_Zopp, Opp) + ; (coq_Zpower, Power) ] + +let qop_spec = + [ (coq_Qplus, Binop (fun x y -> Mc.PEadd (x, y))) + ; (coq_Qminus, Binop (fun x y -> Mc.PEsub (x, y))) + ; (coq_Qmult, Binop (fun x y -> Mc.PEmul (x, y))) + ; (coq_Qopp, Opp) + ; (coq_Qpower, Power) ] + +let rop_spec = + [ (coq_Rplus, Binop (fun x y -> Mc.PEadd (x, y))) + ; (coq_Rminus, Binop (fun x y -> Mc.PEsub (x, y))) + ; (coq_Rmult, Binop (fun x y -> Mc.PEmul (x, y))) + ; (coq_Ropp, Opp) + ; (coq_Rpower, Power) ] + +let parse_constant parse ((genv : Environ.env), sigma) t = parse sigma t + +(** [parse_more_constant parse gl t] returns the reification of term [t]. If [t] is a ground term, then it is first reduced to normal form before using a 'syntactic' parser *) - let parse_more_constant parse gl t = - try parse gl t - with ParseError -> - if debug then Feedback.msg_debug Pp.(str "try harder"); - if is_ground_term gl.env gl.sigma t then - parse gl (Redexpr.cbv_vm gl.env gl.sigma t) - else raise ParseError - - let zconstant = parse_constant parse_z - let qconstant = parse_constant parse_q - let nconstant = parse_constant parse_nat - - (** [parse_more_zexpr parse_constant gl] improves the parsing of exponent +let parse_more_constant parse (genv, sigma) t = + try parse (genv, sigma) t + with ParseError -> + if debug then Feedback.msg_debug Pp.(str "try harder"); + if is_ground_term genv sigma t then + parse (genv, sigma) (Redexpr.cbv_vm genv sigma t) + else raise ParseError + +let zconstant = parse_constant parse_z +let qconstant = parse_constant parse_q +let nconstant = parse_constant parse_nat + +(** [parse_more_zexpr parse_constant gl] improves the parsing of exponent which can be arithmetic expressions (without variables). [parse_constant_expr] returns a constant if the argument is an expression without variables. *) - let rec parse_zexpr gl = - parse_expr gl zconstant - (fun expr (x : EConstr.t) -> - let z = parse_zconstant gl x in - match z with - | Mc.Zneg _ -> Mc.PEc Mc.Z0 - | _ -> Mc.PEpow (expr, Mc.Z.to_N z)) - zop_spec - - and parse_zconstant gl e = - let e, _ = parse_zexpr gl (Env.empty gl) e in - match Mc.zeval_const e with None -> raise ParseError | Some z -> z - - (* NB: R is a different story. - Because it is axiomatised, reducing would not be effective. - Therefore, there is a specific parser for constant over R - *) +let rec parse_zexpr gl = + parse_expr gl zconstant + (fun expr (x : EConstr.t) -> + let z = parse_zconstant gl x in + match z with + | Mc.Zneg _ -> Mc.PEc Mc.Z0 + | _ -> Mc.PEpow (expr, Mc.Z.to_N z)) + zop_spec + +and parse_zconstant gl e = + let e, _ = parse_zexpr gl (Env.empty gl) e in + match Mc.zeval_const e with None -> raise ParseError | Some z -> z + +(* NB: R is a different story. + Because it is axiomatised, reducing would not be effective. + Therefore, there is a specific parser for constant over R +*) - let rconst_assoc = - [ (coq_Rplus, fun x y -> Mc.CPlus (x, y)) - ; (coq_Rminus, fun x y -> Mc.CMinus (x, y)) - ; (coq_Rmult, fun x y -> Mc.CMult (x, y)) - (* coq_Rdiv , (fun x y -> Mc.CMult(x,Mc.CInv y)) ;*) ] +let rconst_assoc = + [ (coq_Rplus, fun x y -> Mc.CPlus (x, y)) + ; (coq_Rminus, fun x y -> Mc.CMinus (x, y)) + ; (coq_Rmult, fun x y -> Mc.CMult (x, y)) + (* coq_Rdiv , (fun x y -> Mc.CMult(x,Mc.CInv y)) ;*) ] - let rconstant gl term = - let sigma = gl.sigma in - let rec rconstant term = - match EConstr.kind sigma term with - | Const x -> - if EConstr.eq_constr sigma term (Lazy.force coq_R0) then Mc.C0 - else if EConstr.eq_constr sigma term (Lazy.force coq_R1) then Mc.C1 - else raise ParseError - | App (op, args) -> ( - try - (* the evaluation order is important in the following *) - let f = assoc_const sigma op rconst_assoc in - let a = rconstant args.(0) in - let b = rconstant args.(1) in - f a b - with ParseError -> ( - match op with - | op when EConstr.eq_constr sigma op (Lazy.force coq_Rinv) -> - let arg = rconstant args.(0) in - if Mc.qeq_bool (Mc.q_of_Rcst arg) {Mc.qnum = Mc.Z0; Mc.qden = Mc.XH} - then raise ParseError - (* This is a division by zero -- no semantics *) - else Mc.CInv arg - | op when EConstr.eq_constr sigma op (Lazy.force coq_Rpower) -> - Mc.CPow - ( rconstant args.(0) - , Mc.Inr (parse_more_constant nconstant gl args.(1)) ) - | op when EConstr.eq_constr sigma op (Lazy.force coq_IQR) -> - Mc.CQ (qconstant gl args.(0)) - | op when EConstr.eq_constr sigma op (Lazy.force coq_IZR) -> - Mc.CZ (parse_more_constant zconstant gl args.(0)) - | _ -> raise ParseError ) ) - | _ -> raise ParseError - in - rconstant term - - let rconstant gl term = - if debug then - Feedback.msg_debug - ( Pp.str "rconstant: " - ++ Printer.pr_leconstr_env gl.env gl.sigma term - ++ fnl () ); - let res = rconstant gl term in - if debug then ( - Printf.printf "rconstant -> %a\n" pp_Rcst res; - flush stdout ); - res +let rconstant (genv, sigma) term = + let rec rconstant term = + match EConstr.kind sigma term with + | Const x -> + if EConstr.eq_constr sigma term (Lazy.force coq_R0) then Mc.C0 + else if EConstr.eq_constr sigma term (Lazy.force coq_R1) then Mc.C1 + else raise ParseError + | App (op, args) -> ( + try + (* the evaluation order is important in the following *) + let f = assoc_const sigma op rconst_assoc in + let a = rconstant args.(0) in + let b = rconstant args.(1) in + f a b + with ParseError -> ( + match op with + | op when EConstr.eq_constr sigma op (Lazy.force coq_Rinv) -> + let arg = rconstant args.(0) in + if Mc.qeq_bool (Mc.q_of_Rcst arg) {Mc.qnum = Mc.Z0; Mc.qden = Mc.XH} + then raise ParseError (* This is a division by zero -- no semantics *) + else Mc.CInv arg + | op when EConstr.eq_constr sigma op (Lazy.force coq_Rpower) -> + Mc.CPow + ( rconstant args.(0) + , Mc.Inr (parse_more_constant nconstant (genv, sigma) args.(1)) ) + | op when EConstr.eq_constr sigma op (Lazy.force coq_IQR) -> + Mc.CQ (qconstant (genv, sigma) args.(0)) + | op when EConstr.eq_constr sigma op (Lazy.force coq_IZR) -> + Mc.CZ (parse_more_constant zconstant (genv, sigma) args.(0)) + | _ -> raise ParseError ) ) + | _ -> raise ParseError + in + rconstant term + +let rconstant (genv, sigma) term = + if debug then + Feedback.msg_debug + (Pp.str "rconstant: " ++ Printer.pr_leconstr_env genv sigma term ++ fnl ()); + let res = rconstant (genv, sigma) term in + if debug then ( + Printf.printf "rconstant -> %a\n" pp_Rcst res; + flush stdout ); + res - let parse_qexpr gl = - parse_expr gl qconstant - (fun expr x -> - let exp = zconstant gl x in - match exp with - | Mc.Zneg _ -> ( - match expr with - | Mc.PEc q -> Mc.PEc (Mc.qpower q exp) - | _ -> raise ParseError ) - | _ -> - let exp = Mc.Z.to_N exp in - Mc.PEpow (expr, exp)) - qop_spec - - let parse_rexpr gl = - parse_expr gl rconstant - (fun expr x -> - let exp = Mc.N.of_nat (parse_nat gl.sigma x) in +let parse_qexpr gl = + parse_expr gl qconstant + (fun expr x -> + let exp = zconstant gl x in + match exp with + | Mc.Zneg _ -> ( + match expr with + | Mc.PEc q -> Mc.PEc (Mc.qpower q exp) + | _ -> raise ParseError ) + | _ -> + let exp = Mc.Z.to_N exp in Mc.PEpow (expr, exp)) - rop_spec - - let parse_arith parse_op parse_expr (k : Mc.kind) env cstr gl = - let sigma = gl.sigma in - if debug then - Feedback.msg_debug - ( Pp.str "parse_arith: " - ++ Printer.pr_leconstr_env gl.env sigma cstr - ++ fnl () ); - match EConstr.kind sigma cstr with - | App (op, args) -> - let op, lhs, rhs = parse_op gl k (op, args) in - let e1, env = parse_expr gl env lhs in - let e2, env = parse_expr gl env rhs in - ({Mc.flhs = e1; Mc.fop = op; Mc.frhs = e2}, env) - | _ -> failwith "error : parse_arith(2)" - - let parse_zarith = parse_arith parse_zop parse_zexpr - let parse_qarith = parse_arith parse_qop parse_qexpr - let parse_rarith = parse_arith parse_rop parse_rexpr - - (* generic parsing of arithmetic expressions *) - - let mkAND b f1 f2 = Mc.AND (b, f1, f2) - let mkOR b f1 f2 = Mc.OR (b, f1, f2) - let mkIff b f1 f2 = Mc.IFF (b, f1, f2) - let mkIMPL b f1 f2 = Mc.IMPL (b, f1, None, f2) - let mkEQ f1 f2 = Mc.EQ (f1, f2) - - let mkformula_binary b g term f1 f2 = - match (f1, f2) with - | Mc.X (b1, _), Mc.X (b2, _) -> Mc.X (b, term) - | _ -> g f1 f2 + qop_spec + +let parse_rexpr (genv, sigma) = + parse_expr (genv, sigma) rconstant + (fun expr x -> + let exp = Mc.N.of_nat (parse_nat sigma x) in + Mc.PEpow (expr, exp)) + rop_spec + +let parse_arith parse_op parse_expr (k : Mc.kind) env cstr (genv, sigma) = + if debug then + Feedback.msg_debug + ( Pp.str "parse_arith: " + ++ Printer.pr_leconstr_env genv sigma cstr + ++ fnl () ); + match EConstr.kind sigma cstr with + | App (op, args) -> + let op, lhs, rhs = parse_op (genv, sigma) k (op, args) in + let e1, env = parse_expr (genv, sigma) env lhs in + let e2, env = parse_expr (genv, sigma) env rhs in + ({Mc.flhs = e1; Mc.fop = op; Mc.frhs = e2}, env) + | _ -> failwith "error : parse_arith(2)" + +let parse_zarith = parse_arith parse_zop parse_zexpr +let parse_qarith = parse_arith parse_qop parse_qexpr +let parse_rarith = parse_arith parse_rop parse_rexpr + +(* generic parsing of arithmetic expressions *) + +let mkAND b f1 f2 = Mc.AND (b, f1, f2) +let mkOR b f1 f2 = Mc.OR (b, f1, f2) +let mkIff b f1 f2 = Mc.IFF (b, f1, f2) +let mkIMPL b f1 f2 = Mc.IMPL (b, f1, None, f2) +let mkEQ f1 f2 = Mc.EQ (f1, f2) + +let mkformula_binary b g term f1 f2 = + match (f1, f2) with + | Mc.X (b1, _), Mc.X (b2, _) -> Mc.X (b, term) + | _ -> g f1 f2 - (** +(** * This is the big generic function for formula parsers. *) - let is_prop env sigma term = - let sort = Retyping.get_sort_of env sigma term in - Sorts.is_prop sort +let is_prop env sigma term = + let sort = Retyping.get_sort_of env sigma term in + Sorts.is_prop sort - type formula_op = - { op_and : EConstr.t - ; op_or : EConstr.t - ; op_iff : EConstr.t - ; op_not : EConstr.t - ; op_tt : EConstr.t - ; op_ff : EConstr.t } +type formula_op = + { op_and : EConstr.t + ; op_or : EConstr.t + ; op_iff : EConstr.t + ; op_not : EConstr.t + ; op_tt : EConstr.t + ; op_ff : EConstr.t } - let prop_op = - lazy - { op_and = Lazy.force coq_and - ; op_or = Lazy.force coq_or - ; op_iff = Lazy.force coq_iff - ; op_not = Lazy.force coq_not - ; op_tt = Lazy.force coq_True - ; op_ff = Lazy.force coq_False } - - let bool_op = - lazy - { op_and = Lazy.force coq_andb - ; op_or = Lazy.force coq_orb - ; op_iff = Lazy.force coq_eqb - ; op_not = Lazy.force coq_negb - ; op_tt = Lazy.force coq_true - ; op_ff = Lazy.force coq_false } - - let parse_formula gl parse_atom env tg term = - let sigma = gl.sigma in - let parse_atom b env tg t = - try - let at, env = parse_atom b env t gl in - (Mc.A (b, at, (tg, t)), env, Tag.next tg) - with ParseError -> (Mc.X (b, t), env, tg) - in - let prop_op = Lazy.force prop_op in - let bool_op = Lazy.force bool_op in - let eq = Lazy.force coq_eq in - let bool = Lazy.force coq_bool in - let rec xparse_formula op k env tg term = - match EConstr.kind sigma term with - | App (l, rst) -> ( - match rst with - | [|a; b|] when EConstr.eq_constr sigma l op.op_and -> - let f, env, tg = xparse_formula op k env tg a in - let g, env, tg = xparse_formula op k env tg b in - (mkformula_binary k (mkAND k) term f g, env, tg) - | [|a; b|] when EConstr.eq_constr sigma l op.op_or -> - let f, env, tg = xparse_formula op k env tg a in - let g, env, tg = xparse_formula op k env tg b in - (mkformula_binary k (mkOR k) term f g, env, tg) - | [|a; b|] when EConstr.eq_constr sigma l op.op_iff -> - let f, env, tg = xparse_formula op k env tg a in - let g, env, tg = xparse_formula op k env tg b in - (mkformula_binary k (mkIff k) term f g, env, tg) - | [|ty; a; b|] - when EConstr.eq_constr sigma l eq && is_convertible gl ty bool -> - let f, env, tg = xparse_formula bool_op Mc.IsBool env tg a in - let g, env, tg = xparse_formula bool_op Mc.IsBool env tg b in - (mkformula_binary Mc.IsProp mkEQ term f g, env, tg) - | [|a|] when EConstr.eq_constr sigma l op.op_not -> - let f, env, tg = xparse_formula op k env tg a in - (Mc.NOT (k, f), env, tg) - | _ -> parse_atom k env tg term ) - | Prod (typ, a, b) - when kind_is_prop k - && (typ.binder_name = Anonymous || EConstr.Vars.noccurn sigma 1 b) - -> +let prop_op = + lazy + { op_and = Lazy.force coq_and + ; op_or = Lazy.force coq_or + ; op_iff = Lazy.force coq_iff + ; op_not = Lazy.force coq_not + ; op_tt = Lazy.force coq_True + ; op_ff = Lazy.force coq_False } + +let bool_op = + lazy + { op_and = Lazy.force coq_andb + ; op_or = Lazy.force coq_orb + ; op_iff = Lazy.force coq_eqb + ; op_not = Lazy.force coq_negb + ; op_tt = Lazy.force coq_true + ; op_ff = Lazy.force coq_false } + +let parse_formula (genv, sigma) parse_atom env tg term = + let parse_atom b env tg t = + try + let at, env = parse_atom b env t (genv, sigma) in + (Mc.A (b, at, (tg, t)), env, Tag.next tg) + with ParseError -> (Mc.X (b, t), env, tg) + in + let prop_op = Lazy.force prop_op in + let bool_op = Lazy.force bool_op in + let eq = Lazy.force coq_eq in + let bool = Lazy.force coq_bool in + let rec xparse_formula op k env tg term = + match EConstr.kind sigma term with + | App (l, rst) -> ( + match rst with + | [|a; b|] when EConstr.eq_constr sigma l op.op_and -> let f, env, tg = xparse_formula op k env tg a in let g, env, tg = xparse_formula op k env tg b in - (mkformula_binary Mc.IsProp (mkIMPL Mc.IsProp) term f g, env, tg) - | _ -> - if EConstr.eq_constr sigma term op.op_tt then (Mc.TT k, env, tg) - else if EConstr.eq_constr sigma term op.op_ff then Mc.(FF k, env, tg) - else (Mc.X (k, term), env, tg) - in - xparse_formula prop_op Mc.IsProp env tg (*Reductionops.whd_zeta*) term + (mkformula_binary k (mkAND k) term f g, env, tg) + | [|a; b|] when EConstr.eq_constr sigma l op.op_or -> + let f, env, tg = xparse_formula op k env tg a in + let g, env, tg = xparse_formula op k env tg b in + (mkformula_binary k (mkOR k) term f g, env, tg) + | [|a; b|] when EConstr.eq_constr sigma l op.op_iff -> + let f, env, tg = xparse_formula op k env tg a in + let g, env, tg = xparse_formula op k env tg b in + (mkformula_binary k (mkIff k) term f g, env, tg) + | [|ty; a; b|] + when EConstr.eq_constr sigma l eq && is_convertible genv sigma ty bool + -> + let f, env, tg = xparse_formula bool_op Mc.IsBool env tg a in + let g, env, tg = xparse_formula bool_op Mc.IsBool env tg b in + (mkformula_binary Mc.IsProp mkEQ term f g, env, tg) + | [|a|] when EConstr.eq_constr sigma l op.op_not -> + let f, env, tg = xparse_formula op k env tg a in + (Mc.NOT (k, f), env, tg) + | _ -> parse_atom k env tg term ) + | Prod (typ, a, b) + when kind_is_prop k + && (typ.binder_name = Anonymous || EConstr.Vars.noccurn sigma 1 b) -> + let f, env, tg = xparse_formula op k env tg a in + let g, env, tg = xparse_formula op k env tg b in + (mkformula_binary Mc.IsProp (mkIMPL Mc.IsProp) term f g, env, tg) + | _ -> + if EConstr.eq_constr sigma term op.op_tt then (Mc.TT k, env, tg) + else if EConstr.eq_constr sigma term op.op_ff then Mc.(FF k, env, tg) + else (Mc.X (k, term), env, tg) + in + xparse_formula prop_op Mc.IsProp env tg (*Reductionops.whd_zeta*) term - (* let dump_bool b = Lazy.force (if b then coq_true else coq_false)*) +(* let dump_bool b = Lazy.force (if b then coq_true else coq_false)*) - let dump_kind k = - Lazy.force (match k with Mc.IsProp -> coq_IsProp | Mc.IsBool -> coq_IsBool) +let dump_kind k = + Lazy.force (match k with Mc.IsProp -> coq_IsProp | Mc.IsBool -> coq_IsBool) - let dump_formula typ dump_atom f = - let app_ctor c args = - EConstr.mkApp - ( Lazy.force c - , Array.of_list - ( typ :: Lazy.force coq_eKind :: Lazy.force coq_unit - :: Lazy.force coq_unit :: args ) ) - in - let rec xdump f = - match f with - | Mc.TT k -> app_ctor coq_TT [dump_kind k] - | Mc.FF k -> app_ctor coq_FF [dump_kind k] - | Mc.AND (k, x, y) -> app_ctor coq_AND [dump_kind k; xdump x; xdump y] - | Mc.OR (k, x, y) -> app_ctor coq_OR [dump_kind k; xdump x; xdump y] - | Mc.IMPL (k, x, _, y) -> - app_ctor coq_IMPL - [ dump_kind k - ; xdump x - ; EConstr.mkApp (Lazy.force coq_None, [|Lazy.force coq_unit|]) - ; xdump y ] - | Mc.NOT (k, x) -> app_ctor coq_NOT [dump_kind k; xdump x] - | Mc.IFF (k, x, y) -> app_ctor coq_IFF [dump_kind k; xdump x; xdump y] - | Mc.EQ (x, y) -> app_ctor coq_EQ [xdump x; xdump y] - | Mc.A (k, x, _) -> - app_ctor coq_Atom [dump_kind k; dump_atom x; Lazy.force coq_tt] - | Mc.X (k, t) -> app_ctor coq_X [dump_kind k; t] - in - xdump f - - let prop_env_of_formula gl form = - Mc.( - let rec doit env = function - | TT _ | FF _ | A (_, _, _) -> env - | X (b, t) -> fst (Env.compute_rank_add env t b) - | AND (b, f1, f2) - |OR (b, f1, f2) - |IMPL (b, f1, _, f2) - |IFF (b, f1, f2) -> - doit (doit env f1) f2 - | NOT (b, f) -> doit env f - | EQ (f1, f2) -> doit (doit env f1) f2 - in - doit (Env.empty gl) form) - - let var_env_of_formula form = - let rec vars_of_expr = function - | Mc.PEX n -> ISet.singleton (CoqToCaml.positive n) - | Mc.PEc z -> ISet.empty - | Mc.PEadd (e1, e2) | Mc.PEmul (e1, e2) | Mc.PEsub (e1, e2) -> - ISet.union (vars_of_expr e1) (vars_of_expr e2) - | Mc.PEopp e | Mc.PEpow (e, _) -> vars_of_expr e - in - let vars_of_atom {Mc.flhs; Mc.fop; Mc.frhs} = - ISet.union (vars_of_expr flhs) (vars_of_expr frhs) +let dump_formula typ dump_atom f = + let app_ctor c args = + EConstr.mkApp + ( Lazy.force c + , Array.of_list + ( typ :: Lazy.force coq_eKind :: Lazy.force coq_unit + :: Lazy.force coq_unit :: args ) ) + in + let rec xdump f = + match f with + | Mc.TT k -> app_ctor coq_TT [dump_kind k] + | Mc.FF k -> app_ctor coq_FF [dump_kind k] + | Mc.AND (k, x, y) -> app_ctor coq_AND [dump_kind k; xdump x; xdump y] + | Mc.OR (k, x, y) -> app_ctor coq_OR [dump_kind k; xdump x; xdump y] + | Mc.IMPL (k, x, _, y) -> + app_ctor coq_IMPL + [ dump_kind k + ; xdump x + ; EConstr.mkApp (Lazy.force coq_None, [|Lazy.force coq_unit|]) + ; xdump y ] + | Mc.NOT (k, x) -> app_ctor coq_NOT [dump_kind k; xdump x] + | Mc.IFF (k, x, y) -> app_ctor coq_IFF [dump_kind k; xdump x; xdump y] + | Mc.EQ (x, y) -> app_ctor coq_EQ [xdump x; xdump y] + | Mc.A (k, x, _) -> + app_ctor coq_Atom [dump_kind k; dump_atom x; Lazy.force coq_tt] + | Mc.X (k, t) -> app_ctor coq_X [dump_kind k; t] + in + xdump f + +let prop_env_of_formula gl form = + Mc.( + let rec doit env = function + | TT _ | FF _ | A (_, _, _) -> env + | X (b, t) -> fst (Env.compute_rank_add env t b) + | AND (b, f1, f2) | OR (b, f1, f2) | IMPL (b, f1, _, f2) | IFF (b, f1, f2) + -> + doit (doit env f1) f2 + | NOT (b, f) -> doit env f + | EQ (f1, f2) -> doit (doit env f1) f2 in - Mc.( - let rec doit = function - | TT _ | FF _ | X _ -> ISet.empty - | A (_, a, (t, c)) -> vars_of_atom a - | AND (_, f1, f2) - |OR (_, f1, f2) - |IMPL (_, f1, _, f2) - |IFF (_, f1, f2) - |EQ (f1, f2) -> - ISet.union (doit f1) (doit f2) - | NOT (_, f) -> doit f - in - doit form) - - type 'cst dump_expr = - { (* 'cst is the type of the syntactic constants *) - interp_typ : EConstr.constr - ; dump_cst : 'cst -> EConstr.constr - ; dump_add : EConstr.constr - ; dump_sub : EConstr.constr - ; dump_opp : EConstr.constr - ; dump_mul : EConstr.constr - ; dump_pow : EConstr.constr - ; dump_pow_arg : Mc.n -> EConstr.constr - ; dump_op_prop : (Mc.op2 * EConstr.constr) list - ; dump_op_bool : (Mc.op2 * EConstr.constr) list } - - let dump_zexpr = - lazy - { interp_typ = Lazy.force coq_Z - ; dump_cst = dump_z - ; dump_add = Lazy.force coq_Zplus - ; dump_sub = Lazy.force coq_Zminus - ; dump_opp = Lazy.force coq_Zopp - ; dump_mul = Lazy.force coq_Zmult - ; dump_pow = Lazy.force coq_Zpower - ; dump_pow_arg = (fun n -> dump_z (CamlToCoq.z (CoqToCaml.n n))) - ; dump_op_prop = List.map (fun (x, y) -> (y, Lazy.force x)) zop_table_prop - ; dump_op_bool = List.map (fun (x, y) -> (y, Lazy.force x)) zop_table_bool - } - - let dump_qexpr = - lazy - { interp_typ = Lazy.force coq_Q - ; dump_cst = dump_q - ; dump_add = Lazy.force coq_Qplus - ; dump_sub = Lazy.force coq_Qminus - ; dump_opp = Lazy.force coq_Qopp - ; dump_mul = Lazy.force coq_Qmult - ; dump_pow = Lazy.force coq_Qpower - ; dump_pow_arg = (fun n -> dump_z (CamlToCoq.z (CoqToCaml.n n))) - ; dump_op_prop = List.map (fun (x, y) -> (y, Lazy.force x)) qop_table_prop - ; dump_op_bool = List.map (fun (x, y) -> (y, Lazy.force x)) qop_table_bool - } - - let rec dump_Rcst_as_R cst = - match cst with - | Mc.C0 -> Lazy.force coq_R0 - | Mc.C1 -> Lazy.force coq_R1 - | Mc.CQ q -> EConstr.mkApp (Lazy.force coq_IQR, [|dump_q q|]) - | Mc.CZ z -> EConstr.mkApp (Lazy.force coq_IZR, [|dump_z z|]) - | Mc.CPlus (x, y) -> - EConstr.mkApp - (Lazy.force coq_Rplus, [|dump_Rcst_as_R x; dump_Rcst_as_R y|]) - | Mc.CMinus (x, y) -> - EConstr.mkApp - (Lazy.force coq_Rminus, [|dump_Rcst_as_R x; dump_Rcst_as_R y|]) - | Mc.CMult (x, y) -> - EConstr.mkApp - (Lazy.force coq_Rmult, [|dump_Rcst_as_R x; dump_Rcst_as_R y|]) - | Mc.CPow (x, y) -> ( - match y with - | Mc.Inl z -> - EConstr.mkApp (Lazy.force coq_powerZR, [|dump_Rcst_as_R x; dump_z z|]) - | Mc.Inr n -> - EConstr.mkApp (Lazy.force coq_Rpower, [|dump_Rcst_as_R x; dump_nat n|]) - ) - | Mc.CInv t -> EConstr.mkApp (Lazy.force coq_Rinv, [|dump_Rcst_as_R t|]) - | Mc.COpp t -> EConstr.mkApp (Lazy.force coq_Ropp, [|dump_Rcst_as_R t|]) - - let dump_rexpr = - lazy - { interp_typ = Lazy.force coq_R - ; dump_cst = dump_Rcst_as_R - ; dump_add = Lazy.force coq_Rplus - ; dump_sub = Lazy.force coq_Rminus - ; dump_opp = Lazy.force coq_Ropp - ; dump_mul = Lazy.force coq_Rmult - ; dump_pow = Lazy.force coq_Rpower - ; dump_pow_arg = (fun n -> dump_nat (CamlToCoq.nat (CoqToCaml.n n))) - ; dump_op_prop = List.map (fun (x, y) -> (y, Lazy.force x)) rop_table_prop - ; dump_op_bool = List.map (fun (x, y) -> (y, Lazy.force x)) rop_table_bool - } - - let prodn n env b = - let rec prodrec = function - | 0, env, b -> b - | n, (v, t) :: l, b -> - prodrec (n - 1, l, EConstr.mkProd (make_annot v Sorts.Relevant, t, b)) - | _ -> assert false + doit (Env.empty gl) form) + +let var_env_of_formula form = + let rec vars_of_expr = function + | Mc.PEX n -> ISet.singleton (CoqToCaml.positive n) + | Mc.PEc z -> ISet.empty + | Mc.PEadd (e1, e2) | Mc.PEmul (e1, e2) | Mc.PEsub (e1, e2) -> + ISet.union (vars_of_expr e1) (vars_of_expr e2) + | Mc.PEopp e | Mc.PEpow (e, _) -> vars_of_expr e + in + let vars_of_atom {Mc.flhs; Mc.fop; Mc.frhs} = + ISet.union (vars_of_expr flhs) (vars_of_expr frhs) + in + Mc.( + let rec doit = function + | TT _ | FF _ | X _ -> ISet.empty + | A (_, a, (t, c)) -> vars_of_atom a + | AND (_, f1, f2) + |OR (_, f1, f2) + |IMPL (_, f1, _, f2) + |IFF (_, f1, f2) + |EQ (f1, f2) -> + ISet.union (doit f1) (doit f2) + | NOT (_, f) -> doit f in - prodrec (n, env, b) + doit form) + +type 'cst dump_expr = + { (* 'cst is the type of the syntactic constants *) + interp_typ : EConstr.constr + ; dump_cst : 'cst -> EConstr.constr + ; dump_add : EConstr.constr + ; dump_sub : EConstr.constr + ; dump_opp : EConstr.constr + ; dump_mul : EConstr.constr + ; dump_pow : EConstr.constr + ; dump_pow_arg : Mc.n -> EConstr.constr + ; dump_op_prop : (Mc.op2 * EConstr.constr) list + ; dump_op_bool : (Mc.op2 * EConstr.constr) list } + +let dump_zexpr = + lazy + { interp_typ = Lazy.force coq_Z + ; dump_cst = dump_z + ; dump_add = Lazy.force coq_Zplus + ; dump_sub = Lazy.force coq_Zminus + ; dump_opp = Lazy.force coq_Zopp + ; dump_mul = Lazy.force coq_Zmult + ; dump_pow = Lazy.force coq_Zpower + ; dump_pow_arg = (fun n -> dump_z (CamlToCoq.z (CoqToCaml.n n))) + ; dump_op_prop = List.map (fun (x, y) -> (y, Lazy.force x)) zop_table_prop + ; dump_op_bool = List.map (fun (x, y) -> (y, Lazy.force x)) zop_table_bool + } + +let dump_qexpr = + lazy + { interp_typ = Lazy.force coq_Q + ; dump_cst = dump_q + ; dump_add = Lazy.force coq_Qplus + ; dump_sub = Lazy.force coq_Qminus + ; dump_opp = Lazy.force coq_Qopp + ; dump_mul = Lazy.force coq_Qmult + ; dump_pow = Lazy.force coq_Qpower + ; dump_pow_arg = (fun n -> dump_z (CamlToCoq.z (CoqToCaml.n n))) + ; dump_op_prop = List.map (fun (x, y) -> (y, Lazy.force x)) qop_table_prop + ; dump_op_bool = List.map (fun (x, y) -> (y, Lazy.force x)) qop_table_bool + } + +let rec dump_Rcst_as_R cst = + match cst with + | Mc.C0 -> Lazy.force coq_R0 + | Mc.C1 -> Lazy.force coq_R1 + | Mc.CQ q -> EConstr.mkApp (Lazy.force coq_IQR, [|dump_q q|]) + | Mc.CZ z -> EConstr.mkApp (Lazy.force coq_IZR, [|dump_z z|]) + | Mc.CPlus (x, y) -> + EConstr.mkApp (Lazy.force coq_Rplus, [|dump_Rcst_as_R x; dump_Rcst_as_R y|]) + | Mc.CMinus (x, y) -> + EConstr.mkApp (Lazy.force coq_Rminus, [|dump_Rcst_as_R x; dump_Rcst_as_R y|]) + | Mc.CMult (x, y) -> + EConstr.mkApp (Lazy.force coq_Rmult, [|dump_Rcst_as_R x; dump_Rcst_as_R y|]) + | Mc.CPow (x, y) -> ( + match y with + | Mc.Inl z -> + EConstr.mkApp (Lazy.force coq_powerZR, [|dump_Rcst_as_R x; dump_z z|]) + | Mc.Inr n -> + EConstr.mkApp (Lazy.force coq_Rpower, [|dump_Rcst_as_R x; dump_nat n|]) ) + | Mc.CInv t -> EConstr.mkApp (Lazy.force coq_Rinv, [|dump_Rcst_as_R t|]) + | Mc.COpp t -> EConstr.mkApp (Lazy.force coq_Ropp, [|dump_Rcst_as_R t|]) + +let dump_rexpr = + lazy + { interp_typ = Lazy.force coq_R + ; dump_cst = dump_Rcst_as_R + ; dump_add = Lazy.force coq_Rplus + ; dump_sub = Lazy.force coq_Rminus + ; dump_opp = Lazy.force coq_Ropp + ; dump_mul = Lazy.force coq_Rmult + ; dump_pow = Lazy.force coq_Rpower + ; dump_pow_arg = (fun n -> dump_nat (CamlToCoq.nat (CoqToCaml.n n))) + ; dump_op_prop = List.map (fun (x, y) -> (y, Lazy.force x)) rop_table_prop + ; dump_op_bool = List.map (fun (x, y) -> (y, Lazy.force x)) rop_table_bool + } + +let prodn n env b = + let rec prodrec = function + | 0, env, b -> b + | n, (v, t) :: l, b -> + prodrec (n - 1, l, EConstr.mkProd (make_annot v Sorts.Relevant, t, b)) + | _ -> assert false + in + prodrec (n, env, b) - (** [make_goal_of_formula depxr vars props form] where +(** [make_goal_of_formula depxr vars props form] where - vars is an environment for the arithmetic variables occurring in form - props is an environment for the propositions occurring in form @return a goal where all the variables and propositions of the formula are quantified *) - let eKind = function - | Mc.IsProp -> EConstr.mkProp - | Mc.IsBool -> Lazy.force coq_bool +let eKind = function + | Mc.IsProp -> EConstr.mkProp + | Mc.IsBool -> Lazy.force coq_bool - let make_goal_of_formula gl dexpr form = - let vars_idx = - List.mapi - (fun i v -> (v, i + 1)) - (ISet.elements (var_env_of_formula form)) - in - (* List.iter (fun (v,i) -> Printf.fprintf stdout "var %i has index %i\n" v i) vars_idx ;*) - let props = prop_env_of_formula gl form in - let fresh_var str i = Names.Id.of_string (str ^ string_of_int i) in - let fresh_prop str i = Names.Id.of_string (str ^ string_of_int i) in - let vars_n = - List.map (fun (_, i) -> (fresh_var "__x" i, dexpr.interp_typ)) vars_idx - in - let props_n = - List.mapi - (fun i (_, k) -> (fresh_prop "__p" (i + 1), eKind k)) - (Env.elements props) - in - let var_name_pos = - List.map2 (fun (idx, _) (id, _) -> (id, idx)) vars_idx vars_n - in - let dump_expr i e = - let rec dump_expr = function - | Mc.PEX n -> - EConstr.mkRel (i + List.assoc (CoqToCaml.positive n) vars_idx) - | Mc.PEc z -> dexpr.dump_cst z - | Mc.PEadd (e1, e2) -> - EConstr.mkApp (dexpr.dump_add, [|dump_expr e1; dump_expr e2|]) - | Mc.PEsub (e1, e2) -> - EConstr.mkApp (dexpr.dump_sub, [|dump_expr e1; dump_expr e2|]) - | Mc.PEopp e -> EConstr.mkApp (dexpr.dump_opp, [|dump_expr e|]) - | Mc.PEmul (e1, e2) -> - EConstr.mkApp (dexpr.dump_mul, [|dump_expr e1; dump_expr e2|]) - | Mc.PEpow (e, n) -> - EConstr.mkApp (dexpr.dump_pow, [|dump_expr e; dexpr.dump_pow_arg n|]) - in - dump_expr e - in - let mkop_prop op e1 e2 = - try EConstr.mkApp (List.assoc op dexpr.dump_op_prop, [|e1; e2|]) - with Not_found -> - EConstr.mkApp (Lazy.force coq_eq, [|dexpr.interp_typ; e1; e2|]) - in - let dump_cstr_prop i {Mc.flhs; Mc.fop; Mc.frhs} = - mkop_prop fop (dump_expr i flhs) (dump_expr i frhs) - in - let mkop_bool op e1 e2 = - try EConstr.mkApp (List.assoc op dexpr.dump_op_bool, [|e1; e2|]) - with Not_found -> - EConstr.mkApp (Lazy.force coq_eq, [|dexpr.interp_typ; e1; e2|]) - in - let dump_cstr_bool i {Mc.flhs; Mc.fop; Mc.frhs} = - mkop_bool fop (dump_expr i flhs) (dump_expr i frhs) - in - let rec xdump_prop pi xi f = - match f with - | Mc.TT _ -> Lazy.force coq_True - | Mc.FF _ -> Lazy.force coq_False - | Mc.AND (_, x, y) -> - EConstr.mkApp - (Lazy.force coq_and, [|xdump_prop pi xi x; xdump_prop pi xi y|]) - | Mc.OR (_, x, y) -> - EConstr.mkApp - (Lazy.force coq_or, [|xdump_prop pi xi x; xdump_prop pi xi y|]) - | Mc.IFF (_, x, y) -> - EConstr.mkApp - (Lazy.force coq_iff, [|xdump_prop pi xi x; xdump_prop pi xi y|]) - | Mc.IMPL (_, x, _, y) -> - EConstr.mkArrow (xdump_prop pi xi x) Sorts.Relevant - (xdump_prop (pi + 1) (xi + 1) y) - | Mc.NOT (_, x) -> - EConstr.mkArrow (xdump_prop pi xi x) Sorts.Relevant - (Lazy.force coq_False) - | Mc.EQ (x, y) -> - EConstr.mkApp - ( Lazy.force coq_eq - , [|Lazy.force coq_bool; xdump_bool pi xi x; xdump_bool pi xi y|] ) - | Mc.A (_, x, _) -> dump_cstr_prop xi x - | Mc.X (_, t) -> - let idx = Env.get_rank props t in - EConstr.mkRel (pi + idx) - and xdump_bool pi xi f = - match f with - | Mc.TT _ -> Lazy.force coq_true - | Mc.FF _ -> Lazy.force coq_false - | Mc.AND (_, x, y) -> - EConstr.mkApp - (Lazy.force coq_andb, [|xdump_bool pi xi x; xdump_bool pi xi y|]) - | Mc.OR (_, x, y) -> - EConstr.mkApp - (Lazy.force coq_orb, [|xdump_bool pi xi x; xdump_bool pi xi y|]) - | Mc.IFF (_, x, y) -> - EConstr.mkApp - (Lazy.force coq_eqb, [|xdump_bool pi xi x; xdump_bool pi xi y|]) - | Mc.IMPL (_, x, _, y) -> - EConstr.mkApp - (Lazy.force coq_implb, [|xdump_bool pi xi x; xdump_bool pi xi y|]) - | Mc.NOT (_, x) -> - EConstr.mkApp (Lazy.force coq_negb, [|xdump_bool pi xi x|]) - | Mc.EQ (x, y) -> assert false - | Mc.A (_, x, _) -> dump_cstr_bool xi x - | Mc.X (_, t) -> - let idx = Env.get_rank props t in - EConstr.mkRel (pi + idx) - in - let nb_vars = List.length vars_n in - let nb_props = List.length props_n in - (* Printf.fprintf stdout "NBProps : %i\n" nb_props ;*) - let subst_prop p = - let idx = Env.get_rank props p in - EConstr.mkVar (Names.Id.of_string (Printf.sprintf "__p%i" idx)) +let make_goal_of_formula gl dexpr form = + let vars_idx = + List.mapi (fun i v -> (v, i + 1)) (ISet.elements (var_env_of_formula form)) + in + (* List.iter (fun (v,i) -> Printf.fprintf stdout "var %i has index %i\n" v i) vars_idx ;*) + let props = prop_env_of_formula gl form in + let fresh_var str i = Names.Id.of_string (str ^ string_of_int i) in + let fresh_prop str i = Names.Id.of_string (str ^ string_of_int i) in + let vars_n = + List.map (fun (_, i) -> (fresh_var "__x" i, dexpr.interp_typ)) vars_idx + in + let props_n = + List.mapi + (fun i (_, k) -> (fresh_prop "__p" (i + 1), eKind k)) + (Env.elements props) + in + let var_name_pos = + List.map2 (fun (idx, _) (id, _) -> (id, idx)) vars_idx vars_n + in + let dump_expr i e = + let rec dump_expr = function + | Mc.PEX n -> + EConstr.mkRel (i + List.assoc (CoqToCaml.positive n) vars_idx) + | Mc.PEc z -> dexpr.dump_cst z + | Mc.PEadd (e1, e2) -> + EConstr.mkApp (dexpr.dump_add, [|dump_expr e1; dump_expr e2|]) + | Mc.PEsub (e1, e2) -> + EConstr.mkApp (dexpr.dump_sub, [|dump_expr e1; dump_expr e2|]) + | Mc.PEopp e -> EConstr.mkApp (dexpr.dump_opp, [|dump_expr e|]) + | Mc.PEmul (e1, e2) -> + EConstr.mkApp (dexpr.dump_mul, [|dump_expr e1; dump_expr e2|]) + | Mc.PEpow (e, n) -> + EConstr.mkApp (dexpr.dump_pow, [|dump_expr e; dexpr.dump_pow_arg n|]) in - let form' = Mc.mapX (fun _ p -> subst_prop p) Mc.IsProp form in - ( prodn nb_props - (List.map (fun (x, y) -> (Name.Name x, y)) props_n) - (prodn nb_vars - (List.map (fun (x, y) -> (Name.Name x, y)) vars_n) - (xdump_prop (List.length vars_n) 0 form)) - , List.rev props_n - , List.rev var_name_pos - , form' ) - - (** + dump_expr e + in + let mkop_prop op e1 e2 = + try EConstr.mkApp (List.assoc op dexpr.dump_op_prop, [|e1; e2|]) + with Not_found -> + EConstr.mkApp (Lazy.force coq_eq, [|dexpr.interp_typ; e1; e2|]) + in + let dump_cstr_prop i {Mc.flhs; Mc.fop; Mc.frhs} = + mkop_prop fop (dump_expr i flhs) (dump_expr i frhs) + in + let mkop_bool op e1 e2 = + try EConstr.mkApp (List.assoc op dexpr.dump_op_bool, [|e1; e2|]) + with Not_found -> + EConstr.mkApp (Lazy.force coq_eq, [|dexpr.interp_typ; e1; e2|]) + in + let dump_cstr_bool i {Mc.flhs; Mc.fop; Mc.frhs} = + mkop_bool fop (dump_expr i flhs) (dump_expr i frhs) + in + let rec xdump_prop pi xi f = + match f with + | Mc.TT _ -> Lazy.force coq_True + | Mc.FF _ -> Lazy.force coq_False + | Mc.AND (_, x, y) -> + EConstr.mkApp + (Lazy.force coq_and, [|xdump_prop pi xi x; xdump_prop pi xi y|]) + | Mc.OR (_, x, y) -> + EConstr.mkApp + (Lazy.force coq_or, [|xdump_prop pi xi x; xdump_prop pi xi y|]) + | Mc.IFF (_, x, y) -> + EConstr.mkApp + (Lazy.force coq_iff, [|xdump_prop pi xi x; xdump_prop pi xi y|]) + | Mc.IMPL (_, x, _, y) -> + EConstr.mkArrow (xdump_prop pi xi x) Sorts.Relevant + (xdump_prop (pi + 1) (xi + 1) y) + | Mc.NOT (_, x) -> + EConstr.mkArrow (xdump_prop pi xi x) Sorts.Relevant (Lazy.force coq_False) + | Mc.EQ (x, y) -> + EConstr.mkApp + ( Lazy.force coq_eq + , [|Lazy.force coq_bool; xdump_bool pi xi x; xdump_bool pi xi y|] ) + | Mc.A (_, x, _) -> dump_cstr_prop xi x + | Mc.X (_, t) -> + let idx = Env.get_rank props t in + EConstr.mkRel (pi + idx) + and xdump_bool pi xi f = + match f with + | Mc.TT _ -> Lazy.force coq_true + | Mc.FF _ -> Lazy.force coq_false + | Mc.AND (_, x, y) -> + EConstr.mkApp + (Lazy.force coq_andb, [|xdump_bool pi xi x; xdump_bool pi xi y|]) + | Mc.OR (_, x, y) -> + EConstr.mkApp + (Lazy.force coq_orb, [|xdump_bool pi xi x; xdump_bool pi xi y|]) + | Mc.IFF (_, x, y) -> + EConstr.mkApp + (Lazy.force coq_eqb, [|xdump_bool pi xi x; xdump_bool pi xi y|]) + | Mc.IMPL (_, x, _, y) -> + EConstr.mkApp + (Lazy.force coq_implb, [|xdump_bool pi xi x; xdump_bool pi xi y|]) + | Mc.NOT (_, x) -> + EConstr.mkApp (Lazy.force coq_negb, [|xdump_bool pi xi x|]) + | Mc.EQ (x, y) -> assert false + | Mc.A (_, x, _) -> dump_cstr_bool xi x + | Mc.X (_, t) -> + let idx = Env.get_rank props t in + EConstr.mkRel (pi + idx) + in + let nb_vars = List.length vars_n in + let nb_props = List.length props_n in + (* Printf.fprintf stdout "NBProps : %i\n" nb_props ;*) + let subst_prop p = + let idx = Env.get_rank props p in + EConstr.mkVar (Names.Id.of_string (Printf.sprintf "__p%i" idx)) + in + let form' = Mc.mapX (fun _ p -> subst_prop p) Mc.IsProp form in + ( prodn nb_props + (List.map (fun (x, y) -> (Name.Name x, y)) props_n) + (prodn nb_vars + (List.map (fun (x, y) -> (Name.Name x, y)) vars_n) + (xdump_prop (List.length vars_n) 0 form)) + , List.rev props_n + , List.rev var_name_pos + , form' ) + +(** * Given a conclusion and a list of affectations, rebuild a term prefixed by * the appropriate letins. * TODO: reverse the list of bindings! *) - let set l concl = - let rec xset acc = function - | [] -> acc - | e :: l -> - let name, expr, typ = e in - xset - (EConstr.mkNamedLetIn - (make_annot (Names.Id.of_string name) Sorts.Relevant) - expr typ acc) - l - in - xset concl l -end - -open M +let set l concl = + let rec xset acc = function + | [] -> acc + | e :: l -> + let name, expr, typ = e in + xset + (EConstr.mkNamedLetIn + (make_annot (Names.Id.of_string name) Sorts.Relevant) + expr typ acc) + l + in + xset concl l let coq_Branch = lazy (constr_of_ref "micromega.VarMap.Branch") let coq_Elt = lazy (constr_of_ref "micromega.VarMap.Elt") @@ -1424,14 +1389,14 @@ let rec pp_proof_term o = function | Micromega.ExProof (p, prf) -> Printf.fprintf o "Ex[%a,%a]" pp_positive p pp_proof_term prf -let rec parse_hyps gl parse_arith env tg hyps = +let rec parse_hyps (genv, sigma) parse_arith env tg hyps = match hyps with | [] -> ([], env, tg) | (i, t) :: l -> - let lhyps, env, tg = parse_hyps gl parse_arith env tg l in - if is_prop gl.env gl.sigma t then + let lhyps, env, tg = parse_hyps (genv, sigma) parse_arith env tg l in + if is_prop genv sigma t then try - let c, env, tg = parse_formula gl parse_arith env tg t in + let c, env, tg = parse_formula (genv, sigma) parse_arith env tg t in ((i, c) :: lhyps, env, tg) with ParseError -> (lhyps, env, tg) else (lhyps, env, tg) @@ -1852,19 +1817,22 @@ let clear_all_no_check = let micromega_gen parse_arith pre_process cnf spec dumpexpr prover tac = Proofview.Goal.enter (fun gl -> let sigma = Tacmach.New.project gl in + let genv = Tacmach.New.pf_env gl in let concl = Tacmach.New.pf_concl gl in let hyps = Tacmach.New.pf_hyps_types gl in try - let gl0 = {env = Tacmach.New.pf_env gl; sigma} in let hyps, concl, env = - parse_goal gl0 parse_arith (Env.empty gl0) hyps concl + parse_goal (genv, sigma) parse_arith + (Env.empty (genv, sigma)) + hyps concl in let env = Env.elements env in let spec = Lazy.force spec in let dumpexpr = Lazy.force dumpexpr in - if debug then Feedback.msg_debug (Pp.str "Env " ++ Env.pp gl0 env); + if debug then + Feedback.msg_debug (Pp.str "Env " ++ Env.pp (genv, sigma) env); match - micromega_tauto pre_process cnf spec prover env hyps concl gl0 + micromega_tauto pre_process cnf spec prover env hyps concl (env, sigma) with | Unknown -> flush stdout; @@ -1873,7 +1841,7 @@ let micromega_gen parse_arith pre_process cnf spec dumpexpr prover tac = Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness") | Prf (ids, ff', res') -> let arith_goal, props, vars, ff_arith = - make_goal_of_formula gl0 dumpexpr ff' + make_goal_of_formula (genv, sigma) dumpexpr ff' in let intro (id, _) = Tactics.introduction id in let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in @@ -1893,7 +1861,9 @@ let micromega_gen parse_arith pre_process cnf spec dumpexpr prover tac = env' ff_arith ] in let goal_props = - List.rev (List.map fst (Env.elements (prop_env_of_formula gl0 ff'))) + List.rev + (List.map fst + (Env.elements (prop_env_of_formula (genv, sigma) ff'))) in let goal_vars = List.map (fun (_, i) -> fst (List.nth env (i - 1))) vars @@ -1971,12 +1941,14 @@ let micromega_genr prover tac = in Proofview.Goal.enter (fun gl -> let sigma = Tacmach.New.project gl in + let genv = Tacmach.New.pf_env gl in let concl = Tacmach.New.pf_concl gl in let hyps = Tacmach.New.pf_hyps_types gl in try - let gl0 = {env = Tacmach.New.pf_env gl; sigma} in let hyps, concl, env = - parse_goal gl0 parse_arith (Env.empty gl0) hyps concl + parse_goal (genv, sigma) parse_arith + (Env.empty (genv, sigma)) + hyps concl in let env = Env.elements env in let spec = Lazy.force spec in @@ -1997,7 +1969,7 @@ let micromega_genr prover tac = match micromega_tauto (fun _ x -> x) - Mc.cnfQ spec prover env hyps' concl' gl0 + Mc.cnfQ spec prover env hyps' concl' (genv, sigma) with | Unknown | Model _ -> flush stdout; @@ -2010,7 +1982,7 @@ let micromega_genr prover tac = in let ff' = abstract_wrt_formula ff' ff in let arith_goal, props, vars, ff_arith = - make_goal_of_formula gl0 (Lazy.force dump_rexpr) ff' + make_goal_of_formula (genv, sigma) (Lazy.force dump_rexpr) ff' in let intro (id, _) = Tactics.introduction id in let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in @@ -2030,7 +2002,9 @@ let micromega_genr prover tac = ; micromega_order_changer res' env' ff_arith ] in let goal_props = - List.rev (List.map fst (Env.elements (prop_env_of_formula gl0 ff'))) + List.rev + (List.map fst + (Env.elements (prop_env_of_formula (genv, sigma) ff'))) in let goal_vars = List.map (fun (_, i) -> fst (List.nth env (i - 1))) vars diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml index fa29e6080e..917961fdcd 100644 --- a/plugins/micromega/zify.ml +++ b/plugins/micromega/zify.ml @@ -464,13 +464,18 @@ module ECstOp = struct let cast x = CstOp x let dest = function CstOp x -> Some x | _ -> None + let isConstruct evd c = + match EConstr.kind evd c with + | Construct _ | Int _ | Float _ -> true + | _ -> false + let mk_elt evd i a = { source = a.(0) ; target = a.(1) ; inj = get_inj evd a.(3) ; cst = a.(4) ; cstinj = a.(5) - ; is_construct = EConstr.isConstruct evd a.(2) } + ; is_construct = isConstruct evd a.(2) } let get_key = 2 end @@ -979,17 +984,21 @@ let is_arrow env evd a p1 p2 = where c is the head symbol and [a] is the array of arguments. The function also transforms (x -> y) as (arrow x y) *) let get_operator barrow env evd e = - match EConstr.kind evd e with + let e' = EConstr.whd_evar evd e in + match EConstr.kind evd e' with | Prod (a, p1, p2) -> - if barrow && is_arrow env evd a p1 p2 then (arrow, [|p1; p2|]) + if barrow && is_arrow env evd a p1 p2 then (arrow, [|p1; p2|], false) else raise Not_found | App (c, a) -> ( - match EConstr.kind evd c with + let c' = EConstr.whd_evar evd c in + match EConstr.kind evd c' with | Construct _ (* e.g. Z0 , Z.pos *) | Const _ (* e.g. Z.max *) | Proj _ |Lambda _ (* e.g projections *) | Ind _ (* e.g. eq *) -> - (c, a) + (c', a, false) | _ -> raise Not_found ) - | Construct _ -> (EConstr.whd_evar evd e, [||]) + | Const _ -> (e', [||], false) + | Construct _ -> (e', [||], true) + | Int _ | Float _ -> (e', [||], true) | _ -> raise Not_found let decompose_app env evd e = @@ -1065,37 +1074,41 @@ let rec trans_expr env evd e = let inj = e.inj in let e = e.constr in try - let c, a = get_operator false env evd e in - let k, t = - find_option (match_operator env evd c a) (HConstr.find_all c !table_cache) - in - let n = Array.length a in - match k with - | CstOp {deriv = c'} -> - ECstOpT.(if c'.is_construct then Term else Prf (c'.cst, c'.cstinj)) - | UnOp {deriv = unop} -> - let prf = - trans_expr env evd - { constr = a.(n - 1) - ; typ = unop.EUnOpT.source1 - ; inj = unop.EUnOpT.inj1_t } - in - app_unop evd e unop a.(n - 1) prf - | BinOp {deriv = binop} -> - let prf1 = - trans_expr env evd - { constr = a.(n - 2) - ; typ = binop.EBinOpT.source1 - ; inj = binop.EBinOpT.inj1 } - in - let prf2 = - trans_expr env evd - { constr = a.(n - 1) - ; typ = binop.EBinOpT.source2 - ; inj = binop.EBinOpT.inj2 } + let c, a, is_constant = get_operator false env evd e in + if is_constant then Term + else + let k, t = + find_option + (match_operator env evd c a) + (HConstr.find_all c !table_cache) in - app_binop evd e binop a.(n - 2) prf1 a.(n - 1) prf2 - | d -> mkvar evd inj e + let n = Array.length a in + match k with + | CstOp {deriv = c'} -> + ECstOpT.(if c'.is_construct then Term else Prf (c'.cst, c'.cstinj)) + | UnOp {deriv = unop} -> + let prf = + trans_expr env evd + { constr = a.(n - 1) + ; typ = unop.EUnOpT.source1 + ; inj = unop.EUnOpT.inj1_t } + in + app_unop evd e unop a.(n - 1) prf + | BinOp {deriv = binop} -> + let prf1 = + trans_expr env evd + { constr = a.(n - 2) + ; typ = binop.EBinOpT.source1 + ; inj = binop.EBinOpT.inj1 } + in + let prf2 = + trans_expr env evd + { constr = a.(n - 1) + ; typ = binop.EBinOpT.source2 + ; inj = binop.EBinOpT.inj2 } + in + app_binop evd e binop a.(n - 2) prf1 a.(n - 1) prf2 + | d -> mkvar evd inj e with Not_found -> (* Feedback.msg_debug Pp.(str "Not found " ++ Termops.Internal.debug_print_constr e); *) diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index d859fe51ab..cb58b9bcb8 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -280,7 +280,7 @@ let interp_wit wit ist gl x = sigma, Tacinterp.Value.cast (topwit wit) arg let interp_hyp ist gl (SsrHyp (loc, id)) = - let s, id' = interp_wit wit_var ist gl CAst.(make ?loc id) in + let s, id' = interp_wit wit_hyp ist gl CAst.(make ?loc id) in if not_section_id id' then s, SsrHyp (loc, id') else hyp_err ?loc "Can't clear section hypothesis " id' diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 89e0c9fcbe..7b584b5159 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -155,7 +155,7 @@ let pr_ssrhyp _ _ _ = pr_hyp let wit_ssrhyprep = add_genarg "ssrhyprep" (fun env sigma -> pr_hyp) let intern_hyp ist (SsrHyp (loc, id) as hyp) = - let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_var) CAst.(make ?loc id)) in + let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_hyp) CAst.(make ?loc id)) in if not_section_id id then hyp else hyp_err ?loc "Can't clear section hypothesis " id diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 5dedae6388..cdd15acb0d 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -204,7 +204,8 @@ exception NoProgress (* comparison can be much faster than the HO one. *) let unif_EQ env sigma p c = - let evars = existential_opt_value0 sigma, Evd.universes sigma in + let env = Environ.set_universes (Evd.universes sigma) env in + let evars = existential_opt_value0 sigma in try let _ = Reduction.conv env p ~evars c in true with _ -> false let unif_EQ_args env sigma pa a = diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 91c155fcce..a12a832f76 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -715,9 +715,9 @@ and detype_r d flags avoid env sigma t = (* Meta in constr are not user-parsable and are mapped to Evar *) if n = Constr_matching.special_meta then (* Using a dash to be unparsable *) - GEvar (Id.of_string_soft "CONTEXT-HOLE", []) + GEvar (CAst.make @@ Id.of_string_soft "CONTEXT-HOLE", []) else - GEvar (Id.of_string_soft ("M" ^ string_of_int n), []) + GEvar (CAst.make @@ Id.of_string_soft ("M" ^ string_of_int n), []) | Var id -> (* Discriminate between section variable and non-section variable *) (try let _ = Global.lookup_named id in GRef (GlobRef.VarRef id, None) @@ -788,12 +788,12 @@ and detype_r d flags avoid env sigma t = let l = Evd.evar_instance_array bound_to_itself_or_letin (Evd.find sigma evk) cl in let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> match EConstr.kind sigma c with Rel n -> (fvs,Int.Set.add n rels) | Var id -> (Id.Set.add id fvs,rels) | _ -> (fvs,rels)) (Id.Set.empty,Int.Set.empty) l in let l = Evd.evar_instance_array (fun d c -> not !print_evar_arguments && (bound_to_itself_or_letin d c && not (isRel sigma c && Int.Set.mem (destRel sigma c) rels || isVar sigma c && (Id.Set.mem (destVar sigma c) fvs)))) (Evd.find sigma evk) cl in - id,l + id,List.map (fun (id,c) -> (CAst.make id,c)) l with Not_found -> Id.of_string ("X" ^ string_of_int (Evar.repr evk)), - (List.map (fun c -> (Id.of_string "__",c)) cl) + (List.map (fun c -> (CAst.make @@ Id.of_string "__",c)) cl) in - GEvar (id, + GEvar (CAst.make id, List.map (on_snd (detype d flags avoid env sigma)) l) | Ind (ind_sp,u) -> GRef (GlobRef.IndRef ind_sp, detype_instance sigma u) diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 5bd26be823..dc5fd80f9e 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -128,7 +128,7 @@ let fix_kind_eq k1 k2 = match k1, k2 with | (GFix _ | GCoFix _), _ -> false let instance_eq f (x1,c1) (x2,c2) = - Id.equal x1 x2 && f c1 c2 + Id.equal x1.CAst.v x2.CAst.v && f c1 c2 let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with | GRef (gr1, u1), GRef (gr2, u2) -> @@ -136,7 +136,7 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with Option.equal (List.equal glob_level_eq) u1 u2 | GVar id1, GVar id2 -> Id.equal id1 id2 | GEvar (id1, arg1), GEvar (id2, arg2) -> - Id.equal id1 id2 && List.equal (instance_eq f) arg1 arg2 + Id.equal id1.CAst.v id2.CAst.v && List.equal (instance_eq f) arg1 arg2 | GPatVar k1, GPatVar k2 -> matching_var_kind_eq k1 k2 | GApp (f1, arg1), GApp (f2, arg2) -> f f1 f2 && List.equal f arg1 arg2 diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 526eac6f1e..a49c8abe26 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -75,7 +75,7 @@ type 'a glob_constr_r = | GVar of Id.t (** An identifier that cannot be regarded as "GRef". Bound variables are typically represented this way. *) - | GEvar of existential_name * (Id.t * 'a glob_constr_g) list + | GEvar of existential_name CAst.t * (lident * 'a glob_constr_g) list | GPatVar of Evar_kinds.matching_var_kind (** Used for patterns only *) | GApp of 'a glob_constr_g * 'a glob_constr_g list | GLambda of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 1e8441dd8a..1dddc5622d 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -48,7 +48,7 @@ type pretype_error = | CannotUnifyBindingType of constr * constr | CannotGeneralize of constr | NoOccurrenceFound of constr * Id.t option - | CannotFindWellTypedAbstraction of constr * constr list * (env * type_error) option + | CannotFindWellTypedAbstraction of constr * constr list * (env * pretype_error) option | WrongAbstractionType of Name.t * constr * types * types | AbstractionOverMeta of Name.t * Name.t | NonLinearUnification of Name.t * constr diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 45997e9a66..714d68165e 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -54,7 +54,7 @@ type pretype_error = | CannotUnifyBindingType of constr * constr | CannotGeneralize of constr | NoOccurrenceFound of constr * Id.t option - | CannotFindWellTypedAbstraction of constr * constr list * (env * type_error) option + | CannotFindWellTypedAbstraction of constr * constr list * (env * pretype_error) option | WrongAbstractionType of Name.t * constr * types * types | AbstractionOverMeta of Name.t * Name.t | NonLinearUnification of Name.t * constr @@ -132,7 +132,7 @@ val error_cannot_unify : ?loc:Loc.t -> env -> Evd.evar_map -> val error_cannot_unify_local : env -> Evd.evar_map -> constr * constr * constr -> 'b val error_cannot_find_well_typed_abstraction : env -> Evd.evar_map -> - constr -> constr list -> (env * type_error) option -> 'b + constr -> constr list -> (env * pretype_error) option -> 'b val error_wrong_abstraction_type : env -> Evd.evar_map -> Name.t -> constr -> types -> types -> 'b diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 7597661ca8..268ad2ae56 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -365,9 +365,9 @@ let inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j = functio | Some t -> Coercion.inh_conv_coerce_to ?loc ~program_mode resolve_tc !!env sigma j t -let check_instance loc subst = function +let check_instance subst = function | [] -> () - | (id,_) :: _ -> + | (CAst.{loc;v=id},_) :: _ -> if List.mem_assoc id subst then user_err ?loc (Id.print id ++ str "appears more than once.") else @@ -493,7 +493,7 @@ type 'a pretype_fun = ?loc:Loc.t -> program_mode:bool -> poly:bool -> bool -> ty type pretyper = { pretype_ref : pretyper -> GlobRef.t * glob_level list option -> unsafe_judgment pretype_fun; pretype_var : pretyper -> Id.t -> unsafe_judgment pretype_fun; - pretype_evar : pretyper -> existential_name * (Id.t * glob_constr) list -> unsafe_judgment pretype_fun; + pretype_evar : pretyper -> existential_name CAst.t * (lident * glob_constr) list -> unsafe_judgment pretype_fun; pretype_patvar : pretyper -> Evar_kinds.matching_var_kind -> unsafe_judgment pretype_fun; pretype_app : pretyper -> glob_constr * glob_constr list -> unsafe_judgment pretype_fun; pretype_lambda : pretyper -> Name.t * binding_kind * glob_constr * glob_constr -> unsafe_judgment pretype_fun; @@ -587,10 +587,10 @@ let pretype_instance self ~program_mode ~poly resolve_tc env sigma loc hyps evk strbrk " is not well-typed.") in let sigma, c, update = try - let c = List.assoc id update in + let c = snd (List.find (fun (CAst.{v=id'},c) -> Id.equal id id') update) in let sigma, c = eval_pretyper self ~program_mode ~poly resolve_tc (mk_tycon t) env sigma c in check_body sigma id (Some c.uj_val); - sigma, c.uj_val, List.remove_assoc id update + sigma, c.uj_val, List.remove_first (fun (CAst.{v=id'},_) -> Id.equal id id') update with Not_found -> try let (n,b',t') = lookup_rel_id id (rel_context !!env) in @@ -609,7 +609,7 @@ let pretype_instance self ~program_mode ~poly resolve_tc env sigma loc hyps evk str " in current context: no binding for " ++ Id.print id ++ str ".") in ((id,c)::subst, update, sigma) in let subst,inst,sigma = List.fold_right f hyps ([],update,sigma) in - check_instance loc subst inst; + check_instance subst inst; sigma, List.map snd subst module Default = @@ -628,13 +628,13 @@ struct let sigma, t_id = pretype_id (fun e r t -> pretype tycon e r t) loc env sigma id in discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma t_id tycon - let pretype_evar self (id, inst) ?loc ~program_mode ~poly resolve_tc tycon env sigma = + let pretype_evar self (CAst.{v=id;loc=locid}, inst) ?loc ~program_mode ~poly resolve_tc tycon env sigma = (* Ne faudrait-il pas s'assurer que hyps est bien un sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *) let id = interp_ltac_id env id in let evk = try Evd.evar_key id sigma - with Not_found -> error_evar_not_found ?loc !!env sigma id in + with Not_found -> error_evar_not_found ?loc:locid !!env sigma id in let hyps = evar_filtered_context (Evd.find sigma evk) in let sigma, args = pretype_instance self ~program_mode ~poly resolve_tc env sigma loc hyps evk inst in let c = mkEvar (evk, args) in @@ -857,7 +857,7 @@ struct typing the argument, so we replace it by an existential variable *) let sigma, c_hole = new_evar env sigma ~src:(loc,Evar_kinds.InternalHole) c1 in - (sigma, make_judge c_hole c1), (c_hole, c, trace) :: bidiargs + (sigma, make_judge c_hole c1), (c_hole, c1, c, trace) :: bidiargs else let tycon = Some c1 in pretype tycon env sigma c, bidiargs @@ -886,12 +886,10 @@ struct let sigma, resj, resj_before_bidi, bidiargs = apply_rec env sigma 0 fj fj candargs [] args in let sigma, resj = refresh_template env sigma resj in let sigma, resj, otrace = inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon in - let refine_arg n (sigma,t) (newarg,origarg,trace) = + let refine_arg n (sigma,t) (newarg,ty,origarg,trace) = (* Refine an argument (originally `origarg`) represented by an evar (`newarg`) to use typing information from the context *) - (* Recover the expected type of the argument *) - let ty = Retyping.get_type_of !!env sigma newarg in - (* Type the argument using this expected type *) + (* Type the argument using the expected type *) let sigma, j = pretype (Some ty) env sigma origarg in (* Unify the (possibly refined) existential variable with the (typechecked) original value *) diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index c03374c59f..7bb4a6e273 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -148,7 +148,7 @@ type 'a pretype_fun = ?loc:Loc.t -> program_mode:bool -> poly:bool -> bool -> Ev type pretyper = { pretype_ref : pretyper -> GlobRef.t * glob_level list option -> unsafe_judgment pretype_fun; pretype_var : pretyper -> Id.t -> unsafe_judgment pretype_fun; - pretype_evar : pretyper -> existential_name * (Id.t * glob_constr) list -> unsafe_judgment pretype_fun; + pretype_evar : pretyper -> existential_name CAst.t * (lident * glob_constr) list -> unsafe_judgment pretype_fun; pretype_patvar : pretyper -> Evar_kinds.matching_var_kind -> unsafe_judgment pretype_fun; pretype_app : pretyper -> glob_constr * glob_constr list -> unsafe_judgment pretype_fun; pretype_lambda : pretyper -> Name.t * binding_kind * glob_constr * glob_constr -> unsafe_judgment pretype_fun; diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 08a6db5639..3352bfce38 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1094,7 +1094,8 @@ let f_conv_leq ?l2r ?reds env ?evars x y = let test_trans_conversion (f: constr Reduction.extended_conversion_function) reds env sigma x y = try let evars ev = safe_evar_value sigma ev in - let _ = f ~reds env ~evars:(evars, Evd.universes sigma) x y in + let env = Environ.set_universes (Evd.universes sigma) env in + let _ = f ~reds env ~evars x y in true with Reduction.NotConvertible -> false | e -> @@ -1112,7 +1113,8 @@ let check_conv ?(pb=Reduction.CUMUL) ?(ts=TransparentState.full) env sigma x y = | Reduction.CONV -> f_conv | Reduction.CUMUL -> f_conv_leq in - try f ~reds:ts env ~evars:(safe_evar_value sigma, Evd.universes sigma) x y; true + let env = Environ.set_universes (Evd.universes sigma) env in + try f ~reds:ts env ~evars:(safe_evar_value sigma) x y; true with Reduction.NotConvertible -> false | Univ.UniverseInconsistency _ -> false | e -> @@ -1138,8 +1140,7 @@ let sigma_check_inductive_instances cv_pb variance u1 u2 sigma = let sigma_univ_state = let open Reduction in - { compare_graph = Evd.universes; - compare_sorts = sigma_compare_sorts; + { compare_sorts = sigma_compare_sorts; compare_instances = sigma_compare_instances; compare_cumul_instances = sigma_check_inductive_instances; } @@ -1164,6 +1165,7 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) | None -> let x = EConstr.Unsafe.to_constr x in let y = EConstr.Unsafe.to_constr y in + let env = Environ.set_universes (Evd.universes sigma) env in let sigma' = conv_fun pb ~l2r:false sigma ts env (sigma, sigma_univ_state) x y in diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 756ccd3438..aeb3873de7 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -220,14 +220,15 @@ let check_allowed_sort env sigma ind c p = else Sorts.relevance_of_sort_family ksort +let check_actual_type env sigma cj t = + try Evarconv.unify_leq_delay env sigma cj.uj_type t + with Evarconv.UnableToUnify (sigma,e) -> error_actual_type env sigma cj t e + let judge_of_cast env sigma cj k tj = let expected_type = tj.utj_val in - match Evarconv.unify_leq_delay env sigma cj.uj_type expected_type with - | exception Evarconv.UnableToUnify _ -> - error_actual_type_core env sigma cj expected_type; - | sigma -> - sigma, { uj_val = mkCast (cj.uj_val, k, expected_type); - uj_type = expected_type } + let sigma = check_actual_type env sigma cj expected_type in + sigma, { uj_val = mkCast (cj.uj_val, k, expected_type); + uj_type = expected_type } let check_fix env sigma pfix = let inj c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in @@ -296,7 +297,8 @@ let judge_of_letin env name defj typj j = uj_type = subst1 defj.uj_val j.uj_type } let check_hyps_inclusion env sigma x hyps = - let evars = Evarutil.safe_evar_value sigma, Evd.universes sigma in + let env = Environ.set_universes (Evd.universes sigma) env in + let evars = Evarutil.safe_evar_value sigma in Typeops.check_hyps_inclusion env ~evars x hyps let type_of_constant env sigma (c,u) = @@ -340,7 +342,7 @@ let judge_of_array env sigma u tj defj tyj = let sigma = Evd.set_leq_sort env sigma tyj.utj_type (Sorts.sort_of_univ (Univ.Universe.make ulev)) in - let check_one sigma j = Evarconv.unify_leq_delay env sigma j.uj_type tyj.utj_val in + let check_one sigma j = check_actual_type env sigma j tyj.utj_val in let sigma = check_one sigma defj in let sigma = Array.fold_left check_one sigma tj in let arr = EConstr.of_constr @@ type_of_array env u in @@ -391,7 +393,7 @@ let rec execute env sigma cstr = let t = mkApp (mkIndU (ci.ci_ind,univs), args) in let sigma, tj = execute env sigma t in let sigma, tj = type_judgment env sigma tj in - let sigma = Evarconv.unify_leq_delay env sigma cj.uj_type tj.utj_val in + let sigma = check_actual_type env sigma cj tj.utj_val in sigma in judge_of_case env sigma ci pj iv cj lfj @@ -492,10 +494,7 @@ and execute_array env = Array.fold_left_map (execute env) let check env sigma c t = let sigma, j = execute env sigma c in - match Evarconv.unify_leq_delay env sigma j.uj_type t with - | exception Evarconv.UnableToUnify _ -> - error_actual_type_core env sigma j t - | sigma -> sigma + check_actual_type env sigma j t (* Type of a constr *) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 207a03d80f..ccfb508964 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -134,8 +134,8 @@ let abstract_list_all env evd typ c l = | Type_errors.TypeError (env',x) -> (* FIXME: plug back the typing information *) error_cannot_find_well_typed_abstraction env evd p l None - | Pretype_errors.PretypeError (env',evd,TypingError x) -> - error_cannot_find_well_typed_abstraction env evd p l (Some (env',x)) in + | Pretype_errors.PretypeError (env',evd,e) -> + error_cannot_find_well_typed_abstraction env evd p l (Some (env',e)) in evd,(p,typp) let set_occurrences_of_last_arg n = diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 900ba0edb9..1420401875 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -218,7 +218,8 @@ and nf_evar env sigma evk stk = let t = List.fold_left fold concl hyps in let t, args = nf_args env sigma args t in let inst, args = Array.chop (List.length hyps) args in - let inst = Array.to_list inst in + (* Evar instances are reversed w.r.t. argument order *) + let inst = Array.rev_to_list inst in let c = mkApp (mkEvar (evk, inst), args) in nf_stk env sigma c t stk | _ -> diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 267f5e0b5f..8da1d636f0 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -227,13 +227,49 @@ let tag_var = tag Tag.variable let pr_evar pr id l = hov 0 ( - tag_evar (str "?" ++ pr_id id) ++ + tag_evar (str "?" ++ pr_lident id) ++ (match l with | [] -> mt() | l -> - let f (id,c) = pr_id id ++ str ":=" ++ pr ltop c in + let f (id,c) = pr_lident id ++ str ":=" ++ pr ltop c in str"@{" ++ hov 0 (prlist_with_sep pr_semicolon f (List.rev l)) ++ str"}")) + (* Assuming "{" and "}" brackets, prints + - if there is enough room + { a; b; c } + - otherwise + { + a; + b; + c + } + Alternatively, replace outer hv with h to get instead: + { a; + b; + c } + Replace the inner hv with hov to respectively get instead (if enough room): + { + a; b; + c + } + or + { a; b; + c } + *) + let pr_record left right pr = function + | [] -> str left ++ str " " ++ str right + | l -> + hv 0 ( + str left ++ + brk (1,String.length left) ++ + hv 0 (prlist_with_sep pr_semicolon pr l) ++ + brk (1,0) ++ + str right) + + let pr_record_body left right pr l = + let pr_defined_field (id, c) = hov 2 (pr_reference id ++ str" :=" ++ pr c) in + pr_record left right pr_defined_field l + let las = lapp let lpator = 0 let lpatrec = 0 @@ -242,11 +278,7 @@ let tag_var = tag Tag.variable let rec pr_patt sep inh p = let (strm,prec) = match CAst.(p.v) with | CPatRecord l -> - let pp (c, p) = - pr_reference c ++ spc() ++ str ":=" ++ pr_patt spc lpattop p - in - (if l = [] then str "{| |}" - else str "{| " ++ prlist_with_sep pr_semicolon pp l ++ str " |}"), lpatrec + pr_record_body "{|" "|}" (pr_patt spc lpattop) l, lpatrec | CPatAlias (p, na) -> pr_patt mt (LevelLe las) p ++ str " as " ++ pr_lname na, las @@ -287,6 +319,7 @@ let tag_var = tag Tag.variable | CPatDelimiters (k,p) -> pr_delimiters k (pr_patt mt lsimplepatt p), 1 + | CPatCast _ -> assert false in @@ -464,11 +497,6 @@ let tag_var = tag Tag.variable pr (LevelLt lapp) a ++ prlist (fun a -> spc () ++ pr_expl_args pr a) l) - let pr_record_body_gen pr l = - spc () ++ - prlist_with_sep pr_semicolon - (fun (id, c) -> pr_reference id ++ str" :=" ++ pr ltop c) l - let pr_forall n = keyword "forall" ++ pr_com_at n ++ spc () let pr_fun n = keyword "fun" ++ pr_com_at n ++ spc () @@ -568,10 +596,7 @@ let tag_var = tag Tag.variable | CApp ((None,a),l) -> return (pr_app (pr mt) a l, lapp) | CRecord l -> - return ( - hv 0 (str"{|" ++ pr_record_body_gen (pr spc) l ++ str" |}"), - latom - ) + return (pr_record_body "{|" "|}" (pr spc ltop) l, latom) | CCases (Constr.LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[{v=([[p]],b)}]) -> return ( hv 0 ( @@ -717,7 +742,5 @@ let tag_var = tag Tag.variable let pr_cases_pattern_expr = pr_patt ltop - let pr_record_body = pr_record_body_gen pr - let pr_binders env sigma = pr_undelimited_binders spc (pr_expr env sigma ltop) diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 2850e4bfa0..02e04573f8 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -41,7 +41,8 @@ val pr_guard_annot -> recursion_order_expr option -> Pp.t -val pr_record_body : (qualid * constr_expr) list -> Pp.t +val pr_record : string -> string -> ('a -> Pp.t) -> 'a list -> Pp.t +val pr_record_body : string -> string -> ('a -> Pp.t) -> (Libnames.qualid * 'a) list -> Pp.t val pr_binders : Environ.env -> Evd.evar_map -> local_binder_expr list -> Pp.t val pr_constr_pattern_expr : Environ.env -> Evd.evar_map -> constr_pattern_expr -> Pp.t val pr_lconstr_pattern_expr : Environ.env -> Evd.evar_map -> constr_pattern_expr -> Pp.t diff --git a/printing/printer.ml b/printing/printer.ml index a1a2d9ae51..bc26caefbe 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -765,9 +765,9 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map v 0 ( int ngoals ++ focused_if_needed ++ str(String.plural ngoals "subgoal") ++ print_extra - ++ str (if (should_gname()) then ", subgoal 1" else "") - ++ (if should_tag() then pr_goal_tag g1 else str"") - ++ pr_goal_name sigma g1 ++ cut () ++ goals + ++ str (if pr_first && (should_gname()) && ngoals > 1 then ", subgoal 1" else "") + ++ (if pr_first && should_tag() then pr_goal_tag g1 else str"") + ++ (if pr_first then pr_goal_name sigma g1 else mt()) ++ cut () ++ goals ++ (if unfocused=[] then str "" else (cut() ++ cut() ++ str "*** Unfocused goals:" ++ cut() ++ pr_rec (List.length rest + 2) unfocused)) diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index dd372ecb0f..b2ebc61b4e 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -514,12 +514,12 @@ let match_goals ot nt = | CHole (k,naming,solve), CHole (k2,naming2,solve2) -> () | CPatVar _, CPatVar _ -> () | CEvar (n,l), CEvar (n2,l2) -> - let oevar = if ogname = "" then Id.to_string n else ogname in - nevar_to_oevar := CString.Map.add (Id.to_string n2) oevar !nevar_to_oevar; + let oevar = if ogname = "" then Id.to_string n.CAst.v else ogname in + nevar_to_oevar := CString.Map.add (Id.to_string n2.CAst.v) oevar !nevar_to_oevar; iter2 (fun x x2 -> let (_, g) = x and (_, g2) = x2 in constr_expr ogname g g2) l l2 | CEvar (n,l), nt' -> (* pass down the old goal evar name *) - match_goals_r (Id.to_string n) nt' nt' + match_goals_r (Id.to_string n.CAst.v) nt' nt' | CSort s, CSort s2 -> () | CCast (c,c'), CCast (c2,c'2) -> constr_expr ogname c c2; diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 3996c64b67..ffae2866c0 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -128,7 +128,7 @@ let classify_vernac e = | Constructors l -> List.map (fun (_,({v=id},_)) -> id) l | RecordDecl (oid,l) -> (match oid with Some {v=x} -> [x] | _ -> []) @ CList.map_filter (function - | AssumExpr({v=Names.Name n},_), _ -> Some n + | AssumExpr({v=Names.Name n},_,_), _ -> Some n | _ -> None) l) l in VtSideff (List.flatten ids, VtLater) | VernacScheme l -> diff --git a/test-suite/bugs/closed/bug_12895.v b/test-suite/bugs/closed/bug_12895.v new file mode 100644 index 0000000000..53adc2981c --- /dev/null +++ b/test-suite/bugs/closed/bug_12895.v @@ -0,0 +1,20 @@ +Fixpoint bug_1 (e1 : nat) {struct e1} + : nat +with bug_2 {H_imp : nat} (e2 : nat) {struct e2} + : nat. +Proof. + - exact e1. + - exact e2. +Admitted. + +Fixpoint hbug_1 (a:bool) (e1 : nat) {struct e1} + : nat +with hbug_2 (a:nat) (e2 : nat) {struct e2} + : nat. +Proof. + - exact e1. + - exact e2. +Admitted. + +Check (hbug_1 : bool -> nat -> nat). +Check (hbug_2 : nat -> nat -> nat). diff --git a/test-suite/bugs/closed/bug_12970.v b/test-suite/bugs/closed/bug_12970.v new file mode 100644 index 0000000000..69ce7ec2c2 --- /dev/null +++ b/test-suite/bugs/closed/bug_12970.v @@ -0,0 +1,4 @@ +Arguments existT _ & _ _. + +Definition f := fun X (A : X -> Type) (P : forall x, A x -> Type) x y => + existT (fun f => forall x, P x (f x)) x y : sigT (fun f => forall x, P x (f x)). diff --git a/test-suite/bugs/closed/bug_13169.v b/test-suite/bugs/closed/bug_13169.v new file mode 100644 index 0000000000..a0b564c725 --- /dev/null +++ b/test-suite/bugs/closed/bug_13169.v @@ -0,0 +1,14 @@ +Goal False. +Proof. + set (H1:=I). + set (x:=true). + assert (H2: x = true) by reflexivity. + set (y:=false). + assert (H3: y = false) by reflexivity. + clearbody H1 x y. + eenough (H4: _ = false). + vm_compute in H4. + (* H4 now has "x:=y" in the evar context. *) + 2: exact H3. + match type of H4 with y = false => idtac end. +Abort. diff --git a/test-suite/bugs/closed/bug_13171.v b/test-suite/bugs/closed/bug_13171.v new file mode 100644 index 0000000000..0564722729 --- /dev/null +++ b/test-suite/bugs/closed/bug_13171.v @@ -0,0 +1,10 @@ +Primitive array := #array_type. + +Goal False. +Proof. + unshelve epose (_:nat). exact_no_check true. + Fail let c := open_constr:([| n | 0 |]) in + let c := eval cbv in c in + let c := type of c in + idtac c. +Abort. diff --git a/test-suite/micromega/int63.v b/test-suite/micromega/int63.v new file mode 100644 index 0000000000..20dfa2631e --- /dev/null +++ b/test-suite/micromega/int63.v @@ -0,0 +1,24 @@ +Require Import ZArith ZifyInt63 Lia. +Require Import Int63. + +Open Scope int63_scope. + +Goal forall (x:int), 0 <= x = true. +Proof. lia. Qed. + +Goal max_int = 9223372036854775807. +Proof. lia. Qed. + +Goal digits = 63. +Proof. lia. Qed. + +Goal wB = (2^63)%Z. +Proof. lia. Qed. + +Goal forall x y, x + y <= max_int = true. +Proof. lia. Qed. + +Goal forall x, x <> 0 -> x / x = 1. +Proof. + nia. +Qed. diff --git a/test-suite/output/Record.out b/test-suite/output/Record.out index d45343fe60..7de1e7d559 100644 --- a/test-suite/output/Record.out +++ b/test-suite/output/Record.out @@ -30,3 +30,43 @@ fun '{| U := T; a := a; q := p |} => (T, p, a) : M -> Type * True * nat fun '{| U := T; a := a; q := p |} => (T, p, a) : M -> Type * True * nat +{| a := 0; b := 0 |} + : T +fun '{| |} => 0 + : LongModuleName.test -> nat + = {| + a := + {| + LongModuleName.long_field_name0 := 0; + LongModuleName.long_field_name1 := 1; + LongModuleName.long_field_name2 := 2; + LongModuleName.long_field_name3 := 3 + |}; + b := + fun + '{| + LongModuleName.long_field_name0 := a; + LongModuleName.long_field_name1 := b; + LongModuleName.long_field_name2 := c; + LongModuleName.long_field_name3 := d + |} => (a, b, c, d) + |} + : T + = {| + a := + {| + long_field_name0 := 0; + long_field_name1 := 1; + long_field_name2 := 2; + long_field_name3 := 3 + |}; + b := + fun + '{| + long_field_name0 := a; + long_field_name1 := b; + long_field_name2 := c; + long_field_name3 := d + |} => (a, b, c, d) + |} + : T diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v index 71a8afa131..13ea37b11e 100644 --- a/test-suite/output/Record.v +++ b/test-suite/output/Record.v @@ -33,3 +33,34 @@ Check fun x:M => let 'D T _ p := x in T. Check fun x:M => let 'D T p := x in (T,p). Check fun x:M => let 'D T a p := x in (T,p,a). Check fun x:M => let '{|U:=T;a:=a;q:=p|} := x in (T,p,a). + +Module FormattingIssue13142. + +Record T {A B} := {a:A;b:B}. + +Module LongModuleName. + Record test := { long_field_name0 : nat; + long_field_name1 : nat; + long_field_name2 : nat; + long_field_name3 : nat }. +End LongModuleName. + +Definition c := + {| LongModuleName.long_field_name0 := 0; + LongModuleName.long_field_name1 := 1; + LongModuleName.long_field_name2 := 2; + LongModuleName.long_field_name3 := 3 |}. + +Definition d := + fun '{| LongModuleName.long_field_name0 := a; + LongModuleName.long_field_name1 := b; + LongModuleName.long_field_name2 := c; + LongModuleName.long_field_name3 := d |} => (a,b,c,d). + +Check {|a:=0;b:=0|}. +Check fun '{| LongModuleName.long_field_name0:=_ |} => 0. +Eval compute in {|a:=c;b:=d|}. +Import LongModuleName. +Eval compute in {|a:=c;b:=d|}. + +End FormattingIssue13142. diff --git a/test-suite/output/goal_output.out b/test-suite/output/goal_output.out index 773533a8d3..17c1aaa55b 100644 --- a/test-suite/output/goal_output.out +++ b/test-suite/output/goal_output.out @@ -2,7 +2,79 @@ Nat.t = nat : Set Nat.t = nat : Set +2 subgoals + + ============================ + True + +subgoal 2 is: + True +2 subgoals, subgoal 1 (?Goal) + + ============================ + True + +subgoal 2 (?Goal0) is: + True 1 subgoal ============================ - False + True +1 subgoal (?Goal0) + + ============================ + True +1 subgoal (?Goal0) + + ============================ + True + +*** Unfocused goals: + +subgoal 2 (?Goal1) is: + True +subgoal 3 (?Goal) is: + True +1 subgoal + + ============================ + True + +*** Unfocused goals: + +subgoal 2 is: + True +subgoal 3 is: + True +This subproof is complete, but there are some unfocused goals. +Focus next goal with bullet -. + +2 subgoals + +subgoal 1 is: + True +subgoal 2 is: + True +This subproof is complete, but there are some unfocused goals. +Focus next goal with bullet -. + +2 subgoals + +subgoal 1 (?Goal0) is: + True +subgoal 2 (?Goal) is: + True +This subproof is complete, but there are some unfocused goals. +Focus next goal with bullet -. + +1 subgoal + +subgoal 1 is: + True +This subproof is complete, but there are some unfocused goals. +Focus next goal with bullet -. + +1 subgoal + +subgoal 1 (?Goal) is: + True diff --git a/test-suite/output/goal_output.v b/test-suite/output/goal_output.v index 327b80b0aa..b1ced94054 100644 --- a/test-suite/output/goal_output.v +++ b/test-suite/output/goal_output.v @@ -6,8 +6,32 @@ Print Nat.t. Timeout 1 Print Nat.t. -Lemma toto: False. Set Printing All. +Lemma toto: True/\True. +Proof. +split. Show. +Set Printing Goal Names. +Show. +Unset Printing Goal Names. +assert True. +- idtac. +Show. +Set Printing Goal Names. +Show. +Set Printing Unfocused. +Show. +Unset Printing Goal Names. +Show. +Unset Printing Unfocused. + auto. +Show. +Set Printing Goal Names. +Show. +Unset Printing Goal Names. +- auto. +Show. +Set Printing Goal Names. +Show. +Unset Printing Goal Names. Abort. - diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v index 998f3f7dd1..73e98ea920 100644 --- a/test-suite/success/Nsatz.v +++ b/test-suite/success/Nsatz.v @@ -1,6 +1,8 @@ Require Import TestSuite.admit. (* compile en user 3m39.915s sur cachalot *) Require Import Nsatz. +Require List. +Import List.ListNotations. (* Example with a generic domain *) @@ -294,7 +296,7 @@ Lemma minh: forall A B C D O E H I:point, Proof. geo_begin. idtac "minh". Time nsatz with radicalmax :=1%N strategy:=1%Z - parameters:=(X O::X B::X C::nil) + parameters:=[X O; X B; X C] variables:= (@nil R). (*Finished transaction in 13. secs (10.102464u,0.s) *) @@ -314,15 +316,15 @@ Proof. geo_begin. idtac "Pappus". Time nsatz with radicalmax :=1%N strategy:=0%Z - parameters:=(X B::X A1::Y A1::X B1::Y B1::X C::Y C1::nil) - variables:= (X B - :: X A1 - :: Y A1 - :: X B1 - :: Y B1 - :: X C - :: Y C1 - :: X C1 :: Y P :: X P :: Y Q :: X Q :: Y S :: X S :: nil). + parameters:=[X B; X A1; Y A1; X B1; Y B1; X C; Y C1] + variables:= [X B; + X A1; + Y A1; + X B1; + Y B1; + X C; + Y C1; + X C1; Y P; X P; Y Q; X Q; Y S; X S]. (*Finished transaction in 8. secs (7.795815u,0.000999999999999s) *) Qed. @@ -347,7 +349,7 @@ Proof. geo_begin. idtac "Simson". Time nsatz with radicalmax :=1%N strategy:=0%Z - parameters:=(X B::Y B::X C::Y C::Y D::nil) + parameters:=[X B; Y B; X C; Y C; Y D] variables:= (@nil R). (* compute -[X Y]. *) (*Finished transaction in 8. secs (7.550852u,0.s) *) @@ -432,20 +434,20 @@ Proof. geo_begin. idtac "Desargues". Time -let lv := rev (X A - :: X B - :: Y B - :: X C - :: Y C - :: Y A1 :: X A1 - :: Y B1 - :: Y C1 - :: X T - :: Y T - :: X Q - :: Y Q :: X P :: Y P :: X C1 :: X B1 :: nil) in +let lv := rev [X A; + X B; + Y B; + X C; + Y C; + Y A1; X A1; + Y B1; + Y C1; + X T; + Y T; + X Q; + Y Q; X P; Y P; X C1; X B1] in nsatz with radicalmax :=1%N strategy:=0%Z - parameters:=(X A::X B::Y B::X C::Y C::X A1::Y B1::Y C1::nil) + parameters:=[X A; X B; Y B; X C; Y C; X A1; Y B1; Y C1] variables:= lv. (*Finished transaction in 8. secs (8.02578u,0.001s)*) Qed. @@ -522,9 +524,9 @@ Lemma hauteurs:forall A B C A1 B1 C1 H:point, geo_begin. idtac "hauteurs". Time - let lv := constr:(Y A1 - :: X A1 :: Y B1 :: X B1 :: Y A :: Y B :: X B :: X A :: X H :: Y C - :: Y C1 :: Y H :: X C1 :: X C :: (@Datatypes.nil R)) in + let lv := constr:([Y A1; + X A1; Y B1; X B1; Y A; Y B; X B; X A; X H; Y C; + Y C1; Y H; X C1; X C]) in nsatz with radicalmax := 2%N strategy := 1%Z parameters := (@Datatypes.nil R) variables := lv. (*Finished transaction in 5. secs (4.360337u,0.008999s)*) diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v index ce07512a1e..beb424dd40 100644 --- a/test-suite/success/Record.v +++ b/test-suite/success/Record.v @@ -93,3 +93,18 @@ Record R : Type := { (* This is used in a couple of development such as UniMatch *) Record S {A:Type} := { a : A; b : forall A:Type, A }. + +(* Bug #13165 on implicit arguments in defined fields *) +Record T := { + f {n:nat} (p:n=n) := nat; + g := f (eq_refl 0) +}. + +(* Slight improvement in when SProp relevance is detected *) +Inductive True : SProp := I. +Inductive eqI : True -> SProp := reflI : eqI I. + +Record U (c:True) := { + u := c; + v := reflI : eqI u; + }. diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 4fa8b3216a..993b7b3ec4 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -459,12 +459,12 @@ Lemma Rplus_eq_0_l : forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 = 0 -> r1 = 0. Proof. intros a b H [H0| H0] H1; auto with real. - absurd (0 < a + b). - rewrite H1; auto with real. - apply Rle_lt_trans with (a + 0). - rewrite Rplus_0_r; assumption. - auto using Rplus_lt_compat_l with real. - rewrite <- H0, Rplus_0_r in H1; assumption. + - absurd (0 < a + b). + + rewrite H1; auto with real. + + apply Rle_lt_trans with (a + 0). + * rewrite Rplus_0_r; assumption. + * auto using Rplus_lt_compat_l with real. + - rewrite <- H0, Rplus_0_r in H1; assumption. Qed. Lemma Rplus_eq_R0 : @@ -1529,7 +1529,7 @@ Qed. Lemma Rinv_1_lt_contravar : forall r1 r2, 1 <= r1 -> r1 < r2 -> / r2 < / r1. Proof. - intros x y H' H'0. + intros x y H' H'0. cut (0 < x); [ intros Lt0 | apply Rlt_le_trans with (r2 := 1) ]; auto with real. apply Rmult_lt_reg_l with (r := x); auto with real. @@ -1753,11 +1753,11 @@ Qed. Lemma INR_IPR : forall p, INR (Pos.to_nat p) = IPR p. Proof. assert (H: forall p, 2 * INR (Pos.to_nat p) = IPR_2 p). - induction p as [p|p|] ; simpl IPR_2. + { induction p as [p|p|] ; simpl IPR_2. rewrite Pos2Nat.inj_xI, S_INR, mult_INR, <- IHp. now rewrite (Rplus_comm (2 * _)). now rewrite Pos2Nat.inj_xO, mult_INR, <- IHp. - apply Rmult_1_r. + apply Rmult_1_r. } intros [p|p|] ; unfold IPR. rewrite Pos2Nat.inj_xI, S_INR, mult_INR, <- H. apply Rplus_comm. @@ -1830,12 +1830,12 @@ Qed. Lemma pow_IZR : forall z n, pow (IZR z) n = IZR (Z.pow z (Z.of_nat n)). Proof. - intros z [|n];simpl;trivial. - rewrite Zpower_pos_nat. - rewrite SuccNat2Pos.id_succ. unfold Zpower_nat;simpl. - rewrite mult_IZR. - induction n;simpl;trivial. - rewrite mult_IZR;ring[IHn]. + intros z [|n];simpl;trivial. + rewrite Zpower_pos_nat. + rewrite SuccNat2Pos.id_succ. unfold Zpower_nat;simpl. + rewrite mult_IZR. + induction n;simpl;trivial. + rewrite mult_IZR;ring[IHn]. Qed. (**********) @@ -2043,7 +2043,7 @@ Proof. Qed. Lemma Ropp_div : forall x y, -x/y = - (x / y). -intros x y; unfold Rdiv; ring. + intros x y; unfold Rdiv; ring. Qed. Lemma Ropp_div_den : forall x y : R, y<>0 -> x / - y = - (x / y). @@ -2068,22 +2068,22 @@ Lemma R_rm : ring_morph 0%R 1%R Rplus Rmult Rminus Ropp eq 0%Z 1%Z Zplus Zmult Zminus Z.opp Zeq_bool IZR. Proof. -constructor ; try easy. -exact plus_IZR. -exact minus_IZR. -exact mult_IZR. -exact opp_IZR. -intros x y H. -apply f_equal. -now apply Zeq_bool_eq. + constructor ; try easy. + - exact plus_IZR. + - exact minus_IZR. + - exact mult_IZR. + - exact opp_IZR. + - intros x y H. + apply f_equal. + now apply Zeq_bool_eq. Qed. Lemma Zeq_bool_IZR x y : IZR x = IZR y -> Zeq_bool x y = true. Proof. -intros H. -apply Zeq_is_eq_bool. -now apply eq_IZR. + intros H. + apply Zeq_is_eq_bool. + now apply eq_IZR. Qed. Add Field RField : Rfield @@ -2127,15 +2127,15 @@ Qed. Lemma Rdiv_lt_0_compat : forall a b, 0 < a -> 0 < b -> 0 < a/b. Proof. -intros; apply Rmult_lt_0_compat;[|apply Rinv_0_lt_compat]; assumption. + intros; apply Rmult_lt_0_compat;[|apply Rinv_0_lt_compat]; assumption. Qed. Lemma Rdiv_plus_distr : forall a b c, (a + b)/c = a/c + b/c. -intros a b c; apply Rmult_plus_distr_r. + intros a b c; apply Rmult_plus_distr_r. Qed. Lemma Rdiv_minus_distr : forall a b c, (a - b)/c = a/c - b/c. -intros a b c; unfold Rminus, Rdiv; rewrite Rmult_plus_distr_r; ring. + intros a b c; unfold Rminus, Rdiv; rewrite Rmult_plus_distr_r; ring. Qed. (* A test for equality function. *) diff --git a/theories/micromega/Zify.v b/theories/micromega/Zify.v index 183fd6a914..01cc9ad810 100644 --- a/theories/micromega/Zify.v +++ b/theories/micromega/Zify.v @@ -16,11 +16,22 @@ Ltac zify_pre_hook := idtac. Ltac zify_post_hook := idtac. -Ltac iter_specs := zify_iter_specs. +Ltac zify_convert_to_euclidean_division_equations_flag := constr:(false). + +(** [zify_internal_to_euclidean_division_equations] is bound in [PreOmega] *) +Ltac zify_internal_to_euclidean_division_equations := idtac. + +Ltac zify_to_euclidean_division_equations := + lazymatch zify_convert_to_euclidean_division_equations_flag with + | true => zify_internal_to_euclidean_division_equations + | false => idtac + end. + Ltac zify := intros; zify_pre_hook ; zify_elim_let ; zify_op ; (zify_iter_specs) ; - zify_saturate ; zify_post_hook. + zify_saturate ; + zify_to_euclidean_division_equations ; zify_post_hook. diff --git a/theories/micromega/ZifyInt63.v b/theories/micromega/ZifyInt63.v new file mode 100644 index 0000000000..27845898aa --- /dev/null +++ b/theories/micromega/ZifyInt63.v @@ -0,0 +1,178 @@ +Require Import ZArith. +Require Import Int63. +Require Import ZifyBool. +Import ZifyClasses. + +Lemma to_Z_bounded : forall x, (0 <= to_Z x < 9223372036854775808)%Z. +Proof. apply to_Z_bounded. Qed. + +Instance Inj_int_Z : InjTyp int Z := + mkinj _ _ to_Z (fun x => 0 <= x < 9223372036854775808)%Z to_Z_bounded. +Add Zify InjTyp Inj_int_Z. + +Instance Op_max_int : CstOp max_int := + { TCst := 9223372036854775807 ; TCstInj := eq_refl }. +Add Zify CstOp Op_max_int. + +Instance Op_digits : CstOp digits := + { TCst := 63 ; TCstInj := eq_refl }. +Add Zify CstOp Op_digits. + +Instance Op_size : CstOp size := + { TCst := 63 ; TCstInj := eq_refl }. +Add Zify CstOp Op_size. + +Instance Op_wB : CstOp wB := + { TCst := 2^63 ; TCstInj := eq_refl }. +Add Zify CstOp Op_wB. + +Lemma ltb_lt : forall n m, + (n <? m)%int63 = (φ (n)%int63 <? φ (m)%int63)%Z. +Proof. + intros. apply Bool.eq_true_iff_eq. + rewrite ltb_spec. rewrite <- Z.ltb_lt. + apply iff_refl. +Qed. + +Instance Op_ltb : BinOp ltb := + {| TBOp := Z.ltb; TBOpInj := ltb_lt |}. +Add Zify BinOp Op_ltb. + +Lemma leb_le : forall n m, + (n <=? m)%int63 = (φ (n)%int63 <=? φ (m)%int63)%Z. +Proof. + intros. apply Bool.eq_true_iff_eq. + rewrite leb_spec. rewrite <- Z.leb_le. + apply iff_refl. +Qed. + +Instance Op_leb : BinOp leb := + {| TBOp := Z.leb; TBOpInj := leb_le |}. +Add Zify BinOp Op_leb. + +Lemma eqb_eq : forall n m, + (n =? m)%int63 = (φ (n)%int63 =? φ (m)%int63)%Z. +Proof. + intros. apply Bool.eq_true_iff_eq. + rewrite eqb_spec. rewrite Z.eqb_eq. + split ; intro H. + now subst; reflexivity. + now apply to_Z_inj in H. +Qed. + +Instance Op_eqb : BinOp eqb := + {| TBOp := Z.eqb; TBOpInj := eqb_eq |}. +Add Zify BinOp Op_eqb. + +Lemma eq_int_inj : forall n m : int, n = m <-> (φ n = φ m)%int63. +Proof. + split; intro H. + rewrite H ; reflexivity. + apply to_Z_inj; auto. +Qed. + +Instance Op_eq : BinRel (@eq int) := + {| TR := @eq Z; TRInj := eq_int_inj |}. +Add Zify BinRel Op_eq. + +Instance Op_add : BinOp add := + {| TBOp := fun x y => (x + y) mod 9223372036854775808%Z; TBOpInj := add_spec |}%Z. +Add Zify BinOp Op_add. + +Instance Op_sub : BinOp sub := + {| TBOp := fun x y => (x - y) mod 9223372036854775808%Z; TBOpInj := sub_spec |}%Z. +Add Zify BinOp Op_sub. + +Instance Op_opp : UnOp Int63.opp := + {| TUOp := (fun x => (- x) mod 9223372036854775808)%Z; TUOpInj := (sub_spec 0) |}%Z. +Add Zify UnOp Op_opp. + +Instance Op_oppcarry : UnOp oppcarry := + {| TUOp := (fun x => 2^63 - x - 1)%Z; TUOpInj := oppcarry_spec |}%Z. +Add Zify UnOp Op_oppcarry. + +Instance Op_succ : UnOp succ := + {| TUOp := (fun x => (x + 1) mod 2^63)%Z; TUOpInj := succ_spec |}%Z. +Add Zify UnOp Op_succ. + +Instance Op_pred : UnOp Int63.pred := + {| TUOp := (fun x => (x - 1) mod 2^63)%Z; TUOpInj := pred_spec |}%Z. +Add Zify UnOp Op_pred. + +Instance Op_mul : BinOp mul := + {| TBOp := fun x y => (x * y) mod 9223372036854775808%Z; TBOpInj := mul_spec |}%Z. +Add Zify BinOp Op_mul. + +Instance Op_gcd : BinOp gcd:= + {| TBOp := (fun x y => Zgcd_alt.Zgcdn (2 * 63)%nat y x) ; TBOpInj := to_Z_gcd |}. +Add Zify BinOp Op_gcd. + +Instance Op_mod : BinOp Int63.mod := + {| TBOp := Z.modulo ; TBOpInj := mod_spec |}. +Add Zify BinOp Op_mod. + +Instance Op_subcarry : BinOp subcarry := + {| TBOp := (fun x y => (x - y - 1) mod 2^63)%Z ; TBOpInj := subcarry_spec |}. +Add Zify BinOp Op_subcarry. + +Instance Op_addcarry : BinOp addcarry := + {| TBOp := (fun x y => (x + y + 1) mod 2^63)%Z ; TBOpInj := addcarry_spec |}. +Add Zify BinOp Op_addcarry. + +Instance Op_lsr : BinOp lsr := + {| TBOp := (fun x y => x / 2^ y)%Z ; TBOpInj := lsr_spec |}. +Add Zify BinOp Op_lsr. + +Instance Op_lsl : BinOp lsl := + {| TBOp := (fun x y => (x * 2^ y) mod 2^ 63)%Z ; TBOpInj := lsl_spec |}. +Add Zify BinOp Op_lsl. + +Instance Op_lor : BinOp Int63.lor := + {| TBOp := Z.lor ; TBOpInj := lor_spec' |}. +Add Zify BinOp Op_lor. + +Instance Op_land : BinOp Int63.land := + {| TBOp := Z.land ; TBOpInj := land_spec' |}. +Add Zify BinOp Op_land. + +Instance Op_lxor : BinOp Int63.lxor := + {| TBOp := Z.lxor ; TBOpInj := lxor_spec' |}. +Add Zify BinOp Op_lxor. + +Instance Op_div : BinOp div := + {| TBOp := Z.div ; TBOpInj := div_spec |}. +Add Zify BinOp Op_div. + +Instance Op_bit : BinOp bit := + {| TBOp := Z.testbit ; TBOpInj := bitE |}. +Add Zify BinOp Op_bit. + +Instance Op_of_Z : UnOp of_Z := + { TUOp := (fun x => x mod 9223372036854775808)%Z; TUOpInj := of_Z_spec }. +Add Zify UnOp Op_of_Z. + +Instance Op_to_Z : UnOp to_Z := + { TUOp := fun x => x ; TUOpInj := fun x : int => eq_refl }. +Add Zify UnOp Op_to_Z. + +Instance Op_is_zero : UnOp is_zero := + { TUOp := (Z.eqb 0) ; TUOpInj := is_zeroE }. +Add Zify UnOp Op_is_zero. + +Lemma is_evenE : forall x, + is_even x = Z.even φ (x)%int63. +Proof. + intros. + generalize (is_even_spec x). + rewrite Z_evenE. + destruct (is_even x). + symmetry. apply Z.eqb_eq. auto. + symmetry. apply Z.eqb_neq. congruence. +Qed. + +Instance Op_is_even : UnOp is_even := + { TUOp := Z.even ; TUOpInj := is_evenE }. +Add Zify UnOp Op_is_even. + + +Ltac Zify.zify_convert_to_euclidean_division_equations_flag ::= constr:(true). diff --git a/theories/omega/PreOmega.v b/theories/omega/PreOmega.v index 506a4108ee..70f25e7243 100644 --- a/theories/omega/PreOmega.v +++ b/theories/omega/PreOmega.v @@ -573,4 +573,6 @@ Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *. Require Import ZifyClasses ZifyInst. Require Zify. +Ltac Zify.zify_internal_to_euclidean_division_equations ::= Z.to_euclidean_division_equations. + Ltac zify := Zify.zify. diff --git a/user-contrib/Ltac2/tac2quote.ml b/user-contrib/Ltac2/tac2quote.ml index b346b3ee5c..90f8008dc2 100644 --- a/user-contrib/Ltac2/tac2quote.ml +++ b/user-contrib/Ltac2/tac2quote.ml @@ -229,7 +229,7 @@ let check_pattern_id ?loc id = let pattern_vars pat = let rec aux () accu pat = match pat.CAst.v with | Constrexpr.CPatVar id - | Constrexpr.CEvar (id, []) -> + | Constrexpr.CEvar ({CAst.v=id}, []) -> let loc = pat.CAst.loc in let () = check_pattern_id ?loc id in Id.Map.add id loc accu diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 401ba0fba4..12194ea20c 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -68,10 +68,12 @@ let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name let inst = instance_of_univ_entry univs in (gr,inst) -let interp_assumption ~program_mode sigma env impls c = +let interp_assumption ~program_mode env sigma impl_env bl c = let flags = { Pretyping.all_no_fail_flags with program_mode } in - let sigma, (ty, impls) = interp_type_evars_impls ~flags env sigma ~impls c in - sigma, (ty, impls) + let sigma, (impls, ((env_bl, ctx), impls1)) = interp_context_evars ~program_mode ~impl_env env sigma bl in + let sigma, (ty, impls2) = interp_type_evars_impls ~flags env_bl sigma ~impls c in + let ty = EConstr.it_mkProd_or_LetIn ty ctx in + sigma, ty, impls1@impls2 (* When monomorphic the universe constraints and universe names are declared with the first declaration only. *) @@ -153,7 +155,7 @@ let do_assumptions ~program_mode ~poly ~scope ~kind nl l = in (* We interpret all declarations in the same evar_map, i.e. as a telescope. *) let (sigma,_,_),l = List.fold_left_map (fun (sigma,env,ienv) (is_coe,(idl,c)) -> - let sigma,(t,imps) = interp_assumption ~program_mode sigma env ienv c in + let sigma,t,imps = interp_assumption ~program_mode env sigma ienv [] c in let r = Retyping.relevance_of_type env sigma t in let env = EConstr.push_named_context (List.map (fun {CAst.v=id} -> LocalAssum (make_annot id r,t)) idl) env in diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 3d425ad768..64b8212b90 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -14,6 +14,15 @@ open Constrexpr (** {6 Parameters/Assumptions} *) +val interp_assumption + : program_mode:bool + -> Environ.env + -> Evd.evar_map + -> Constrintern.internalization_env + -> Constrexpr.local_binder_expr list + -> constr_expr + -> Evd.evar_map * EConstr.t * Impargs.manual_implicits + val do_assumptions : program_mode:bool -> poly:bool diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 37b7106856..c1dbf0a1ea 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -81,14 +81,11 @@ let protect_pattern_in_binder bl c ctypopt = else (bl, c, ctypopt, fun f env evd c -> f env evd c) -let interp_definition ~program_mode pl bl ~poly red_option c ctypopt = +let interp_definition ~program_mode env evd impl_env bl red_option c ctypopt = let flags = Pretyping.{ all_no_fail_flags with program_mode } in - let env = Global.env() in - (* Explicitly bound universes and constraints *) - let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env pl in let (bl, c, ctypopt, apply_under_binders) = protect_pattern_in_binder bl c ctypopt in (* Build the parameters *) - let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars ~program_mode env evd bl in + let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars ~program_mode ~impl_env env evd bl in (* Build the type *) let evd, tyopt = Option.fold_left_map (interp_type_evars_impls ~flags ~impls env_bl) @@ -111,12 +108,15 @@ let interp_definition ~program_mode pl bl ~poly red_option c ctypopt = (* Declare the definition *) let c = EConstr.it_mkLambda_or_LetIn c ctx in let tyopt = Option.map (fun ty -> EConstr.it_mkProd_or_LetIn ty ctx) tyopt in - (c, tyopt), evd, udecl, imps + evd, (c, tyopt), imps let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = let program_mode = false in - let (body, types), evd, udecl, impargs = - interp_definition ~program_mode udecl bl ~poly red_option c ctypopt + let env = Global.env() in + (* Explicitly bound universes and constraints *) + let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env udecl in + let evd, (body, types), impargs = + interp_definition ~program_mode env evd empty_internalization_env bl red_option c ctypopt in let kind = Decls.IsDefinition kind in let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types () in @@ -127,8 +127,11 @@ let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = let program_mode = true in - let (body, types), evd, udecl, impargs = - interp_definition ~program_mode udecl bl ~poly red_option c ctypopt + let env = Global.env() in + (* Explicitly bound universes and constraints *) + let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env udecl in + let evd, (body, types), impargs = + interp_definition ~program_mode env evd empty_internalization_env bl red_option c ctypopt in let term, typ, uctx, obls = Declare.Obls.prepare_obligation ~name ~body ~types evd in let pm, _ = diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index d95e64a85f..7420235449 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -14,6 +14,17 @@ open Constrexpr (** {6 Definitions/Let} *) +val interp_definition + : program_mode:bool + -> Environ.env + -> Evd.evar_map + -> Constrintern.internalization_env + -> Constrexpr.local_binder_expr list + -> red_expr option + -> constr_expr + -> constr_expr option + -> Evd.evar_map * (EConstr.t * EConstr.t option) * Impargs.manual_implicits + val do_definition : ?hook:Declare.Hook.t -> name:Id.t diff --git a/vernac/declare.ml b/vernac/declare.ml index ae7878b615..5274a6da3b 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -1854,7 +1854,8 @@ module MutualEntry : sig val declare_variable : pinfo:Proof_info.t -> uctx:UState.t - -> Entries.parameter_entry + -> sec_vars:Id.Set.t option + -> univs:Entries.universes_entry -> Names.GlobRef.t list val declare_mutdef @@ -1920,10 +1921,11 @@ end = struct in List.map_i (declare_mutdef ~pinfo ~uctx pe) 0 pinfo.Proof_info.cinfo - let declare_variable ~pinfo ~uctx pe = + let declare_variable ~pinfo ~uctx ~sec_vars ~univs = let { Info.scope; hook } = pinfo.Proof_info.info in List.map_i ( fun i { CInfo.name; typ; impargs } -> + let pe = (sec_vars, (typ, univs), None) in declare_assumption ~name ~scope ~hook ~impargs ~uctx pe ) 0 pinfo.Proof_info.cinfo @@ -1953,8 +1955,8 @@ let compute_proof_using_for_admitted proof typ pproofs = Some (Environ.really_needed env (Id.Set.union ids_typ ids_def)) | _ -> None -let finish_admitted ~pm ~pinfo ~uctx pe = - let cst = MutualEntry.declare_variable ~pinfo ~uctx pe in +let finish_admitted ~pm ~pinfo ~uctx ~sec_vars ~univs = + let cst = MutualEntry.declare_variable ~pinfo ~uctx ~sec_vars ~univs in (* If the constant was an obligation we need to update the program map *) match CEphemeron.get pinfo.Proof_info.proof_ending with | Proof_ending.End_obligation oinfo -> @@ -1974,7 +1976,7 @@ let save_admitted ~pm ~proof = let sec_vars = compute_proof_using_for_admitted proof typ pproofs in let uctx = get_initial_euctx proof in let univs = UState.check_univ_decl ~poly uctx udecl in - finish_admitted ~pm ~pinfo:proof.pinfo ~uctx (sec_vars, (typ, univs), None) + finish_admitted ~pm ~pinfo:proof.pinfo ~uctx ~sec_vars ~univs (************************************************************************) (* Saving a lemma-like constant *) @@ -2097,12 +2099,9 @@ let save_lemma_admitted_delayed ~pm ~proof ~pinfo = let poly = match proof_entry_universes with | Entries.Monomorphic_entry _ -> false | Entries.Polymorphic_entry (_, _) -> true in - let typ = match proof_entry_type with - | None -> CErrors.user_err Pp.(str "Admitted requires an explicit statement"); - | Some typ -> typ in - let ctx = UState.univ_entry ~poly uctx in + let univs = UState.univ_entry ~poly uctx in let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in - finish_admitted ~pm ~uctx ~pinfo (sec_vars, (typ, ctx), None) + finish_admitted ~pm ~uctx ~pinfo ~sec_vars ~univs let save_lemma_proved_delayed ~pm ~proof ~pinfo ~idopt = (* vio2vo calls this but with invalid info, we have to workaround diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 49d4847fde..dfc7b05b51 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -429,19 +429,19 @@ GRAMMAR EXTEND Gram ; record_binder_body: [ [ l = binders; oc = of_type_with_opt_coercion; - t = lconstr -> { fun id -> (oc,AssumExpr (id,mkProdCN ~loc l t)) } + t = lconstr -> { fun id -> (oc,AssumExpr (id,l,t)) } | l = binders; oc = of_type_with_opt_coercion; t = lconstr; ":="; b = lconstr -> { fun id -> - (oc,DefExpr (id,mkLambdaCN ~loc l b,Some (mkProdCN ~loc l t))) } + (oc,DefExpr (id,l,b,Some t)) } | l = binders; ":="; b = lconstr -> { fun id -> match b.CAst.v with | CCast(b', (CastConv t|CastVM t|CastNative t)) -> - (NoInstance,DefExpr(id,mkLambdaCN ~loc l b',Some (mkProdCN ~loc l t))) + (NoInstance,DefExpr(id,l,b',Some t)) | _ -> - (NoInstance,DefExpr(id,mkLambdaCN ~loc l b,None)) } ] ] + (NoInstance,DefExpr(id,l,b,None)) } ] ] ; record_binder: - [ [ id = name -> { (NoInstance,AssumExpr(id, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) } + [ [ id = name -> { (NoInstance,AssumExpr(id, [], CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) } | id = name; f = record_binder_body -> { f id } ] ] ; assum_list: diff --git a/vernac/himsg.ml b/vernac/himsg.ml index a9de01bfd0..5f7eb78a40 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -866,7 +866,7 @@ let explain_unsatisfiable_constraints env sigma constr comp = let info = Evar.Map.find ev undef in explain_typeclass_resolution env sigma info k ++ fnl () ++ cstr -let explain_pretype_error env sigma err = +let rec explain_pretype_error env sigma err = let env = Evardefine.env_nf_betaiotaevar sigma env in let env = make_all_name_different env sigma in match err with @@ -893,7 +893,7 @@ let explain_pretype_error env sigma err = | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type env sigma m n | CannotFindWellTypedAbstraction (p,l,e) -> explain_cannot_find_well_typed_abstraction env sigma p l - (Option.map (fun (env',e) -> explain_type_error env' sigma e) e) + (Option.map (fun (env',e) -> explain_pretype_error env' sigma e) e) | WrongAbstractionType (n,a,t,u) -> explain_wrong_abstraction_type env sigma n a t u | AbstractionOverMeta (m,n) -> explain_abstraction_over_meta env m n diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index f972e05d3b..0e660bf20c 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -508,13 +508,15 @@ let pr_oc = function let pr_record_field (x, { rf_subclass = oc ; rf_priority = pri ; rf_notation = ntn }) = let prx = match x with - | AssumExpr (id,t) -> + | AssumExpr (id,binders,t) -> hov 1 (pr_lname id ++ + pr_binders_arg binders ++ spc() ++ pr_oc oc ++ spc() ++ pr_lconstr_expr t) - | DefExpr(id,b,opt) -> (match opt with + | DefExpr(id,binders,b,opt) -> (match opt with | Some t -> hov 1 (pr_lname id ++ + pr_binders_arg binders ++ spc() ++ pr_oc oc ++ spc() ++ pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b) | None -> @@ -524,8 +526,7 @@ let pr_record_field (x, { rf_subclass = oc ; rf_priority = pri ; rf_notation = n prx ++ prpri ++ prlist (pr_decl_notation @@ pr_constr) ntn let pr_record_decl c fs = - pr_opt pr_lident c ++ (if c = None then str"{" else str" {") ++ - hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}") + pr_opt pr_lident c ++ pr_record "{" "}" pr_record_field fs let pr_printable = function | PrintFullContext -> @@ -966,7 +967,7 @@ let pr_vernac_expr v = str":" ++ spc () ++ pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info ++ (match props with - | Some (true, { v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}" + | Some (true, { v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ pr_record_body "{" "}" pr_lconstr l | Some (true,_) -> assert false | Some (false,p) -> spc () ++ str":=" ++ spc () ++ pr_constr p | None -> mt())) diff --git a/vernac/record.ml b/vernac/record.ml index e362cb052a..a4bf9893d9 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -62,23 +62,33 @@ let () = let interp_fields_evars env sigma ~ninds ~nparams impls_env nots l = let _, sigma, impls, newfs, _ = List.fold_left2 - (fun (env, sigma, uimpls, params, impls) no ({CAst.loc;v=i}, b, t) -> - let sigma, (t', impl) = interp_type_evars_impls env sigma ~impls t in - let r = Retyping.relevance_of_type env sigma t' in - let sigma, b' = - Option.cata (fun x -> on_snd (fun x -> Some (fst x)) @@ - interp_casted_constr_evars_impls ~program_mode:false env sigma ~impls x t') (sigma,None) b in - let impls = + (fun (env, sigma, uimpls, params, impls_env) no d -> + let sigma, (i, b, t), impl = match d with + | Vernacexpr.AssumExpr({CAst.loc;v=id},bl,t) -> + (* Temporary compatibility with the type-classes heuristics *) + (* which are applied after the interpretation of bl and *) + (* before the one of t otherwise (see #13166) *) + let t = if bl = [] then t else mkCProdN bl t in + let sigma, t, impl = + ComAssumption.interp_assumption ~program_mode:false env sigma impls_env [] t in + sigma, (id, None, t), impl + | Vernacexpr.DefExpr({CAst.loc;v=id},bl,b,t) -> + let sigma, (b, t), impl = + ComDefinition.interp_definition ~program_mode:false env sigma impls_env bl None b t in + let t = match t with Some t -> t | None -> Retyping.get_type_of env sigma b in + sigma, (id, Some b, t), impl in + let r = Retyping.relevance_of_type env sigma t in + let impls_env = match i with - | Anonymous -> impls - | Name id -> Id.Map.add id (compute_internalization_data env sigma id Constrintern.Method t' impl) impls + | Anonymous -> impls_env + | Name id -> Id.Map.add id (compute_internalization_data env sigma id Constrintern.Method t impl) impls_env in - let d = match b' with - | None -> LocalAssum (make_annot i r,t') - | Some b' -> LocalDef (make_annot i r,b',t') + let d = match b with + | None -> LocalAssum (make_annot i r,t) + | Some b -> LocalDef (make_annot i r,b,t) in - List.iter (Metasyntax.set_notation_for_interpretation env impls) no; - (EConstr.push_rel d env, sigma, impl :: uimpls, d::params, impls)) + List.iter (Metasyntax.set_notation_for_interpretation env impls_env) no; + (EConstr.push_rel d env, sigma, impl :: uimpls, d::params, impls_env)) (env, sigma, [], [], impls_env) nots l in let _, _, sigma = Context.Rel.fold_outside ~init:(env,0,sigma) (fun f (env,k,sigma) -> @@ -101,14 +111,6 @@ let compute_constructor_level evars env l = in (EConstr.push_rel d env, univ)) l (env, Univ.Universe.sprop) -let binder_of_decl = function - | Vernacexpr.AssumExpr(n,t) -> (n,None,t) - | Vernacexpr.DefExpr(n,c,t) -> - (n,Some c, match t with Some c -> c - | None -> CAst.make ?loc:n.CAst.loc @@ CHole (None, Namegen.IntroAnonymous, None)) - -let binders_of_decls = List.map binder_of_decl - let check_anonymous_type ind = match ind with | { CAst.v = CSort (Glob_term.UAnonymous {rigid=true}) } -> true @@ -176,7 +178,7 @@ let typecheck_params_and_fields def poly pl ps records = let ninds = List.length arities in let nparams = List.length newps in let fold sigma (_, _, nots, fs) arity = - interp_fields_evars env_ar sigma ~ninds ~nparams impls_env nots (binders_of_decls fs) + interp_fields_evars env_ar sigma ~ninds ~nparams impls_env nots fs in let (sigma, data) = List.fold_left2_map fold sigma records arities in let sigma = @@ -676,8 +678,8 @@ open Vernacexpr let check_unique_names records = let extract_name acc (rf_decl, _) = match rf_decl with - Vernacexpr.AssumExpr({CAst.v=Name id},_) -> id::acc - | Vernacexpr.DefExpr ({CAst.v=Name id},_,_) -> id::acc + Vernacexpr.AssumExpr({CAst.v=Name id},_,_) -> id::acc + | Vernacexpr.DefExpr ({CAst.v=Name id},_,_,_) -> id::acc | _ -> acc in let allnames = List.fold_left (fun acc (_, id, _, cfs, _, _) -> diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 0d3f38d139..3ced38d6ea 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -700,7 +700,7 @@ let vernac_record ~template udecl ~cumulative k ~poly finite records = if Dumpglob.dump () then let () = Dumpglob.dump_definition id false "rec" in let iter (x, _) = match x with - | Vernacexpr.AssumExpr ({loc;v=Name id}, _) -> + | Vernacexpr.(AssumExpr ({loc;v=Name id}, _, _) | DefExpr ({loc;v=Name id}, _, _, _)) -> Dumpglob.dump_definition (make ?loc id) false "proj" | _ -> () in @@ -777,7 +777,7 @@ let vernac_inductive ~atts kind indl = in let (coe, (lid, ce)) = l in let coe' = if coe then BackInstance else NoInstance in - let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce), + let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), [], ce), { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true } in vernac_record ~template udecl ~cumulative (Class true) ~poly finite [id, bl, c, None, [f]] else if List.for_all is_record indl then diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index eeebb43114..6a9a74144f 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -167,8 +167,8 @@ type fixpoint_expr = recursion_order_expr option fix_expr_gen type cofixpoint_expr = unit fix_expr_gen type local_decl_expr = - | AssumExpr of lname * constr_expr - | DefExpr of lname * constr_expr * constr_expr option + | AssumExpr of lname * local_binder_expr list * constr_expr + | DefExpr of lname * local_binder_expr list * constr_expr * constr_expr option type inductive_kind = Inductive_kw | CoInductive | Variant | Record | Structure | Class of bool (* true = definitional, false = inductive *) type simple_binder = lident list * constr_expr |