diff options
103 files changed, 1558 insertions, 921 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 5dd3760793..04b75bfdf6 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -26,7 +26,7 @@ variables: COQIDE_PACKAGES: "libgtk2.0-dev libgtksourceview2.0-dev" #COQIDE_PACKAGES_32BIT: "libgtk2.0-dev:i386 libgtksourceview2.0-dev:i386" COQIDE_OPAM: "lablgtk-extras" - COQIDE_OPAM_BE: "num lablgtk.2.18.6 lablgtk-extras.1.6" + COQIDE_OPAM_BE: "lablgtk.2.18.6 lablgtk-extras.1.6" COQDOC_PACKAGES: "texlive-latex-base texlive-latex-recommended texlive-latex-extra texlive-math-extra texlive-fonts-recommended texlive-fonts-extra latex-xcolor ghostscript transfig imagemagick tipa" COQDOC_OPAM: "hevea" @@ -49,7 +49,7 @@ before_script: - opam switch ${COMPILER} - eval $(opam config env) - opam config list - - opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind ${EXTRA_OPAM} + - opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind num ${EXTRA_OPAM} - rm -rf ~/.opam/log/ - opam list @@ -57,6 +57,9 @@ Tactics - A bug fixed in "rewrite H in *" and "rewrite H in * |-" may cause a few rare incompatibilities (it was unintendedly recursively rewriting in the side conditions generated by H). +- Added tactics "assert_succeeds tac" and "assert_fails tac" to ensure + properties of the executation of a tactic without keeping the effect + of the execution. Focusing @@ -75,6 +78,8 @@ Vernacular Commands - For the Extraction Language command, "OCaml" is spelled correctly. The older "Ocaml" is still accepted, but deprecated. - Using “Require” inside a section is deprecated. +- An experimental command "Show Extraction" allows to extract the content + of the current ongoing proof (grant wish #4129). Universes @@ -107,6 +112,12 @@ CoqIDE - Find and Replace All report the number of occurrences found; Find indicates when it wraps. +coqdep + +- Learned to read -I, -Q, -R and filenames from _CoqProject files. + This is used by coq_makefile when generating dependencies for .v + files (but not other files). + Documentation - The Coq FAQ, formerly located at https://coq.inria.fr/faq, has been diff --git a/Makefile.build b/Makefile.build index f583c33378..ffe6057574 100644 --- a/Makefile.build +++ b/Makefile.build @@ -386,21 +386,16 @@ coqbinaries: $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE) coqbyte: $(COQTOPBYTE) $(CHICKENBYTE) -COQTOP_OPT_MLTOP=toplevel/coqtop_opt_bin.cmx -COQTOP_BYTE_MLTOP=toplevel/coqtop_byte_bin.cmo - -$(COQTOP_BYTE_MLTOP): toplevel/coqtop_byte_bin.ml - $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -package compiler-libs.toplevel -c $< +COQTOP_OPT=toplevel/coqtop_opt_bin.ml +COQTOP_BYTE=toplevel/coqtop_byte_bin.ml ifeq ($(BEST),opt) -$(COQTOPEXE): $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) $(COQTOP_OPT_MLTOP) +$(COQTOPEXE): $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) $(COQTOP_OPT) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(OCAMLOPT) -linkall -linkpkg -I toplevel \ + $(HIDE)$(OCAMLOPT) -linkall -linkpkg -I vernac -I toplevel \ -I kernel/byterun/ -cclib -lcoqrun \ - $(SYSMOD) -package camlp5.gramlib \ - $(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) \ - $(COQTOP_OPT_MLTOP) toplevel/coqtop_bin.ml -o $@ + $(SYSMOD) -package camlp5.gramlib \ + $(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) $(COQTOP_OPT) -o $@ $(STRIP) $@ $(CODESIGN) $@ else @@ -409,13 +404,12 @@ $(COQTOPEXE): $(COQTOPBYTE) endif # VMBYTEFLAGS will either contain -custom of the right -dllpath for the VM -$(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(COQTOP_BYTE_MLTOP) +$(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(COQTOP_BYTE) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(OCAMLC) -linkall -linkpkg -I toplevel \ + $(HIDE)$(OCAMLC) -linkall -linkpkg -I lib -I vernac -I toplevel \ -I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \ - $(SYSMOD) -package camlp5.gramlib,compiler-libs.toplevel \ - $(LINKCMO) $(BYTEFLAGS) \ - $(COQTOP_BYTE_MLTOP) toplevel/coqtop_bin.ml -o $@ + $(SYSMOD) -package camlp5.gramlib,compiler-libs.toplevel \ + $(LINKCMO) $(BYTEFLAGS) $(COQTOP_BYTE) -o $@ # For coqc COQCCMO:=clib/clib.cma lib/lib.cma toplevel/usage.cmo tools/coqc.cmo diff --git a/checker/checker.ml b/checker/checker.ml index b2aeb1f144..fd2725c859 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -17,10 +17,10 @@ open Check let () = at_exit flush_all -let chk_pp = Pp.pp_with Format.std_formatter +let pp_arrayi pp fmt a = Array.iteri (fun i x -> pp fmt (i,x)) a let fatal_error info anomaly = - flush_all (); Format.eprintf "@[Fatal Error: @[%a@]@]%!@\n" Pp.pp_with info; flush_all (); + flush_all (); Format.eprintf "@[Fatal Error: @[%a@]@]@\n%!" Pp.pp_with info; flush_all (); exit (if anomaly then 129 else 1) let coq_root = Id.of_string "Coq" @@ -269,26 +269,26 @@ let explain_exn = function | Generalization _ -> str"Generalization" | ActualType _ -> str"ActualType" | CantApplyBadType ((n,a,b),(hd,hdty),args) -> - Format.printf "====== ill-typed term ====@\n"; - Format.printf "@[<hov 2>application head=@ "; - Print.print_pure_constr hd; - Format.printf "@]@\n@[<hov 2>head type=@ "; - Print.print_pure_constr hdty; - Format.printf "@]@\narguments:@\n@[<hv>"; - Array.iteri (fun i (t,ty) -> - Format.printf "@[<hov 2>arg %d=@ " (i+1); - Print.print_pure_constr t; - Format.printf "@ type=@ "; - Print.print_pure_constr ty) args; - Format.printf "@]@\n====== type error ====@\n"; - Print.print_pure_constr b; - Format.printf "@\nis not convertible with@\n"; - Print.print_pure_constr a; - Format.printf "@\n====== universes ====@\n"; - chk_pp - (Univ.pr_universes - (ctx.Environ.env_stratification.Environ.env_universes)); - str "\nCantApplyBadType at argument " ++ int n + (* This mix of printf / pp was here before... *) + let fmt = Format.std_formatter in + let open Format in + let open Print in + fprintf fmt "====== ill-typed term ====@\n"; + fprintf fmt "@[<hov 2>application head=@ %a@]@\n" print_pure_constr hd; + fprintf fmt "@[<hov 2>head type=@ %a@]@\n" print_pure_constr hdty; + let pp_arg fmt (i,(t,ty)) = fprintf fmt "@[<hv>@[<1>arg %d=@ @[%a@]@]@,@[<1>type=@ @[%a@]@]@]@\n@," (i+1) + print_pure_constr t print_pure_constr ty + in + fprintf fmt "arguments:@\n@[<hv>%a@]@\n" (pp_arrayi pp_arg) args; + fprintf fmt "====== type error ====@\n"; + fprintf fmt "%a@\n" print_pure_constr b; + fprintf fmt "is not convertible with@\n"; + fprintf fmt "%a@\n" print_pure_constr a; + fprintf fmt "====== universes ====@\n"; + fprintf fmt "%a@\n%!" Pp.pp_with + (Univ.pr_universes + (ctx.Environ.env_stratification.Environ.env_universes)); + str "CantApplyBadType at argument " ++ int n | CantApplyNonFunctional _ -> str"CantApplyNonFunctional" | IllFormedRecBody _ -> str"IllFormedRecBody" | IllTypedRecBody _ -> str"IllTypedRecBody" diff --git a/checker/print.ml b/checker/print.ml index c1fa8f94c5..fc9cd687e8 100644 --- a/checker/print.ml +++ b/checker/print.ml @@ -12,137 +12,85 @@ open Format open Cic open Names -let chk_pp = Pp.pp_with Format.std_formatter +let chk_pp fmt = Pp.pp_with fmt +let pp_arrayi pp fmt a = Array.iteri (fun i x -> pp fmt (i,x)) a +let pp_instance fmt i = chk_pp fmt (Univ.Instance.pr i) +let pp_id fmt id = fprintf fmt "%s" (Id.to_string id) -let print_instance i = chk_pp (Univ.Instance.pr i) - -let print_pure_constr csr = - let rec term_display c = match c with - | Rel n -> print_string "#"; print_int n - | Meta n -> print_string "Meta("; print_int n; print_string ")" - | Var id -> print_string (Id.to_string id) - | Sort s -> sort_display s - | Cast (c,_, t) -> open_hovbox 1; - print_string "("; (term_display c); print_cut(); - print_string "::"; (term_display t); print_string ")"; close_box() +let print_pure_constr fmt csr = + let rec pp_term fmt c = match c with + | Rel n -> fprintf fmt "#%d" n + | Meta n -> fprintf fmt "Meta(%d)" n + | Var id -> pp_id fmt id + | Sort s -> pp_sort fmt s + | Cast (c,_, t) -> + fprintf fmt "@[<hov 1>(%a@;::%a)@]" pp_term c pp_term t | Prod (Name(id),t,c) -> - open_hovbox 1; - print_string"("; print_string (Id.to_string id); - print_string ":"; box_display t; - print_string ")"; print_cut(); - box_display c; close_box() + fprintf fmt "@[<hov 1>(%a:%a)@;@[%a@]@]" pp_id id pp_term t pp_term c | Prod (Anonymous,t,c) -> - print_string"("; box_display t; print_cut(); print_string "->"; - box_display c; print_string ")"; + fprintf fmt "(%a@,->@[%a@])" pp_term t pp_term c | Lambda (na,t,c) -> - print_string "["; name_display na; - print_string ":"; box_display t; print_string "]"; - print_cut(); box_display c; + fprintf fmt "[%a:@[%a@]]@,@[%a@]" pp_name na pp_term t pp_term c | LetIn (na,b,t,c) -> - print_string "["; name_display na; print_string "="; - box_display b; print_cut(); - print_string ":"; box_display t; print_string "]"; - print_cut(); box_display c; + fprintf fmt "[%a=@[%a@]@,:@[%a@]]@,@[%a@]" pp_name na pp_term b pp_term t pp_term c | App (c,l) -> - print_string "("; - box_display c; - Array.iter (fun x -> print_space (); box_display x) l; - print_string ")" - | Evar _ -> print_string "Evar#" - | Const (c,u) -> print_string "Cons("; - sp_con_display c; - print_string ","; print_instance u; - print_string ")" + fprintf fmt "(@[%a@]@, @[<hov 1>%a@])" pp_term c (pp_arrayi (fun _ (_,s) -> fprintf fmt "@[%a@]@," pp_term s)) l; + | Evar _ -> pp_print_string fmt "Evar#" + | Const (c,u) -> + fprintf fmt "Cons(@[%a,%a@])" sp_con_display c pp_instance u | Ind ((sp,i),u) -> - print_string "Ind("; - sp_display sp; - print_string ","; print_int i; - print_string ","; print_instance u; - print_string ")" + fprintf fmt "Ind(@[%a,%d,%a@])" sp_display sp i pp_instance u | Construct (((sp,i),j),u) -> - print_string "Constr("; - sp_display sp; - print_string ","; - print_int i; print_string ","; print_int j; - print_string ","; print_instance u; print_string ")" + fprintf fmt "Constr(%a,%d,%d,%a)" sp_display sp i j pp_instance u | Case (ci,p,c,bl) -> - open_vbox 0; - print_string "<"; box_display p; print_string ">"; - print_cut(); print_string "Case"; - print_space(); box_display c; print_space (); print_string "of"; - open_vbox 0; - Array.iter (fun x -> print_cut(); box_display x) bl; - close_box(); - print_cut(); - print_string "end"; - close_box() + let pp_match fmt (_,mc) = fprintf fmt " @[%a@]" pp_term mc in + fprintf fmt "@[<v><@[%a@]>@,Case@ @[%a@]@ of@[<v>%a@]@,end@]" pp_term p pp_term c (pp_arrayi pp_match) bl | Fix ((t,i),(lna,tl,bl)) -> - print_string "Fix("; print_int i; print_string ")"; - print_cut(); - open_vbox 0; - let print_fix () = - for k = 0 to (Array.length tl) - 1 do - open_vbox 0; - name_display lna.(k); print_string "/"; - print_int t.(k); print_cut(); print_string ":"; - box_display tl.(k) ; print_cut(); print_string ":="; - box_display bl.(k); close_box (); - print_cut() - done - in print_string"{"; print_fix(); print_string"}" + let pp_fixc fmt (k,_) = + fprintf fmt "@[<v 0> %a/%d@,:@[%a@]@,:=@[%a@]@]@," pp_name lna.(k) t.(k) pp_term tl.(k) pp_term bl.(k) in + fprintf fmt "Fix(%d)@,@[<v>{%a}@]" i (pp_arrayi pp_fixc) tl | CoFix(i,(lna,tl,bl)) -> - print_string "CoFix("; print_int i; print_string ")"; - print_cut(); - open_vbox 0; - let print_fix () = - for k = 0 to (Array.length tl) - 1 do - open_vbox 1; - name_display lna.(k); print_cut(); print_string ":"; - box_display tl.(k) ; print_cut(); print_string ":="; - box_display bl.(k); close_box (); - print_cut(); - done - in print_string"{"; print_fix (); print_string"}" + let pp_fixc fmt (k,_) = + fprintf fmt "@[<v 0> %a@,:@[%a@]@,:=@[%a@]@]@," pp_name lna.(k) pp_term tl.(k) pp_term bl.(k) in + fprintf fmt "CoFix(%d)@,@[<v>{%a}@]" i (pp_arrayi pp_fixc) tl | Proj (p, c) -> - print_string "Proj("; sp_con_display (Projection.constant p); print_string ","; - box_display c; print_string ")" + fprintf fmt "Proj(%a,@,@[%a@])" sp_con_display (Projection.constant p) pp_term c - and box_display c = open_hovbox 1; term_display c; close_box() + and pp_sort fmt = function + | Prop(Pos) -> pp_print_string fmt "Set" + | Prop(Null) -> pp_print_string fmt "Prop" + | Type u -> fprintf fmt "Type(%a)" chk_pp (Univ.pr_uni u) - and sort_display = function - | Prop(Pos) -> print_string "Set" - | Prop(Null) -> print_string "Prop" - | Type u -> print_string "Type("; chk_pp (Univ.pr_uni u); print_string ")" + and pp_name fmt = function + | Name id -> pp_id fmt id + | Anonymous -> pp_print_string fmt "_" - and name_display = function - | Name id -> print_string (Id.to_string id) - | Anonymous -> print_string "_" (* Remove the top names for library and Scratch to avoid long names *) - and sp_display sp = -(* let dir,l = decode_kn sp in + and sp_display fmt sp = +(* let dir,l = decode_kn sp in let ls = match List.rev_map Id.to_string (DirPath.repr dir) with ("Top"::l)-> l | ("Coq"::_::l) -> l | l -> l in List.iter (fun x -> print_string x; print_string ".") ls;*) - print_string (MutInd.debug_to_string sp) - and sp_con_display sp = -(* let dir,l = decode_kn sp in + pp_print_string fmt (MutInd.debug_to_string sp) + + and sp_con_display fmt sp = + (* + let dir,l = decode_kn sp in let ls = match List.rev_map Id.to_string (DirPath.repr dir) with ("Top"::l)-> l | ("Coq"::_::l) -> l | l -> l in List.iter (fun x -> print_string x; print_string ".") ls;*) - print_string (Constant.debug_to_string sp) + pp_print_string fmt (Constant.debug_to_string sp) in - try - box_display csr; print_flush() - with e -> - print_string (Printexc.to_string e);print_flush (); - raise e - - - + try + fprintf fmt "@[%a@]%!" pp_term csr + with e -> + pp_print_string fmt (Printexc.to_string e); + print_flush (); + raise e diff --git a/checker/print.mli b/checker/print.mli index 67562125f7..da1362ca5c 100644 --- a/checker/print.mli +++ b/checker/print.mli @@ -10,4 +10,4 @@ open Cic -val print_pure_constr : constr -> unit +val print_pure_constr : Format.formatter -> constr -> unit diff --git a/checker/reduction.ml b/checker/reduction.ml index 67d00b21d9..97255dd49e 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -201,7 +201,9 @@ let convert_constructors if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then convert_universes univs u1 u2 else - convert_inductive_instances CONV cumi u1 u2 univs + (** By invariant, both constructors have a common supertype, + so they are convertible _at that type_. *) + () (* Convertibility of sorts *) diff --git a/clib/option.ml b/clib/option.ml index 21913e8f7a..32fe2fc5f5 100644 --- a/clib/option.ml +++ b/clib/option.ml @@ -52,6 +52,9 @@ let get = function (** [make x] returns [Some x]. *) let make x = Some x +(** [bind x f] is [f y] if [x] is [Some y] and [None] otherwise *) +let bind x f = match x with Some y -> f y | None -> None + (** [init b x] returns [Some x] if [b] is [true] and [None] otherwise. *) let init b x = if b then diff --git a/clib/option.mli b/clib/option.mli index 2260993526..67b42268a7 100644 --- a/clib/option.mli +++ b/clib/option.mli @@ -43,6 +43,9 @@ val get : 'a option -> 'a (** [make x] returns [Some x]. *) val make : 'a -> 'a option +(** [bind x f] is [f y] if [x] is [Some y] and [None] otherwise *) +val bind : 'a option -> ('a -> 'b option) -> 'b option + (** [init b x] returns [Some x] if [b] is [true] and [None] otherwise. *) val init : bool -> 'a -> 'a option diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 0a4d0ef9aa..3ed697d8be 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -156,6 +156,8 @@ is understood as & | & {\tt type\_term} {\term}\\ & | & {\tt numgoals} \\ & | & {\tt guard} {\it test}\\ +& | & {\tt assert\_fails} {\tacexprpref}\\ +& | & {\tt assert\_succeds} {\tacexprpref}\\ & | & \atomictac\\ & | & {\qualid} \nelist{\tacarg}{}\\ & | & {\atom} @@ -598,6 +600,22 @@ The experimental status of this tactic pertains to the fact if $v$ performs side \ErrMsg \errindex{This tactic has more than one success} +\subsubsection[Checking the failure]{Checking the failure\tacindex{assert\_fails}\index{Tacticals!assert\_fails@{\tt assert\_fails}}} + +Coq provides a derived tactic to check that a tactic \emph{fails}: +\begin{quote} +{\tt assert\_fails} {\tacexpr} +\end{quote} +This behaves like {\tt tryif {\tacexpr} then fail 0 tac "succeeds" else idtac}. + +\subsubsection[Checking the success]{Checking the success\tacindex{assert\_succeeds}\index{Tacticals!assert\_succeeds@{\tt assert\_succeeds}}} + +Coq provides a derived tactic to check that a tactic has \emph{at least one} success: +\begin{quote} +{\tt assert\_succeeds} {\tacexpr} +\end{quote} +This behaves like {\tt tryif (assert\_fails tac) then fail 0 tac "fails" else idtac}. + \subsubsection[Solving]{Solving\tacindex{solve} \index{Tacticals!solve@{\tt solve}}} diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index a2739e457e..8c09b23a5a 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -598,5 +598,6 @@ through the <tt>Require Import</tt> command.</p> theories/Compat/AdmitAxiom.v theories/Compat/Coq86.v theories/Compat/Coq87.v + theories/Compat/Coq88.v </dd> </dl> diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 7674cf67aa..6b3ce048f7 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -89,15 +89,15 @@ let nf_evars_universes evm = (Evd.universe_subst evm) let nf_evars_and_universes evm = - let evm = Evd.nf_constraints evm in + let evm = Evd.minimize_universes evm in evm, nf_evars_universes evm let e_nf_evars_and_universes evdref = - evdref := Evd.nf_constraints !evdref; + evdref := Evd.minimize_universes !evdref; nf_evars_universes !evdref, Evd.universe_subst !evdref let nf_evar_map_universes evm = - let evm = Evd.nf_constraints evm in + let evm = Evd.minimize_universes evm in let subst = Evd.universe_subst evm in if Univ.LMap.is_empty subst then evm, nf_evar0 evm else diff --git a/engine/evd.ml b/engine/evd.ml index e7d542d122..b7b87370e2 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -253,21 +253,8 @@ let instantiate_evar_array info c args = | [] -> c | _ -> replace_vars inst c -type evar_universe_context = UState.t -type 'a in_evar_universe_context = 'a * evar_universe_context - -let empty_evar_universe_context = UState.empty -let union_evar_universe_context = UState.union -let evar_universe_context_set = UState.context_set -let evar_universe_context_constraints = UState.constraints -let evar_context_universe_context = UState.context -let evar_universe_context_of = UState.of_context_set -let evar_universe_context_subst = UState.subst -let add_constraints_context = UState.add_constraints -let add_universe_constraints_context = UState.add_universe_constraints -let constrain_variables = UState.constrain_variables -let evar_universe_context_of_binders = UState.of_binders +type 'a in_evar_universe_context = 'a * UState.t (*******************************************************************) (* Metamaps *) @@ -421,13 +408,15 @@ let key id (_, idtoev) = end +type goal_kind = ToShelve | ToGiveUp + type evar_map = { (** Existential variables *) defn_evars : evar_info EvMap.t; undf_evars : evar_info EvMap.t; evar_names : EvNames.t; (** Universes *) - universes : evar_universe_context; + universes : UState.t; (** Conversion problems *) conv_pbs : evar_constraint list; last_mods : Evar.Set.t; @@ -445,6 +434,7 @@ type evar_map = { name) of the evar which will be instantiated with a term containing [e]. *) + future_goals_status : goal_kind EvMap.t; extras : Store.t; } @@ -484,7 +474,8 @@ let remove d e = | Some e' -> if Evar.equal e e' then None else d.principal_future_goal in let future_goals = List.filter (fun e' -> not (Evar.equal e e')) d.future_goals in - { d with undf_evars; defn_evars; principal_future_goal; future_goals } + let future_goals_status = EvMap.remove e d.future_goals_status in + { d with undf_evars; defn_evars; principal_future_goal; future_goals; future_goals_status } let find d e = try EvMap.find e d.undf_evars @@ -558,10 +549,10 @@ let existential_type d (n, args) = instantiate_evar_array info info.evar_concl args let add_constraints d c = - { d with universes = add_constraints_context d.universes c } + { d with universes = UState.add_constraints d.universes c } let add_universe_constraints d c = - { d with universes = add_universe_constraints_context d.universes c } + { d with universes = UState.add_universe_constraints d.universes c } (*** /Lifting... ***) @@ -586,7 +577,7 @@ let create_evar_defs sigma = { sigma with let empty = { defn_evars = EvMap.empty; undf_evars = EvMap.empty; - universes = empty_evar_universe_context; + universes = UState.empty; conv_pbs = []; last_mods = Evar.Set.empty; metas = Metamap.empty; @@ -594,6 +585,7 @@ let empty = { evar_names = EvNames.empty; (* id<->key for undefined evars *) future_goals = []; principal_future_goal = None; + future_goals_status = EvMap.empty; extras = Store.empty; } @@ -609,14 +601,14 @@ let evars_reset_evd ?(with_conv_pbs=false) ?(with_univs=true) evd d = let last_mods = if with_conv_pbs then evd.last_mods else d.last_mods in let universes = if not with_univs then evd.universes - else union_evar_universe_context evd.universes d.universes + else UState.union evd.universes d.universes in { evd with metas = d.metas; last_mods; conv_pbs; universes } let merge_universe_context evd uctx' = - { evd with universes = union_evar_universe_context evd.universes uctx' } + { evd with universes = UState.union evd.universes uctx' } let set_universe_context evd uctx' = { evd with universes = uctx' } @@ -798,16 +790,6 @@ let make_flexible_variable evd ~algebraic u = { evd with universes = UState.make_flexible_variable evd.universes ~algebraic u } -let make_evar_universe_context e l = - let uctx = UState.make (Environ.universes e) in - match l with - | None -> uctx - | Some us -> - List.fold_left - (fun uctx { CAst.loc; v = id } -> - fst (UState.new_univ_variable ?loc univ_rigid (Some id) uctx)) - uctx us - (****************************************) (* Operations on constants *) (****************************************) @@ -910,10 +892,6 @@ let check_eq evd s s' = let check_leq evd s s' = UGraph.check_leq (UState.ugraph evd.universes) s s' -let normalize_evar_universe_context_variables = UState.normalize_variables - -let abstract_undefined_variables = UState.abstract_undefined_variables - let fix_undefined_variables evd = { evd with universes = UState.fix_undefined_variables evd.universes } @@ -922,16 +900,14 @@ let refresh_undefined_universes evd = let evd' = cmap (subst_univs_level_constr subst) {evd with universes = uctx'} in evd', subst -let normalize_evar_universe_context = UState.normalize - -let nf_univ_variables evd = - let subst, uctx' = normalize_evar_universe_context_variables evd.universes in +let nf_univ_variables evd = + let subst, uctx' = UState.normalize_variables evd.universes in let evd' = {evd with universes = uctx'} in evd', subst -let nf_constraints evd = - let subst, uctx' = normalize_evar_universe_context_variables evd.universes in - let uctx' = normalize_evar_universe_context uctx' in +let minimize_universes evd = + let subst, uctx' = UState.normalize_variables evd.universes in + let uctx' = UState.minimize uctx' in {evd with universes = uctx'} let universe_of_name evd s = UState.universe_of_name evd.universes s @@ -958,25 +934,72 @@ let drop_side_effects evd = let eval_side_effects evd = evd.effects (* Future goals *) -let declare_future_goal evk evd = - { evd with future_goals = evk::evd.future_goals } +let declare_future_goal ?tag evk evd = + { evd with future_goals = evk::evd.future_goals; + future_goals_status = Option.fold_right (EvMap.add evk) tag evd.future_goals_status } -let declare_principal_goal evk evd = +let declare_principal_goal ?tag evk evd = match evd.principal_future_goal with | None -> { evd with future_goals = evk::evd.future_goals; - principal_future_goal=Some evk; } + principal_future_goal=Some evk; + future_goals_status = Option.fold_right (EvMap.add evk) tag evd.future_goals_status; + } | Some _ -> CErrors.user_err Pp.(str "Only one main subgoal per instantiation.") +type future_goals = Evar.t list * Evar.t option * goal_kind EvMap.t + let future_goals evd = evd.future_goals let principal_future_goal evd = evd.principal_future_goal -let reset_future_goals evd = - { evd with future_goals = [] ; principal_future_goal=None } +let save_future_goals evd = + (evd.future_goals, evd.principal_future_goal, evd.future_goals_status) -let restore_future_goals evd gls pgl = - { evd with future_goals = gls ; principal_future_goal = pgl } +let reset_future_goals evd = + { evd with future_goals = [] ; principal_future_goal = None; + future_goals_status = EvMap.empty } + +let restore_future_goals evd (gls,pgl,map) = + { evd with future_goals = gls ; principal_future_goal = pgl; + future_goals_status = map } + +let fold_future_goals f sigma (gls,pgl,map) = + List.fold_left f sigma gls + +let map_filter_future_goals f (gls,pgl,map) = + (* Note: map is now a superset of filtered evs, but its size should + not be too big, so that's probably ok not to update it *) + (List.map_filter f gls,Option.bind pgl f,map) + +let filter_future_goals f (gls,pgl,map) = + (List.filter f gls,Option.bind pgl (fun a -> if f a then Some a else None),map) + +let dispatch_future_goals_gen distinguish_shelf (gls,pgl,map) = + let rec aux (comb,shelf,givenup as acc) = function + | [] -> acc + | evk :: gls -> + let acc = + try match EvMap.find evk map with + | ToGiveUp -> (comb,shelf,evk::givenup) + | ToShelve -> + if distinguish_shelf then (comb,evk::shelf,givenup) + else raise Not_found + with Not_found -> (evk::comb,shelf,givenup) in + aux acc gls in + (* Note: this reverses the order of initial list on purpose *) + let (comb,shelf,givenup) = aux ([],[],[]) gls in + (comb,shelf,givenup,pgl) + +let dispatch_future_goals = + dispatch_future_goals_gen true + +let extract_given_up_future_goals goals = + let (comb,_,givenup,_) = dispatch_future_goals_gen false goals in + (comb,givenup) + +let shelve_on_future_goals shelved (gls,pgl,map) = + (shelved @ gls, pgl, List.fold_right (fun evk -> EvMap.add evk ToShelve) shelved map) (**********************************************************) (* Accessing metas *) @@ -993,6 +1016,7 @@ let set_metas evd metas = { effects = evd.effects; evar_names = evd.evar_names; future_goals = evd.future_goals; + future_goals_status = evd.future_goals_status; principal_future_goal = evd.principal_future_goal; extras = evd.extras; } @@ -1076,7 +1100,7 @@ let clear_metas evd = {evd with metas = Metamap.empty} let meta_merge ?(with_univs = true) evd1 evd2 = let metas = Metamap.fold Metamap.add evd1.metas evd2.metas in let universes = - if with_univs then union_evar_universe_context evd2.universes evd1.universes + if with_univs then UState.union evd2.universes evd1.universes else evd2.universes in {evd2 with universes; metas; } @@ -1176,3 +1200,25 @@ module Monad = (* Failure explanation *) type unsolvability_explanation = SeveralInstancesFound of int + +(** Deprecated *) +type evar_universe_context = UState.t +let empty_evar_universe_context = UState.empty +let union_evar_universe_context = UState.union +let evar_universe_context_set = UState.context_set +let evar_universe_context_constraints = UState.constraints +let evar_context_universe_context = UState.context +let evar_universe_context_of = UState.of_context_set +let evar_universe_context_subst = UState.subst +let add_constraints_context = UState.add_constraints +let constrain_variables = UState.constrain_variables +let evar_universe_context_of_binders = UState.of_binders +let make_evar_universe_context e l = + let g = Environ.universes e in + match l with + | None -> UState.make g + | Some l -> UState.make_with_initial_binders g l +let normalize_evar_universe_context_variables = UState.normalize_variables +let abstract_undefined_variables = UState.abstract_undefined_variables +let normalize_evar_universe_context = UState.minimize +let nf_constraints = minimize_universes diff --git a/engine/evd.mli b/engine/evd.mli index ed3316c16d..bd9d75c6b0 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -282,11 +282,13 @@ val drop_side_effects : evar_map -> evar_map (** {5 Future goals} *) -val declare_future_goal : Evar.t -> evar_map -> evar_map +type goal_kind = ToShelve | ToGiveUp + +val declare_future_goal : ?tag:goal_kind -> Evar.t -> evar_map -> evar_map (** Adds an existential variable to the list of future goals. For internal uses only. *) -val declare_principal_goal : Evar.t -> evar_map -> evar_map +val declare_principal_goal : ?tag:goal_kind -> Evar.t -> evar_map -> evar_map (** Adds an existential variable to the list of future goals and make it principal. Only one existential variable can be made principal, an error is raised otherwise. For internal uses only. *) @@ -299,16 +301,41 @@ val principal_future_goal : evar_map -> Evar.t option (** Retrieves the name of the principal existential variable if there is one. Used by the [refine] primitive of the tactic engine. *) +type future_goals + +val save_future_goals : evar_map -> future_goals +(** Retrieves the list of future goals including the principal future + goal. Used by the [refine] primitive of the tactic engine. *) + val reset_future_goals : evar_map -> evar_map (** Clears the list of future goals (as well as the principal future goal). Used by the [refine] primitive of the tactic engine. *) -val restore_future_goals : evar_map -> Evar.t list -> Evar.t option -> evar_map +val restore_future_goals : evar_map -> future_goals -> evar_map (** Sets the future goals (including the principal future goal) to a previous value. Intended to be used after a local list of future goals has been consumed. Used by the [refine] primitive of the tactic engine. *) +val fold_future_goals : (evar_map -> Evar.t -> evar_map) -> evar_map -> future_goals -> evar_map +(** Fold future goals *) + +val map_filter_future_goals : (Evar.t -> Evar.t option) -> future_goals -> future_goals +(** Applies a function on the future goals *) + +val filter_future_goals : (Evar.t -> bool) -> future_goals -> future_goals +(** Applies a filter on the future goals *) + +val dispatch_future_goals : future_goals -> Evar.t list * Evar.t list * Evar.t list * Evar.t option +(** Returns the future_goals dispatched into regular, shelved, given_up + goals; last argument is the goal tagged as principal if any *) + +val extract_given_up_future_goals : future_goals -> Evar.t list * Evar.t list +(** An ad hoc variant for Proof.proof; not for general use *) + +val shelve_on_future_goals : Evar.t list -> future_goals -> future_goals +(** Push goals on the shelve of future goals *) + (** {5 Sort variables} Evar maps also keep track of the universe constraints defined at a given @@ -493,22 +520,31 @@ val univ_flexible_alg : rigid type 'a in_evar_universe_context = 'a * UState.t val evar_universe_context_set : UState.t -> Univ.ContextSet.t +[@@ocaml.deprecated "Alias of UState.context_set"] val evar_universe_context_constraints : UState.t -> Univ.Constraint.t +[@@ocaml.deprecated "Alias of UState.constraints"] val evar_context_universe_context : UState.t -> Univ.UContext.t [@@ocaml.deprecated "alias of UState.context"] val evar_universe_context_of : Univ.ContextSet.t -> UState.t +[@@ocaml.deprecated "Alias of UState.of_context_set"] val empty_evar_universe_context : UState.t +[@@ocaml.deprecated "Alias of UState.empty"] val union_evar_universe_context : UState.t -> UState.t -> UState.t +[@@ocaml.deprecated "Alias of UState.union"] val evar_universe_context_subst : UState.t -> Universes.universe_opt_subst +[@@ocaml.deprecated "Alias of UState.subst"] val constrain_variables : Univ.LSet.t -> UState.t -> UState.t +[@@ocaml.deprecated "Alias of UState.constrain_variables"] val evar_universe_context_of_binders : Universes.universe_binders -> UState.t +[@@ocaml.deprecated "Alias of UState.of_binders"] val make_evar_universe_context : env -> Misctypes.lident list option -> UState.t +[@@ocaml.deprecated "Use UState.make or UState.make_with_initial_binders"] val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map (** Raises Not_found if not a name for a universe in this map. *) val universe_of_name : evar_map -> Id.t -> Univ.Level.t @@ -516,13 +552,15 @@ val universe_of_name : evar_map -> Id.t -> Univ.Level.t val universe_binders : evar_map -> Universes.universe_binders val add_constraints_context : UState.t -> Univ.Constraint.t -> UState.t +[@@ocaml.deprecated "Alias of UState.add_constraints"] val normalize_evar_universe_context_variables : UState.t -> Univ.universe_subst in_evar_universe_context +[@@ocaml.deprecated "Alias of UState.normalize_variables"] -val normalize_evar_universe_context : UState.t -> - UState.t +val normalize_evar_universe_context : UState.t -> UState.t +[@@ocaml.deprecated "Alias of UState.minimize"] val new_univ_level_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Level.t val new_univ_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Universe.t @@ -581,12 +619,16 @@ val with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_co val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst val abstract_undefined_variables : UState.t -> UState.t +[@@ocaml.deprecated "Alias of UState.abstract_undefined_variables"] val fix_undefined_variables : evar_map -> evar_map val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_subst +(** Universe minimization *) +val minimize_universes : evar_map -> evar_map val nf_constraints : evar_map -> evar_map +[@@ocaml.deprecated "Alias of Evd.minimize_universes"] val update_sigma_env : evar_map -> env -> evar_map diff --git a/engine/proofview.ml b/engine/proofview.ml index 8a844bbf54..22271dd02c 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -768,10 +768,11 @@ let with_shelf tac = tac >>= fun ans -> Pv.get >>= fun npv -> let { shelf = gls; solution = sigma } = npv in + (* The pending future goals are necessarily coming from V82.tactic *) + (* and thus considered as to shelve, as in Proof.run_tactic *) let gls' = Evd.future_goals sigma in - let fgoals = Evd.future_goals solution in - let pgoal = Evd.principal_future_goal solution in - let sigma = Evd.restore_future_goals sigma fgoals pgoal in + let fgoals = Evd.save_future_goals solution in + let sigma = Evd.restore_future_goals sigma fgoals in (* Ensure we mark and return only unsolved goals *) let gls' = undefined_evars sigma (CList.rev_append gls' gls) in let sigma = CList.fold_left (mark_in_evm ~goal:false) sigma gls' in @@ -1011,6 +1012,15 @@ module Unsafe = struct let tclSETGOALS = Comb.set + let tclGETSHELF = Shelf.get + + let tclSETSHELF = Shelf.set + + let tclPUTSHELF to_shelve = + tclBIND tclGETSHELF (fun shelf -> tclSETSHELF (to_shelve@shelf)) + + let tclPUTGIVENUP = Giveup.put + let tclEVARSADVANCE evd = Pv.modify (fun ps -> { ps with solution = evd; comb = undefined evd ps.comb }) diff --git a/engine/proofview.mli b/engine/proofview.mli index 4862791874..e7be665527 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -435,6 +435,18 @@ module Unsafe : sig (** [tclGETGOALS] returns the list of goals under focus. *) val tclGETGOALS : Proofview_monad.goal_with_state list tactic + (** [tclSETSHELF gls] sets goals [gls] as the current shelf. *) + val tclSETSHELF : Evar.t list -> unit tactic + + (** [tclGETSHELF] returns the list of goals on the shelf. *) + val tclGETSHELF : Evar.t list tactic + + (** [tclPUTSHELF] appends goals to the shelf. *) + val tclPUTSHELF : Evar.t list -> unit tactic + + (** [tclPUTGIVENUP] add an given up goal. *) + val tclPUTGIVENUP : Evar.t list -> unit tactic + (** Sets the evar universe context. *) val tclEVARUNIVCONTEXT : UState.t -> unit tactic diff --git a/engine/termops.ml b/engine/termops.ml index c615155d1f..35258762a7 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -294,12 +294,11 @@ let reference_of_level evd l = UState.reference_of_level (Evd.evar_universe_cont let pr_evar_universe_context ctx = let open UState in - let open Evd in let prl = pr_uctx_level ctx in if UState.is_empty ctx then mt () else (str"UNIVERSES:"++brk(0,1)++ - h 0 (Univ.pr_universe_context_set prl (evar_universe_context_set ctx)) ++ fnl () ++ + h 0 (Univ.pr_universe_context_set prl (UState.context_set ctx)) ++ fnl () ++ str"ALGEBRAIC UNIVERSES:"++brk(0,1)++ h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++ str"UNDEFINED UNIVERSES:"++brk(0,1)++ diff --git a/engine/uState.ml b/engine/uState.ml index 00825208b3..e57afd743a 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -476,6 +476,13 @@ let new_univ_variable ?loc rigid name uctx_initial_universes = initial} in uctx', u +let make_with_initial_binders e us = + let uctx = make e in + List.fold_left + (fun uctx { CAst.loc; v = id } -> + fst (new_univ_variable ?loc univ_rigid (Some id) uctx)) + uctx us + let add_global_univ uctx u = let initial = UGraph.add_universe u true uctx.uctx_initial_universes @@ -578,7 +585,7 @@ let refresh_undefined_univ_variables uctx = uctx_initial_universes = initial } in uctx', subst -let normalize uctx = +let minimize uctx = let ((vars',algs'), us') = Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables uctx.uctx_univ_algebraic @@ -606,3 +613,6 @@ let update_sigma_env uctx env = uctx_universes = univs } in merge true univ_rigid eunivs eunivs.uctx_local + +(** Deprecated *) +let normalize = minimize diff --git a/engine/uState.mli b/engine/uState.mli index 68fe350c01..9a2bc706be 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -26,6 +26,8 @@ val empty : t val make : UGraph.t -> t +val make_with_initial_binders : UGraph.t -> Misctypes.lident list -> t + val is_empty : t -> bool val union : t -> t -> t @@ -131,7 +133,10 @@ val fix_undefined_variables : t -> t val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst +(** Universe minimization *) +val minimize : t -> t val normalize : t -> t +[@@ocaml.deprecated "Alias of UState.minimize"] type universe_decl = (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index 6c072e36ad..525be64325 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -13,15 +13,6 @@ open Q_util open Argextend -(** Quotation difference for match clauses *) - -let default_patt loc = - (<:patt< _ >>, ploc_vala None, <:expr< failwith "Extension: cannot occur" >>) - -let make_fun loc cl = - let l = cl @ [default_patt loc] in - MLast.ExFun (loc, ploc_vala l) (* correspond to <:expr< fun [ $list:l$ ] >> *) - let plugin_name = <:expr< __coq_plugin_name >> let mlexpr_of_ident id = @@ -29,112 +20,33 @@ let mlexpr_of_ident id = let id = "$" ^ id in <:expr< Names.Id.of_string_soft $str:id$ >> -let rec make_patt = function - | [] -> <:patt< [] >> - | ExtNonTerminal (_, Some p) :: l -> - <:patt< [ $lid:p$ :: $make_patt l$ ] >> - | _::l -> make_patt l - -let rec make_let raw e = function - | [] -> <:expr< fun $lid:"ist"$ -> $e$ >> - | ExtNonTerminal (g, Some p) :: l -> - let t = type_of_user_symbol g in - let loc = MLast.loc_of_expr e in - let e = make_let raw e l in - let v = - if raw then <:expr< Genarg.out_gen $make_rawwit loc t$ $lid:p$ >> - else <:expr< Tacinterp.Value.cast $make_topwit loc t$ $lid:p$ >> in - <:expr< let $lid:p$ = $v$ in $e$ >> - | _::l -> make_let raw e l - -let make_clause (pt,e) = - (make_patt pt, - ploc_vala None, - make_let false e pt) - -let make_fun_clauses loc s l = - let map c = make_fun loc [make_clause c] in - mlexpr_of_list map l - -let get_argt e = <:expr< (fun e -> match e with [ Genarg.ExtraArg tag -> tag | _ -> assert False ]) $e$ >> - let rec mlexpr_of_symbol = function -| Ulist1 s -> <:expr< Extend.Ulist1 $mlexpr_of_symbol s$ >> -| Ulist1sep (s,sep) -> <:expr< Extend.Ulist1sep $mlexpr_of_symbol s$ $str:sep$ >> -| Ulist0 s -> <:expr< Extend.Ulist0 $mlexpr_of_symbol s$ >> -| Ulist0sep (s,sep) -> <:expr< Extend.Ulist0sep $mlexpr_of_symbol s$ $str:sep$ >> -| Uopt s -> <:expr< Extend.Uopt $mlexpr_of_symbol s$ >> +| Ulist1 s -> <:expr< Extend.TUlist1 $mlexpr_of_symbol s$ >> +| Ulist1sep (s,sep) -> <:expr< Extend.TUlist1sep $mlexpr_of_symbol s$ $str:sep$ >> +| Ulist0 s -> <:expr< Extend.TUlist0 $mlexpr_of_symbol s$ >> +| Ulist0sep (s,sep) -> <:expr< Extend.TUlist0sep $mlexpr_of_symbol s$ $str:sep$ >> +| Uopt s -> <:expr< Extend.TUopt $mlexpr_of_symbol s$ >> | Uentry e -> - let arg = get_argt <:expr< $lid:"wit_"^e$ >> in - <:expr< Extend.Uentry (Genarg.ArgT.Any $arg$) >> + let wit = <:expr< $lid:"wit_"^e$ >> in + <:expr< Extend.TUentry (Genarg.get_arg_tag $wit$) >> | Uentryl (e, l) -> assert (e = "tactic"); - let arg = get_argt <:expr< Tacarg.wit_tactic >> in - <:expr< Extend.Uentryl (Genarg.ArgT.Any $arg$) $mlexpr_of_int l$>> - -let make_prod_item = function - | ExtTerminal s -> <:expr< Tacentries.TacTerm $str:s$ >> - | ExtNonTerminal (g, id) -> - <:expr< Tacentries.TacNonTerm (Loc.tag ( $mlexpr_of_symbol g$ , $mlexpr_of_option mlexpr_of_ident id$ ) ) >> - -let mlexpr_of_clause cl = - mlexpr_of_list (fun (a,_) -> mlexpr_of_list make_prod_item a) cl - -(** Special treatment of constr entries *) -let is_constr_gram = function -| ExtTerminal _ -> false -| ExtNonTerminal (Uentry "constr", _) -> true -| _ -> false - -let make_var = function - | ExtNonTerminal (_, p) -> p - | _ -> assert false - -let declare_tactic loc tacname ~level clause = match clause with -| [(ExtTerminal name) :: rem, tac] when List.for_all is_constr_gram rem -> - (** The extension is only made of a name followed by constr entries: we do not - add any grammar nor printing rule and add it as a true Ltac definition. *) - let patt = make_patt rem in - let vars = List.map make_var rem in - let vars = mlexpr_of_list (mlexpr_of_name mlexpr_of_ident) vars in - let entry = mlexpr_of_string tacname in - let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in - let ml = <:expr< { Tacexpr.mltac_name = $se$; Tacexpr.mltac_index = 0 } >> in - let name = mlexpr_of_string name in - let tac = match rem with - | [] -> - (** Special handling of tactics without arguments: such tactics do not do - a Proofview.Goal.nf_enter to compute their arguments. It matters for some - whole-prof tactics like [shelve_unifiable]. *) - <:expr< fun _ $lid:"ist"$ -> $tac$ >> - | _ -> - let f = make_fun loc [patt, ploc_vala None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in - <:expr< Tacinterp.lift_constr_tac_to_ml_tac $vars$ $f$ >> - in - (** Arguments are not passed directly to the ML tactic in the TacML node, - the ML tactic retrieves its arguments in the [ist] environment instead. - This is the rôle of the [lift_constr_tac_to_ml_tac] function. *) - let body = <:expr< Tacexpr.TacFun ($vars$, Tacexpr.TacML (Loc.tag ( $ml$ , []))) >> in - let name = <:expr< Names.Id.of_string $name$ >> in - declare_str_items loc - [ <:str_item< do { - let obj () = Tacenv.register_ltac True False $name$ $body$ in - let () = Tacenv.register_ml_tactic $se$ [|$tac$|] in - Mltop.declare_cache_obj obj $plugin_name$ } >> - ] -| _ -> - (** Otherwise we add parsing and printing rules to generate a call to a - TacML tactic. *) - let entry = mlexpr_of_string tacname in - let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in - let gl = mlexpr_of_clause clause in - let level = mlexpr_of_int level in - let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ ~{ level = $level$ } $gl$ >> in - declare_str_items loc - [ <:str_item< do { - Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc tacname clause$); - Mltop.declare_cache_obj $obj$ $plugin_name$; } >> - ] + let wit = <:expr< $lid:"wit_"^e$ >> in + <:expr< Extend.TUentryl (Genarg.get_arg_tag $wit$) $mlexpr_of_int l$>> + +let rec mlexpr_of_clause = function +| [] -> <:expr< TyNil >> +| ExtTerminal s :: cl -> <:expr< TyIdent($str:s$, $mlexpr_of_clause cl$) >> +| ExtNonTerminal(g,None) :: cl -> + <:expr< TyAnonArg(Loc.tag($mlexpr_of_symbol g$), $mlexpr_of_clause cl$) >> +| ExtNonTerminal(g,Some id) :: cl -> + <:expr< TyArg(Loc.tag($mlexpr_of_symbol g$, $mlexpr_of_ident id$), $mlexpr_of_clause cl$) >> + +let rec binders_of_clause e = function +| [] -> <:expr< fun ist -> $e$ >> +| ExtNonTerminal(_,None) :: cl -> binders_of_clause e cl +| ExtNonTerminal(_,Some id) :: cl -> <:expr< fun $lid:id$ -> $binders_of_clause e cl$ >> +| _ :: cl -> binders_of_clause e cl open Pcaml @@ -146,13 +58,17 @@ EXTEND OPT "|"; l = LIST1 tacrule SEP "|"; "END" -> let level = match level with Some i -> int_of_string i | None -> 0 in - declare_tactic loc s ~level l ] ] + let level = mlexpr_of_int level in + let l = <:expr< Tacentries.($mlexpr_of_list (fun x -> x) l$) >> in + declare_str_items loc [ <:str_item< Tacentries.tactic_extend $plugin_name$ $str:s$ ~{ level = $level$ } $l$ >> ] ] ] ; tacrule: [ [ "["; l = LIST1 tacargs; "]"; - "->"; "["; e = Pcaml.expr; "]" -> (l,e) + "->"; "["; e = Pcaml.expr; "]" -> + <:expr< TyML($mlexpr_of_clause l$, $binders_of_clause e l$) >> ] ] ; + tacargs: [ [ e = LIDENT; "("; s = LIDENT; ")" -> let e = parse_user_entry e "" in diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index 24ee0042be..a2872d07f6 100644 --- a/grammar/vernacextend.mlp +++ b/grammar/vernacextend.mlp @@ -12,7 +12,6 @@ open Q_util open Argextend -open Tacextend type rule = { r_head : string option; @@ -27,6 +26,21 @@ type rule = { (** Whether this entry is deprecated *) } +(** Quotation difference for match clauses *) + +let default_patt loc = + (<:patt< _ >>, ploc_vala None, <:expr< failwith "Extension: cannot occur" >>) + +let make_fun loc cl = + let l = cl @ [default_patt loc] in + MLast.ExFun (loc, ploc_vala l) (* correspond to <:expr< fun [ $list:l$ ] >> *) + +let rec make_patt = function + | [] -> <:patt< [] >> + | ExtNonTerminal (_, Some p) :: l -> + <:patt< [ $lid:p$ :: $make_patt l$ ] >> + | _::l -> make_patt l + let rec make_let e = function | [] -> e | ExtNonTerminal (g, Some p) :: l -> diff --git a/intf/extend.ml b/intf/extend.ml index 10c9b3dc14..734b859f60 100644 --- a/intf/extend.ml +++ b/intf/extend.ml @@ -85,6 +85,15 @@ type 'a user_symbol = | Uentry of 'a | Uentryl of 'a * int +type ('a,'b,'c) ty_user_symbol = +| TUlist1 : ('a,'b,'c) ty_user_symbol -> ('a list,'b list,'c list) ty_user_symbol +| TUlist1sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol +| TUlist0 : ('a,'b,'c) ty_user_symbol -> ('a list,'b list,'c list) ty_user_symbol +| TUlist0sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol +| TUopt : ('a,'b,'c) ty_user_symbol -> ('a option, 'b option, 'c option) ty_user_symbol +| TUentry : ('a, 'b, 'c) Genarg.ArgT.tag -> ('a,'b,'c) ty_user_symbol +| TUentryl : ('a, 'b, 'c) Genarg.ArgT.tag * int -> ('a,'b,'c) ty_user_symbol + (** {5 Type-safe grammar extension} *) type ('self, 'a) symbol = diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 91c042130a..9bed598bb7 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -1069,6 +1069,9 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = try find_inductive env a with Not_found -> raise_err env i (RecursionNotOnInductiveType a) in + let mib,_ = lookup_mind_specif env (out_punivs mind) in + if mib.mind_finite != Finite then + raise_err env i (RecursionNotOnInductiveType a); (mind, (env', b)) else check_occur env' (n+1) b else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call.") diff --git a/kernel/reduction.ml b/kernel/reduction.ml index e9be1b35df..b3e6894143 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -269,8 +269,9 @@ let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u if not (Int.equal num_cnstr_args nargs) then cmp_instances u1 u2 s else - let csts = get_cumulativity_constraints CONV cumi u1 u2 in - cmp_cumul csts s + (** By invariant, both constructors have a common supertype, + so they are convertible _at that type_. *) + s let convert_constructors ctor nargs u1 u2 (s, check) = convert_constructors_gen (check.compare_instances ~flex:false) check.compare_cumul_instances diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4 index 40945939f2..d6c340f691 100644 --- a/lib/coqProject_file.ml4 +++ b/lib/coqProject_file.ml4 @@ -8,27 +8,32 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +type arg_source = CmdLine | ProjectFile + +type 'a sourced = { thing : 'a; source : arg_source } + type project = { project_file : string option; makefile : string option; install_kind : install option; use_ocamlopt : bool; - v_files : string list; - mli_files : string list; - ml4_files : string list; - ml_files : string list; - mllib_files : string list; - mlpack_files : string list; - - ml_includes : path list; - r_includes : (path * logic_path) list; - q_includes : (path * logic_path) list; - extra_args : string list; - defs : (string * string) list; - - extra_targets : extra_target list; - subdirs : string list; + v_files : string sourced list; + mli_files : string sourced list; + ml4_files : string sourced list; + ml_files : string sourced list; + mllib_files : string sourced list; + mlpack_files : string sourced list; + + ml_includes : path sourced list; + r_includes : (path * logic_path) sourced list; + q_includes : (path * logic_path) sourced list; + extra_args : string sourced list; + defs : (string * string) sourced list; + + (* deprecated in favor of a Makefile.local using :: rules *) + extra_targets : extra_target sourced list; + subdirs : string sourced list; } and extra_target = { target : string; @@ -114,6 +119,7 @@ let exists_dir dir = let process_cmd_line orig_dir proj args = let parsing_project_file = ref (proj.project_file <> None) in + let sourced x = { thing = x; source = if !parsing_project_file then ProjectFile else CmdLine } in let orig_dir = (* avoids turning foo.v in ./foo.v *) if orig_dir = "." then "" else orig_dir in let error s = Format.eprintf "@[%a]@@\n%!" Pp.pp_with Pp.(str (s^".")); exit 1 in @@ -143,17 +149,17 @@ let process_cmd_line orig_dir proj args = aux { proj with install_kind = Some install } r | "-extra" :: target :: dependencies :: command :: r -> let tgt = { target; dependencies; phony = false; command } in - aux { proj with extra_targets = proj.extra_targets @ [tgt] } r + aux { proj with extra_targets = proj.extra_targets @ [sourced tgt] } r | "-extra-phony" :: target :: dependencies :: command :: r -> let tgt = { target; dependencies; phony = true; command } in - aux { proj with extra_targets = proj.extra_targets @ [tgt] } r + aux { proj with extra_targets = proj.extra_targets @ [sourced tgt] } r | "-Q" :: d :: lp :: r -> - aux { proj with q_includes = proj.q_includes @ [mk_path d,lp] } r + aux { proj with q_includes = proj.q_includes @ [sourced (mk_path d,lp)] } r | "-I" :: d :: r -> - aux { proj with ml_includes = proj.ml_includes @ [mk_path d] } r + aux { proj with ml_includes = proj.ml_includes @ [sourced (mk_path d)] } r | "-R" :: d :: lp :: r -> - aux { proj with r_includes = proj.r_includes @ [mk_path d,lp] } r + aux { proj with r_includes = proj.r_includes @ [sourced (mk_path d,lp)] } r | "-f" :: file :: r -> if !parsing_project_file then @@ -178,20 +184,21 @@ let process_cmd_line orig_dir proj args = error "Option -o given more than once"; aux { proj with makefile = Some file } r | v :: "=" :: def :: r -> - aux { proj with defs = proj.defs @ [v,def] } r + aux { proj with defs = proj.defs @ [sourced (v,def)] } r | "-arg" :: a :: r -> - aux { proj with extra_args = proj.extra_args @ [a] } r + aux { proj with extra_args = proj.extra_args @ [sourced a] } r | f :: r -> let f = CUnix.correct_path f orig_dir in let proj = - if exists_dir f then { proj with subdirs = proj.subdirs @ [f] } + if exists_dir f then { proj with subdirs = proj.subdirs @ [sourced f] } else match CUnix.get_extension f with - | ".v" -> { proj with v_files = proj.v_files @ [f] } - | ".ml" -> { proj with ml_files = proj.ml_files @ [f] } - | ".ml4" -> { proj with ml4_files = proj.ml4_files @ [f] } - | ".mli" -> { proj with mli_files = proj.mli_files @ [f] } - | ".mllib" -> { proj with mllib_files = proj.mllib_files @ [f] } - | ".mlpack" -> { proj with mlpack_files = proj.mlpack_files @ [f] } + | ".v" -> + { proj with v_files = proj.v_files @ [sourced f] } + | ".ml" -> { proj with ml_files = proj.ml_files @ [sourced f] } + | ".ml4" -> { proj with ml4_files = proj.ml4_files @ [sourced f] } + | ".mli" -> { proj with mli_files = proj.mli_files @ [sourced f] } + | ".mllib" -> { proj with mllib_files = proj.mllib_files @ [sourced f] } + | ".mlpack" -> { proj with mlpack_files = proj.mlpack_files @ [sourced f] } | _ -> raise (Parsing_error ("Unknown option "^f)) in aux proj r in @@ -215,16 +222,34 @@ let rec find_project_file ~from ~projfile_name = else find_project_file ~from:newdir ~projfile_name ;; +let all_files { v_files; ml_files; mli_files; ml4_files; + mllib_files; mlpack_files } = + v_files @ mli_files @ ml4_files @ ml_files @ mllib_files @ mlpack_files + +let map_sourced_list f l = List.map (fun x -> f x.thing) l +;; + +let map_cmdline f l = CList.map_filter (function + | {thing=x; source=CmdLine} -> Some (f x) + | {source=ProjectFile} -> None) l + let coqtop_args_from_project { ml_includes; r_includes; q_includes; extra_args } = - let map = List.map in + let map = map_sourced_list in let args = map (fun { canonical_path = i } -> ["-I"; i]) ml_includes @ map (fun ({ canonical_path = i }, l) -> ["-Q"; i; l]) q_includes @ map (fun ({ canonical_path = p }, l) -> ["-R"; p; l]) r_includes @ - [extra_args] in + [map (fun x -> x) extra_args] in List.flatten args ;; +let filter_cmdline l = CList.map_filter + (function {thing; source=CmdLine} -> Some thing | {source=ProjectFile} -> None) + l +;; + +let forget_source {thing} = thing + (* vim:set ft=ocaml: *) diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli index 5a4dd3659f..5780bb5d78 100644 --- a/lib/coqProject_file.mli +++ b/lib/coqProject_file.mli @@ -10,29 +10,32 @@ exception Parsing_error of string +type arg_source = CmdLine | ProjectFile + +type 'a sourced = { thing : 'a; source : arg_source } + type project = { project_file : string option; makefile : string option; install_kind : install option; use_ocamlopt : bool; - v_files : string list; - mli_files : string list; - ml4_files : string list; - ml_files : string list; - mllib_files : string list; - mlpack_files : string list; + v_files : string sourced list; + mli_files : string sourced list; + ml4_files : string sourced list; + ml_files : string sourced list; + mllib_files : string sourced list; + mlpack_files : string sourced list; - ml_includes : path list; - r_includes : (path * logic_path) list; - q_includes : (path * logic_path) list; - extra_args : string list; - defs : (string * string) list; + ml_includes : path sourced list; + r_includes : (path * logic_path) sourced list; + q_includes : (path * logic_path) sourced list; + extra_args : string sourced list; + defs : (string * string) sourced list; (* deprecated in favor of a Makefile.local using :: rules *) - extra_targets : extra_target list; - subdirs : string list; - + extra_targets : extra_target sourced list; + subdirs : string sourced list; } and extra_target = { target : string; @@ -52,3 +55,14 @@ val read_project_file : string -> project val coqtop_args_from_project : project -> string list val find_project_file : from:string -> projfile_name:string -> string option +val all_files : project -> string sourced list + +val map_sourced_list : ('a -> 'b) -> 'a sourced list -> 'b list + +(** Only uses the elements with source=CmdLine *) +val map_cmdline : ('a -> 'b) -> 'a sourced list -> 'b list + +(** Only uses the elements with source=CmdLine *) +val filter_cmdline : 'a sourced list -> 'a list + +val forget_source : 'a sourced -> 'a diff --git a/lib/genarg.ml b/lib/genarg.ml index cf3a2bee7f..209d1b271e 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -174,19 +174,22 @@ sig val default : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb, 'top) obj option end +let get_arg_tag = function +| ExtraArg s -> s +| _ -> assert false + module Register (M : GenObj) = struct module GenMap = ArgMap(struct type ('r, 'g, 't) t = ('r, 'g, 't) M.obj end) let arg0_map = ref GenMap.empty - let register0 arg f = match arg with - | ExtraArg s -> + let register0 arg f = + let s = get_arg_tag arg in if GenMap.mem s !arg0_map then let msg = str M.name ++ str " function already registered: " ++ str (ArgT.repr s) ++ str "." in CErrors.anomaly msg else arg0_map := GenMap.add s (GenMap.Pack f) !arg0_map - | _ -> assert false let get_obj0 name = try @@ -199,8 +202,6 @@ struct (** For now, the following function is quite dummy and should only be applied to an extra argument type, otherwise, it will badly fail. *) - let obj t = match t with - | ExtraArg s -> get_obj0 s - | _ -> assert false + let obj t = get_obj0 @@ get_arg_tag t end diff --git a/lib/genarg.mli b/lib/genarg.mli index d49cb334a0..bb85f99e3c 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -159,6 +159,9 @@ val unquote : ('a, 'co) abstract_argument_type -> argument_type This is boilerplate code used here and there in the code of Coq. *) +val get_arg_tag : ('a, 'b, 'c) genarg_type -> ('a, 'b, 'c) ArgT.tag +(** Works only on base objects (ExtraArg), otherwise fails badly. *) + module type GenObj = sig type ('raw, 'glb, 'top) obj diff --git a/man/coqdep.1 b/man/coqdep.1 index ed727db7c8..c417402c25 100644 --- a/man/coqdep.1 +++ b/man/coqdep.1 @@ -80,6 +80,9 @@ Prints the dependencies of Caml modules. \" of each Coq file given as argument and complete (if needed) \" the list of Caml modules. The new command is printed on \" the standard output. No dependency is computed with this option. +.TP +.BI \-f \ file +Read filenames and options -I, -R and -Q from a _CoqProject FILE. .TP .BI \-I/\-Q/\-R \ options Have the same effects on load path and modules names as for other diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 722b3990cb..a4e8c44cd0 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -137,22 +137,25 @@ let check_arity env cb = let t = cb.const_type in if Reduction.is_arity env t then raise Impossible -let check_fix env cb i = +let get_body lbody = + EConstr.of_constr (Mod_subst.force_constr lbody) + +let check_fix env sg cb i = match cb.const_body with | Def lbody -> - (match Constr.kind (Mod_subst.force_constr lbody) with - | Fix ((_,j),recd) when Int.equal i j -> check_arity env cb; (true,recd) + (match EConstr.kind sg (get_body lbody) with + | Fix ((_,j),recd) when Int.equal i j -> check_arity env cb; (true,recd) | CoFix (j,recd) when Int.equal i j -> check_arity env cb; (false,recd) | _ -> raise Impossible) | Undef _ | OpaqueDef _ -> raise Impossible -let prec_declaration_equal (na1, ca1, ta1) (na2, ca2, ta2) = +let prec_declaration_equal sg (na1, ca1, ta1) (na2, ca2, ta2) = Array.equal Name.equal na1 na2 && - Array.equal Constr.equal ca1 ca2 && - Array.equal Constr.equal ta1 ta2 + Array.equal (EConstr.eq_constr sg) ca1 ca2 && + Array.equal (EConstr.eq_constr sg) ta1 ta2 -let factor_fix env l cb msb = - let _,recd as check = check_fix env cb 0 in +let factor_fix env sg l cb msb = + let _,recd as check = check_fix env sg cb 0 in let n = Array.length (let fi,_,_ = recd in fi) in if Int.equal n 1 then [|l|], recd, msb else begin @@ -163,9 +166,9 @@ let factor_fix env l cb msb = (fun j -> function | (l,SFBconst cb') -> - let check' = check_fix env cb' (j+1) in - if not ((fst check : bool) == (fst check') && - prec_declaration_equal (snd check) (snd check')) + let check' = check_fix env sg cb' (j+1) in + if not ((fst check : bool) == (fst check') && + prec_declaration_equal sg (snd check) (snd check')) then raise Impossible; labels.(j+1) <- l; | _ -> raise Impossible) msb'; @@ -248,7 +251,9 @@ and extract_mexpr_spec env mp1 (me_struct_o,me_alg) = match me_alg with let me_struct,delta = flatten_modtype env mp1 me' me_struct_o in let env' = env_for_mtb_with_def env mp1 me_struct delta idl in let mt = extract_mexpr_spec env mp1 (None,me') in - (match extract_with_type env' c with (* cb may contain some kn *) + let sg = Evd.from_env env in + (match extract_with_type env' sg (EConstr.of_constr c) with + (* cb may contain some kn *) | None -> mt | Some (vl,typ) -> type_iter_references Visit.add_ref typ; @@ -299,12 +304,13 @@ let rec extract_structure env mp reso ~all = function | [] -> [] | (l,SFBconst cb) :: struc -> (try - let vl,recd,struc = factor_fix env l cb struc in + let sg = Evd.from_env env in + let vl,recd,struc = factor_fix env sg l cb struc in let vc = Array.map (make_cst reso mp) vl in let ms = extract_structure env mp reso ~all struc in let b = Array.exists Visit.needed_cst vc in if all || b then - let d = extract_fixpoint env vc recd in + let d = extract_fixpoint env sg vc recd in if (not b) && (logical_decl d) then ms else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms @@ -572,8 +578,8 @@ let print_structure_to_file (fn,si,mo) dry struc = let reset () = Visit.reset (); reset_tables (); reset_renaming_tables Everything -let init ?(compute=false) modular library = - check_inside_section (); check_inside_module (); +let init ?(compute=false) ?(inner=false) modular library = + if not inner then (check_inside_section (); check_inside_module ()); set_keywords (descr ()).keywords; set_modular modular; set_library library; @@ -701,10 +707,9 @@ let flatten_structure struc = and flatten_elems l = List.flatten (List.map flatten_elem l) in flatten_elems (List.flatten (List.map snd struc)) -let structure_for_compute c = +let structure_for_compute env sg c = init false false ~compute:true; - let env = Global.env () in - let ast, mlt = Extraction.extract_constr env c in + let ast, mlt = Extraction.extract_constr env sg c in let ast = Mlutil.normalize ast in let refs = ref Refset.empty in let add_ref r = refs := Refset.add r !refs in @@ -744,3 +749,20 @@ let extract_and_compile l = let base = Filename.chop_suffix f ".ml" in let () = remove (base^".cmo"); remove (base^".cmi") in Feedback.msg_notice (str "Extracted code successfully compiled") + +(* Show the extraction of the current ongoing proof *) + +let show_extraction () = + init ~inner:true false false; + let prf = Proof_global.give_me_the_proof () in + let sigma, env = Pfedit.get_current_context () in + let trms = Proof.partial_proof prf in + let extr_term t = + let ast, ty = extract_constr env sigma t in + let mp = Lib.current_mp () in + let l = Label.of_id (Proof_global.get_current_proof_name ()) in + let fake_ref = ConstRef (Constant.make2 mp l) in + let decl = Dterm (fake_ref, ast, ty) in + print_one_decl [] mp decl + in + Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl extr_term trms) diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 464f109be2..591d3bb86e 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -36,4 +36,9 @@ val print_one_decl : (* Used by Extraction Compute *) val structure_for_compute : - Constr.t -> (Miniml.ml_decl list) * Miniml.ml_ast * Miniml.ml_type + Environ.env -> Evd.evar_map -> EConstr.t -> + Miniml.ml_decl list * Miniml.ml_ast * Miniml.ml_type + +(* Show the extraction of the current ongoing proof *) + +val show_extraction : unit -> unit diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index ce49700561..f25f636249 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -13,7 +13,6 @@ open Util open Names open Term open Constr -open Vars open Declarations open Declareops open Environ @@ -36,20 +35,18 @@ exception I of inductive_kind (* A set of all fixpoint functions currently being extracted *) let current_fixpoints = ref ([] : Constant.t list) -let none = Evd.empty - (* NB: In OCaml, [type_of] and [get_of] might raise [SingletonInductiveBecomeProp]. This exception will be caught in late wrappers around the exported functions of this file, in order to display the location of the issue. *) -let type_of env c = +let type_of env sg c = let polyprop = (lang() == Haskell) in - EConstr.Unsafe.to_constr (Retyping.get_type_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c))) + Retyping.get_type_of ~polyprop env sg (strip_outer_cast sg c) -let sort_of env c = +let sort_of env sg c = let polyprop = (lang() == Haskell) in - Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c)) + Retyping.get_sort_family_of ~polyprop env sg (strip_outer_cast sg c) (*S Generation of flags and signatures. *) @@ -73,61 +70,91 @@ type scheme = TypeScheme | Default type flag = info * scheme -let whd_all env t = - EConstr.Unsafe.to_constr (whd_all env none (EConstr.of_constr t)) - -let whd_betaiotazeta t = - EConstr.Unsafe.to_constr (whd_betaiotazeta none (EConstr.of_constr t)) - (*s [flag_of_type] transforms a type [t] into a [flag]. Really important function. *) -let rec flag_of_type env t : flag = - let t = whd_all env t in - match Constr.kind t with - | Prod (x,t,c) -> flag_of_type (push_rel (LocalAssum (x,t)) env) c - | Sort s when Sorts.is_prop s -> (Logic,TypeScheme) +let rec flag_of_type env sg t : flag = + let t = whd_all env sg t in + match EConstr.kind sg t with + | Prod (x,t,c) -> flag_of_type (EConstr.push_rel (LocalAssum (x,t)) env) sg c + | Sort s when Sorts.is_prop (EConstr.ESorts.kind sg s) -> (Logic,TypeScheme) | Sort _ -> (Info,TypeScheme) - | _ -> if (sort_of env t) == InProp then (Logic,Default) else (Info,Default) + | _ -> if (sort_of env sg t) == InProp then (Logic,Default) else (Info,Default) (*s Two particular cases of [flag_of_type]. *) -let is_default env t = match flag_of_type env t with +let is_default env sg t = match flag_of_type env sg t with | (Info, Default) -> true | _ -> false exception NotDefault of kill_reason -let check_default env t = - match flag_of_type env t with +let check_default env sg t = + match flag_of_type env sg t with | _,TypeScheme -> raise (NotDefault Ktype) | Logic,_ -> raise (NotDefault Kprop) | _ -> () -let is_info_scheme env t = match flag_of_type env t with +let is_info_scheme env sg t = match flag_of_type env sg t with | (Info, TypeScheme) -> true | _ -> false let push_rel_assum (n, t) env = - Environ.push_rel (LocalAssum (n, t)) env + EConstr.push_rel (LocalAssum (n, t)) env + +let push_rels_assum assums = + EConstr.push_rel_context (List.map (fun (x,t) -> LocalAssum (x,t)) assums) + +let get_body lconstr = EConstr.of_constr (Mod_subst.force_constr lconstr) + +let get_opaque env c = + EConstr.of_constr + (Opaqueproof.force_proof (Environ.opaque_tables env) c) + +let applistc c args = EConstr.mkApp (c, Array.of_list args) + +(* Same as [Environ.push_rec_types], but for [EConstr.t] *) +let push_rec_types (lna,typarray,_) env = + let ctxt = + Array.map2_i + (fun i na t -> LocalAssum (na, EConstr.Vars.lift i t)) lna typarray + in + Array.fold_left (fun e assum -> EConstr.push_rel assum e) env ctxt + +(* Same as [Termops.nb_lam], but for [EConstr.t] *) +let nb_lam sg c = List.length (fst (EConstr.decompose_lam sg c)) + +(* Same as [Term.decompose_lam_n] but for [EConstr.t] *) +let decompose_lam_n sg n = + let rec lamdec_rec l n c = + if n <= 0 then l,c + else match EConstr.kind sg c with + | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c + | Cast (c,_,_) -> lamdec_rec l n c + | _ -> raise Not_found + in + lamdec_rec [] n (*s [type_sign] gernerates a signature aimed at treating a type application. *) -let rec type_sign env c = - match Constr.kind (whd_all env c) with +let rec type_sign env sg c = + match EConstr.kind sg (whd_all env sg c) with | Prod (n,t,d) -> - (if is_info_scheme env t then Keep else Kill Kprop) - :: (type_sign (push_rel_assum (n,t) env) d) + (if is_info_scheme env sg t then Keep else Kill Kprop) + :: (type_sign (push_rel_assum (n,t) env) sg d) | _ -> [] -let rec type_scheme_nb_args env c = - match Constr.kind (whd_all env c) with +let rec type_scheme_nb_args env sg c = + match EConstr.kind sg (whd_all env sg c) with | Prod (n,t,d) -> - let n = type_scheme_nb_args (push_rel_assum (n,t) env) d in - if is_info_scheme env t then n+1 else n + let n = type_scheme_nb_args (push_rel_assum (n,t) env) sg d in + if is_info_scheme env sg t then n+1 else n | _ -> 0 -let _ = Hook.set type_scheme_nb_args_hook type_scheme_nb_args +let type_scheme_nb_args' env c = + type_scheme_nb_args env (Evd.from_env env) (EConstr.of_constr c) + +let _ = Hook.set type_scheme_nb_args_hook type_scheme_nb_args' (*s [type_sign_vl] does the same, plus a type var list. *) @@ -147,19 +174,19 @@ let make_typvar n vl = let vl = Id.Set.of_list vl in next_ident_away id' vl -let rec type_sign_vl env c = - match Constr.kind (whd_all env c) with +let rec type_sign_vl env sg c = + match EConstr.kind sg (whd_all env sg c) with | Prod (n,t,d) -> - let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in - if not (is_info_scheme env t) then Kill Kprop::s, vl - else Keep::s, (make_typvar n vl) :: vl + let s,vl = type_sign_vl (push_rel_assum (n,t) env) sg d in + if not (is_info_scheme env sg t) then Kill Kprop::s, vl + else Keep::s, (make_typvar n vl) :: vl | _ -> [],[] -let rec nb_default_params env c = - match Constr.kind (whd_all env c) with +let rec nb_default_params env sg c = + match EConstr.kind sg (whd_all env sg c) with | Prod (n,t,d) -> - let n = nb_default_params (push_rel_assum (n,t) env) d in - if is_default env t then n+1 else n + let n = nb_default_params (push_rel_assum (n,t) env) sg d in + if is_default env sg t then n+1 else n | _ -> 0 (* Enriching a signature with implicit information *) @@ -226,62 +253,62 @@ let parse_ind_args si args relmax = generate ML type var anymore (in subterms for example). *) -let rec extract_type env db j c args = - match Constr.kind (whd_betaiotazeta c) with +let rec extract_type env sg db j c args = + match EConstr.kind sg (whd_betaiotazeta sg c) with | App (d, args') -> - (* We just accumulate the arguments. *) - extract_type env db j d (Array.to_list args' @ args) + (* We just accumulate the arguments. *) + extract_type env sg db j d (Array.to_list args' @ args) | Lambda (_,_,d) -> (match args with | [] -> assert false (* A lambda cannot be a type. *) - | a :: args -> extract_type env db j (subst1 a d) args) + | a :: args -> extract_type env sg db j (EConstr.Vars.subst1 a d) args) | Prod (n,t,d) -> assert (List.is_empty args); let env' = push_rel_assum (n,t) env in - (match flag_of_type env t with + (match flag_of_type env sg t with | (Info, Default) -> (* Standard case: two [extract_type] ... *) - let mld = extract_type env' (0::db) j d [] in + let mld = extract_type env' sg (0::db) j d [] in (match expand env mld with | Tdummy d -> Tdummy d - | _ -> Tarr (extract_type env db 0 t [], mld)) + | _ -> Tarr (extract_type env sg db 0 t [], mld)) | (Info, TypeScheme) when j > 0 -> (* A new type var. *) - let mld = extract_type env' (j::db) (j+1) d [] in + let mld = extract_type env' sg (j::db) (j+1) d [] in (match expand env mld with | Tdummy d -> Tdummy d | _ -> Tarr (Tdummy Ktype, mld)) | _,lvl -> - let mld = extract_type env' (0::db) j d [] in + let mld = extract_type env' sg (0::db) j d [] in (match expand env mld with | Tdummy d -> Tdummy d | _ -> let reason = if lvl == TypeScheme then Ktype else Kprop in Tarr (Tdummy reason, mld))) | Sort _ -> Tdummy Ktype (* The two logical cases. *) - | _ when sort_of env (applistc c args) == InProp -> Tdummy Kprop + | _ when sort_of env sg (applistc c args) == InProp -> Tdummy Kprop | Rel n -> - (match lookup_rel n env with - | LocalDef (_,t,_) -> extract_type env db j (lift n t) args + (match EConstr.lookup_rel n env with + | LocalDef (_,t,_) -> + extract_type env sg db j (EConstr.Vars.lift n t) args | _ -> (* Asks [db] a translation for [n]. *) if n > List.length db then Tunknown else let n' = List.nth db (n-1) in if Int.equal n' 0 then Tunknown else Tvar n') - | Const (kn,u as c) -> - let r = ConstRef kn in - let cb = lookup_constant kn env in - let typ = Typeops.type_of_constant_in env c in - (match flag_of_type env typ with + | Const (kn,u) -> + let r = ConstRef kn in + let typ = type_of env sg (EConstr.mkConstU (kn,u)) in + (match flag_of_type env sg typ with | (Logic,_) -> assert false (* Cf. logical cases above *) | (Info, TypeScheme) -> - let mlt = extract_type_app env db (r, type_sign env typ) args in - (match cb.const_body with + let mlt = extract_type_app env sg db (r, type_sign env sg typ) args in + (match (lookup_constant kn env).const_body with | Undef _ | OpaqueDef _ -> mlt - | Def _ when is_custom r -> mlt + | Def _ when is_custom (ConstRef kn) -> mlt | Def lbody -> - let newc = applistc (Mod_subst.force_constr lbody) args in - let mlt' = extract_type env db j newc [] in + let newc = applistc (get_body lbody) args in + let mlt' = extract_type env sg db j newc [] in (* ML type abbreviations interact badly with Coq *) (* reduction, so [mlt] and [mlt'] might be different: *) (* The more precise is [mlt'], extracted after reduction *) @@ -290,36 +317,51 @@ let rec extract_type env db j c args = if eq_ml_type (expand env mlt) (expand env mlt') then mlt else mlt') | (Info, Default) -> (* Not an ML type, for example [(c:forall X, X->X) Type nat] *) - (match cb.const_body with + (match (lookup_constant kn env).const_body with | Undef _ | OpaqueDef _ -> Tunknown (* Brutal approx ... *) | Def lbody -> (* We try to reduce. *) - let newc = applistc (Mod_subst.force_constr lbody) args in - extract_type env db j newc [])) + let newc = applistc (get_body lbody) args in + extract_type env sg db j newc [])) | Ind ((kn,i),u) -> - let s = (extract_ind env kn).ind_packets.(i).ip_sign in - extract_type_app env db (IndRef (kn,i),s) args + let s = (extract_ind env kn).ind_packets.(i).ip_sign in + extract_type_app env sg db (IndRef (kn,i),s) args | Proj (p,t) -> (* Let's try to reduce, if it hasn't already been done. *) if Projection.unfolded p then Tunknown - else extract_type env db j (mkProj (Projection.unfold p, t)) args + else + extract_type env sg db j (EConstr.mkProj (Projection.unfold p, t)) args | Case _ | Fix _ | CoFix _ -> Tunknown - | Var _ | Meta _ | Evar _ | Cast _ | LetIn _ | Construct _ -> assert false + | Evar _ | Meta _ -> Taxiom (* only possible during Show Extraction *) + | Var v -> + (* For Show Extraction *) + let open Context.Named.Declaration in + (match EConstr.lookup_named v env with + | LocalDef (_,body,_) -> + extract_type env sg db j (EConstr.applist (body,args)) [] + | LocalAssum (_,ty) -> + let r = VarRef v in + (match flag_of_type env sg ty with + | (Logic,_) -> assert false (* Cf. logical cases above *) + | (Info, TypeScheme) -> + extract_type_app env sg db (r, type_sign env sg ty) args + | (Info, Default) -> Tunknown)) + | Cast _ | LetIn _ | Construct _ -> assert false (*s Auxiliary function dealing with type application. Precondition: [r] is a type scheme represented by the signature [s], and is completely applied: [List.length args = List.length s]. *) -and extract_type_app env db (r,s) args = +and extract_type_app env sg db (r,s) args = let ml_args = List.fold_right (fun (b,c) a -> if b == Keep then - let p = List.length (fst (splay_prod env none (EConstr.of_constr (type_of env c)))) in + let p = List.length (fst (splay_prod env sg (type_of env sg c))) in let db = iterate (fun l -> 0 :: l) p db in - (extract_type_scheme env db c p) :: a + (extract_type_scheme env sg db c p) :: a else a) (List.combine s args) [] - in Tglob (r, ml_args) + in Tglob (r, ml_args) (*S Extraction of a type scheme. *) @@ -330,19 +372,18 @@ and extract_type_app env db (r,s) args = (* [db] is a context for translating Coq [Rel] into ML type [Tvar]. *) -and extract_type_scheme env db c p = - if Int.equal p 0 then extract_type env db 0 c [] +and extract_type_scheme env sg db c p = + if Int.equal p 0 then extract_type env sg db 0 c [] else - let c = whd_betaiotazeta c in - match Constr.kind c with + let c = whd_betaiotazeta sg c in + match EConstr.kind sg c with | Lambda (n,t,d) -> - extract_type_scheme (push_rel_assum (n,t) env) db d (p-1) + extract_type_scheme (push_rel_assum (n,t) env) sg db d (p-1) | _ -> - let rels = fst (splay_prod env none (EConstr.of_constr (type_of env c))) in - let rels = List.map (on_snd EConstr.Unsafe.to_constr) rels in + let rels = fst (splay_prod env sg (type_of env sg c)) in let env = push_rels_assum rels env in - let eta_args = List.rev_map mkRel (List.interval 1 p) in - extract_type env db 0 (lift p c) eta_args + let eta_args = List.rev_map EConstr.mkRel (List.interval 1 p) in + extract_type env sg db 0 (EConstr.Vars.lift p c) eta_args (*S Extraction of an inductive type. *) @@ -384,6 +425,7 @@ and extract_really_ind env kn mib = let mip0 = mib.mind_packets.(0) in let npar = mib.mind_nparams in let epar = push_rel_context mib.mind_params_ctxt env in + let sg = Evd.from_env env in (* First pass: we store inductive signatures together with *) (* their type var list. *) let packets = @@ -391,8 +433,9 @@ and extract_really_ind env kn mib = (fun i mip -> let (_,u),_ = Universes.fresh_inductive_instance env (kn,i) in let ar = Inductive.type_of_inductive env ((mib,mip),u) in - let info = (fst (flag_of_type env ar) = Info) in - let s,v = if info then type_sign_vl env ar else [],[] in + let ar = EConstr.of_constr ar in + let info = (fst (flag_of_type env sg ar) = Info) in + let s,v = if info then type_sign_vl env sg ar else [],[] in let t = Array.make (Array.length mip.mind_nf_lc) [] in { ip_typename = mip.mind_typename; ip_consnames = mip.mind_consnames; @@ -424,7 +467,8 @@ and extract_really_ind env kn mib = in let dbmap = parse_ind_args p.ip_sign args (nprods + npar) in let db = db_from_ind dbmap npar in - p.ip_types.(j) <- extract_type_cons epar db dbmap t (npar+1) + p.ip_types.(j) <- + extract_type_cons epar sg db dbmap (EConstr.of_constr t) (npar+1) done done; (* Third pass: we determine special cases. *) @@ -477,10 +521,9 @@ and extract_really_ind env kn mib = (* Is this record officially declared with its projections ? *) (* If so, we use this information. *) begin try - let n = nb_default_params env - (Inductive.type_of_inductive env ((mib,mip0),u)) - in - let check_proj kn = if Cset.mem kn !projs then add_projection n kn ip + let ty = Inductive.type_of_inductive env ((mib,mip0),u) in + let n = nb_default_params env sg (EConstr.of_constr ty) in + let check_proj kn = if Cset.mem kn !projs then add_projection n kn ip in List.iter (Option.iter check_proj) (lookup_projections ip) with Not_found -> () @@ -505,13 +548,13 @@ and extract_really_ind env kn mib = - [i] is the rank of the current product (initially [params_nb+1]) *) -and extract_type_cons env db dbmap c i = - match Constr.kind (whd_all env c) with +and extract_type_cons env sg db dbmap c i = + match EConstr.kind sg (whd_all env sg c) with | Prod (n,t,d) -> let env' = push_rel_assum (n,t) env in let db' = (try Int.Map.find i dbmap with Not_found -> 0) :: db in - let l = extract_type_cons env' db' dbmap d (i+1) in - (extract_type env db 0 t []) :: l + let l = extract_type_cons env' sg db' dbmap d (i+1) in + (extract_type env sg db 0 t []) :: l | _ -> [] (*s Recording the ML type abbreviation of a Coq type scheme constant. *) @@ -526,16 +569,17 @@ and mlt_env env r = match r with match lookup_typedef kn cb with | Some _ as o -> o | None -> - let typ = cb.const_type + let sg = Evd.from_env env in + let typ = EConstr.of_constr cb.const_type (* FIXME not sure if we should instantiate univs here *) in - match flag_of_type env typ with - | Info,TypeScheme -> - let body = Mod_subst.force_constr l_body in - let s = type_sign env typ in - let db = db_from_sign s in - let t = extract_type_scheme env db body (List.length s) - in add_typedef kn cb t; Some t - | _ -> None + match flag_of_type env sg typ with + | Info,TypeScheme -> + let body = get_body l_body in + let s = type_sign env sg typ in + let db = db_from_sign s in + let t = extract_type_scheme env sg db body (List.length s) + in add_typedef kn cb t; Some t + | _ -> None and expand env = type_expand (mlt_env env) and type2signature env = type_to_signature (mlt_env env) @@ -545,16 +589,16 @@ let type_expunge_from_sign env = type_expunge_from_sign (mlt_env env) (*s Extraction of the type of a constant. *) -let record_constant_type env kn opt_typ = +let record_constant_type env sg kn opt_typ = let cb = lookup_constant kn env in match lookup_cst_type kn cb with | Some schema -> schema | None -> let typ = match opt_typ with - | None -> cb.const_type + | None -> EConstr.of_constr cb.const_type | Some typ -> typ in - let mlt = extract_type env [] 1 typ [] in + let mlt = extract_type env sg [] 1 typ [] in let schema = (type_maxvar mlt, mlt) in let () = add_cst_type kn cb schema in schema @@ -566,75 +610,86 @@ let record_constant_type env kn opt_typ = (* [mle] is a ML environment [Mlenv.t]. *) (* [mlt] is the ML type we want our extraction of [(c args)] to have. *) -let rec extract_term env mle mlt c args = - match Constr.kind c with +let rec extract_term env sg mle mlt c args = + match EConstr.kind sg c with | App (f,a) -> - extract_term env mle mlt f (Array.to_list a @ args) + extract_term env sg mle mlt f (Array.to_list a @ args) | Lambda (n, t, d) -> let id = id_of_name n in (match args with | a :: l -> (* We make as many [LetIn] as possible. *) - let d' = mkLetIn (Name id,a,t,applistc d (List.map (lift 1) l)) - in extract_term env mle mlt d' [] + let l' = List.map (EConstr.Vars.lift 1) l in + let d' = EConstr.mkLetIn (Name id,a,t,applistc d l') in + extract_term env sg mle mlt d' [] | [] -> let env' = push_rel_assum (Name id, t) env in let id, a = - try check_default env t; Id id, new_meta() - with NotDefault d -> Dummy, Tdummy d + try check_default env sg t; Id id, new_meta() + with NotDefault d -> Dummy, Tdummy d in let b = new_meta () in (* If [mlt] cannot be unified with an arrow type, then magic! *) let magic = needs_magic (mlt, Tarr (a, b)) in - let d' = extract_term env' (Mlenv.push_type mle a) b d [] in + let d' = extract_term env' sg (Mlenv.push_type mle a) b d [] in put_magic_if magic (MLlam (id, d'))) | LetIn (n, c1, t1, c2) -> let id = id_of_name n in - let env' = push_rel (LocalDef (Name id, c1, t1)) env in + let env' = EConstr.push_rel (LocalDef (Name id, c1, t1)) env in (* We directly push the args inside the [LetIn]. TODO: the opt_let_app flag is supposed to prevent that *) - let args' = List.map (lift 1) args in + let args' = List.map (EConstr.Vars.lift 1) args in (try - check_default env t1; + check_default env sg t1; let a = new_meta () in - let c1' = extract_term env mle a c1 [] in + let c1' = extract_term env sg mle a c1 [] in (* The type of [c1'] is generalized and stored in [mle]. *) let mle' = if generalizable c1' then Mlenv.push_gen mle a else Mlenv.push_type mle a in - MLletin (Id id, c1', extract_term env' mle' mlt c2 args') + MLletin (Id id, c1', extract_term env' sg mle' mlt c2 args') with NotDefault d -> let mle' = Mlenv.push_std_type mle (Tdummy d) in - ast_pop (extract_term env' mle' mlt c2 args')) + ast_pop (extract_term env' sg mle' mlt c2 args')) | Const (kn,_) -> - extract_cst_app env mle mlt kn args + extract_cst_app env sg mle mlt kn args | Construct (cp,_) -> - extract_cons_app env mle mlt cp args + extract_cons_app env sg mle mlt cp args | Proj (p, c) -> - let term = Retyping.expand_projection env (Evd.from_env env) p (EConstr.of_constr c) [] in - let term = EConstr.Unsafe.to_constr term in - extract_term env mle mlt term args + let term = Retyping.expand_projection env (Evd.from_env env) p c [] in + extract_term env sg mle mlt term args | Rel n -> (* As soon as the expected [mlt] for the head is known, *) (* we unify it with an fresh copy of the stored type of [Rel n]. *) let extract_rel mlt = put_magic (mlt, Mlenv.get mle n) (MLrel n) - in extract_app env mle mlt extract_rel args + in extract_app env sg mle mlt extract_rel args | Case ({ci_ind=ip},_,c0,br) -> - extract_app env mle mlt (extract_case env mle (ip,c0,br)) args + extract_app env sg mle mlt (extract_case env sg mle (ip,c0,br)) args | Fix ((_,i),recd) -> - extract_app env mle mlt (extract_fix env mle i recd) args + extract_app env sg mle mlt (extract_fix env sg mle i recd) args | CoFix (i,recd) -> - extract_app env mle mlt (extract_fix env mle i recd) args - | Cast (c,_,_) -> extract_term env mle mlt c args - | Ind _ | Prod _ | Sort _ | Meta _ | Evar _ | Var _ -> assert false + extract_app env sg mle mlt (extract_fix env sg mle i recd) args + | Cast (c,_,_) -> extract_term env sg mle mlt c args + | Evar _ | Meta _ -> MLaxiom + | Var v -> + (* Only during Show Extraction *) + let open Context.Named.Declaration in + let ty = match EConstr.lookup_named v env with + | LocalAssum (_,ty) -> ty + | LocalDef (_,_,ty) -> ty + in + let vty = extract_type env sg [] 0 ty [] in + let extract_var mlt = put_magic (mlt,vty) (MLglob (VarRef v)) in + extract_app env sg mle mlt extract_var args + | Ind _ | Prod _ | Sort _ -> assert false (*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *) -and extract_maybe_term env mle mlt c = - try check_default env (type_of env c); - extract_term env mle mlt c [] +and extract_maybe_term env sg mle mlt c = + try check_default env sg (type_of env sg c); + extract_term env sg mle mlt c [] with NotDefault d -> put_magic (mlt, Tdummy d) (MLdummy d) @@ -644,28 +699,28 @@ and extract_maybe_term env mle mlt c = This gives us the expected type of the head. Then we use the [mk_head] to produce the ML head from this type. *) -and extract_app env mle mlt mk_head args = +and extract_app env sg mle mlt mk_head args = let metas = List.map new_meta args in let type_head = type_recomp (metas, mlt) in - let mlargs = List.map2 (extract_maybe_term env mle) metas args in + let mlargs = List.map2 (extract_maybe_term env sg mle) metas args in mlapp (mk_head type_head) mlargs (*s Auxiliary function used to extract arguments of constant or constructor. *) -and make_mlargs env e s args typs = +and make_mlargs env sg e s args typs = let rec f = function | [], [], _ -> [] - | a::la, t::lt, [] -> extract_maybe_term env e t a :: (f (la,lt,[])) - | a::la, t::lt, Keep::s -> extract_maybe_term env e t a :: (f (la,lt,s)) + | a::la, t::lt, [] -> extract_maybe_term env sg e t a :: (f (la,lt,[])) + | a::la, t::lt, Keep::s -> extract_maybe_term env sg e t a :: (f (la,lt,s)) | _::la, _::lt, _::s -> f (la,lt,s) | _ -> assert false in f (args,typs,s) (*s Extraction of a constant applied to arguments. *) -and extract_cst_app env mle mlt kn args = +and extract_cst_app env sg mle mlt kn args = (* First, the [ml_schema] of the constant, in expanded version. *) - let nb,t = record_constant_type env kn None in + let nb,t = record_constant_type env sg kn None in let schema = nb, expand env t in (* Can we instantiate types variables for this constant ? *) (* In Ocaml, inside the definition of this constant, the answer is no. *) @@ -691,7 +746,7 @@ and extract_cst_app env mle mlt kn args = let ls = List.length s in let la = List.length args in (* The ml arguments, already expunged from known logical ones *) - let mla = make_mlargs env mle s args metas in + let mla = make_mlargs env sg mle s args metas in let mla = if magic1 || lang () != Ocaml then mla else @@ -736,7 +791,7 @@ and extract_cst_app env mle mlt kn args = they are fixed, and thus are not used for the computation. \end{itemize} *) -and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = +and extract_cons_app env sg mle mlt (((kn,i) as ip,j) as cp) args = (* First, we build the type of the constructor, stored in small pieces. *) let mi = extract_ind env kn in let params_nb = mi.ind_nparams in @@ -777,7 +832,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = put_magic_if magic2 (dummy_lams (anonym_or_dummy_lams head' s) (params_nb - la)) else - let mla = make_mlargs env mle s args' metas in + let mla = make_mlargs env sg mle s args' metas in if Int.equal la (ls + params_nb) then put_magic_if (magic2 && not magic1) (head mla) else (* [ params_nb <= la <= ls + params_nb ] *) @@ -788,7 +843,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = (*S Extraction of a case. *) -and extract_case env mle ((kn,i) as ip,c,br) mlt = +and extract_case env sg mle ((kn,i) as ip,c,br) mlt = (* [br]: bodies of each branch (in functional form) *) (* [ni]: number of arguments without parameters in each branch *) let ni = constructors_nrealargs_env env ip in @@ -799,9 +854,9 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = MLexn "absurd case" end else (* [c] has an inductive type, and is not a type scheme type. *) - let t = type_of env c in + let t = type_of env sg c in (* The only non-informative case: [c] is of sort [Prop] *) - if (sort_of env t) == InProp then + if (sort_of env sg t) == InProp then begin add_recursors env kn; (* May have passed unseen if logical ... *) (* Logical singleton case: *) @@ -809,7 +864,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = assert (Int.equal br_size 1); let s = iterate (fun l -> Kill Kprop :: l) ni.(0) [] in let mlt = iterate (fun t -> Tarr (Tdummy Kprop, t)) ni.(0) mlt in - let e = extract_maybe_term env mle mlt br.(0) in + let e = extract_maybe_term env sg mle mlt br.(0) in snd (case_expunge s e) end else @@ -818,7 +873,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = let metas = Array.init (List.length oi.ip_vars) new_meta in (* The extraction of the head. *) let type_head = Tglob (IndRef ip, Array.to_list metas) in - let a = extract_term env mle type_head c [] in + let a = extract_term env sg mle type_head c [] in (* The extraction of each branch. *) let extract_branch i = let r = ConstructRef (ip,i+1) in @@ -829,7 +884,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = let s = List.map (type2sign env) oi.ip_types.(i) in let s = sign_with_implicits r s mi.ind_nparams in (* Extraction of the branch (in functional form). *) - let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in + let e = extract_maybe_term env sg mle (type_recomp (l,mlt)) br.(i) in (* We suppress dummy arguments according to signature. *) let ids,e = case_expunge s e in (List.rev ids, Pusual r, e) @@ -851,12 +906,12 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = (*s Extraction of a (co)-fixpoint. *) -and extract_fix env mle i (fi,ti,ci as recd) mlt = +and extract_fix env sg mle i (fi,ti,ci as recd) mlt = let env = push_rec_types recd env in let metas = Array.map new_meta fi in metas.(i) <- mlt; let mle = Array.fold_left Mlenv.push_type mle metas in - let ei = Array.map2 (extract_maybe_term env mle) metas ci in + let ei = Array.map2 (extract_maybe_term env sg mle) metas ci in MLfix (i, Array.map id_of_name fi, ei) (*S ML declarations. *) @@ -864,34 +919,34 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt = (* [decomp_lams_eta env c t] finds the number [n] of products in the type [t], and decompose the term [c] in [n] lambdas, with eta-expansion if needed. *) -let decomp_lams_eta_n n m env c t = - let rels = fst (splay_prod_n env none n (EConstr.of_constr t)) in - let rels = List.map (fun (LocalAssum (id,c) | LocalDef (id,_,c)) -> (id,EConstr.Unsafe.to_constr c)) rels in - let rels',c = decompose_lam c in +let decomp_lams_eta_n n m env sg c t = + let rels = fst (splay_prod_n env sg n t) in + let rels = List.map (fun (LocalAssum (id,c) | LocalDef (id,_,c)) -> (id,c)) rels in + let rels',c = EConstr.decompose_lam sg c in let d = n - m in (* we'd better keep rels' as long as possible. *) let rels = (List.firstn d rels) @ rels' in - let eta_args = List.rev_map mkRel (List.interval 1 d) in - rels, applistc (lift d c) eta_args + let eta_args = List.rev_map EConstr.mkRel (List.interval 1 d) in + rels, applistc (EConstr.Vars.lift d c) eta_args (* Let's try to identify some situation where extracted code will allow generalisation of type variables *) -let rec gentypvar_ok c = match Constr.kind c with +let rec gentypvar_ok sg c = match EConstr.kind sg c with | Lambda _ | Const _ -> true | App (c,v) -> (* if all arguments are variables, these variables will disappear after extraction (see [empty_s] below) *) - Array.for_all isRel v && gentypvar_ok c - | Cast (c,_,_) -> gentypvar_ok c + Array.for_all (EConstr.isRel sg) v && gentypvar_ok sg c + | Cast (c,_,_) -> gentypvar_ok sg c | _ -> false (*s From a constant to a ML declaration. *) -let extract_std_constant env kn body typ = +let extract_std_constant env sg kn body typ = reset_meta_count (); (* The short type [t] (i.e. possibly with abbreviations). *) - let t = snd (record_constant_type env kn (Some typ)) in + let t = snd (record_constant_type env sg kn (Some typ)) in (* The real type [t']: without head products, expanded, *) (* and with [Tvar] translated to [Tvar'] (not instantiable). *) let l,t' = type_decomp (expand env (var2var' t)) in @@ -906,14 +961,14 @@ let extract_std_constant env kn body typ = break user's clever let-ins and partial applications). *) let rels, c = let n = List.length s - and m = nb_lam Evd.empty (EConstr.of_constr body) (** FIXME *) in - if n <= m then decompose_lam_n n body + and m = nb_lam sg body in + if n <= m then decompose_lam_n sg n body else let s,s' = List.chop m s in if List.for_all ((==) Keep) s' && (lang () == Haskell || sign_kind s != UnsafeLogicalSig) - then decompose_lam_n m body - else decomp_lams_eta_n n m env body typ + then decompose_lam_n sg m body + else decomp_lams_eta_n n m env sg body typ in (* Should we do one eta-expansion to avoid non-generalizable '_a ? *) let rels, c = @@ -921,9 +976,9 @@ let extract_std_constant env kn body typ = let s,s' = List.chop n s in let k = sign_kind s in let empty_s = (k == EmptySig || k == SafeLogicalSig) in - if lang () == Ocaml && empty_s && not (gentypvar_ok c) + if lang () == Ocaml && empty_s && not (gentypvar_ok sg c) && not (List.is_empty s') && not (Int.equal (type_maxvar t) 0) - then decomp_lams_eta_n (n+1) n env body typ + then decomp_lams_eta_n (n+1) n env sg body typ else rels,c in let n = List.length rels in @@ -937,16 +992,16 @@ let extract_std_constant env kn body typ = (* The according Coq environment. *) let env = push_rels_assum rels env in (* The real extraction: *) - let e = extract_term env mle t' c [] in + let e = extract_term env sg mle t' c [] in (* Expunging term and type from dummy lambdas. *) let trm = term_expunge s (ids,e) in trm, type_expunge_from_sign env s t (* Extracts the type of an axiom, honors the Extraction Implicit declaration. *) -let extract_axiom env kn typ = +let extract_axiom env sg kn typ = reset_meta_count (); (* The short type [t] (i.e. possibly with abbreviations). *) - let t = snd (record_constant_type env kn (Some typ)) in + let t = snd (record_constant_type env sg kn (Some typ)) in (* The real type [t']: without head products, expanded, *) (* and with [Tvar] translated to [Tvar'] (not instantiable). *) let l,_ = type_decomp (expand env (var2var' t)) in @@ -955,18 +1010,19 @@ let extract_axiom env kn typ = let s = sign_with_implicits (ConstRef kn) s 0 in type_expunge_from_sign env s t -let extract_fixpoint env vkn (fi,ti,ci) = +let extract_fixpoint env sg vkn (fi,ti,ci) = let n = Array.length vkn in let types = Array.make n (Tdummy Kprop) and terms = Array.make n (MLdummy Kprop) in let kns = Array.to_list vkn in current_fixpoints := kns; (* for replacing recursive calls [Rel ..] by the corresponding [Const]: *) - let sub = List.rev_map mkConst kns in + let sub = List.rev_map EConstr.mkConst kns in for i = 0 to n-1 do - if sort_of env ti.(i) != InProp then + if sort_of env sg ti.(i) != InProp then try - let e,t = extract_std_constant env vkn.(i) (substl sub ci.(i)) ti.(i) in + let e,t = extract_std_constant env sg vkn.(i) + (EConstr.Vars.substl sub ci.(i)) ti.(i) in terms.(i) <- e; types.(i) <- t; with SingletonInductiveBecomesProp id -> @@ -976,32 +1032,33 @@ let extract_fixpoint env vkn (fi,ti,ci) = Dfix (Array.map (fun kn -> ConstRef kn) vkn, terms, types) let extract_constant env kn cb = + let sg = Evd.from_env env in let r = ConstRef kn in - let typ = cb.const_type in + let typ = EConstr.of_constr cb.const_type in let warn_info () = if not (is_custom r) then add_info_axiom r in let warn_log () = if not (constant_has_body cb) then add_log_axiom r in let mk_typ_ax () = - let n = type_scheme_nb_args env typ in + let n = type_scheme_nb_args env sg typ in let ids = iterate (fun l -> anonymous_name::l) n [] in Dtype (r, ids, Taxiom) in let mk_typ c = - let s,vl = type_sign_vl env typ in + let s,vl = type_sign_vl env sg typ in let db = db_from_sign s in - let t = extract_type_scheme env db c (List.length s) + let t = extract_type_scheme env sg db c (List.length s) in Dtype (r, vl, t) in let mk_ax () = - let t = extract_axiom env kn typ in + let t = extract_axiom env sg kn typ in Dterm (r, MLaxiom, t) in let mk_def c = - let e,t = extract_std_constant env kn c typ in + let e,t = extract_std_constant env sg kn c typ in Dterm (r,e,t) in try - match flag_of_type env typ with + match flag_of_type env sg typ with | (Logic,TypeScheme) -> warn_log (); Dtype (r, [], Tdummy Ktype) | (Logic,Default) -> warn_log (); Dterm (r, MLdummy Kprop, Tdummy Kprop) | (Info,TypeScheme) -> @@ -1009,73 +1066,72 @@ let extract_constant env kn cb = | Undef _ -> warn_info (); mk_typ_ax () | Def c -> (match cb.const_proj with - | None -> mk_typ (Mod_subst.force_constr c) - | Some pb -> mk_typ pb.proj_body) + | None -> mk_typ (get_body c) + | Some pb -> mk_typ (EConstr.of_constr pb.proj_body)) | OpaqueDef c -> add_opaque r; - if access_opaque () then - mk_typ (Opaqueproof.force_proof (Environ.opaque_tables env) c) + if access_opaque () then mk_typ (get_opaque env c) else mk_typ_ax ()) | (Info,Default) -> (match cb.const_body with | Undef _ -> warn_info (); mk_ax () | Def c -> (match cb.const_proj with - | None -> mk_def (Mod_subst.force_constr c) - | Some pb -> mk_def pb.proj_body) + | None -> mk_def (get_body c) + | Some pb -> mk_def (EConstr.of_constr pb.proj_body)) | OpaqueDef c -> add_opaque r; - if access_opaque () then - mk_def (Opaqueproof.force_proof (Environ.opaque_tables env) c) + if access_opaque () then mk_def (get_opaque env c) else mk_ax ()) with SingletonInductiveBecomesProp id -> error_singleton_become_prop id (Some (ConstRef kn)) let extract_constant_spec env kn cb = + let sg = Evd.from_env env in let r = ConstRef kn in - let typ = cb.const_type in + let typ = EConstr.of_constr cb.const_type in try - match flag_of_type env typ with + match flag_of_type env sg typ with | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype)) | (Logic, Default) -> Sval (r, Tdummy Kprop) | (Info, TypeScheme) -> - let s,vl = type_sign_vl env typ in + let s,vl = type_sign_vl env sg typ in (match cb.const_body with | Undef _ | OpaqueDef _ -> Stype (r, vl, None) | Def body -> let db = db_from_sign s in - let body = Mod_subst.force_constr body in - let t = extract_type_scheme env db body (List.length s) - in Stype (r, vl, Some t)) + let body = get_body body in + let t = extract_type_scheme env sg db body (List.length s) + in Stype (r, vl, Some t)) | (Info, Default) -> - let t = snd (record_constant_type env kn (Some typ)) in - Sval (r, type_expunge env t) + let t = snd (record_constant_type env sg kn (Some typ)) in + Sval (r, type_expunge env t) with SingletonInductiveBecomesProp id -> error_singleton_become_prop id (Some (ConstRef kn)) -let extract_with_type env c = +let extract_with_type env sg c = try - let typ = type_of env c in - match flag_of_type env typ with + let typ = type_of env sg c in + match flag_of_type env sg typ with | (Info, TypeScheme) -> - let s,vl = type_sign_vl env typ in - let db = db_from_sign s in - let t = extract_type_scheme env db c (List.length s) in - Some (vl, t) + let s,vl = type_sign_vl env sg typ in + let db = db_from_sign s in + let t = extract_type_scheme env sg db c (List.length s) in + Some (vl, t) | _ -> None with SingletonInductiveBecomesProp id -> error_singleton_become_prop id None -let extract_constr env c = +let extract_constr env sg c = reset_meta_count (); try - let typ = type_of env c in - match flag_of_type env typ with + let typ = type_of env sg c in + match flag_of_type env sg typ with | (_,TypeScheme) -> MLdummy Ktype, Tdummy Ktype | (Logic,_) -> MLdummy Kprop, Tdummy Kprop | (Info,Default) -> - let mlt = extract_type env [] 1 typ [] in - extract_term env Mlenv.empty mlt c [], mlt + let mlt = extract_type env sg [] 1 typ [] in + extract_term env sg Mlenv.empty mlt c [], mlt with SingletonInductiveBecomesProp id -> error_singleton_become_prop id None diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli index a0f2885a42..d27c79cb62 100644 --- a/plugins/extraction/extraction.mli +++ b/plugins/extraction/extraction.mli @@ -11,9 +11,9 @@ (*s Extraction from Coq terms to Miniml. *) open Names -open Constr open Declarations open Environ +open Evd open Miniml val extract_constant : env -> Constant.t -> constant_body -> ml_decl @@ -22,16 +22,18 @@ val extract_constant_spec : env -> Constant.t -> constant_body -> ml_spec (** For extracting "module ... with ..." declaration *) -val extract_with_type : env -> constr -> ( Id.t list * ml_type ) option +val extract_with_type : + env -> evar_map -> EConstr.t -> ( Id.t list * ml_type ) option val extract_fixpoint : - env -> Constant.t array -> (constr, types) prec_declaration -> ml_decl + env -> evar_map -> Constant.t array -> + (EConstr.t, EConstr.types) Constr.prec_declaration -> ml_decl val extract_inductive : env -> MutInd.t -> ml_ind -(** For extraction compute *) +(** For Extraction Compute and Show Extraction *) -val extract_constr : env -> constr -> ml_ast * ml_type +val extract_constr : env -> evar_map -> EConstr.t -> ml_ast * ml_type (*s Is a [ml_decl] or a [ml_spec] logical ? *) diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 468f2fe8ca..93909f3e64 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -160,3 +160,9 @@ VERNAC COMMAND EXTEND ExtractionInductive CLASSIFIED AS SIDEFF mlname(id) "[" mlname_list(idl) "]" string_opt(o) ] -> [ extract_inductive x id idl o ] END +(* Show the extraction of the current proof *) + +VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY +| [ "Show" "Extraction" ] + -> [ show_extraction () ] +END diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 0bcda69d4d..6c421491fc 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -38,14 +38,13 @@ module Refset' = Refset_env let occur_kn_in_ref kn = function | IndRef (kn',_) | ConstructRef ((kn',_),_) -> MutInd.equal kn kn' - | ConstRef _ -> false - | VarRef _ -> assert false + | ConstRef _ | VarRef _ -> false let repr_of_r = function | ConstRef kn -> Constant.repr3 kn | IndRef (kn,_) | ConstructRef ((kn,_),_) -> MutInd.repr3 kn - | VarRef _ -> assert false + | VarRef v -> KerName.repr (Lib.make_kn v) let modpath_of_r r = let mp,_,_ = repr_of_r r in mp @@ -279,7 +278,7 @@ let safe_basename_of_global r = | ConstructRef ((kn,i),j) -> (try (unsafe_lookup_ind kn).ind_packets.(i).ip_consnames.(j-1) with Not_found -> last_chance r) - | VarRef _ -> assert false + | VarRef v -> v let string_of_global r = try string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty r) diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.ml4 index b3bcc99840..2251a66204 100644 --- a/plugins/ltac/g_eqdecide.ml4 +++ b/plugins/ltac/g_eqdecide.ml4 @@ -15,6 +15,7 @@ (************************************************************************) open Eqdecide +open Stdarg DECLARE PLUGIN "ltac_plugin" diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 6e38b46413..e0368153e5 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1922,7 +1922,7 @@ let build_morphism_signature env sigma m = in let morph = e_app_poly env evd PropGlobal.proper_type [| t; sig_; m |] in let evd = solve_constraints env !evd in - let evd = Evd.nf_constraints evd in + let evd = Evd.minimize_universes evd in let m = Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr morph) in Pretyping.check_evars env Evd.empty evd (EConstr.of_constr m); Evd.evar_universe_context evd, m diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 4665ff9ed3..2c7ebb7458 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -16,6 +16,7 @@ open Misctypes open Genarg open Stdarg open Geninterp +open Pp exception CannotCoerceTo of string @@ -94,6 +95,38 @@ let to_option v = prj Val.typ_opt v let to_pair v = prj Val.typ_pair v +let cast_error wit v = + let pr_v = Pptactic.pr_value Pptactic.ltop v in + let Val.Dyn (tag, _) = v in + let tag = Val.pr tag in + CErrors.user_err (str "Type error: value " ++ pr_v ++ str " is a " ++ tag + ++ str " while type " ++ Val.pr wit ++ str " was expected.") + +let unbox wit v ans = match ans with +| None -> cast_error wit v +| Some x -> x + +let rec prj : type a. a Val.tag -> Val.t -> a = fun tag v -> match tag with +| Val.List tag -> List.map (fun v -> prj tag v) (unbox Val.typ_list v (to_list v)) +| Val.Opt tag -> Option.map (fun v -> prj tag v) (unbox Val.typ_opt v (to_option v)) +| Val.Pair (tag1, tag2) -> + let (x, y) = unbox Val.typ_pair v (to_pair v) in + (prj tag1 x, prj tag2 y) +| Val.Base t -> + let Val.Dyn (t', x) = v in + match Val.eq t t' with + | None -> cast_error t v + | Some Refl -> x +let rec tag_of_arg : type a b c. (a, b, c) genarg_type -> c Val.tag = fun wit -> match wit with +| ExtraArg _ -> Geninterp.val_tag (topwit wit) +| ListArg t -> Val.List (tag_of_arg t) +| OptArg t -> Val.Opt (tag_of_arg t) +| PairArg (t1, t2) -> Val.Pair (tag_of_arg t1, tag_of_arg t2) + +let val_cast arg v = prj (tag_of_arg arg) v + +let cast (Topwit wit) v = val_cast wit v + end let is_variable env id = @@ -334,3 +367,46 @@ let coerce_to_int_or_var_list v = | Some l -> let map n = ArgArg (coerce_to_int n) in List.map map l + +(** Abstract application, to print ltac functions *) +type appl = + | UnnamedAppl (** For generic applications: nothing is printed *) + | GlbAppl of (Names.KerName.t * Val.t list) list + (** For calls to global constants, some may alias other. *) + +(* Values for interpretation *) +type tacvalue = + | VFun of appl*Tacexpr.ltac_trace * Val.t Id.Map.t * + Name.t list * Tacexpr.glob_tactic_expr + | VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr + +let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) = + let wit = Genarg.create_arg "tacvalue" in + let () = register_val0 wit None in + let () = Genprint.register_val_print0 (base_val_typ wit) + (fun _ -> Genprint.TopPrinterBasic (fun () -> str "<tactic closure>")) in + wit + +let pr_argument_type arg = + let Val.Dyn (tag, _) = arg in + Val.pr tag + +(** TODO: unify printing of generic Ltac values in case of coercion failure. *) + +(* Displays a value *) +let pr_value env v = + let pr_with_env pr = + match env with + | Some (env,sigma) -> pr env sigma + | None -> str "a value of type" ++ spc () ++ pr_argument_type v in + let open Genprint in + match generic_val_print v with + | TopPrinterBasic pr -> pr () + | TopPrinterNeedsContext pr -> pr_with_env pr + | TopPrinterNeedsContextAndLevel { default_already_surrounded; printer } -> + pr_with_env (fun env sigma -> printer env sigma default_already_surrounded) + +let error_ltac_variable ?loc id env v s = + CErrors.user_err ?loc (str "Ltac variable " ++ Id.print id ++ + strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++ + strbrk "which cannot be coerced to " ++ str s ++ str".") diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index ce05d70e88..1fa5e3c076 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -42,6 +42,7 @@ sig val to_list : t -> t list option val to_option : t -> t option option val to_pair : t -> (t * t) option + val cast : 'a typed_abstract_argument_type -> Geninterp.Val.t -> 'a end (** {5 Coercion functions} *) @@ -92,3 +93,21 @@ val coerce_to_int_or_var_list : Value.t -> int or_var list val wit_constr_context : (Empty.t, Empty.t, EConstr.constr) genarg_type val wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_binders) genarg_type + +val error_ltac_variable : ?loc:Loc.t -> Id.t -> + (Environ.env * Evd.evar_map) option -> Value.t -> string -> 'a + +(** Abstract application, to print ltac functions *) +type appl = + | UnnamedAppl (** For generic applications: nothing is printed *) + | GlbAppl of (Names.KerName.t * Val.t list) list + (** For calls to global constants, some may alias other. *) + +type tacvalue = + | VFun of appl*Tacexpr.ltac_trace * Val.t Id.Map.t * + Name.t list * Tacexpr.glob_tactic_expr + | VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr + +val wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type + +val pr_value : (Environ.env * Evd.evar_map) option -> Geninterp.Val.t -> Pp.t diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 42f2abd73c..566fc28733 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -554,3 +554,138 @@ let () = AnyEntry Pltac.tactic_arg; ] in register_grammars_by_name "tactic" entries + +type _ ty_sig = +| TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig +| TyIdent : string * 'r ty_sig -> 'r ty_sig +| TyArg : + (('a, 'b, 'c) Extend.ty_user_symbol * Id.t) Loc.located * 'r ty_sig -> ('c -> 'r) ty_sig +| TyAnonArg : + ('a, 'b, 'c) Extend.ty_user_symbol Loc.located * 'r ty_sig -> 'r ty_sig + +type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml + +let rec untype_user_symbol : type a b c. (a,b,c) ty_user_symbol -> Genarg.ArgT.any user_symbol = fun tu -> + match tu with + | TUlist1 l -> Ulist1(untype_user_symbol l) + | TUlist1sep(l,s) -> Ulist1sep(untype_user_symbol l, s) + | TUlist0 l -> Ulist0(untype_user_symbol l) + | TUlist0sep(l,s) -> Ulist0sep(untype_user_symbol l, s) + | TUopt(o) -> Uopt(untype_user_symbol o) + | TUentry a -> Uentry (Genarg.ArgT.Any a) + | TUentryl (a,i) -> Uentryl (Genarg.ArgT.Any a,i) + +let rec clause_of_sign : type a. a ty_sig -> Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list = + fun sign -> match sign with + | TyNil -> [] + | TyIdent (s, sig') -> TacTerm s :: clause_of_sign sig' + | TyArg ((loc,(a,id)),sig') -> + TacNonTerm (loc,(untype_user_symbol a,Some id)) :: clause_of_sign sig' + | TyAnonArg ((loc,a),sig') -> + TacNonTerm (loc,(untype_user_symbol a,None)) :: clause_of_sign sig' + +let clause_of_ty_ml = function + | TyML (t,_) -> clause_of_sign t + +let rec prj : type a b c. (a,b,c) Extend.ty_user_symbol -> (a,b,c) genarg_type = function + | TUentry a -> ExtraArg a + | TUentryl (a,l) -> ExtraArg a + | TUopt(o) -> OptArg (prj o) + | TUlist1 l -> ListArg (prj l) + | TUlist1sep (l,_) -> ListArg (prj l) + | TUlist0 l -> ListArg (prj l) + | TUlist0sep (l,_) -> ListArg (prj l) + +let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic = + fun sign tac -> + match sign with + | TyNil -> + begin fun vals ist -> match vals with + | [] -> tac ist + | _ :: _ -> assert false + end + | TyIdent (s, sig') -> eval_sign sig' tac + | TyArg ((_loc,(a,id)), sig') -> + let f = eval_sign sig' in + begin fun tac vals ist -> match vals with + | [] -> assert false + | v :: vals -> + let v' = Taccoerce.Value.cast (topwit (prj a)) v in + f (tac v') vals ist + end tac + | TyAnonArg ((_loc,a), sig') -> eval_sign sig' tac + +let eval : ty_ml -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic = function + | TyML (t,tac) -> eval_sign t tac + +let is_constr_entry = function +| TUentry a -> Option.has_some @@ genarg_type_eq (ExtraArg a) Stdarg.wit_constr +| _ -> false + +let rec only_constr : type a. a ty_sig -> bool = function +| TyNil -> true +| TyIdent(_,_) -> false +| TyArg((_,(u,_)),s) -> if is_constr_entry u then only_constr s else false +| TyAnonArg((_,u),s) -> if is_constr_entry u then only_constr s else false + +let rec mk_sign_vars : type a. a ty_sig -> Name.t list = function +| TyNil -> [] +| TyIdent (_,s) -> mk_sign_vars s +| TyArg((_,(_,name)),s) -> Name name :: mk_sign_vars s +| TyAnonArg((_,_),s) -> Anonymous :: mk_sign_vars s + +let dummy_id = Id.of_string "_" + +let lift_constr_tac_to_ml_tac vars tac = + let tac _ ist = Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in + let map = function + | Anonymous -> None + | Name id -> + let c = Id.Map.find id ist.Geninterp.lfun in + try Some (Taccoerce.Value.of_constr @@ Taccoerce.coerce_to_closed_constr env c) + with Taccoerce.CannotCoerceTo ty -> + Taccoerce.error_ltac_variable dummy_id (Some (env,sigma)) c ty + in + let args = List.map_filter map vars in + tac args ist + end in + tac + +let tactic_extend plugin_name tacname ~level sign = + let open Tacexpr in + let ml_tactic_name = + { mltac_tactic = tacname; + mltac_plugin = plugin_name } + in + match sign with + | [TyML (TyIdent (name, s),tac) as ml_tac] when only_constr s -> + (** The extension is only made of a name followed by constr entries: we do not + add any grammar nor printing rule and add it as a true Ltac definition. *) + (* + let patt = make_patt rem in + let vars = List.map make_var rem in + let vars = mlexpr_of_list (mlexpr_of_name mlexpr_of_ident) vars in + *) + let vars = mk_sign_vars s in + let ml = { Tacexpr.mltac_name = ml_tactic_name; Tacexpr.mltac_index = 0 } in + let tac = match s with + | TyNil -> eval ml_tac + (** Special handling of tactics without arguments: such tactics do not do + a Proofview.Goal.nf_enter to compute their arguments. It matters for some + whole-prof tactics like [shelve_unifiable]. *) + | _ -> lift_constr_tac_to_ml_tac vars (eval ml_tac) + in + (** Arguments are not passed directly to the ML tactic in the TacML node, + the ML tactic retrieves its arguments in the [ist] environment instead. + This is the rôle of the [lift_constr_tac_to_ml_tac] function. *) + let body = Tacexpr.TacFun (vars, Tacexpr.TacML (Loc.tag (ml, [])))in + let id = Names.Id.of_string name in + let obj () = Tacenv.register_ltac true false id body in + let () = Tacenv.register_ml_tactic ml_tactic_name [|tac|] in + Mltop.declare_cache_obj obj plugin_name + | _ -> + let obj () = add_ml_tactic_notation ml_tactic_name ~level (List.map clause_of_ty_ml sign) in + Tacenv.register_ml_tactic ml_tactic_name @@ Array.of_list (List.map eval sign); + Mltop.declare_cache_obj obj plugin_name diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 02e2f0f60e..3f804ee8d1 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -67,3 +67,15 @@ val print_ltacs : unit -> unit val print_located_tactic : Libnames.reference -> unit (** Display the absolute name of a tactic. *) + +type _ ty_sig = +| TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig +| TyIdent : string * 'r ty_sig -> 'r ty_sig +| TyArg : + (('a, 'b, 'c) Extend.ty_user_symbol * Names.Id.t) Loc.located * 'r ty_sig -> ('c -> 'r) ty_sig +| TyAnonArg : + ('a, 'b, 'c) Extend.ty_user_symbol Loc.located * 'r ty_sig -> 'r ty_sig + +type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml + +val tactic_extend : string -> string -> level:Int.t -> ty_ml list -> unit diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index cd9d9bac2c..991afe9c60 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -79,9 +79,6 @@ let out_gen wit v = let val_tag wit = val_tag (topwit wit) -let base_val_typ wit = - match val_tag wit with Val.Base t -> t | _ -> anomaly (str "Not a base val.") - let pr_argument_type arg = let Val.Dyn (tag, _) = arg in Val.pr tag @@ -93,11 +90,6 @@ let safe_msgnl s = type value = Val.t -(** Abstract application, to print ltac functions *) -type appl = - | UnnamedAppl (** For generic applications: nothing is printed *) - | GlbAppl of (Names.KerName.t * Val.t list) list - (** For calls to global constants, some may alias other. *) let push_appl appl args = match appl with | UnnamedAppl -> UnnamedAppl @@ -121,19 +113,6 @@ let combine_appl appl1 appl2 = | UnnamedAppl,a | a,UnnamedAppl -> a | GlbAppl l1 , GlbAppl l2 -> GlbAppl (l2@l1) -(* Values for interpretation *) -type tacvalue = - | VFun of appl*ltac_trace * value Id.Map.t * - Name.t list * glob_tactic_expr - | VRec of value Id.Map.t ref * glob_tactic_expr - -let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) = - let wit = Genarg.create_arg "tacvalue" in - let () = register_val0 wit None in - let () = Genprint.register_val_print0 (base_val_typ wit) - (fun _ -> Genprint.TopPrinterBasic (fun () -> str "<tactic closure>")) in - wit - let of_tacvalue v = in_gen (topwit wit_tacvalue) v let to_tacvalue v = out_gen (topwit wit_tacvalue) v @@ -169,39 +148,6 @@ module Value = struct let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in of_tacvalue closure - let cast_error wit v = - let pr_v = Pptactic.pr_value Pptactic.ltop v in - let Val.Dyn (tag, _) = v in - let tag = Val.pr tag in - user_err (str "Type error: value " ++ pr_v ++ str " is a " ++ tag - ++ str " while type " ++ Val.pr wit ++ str " was expected.") - - let unbox wit v ans = match ans with - | None -> cast_error wit v - | Some x -> x - - let rec prj : type a. a Val.tag -> Val.t -> a = fun tag v -> match tag with - | Val.List tag -> List.map (fun v -> prj tag v) (unbox Val.typ_list v (to_list v)) - | Val.Opt tag -> Option.map (fun v -> prj tag v) (unbox Val.typ_opt v (to_option v)) - | Val.Pair (tag1, tag2) -> - let (x, y) = unbox Val.typ_pair v (to_pair v) in - (prj tag1 x, prj tag2 y) - | Val.Base t -> - let Val.Dyn (t', x) = v in - match Val.eq t t' with - | None -> cast_error t v - | Some Refl -> x - - let rec tag_of_arg : type a b c. (a, b, c) genarg_type -> c Val.tag = fun wit -> match wit with - | ExtraArg _ -> val_tag wit - | ListArg t -> Val.List (tag_of_arg t) - | OptArg t -> Val.Opt (tag_of_arg t) - | PairArg (t1, t2) -> Val.Pair (tag_of_arg t1, tag_of_arg t2) - - let val_cast arg v = prj (tag_of_arg arg) v - - let cast (Topwit wit) v = val_cast wit v - end let print_top_val env v = Pptactic.pr_value Pptactic.ltop v @@ -233,21 +179,6 @@ let curr_debug ist = match TacStore.get ist.extra f_debug with | None -> DebugOff | Some level -> level -(** TODO: unify printing of generic Ltac values in case of coercion failure. *) - -(* Displays a value *) -let pr_value env v = - let pr_with_env pr = - match env with - | Some (env,sigma) -> pr env sigma - | None -> str "a value of type" ++ spc () ++ pr_argument_type v in - let open Genprint in - match generic_val_print v with - | TopPrinterBasic pr -> pr () - | TopPrinterNeedsContext pr -> pr_with_env pr - | TopPrinterNeedsContextAndLevel { default_already_surrounded; printer } -> - pr_with_env (fun env sigma -> printer env sigma default_already_surrounded) - let pr_closure env ist body = let pp_body = Pptactic.pr_glob_tactic env body in let pr_sep () = fnl () in @@ -360,15 +291,11 @@ let debugging_exception_step ist signal_anomaly e pp = debugging_step ist (fun () -> pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ explain_exc e) -let error_ltac_variable ?loc id env v s = - user_err ?loc (str "Ltac variable " ++ Id.print id ++ - strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++ - strbrk "which cannot be coerced to " ++ str s ++ str".") - (* Raise Not_found if not in interpretation sign *) let try_interp_ltac_var coerce ist env {loc;v=id} = let v = Id.Map.find id ist.lfun in - try coerce v with CannotCoerceTo s -> error_ltac_variable ?loc id env v s + try coerce v with CannotCoerceTo s -> + Taccoerce.error_ltac_variable ?loc id env v s let interp_ltac_var coerce ist env locid = try try_interp_ltac_var coerce ist env locid @@ -2090,27 +2017,6 @@ let _ = in Pretyping.register_constr_interp0 wit_tactic eval -(** Used in tactic extension **) - -let dummy_id = Id.of_string "_" - -let lift_constr_tac_to_ml_tac vars tac = - let tac _ ist = Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = project gl in - let map = function - | Anonymous -> None - | Name id -> - let c = Id.Map.find id ist.lfun in - try Some (coerce_to_closed_constr env c) - with CannotCoerceTo ty -> - error_ltac_variable dummy_id (Some (env,sigma)) c ty - in - let args = List.map_filter map vars in - tac args ist - end in - tac - let vernac_debug b = set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff) diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index 3f3b8e5558..bd44bdbea4 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -133,13 +133,5 @@ val interp_int : interp_sign -> lident -> int val interp_int_or_var : interp_sign -> int or_var -> int -val error_ltac_variable : ?loc:Loc.t -> Id.t -> - (Environ.env * Evd.evar_map) option -> value -> string -> 'a - -(** Transforms a constr-expecting tactic into a tactic finding its arguments in - the Ltac environment according to the given names. *) -val lift_constr_tac_to_ml_tac : Name.t list -> - (constr list -> Geninterp.interp_sign -> unit Proofview.tactic) -> Tacenv.ml_tactic - val default_ist : unit -> Geninterp.interp_sign (** Empty ist with debug set on the current value. *) diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4 index c8112eaa99..4ac49adb90 100644 --- a/plugins/nsatz/g_nsatz.ml4 +++ b/plugins/nsatz/g_nsatz.ml4 @@ -9,6 +9,7 @@ (************************************************************************) open Ltac_plugin +open Stdarg DECLARE PLUGIN "nsatz_plugin" diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 43c29a08a8..f049963f1c 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1193,7 +1193,7 @@ let pf_interp_gen_aux gl to_ind ((oclr, occ), t) = else let gl, ccl = pf_mkprod gl c cl in false, pat, ccl, c, clr,ucst,gl else if to_ind && occ = None then let nv, p, _, ucst' = pf_abs_evars gl (fst pat, c) in - let ucst = Evd.union_evar_universe_context ucst ucst' in + let ucst = UState.union ucst ucst' in if nv = 0 then anomaly "occur_existential but no evars" else let gl, pty = pfe_type_of gl p in false, pat, EConstr.mkProd (constr_name (project gl) c, pty, Tacmach.pf_concl gl), p, clr,ucst,gl diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 859513d5cd..57635edac4 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -216,7 +216,7 @@ let same_proj sigma t1 t2 = let all_ok _ _ = true let fake_pmatcher_end () = - mkProp, L2R, (Evd.empty, Evd.empty_evar_universe_context, mkProp) + mkProp, L2R, (Evd.empty, UState.empty, mkProp) let unfoldintac occ rdx t (kt,_) gl = let fs sigma x = Reductionops.nf_evar sigma x in diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 62c35d6dfa..33b18001c9 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -361,7 +361,7 @@ let unif_end env sigma0 ise0 pt ok = if ise2 == ise1 then (s, uc, t) else let s, uc', t = nf_open_term sigma0 ise2 t in - s, Evd.union_evar_universe_context uc uc', t + s, UState.union uc uc', t let unify_HO env sigma0 t1 t2 = let sigma = unif_HO env sigma0 t1 t2 in @@ -1268,7 +1268,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let sigma,pat= mk_tpattern ?hack env sigma0 (sigma,p) ok L2R (fs sigma t) in sigma, [pat] in match pattern with - | None -> do_subst env0 concl0 concl0 1, Evd.empty_evar_universe_context + | None -> do_subst env0 concl0 concl0 1, UState.empty | Some (sigma, (T rp | In_T rp)) -> let rp = fs sigma rp in let ise = create_evar_defs sigma in diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 0a63985bf1..fe2e86a482 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -530,8 +530,15 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty UnifFailure (evd, NotSameHead) else begin - let evd' = check_leq_inductives evd cumi u u' in - Success (check_leq_inductives evd' cumi u' u) + (** Both constructors should be liftable to the same supertype + at which we compare them, but we don't have access to that type in + untyped unification. We hence try to enforce that one is lower + than the other, also unifying more universes in the process. + If this fails we just leave the universes as is, as in conversion. *) + try Success (check_leq_inductives evd cumi u u') + with Univ.UniverseInconsistency _ -> + try Success (check_leq_inductives evd cumi u' u) + with Univ.UniverseInconsistency e -> Success evd end end in diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml index d16f046fab..8864be5761 100644 --- a/pretyping/univdecls.ml +++ b/pretyping/univdecls.ml @@ -38,7 +38,7 @@ let interp_univ_constraints env evd cstrs = let interp_univ_decl env decl = let open Misctypes in let pl : lident list = decl.univdecl_instance in - let evd = Evd.from_ctx (Evd.make_evar_universe_context env (Some pl)) in + let evd = Evd.from_ctx (UState.make_with_initial_binders (Environ.universes env) pl) in let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in let decl = { univdecl_instance = pl; univdecl_extensible_instance = decl.univdecl_extensible_instance; diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 3682b7c25b..9da94e42ae 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -94,7 +94,7 @@ let print_ref reduce ref udecl = let env = Global.env () in let bl = Universes.universe_binders_with_opt_names ref (Array.to_list (Univ.Instance.to_array inst)) udecl in - let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in + let sigma = Evd.from_ctx (UState.of_binders bl) in let inst = if Global.is_polymorphic ref then Printer.pr_universe_instance sigma univs else mt () @@ -593,7 +593,7 @@ let print_constant with_values sep sp udecl = Array.to_list (Instance.to_array inst) in let ctx = - Evd.evar_universe_context_of_binders + UState.of_binders (Universes.universe_binders_with_opt_names (ConstRef sp) ulist udecl) in let env = Global.env () and sigma = Evd.from_ctx ctx in diff --git a/printing/printer.ml b/printing/printer.ml index 917ee2021a..e50d302b33 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -539,7 +539,7 @@ let pr_evgl_sign sigma evi = let ids = List.rev_map NamedDecl.get_id l in let warn = if List.is_empty ids then mt () else - (str "(" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)") + (str " (" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)") in let pc = pr_lconstr_env env sigma evi.evar_concl in let candidates = @@ -551,7 +551,7 @@ let pr_evgl_sign sigma evi = mt () in hov 0 (str"[" ++ ps ++ spc () ++ str"|- " ++ pc ++ str"]" ++ - candidates ++ spc () ++ warn) + candidates ++ warn) (* Print an existential variable *) @@ -560,15 +560,25 @@ let pr_evar sigma (evk, evi) = hov 0 (pr_existential_key sigma evk ++ str " : " ++ pegl) (* Print an enumerated list of existential variables *) -let rec pr_evars_int_hd head sigma i = function +let rec pr_evars_int_hd pr sigma i = function | [] -> mt () | (evk,evi)::rest -> - (hov 0 (head i ++ pr_evar sigma (evk,evi))) ++ - (match rest with [] -> mt () | _ -> fnl () ++ pr_evars_int_hd head sigma (i+1) rest) - -let pr_evars_int sigma i evs = pr_evars_int_hd (fun i -> str "Existential " ++ int i ++ str " =" ++ spc ()) sigma i (Evar.Map.bindings evs) - -let pr_evars sigma evs = pr_evars_int_hd (fun i -> mt ()) sigma 1 (Evar.Map.bindings evs) + (hov 0 (pr i evk evi)) ++ + (match rest with [] -> mt () | _ -> fnl () ++ pr_evars_int_hd pr sigma (i+1) rest) + +let pr_evars_int sigma ~shelf ~givenup i evs = + let pr_status i = + if List.mem i shelf then str " (shelved)" + else if List.mem i givenup then str " (given up)" + else mt () in + pr_evars_int_hd + (fun i evk evi -> + str "Existential " ++ int i ++ str " =" ++ + spc () ++ pr_evar sigma (evk,evi) ++ pr_status evk) + sigma i (Evar.Map.bindings evs) + +let pr_evars sigma evs = + pr_evars_int_hd (fun i evk evi -> pr_evar sigma (evk,evi)) sigma 1 (Evar.Map.bindings evs) (* Display a list of evars given by their name, with a prefix *) let pr_ne_evar_set hd tl sigma l = @@ -686,7 +696,7 @@ let print_dependent_evars gl sigma seeds = (* spiwack: [pr_first] is true when the first goal must be singled out and printed in its entirety. *) let default_pr_subgoals ?(pr_first=true) - close_cmd sigma seeds shelf stack unfocused goals = + close_cmd sigma ~seeds ~shelf ~stack ~unfocused ~goals = (** Printing functions for the extra informations. *) let rec print_stack a = function | [] -> Pp.int a @@ -748,7 +758,7 @@ let default_pr_subgoals ?(pr_first=true) if Evar.Map.is_empty exl then (str"No more subgoals." ++ print_dependent_evars None sigma seeds) else - let pei = pr_evars_int sigma 1 exl in + let pei = pr_evars_int sigma ~shelf ~givenup:[] 1 exl in v 0 ((str "No more subgoals," ++ str " but there are non-instantiated existential variables:" ++ cut () ++ (hov 0 pei) @@ -775,7 +785,7 @@ let default_pr_subgoals ?(pr_first=true) type printer_pr = { - pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> Evar.t list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t; + pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> seeds:goal list -> shelf:goal list -> stack:int list -> unfocused:goal list -> goals:goal list -> Pp.t; pr_subgoal : int -> evar_map -> goal list -> Pp.t; pr_goal : goal sigma -> Pp.t; } @@ -809,16 +819,16 @@ let pr_open_subgoals ~proof = begin match goals with | [] -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in begin match bgoals,shelf,given_up with - | [] , [] , [] -> pr_subgoals None sigma seeds shelf stack [] goals + | [] , [] , [] -> pr_subgoals None sigma ~seeds ~shelf ~stack ~unfocused:[] ~goals | [] , [] , _ -> Feedback.msg_info (str "No more subgoals, but there are some goals you gave up:"); fnl () - ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] [] given_up + ++ pr_subgoals ~pr_first:false None bsigma ~seeds ~shelf:[] ~stack:[] ~unfocused:[] ~goals:given_up ++ fnl () ++ str "You need to go back and solve them." | [] , _ , _ -> Feedback.msg_info (str "All the remaining goals are on the shelf."); fnl () - ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] [] shelf + ++ pr_subgoals ~pr_first:false None bsigma ~seeds ~shelf:[] ~stack:[] ~unfocused:[] ~goals:shelf | _ , _, _ -> let end_cmd = str "This subproof is complete, but there are some unfocused goals." ++ @@ -826,13 +836,13 @@ let pr_open_subgoals ~proof = if Pp.ismt s then s else fnl () ++ s) ++ fnl () in - pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] [] bgoals + pr_subgoals ~pr_first:false (Some end_cmd) bsigma ~seeds ~shelf ~stack:[] ~unfocused:[] ~goals:bgoals end | _ -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in let bgoals_focused, bgoals_unfocused = List.partition (fun x -> List.mem x goals) bgoals in let unfocused_if_needed = if should_unfoc() then bgoals_unfocused else [] in - pr_subgoals ~pr_first:true None bsigma seeds shelf [] unfocused_if_needed bgoals_focused + pr_subgoals ~pr_first:true None bsigma ~seeds ~shelf ~stack:[] ~unfocused:unfocused_if_needed ~goals:bgoals_focused end let pr_nth_open_subgoal ~proof n = diff --git a/printing/printer.mli b/printing/printer.mli index e32cb0921e..41843680bc 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -183,8 +183,7 @@ val pr_goal : goal sigma -> Pp.t focused goals unless the conrresponding option [enable_unfocused_goal_printing] is set. [seeds] is for printing dependent evars (mainly for emacs proof tree mode). *) -val pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> Evar.t list -> Goal.goal list -> int list - -> goal list -> goal list -> Pp.t +val pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> seeds:goal list -> shelf:goal list -> stack:int list -> unfocused:goal list -> goals:goal list -> Pp.t val pr_subgoal : int -> evar_map -> goal list -> Pp.t val pr_concl : int -> evar_map -> goal -> Pp.t @@ -192,7 +191,7 @@ val pr_concl : int -> evar_map -> goal -> Pp.t val pr_open_subgoals : proof:Proof.t -> Pp.t val pr_nth_open_subgoal : proof:Proof.t -> int -> Pp.t val pr_evar : evar_map -> (Evar.t * evar_info) -> Pp.t -val pr_evars_int : evar_map -> int -> evar_info Evar.Map.t -> Pp.t +val pr_evars_int : evar_map -> shelf:goal list -> givenup:goal list -> int -> evar_info Evar.Map.t -> Pp.t val pr_evars : evar_map -> evar_info Evar.Map.t -> Pp.t val pr_ne_evar_set : Pp.t -> Pp.t -> evar_map -> Evar.Set.t -> Pp.t @@ -225,7 +224,8 @@ val pr_assumptionset : env -> evar_map -> types ContextObjectMap.t -> Pp.t val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t type printer_pr = { - pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> Evar.t list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t; + pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> seeds:goal list -> shelf:goal list -> stack:int list -> unfocused:goal list -> goals:goal list -> Pp.t; + pr_subgoal : int -> evar_map -> goal list -> Pp.t; pr_goal : goal sigma -> Pp.t; } diff --git a/printing/printmod.ml b/printing/printmod.ml index 43796ec618..e076c10f3b 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -141,7 +141,7 @@ let print_mutual_inductive env mind mib udecl = else [] in let bl = Universes.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in - let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in + let sigma = Evd.from_ctx (UState.of_binders bl) in hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++ Printer.pr_cumulative (Declareops.inductive_is_polymorphic mib) @@ -185,7 +185,7 @@ let print_record env mind mib udecl = let envpar = push_rel_context params env in let bl = Universes.universe_binders_with_opt_names (IndRef (mind,0)) (Array.to_list (Univ.Instance.to_array u)) udecl in - let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in + let sigma = Evd.from_ctx (UState.of_binders bl) in let keyword = let open Declarations in match mib.mind_finite with diff --git a/proofs/goal.ml b/proofs/goal.ml index ed0d76f93a..ba7e458f3a 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -62,8 +62,7 @@ module V82 = struct goals are restored to their initial value after the evar is created. *) let concl = EConstr.Unsafe.to_constr concl in - let prev_future_goals = Evd.future_goals evars in - let prev_principal_goal = Evd.principal_future_goal evars in + let prev_future_goals = Evd.save_future_goals evars in let evi = { Evd.evar_hyps = hyps; Evd.evar_concl = concl; Evd.evar_filter = Evd.Filter.identity; @@ -74,7 +73,7 @@ module V82 = struct in let evi = Typeclasses.mark_unresolvable evi in let (evars, evk) = Evarutil.new_pure_evar_full evars evi in - let evars = Evd.restore_future_goals evars prev_future_goals prev_principal_goal in + let evars = Evd.restore_future_goals evars prev_future_goals in let ctxt = Environ.named_context_of_val hyps in let inst = Array.map_of_list (NamedDecl.get_id %> EConstr.mkVar) ctxt in let ev = EConstr.mkEvar (evk,inst) in diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 03babfede2..8725f51cd7 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -170,6 +170,8 @@ let refine_by_tactic env sigma ty tac = ones created during the tactic invocation easily. *) let eff = Evd.eval_side_effects sigma in let sigma = Evd.drop_side_effects sigma in + (** Save the existing goals *) + let prev_future_goals = save_future_goals sigma in (** Start a proof *) let prf = Proof.start sigma [env, ty] in let (prf, _) = @@ -180,7 +182,8 @@ let refine_by_tactic env sigma ty tac = iraise (e, info) in (** Plug back the retrieved sigma *) - let sigma = Proof.in_proof prf (fun sigma -> sigma) in + let (goals,stack,shelf,given_up,sigma) = Proof.proof prf in + assert (stack = []); let ans = match Proof.initial_goals prf with | [c, _] -> c | _ -> assert false @@ -192,6 +195,17 @@ let refine_by_tactic env sigma ty tac = (** Reset the old side-effects *) let sigma = Evd.drop_side_effects sigma in let sigma = Evd.emit_side_effects eff sigma in + (** Restore former goals *) + let sigma = restore_future_goals sigma prev_future_goals in + (** Push remaining goals as future_goals which is the only way we + have to inform the caller that there are goals to collect while + not being encapsulated in the monad *) + (** Goals produced by tactic "shelve" *) + let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToShelve) shelf sigma in + (** Goals produced by tactic "give_up" *) + let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToGiveUp) given_up sigma in + (** Other goals *) + let sigma = List.fold_right Evd.declare_future_goal goals sigma in (** Get rid of the fresh side-effects by internalizing them in the term itself. Note that this is unsound, because the tactic may have solved other goals that were already present during its invocation, so that diff --git a/proofs/proof.ml b/proofs/proof.ml index 24f570f01e..51e0a1d614 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -347,7 +347,11 @@ let run_tactic env tac pr = Proofview.tclEVARMAP >>= fun sigma -> (* Already solved goals are not to be counted as shelved. Nor are they to be marked as unresolvable. *) - let retrieved = undef sigma (List.rev (Evd.future_goals sigma)) in + let retrieved = Evd.filter_future_goals (Evd.is_undefined sigma) (Evd.save_future_goals sigma) in + let retrieved,retrieved_given_up = Evd.extract_given_up_future_goals retrieved in + (* Check that retrieved given up is empty *) + if not (List.is_empty retrieved_given_up) then + CErrors.anomaly Pp.(str "Evars generated outside of proof engine (e.g. V82, clear, ...) are not supposed to be explicitly given up."); let sigma = List.fold_left Proofview.Unsafe.mark_as_goal sigma retrieved in Proofview.Unsafe.tclEVARS sigma >>= fun () -> Proofview.tclUNIT retrieved diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index d713b0999a..15f34ccc6b 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -169,6 +169,7 @@ let with_current_proof f = let p = { p with proof = newpr } in pstates := p :: rest; ret + let simple_with_current_proof f = with_current_proof (fun t p -> f t p , ()) let compact_the_proof () = simple_with_current_proof (fun _ -> Proof.compact) @@ -341,7 +342,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let subst_evar k = Proof.in_proof proof (fun m -> Evd.existential_opt_value m k) in let nf = Universes.nf_evars_and_universes_opt_subst subst_evar - (Evd.evar_universe_context_subst universes) in + (UState.subst universes) in let make_body = if poly || now then let make_body t (c, eff) = @@ -436,7 +437,7 @@ let return_proof ?(allow_partial=false) () = | Proof.HasUnresolvedEvar-> error(strbrk"Attempt to save a proof with existential variables still non-instantiated") in let eff = Evd.eval_side_effects evd in - let evd = Evd.nf_constraints evd in + let evd = Evd.minimize_universes evd in (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate side-effects... This may explain why one need to uniquize side-effects thereafter... *) diff --git a/proofs/refine.ml b/proofs/refine.ml index 50fd1c4722..909556b1ee 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -78,22 +78,20 @@ let generic_refine ~typecheck f gl = let state = Proofview.Goal.state gl in (** Save the [future_goals] state to restore them after the refinement. *) - let prev_future_goals = Evd.future_goals sigma in - let prev_principal_goal = Evd.principal_future_goal sigma in + let prev_future_goals = Evd.save_future_goals sigma in (** Create the refinement term *) Proofview.Unsafe.tclEVARS (Evd.reset_future_goals sigma) >>= fun () -> f >>= fun (v, c) -> Proofview.tclEVARMAP >>= fun sigma -> Proofview.V82.wrap_exceptions begin fun () -> - let evs = Evd.future_goals sigma in - let evkmain = Evd.principal_future_goal sigma in + let evs = Evd.save_future_goals sigma in (** Redo the effects in sigma in the monad's env *) let privates_csts = Evd.eval_side_effects sigma in let sideff = Safe_typing.side_effects_of_private_constants privates_csts in let env = add_side_effects env sideff in (** Check that the introduced evars are well-typed *) let fold accu ev = typecheck_evar ev env accu in - let sigma = if typecheck then CList.fold_left fold sigma evs else sigma in + let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in (** Check that the refined term is typesafe *) let sigma = if typecheck then typecheck_proof c concl env sigma else sigma in (** Check that the goal itself does not appear in the refined term *) @@ -102,6 +100,11 @@ let generic_refine ~typecheck f gl = if not (Evarutil.occur_evar_upto sigma self c) then () else Pretype_errors.error_occur_check env sigma self c in + (** Restore the [future goals] state. *) + let sigma = Evd.restore_future_goals sigma prev_future_goals in + (** Select the goals *) + let evs = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) evs in + let comb,shelf,given_up,evkmain = Evd.dispatch_future_goals evs in (** Proceed to the refinement *) let c = EConstr.Unsafe.to_constr c in let sigma = match Proofview.Unsafe.advance sigma self with @@ -118,10 +121,7 @@ let generic_refine ~typecheck f gl = | None -> sigma | Some id -> Evd.rename evk id sigma in - (** Restore the [future goals] state. *) - let sigma = Evd.restore_future_goals sigma prev_future_goals prev_principal_goal in - (** Select the goals *) - let comb = CList.map_filter (Proofview.Unsafe.advance sigma) (CList.rev evs) in + (** Mark goals *) let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in let trace () = Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)) in @@ -129,6 +129,8 @@ let generic_refine ~typecheck f gl = Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*> Proofview.Unsafe.tclEVARS sigma <*> Proofview.Unsafe.tclSETGOALS comb <*> + Proofview.Unsafe.tclPUTSHELF shelf <*> + Proofview.Unsafe.tclPUTGIVENUP given_up <*> Proofview.tclUNIT v end diff --git a/stm/stm.ml b/stm/stm.ml index d878bbb304..b3da97c6e0 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2482,7 +2482,7 @@ let known_state ?(redefine_qed=false) ~cache id = match keep with | VtDrop -> None | VtKeepAsAxiom -> - let ctx = Evd.empty_evar_universe_context in + let ctx = UState.empty in let fp = Future.from_val ([],ctx) in qed.fproof <- Some (fp, ref false); None | VtKeep -> diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 9f66248897..0260460e64 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -966,14 +966,15 @@ module Search = struct top_sort evm' goals else List.map (fun (ev, _) -> ev) (Evar.Map.bindings goals) in - let fgoals = Evd.future_goals evm in - let pgoal = Evd.principal_future_goal evm in + let fgoals = Evd.save_future_goals evm in let _, pv = Proofview.init evm' [] in let pv = Proofview.unshelve goals pv in try let (), pv', (unsafe, shelved, gaveup), _ = Proofview.apply env tac pv in + if not (List.is_empty gaveup) then + CErrors.anomaly (Pp.str "run_on_evars not assumed to apply tactics generating given up goals."); if Proofview.finished pv' then let evm' = Proofview.return pv' in assert(Evd.fold_undefined (fun ev _ acc -> @@ -983,7 +984,8 @@ module Search = struct (str "leaking evar " ++ int (Evar.repr ev) ++ spc () ++ pr_ev evm' ev); acc && okev) evm' true); - let evm' = Evd.restore_future_goals evm' (shelved @ fgoals) pgoal in + let fgoals = Evd.shelve_on_future_goals shelved fgoals in + let evm' = Evd.restore_future_goals evm' fgoals in let evm' = evars_reset_evd ~with_conv_pbs:true ~with_univs:false evm' evm in Some evm' else raise Not_found diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 45926551b4..477de6452e 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -214,7 +214,7 @@ let build_sym_scheme env ind = rel_vect (2*nrealargs+2) nrealargs])), mkRel 1 (* varH *), [|cstr (nrealargs+1)|])))) - in c, Evd.evar_universe_context_of ctx + in c, UState.of_context_set ctx let sym_scheme_kind = declare_individual_scheme_object "_sym_internal" @@ -285,7 +285,7 @@ let build_sym_involutive_scheme env ind = mkRel 1|])), mkRel 1 (* varH *), [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|])))) - in (c, Evd.evar_universe_context_of ctx), eff + in (c, UState.of_context_set ctx), eff let sym_involutive_scheme_kind = declare_individual_scheme_object "_sym_involutive" @@ -439,7 +439,7 @@ let build_l2r_rew_scheme dep env ind kind = [|main_body|]) else main_body)))))) - in (c, Evd.evar_universe_context_of ctx), + in (c, UState.of_context_set ctx), Safe_typing.concat_private eff' eff (**********************************************************************) @@ -528,7 +528,7 @@ let build_l2r_forward_rew_scheme dep env ind kind = (if dep then realsign_ind_P 1 applied_ind_P' else realsign_P 2) s) (mkNamedLambda varHC applied_PC' (mkVar varHC))|]))))) - in c, Evd.evar_universe_context_of ctx + in c, UState.of_context_set ctx (**********************************************************************) (* Build the right-to-left rewriting lemma for hypotheses associated *) @@ -601,7 +601,7 @@ let build_r2l_forward_rew_scheme dep env ind kind = lift (nrealargs+3) applied_PC, mkRel 1)|]), [|mkVar varHC|])))))) - in c, Evd.evar_universe_context_of ctx + in c, UState.of_context_set ctx (**********************************************************************) (* This function "repairs" the non-dependent r2l forward rewriting *) @@ -808,7 +808,7 @@ let build_congr env (eq,refl,ctx) ind = [|mkApp (refl, [|mkVar varB; mkApp (mkVar varf, [|lift (mip.mind_nrealargs+3) b|])|])|])))))) - in c, Evd.evar_universe_context_of ctx + in c, UState.of_context_set ctx let congr_scheme_kind = declare_individual_scheme_object "_congr" (fun _ ind -> diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index b960a845ce..62ead57f38 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -122,8 +122,8 @@ let compute_name internal id = let define internal id c p univs = let fd = declare_constant ~internal in let id = compute_name internal id in - let ctx = Evd.normalize_evar_universe_context univs in - let c = Universes.subst_opt_univs_constr (Evd.evar_universe_context_subst ctx) c in + let ctx = UState.minimize univs in + let c = Universes.subst_opt_univs_constr (UState.subst ctx) c in let univs = if p then Polymorphic_const_entry (UState.context ctx) else Monomorphic_const_entry (UState.context_set ctx) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 655283c204..a4cdc1592a 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -218,7 +218,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = end in let avoid = ref Id.Set.empty in let _,_,_,_,sigma = Proof.proof pf in - let sigma = Evd.nf_constraints sigma in + let sigma = Evd.minimize_universes sigma in let rec fill_holes c = match EConstr.kind sigma c with | Evar (e,args) -> diff --git a/test-suite/bugs/closed/6313.v b/test-suite/bugs/closed/6313.v new file mode 100644 index 0000000000..4d263c5a82 --- /dev/null +++ b/test-suite/bugs/closed/6313.v @@ -0,0 +1,64 @@ +(* Former open goals in nested proofs were lost *) + +(* This used to fail with "Incorrect number of goals (expected 1 tactic)." *) + +Inductive foo := a | b | c. +Goal foo -> foo. + intro x. + simple refine (match x with + | a => _ + | b => ltac:(exact b) + | c => _ + end); [exact a|exact c]. +Abort. + +(* This used to leave the goal on the shelf and fails at reflexivity *) + +Goal (True/\0=0 -> True) -> True. + intro f. + refine + (f ltac:(split; only 1:exact I)). + reflexivity. +Qed. + +(* The "Unshelve" used to not see the explicitly "shelved" goal *) + +Lemma f (b:comparison) : b=b. +refine (match b with + Eq => ltac:(shelve) + | Lt => ltac:(give_up) + | Gt => _ + end). +exact (eq_refl Gt). +Unshelve. +exact (eq_refl Eq). +Fail auto. (* Check that there are no more regular subgoals *) +Admitted. + +(* The "Unshelve" used to not see the explicitly "shelved" goal *) + +Lemma f2 (b:comparison) : b=b. +refine (match b with + Eq => ltac:(shelve) + | Lt => ltac:(give_up) + | Gt => _ + end). +Unshelve. (* Note: Unshelve puts goals at the end *) +exact (eq_refl Gt). +exact (eq_refl Eq). +Fail auto. (* Check that there are no more regular subgoals *) +Admitted. + +(* The "unshelve" used to not see the explicitly "shelved" goal *) + +Lemma f3 (b:comparison) : b=b. +unshelve refine (match b with + Eq => ltac:(shelve) + | Lt => ltac:(give_up) + | Gt => _ + end). +(* Note: unshelve puts goals at the beginning *) +exact (eq_refl Eq). +exact (eq_refl Gt). +Fail auto. (* Check that there are no more regular subgoals *) +Admitted. diff --git a/test-suite/failure/fixpointeta.v b/test-suite/failure/fixpointeta.v new file mode 100644 index 0000000000..9af719322f --- /dev/null +++ b/test-suite/failure/fixpointeta.v @@ -0,0 +1,70 @@ + +Set Primitive Projections. + +Record R := C { p : nat }. +(* R is defined +p is defined *) + +Unset Primitive Projections. +Record R' := C' { p' : nat }. + + + +Fail Definition f := fix f (x : R) : nat := p x. +(** Not allowed to make fixpoint defs on (non-recursive) records + having eta *) + +Fail Definition f := fix f (x : R') : nat := p' x. +(** Even without eta (R' is not primitive here), as long as they're + found to be BiFinite (non-recursive), we disallow it *) + +(* + +(* Subject reduction failure example, if we allowed fixpoints *) + +Set Primitive Projections. + +Record R := C { p : nat }. + +Definition f := fix f (x : R) : nat := p x. + +(* eta rule for R *) +Definition Rtr (P : R -> Type) x (v : P (C (p x))) : P x + := v. + +Definition goal := forall x, f x = p x. + +(* when we compute the Rtr away typechecking will fail *) +Definition thing : goal := fun x => +(Rtr (fun x => f x = p x) x (eq_refl _)). + +Definition thing' := Eval compute in thing. + +Fail Check (thing = thing'). +(* +The command has indeed failed with message: +The term "thing'" has type "forall x : R, (let (p) := x in p) = (let (p) := x in p)" +while it is expected to have type "goal" (cannot unify "(let (p) := x in p) = (let (p) := x in p)" +and "f x = p x"). +*) + +Definition thing_refl := eq_refl thing. + +Fail Definition thing_refl' := Eval compute in thing_refl. +(* +The command has indeed failed with message: +Illegal application: +The term "@eq_refl" of type "forall (A : Type) (x : A), x = x" +cannot be applied to the terms + "forall x : R, (fix f (x0 : R) : nat := let (p) := x0 in p) x = (let (p) := x in p)" : "Prop" + "fun x : R => eq_refl" : "forall x : R, (let (p) := x in p) = (let (p) := x in p)" +The 2nd term has type "forall x : R, (let (p) := x in p) = (let (p) := x in p)" +which should be coercible to + "forall x : R, (fix f (x0 : R) : nat := let (p) := x0 in p) x = (let (p) := x in p)". + *) + +Definition more_refls : thing_refl = thing_refl. +Proof. + compute. reflexivity. +Fail Defined. Abort. + *) diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v index abf8be72ef..d163dfbcd2 100644 --- a/test-suite/micromega/square.v +++ b/test-suite/micromega/square.v @@ -40,7 +40,7 @@ Proof. Qed. -Lemma QdenZpower : forall x : Q, ' Qden (x ^ 2)%Q = ('(Qden x) ^ 2) %Z. +Lemma QdenZpower : forall x : Q, Zpos (Qden (x ^ 2)%Q) = (Zpos (Qden x) ^ 2) %Z. Proof. intros. destruct x. @@ -54,9 +54,9 @@ Qed. Theorem sqrt2_not_rational : ~exists x:Q, x^2==2#1. Proof. unfold Qeq; intros (x,HQeq); simpl (Qden (2#1)) in HQeq; rewrite Z.mul_1_r in HQeq. - assert (Heq : (Qnum x ^ 2 = 2 * ' Qden x ^ 2%Q)%Z) by + assert (Heq : (Qnum x ^ 2 = 2 * Zpos (Qden x) ^ 2%Q)%Z) by (rewrite QnumZpower in HQeq ; rewrite QdenZpower in HQeq ; auto). assert (Hnx : (Qnum x <> 0)%Z) by (intros Hx; simpl in HQeq; rewrite Hx in HQeq; discriminate HQeq). - apply integer_statement; exists (Qnum x); exists (' Qden x); auto. + apply integer_statement; exists (Qnum x); exists (Zpos (Qden x)); auto. Qed. diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 4df21ae353..e73312c679 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -11,7 +11,7 @@ notation scopes add ': clear scopes' [arguments-assert,vernacular] eq_refl : ?y = ?y where -?y : [ |- nat] +?y : [ |- nat] Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x For eq_refl: Arguments are renamed to B, y diff --git a/test-suite/output/Existentials.out b/test-suite/output/Existentials.out index 9680d2bbff..18f5d89f66 100644 --- a/test-suite/output/Existentials.out +++ b/test-suite/output/Existentials.out @@ -1,4 +1,4 @@ -Existential 1 = ?Goal : [p : nat q := S p : nat n : nat m : nat |- ?y = m] +Existential 1 = ?Goal : [p : nat q := S p : nat n : nat m : nat |- ?y = m] Existential 2 = -?y : [p : nat q := S p : nat n : nat m : nat |- nat] (p, q cannot be used) -Existential 3 = ?Goal0 : [q : nat n : nat m : nat |- n = ?y] +?y : [p : nat q := S p : nat n : nat m : nat |- nat] (p, q cannot be used) (shelved) +Existential 3 = ?Goal0 : [q : nat n : nat m : nat |- n = ?y] diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index e6a6e0288a..864b6151a1 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -33,24 +33,24 @@ fun f : forall x : nat * (bool * unit), ?T => CURRY (x : nat) (y : bool), f : (forall x : nat * (bool * unit), ?T) -> forall (x : nat) (y : bool), ?T@{x:=(x, (y, tt))} where -?T : [x : nat * (bool * unit) |- Type] +?T : [x : nat * (bool * unit) |- Type] fun f : forall x : bool * (nat * unit), ?T => CURRYINV (x : nat) (y : bool), f : (forall x : bool * (nat * unit), ?T) -> forall (x : nat) (y : bool), ?T@{x:=(y, (x, tt))} where -?T : [x : bool * (nat * unit) |- Type] +?T : [x : bool * (nat * unit) |- Type] fun f : forall x : unit * nat * bool, ?T => CURRYLEFT (x : nat) (y : bool), f : (forall x : unit * nat * bool, ?T) -> forall (x : nat) (y : bool), ?T@{x:=(tt, x, y)} where -?T : [x : unit * nat * bool |- Type] +?T : [x : unit * nat * bool |- Type] fun f : forall x : unit * bool * nat, ?T => CURRYINVLEFT (x : nat) (y : bool), f : (forall x : unit * bool * nat, ?T) -> forall (x : nat) (y : bool), ?T@{x:=(tt, y, x)} where -?T : [x : unit * bool * nat |- Type] +?T : [x : unit * bool * nat |- Type] forall n : nat, {#n | 1 > n} : Prop forall x : nat, {|x | x > 0|} diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 668b4e5788..6f41b2fcf9 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -149,24 +149,24 @@ inmod@{u} -> Type@{v} (* u v |= *) Applied.infunct is universe polymorphic -axfoo@{i Top.41 Top.42} : Type@{Top.41} -> Type@{i} -(* i Top.41 Top.42 |= *) +axfoo@{i Top.44 Top.45} : Type@{Top.44} -> Type@{i} +(* i Top.44 Top.45 |= *) axfoo is universe polymorphic Argument scope is [type_scope] Expands to: Constant Top.axfoo -axbar@{i Top.41 Top.42} : Type@{Top.42} -> Type@{i} -(* i Top.41 Top.42 |= *) +axbar@{i Top.44 Top.45} : Type@{Top.45} -> Type@{i} +(* i Top.44 Top.45 |= *) axbar is universe polymorphic Argument scope is [type_scope] Expands to: Constant Top.axbar -axfoo' : Type@{Top.44} -> Type@{axbar'.i} +axfoo' : Type@{Top.47} -> Type@{axbar'.i} axfoo' is not universe polymorphic Argument scope is [type_scope] Expands to: Constant Top.axfoo' -axbar' : Type@{Top.44} -> Type@{axbar'.i} +axbar' : Type@{Top.47} -> Type@{axbar'.i} axbar' is not universe polymorphic Argument scope is [type_scope] diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index 266d94ad99..c6efc240a6 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -44,6 +44,9 @@ Module mono. Monomorphic Definition monomono := Type@{MONOU}. Check monomono. + + Monomorphic Inductive monoind@{i} : Type@{i} := . + Monomorphic Record monorecord@{i} : Type@{i} := mkmonorecord {}. End mono. Check mono.monomono. (* qualified MONOU *) Import mono. diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out index 2dbe215bfd..f7ffd1959a 100644 --- a/test-suite/output/inference.out +++ b/test-suite/output/inference.out @@ -7,10 +7,10 @@ fun e : option L => match e with fun n : nat => let y : T n := A n in ?t ?x : T n : forall n : nat, T n where -?t : [n : nat y := A n : T n |- ?T -> T n] -?x : [n : nat y := A n : T n |- ?T] +?t : [n : nat y := A n : T n |- ?T -> T n] +?x : [n : nat y := A n : T n |- ?T] fun n : nat => ?t ?x : T n : forall n : nat, T n where -?t : [n : nat |- ?T -> T n] -?x : [n : nat |- ?T] +?t : [n : nat |- ?T -> T n] +?x : [n : nat |- ?T] diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index 6962e43e7e..8d08f5975e 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -172,3 +172,14 @@ Hint Cut [_* (a_is_b | b_is_c | c_is_d | d_is_e) Timeout 1 Fail apply _. (* 0.06s *) Abort. End HintCut. + + +(* Check that auto-like tactics do not prefer "eq_refl" over more complex solutions, *) +(* e.g. those tactics when considering a goal with existential varibles *) +(* like "m = ?n" won't pick "plus_n_O" hint over "eq_refl" hint. *) +(* See this Coq club post for more detail: *) +(* https://sympa.inria.fr/sympa/arc/coq-club/2017-12/msg00103.html *) + +Goal forall (m : nat), exists n, m = n /\ m = n. + intros m; eexists; split; [trivial | reflexivity]. +Qed. diff --git a/test-suite/success/ShowExtraction.v b/test-suite/success/ShowExtraction.v new file mode 100644 index 0000000000..e34c240c5d --- /dev/null +++ b/test-suite/success/ShowExtraction.v @@ -0,0 +1,31 @@ + +Require Extraction. +Require Import List. + +Section Test. +Variable A : Type. +Variable decA : forall (x y:A), {x=y}+{x<>y}. + +(** Should fail when no proofs are started *) +Fail Show Extraction. + +Lemma decListA : forall (xs ys : list A), {xs=ys}+{xs<>ys}. +Proof. +Show Extraction. +fix 1. +destruct xs as [|x xs], ys as [|y ys]. +Show Extraction. +- now left. +- now right. +- now right. +- Show Extraction. + destruct (decA x y). + + destruct (decListA xs ys). + * left; now f_equal. + * Show Extraction. + right. congruence. + + right. congruence. +Show Extraction. +Defined. + +End Test. diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v index e05762477d..4dda360423 100644 --- a/test-suite/success/cumulativity.v +++ b/test-suite/success/cumulativity.v @@ -134,3 +134,24 @@ Definition withparams_co@{i i' j|i < i', i' < j} : withparams@{i j} -> withparam Fail Definition withparams_not_irr@{i i' j|i' < i, i' < j} : withparams@{i j} -> withparams@{i' j} := fun x => x. + +(** Cumulative constructors *) + + +Record twotys@{u v w} : Type@{w} := + twoconstr { fstty : Type@{u}; sndty : Type@{v} }. + +Monomorphic Universes i j k l. + +Monomorphic Constraint i < j. +Monomorphic Constraint j < k. +Monomorphic Constraint k < l. + +Parameter Tyi : Type@{i}. + +Definition checkcumul := + eq_refl _ : @eq twotys@{k k l} (twoconstr@{i j k} Tyi Tyi) (twoconstr@{j i k} Tyi Tyi). + +(* They can only be compared at the highest type *) +Fail Definition checkcumul' := + eq_refl _ : @eq twotys@{i k l} (twoconstr@{i j k} Tyi Tyi) (twoconstr@{j i k} Tyi Tyi). diff --git a/theories/Compat/Coq87.v b/theories/Compat/Coq87.v index 89556ee75f..dc1397aff2 100644 --- a/theories/Compat/Coq87.v +++ b/theories/Compat/Coq87.v @@ -9,6 +9,7 @@ (************************************************************************) (** Compatibility file for making Coq act similar to Coq v8.7 *) +Require Export Coq.Compat.Coq88. (* In 8.7, omega wasn't taking advantage of local abbreviations, see bug 148 and PR#768. For adjusting this flag, we're forced to diff --git a/theories/Compat/Coq88.v b/theories/Compat/Coq88.v new file mode 100644 index 0000000000..4142af05d2 --- /dev/null +++ b/theories/Compat/Coq88.v @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Compatibility file for making Coq act similar to Coq v8.8 *) diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index 73c8c5ef42..d5322d0945 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -92,7 +92,9 @@ Lemma plus_n_O : forall n:nat, n = n + 0. Proof. induction n; simpl; auto. Qed. -Hint Resolve plus_n_O: core. + +Remove Hints eq_refl : core. +Hint Resolve plus_n_O eq_refl: core. (* We want eq_refl to have higher priority than plus_n_O *) Lemma plus_O_n : forall n:nat, 0 + n = n. Proof. diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 9e6c26b10c..8df533e743 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -255,6 +255,7 @@ Tactic Notation "dependent" "induction" ident(H) := writing a version of [inversion] / [dependent destruction] which does not lose information, i.e., does not turn a goal which is provable into one which requires axiom K / UIP. *) + Ltac simpl_proj_exist_in H := repeat match type of H with | context G[proj1_sig (exist _ ?x ?p)] @@ -310,8 +311,20 @@ Ltac inversion_sigma_step := Ltac inversion_sigma := repeat inversion_sigma_step. (** A version of [time] that works for constrs *) + Ltac time_constr tac := let eval_early := match goal with _ => restart_timer end in let ret := tac () in let eval_early := match goal with _ => finish_timing ( "Tactic evaluation" ) end in ret. + +(** Useful combinators *) + +Ltac assert_fails tac := + tryif tac then fail 0 tac "succeeds" else idtac. +Ltac assert_succeeds tac := + tryif (assert_fails tac) then fail 0 tac "fails" else idtac. +Tactic Notation "assert_succeeds" tactic3(tac) := + assert_succeeds tac. +Tactic Notation "assert_fails" tactic3(tac) := + assert_fails tac. diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 467f263be8..35706e7fa2 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -227,9 +227,7 @@ Infix "/" := Qdiv : Q_scope. (** A light notation for [Zpos] *) -Notation " ' x " := (Zpos x) (at level 20, no associativity) : Z_scope. - -Lemma Qmake_Qdiv a b : a#b==inject_Z a/inject_Z ('b). +Lemma Qmake_Qdiv a b : a#b==inject_Z a/inject_Z (Zpos b). Proof. unfold Qeq. simpl. ring. Qed. @@ -242,9 +240,9 @@ Proof. Open Scope Z_scope. intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0; simpl in *. simpl_mult; ring_simplify. - replace (p1 * 'r2 * 'q2) with (p1 * 'q2 * 'r2) by ring. + replace (p1 * Zpos r2 * Zpos q2) with (p1 * Zpos q2 * Zpos r2) by ring. rewrite H. - replace (r1 * 'p2 * 'q2 * 's2) with (r1 * 's2 * 'p2 * 'q2) by ring. + replace (r1 * Zpos p2 * Zpos q2 * Zpos s2) with (r1 * Zpos s2 * Zpos p2 * Zpos q2) by ring. rewrite H0. ring. Close Scope Z_scope. @@ -255,7 +253,7 @@ Proof. unfold Qeq, Qopp; simpl. Open Scope Z_scope. intros x y H; simpl. - replace (- Qnum x * ' Qden y) with (- (Qnum x * ' Qden y)) by ring. + replace (- Qnum x * Zpos (Qden y)) with (- (Qnum x * Zpos (Qden y))) by ring. rewrite H; ring. Close Scope Z_scope. Qed. @@ -272,9 +270,9 @@ Proof. Open Scope Z_scope. intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0; simpl in *. intros; simpl_mult; ring_simplify. - replace (q1 * s1 * 'p2) with (q1 * 'p2 * s1) by ring. + replace (q1 * s1 * Zpos p2) with (q1 * Zpos p2 * s1) by ring. rewrite <- H. - replace (p1 * r1 * 'q2 * 's2) with (r1 * 's2 * p1 * 'q2) by ring. + replace (p1 * r1 * Zpos q2 * Zpos s2) with (r1 * Zpos s2 * p1 * Zpos q2) by ring. rewrite H0. ring. Close Scope Z_scope. @@ -305,13 +303,13 @@ Proof. unfold Qeq, Qcompare. Open Scope Z_scope. intros (p1,p2) (q1,q2) H (r1,r2) (s1,s2) H'; simpl in *. - rewrite <- (Zcompare_mult_compat (q2*s2) (p1*'r2)). - rewrite <- (Zcompare_mult_compat (p2*r2) (q1*'s2)). - change ('(q2*s2)) with ('q2 * 's2). - change ('(p2*r2)) with ('p2 * 'r2). - replace ('q2 * 's2 * (p1*'r2)) with ((p1*'q2)*'r2*'s2) by ring. + rewrite <- (Zcompare_mult_compat (q2*s2) (p1*Zpos r2)). + rewrite <- (Zcompare_mult_compat (p2*r2) (q1*Zpos s2)). + change (Zpos (q2*s2)) with (Zpos q2 * Zpos s2). + change (Zpos (p2*r2)) with (Zpos p2 * Zpos r2). + replace (Zpos q2 * Zpos s2 * (p1*Zpos r2)) with ((p1*Zpos q2)*Zpos r2*Zpos s2) by ring. rewrite H. - replace ('q2 * 's2 * (r1*'p2)) with ((r1*'s2)*'q2*'p2) by ring. + replace (Zpos q2 * Zpos s2 * (r1*Zpos p2)) with ((r1*Zpos s2)*Zpos q2*Zpos p2) by ring. rewrite H'. f_equal; ring. Close Scope Z_scope. @@ -572,8 +570,8 @@ Lemma Qle_trans : forall x y z, x<=y -> y<=z -> x<=z. Proof. unfold Qle; intros (x1, x2) (y1, y2) (z1, z2); simpl; intros. Open Scope Z_scope. - apply Z.mul_le_mono_pos_r with ('y2); [easy|]. - apply Z.le_trans with (y1 * 'x2 * 'z2). + apply Z.mul_le_mono_pos_r with (Zpos y2); [easy|]. + apply Z.le_trans with (y1 * Zpos x2 * Zpos z2). - rewrite Z.mul_shuffle0. now apply Z.mul_le_mono_pos_r. - rewrite Z.mul_shuffle0, (Z.mul_shuffle0 z1). now apply Z.mul_le_mono_pos_r. @@ -620,8 +618,8 @@ Lemma Qle_lt_trans : forall x y z, x<=y -> y<z -> x<z. Proof. unfold Qle, Qlt; intros (x1, x2) (y1, y2) (z1, z2); simpl; intros. Open Scope Z_scope. - apply Z.mul_lt_mono_pos_r with ('y2); [easy|]. - apply Z.le_lt_trans with (y1 * 'x2 * 'z2). + apply Z.mul_lt_mono_pos_r with (Zpos y2); [easy|]. + apply Z.le_lt_trans with (y1 * Zpos x2 * Zpos z2). - rewrite Z.mul_shuffle0. now apply Z.mul_le_mono_pos_r. - rewrite Z.mul_shuffle0, (Z.mul_shuffle0 z1). now apply Z.mul_lt_mono_pos_r. @@ -632,8 +630,8 @@ Lemma Qlt_le_trans : forall x y z, x<y -> y<=z -> x<z. Proof. unfold Qle, Qlt; intros (x1, x2) (y1, y2) (z1, z2); simpl; intros. Open Scope Z_scope. - apply Z.mul_lt_mono_pos_r with ('y2); [easy|]. - apply Z.lt_le_trans with (y1 * 'x2 * 'z2). + apply Z.mul_lt_mono_pos_r with (Zpos y2); [easy|]. + apply Z.lt_le_trans with (y1 * Zpos x2 * Zpos z2). - rewrite Z.mul_shuffle0. now apply Z.mul_lt_mono_pos_r. - rewrite Z.mul_shuffle0, (Z.mul_shuffle0 z1). now apply Z.mul_le_mono_pos_r. @@ -723,9 +721,9 @@ Proof. match goal with |- ?a <= ?b => ring_simplify a b end. rewrite Z.add_comm. apply Z.add_le_mono. - match goal with |- ?a <= ?b => ring_simplify z1 t1 ('z2) ('t2) a b end. + match goal with |- ?a <= ?b => ring_simplify z1 t1 (Zpos z2) (Zpos t2) a b end. auto with zarith. - match goal with |- ?a <= ?b => ring_simplify x1 y1 ('x2) ('y2) a b end. + match goal with |- ?a <= ?b => ring_simplify x1 y1 (Zpos x2) (Zpos y2) a b end. auto with zarith. Close Scope Z_scope. Qed. @@ -740,9 +738,9 @@ Proof. match goal with |- ?a < ?b => ring_simplify a b end. rewrite Z.add_comm. apply Z.add_le_lt_mono. - match goal with |- ?a <= ?b => ring_simplify z1 t1 ('z2) ('t2) a b end. + match goal with |- ?a <= ?b => ring_simplify z1 t1 (Zpos z2) (Zpos t2) a b end. auto with zarith. - match goal with |- ?a < ?b => ring_simplify x1 y1 ('x2) ('y2) a b end. + match goal with |- ?a < ?b => ring_simplify x1 y1 (Zpos x2) (Zpos y2) a b end. do 2 (apply Z.mul_lt_mono_pos_r;try easy). Close Scope Z_scope. Qed. diff --git a/theories/QArith/Qabs.v b/theories/QArith/Qabs.v index 48be894179..31eb41bc93 100644 --- a/theories/QArith/Qabs.v +++ b/theories/QArith/Qabs.v @@ -28,8 +28,8 @@ intros [xn xd] [yn yd] H. simpl. unfold Qeq in *. simpl in *. -change (' yd)%Z with (Z.abs (' yd)). -change (' xd)%Z with (Z.abs (' xd)). +change (Zpos yd)%Z with (Z.abs (Zpos yd)). +change (Zpos xd)%Z with (Z.abs (Zpos xd)). repeat rewrite <- Z.abs_mul. congruence. Qed. @@ -88,8 +88,8 @@ unfold Qplus. unfold Qle. simpl. apply Z.mul_le_mono_nonneg_r;auto with *. -change (' yd)%Z with (Z.abs (' yd)). -change (' xd)%Z with (Z.abs (' xd)). +change (Zpos yd)%Z with (Z.abs (Zpos yd)). +change (Zpos xd)%Z with (Z.abs (Zpos xd)). repeat rewrite <- Z.abs_mul. apply Z.abs_triangle. Qed. diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index e25f69c316..1510a7b825 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -30,7 +30,7 @@ Lemma Qred_identity : Proof. intros (a,b) H; simpl in *. rewrite <- Z.ggcd_gcd in H. - generalize (Z.ggcd_correct_divisors a ('b)). + generalize (Z.ggcd_correct_divisors a (Zpos b)). destruct Z.ggcd as (g,(aa,bb)); simpl in *; subst. rewrite !Z.mul_1_l. now intros (<-,<-). Qed. @@ -39,7 +39,7 @@ Lemma Qred_identity2 : forall q:Q, Qred q = q -> Z.gcd (Qnum q) (QDen q) = 1%Z. Proof. intros (a,b) H; simpl in *. - generalize (Z.gcd_nonneg a ('b)) (Z.ggcd_correct_divisors a ('b)). + generalize (Z.gcd_nonneg a (Zpos b)) (Z.ggcd_correct_divisors a (Zpos b)). rewrite <- Z.ggcd_gcd. destruct Z.ggcd as (g,(aa,bb)); simpl in *. injection H as <- <-. intros H (_,H'). diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v index 3fd78f092a..0107822093 100644 --- a/theories/QArith/Qpower.v +++ b/theories/QArith/Qpower.v @@ -90,7 +90,7 @@ rewrite Qinv_power. reflexivity. Qed. -Lemma Qinv_power_n : forall n p, (1#p)^n == /(inject_Z ('p))^n. +Lemma Qinv_power_n : forall n p, (1#p)^n == /(inject_Z (Zpos p))^n. Proof. intros n p. rewrite Qmake_Qdiv. @@ -190,7 +190,7 @@ unfold Z.succ. rewrite Zpower_exp; auto with *; try discriminate. rewrite Qpower_plus' by discriminate. rewrite <- IHn by discriminate. -replace (a^'n*a^1)%Z with (a^'n*a)%Z by ring. +replace (a^Zpos n*a^1)%Z with (a^Zpos n*a)%Z by ring. ring_simplify. reflexivity. Qed. diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v index 14ab1700e7..c832962590 100644 --- a/theories/QArith/Qreals.v +++ b/theories/QArith/Qreals.v @@ -167,8 +167,8 @@ unfold Qinv, Q2R, Qeq; intros (x1, x2). case x1; unfold Qnum, Qden. simpl; intros; elim H; trivial. intros; field; auto. intros; - change (IZR (Zneg x2)) with (- IZR (' x2))%R; - change (IZR (Zneg p)) with (- IZR (' p))%R; + change (IZR (Zneg x2)) with (- IZR (Zpos x2))%R; + change (IZR (Zneg p)) with (- IZR (Zpos p))%R; simpl; field; (*auto 8 with real.*) repeat split; auto; auto with real. Qed. diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index 7b08515d21..17307c8279 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -21,14 +21,14 @@ Notation Z2P_correct := Z2Pos.id (only parsing). Definition Qred (q:Q) := let (q1,q2) := q in - let (r1,r2) := snd (Z.ggcd q1 ('q2)) + let (r1,r2) := snd (Z.ggcd q1 (Zpos q2)) in r1#(Z.to_pos r2). Lemma Qred_correct : forall q, (Qred q) == q. Proof. unfold Qred, Qeq; intros (n,d); simpl. - generalize (Z.ggcd_gcd n ('d)) (Z.gcd_nonneg n ('d)) - (Z.ggcd_correct_divisors n ('d)). + generalize (Z.ggcd_gcd n (Zpos d)) (Z.gcd_nonneg n (Zpos d)) + (Z.ggcd_correct_divisors n (Zpos d)). destruct (Z.ggcd n (Zpos d)) as (g,(nn,dd)); simpl. Open Scope Z_scope. intros Hg LE (Hn,Hd). rewrite Hd, Hn. @@ -45,13 +45,13 @@ Proof. unfold Qred, Qeq in *; simpl in *. Open Scope Z_scope. intros H. - generalize (Z.ggcd_gcd a ('b)) (Zgcd_is_gcd a ('b)) - (Z.gcd_nonneg a ('b)) (Z.ggcd_correct_divisors a ('b)). + generalize (Z.ggcd_gcd a (Zpos b)) (Zgcd_is_gcd a (Zpos b)) + (Z.gcd_nonneg a (Zpos b)) (Z.ggcd_correct_divisors a (Zpos b)). destruct (Z.ggcd a (Zpos b)) as (g,(aa,bb)). simpl. intros <- Hg1 Hg2 (Hg3,Hg4). assert (Hg0 : g <> 0) by (intro; now subst g). - generalize (Z.ggcd_gcd c ('d)) (Zgcd_is_gcd c ('d)) - (Z.gcd_nonneg c ('d)) (Z.ggcd_correct_divisors c ('d)). + generalize (Z.ggcd_gcd c (Zpos d)) (Zgcd_is_gcd c (Zpos d)) + (Z.gcd_nonneg c (Zpos d)) (Z.ggcd_correct_divisors c (Zpos d)). destruct (Z.ggcd c (Zpos d)) as (g',(cc,dd)). simpl. intros <- Hg'1 Hg'2 (Hg'3,Hg'4). assert (Hg'0 : g' <> 0) by (intro; now subst g'). diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v index e4e9749727..7c5ddbb6a9 100644 --- a/theories/QArith/Qround.v +++ b/theories/QArith/Qround.v @@ -80,11 +80,11 @@ unfold Qlt. simpl. replace (n*1)%Z with n by ring. ring_simplify. -replace (n / ' d * ' d + ' d)%Z with - (('d * (n / 'd) + n mod 'd) + 'd - n mod 'd)%Z by ring. +replace (n / Zpos d * Zpos d + Zpos d)%Z with + ((Zpos d * (n / Zpos d) + n mod Zpos d) + Zpos d - n mod Zpos d)%Z by ring. rewrite <- Z_div_mod_eq; auto with*. rewrite <- Z.lt_add_lt_sub_r. -destruct (Z_mod_lt n ('d)); auto with *. +destruct (Z_mod_lt n (Zpos d)); auto with *. Qed. Hint Resolve Qlt_floor : qarith. @@ -107,9 +107,9 @@ Proof. intros [xn xd] [yn yd] Hxy. unfold Qle in *. simpl in *. -rewrite <- (Zdiv_mult_cancel_r xn ('xd) ('yd)); auto with *. -rewrite <- (Zdiv_mult_cancel_r yn ('yd) ('xd)); auto with *. -rewrite (Z.mul_comm ('yd) ('xd)). +rewrite <- (Zdiv_mult_cancel_r xn (Zpos xd) (Zpos yd)); auto with *. +rewrite <- (Zdiv_mult_cancel_r yn (Zpos yd) (Zpos xd)); auto with *. +rewrite (Z.mul_comm (Zpos yd) (Zpos xd)). apply Z_div_le; auto with *. Qed. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 727fd3ec37..e9f64542c1 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -23,6 +23,7 @@ MLFILES := $(COQMF_MLFILES) ML4FILES := $(COQMF_ML4FILES) MLPACKFILES := $(COQMF_MLPACKFILES) MLLIBFILES := $(COQMF_MLLIBFILES) +CMDLINE_VFILES := $(COQMF_CMDLINE_VFILES) INSTALLCOQDOCROOT := $(COQMF_INSTALLCOQDOCROOT) OTHERFLAGS := $(COQMF_OTHERFLAGS) COQ_SRC_SUBDIRS := $(COQMF_COQ_SRC_SUBDIRS) @@ -30,6 +31,7 @@ OCAMLLIBS := $(COQMF_OCAMLLIBS) SRC_SUBDIRS := $(COQMF_SRC_SUBDIRS) COQLIBS := $(COQMF_COQLIBS) COQLIBS_NOML := $(COQMF_COQLIBS_NOML) +CMDLINE_COQLIBS := $(COQMF_CMDLINE_COQLIBS) LOCAL := $(COQMF_LOCAL) COQLIB := $(COQMF_COQLIB) DOCDIR := $(COQMF_DOCDIR) @@ -724,9 +726,14 @@ $(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack $(SHOW)'COQDEP $<' $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok) +# If this makefile is created using a _CoqProject we have coqdep get +# options from it. This avoids argument length limits for pathological +# projects. Note that extra options might be on the command line. +VDFILE_FLAGS:=$(if @PROJECT_FILE@,-f @PROJECT_FILE@,) $(CMDLINE_COQLIBS) $(CMDLINE_VFILES) + $(VDFILE).d: $(VFILES) $(SHOW)'COQDEP VFILES' - $(HIDE)$(COQDEP) $(COQLIBS) -dyndep var -c $(VFILES) $(redir_if_ok) + $(HIDE)$(COQDEP) -dyndep var $(VDFILE_FLAGS) $(redir_if_ok) # Misc ######################################################################## diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index ef4428755a..6cd520d607 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -13,6 +13,8 @@ open CoqProject_file open Printf +let (>) f g = fun x -> g (f x) + let output_channel = ref stdout let makefile_name = ref "Makefile" let make_name = ref "" @@ -175,21 +177,22 @@ let generate_conf_extra_target oc sps = in if sps <> [] then section oc "Extra targets. (-extra and -extra-phony, DEPRECATED)"; - List.iter pr_path sps + List.iter (forget_source > pr_path) sps let generate_conf_subdirs oc sds = if sds <> [] then section oc "Subdirectories. (DEPRECATED)"; - List.iter (fprintf oc ".PHONY:%s\n") sds; - List.iter (fprintf oc "post-all::\n\tcd \"%s\" && $(MAKE) all\n") sds; - List.iter (fprintf oc "clean::\n\tcd \"%s\" && $(MAKE) clean\n") sds; - List.iter (fprintf oc "archclean::\n\tcd \"%s\" && $(MAKE) archclean\n") sds; - List.iter (fprintf oc "install-extra::\n\tcd \"%s\" && $(MAKE) install\n") sds + let iter f = List.iter (forget_source > f) in + iter (fprintf oc ".PHONY:%s\n") sds; + iter (fprintf oc "post-all::\n\tcd \"%s\" && $(MAKE) all\n") sds; + iter (fprintf oc "clean::\n\tcd \"%s\" && $(MAKE) clean\n") sds; + iter (fprintf oc "archclean::\n\tcd \"%s\" && $(MAKE) archclean\n") sds; + iter (fprintf oc "install-extra::\n\tcd \"%s\" && $(MAKE) install\n") sds let generate_conf_includes oc { ml_includes; r_includes; q_includes } = section oc "Path directives (-I, -R, -Q)."; let module S = String in - let open List in + let map = map_sourced_list in let dash1 opt v = sprintf "-%s %s" opt (quote v) in let dash2 opt v1 v2 = sprintf "-%s %s %s" opt (quote v1) (quote v2) in fprintf oc "COQMF_OCAMLLIBS = %s\n" @@ -202,7 +205,11 @@ let generate_conf_includes oc { ml_includes; r_includes; q_includes } = (S.concat " " (map (fun ({ path },l) -> dash2 "R" path l) r_includes)); fprintf oc "COQMF_COQLIBS_NOML = %s %s\n" (S.concat " " (map (fun ({ path },l) -> dash2 "Q" path l) q_includes)) - (S.concat " " (map (fun ({ path },l) -> dash2 "R" path l) r_includes)) + (S.concat " " (map (fun ({ path },l) -> dash2 "R" path l) r_includes)); + fprintf oc "COQMF_CMDLINE_COQLIBS = %s %s %s\n" + (S.concat " " (map_cmdline (fun { path } -> dash1 "I" path) ml_includes)) + (S.concat " " (map_cmdline (fun ({ path },l) -> dash2 "Q" path l) q_includes)) + (S.concat " " (map_cmdline (fun ({ path },l) -> dash2 "R" path l) r_includes)); ;; let windrive s = @@ -219,10 +226,10 @@ let generate_conf_coq_config oc args = ;; let generate_conf_files oc - { v_files; mli_files; ml4_files; ml_files; mllib_files; mlpack_files } + { v_files; mli_files; ml4_files; ml_files; mllib_files; mlpack_files; } = let module S = String in - let open List in + let map = map_sourced_list in section oc "Project files."; fprintf oc "COQMF_VFILES = %s\n" (S.concat " " (map quote v_files)); fprintf oc "COQMF_MLIFILES = %s\n" (S.concat " " (map quote mli_files)); @@ -230,6 +237,8 @@ let generate_conf_files oc fprintf oc "COQMF_ML4FILES = %s\n" (S.concat " " (map quote ml4_files)); fprintf oc "COQMF_MLPACKFILES = %s\n" (S.concat " " (map quote mlpack_files)); fprintf oc "COQMF_MLLIBFILES = %s\n" (S.concat " " (map quote mllib_files)); + let cmdline_vfiles = filter_cmdline v_files in + fprintf oc "COQMF_CMDLINE_VFILES = %s\n" (S.concat " " (List.map quote cmdline_vfiles)); ;; let rec all_start_with prefix = function @@ -246,12 +255,12 @@ let rec logic_gcd acc = function else acc let generate_conf_doc oc { defs; q_includes; r_includes } = - let includes = List.map snd (q_includes @ r_includes) in + let includes = List.map (forget_source > snd) (q_includes @ r_includes) in let logpaths = List.map (CString.split '.') includes in let gcd = logic_gcd [] logpaths in let root = if gcd = [] then - if not (List.mem_assoc "INSTALLDEFAULTROOT" defs) then begin + if not (List.exists (fun x -> fst x.thing = "INSTALLDEFAULTROOT") defs) then begin let destination = "orphan_" ^ (String.concat "_" includes) in eprintf "Warning: no common logical root\n"; eprintf "Warning: in such case INSTALLDEFAULTROOT must be defined\n"; @@ -264,9 +273,9 @@ let generate_conf_doc oc { defs; q_includes; r_includes } = let generate_conf_defs oc { defs; extra_args } = section oc "Extra variables."; - List.iter (fun (k,v) -> Printf.fprintf oc "%s = %s\n" k v) defs; + List.iter (forget_source > (fun (k,v) -> Printf.fprintf oc "%s = %s\n" k v)) defs; Printf.fprintf oc "COQMF_OTHERFLAGS = %s\n" - (String.concat " " extra_args) + (String.concat " " (List.map forget_source extra_args)) let generate_conf oc project args = fprintf oc "# This configuration file was generated by running:\n"; @@ -284,10 +293,10 @@ let ensure_root_dir ({ ml_includes; r_includes; q_includes; v_files; ml_files; mli_files; ml4_files; mllib_files; mlpack_files } as project) -= - let open List in + = + let exists f = List.exists (forget_source > f) in let here = Sys.getcwd () in - let not_tops = List.for_all (fun s -> s <> Filename.basename s) in + let not_tops = List.for_all (fun s -> s.thing <> Filename.basename s.thing) in if exists (fun { canonical_path = x } -> x = here) ml_includes || exists (fun ({ canonical_path = x },_) -> is_prefix x here) r_includes || exists (fun ({ canonical_path = x },_) -> is_prefix x here) q_includes @@ -297,29 +306,27 @@ let ensure_root_dir then project else + let source x = {thing=x; source=CmdLine} in let here_path = { path = "."; canonical_path = here } in { project with - ml_includes = here_path :: ml_includes; - r_includes = (here_path, "Top") :: r_includes } + ml_includes = source here_path :: ml_includes; + r_includes = source (here_path, "Top") :: r_includes } ;; let warn_install_at_root_directory - { q_includes; r_includes; - v_files; ml_files; mli_files; ml4_files; - mllib_files; mlpack_files } + ({ q_includes; r_includes; } as project) = let open CList in let inc_top_p = map_filter - (fun ({ path } ,ldir) -> if ldir = "" then Some path else None) + (fun {thing=({ path } ,ldir)} -> if ldir = "" then Some path else None) (r_includes @ q_includes) in - let files = - v_files @ mli_files @ ml4_files @ ml_files @ mllib_files @ mlpack_files in - let bad = filter (fun f -> mem (Filename.dirname f) inc_top_p) files in + let files = all_files project in + let bad = filter (fun f -> mem (Filename.dirname f.thing) inc_top_p) files in if bad <> [] then begin eprintf "Warning: No file should be installed at the root of Coq's library.\n"; eprintf "Warning: No logical path (-R, -Q) applies to these files:\n"; - List.iter (fun x -> eprintf "Warning: %s\n" x) bad; + List.iter (fun x -> eprintf "Warning: %s\n" x.thing) bad; eprintf "\n"; end ;; @@ -328,10 +335,10 @@ let check_overlapping_include { q_includes; r_includes } = let pwd = Sys.getcwd () in let aux = function | [] -> () - | ({ path; canonical_path }, _) :: l -> + | {thing = { path; canonical_path }, _} :: l -> if not (is_prefix pwd canonical_path) then eprintf "Warning: %s (used in -R or -Q) is not a subdirectory of the current directory\n\n" path; - List.iter (fun ({ path = p; canonical_path = cp }, _) -> + List.iter (fun {thing={ path = p; canonical_path = cp }, _} -> if is_prefix canonical_path cp || is_prefix cp canonical_path then eprintf "Warning: %s and %s overlap (used in -R or -Q)\n\n" path p) l @@ -354,7 +361,7 @@ let destination_of { ml_includes; q_includes; r_includes; } file = clean_path (physical_dir_of_logical_dir logic ^ "/" ^ chop_prefix canonical_path file_dir ^ "/") in let candidates = - CList.map_filter (fun ({ canonical_path }, logic) -> + CList.map_filter (fun {thing={ canonical_path }, logic} -> if is_prefix canonical_path file_dir then Some(mk_destination logic canonical_path) else None) includes @@ -364,10 +371,10 @@ let destination_of { ml_includes; q_includes; r_includes; } file = (* BACKWARD COMPATIBILITY: -I into the only logical root *) begin match r_includes, - List.find (fun { canonical_path = p } -> is_prefix p file_dir) + List.find (fun {thing={ canonical_path = p }} -> is_prefix p file_dir) ml_includes with - | [{ canonical_path }, logic], { canonical_path = p } -> + | [{thing={ canonical_path }, logic}], {thing={ canonical_path = p }} -> let destination = clean_path (physical_dir_of_logical_dir logic ^ "/" ^ chop_prefix p file_dir ^ "/") in diff --git a/tools/coqdep.ml b/tools/coqdep.ml index f4f143b3b0..12b5cab0ac 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -446,6 +446,7 @@ let usage () = eprintf " -boot : For coq developers, prints dependencies over coq library files (omitted by default).\n"; eprintf " -sort : output the given file name ordered by dependencies\n"; eprintf " -noglob | -no-glob : \n"; + eprintf " -f file : read -I, -Q, -R and filenames from _CoqProject-formatted FILE."; eprintf " -I dir -as logname : add (non recursively) dir to coq load path under logical name logname\n"; eprintf " -I dir : add (non recursively) dir to ocaml path\n"; eprintf " -R dir -as logname : add and import dir recursively to coq load path under logical name logname\n"; (* deprecate? *) @@ -462,6 +463,19 @@ let usage () = let split_period = Str.split (Str.regexp (Str.quote ".")) +let add_q_include path l = add_rec_dir_no_import add_known path (split_period l) + +let add_r_include path l = add_rec_dir_import add_known path (split_period l) + +let treat_coqproject f = + let open CoqProject_file in + let iter_sourced f = List.iter (fun {thing} -> f thing) in + let project = read_project_file f in + iter_sourced (fun { path } -> add_caml_dir path) project.ml_includes; + iter_sourced (fun ({ path }, l) -> add_q_include path l) project.q_includes; + iter_sourced (fun ({ path }, l) -> add_r_include path l) project.r_includes; + iter_sourced (fun f -> treat_file None f) (all_files project) + let rec parse = function | "-c" :: ll -> option_c := true; parse ll | "-D" :: ll -> option_D := true; parse ll @@ -469,10 +483,11 @@ let rec parse = function | "-boot" :: ll -> option_boot := true; parse ll | "-sort" :: ll -> option_sort := true; parse ll | ("-noglob" | "-no-glob") :: ll -> option_noglob := true; parse ll + | "-f" :: f :: ll -> treat_coqproject f; parse ll | "-I" :: r :: ll -> add_caml_dir r; parse ll | "-I" :: [] -> usage () - | "-R" :: r :: ln :: ll -> add_rec_dir_import add_known r (split_period ln); parse ll - | "-Q" :: r :: ln :: ll -> add_rec_dir_no_import add_known r (split_period ln); parse ll + | "-R" :: r :: ln :: ll -> add_r_include r ln; parse ll + | "-Q" :: r :: ln :: ll -> add_q_include r ln; parse ll | "-R" :: ([] | [_]) -> usage () | "-dumpgraph" :: f :: ll -> option_dump := Some (false, f); parse ll | "-dumpgraphbox" :: f :: ll -> option_dump := Some (true, f); parse ll diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 341888d09c..cd831c05ca 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -344,13 +344,13 @@ let init_color color_mode = match colors with | None -> (** Default colors *) + Topfmt.default_styles (); Topfmt.init_terminal_output ~color:true | Some "" -> (** No color output *) Topfmt.init_terminal_output ~color:false | Some s -> (** Overwrite all colors *) - Topfmt.clear_styles (); Topfmt.parse_color_config s; Topfmt.init_terminal_output ~color:true end diff --git a/toplevel/coqtop_bin.ml b/toplevel/coqtop_bin.ml deleted file mode 100644 index 56aced92a8..0000000000 --- a/toplevel/coqtop_bin.ml +++ /dev/null @@ -1,2 +0,0 @@ -(* Main coqtop initialization *) -let () = Coqtop.start() diff --git a/toplevel/coqtop_byte_bin.ml b/toplevel/coqtop_byte_bin.ml index 7d8354ec3d..0b65cebbbc 100644 --- a/toplevel/coqtop_byte_bin.ml +++ b/toplevel/coqtop_byte_bin.ml @@ -1,3 +1,13 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + let drop_setup () = begin try (* Enable rectypes in the toplevel if it has the directive #rectypes *) @@ -18,4 +28,7 @@ let drop_setup () = ml_loop = (fun () -> Toploop.loop ppf); }) -let _ = drop_setup () +(* Main coqtop initialization *) +let _ = + drop_setup (); + Coqtop.start() diff --git a/toplevel/coqtop_opt_bin.ml b/toplevel/coqtop_opt_bin.ml index 410b4679ae..ea4c0ea520 100644 --- a/toplevel/coqtop_opt_bin.ml +++ b/toplevel/coqtop_opt_bin.ml @@ -1,3 +1,16 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + let drop_setup () = Mltop.remove () -let _ = drop_setup () +(* Main coqtop initialization *) +let _ = + drop_setup (); + Coqtop.start() diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 9b7b88b51a..2879feba78 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -323,7 +323,7 @@ let build_beq_scheme mode kn = raise NoDecidabilityCoInductive; let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in create_input fix), - Evd.make_evar_universe_context (Global.env ()) None), + UState.make (Global.universes ())), !eff let beq_scheme_kind = declare_mutual_scheme_object "_beq" build_beq_scheme @@ -671,7 +671,7 @@ let make_bl_scheme mode mind = let lnonparrec,lnamesparrec = (* TODO subst *) context_chop (nparams-nparrec) mib.mind_params_ctxt in let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in - let ctx = Evd.make_evar_universe_context (Global.env ()) None in + let ctx = UState.make (Global.universes ()) in let side_eff = side_effect_of_mode mode in let bl_goal = EConstr.of_constr bl_goal in let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx bl_goal @@ -795,7 +795,7 @@ let make_lb_scheme mode mind = let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in - let ctx = Evd.make_evar_universe_context (Global.env ()) None in + let ctx = UState.make (Global.universes ()) in let side_eff = side_effect_of_mode mode in let lb_goal = EConstr.of_constr lb_goal in let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx lb_goal @@ -965,7 +965,7 @@ let make_eq_decidability mode mind = let nparams = mib.mind_nparams in let nparrec = mib.mind_nparams_rec in let u = Univ.Instance.empty in - let ctx = Evd.make_evar_universe_context (Global.env ()) None in + let ctx = UState.make (Global.universes ()) in let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in let side_eff = side_effect_of_mode mode in diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 1712634daf..6a590758fd 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -160,7 +160,7 @@ let do_assumptions kind nl l = in let sigma = solve_remaining_evars all_and_fail_flags env sigma Evd.empty in (* The universe constraints come from the whole telescope. *) - let sigma = Evd.nf_constraints sigma in + let sigma = Evd.minimize_universes sigma in let nf_evar c = EConstr.to_constr sigma c in let uvars, l = List.fold_left_map (fun uvars (coe,t,imps) -> let t = nf_evar t in diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 01dbe0a0d0..b18a60a1f1 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -85,7 +85,7 @@ let interp_definition pl bl poly red_option c ctypopt = evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsty, Some ty in (* universe minimization *) - let evd = Evd.nf_constraints evd in + let evd = Evd.minimize_universes evd in (* Substitute evars and universes, and add parameters. Note: in program mode some evars may remain. *) let ctx = List.map (EConstr.to_rel_decl evd) ctx in diff --git a/vernac/himsg.ml b/vernac/himsg.ml index c839ed0c70..131b1fab66 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -425,7 +425,7 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj = str "Not enough abstractions in the definition" | RecursionNotOnInductiveType c -> str "Recursive definition on" ++ spc () ++ pr_lconstr_env env sigma c ++ - spc () ++ str "which should be an inductive type" + spc () ++ str "which should be a recursive inductive type" | RecursionOnIllegalTerm(j,(arg_env, arg),le,lt) -> let arg_env = make_all_name_different arg_env sigma in let called = diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 41c44b126d..27587416b1 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -381,7 +381,7 @@ let do_mutual_induction_scheme lnamedepindsort = | None -> let _, ctx = Global.type_of_global_in_context env0 (IndRef ind) in let u, ctx = Universes.fresh_instance_from ctx None in - let evd = Evd.from_ctx (Evd.evar_universe_context_of ctx) in + let evd = Evd.from_ctx (UState.of_context_set ctx) in evd, (ind,u), Some u | Some ui -> evd, (ind, ui), inst in diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 6447fc3502..4f16e1cf6e 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -472,7 +472,7 @@ let subst_body expand prg = let declare_definition prg = let body, typ = subst_body true prg in let nf = Universes.nf_evars_and_universes_opt_subst (fun x -> None) - (Evd.evar_universe_context_subst prg.prg_ctx) in + (UState.subst prg.prg_ctx) in let opaque = prg.prg_opaque in let fix_exn = Hook.get get_fix_exn () in let typ = nf typ in diff --git a/vernac/record.ml b/vernac/record.ml index e21f53f55e..6e745b2af7 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -594,13 +594,12 @@ let definition_structure (kind,cum,poly,finite,(is_coe,({CAst.loc;v=idstruc},pl) let pl, univs, arity, template, implpars, params, implfs, fields = States.with_state_protection (fun () -> typecheck_params_and_fields finite (kind = Class true) idstruc poly pl s ps notations fs) () in - let gr = match kind with + match kind with | Class def -> - let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in - let gr = declare_class finite def cum pl univs (loc,idstruc) idbuild - implpars params arity template implfs fields is_coe coers priorities in - gr - | _ -> + let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in + declare_class finite def cum pl univs (loc,idstruc) idbuild + implpars params arity template implfs fields is_coe coers priorities + | _ -> let implfs = List.map (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs @@ -618,7 +617,4 @@ let definition_structure (kind,cum,poly,finite,(is_coe,({CAst.loc;v=idstruc},pl) let ind = declare_structure finite pl univs idstruc idbuild implpars params arity template implfs fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) in - IndRef ind - in - Declare.declare_univ_binders gr pl; - gr + IndRef ind diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 4e4077f427..055f6676e8 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -187,8 +187,8 @@ let init_tag_map styles = let set accu (name, st) = CString.Map.add name st accu in tag_map := List.fold_left set !tag_map styles -let clear_styles () = - tag_map := CString.Map.empty +let default_styles () = + init_tag_map (default_tag_map ()) let parse_color_config file = let styles = Terminal.parse file in @@ -257,7 +257,6 @@ let make_printing_functions () = print_prefix, print_suffix let init_terminal_output ~color = - init_tag_map (default_tag_map ()); let push_tag, pop_tag, clear_tag = make_style_stack () in let print_prefix, print_suffix = make_printing_functions () in let tag_handler ft = { diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index 2fdefc6fc5..579b456a28 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -43,7 +43,7 @@ val std_logger : ?pre_hdr:Pp.t -> Feedback.level -> Pp.t -> unit val emacs_logger : ?pre_hdr:Pp.t -> Feedback.level -> Pp.t -> unit (** Color output *) -val clear_styles : unit -> unit +val default_styles : unit -> unit val parse_color_config : string -> unit val dump_tags : unit -> (string * Terminal.style) list diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 5779c07ab3..4c9b41b216 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -66,13 +66,13 @@ let show_proof () = let show_top_evars () = (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *) let pfts = Proof_global.give_me_the_proof () in - let gls,_,_,_,sigma = Proof.proof pfts in - pr_evars_int sigma 1 (Evd.undefined_map sigma) + let gls,_,shelf,givenup,sigma = Proof.proof pfts in + pr_evars_int sigma ~shelf ~givenup 1 (Evd.undefined_map sigma) let show_universes () = let pfts = Proof_global.give_me_the_proof () in let gls,_,_,_,sigma = Proof.proof pfts in - let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in + let ctx = Evd.universe_context_set (Evd.minimize_universes sigma) in Termops.pr_evar_universe_context (Evd.evar_universe_context sigma) ++ fnl () ++ str "Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx |