diff options
110 files changed, 1517 insertions, 1061 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index fcf6413be..7c3489de4 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -284,6 +284,9 @@ ci-coquelicot: <<: *ci-template-vars EXTRA_PACKAGES: "$TIMING_PACKAGES autoconf" +ci-equations: + <<: *ci-template + ci-geocoq: <<: *ci-template allow_failure: true diff --git a/.travis.yml b/.travis.yml index 3ebfbefd2..1f6bb11e0 100644 --- a/.travis.yml +++ b/.travis.yml @@ -50,6 +50,7 @@ env: - TEST_TARGET="ci-compcert TIMED=1" - TEST_TARGET="ci-coq-dpdgraph" EXTRA_OPAM="ocamlgraph" - TEST_TARGET="ci-coquelicot TIMED=1" + - TEST_TARGET="ci-equations TIMED=1" - TEST_TARGET="ci-geocoq TIMED=1" - TEST_TARGET="ci-fiat-crypto TIMED=1" - TEST_TARGET="ci-fiat-parsers TIMED=1" diff --git a/API/API.ml b/API/API.ml index f588fe193..78d9c0c26 100644 --- a/API/API.ml +++ b/API/API.ml @@ -275,6 +275,7 @@ module Command = Command module Classes = Classes (* module Record *) (* module Assumptions *) +module Vernacstate = Vernacstate module Vernacinterp = Vernacinterp module Mltop = Mltop module Topfmt = Topfmt diff --git a/API/API.mli b/API/API.mli index 704f1a356..86c6f1415 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4389,6 +4389,8 @@ sig val default_binder_kind : Constrexpr.binder_kind val mkLetInC : Names.Name.t Loc.located * Constrexpr.constr_expr * Constrexpr.constr_expr option * Constrexpr.constr_expr -> Constrexpr.constr_expr val mkCProdN : ?loc:Loc.t -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> Constrexpr.constr_expr + val replace_vars_constr_expr : + Names.Id.t Names.Id.Map.t -> Constrexpr.constr_expr -> Constrexpr.constr_expr end module Notation_ops : @@ -4443,8 +4445,11 @@ end module Topconstr : sig + val replace_vars_constr_expr : - Names.Id.t Names.Id.Map.t -> Constrexpr.constr_expr -> Constrexpr.constr_expr + Names.Id.t Names.Id.Map.t -> Constrexpr.constr_expr -> Constrexpr.constr_expr + [@@ocaml.deprecated "use Constrexpr_ops.free_vars_of_constr_expr"] + end module Constrintern : @@ -4645,16 +4650,23 @@ sig type proof type 'a focus_kind + val proof : proof -> + Goal.goal list * (Goal.goal list * Goal.goal list) list * + Goal.goal list * Goal.goal list * Evd.evar_map + val run_tactic : Environ.env -> unit Proofview.tactic -> proof -> proof * (bool * Proofview_monad.Info.tree) val unshelve : proof -> proof val maximal_unfocus : 'a focus_kind -> proof -> proof val pr_proof : proof -> Pp.t + module V82 : sig val grab_evars : proof -> proof val subgoals : proof -> Goal.goal list Evd.sigma + [@@ocaml.deprecated "Use the first and fifth argument of [Proof.proof]"] + end end @@ -5138,12 +5150,20 @@ sig val pr_lconstr_env : Environ.env -> Evd.evar_map -> Constr.t -> Pp.t val pr_constr : Constr.t -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_lconstr : Constr.t -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_econstr : EConstr.constr -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] + val pr_glob_constr : Glob_term.glob_constr -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] + val pr_constr_pattern : Pattern.constr_pattern -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] + val pr_glob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.t val pr_lglob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.t val pr_econstr_n_env : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> EConstr.constr -> Pp.t @@ -5151,11 +5171,17 @@ sig val pr_constr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t val pr_lconstr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t val pr_closed_glob : Ltac_pretype.closed_glob_constr -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_lglob_constr : Glob_term.glob_constr -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_leconstr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t val pr_leconstr : EConstr.constr -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] + val pr_global : Globnames.global_reference -> Pp.t val pr_lconstr_under_binders : Ltac_pretype.constr_under_binders -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] + val pr_lconstr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t val pr_constr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t @@ -5164,7 +5190,11 @@ sig val pr_rel_context_of : Environ.env -> Evd.evar_map -> Pp.t val pr_named_context_of : Environ.env -> Evd.evar_map -> Pp.t val pr_ltype : Term.types -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] + val pr_ljudge : EConstr.unsafe_judgment -> Pp.t * Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] + val pr_idpred : Names.Id.Pred.t -> Pp.t val pr_cpred : Names.Cpred.t -> Pp.t val pr_transparent_state : Names.transparent_state -> Pp.t @@ -5677,7 +5707,9 @@ sig val create_hint_db : bool -> hint_db_name -> Names.transparent_state -> bool -> unit val empty_hint_info : 'a Vernacexpr.hint_info_gen val repr_hint : hint -> (raw_hint * Clenv.clausenv) hint_ast + val pr_hint_db_env : Environ.env -> Evd.evar_map -> Hint_db.t -> Pp.t val pr_hint_db : Hint_db.t -> Pp.t + [@@ocaml.deprecated "please used pr_hint_db_env"] end module Auto : @@ -5754,7 +5786,7 @@ sig val add_rew_rules : string -> raw_rew_rule list -> unit val find_rewrites : string -> rew_rule list val find_matches : string -> Constr.t -> rew_rule list - val print_rewrite_hintdb : string -> Pp.t + val print_rewrite_hintdb : Environ.env -> Evd.evar_map -> string -> Pp.t end (************************************************************************) @@ -5787,11 +5819,12 @@ sig Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> Globnames.global_reference -> 'a val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit val get_current_context : unit -> Evd.evar_map * Environ.env + [@@ocaml.deprecated "please use [Pfedit.get_current_context]"] end module Himsg : sig - val explain_refiner_error : Logic.refiner_error -> Pp.t + val explain_refiner_error : Environ.env -> Evd.evar_map -> Logic.refiner_error -> Pp.t val explain_pretype_error : Environ.env -> Evd.evar_map -> Pretype_errors.pretype_error -> Pp.t end @@ -5929,14 +5962,30 @@ sig Names.Id.t end +module Vernacstate : +sig + + type t = { (* TODO: inline records in OCaml 4.03 *) + system : States.state; (* summary + libstack *) + proof : Proof_global.state; (* proof state *) + shallow : bool (* is the state trimmed down (libstack) *) + } + + (* XXX: This should not be exported *) + val freeze_interp_state : Summary.marshallable -> t + val unfreeze_interp_state : t -> unit + +end + module Vernacinterp : sig + type deprecation = bool - type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> unit + type vernac_command = + Genarg.raw_generic_argument list -> Loc.t option -> Vernacstate.t -> Vernacstate.t - val vinterp_add : deprecation -> Vernacexpr.extend_name -> - vernac_command -> unit + val vinterp_add : deprecation -> Vernacexpr.extend_name -> vernac_command -> unit end @@ -5958,15 +6007,6 @@ end module Vernacentries : sig - type interp_state = { (* TODO: inline records in OCaml 4.03 *) - system : States.state; (* summary + libstack *) - proof : Proof_global.state; (* proof state *) - shallow : bool (* is the state trimmed down (libstack) *) - } - - val freeze_interp_state : Summary.marshallable -> interp_state - val unfreeze_interp_state : interp_state -> unit - val dump_global : Libnames.reference Misctypes.or_by_notation -> unit val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr -> Evd.evar_map * Redexpr.red_expr) Hook.t @@ -5998,7 +6038,7 @@ sig val get_doc : Feedback.doc_id -> doc val state_of_id : doc:doc -> - Stateid.t -> [ `Valid of Vernacentries.interp_state option | `Expired | `Error of exn ] + Stateid.t -> [ `Valid of Vernacstate.t option | `Expired | `Error of exn ] end (************************************************************************) diff --git a/Makefile.build b/Makefile.build index 991942bf0..39b793d2b 100644 --- a/Makefile.build +++ b/Makefile.build @@ -734,8 +734,8 @@ $(MICROMEGAV:.v=.vo) $(MICROMEGAV:.v=.glob) : $(MICROMEGAV) theories/Init/Prelud $(SHOW)'COQC $<' $(HIDE)rm -f $*.glob $(HIDE)$(BOOTCOQC) $< | sed -e '$$d' > $(MICROMEGAGEN) - $(HIDE)cmp -s $(MICROMEGAML) $(MICROMEGAGEN) || \ - echo "Warning: $(MICROMEGAML) and the code generated by $(MICROMEGAV) differ !" + $(HIDE)diff -u --strip-trailing-cr $(MICROMEGAML) $(MICROMEGAGEN) || \ + (2>&1 echo "Error: $(MICROMEGAML) and the code generated by $(MICROMEGAV) differ !" && false) # The general rule for building .vo files : diff --git a/Makefile.ci b/Makefile.ci index 0b2cbb663..a17d4ddf7 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -5,6 +5,7 @@ CI_TARGETS=ci-all \ ci-coq-dpdgraph \ ci-coquelicot \ ci-cpdt \ + ci-equations \ ci-fiat-crypto \ ci-fiat-parsers \ ci-flocq \ diff --git a/Makefile.install b/Makefile.install index 55229deb9..b590aad54 100644 --- a/Makefile.install +++ b/Makefile.install @@ -144,7 +144,7 @@ install-coq-manpages: install-emacs: $(MKDIR) $(FULLEMACSLIB) - $(INSTALLLIB) tools/gallina-db.el tools/coq-font-lock.el tools/gallina-syntax.el tools/gallina.el tools/coq-inferior.el $(FULLEMACSLIB) + $(INSTALLLIB) tools/gallina-db.el tools/coq-font-lock.el tools/gallina-syntax.el tools/gallina.el tools/inferior-coq.el $(FULLEMACSLIB) # command to update TeX' kpathsea database #UPDATETEX = $(MKTEXLSR) /usr/share/texmf /var/spool/texmf $(BASETEXDIR) > /dev/null diff --git a/dev/base_include b/dev/base_include index f2912e112..1da5e3ed1 100644 --- a/dev/base_include +++ b/dev/base_include @@ -130,7 +130,6 @@ open Reserve open Syntax_def open Constrexpr open Constrexpr_ops -open Topconstr open Notation_term open Notation_ops open Prettyp @@ -231,7 +230,7 @@ let pf_e gl s = let _ = Flags.in_debugger := false let _ = Flags.in_toplevel := true let _ = Constrextern.set_extern_reference - (fun ?loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));; + (fun ?loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Id.Set.empty r));; let go () = Coqloop.loop Option.(get !Coqtop.drop_last_doc) diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index cb1493d6a..168a34e6e 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -135,3 +135,9 @@ ######################################################################## : ${bignums_CI_BRANCH:=master} : ${bignums_CI_GITURL:=https://github.com/coq/bignums.git} + +######################################################################## +# Equations +######################################################################## +: ${Equations_CI_BRANCH:=8.8+alpha} +: ${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations.git} diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh new file mode 100755 index 000000000..f7470463d --- /dev/null +++ b/dev/ci/ci-equations.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +Equations_CI_DIR=${CI_BUILD_DIR}/Equations + +git_checkout ${Equations_CI_BRANCH} ${Equations_CI_GITURL} ${Equations_CI_DIR} + +( cd ${Equations_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} && make -j ${NJOBS} test-suite && make -j ${NJOBS} examples && make install) diff --git a/dev/top_printers.ml b/dev/top_printers.ml index b4c8ae33c..0f496d3b9 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -60,6 +60,7 @@ let pprecarg = function let ppwf_paths x = pp (Rtree.pp_tree pprecarg x) (* term printers *) +let envpp pp = let sigma,env = Pfedit.get_current_context () in pp env sigma let rawdebug = ref false let ppevar evk = pp (str (Evd.string_of_existential evk)) let ppconstr x = pp (Termops.print_constr (EConstr.of_constr x)) @@ -69,9 +70,9 @@ let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr (EConstr.o let ppterm = ppconstr let ppsconstr x = ppconstr (Mod_subst.force_constr x) let ppconstr_univ x = Constrextern.with_universes ppconstr x -let ppglob_constr = (fun x -> pp(pr_lglob_constr x)) -let pppattern = (fun x -> pp(pr_constr_pattern x)) -let pptype = (fun x -> try pp(pr_ltype x) with e -> pp (str (Printexc.to_string e))) +let ppglob_constr = (fun x -> pp(pr_lglob_constr_env (Global.env()) x)) +let pppattern = (fun x -> pp(envpp pr_constr_pattern_env x)) +let pptype = (fun x -> try pp(envpp pr_ltype_env x) with e -> pp (str (Printexc.to_string e))) let ppfconstr c = ppconstr (CClosure.term_of_fconstr c) let ppbigint n = pp (str (Bigint.to_string n));; @@ -121,7 +122,7 @@ let rec pr_closure {idents=idents;typed=typed;untyped=untyped} = and pr_closed_glob_constr_idmap x = pridmap (fun _ -> pr_closed_glob_constr) x and pr_closed_glob_constr {closure=closure;term=term} = - pr_closure closure ++ pr_lglob_constr term + pr_closure closure ++ (pr_lglob_constr_env Global.(env ())) term let ppclosure x = pp (pr_closure x) let ppclosedglobconstr x = pp (pr_closed_glob_constr x) @@ -140,14 +141,14 @@ let safe_pr_global = function let ppglobal x = try pp(pr_global x) with _ -> safe_pr_global x let ppconst (sp,j) = - pp (str"#" ++ KerName.print sp ++ str"=" ++ pr_lconstr j.uj_val) + pp (str"#" ++ KerName.print sp ++ str"=" ++ envpp pr_lconstr_env j.uj_val) let ppvar ((id,a)) = - pp (str"#" ++ Id.print id ++ str":" ++ pr_lconstr a) + pp (str"#" ++ Id.print id ++ str":" ++ envpp pr_lconstr_env a) let genppj f j = let (c,t) = f j in (c ++ str " : " ++ t) -let ppj j = pp (genppj pr_ljudge j) +let ppj j = pp (genppj (envpp pr_ljudge_env) j) let prsubst s = pp (Mod_subst.debug_pr_subst s) let prdelta s = pp (Mod_subst.debug_pr_delta s) @@ -175,13 +176,13 @@ let ppclenv clenv = pp(pr_clenv clenv) let ppgoalgoal gl = pp(Goal.pr_goal gl) let ppgoal g = pp(Printer.pr_goal g) let ppgoalsigma g = pp(Printer.pr_goal g ++ Termops.pr_evar_map None (Refiner.project g)) -let pphintdb db = pp(Hints.pr_hint_db db) +let pphintdb db = pp(envpp Hints.pr_hint_db_env db) let ppproofview p = let gls,sigma = Proofview.proofview p in pp(pr_enum Goal.pr_goal gls ++ fnl () ++ Termops.pr_evar_map (Some 1) sigma) let ppopenconstr (x : Evd.open_constr) = - let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) evd ++ pr_constr c) + let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) evd ++ envpp pr_constr_env c) (* spiwack: deactivated until a replacement is found let pppftreestate p = pp(print_pftreestate p) *) @@ -508,7 +509,7 @@ let _ = (function [c] when genarg_tag c = unquote (topwit wit_constr) && true -> let c = out_gen (rawwit wit_constr) c in - (fun _ -> in_current_context constr_display c) + (fun _ st -> in_current_context constr_display c; st) | _ -> failwith "Vernac extension: cannot occur") with e -> pp (CErrors.print e) @@ -524,7 +525,7 @@ let _ = (function [c] when genarg_tag c = unquote (topwit wit_constr) && true -> let c = out_gen (rawwit wit_constr) c in - (fun _ -> in_current_context print_pure_constr c) + (fun _ st -> in_current_context print_pure_constr c; st) | _ -> failwith "Vernac extension: cannot occur") with e -> pp (CErrors.print e) diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index 8f846f2f5..c411db100 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -467,7 +467,7 @@ the \Coq\ language, and also a rudimentary indentation facility: \end{itemize} An inferior mode to run \Coq\ under Emacs, by Marco Maggesi, is also -included in the distribution, in file \texttt{coq-inferior.el}. +included in the distribution, in file \texttt{inferior-coq.el}. Instructions to use it are contained in this file. \subsection[{\ProofGeneral}]{{\ProofGeneral}\index{Proof General@{\ProofGeneral}}} diff --git a/engine/proofview.mli b/engine/proofview.mli index 0379d4b49..7f7acf874 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -563,6 +563,7 @@ module V82 : sig (* Returns the open goals of the proofview together with the evar_map to interpret them. *) val goals : proofview -> Evar.t list Evd.sigma + [@@ocaml.deprecated "Use [Proofview.proofview]"] val top_goals : entry -> proofview -> Evar.t list Evd.sigma diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index 874712124..12308bede 100644 --- a/grammar/vernacextend.mlp +++ b/grammar/vernacextend.mlp @@ -158,18 +158,26 @@ EXTEND deprecation: [ [ "DEPRECATED" -> () ] ] ; - (* spiwack: comment-by-guessing: it seems that the isolated string (which - otherwise could have been another argument) is not passed to the - VernacExtend interpreter function to discriminate between the clauses. *) + (* spiwack: comment-by-guessing: it seems that the isolated string + (which otherwise could have been another argument) is not passed + to the VernacExtend interpreter function to discriminate between + the clauses. *) + + (* ejga: Due to the LocalityFixme abomination we cannot eta-expand + [e] as we'd like to, so we need to use the below mess with [fun + st -> st]. + + At some point We should solve the mess and extend + vernacextend.mlp with locality info. *) rule: [ [ "["; s = STRING; l = LIST0 args; "]"; d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> let () = if s = "" then failwith "Command name is empty." in - let b = <:expr< fun loc -> $e$ >> in + let b = <:expr< fun loc -> ( let () = $e$ in fun st -> st ) >> in { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; } | "[" ; "-" ; l = LIST1 args ; "]" ; d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> - let b = <:expr< fun loc -> $e$ >> in + let b = <:expr< fun loc -> ( let () = $e$ in fun st -> st ) >> in { r_head = None; r_patt = l; r_class = c; r_branch = b; r_depr = d; } ] ] ; diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 7cbab56d4..cfc0e09a0 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -217,7 +217,7 @@ let evars () = let doc = get_doc () in set_doc @@ Stm.finish ~doc; let pfts = Proof_global.give_me_the_proof () in - let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in + let all_goals, _, _, _, sigma = Proof.proof pfts in let exl = Evar.Map.bindings (Evd.undefined_map sigma) in let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar sigma ev); } in let el = List.map map_evar exl in @@ -227,7 +227,7 @@ let evars () = let hints () = try let pfts = Proof_global.give_me_the_proof () in - let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in + let all_goals, _, _, _, sigma = Proof.proof pfts in match all_goals with | [] -> None | g :: _ -> diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 771c13734..737e86848 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -9,6 +9,7 @@ open Pp open Util open Names +open Nameops open Libnames open Constrexpr open Misctypes @@ -72,22 +73,22 @@ let rec cases_pattern_expr_eq p1 p2 = Option.equal (List.equal cases_pattern_expr_eq) a1 a2 && List.equal cases_pattern_expr_eq b1 b2 | CPatAtom(r1), CPatAtom(r2) -> - Option.equal eq_reference r1 r2 + Option.equal eq_reference r1 r2 | CPatOr a1, CPatOr a2 -> - List.equal cases_pattern_expr_eq a1 a2 + List.equal cases_pattern_expr_eq a1 a2 | CPatNotation (n1, s1, l1), CPatNotation (n2, s2, l2) -> String.equal n1 n2 && cases_pattern_notation_substitution_eq s1 s2 && List.equal cases_pattern_expr_eq l1 l2 | CPatPrim i1, CPatPrim i2 -> - prim_token_eq i1 i2 + prim_token_eq i1 i2 | CPatRecord l1, CPatRecord l2 -> - let equal (r1, e1) (r2, e2) = - eq_reference r1 r2 && cases_pattern_expr_eq e1 e2 - in - List.equal equal l1 l2 + let equal (r1, e1) (r2, e2) = + eq_reference r1 r2 && cases_pattern_expr_eq e1 e2 + in + List.equal equal l1 l2 | CPatDelimiters(s1,e1), CPatDelimiters(s2,e2) -> - String.equal s1 s2 && cases_pattern_expr_eq e1 e2 + String.equal s1 s2 && cases_pattern_expr_eq e1 e2 | _ -> false and cases_pattern_notation_substitution_eq (s1, n1) (s2, n2) = @@ -103,79 +104,79 @@ let eq_universes u1 u2 = let rec constr_expr_eq e1 e2 = if CAst.(e1.v == e2.v) then true else match CAst.(e1.v, e2.v) with - | CRef (r1,u1), CRef (r2,u2) -> eq_reference r1 r2 && eq_universes u1 u2 - | CFix(id1,fl1), CFix(id2,fl2) -> + | CRef (r1,u1), CRef (r2,u2) -> eq_reference r1 r2 && eq_universes u1 u2 + | CFix(id1,fl1), CFix(id2,fl2) -> eq_located Id.equal id1 id2 && List.equal fix_expr_eq fl1 fl2 - | CCoFix(id1,fl1), CCoFix(id2,fl2) -> + | CCoFix(id1,fl1), CCoFix(id2,fl2) -> eq_located Id.equal id1 id2 && List.equal cofix_expr_eq fl1 fl2 - | CProdN(bl1,a1), CProdN(bl2,a2) -> + | CProdN(bl1,a1), CProdN(bl2,a2) -> List.equal binder_expr_eq bl1 bl2 && constr_expr_eq a1 a2 - | CLambdaN(bl1,a1), CLambdaN(bl2,a2) -> + | CLambdaN(bl1,a1), CLambdaN(bl2,a2) -> List.equal binder_expr_eq bl1 bl2 && constr_expr_eq a1 a2 - | CLetIn((_,na1),a1,t1,b1), CLetIn((_,na2),a2,t2,b2) -> + | CLetIn((_,na1),a1,t1,b1), CLetIn((_,na2),a2,t2,b2) -> Name.equal na1 na2 && constr_expr_eq a1 a2 && Option.equal constr_expr_eq t1 t2 && constr_expr_eq b1 b2 - | CAppExpl((proj1,r1,_),al1), CAppExpl((proj2,r2,_),al2) -> + | CAppExpl((proj1,r1,_),al1), CAppExpl((proj2,r2,_),al2) -> Option.equal Int.equal proj1 proj2 && eq_reference r1 r2 && List.equal constr_expr_eq al1 al2 - | CApp((proj1,e1),al1), CApp((proj2,e2),al2) -> + | CApp((proj1,e1),al1), CApp((proj2,e2),al2) -> Option.equal Int.equal proj1 proj2 && constr_expr_eq e1 e2 && List.equal args_eq al1 al2 - | CRecord l1, CRecord l2 -> - let field_eq (r1, e1) (r2, e2) = - eq_reference r1 r2 && constr_expr_eq e1 e2 - in - List.equal field_eq l1 l2 - | CCases(_,r1,a1,brl1), CCases(_,r2,a2,brl2) -> + | CRecord l1, CRecord l2 -> + let field_eq (r1, e1) (r2, e2) = + eq_reference r1 r2 && constr_expr_eq e1 e2 + in + List.equal field_eq l1 l2 + | CCases(_,r1,a1,brl1), CCases(_,r2,a2,brl2) -> (** Don't care about the case_style *) Option.equal constr_expr_eq r1 r2 && List.equal case_expr_eq a1 a2 && List.equal branch_expr_eq brl1 brl2 - | CLetTuple (n1, (m1, e1), t1, b1), CLetTuple (n2, (m2, e2), t2, b2) -> - List.equal (eq_located Name.equal) n1 n2 && - Option.equal (eq_located Name.equal) m1 m2 && - Option.equal constr_expr_eq e1 e2 && - constr_expr_eq t1 t2 && - constr_expr_eq b1 b2 - | CIf (e1, (n1, r1), t1, f1), CIf (e2, (n2, r2), t2, f2) -> - constr_expr_eq e1 e2 && - Option.equal (eq_located Name.equal) n1 n2 && - Option.equal constr_expr_eq r1 r2 && - constr_expr_eq t1 t2 && - constr_expr_eq f1 f2 - | CHole _, CHole _ -> true - | CPatVar i1, CPatVar i2 -> - Id.equal i1 i2 - | CEvar (id1, c1), CEvar (id2, c2) -> - Id.equal id1 id2 && List.equal instance_eq c1 c2 - | CSort s1, CSort s2 -> - Miscops.glob_sort_eq s1 s2 - | CCast(a1,(CastConv b1|CastVM b1)), CCast(a2,(CastConv b2|CastVM b2)) -> + | CLetTuple (n1, (m1, e1), t1, b1), CLetTuple (n2, (m2, e2), t2, b2) -> + List.equal (eq_located Name.equal) n1 n2 && + Option.equal (eq_located Name.equal) m1 m2 && + Option.equal constr_expr_eq e1 e2 && + constr_expr_eq t1 t2 && + constr_expr_eq b1 b2 + | CIf (e1, (n1, r1), t1, f1), CIf (e2, (n2, r2), t2, f2) -> + constr_expr_eq e1 e2 && + Option.equal (eq_located Name.equal) n1 n2 && + Option.equal constr_expr_eq r1 r2 && + constr_expr_eq t1 t2 && + constr_expr_eq f1 f2 + | CHole _, CHole _ -> true + | CPatVar i1, CPatVar i2 -> + Id.equal i1 i2 + | CEvar (id1, c1), CEvar (id2, c2) -> + Id.equal id1 id2 && List.equal instance_eq c1 c2 + | CSort s1, CSort s2 -> + Miscops.glob_sort_eq s1 s2 + | CCast(a1,(CastConv b1|CastVM b1)), CCast(a2,(CastConv b2|CastVM b2)) -> constr_expr_eq a1 a2 && constr_expr_eq b1 b2 - | CCast(a1,CastCoerce), CCast(a2, CastCoerce) -> + | CCast(a1,CastCoerce), CCast(a2, CastCoerce) -> constr_expr_eq a1 a2 - | CNotation(n1, s1), CNotation(n2, s2) -> + | CNotation(n1, s1), CNotation(n2, s2) -> String.equal n1 n2 && constr_notation_substitution_eq s1 s2 - | CPrim i1, CPrim i2 -> - prim_token_eq i1 i2 - | CGeneralization (bk1, ak1, e1), CGeneralization (bk2, ak2, e2) -> - binding_kind_eq bk1 bk2 && - Option.equal abstraction_kind_eq ak1 ak2 && - constr_expr_eq e1 e2 - | CDelimiters(s1,e1), CDelimiters(s2,e2) -> - String.equal s1 s2 && - constr_expr_eq e1 e2 - | _ -> false + | CPrim i1, CPrim i2 -> + prim_token_eq i1 i2 + | CGeneralization (bk1, ak1, e1), CGeneralization (bk2, ak2, e2) -> + binding_kind_eq bk1 bk2 && + Option.equal abstraction_kind_eq ak1 ak2 && + constr_expr_eq e1 e2 + | CDelimiters(s1,e1), CDelimiters(s2,e2) -> + String.equal s1 s2 && + constr_expr_eq e1 e2 + | _ -> false and args_eq (a1,e1) (a2,e2) = Option.equal (eq_located explicitation_eq) e1 e2 && @@ -209,19 +210,19 @@ and cofix_expr_eq (id1,bl1,a1,b1) (id2,bl2,a2,b2) = constr_expr_eq b1 b2 and recursion_order_expr_eq r1 r2 = match r1, r2 with -| CStructRec, CStructRec -> true -| CWfRec e1, CWfRec e2 -> constr_expr_eq e1 e2 -| CMeasureRec (e1, o1), CMeasureRec (e2, o2) -> - constr_expr_eq e1 e2 && Option.equal constr_expr_eq o1 o2 -| _ -> false + | CStructRec, CStructRec -> true + | CWfRec e1, CWfRec e2 -> constr_expr_eq e1 e2 + | CMeasureRec (e1, o1), CMeasureRec (e2, o2) -> + constr_expr_eq e1 e2 && Option.equal constr_expr_eq o1 o2 + | _ -> false and local_binder_eq l1 l2 = match l1, l2 with -| CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) -> - eq_located Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2 -| CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) -> - (** Don't care about the [binder_kind] *) - List.equal (eq_located Name.equal) n1 n2 && constr_expr_eq e1 e2 -| _ -> false + | CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) -> + eq_located Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2 + | CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) -> + (** Don't care about the [binder_kind] *) + List.equal (eq_located Name.equal) n1 n2 && constr_expr_eq e1 e2 + | _ -> false and constr_notation_substitution_eq (e1, el1, bl1) (e2, el2, bl2) = List.equal constr_expr_eq e1 e2 && @@ -245,6 +246,270 @@ let local_binders_loc bll = match bll with | [] -> None | h :: l -> Loc.merge_opt (local_binder_loc h) (local_binder_loc (List.last bll)) +(** Folds and maps *) + +(* Legacy functions *) +let down_located f (_l, x) = f x +let located_fold_left f x (_l, y) = f x y + +let is_constructor id = + try Globnames.isConstructRef + (Smartlocate.global_of_extended_global + (Nametab.locate_extended (qualid_of_ident id))) + with Not_found -> false + +let rec cases_pattern_fold_names f a pt = match CAst.(pt.v) with + | CPatRecord l -> + List.fold_left (fun acc (r, cp) -> cases_pattern_fold_names f acc cp) a l + | CPatAlias (pat,id) -> f id a + | CPatOr (patl) -> + List.fold_left (cases_pattern_fold_names f) a patl + | CPatCstr (_,patl1,patl2) -> + List.fold_left (cases_pattern_fold_names f) + (Option.fold_left (List.fold_left (cases_pattern_fold_names f)) a patl1) patl2 + | CPatNotation (_,(patl,patll),patl') -> + List.fold_left (cases_pattern_fold_names f) + (List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)) patl' + | CPatDelimiters (_,pat) -> cases_pattern_fold_names f a pat + | CPatAtom (Some (Ident (_,id))) when not (is_constructor id) -> f id a + | CPatPrim _ | CPatAtom _ -> a + | CPatCast ({CAst.loc},_) -> + CErrors.user_err ?loc ~hdr:"cases_pattern_fold_names" + (Pp.strbrk "Casts are not supported here.") + +let ids_of_pattern = + cases_pattern_fold_names Id.Set.add Id.Set.empty + +let ids_of_pattern_list = + List.fold_left + (located_fold_left + (List.fold_left (cases_pattern_fold_names Id.Set.add))) + Id.Set.empty + +let ids_of_cases_indtype p = + cases_pattern_fold_names Id.Set.add Id.Set.empty p + +let ids_of_cases_tomatch tms = + List.fold_right + (fun (_, ona, indnal) l -> + Option.fold_right (fun t ids -> cases_pattern_fold_names Id.Set.add ids t) + indnal + (Option.fold_right (down_located (Name.fold_right Id.Set.add)) ona l)) + tms Id.Set.empty + +let rec fold_constr_expr_binders g f n acc b = function + | (nal,bk,t)::l -> + let nal = snd (List.split nal) in + let n' = List.fold_right (Name.fold_right g) nal n in + f n (fold_constr_expr_binders g f n' acc b l) t + | [] -> + f n acc b + +let rec fold_local_binders g f n acc b = function + | CLocalAssum (nal,bk,t)::l -> + let nal = snd (List.split nal) in + let n' = List.fold_right (Name.fold_right g) nal n in + f n (fold_local_binders g f n' acc b l) t + | CLocalDef ((_,na),c,t)::l -> + Option.fold_left (f n) (f n (fold_local_binders g f (Name.fold_right g na n) acc b l) c) t + | CLocalPattern (_,(pat,t))::l -> + let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in + Option.fold_left (f n) acc t + | [] -> + f n acc b + +let fold_constr_expr_with_binders g f n acc = CAst.with_val (function + | CAppExpl ((_,_,_),l) -> List.fold_left (f n) acc l + | CApp ((_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l) + | CProdN (l,b) | CLambdaN (l,b) -> fold_constr_expr_binders g f n acc b l + | CLetIn (na,a,t,b) -> + f (Name.fold_right g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b + | CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b + | CCast (a,CastCoerce) -> f n acc a + | CNotation (_,(l,ll,bll)) -> + (* The following is an approximation: we don't know exactly if + an ident is binding nor to which subterms bindings apply *) + let acc = List.fold_left (f n) acc (l@List.flatten ll) in + List.fold_left (fun acc bl -> fold_local_binders g f n acc (CAst.make @@ CHole (None,IntroAnonymous,None)) bl) acc bll + | CGeneralization (_,_,c) -> f n acc c + | CDelimiters (_,a) -> f n acc a + | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CRef _ -> + acc + | CRecord l -> List.fold_left (fun acc (id, c) -> f n acc c) acc l + | CCases (sty,rtnpo,al,bl) -> + let ids = ids_of_cases_tomatch al in + let acc = Option.fold_left (f (Id.Set.fold g ids n)) acc rtnpo in + let acc = List.fold_left (f n) acc (List.map (fun (fst,_,_) -> fst) al) in + List.fold_right (fun (loc,(patl,rhs)) acc -> + let ids = ids_of_pattern_list patl in + f (Id.Set.fold g ids n) acc rhs) bl acc + | CLetTuple (nal,(ona,po),b,c) -> + let n' = List.fold_right (down_located (Name.fold_right g)) nal n in + f (Option.fold_right (down_located (Name.fold_right g)) ona n') (f n acc b) c + | CIf (c,(ona,po),b1,b2) -> + let acc = f n (f n (f n acc b1) b2) c in + Option.fold_left + (f (Option.fold_right (down_located (Name.fold_right g)) ona n)) acc po + | CFix (_,l) -> + let n' = List.fold_right (fun ((_,id),_,_,_,_) -> g id) l n in + List.fold_right (fun (_,(_,o),lb,t,c) acc -> + fold_local_binders g f n' + (fold_local_binders g f n acc t lb) c lb) l acc + | CCoFix (_,_) -> + Feedback.msg_warning (strbrk "Capture check in multiple binders not done"); acc + ) + +let free_vars_of_constr_expr c = + let rec aux bdvars l = function + | { CAst.v = CRef (Ident (_,id),_) } -> if Id.List.mem id bdvars then l else Id.Set.add id l + | c -> fold_constr_expr_with_binders (fun a l -> a::l) aux bdvars l c + in aux [] Id.Set.empty c + +let occur_var_constr_expr id c = Id.Set.mem id (free_vars_of_constr_expr c) + +(* Used in correctness and interface *) +let map_binder g e nal = List.fold_right (down_located (Name.fold_right g)) nal e + +let map_binders f g e bl = + (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *) + let h (e,bl) (nal,bk,t) = (map_binder g e nal,(nal,bk,f e t)::bl) in + let (e,rbl) = List.fold_left h (e,[]) bl in + (e, List.rev rbl) + +let map_local_binders f g e bl = + (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *) + let h (e,bl) = function + CLocalAssum(nal,k,ty) -> + (map_binder g e nal, CLocalAssum(nal,k,f e ty)::bl) + | CLocalDef((loc,na),c,ty) -> + (Name.fold_right g na e, CLocalDef((loc,na),f e c,Option.map (f e) ty)::bl) + | CLocalPattern (loc,(pat,t)) -> + let ids = ids_of_pattern pat in + (Id.Set.fold g ids e, CLocalPattern (loc,(pat,Option.map (f e) t))::bl) in + let (e,rbl) = List.fold_left h (e,[]) bl in + (e, List.rev rbl) + +let map_constr_expr_with_binders g f e = CAst.map (function + | CAppExpl (r,l) -> CAppExpl (r,List.map (f e) l) + | CApp ((p,a),l) -> + CApp ((p,f e a),List.map (fun (a,i) -> (f e a,i)) l) + | CProdN (bl,b) -> + let (e,bl) = map_binders f g e bl in CProdN (bl,f e b) + | CLambdaN (bl,b) -> + let (e,bl) = map_binders f g e bl in CLambdaN (bl,f e b) + | CLetIn (na,a,t,b) -> + CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (snd na) e) b) + | CCast (a,c) -> CCast (f e a, Miscops.map_cast_type (f e) c) + | CNotation (n,(l,ll,bll)) -> + (* This is an approximation because we don't know what binds what *) + CNotation (n,(List.map (f e) l,List.map (List.map (f e)) ll, + List.map (fun bl -> snd (map_local_binders f g e bl)) bll)) + | CGeneralization (b,a,c) -> CGeneralization (b,a,f e c) + | CDelimiters (s,a) -> CDelimiters (s,f e a) + | CHole _ | CEvar _ | CPatVar _ | CSort _ + | CPrim _ | CRef _ as x -> x + | CRecord l -> CRecord (List.map (fun (id, c) -> (id, f e c)) l) + | CCases (sty,rtnpo,a,bl) -> + let bl = List.map (fun (loc,(patl,rhs)) -> + let ids = ids_of_pattern_list patl in + (loc,(patl,f (Id.Set.fold g ids e) rhs))) bl in + let ids = ids_of_cases_tomatch a in + let po = Option.map (f (Id.Set.fold g ids e)) rtnpo in + CCases (sty, po, List.map (fun (tm,x,y) -> f e tm,x,y) a,bl) + | CLetTuple (nal,(ona,po),b,c) -> + let e' = List.fold_right (down_located (Name.fold_right g)) nal e in + let e'' = Option.fold_right (down_located (Name.fold_right g)) ona e in + CLetTuple (nal,(ona,Option.map (f e'') po),f e b,f e' c) + | CIf (c,(ona,po),b1,b2) -> + let e' = Option.fold_right (down_located (Name.fold_right g)) ona e in + CIf (f e c,(ona,Option.map (f e') po),f e b1,f e b2) + | CFix (id,dl) -> + CFix (id,List.map (fun (id,n,bl,t,d) -> + let (e',bl') = map_local_binders f g e bl in + let t' = f e' t in + (* Note: fix names should be inserted before the arguments... *) + let e'' = List.fold_left (fun e ((_,id),_,_,_,_) -> g id e) e' dl in + let d' = f e'' d in + (id,n,bl',t',d')) dl) + | CCoFix (id,dl) -> + CCoFix (id,List.map (fun (id,bl,t,d) -> + let (e',bl') = map_local_binders f g e bl in + let t' = f e' t in + let e'' = List.fold_left (fun e ((_,id),_,_,_) -> g id e) e' dl in + let d' = f e'' d in + (id,bl',t',d')) dl) + ) + +(* Used in constrintern *) +let rec replace_vars_constr_expr l = function + | { CAst.loc; v = CRef (Ident (loc_id,id),us) } as x -> + (try CAst.make ?loc @@ CRef (Ident (loc_id,Id.Map.find id l),us) with Not_found -> x) + | c -> map_constr_expr_with_binders Id.Map.remove + replace_vars_constr_expr l c + +(* Returns the ranges of locs of the notation that are not occupied by args *) +(* and which are then occupied by proper symbols of the notation (or spaces) *) + +let locs_of_notation ?loc locs ntn = + let unloc loc = Option.cata Loc.unloc (0,0) loc in + let (bl, el) = unloc loc in + let locs = List.map unloc locs in + let rec aux pos = function + | [] -> if Int.equal pos el then [] else [(pos,el)] + | (ba,ea)::l -> if Int.equal pos ba then aux ea l else (pos,ba)::aux ea l + in aux bl (List.sort (fun l1 l2 -> fst l1 - fst l2) locs) + +let ntn_loc ?loc (args,argslist,binderslist) = + locs_of_notation ?loc + (List.map constr_loc (args@List.flatten argslist)@ + List.map local_binders_loc binderslist) + +let patntn_loc ?loc (args,argslist) = + locs_of_notation ?loc + (List.map cases_pattern_expr_loc (args@List.flatten argslist)) + +let error_invalid_pattern_notation ?loc () = + CErrors.user_err ?loc (str "Invalid notation for pattern.") + +(* Interpret the index of a recursion order annotation *) +let split_at_annot bl na = + let names = List.map snd (names_of_local_assums bl) in + match na with + | None -> + begin match names with + | [] -> CErrors.user_err (Pp.str "A fixpoint needs at least one parameter.") + | _ -> ([], bl) + end + | Some (loc, id) -> + let rec aux acc = function + | CLocalAssum (bls, k, t) as x :: rest -> + let test (_, na) = match na with + | Name id' -> Id.equal id id' + | Anonymous -> false + in + let l, r = List.split_when test bls in + begin match r with + | [] -> aux (x :: acc) rest + | _ -> + let ans = match l with + | [] -> acc + | _ -> CLocalAssum (l, k, t) :: acc + in + (List.rev ans, CLocalAssum (r, k, t) :: rest) + end + | CLocalDef ((_,na),_,_) as x :: rest -> + if Name.equal (Name id) na then + CErrors.user_err ?loc + (Id.print id ++ str" must be a proper parameter and not a local definition.") + else + aux (x :: acc) rest + | CLocalPattern (_,_) :: rest -> + Loc.raise ?loc (Stream.Error "pattern with quote not allowed after fix") + | [] -> + CErrors.user_err ?loc + (str "No parameter named " ++ Id.print id ++ str".") + in aux [] bl + (** Pseudo-constructors *) let mkIdentC id = CAst.make @@ CRef (Ident (Loc.tag id),None) @@ -265,38 +530,40 @@ let add_name_in_env env n = | Anonymous -> env | Name id -> id :: env -let (fresh_var, fresh_var_hook) = Hook.make ~default:(fun _ _ -> assert false) () +let fresh_var env c = + Namegen.next_ident_away (Id.of_string "pat") + (List.fold_left (fun accu id -> Id.Set.add id accu) (free_vars_of_constr_expr c) env) let expand_binders ?loc mkC bl c = let rec loop ?loc bl c = match bl with | [] -> ([], c) | b :: bl -> - match b with - | CLocalDef ((loc1,_) as n, oty, b) -> - let env, c = loop ?loc:(Loc.merge_opt loc1 loc) bl c in - let env = add_name_in_env env n in - (env, CAst.make ?loc @@ CLetIn (n,oty,b,c)) - | CLocalAssum ((loc1,_)::_ as nl, bk, t) -> - let env, c = loop ?loc:(Loc.merge_opt loc1 loc) bl c in - let env = List.fold_left add_name_in_env env nl in - (env, mkC ?loc (nl,bk,t) c) - | CLocalAssum ([],_,_) -> loop ?loc bl c - | CLocalPattern (loc1, (p, ty)) -> - let env, c = loop ?loc:(Loc.merge_opt loc1 loc) bl c in - let ni = Hook.get fresh_var env c in - let id = (loc1, Name ni) in - let ty = match ty with - | Some ty -> ty - | None -> CAst.make ?loc:loc1 @@ CHole (None, IntroAnonymous, None) - in - let e = CAst.make @@ CRef (Libnames.Ident (loc1, ni), None) in - let c = CAst.make ?loc @@ - CCases - (LetPatternStyle, None, [(e,None,None)], - [(Loc.tag ?loc:loc1 ([(loc1,[p])], c))]) - in - (ni :: env, mkC ?loc ([id],Default Explicit,ty) c) + match b with + | CLocalDef ((loc1,_) as n, oty, b) -> + let env, c = loop ?loc:(Loc.merge_opt loc1 loc) bl c in + let env = add_name_in_env env n in + (env, CAst.make ?loc @@ CLetIn (n,oty,b,c)) + | CLocalAssum ((loc1,_)::_ as nl, bk, t) -> + let env, c = loop ?loc:(Loc.merge_opt loc1 loc) bl c in + let env = List.fold_left add_name_in_env env nl in + (env, mkC ?loc (nl,bk,t) c) + | CLocalAssum ([],_,_) -> loop ?loc bl c + | CLocalPattern (loc1, (p, ty)) -> + let env, c = loop ?loc:(Loc.merge_opt loc1 loc) bl c in + let ni = fresh_var env c in + let id = (loc1, Name ni) in + let ty = match ty with + | Some ty -> ty + | None -> CAst.make ?loc:loc1 @@ CHole (None, IntroAnonymous, None) + in + let e = CAst.make @@ CRef (Libnames.Ident (loc1, ni), None) in + let c = CAst.make ?loc @@ + CCases + (LetPatternStyle, None, [(e,None,None)], + [(Loc.tag ?loc:loc1 ([(loc1,[p])], c))]) + in + (ni :: env, mkC ?loc ([id],Default Explicit,ty) c) in let (_, c) = loop ?loc bl c in c @@ -309,24 +576,34 @@ let mkCLambdaN ?loc bll c = let mk ?loc b c = CAst.make ?loc @@ CLambdaN ([b],c) in expand_binders ?loc mk bll c -(* Deprecated *) -let abstract_constr_expr c bl = mkCLambdaN ?loc:(local_binders_loc bl) bl c -let prod_constr_expr c bl = mkCProdN ?loc:(local_binders_loc bl) bl c - let coerce_reference_to_id = function | Ident (_,id) -> id | Qualid (loc,_) -> - CErrors.user_err ?loc ~hdr:"coerce_reference_to_id" - (str "This expression should be a simple identifier.") + CErrors.user_err ?loc ~hdr:"coerce_reference_to_id" + (str "This expression should be a simple identifier.") let coerce_to_id = function | { CAst.v = CRef (Ident (loc,id),None) } -> (loc,id) | { CAst.loc; _ } -> CErrors.user_err ?loc - ~hdr:"coerce_to_id" - (str "This expression should be a simple identifier.") + ~hdr:"coerce_to_id" + (str "This expression should be a simple identifier.") let coerce_to_name = function | { CAst.v = CRef (Ident (loc,id),None) } -> (loc,Name id) | { CAst.loc; CAst.v = CHole (None,Misctypes.IntroAnonymous,None) } -> (loc,Anonymous) | { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_name" (str "This expression should be a name.") + +let asymmetric_patterns = ref (false) +let _ = Goptions.declare_bool_option { + Goptions.optdepr = false; + Goptions.optname = "no parameters in constructors"; + Goptions.optkey = ["Asymmetric";"Patterns"]; + Goptions.optread = (fun () -> !asymmetric_patterns); + Goptions.optwrite = (fun a -> asymmetric_patterns:=a); +} + +(************************************************************************) +(* Deprecated *) +let abstract_constr_expr c bl = mkCLambdaN ?loc:(local_binders_loc bl) bl c +let prod_constr_expr c bl = mkCProdN ?loc:(local_binders_loc bl) bl c diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 7bd275e51..3ecb3d321 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -56,11 +56,11 @@ val mkCProdN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_exp (** @deprecated variant of mkCLambdaN *) val abstract_constr_expr : constr_expr -> local_binder_expr list -> constr_expr +[@@ocaml.deprecated "deprecated variant of mkCLambdaN"] (** @deprecated variant of mkCProdN *) val prod_constr_expr : constr_expr -> local_binder_expr list -> constr_expr - -val fresh_var_hook : (Names.Id.t list -> Constrexpr.constr_expr -> Names.Id.t) Hook.t +[@@ocaml.deprecated "deprecated variant of mkCProdN"] (** {6 Destructors}*) @@ -83,3 +83,36 @@ val names_of_local_binders : local_binder_expr list -> Name.t located list val names_of_local_assums : local_binder_expr list -> Name.t located list (** Same as [names_of_local_binder_exprs], but does not take the [let] bindings into account. *) + +(** { 6 Folds and maps } *) + +(** Used in typeclasses *) +val fold_constr_expr_with_binders : (Id.t -> 'a -> 'a) -> + ('a -> 'b -> constr_expr -> 'b) -> 'a -> 'b -> constr_expr -> 'b + +(** Used in correctness and interface; absence of var capture not guaranteed + in pattern-matching clauses and in binders of the form [x,y:T(x)] *) + +val map_constr_expr_with_binders : + (Id.t -> 'a -> 'a) -> ('a -> constr_expr -> constr_expr) -> + 'a -> constr_expr -> constr_expr + +val replace_vars_constr_expr : + Id.t Id.Map.t -> constr_expr -> constr_expr + +(** Specific function for interning "in indtype" syntax of "match" *) +val ids_of_cases_indtype : cases_pattern_expr -> Id.Set.t + +val free_vars_of_constr_expr : constr_expr -> Id.Set.t +val occur_var_constr_expr : Id.t -> constr_expr -> bool + +val split_at_annot : local_binder_expr list -> Id.t located option -> local_binder_expr list * local_binder_expr list + +val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> string -> (int * int) list +val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> string -> (int * int) list + +(** For cases pattern parsing errors *) +val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a + +(** Placeholder for global option, should be moved to a parameter *) +val asymmetric_patterns : bool ref diff --git a/interp/constrextern.ml b/interp/constrextern.ml index e1cf8f196..e1df24f71 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -21,7 +21,6 @@ open CAst open Constrexpr open Constrexpr_ops open Notation_ops -open Topconstr open Glob_term open Glob_ops open Pattern @@ -185,18 +184,8 @@ let with_universes f = Flags.with_option print_universes f let with_meta_as_hole f = Flags.with_option print_meta_as_hole f let without_symbols f = Flags.with_option print_no_symbol f -(* XXX: Where to put this in the library? Util maybe? *) -let protect_ref r nf f x = - let old_ref = !r in - r := nf !r; - try let res = f x in r := old_ref; res - with reraise -> - let reraise = Backtrace.add_backtrace reraise in - r := old_ref; - Exninfo.iraise reraise - let without_specific_symbols l = - protect_ref inactive_notations_table + Flags.with_modified_ref inactive_notations_table (fun tbl -> IRuleSet.(union (of_list l) tbl)) (**********************************************************************) @@ -424,7 +413,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = with Not_found | No_match | Exit -> let c = extern_reference ?loc Id.Set.empty (ConstructRef cstrsp) in - if !Topconstr.asymmetric_patterns then + if !asymmetric_patterns then if pattern_printable_in_both_syntax cstrsp then CPatCstr (c, None, args) else CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), []) @@ -456,7 +445,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) List.map (extern_cases_pattern_in_scope subscope vars) c) substlist in let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in - let l2' = if !Topconstr.asymmetric_patterns || not (List.is_empty ll) then l2 + let l2' = if !asymmetric_patterns || not (List.is_empty ll) then l2 else match drop_implicits_in_patt gr nb_to_drop l2 with |Some true_args -> true_args @@ -472,7 +461,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) extern_cases_pattern_in_scope (scopt,scl@scopes) vars c) subst in let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in - let l2' = if !Topconstr.asymmetric_patterns then l2 + let l2' = if !asymmetric_patterns then l2 else match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with |Some true_args -> true_args diff --git a/interp/constrextern.mli b/interp/constrextern.mli index d980b1995..51b06580e 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -60,6 +60,19 @@ val set_extern_reference : val get_extern_reference : unit -> (?loc:Loc.t -> Id.Set.t -> global_reference -> reference) +(** WARNING: The following functions are evil due to + side-effects. Think of the following case as used in the printer: + + without_specific_symbols [SynDefRule kn] (pr_glob_constr_env env) c + + vs + + without_specific_symbols [SynDefRule kn] pr_glob_constr_env env c + + which one is wrong? We should turn this kind of state into an + explicit argument. +*) + (** This forces printing universe names of Type\{.\} *) val with_universes : ('a -> 'b) -> 'a -> 'b diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c4e0ac500..977146b2f 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -24,7 +24,6 @@ open Constrexpr open Constrexpr_ops open Notation_term open Notation_ops -open Topconstr open Nametab open Notation open Inductiveops @@ -534,8 +533,9 @@ let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function | Name id -> try (* Binders bound in the notation are considered first-order objects *) - let _,na = coerce_to_name (fst (Id.Map.find id terms)) in - (renaming,{env with ids = Name.fold_right Id.Set.add na env.ids}), na + let _,na as locna = coerce_to_name (fst (Id.Map.find id terms)) in + let env = push_name_env Id.Map.empty (Variable,[],[],[]) env locna in + (renaming,env), na with Not_found -> (* Binders not bound in the notation do not capture variables *) (* outside the notation (i.e. in the substitution) *) @@ -747,7 +747,14 @@ let gvar (loc, id) us = match us with str " cannot have a universe instance") let intern_var genv (ltacvars,ntnvars) namedctx loc id us = - (* Is [id] an inductive type potentially with implicit *) + (* Is [id] a notation variable *) + if Id.Map.mem id ntnvars then + begin + if not (Id.Map.mem id genv.impls) then set_var_scope ?loc id true genv ntnvars; + gvar (loc,id) us, [], [], [] + end + else + (* Is [id] registered with implicit arguments *) try let ty,expl_impls,impls,argsc = Id.Map.find id genv.impls in let expl_impls = List.map @@ -760,12 +767,8 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id us = if Id.Set.mem id genv.ids || Id.Set.mem id ltacvars.ltac_vars then gvar (loc,id) us, [], [], [] - (* Is [id] a notation variable *) - else if Id.Map.mem id ntnvars - then - (set_var_scope ?loc id true genv ntnvars; gvar (loc,id) us, [], [], []) - (* Is [id] the special variable for recursive notations *) else if Id.equal id ldots_var + (* Is [id] the special variable for recursive notations? *) then if Id.Map.is_empty ntnvars then error_ldots_var ?loc else gvar (loc,id) us, [], [], [] diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index a5302b54d..519f2480b 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -94,8 +94,8 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = let rec aux bdvars l c = match CAst.(c.v) with | CRef (Ident (loc,id),_) -> found loc id bdvars l | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef (Ident (_, id),_) } :: _, [], [])) when not (Id.Set.mem id bdvars) -> - Topconstr.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l c - | _ -> Topconstr.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c + Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l c + | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c in aux bound l c let ids_of_names l = diff --git a/interp/interp.mllib b/interp/interp.mllib index e3500cfea..bb22cf468 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -1,13 +1,13 @@ Tactypes Stdarg Genintern -Constrexpr_ops Notation_ops -Ppextend Notation -Dumpglob Syntax_def Smartlocate +Constrexpr_ops +Ppextend +Dumpglob Topconstr Reserve Impargs diff --git a/interp/topconstr.ml b/interp/topconstr.ml index c64d3aa26..ecfb766ff 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -6,294 +6,16 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i*) -open Pp -open CErrors -open Util -open Names -open Nameops -open Libnames -open Misctypes -open Constrexpr open Constrexpr_ops -(*i*) - -let asymmetric_patterns = ref (false) -let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; - Goptions.optname = "no parameters in constructors"; - Goptions.optkey = ["Asymmetric";"Patterns"]; - Goptions.optread = (fun () -> !asymmetric_patterns); - Goptions.optwrite = (fun a -> asymmetric_patterns:=a); -} - -(**********************************************************************) -(* Miscellaneous *) - -let error_invalid_pattern_notation ?loc () = - user_err ?loc (str "Invalid notation for pattern.") - -(* Legacy functions *) -let down_located f (_l, x) = f x -let located_fold_left f x (_l, y) = f x y - -(**********************************************************************) -(* Functions on constr_expr *) - -let is_constructor id = - try Globnames.isConstructRef - (Smartlocate.global_of_extended_global - (Nametab.locate_extended (qualid_of_ident id))) - with Not_found -> false - -let rec cases_pattern_fold_names f a pt = match CAst.(pt.v) with - | CPatRecord l -> - List.fold_left (fun acc (r, cp) -> cases_pattern_fold_names f acc cp) a l - | CPatAlias (pat,id) -> f id a - | CPatOr (patl) -> - List.fold_left (cases_pattern_fold_names f) a patl - | CPatCstr (_,patl1,patl2) -> - List.fold_left (cases_pattern_fold_names f) - (Option.fold_left (List.fold_left (cases_pattern_fold_names f)) a patl1) patl2 - | CPatNotation (_,(patl,patll),patl') -> - List.fold_left (cases_pattern_fold_names f) - (List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)) patl' - | CPatDelimiters (_,pat) -> cases_pattern_fold_names f a pat - | CPatAtom (Some (Ident (_,id))) when not (is_constructor id) -> f id a - | CPatPrim _ | CPatAtom _ -> a - | CPatCast ({CAst.loc},_) -> - CErrors.user_err ?loc ~hdr:"cases_pattern_fold_names" - (Pp.strbrk "Casts are not supported here.") - -let ids_of_pattern = - cases_pattern_fold_names Id.Set.add Id.Set.empty - -let ids_of_pattern_list = - List.fold_left - (located_fold_left - (List.fold_left (cases_pattern_fold_names Id.Set.add))) - Id.Set.empty - -let ids_of_cases_indtype p = - cases_pattern_fold_names Id.Set.add Id.Set.empty p - -let ids_of_cases_tomatch tms = - List.fold_right - (fun (_, ona, indnal) l -> - Option.fold_right (fun t ids -> cases_pattern_fold_names Id.Set.add ids t) - indnal - (Option.fold_right (down_located (Name.fold_right Id.Set.add)) ona l)) - tms Id.Set.empty - -let rec fold_constr_expr_binders g f n acc b = function - | (nal,bk,t)::l -> - let nal = snd (List.split nal) in - let n' = List.fold_right (Name.fold_right g) nal n in - f n (fold_constr_expr_binders g f n' acc b l) t - | [] -> - f n acc b - -let rec fold_local_binders g f n acc b = function - | CLocalAssum (nal,bk,t)::l -> - let nal = snd (List.split nal) in - let n' = List.fold_right (Name.fold_right g) nal n in - f n (fold_local_binders g f n' acc b l) t - | CLocalDef ((_,na),c,t)::l -> - Option.fold_left (f n) (f n (fold_local_binders g f (Name.fold_right g na n) acc b l) c) t - | CLocalPattern (_,(pat,t))::l -> - let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in - Option.fold_left (f n) acc t - | [] -> - f n acc b - -let fold_constr_expr_with_binders g f n acc = CAst.with_val (function - | CAppExpl ((_,_,_),l) -> List.fold_left (f n) acc l - | CApp ((_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l) - | CProdN (l,b) | CLambdaN (l,b) -> fold_constr_expr_binders g f n acc b l - | CLetIn (na,a,t,b) -> - f (Name.fold_right g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b - | CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b - | CCast (a,CastCoerce) -> f n acc a - | CNotation (_,(l,ll,bll)) -> - (* The following is an approximation: we don't know exactly if - an ident is binding nor to which subterms bindings apply *) - let acc = List.fold_left (f n) acc (l@List.flatten ll) in - List.fold_left (fun acc bl -> fold_local_binders g f n acc (CAst.make @@ CHole (None,IntroAnonymous,None)) bl) acc bll - | CGeneralization (_,_,c) -> f n acc c - | CDelimiters (_,a) -> f n acc a - | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CRef _ -> - acc - | CRecord l -> List.fold_left (fun acc (id, c) -> f n acc c) acc l - | CCases (sty,rtnpo,al,bl) -> - let ids = ids_of_cases_tomatch al in - let acc = Option.fold_left (f (Id.Set.fold g ids n)) acc rtnpo in - let acc = List.fold_left (f n) acc (List.map (fun (fst,_,_) -> fst) al) in - List.fold_right (fun (loc,(patl,rhs)) acc -> - let ids = ids_of_pattern_list patl in - f (Id.Set.fold g ids n) acc rhs) bl acc - | CLetTuple (nal,(ona,po),b,c) -> - let n' = List.fold_right (down_located (Name.fold_right g)) nal n in - f (Option.fold_right (down_located (Name.fold_right g)) ona n') (f n acc b) c - | CIf (c,(ona,po),b1,b2) -> - let acc = f n (f n (f n acc b1) b2) c in - Option.fold_left - (f (Option.fold_right (down_located (Name.fold_right g)) ona n)) acc po - | CFix (_,l) -> - let n' = List.fold_right (fun ((_,id),_,_,_,_) -> g id) l n in - List.fold_right (fun (_,(_,o),lb,t,c) acc -> - fold_local_binders g f n' - (fold_local_binders g f n acc t lb) c lb) l acc - | CCoFix (_,_) -> - Feedback.msg_warning (strbrk "Capture check in multiple binders not done"); acc - ) - -let free_vars_of_constr_expr c = - let rec aux bdvars l = function - | { CAst.v = CRef (Ident (_,id),_) } -> if Id.List.mem id bdvars then l else Id.Set.add id l - | c -> fold_constr_expr_with_binders (fun a l -> a::l) aux bdvars l c - in aux [] Id.Set.empty c - -let occur_var_constr_expr id c = Id.Set.mem id (free_vars_of_constr_expr c) - -(* Interpret the index of a recursion order annotation *) - -let split_at_annot bl na = - let names = List.map snd (names_of_local_assums bl) in - match na with - | None -> - begin match names with - | [] -> user_err (Pp.str "A fixpoint needs at least one parameter.") - | _ -> ([], bl) - end - | Some (loc, id) -> - let rec aux acc = function - | CLocalAssum (bls, k, t) as x :: rest -> - let test (_, na) = match na with - | Name id' -> Id.equal id id' - | Anonymous -> false - in - let l, r = List.split_when test bls in - begin match r with - | [] -> aux (x :: acc) rest - | _ -> - let ans = match l with - | [] -> acc - | _ -> CLocalAssum (l, k, t) :: acc - in - (List.rev ans, CLocalAssum (r, k, t) :: rest) - end - | CLocalDef ((_,na),_,_) as x :: rest -> - if Name.equal (Name id) na then - user_err ?loc - (Id.print id ++ str" must be a proper parameter and not a local definition.") - else - aux (x :: acc) rest - | CLocalPattern (_,_) :: rest -> - Loc.raise ?loc (Stream.Error "pattern with quote not allowed after fix") - | [] -> - user_err ?loc - (str "No parameter named " ++ Id.print id ++ str".") - in aux [] bl - -(* Used in correctness and interface *) - -let map_binder g e nal = List.fold_right (down_located (Name.fold_right g)) nal e - -let map_binders f g e bl = - (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *) - let h (e,bl) (nal,bk,t) = (map_binder g e nal,(nal,bk,f e t)::bl) in - let (e,rbl) = List.fold_left h (e,[]) bl in - (e, List.rev rbl) - -let map_local_binders f g e bl = - (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *) - let h (e,bl) = function - CLocalAssum(nal,k,ty) -> - (map_binder g e nal, CLocalAssum(nal,k,f e ty)::bl) - | CLocalDef((loc,na),c,ty) -> - (Name.fold_right g na e, CLocalDef((loc,na),f e c,Option.map (f e) ty)::bl) - | CLocalPattern (loc,(pat,t)) -> - let ids = ids_of_pattern pat in - (Id.Set.fold g ids e, CLocalPattern (loc,(pat,Option.map (f e) t))::bl) in - let (e,rbl) = List.fold_left h (e,[]) bl in - (e, List.rev rbl) - -let map_constr_expr_with_binders g f e = CAst.map (function - | CAppExpl (r,l) -> CAppExpl (r,List.map (f e) l) - | CApp ((p,a),l) -> - CApp ((p,f e a),List.map (fun (a,i) -> (f e a,i)) l) - | CProdN (bl,b) -> - let (e,bl) = map_binders f g e bl in CProdN (bl,f e b) - | CLambdaN (bl,b) -> - let (e,bl) = map_binders f g e bl in CLambdaN (bl,f e b) - | CLetIn (na,a,t,b) -> - CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (snd na) e) b) - | CCast (a,c) -> CCast (f e a, Miscops.map_cast_type (f e) c) - | CNotation (n,(l,ll,bll)) -> - (* This is an approximation because we don't know what binds what *) - CNotation (n,(List.map (f e) l,List.map (List.map (f e)) ll, - List.map (fun bl -> snd (map_local_binders f g e bl)) bll)) - | CGeneralization (b,a,c) -> CGeneralization (b,a,f e c) - | CDelimiters (s,a) -> CDelimiters (s,f e a) - | CHole _ | CEvar _ | CPatVar _ | CSort _ - | CPrim _ | CRef _ as x -> x - | CRecord l -> CRecord (List.map (fun (id, c) -> (id, f e c)) l) - | CCases (sty,rtnpo,a,bl) -> - let bl = List.map (fun (loc,(patl,rhs)) -> - let ids = ids_of_pattern_list patl in - (loc,(patl,f (Id.Set.fold g ids e) rhs))) bl in - let ids = ids_of_cases_tomatch a in - let po = Option.map (f (Id.Set.fold g ids e)) rtnpo in - CCases (sty, po, List.map (fun (tm,x,y) -> f e tm,x,y) a,bl) - | CLetTuple (nal,(ona,po),b,c) -> - let e' = List.fold_right (down_located (Name.fold_right g)) nal e in - let e'' = Option.fold_right (down_located (Name.fold_right g)) ona e in - CLetTuple (nal,(ona,Option.map (f e'') po),f e b,f e' c) - | CIf (c,(ona,po),b1,b2) -> - let e' = Option.fold_right (down_located (Name.fold_right g)) ona e in - CIf (f e c,(ona,Option.map (f e') po),f e b1,f e b2) - | CFix (id,dl) -> - CFix (id,List.map (fun (id,n,bl,t,d) -> - let (e',bl') = map_local_binders f g e bl in - let t' = f e' t in - (* Note: fix names should be inserted before the arguments... *) - let e'' = List.fold_left (fun e ((_,id),_,_,_,_) -> g id e) e' dl in - let d' = f e'' d in - (id,n,bl',t',d')) dl) - | CCoFix (id,dl) -> - CCoFix (id,List.map (fun (id,bl,t,d) -> - let (e',bl') = map_local_binders f g e bl in - let t' = f e' t in - let e'' = List.fold_left (fun e ((_,id),_,_,_) -> g id e) e' dl in - let d' = f e'' d in - (id,bl',t',d')) dl) - ) - -(* Used in constrintern *) -let rec replace_vars_constr_expr l = function - | { CAst.loc; v = CRef (Ident (loc_id,id),us) } as x -> - (try CAst.make ?loc @@ CRef (Ident (loc_id,Id.Map.find id l),us) with Not_found -> x) - | c -> map_constr_expr_with_binders Id.Map.remove - replace_vars_constr_expr l c - -(* Returns the ranges of locs of the notation that are not occupied by args *) -(* and which are then occupied by proper symbols of the notation (or spaces) *) - -let locs_of_notation ?loc locs ntn = - let unloc loc = Option.cata Loc.unloc (0,0) loc in - let (bl, el) = unloc loc in - let locs = List.map unloc locs in - let rec aux pos = function - | [] -> if Int.equal pos el then [] else [(pos,el)] - | (ba,ea)::l -> if Int.equal pos ba then aux ea l else (pos,ba)::aux ea l - in aux bl (List.sort (fun l1 l2 -> fst l1 - fst l2) locs) - -let ntn_loc ?loc (args,argslist,binderslist) = - locs_of_notation ?loc - (List.map constr_loc (args@List.flatten argslist)@ - List.map local_binders_loc binderslist) - -let patntn_loc ?loc (args,argslist) = - locs_of_notation ?loc - (List.map cases_pattern_expr_loc (args@List.flatten argslist)) +let asymmetric_patterns = asymmetric_patterns +let error_invalid_pattern_notation = error_invalid_pattern_notation +let split_at_annot = split_at_annot +let ntn_loc = ntn_loc +let patntn_loc = patntn_loc +let map_constr_expr_with_binders = map_constr_expr_with_binders +let fold_constr_expr_with_binders = fold_constr_expr_with_binders +let ids_of_cases_indtype = ids_of_cases_indtype +let occur_var_constr_expr = occur_var_constr_expr +let free_vars_of_constr_expr = free_vars_of_constr_expr +let replace_vars_constr_expr = replace_vars_constr_expr diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 922f87955..9fc02461e 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -10,40 +10,43 @@ open Loc open Names open Constrexpr -(** Topconstr *) - +(** Topconstr: This whole module is deprecated in favor of Constrexpr_ops *) val asymmetric_patterns : bool ref +[@@ocaml.deprecated "use Constrexpr_ops.asymmetric_patterns"] (** Utilities on constr_expr *) +val split_at_annot : local_binder_expr list -> Id.t located option -> local_binder_expr list * local_binder_expr list +[@@ocaml.deprecated "use Constrexpr_ops.split_at_annot"] + +val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> string -> (int * int) list +[@@ocaml.deprecated "use Constrexpr_ops.ntn_loc"] +val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> string -> (int * int) list +[@@ocaml.deprecated "use Constrexpr_ops.patntn_loc"] + +(** For cases pattern parsing errors *) +val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a +[@@ocaml.deprecated "use Constrexpr_ops.error_invalid_pattern_notation"] -val replace_vars_constr_expr : - Id.t Id.Map.t -> constr_expr -> constr_expr +(*************************************************************************) +val replace_vars_constr_expr : Id.t Id.Map.t -> constr_expr -> constr_expr +[@@ocaml.deprecated "use Constrexpr_ops.free_vars_of_constr_expr"] val free_vars_of_constr_expr : constr_expr -> Id.Set.t +[@@ocaml.deprecated "use Constrexpr_ops.free_vars_of_constr_expr"] + val occur_var_constr_expr : Id.t -> constr_expr -> bool +[@@ocaml.deprecated "use Constrexpr_ops.occur_var_constr_expr"] (** Specific function for interning "in indtype" syntax of "match" *) val ids_of_cases_indtype : cases_pattern_expr -> Id.Set.t - -val split_at_annot : local_binder_expr list -> Id.t located option -> local_binder_expr list * local_binder_expr list +[@@ocaml.deprecated "use Constrexpr_ops.ids_of_cases_indtype"] (** Used in typeclasses *) - val fold_constr_expr_with_binders : (Id.t -> 'a -> 'a) -> ('a -> 'b -> constr_expr -> 'b) -> 'a -> 'b -> constr_expr -> 'b - -(** Used in correctness and interface; absence of var capture not guaranteed - in pattern-matching clauses and in binders of the form [x,y:T(x)] *) +[@@ocaml.deprecated "use Constrexpr_ops.fold_constr_expr_with_binders"] val map_constr_expr_with_binders : (Id.t -> 'a -> 'a) -> ('a -> constr_expr -> constr_expr) -> 'a -> constr_expr -> constr_expr - -val ntn_loc : - ?loc:Loc.t -> constr_notation_substitution -> string -> (int * int) list -val patntn_loc : - ?loc:Loc.t -> cases_pattern_notation_substitution -> string -> (int * int) list - -(** For cases pattern parsing errors *) - -val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a +[@@ocaml.deprecated "use Constrexpr_ops.map_constr_expr_with_binders"] diff --git a/lib/flags.ml b/lib/flags.ml index 323b5492d..ddc8f8482 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -6,13 +6,17 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -let with_option o f x = - let old = !o in o:=true; - try let r = f x in if !o = true then o := old; r - with reraise -> - let reraise = Backtrace.add_backtrace reraise in - let () = o := old in - Exninfo.iraise reraise +let with_modified_ref r nf f x = + let old_ref = !r in r := nf !r; + try let res = f x in r := old_ref; res + with reraise -> + let reraise = Backtrace.add_backtrace reraise in + r := old_ref; + Exninfo.iraise reraise + +let with_option o f x = with_modified_ref o (fun _ -> true) f x +let without_option o f x = with_modified_ref o (fun _ -> false) f x +let with_extra_values o l f x = with_modified_ref o (fun ol -> ol@l) f x let with_options ol f x = let vl = List.map (!) ol in @@ -25,22 +29,6 @@ let with_options ol f x = let () = List.iter2 (:=) ol vl in Exninfo.iraise reraise -let without_option o f x = - let old = !o in o:=false; - try let r = f x in if !o = false then o := old; r - with reraise -> - let reraise = Backtrace.add_backtrace reraise in - let () = o := old in - Exninfo.iraise reraise - -let with_extra_values o l f x = - let old = !o in o:=old@l; - try let r = f x in o := old; r - with reraise -> - let reraise = Backtrace.add_backtrace reraise in - let () = o := old in - Exninfo.iraise reraise - let boot = ref false let record_aux_file = ref false diff --git a/lib/flags.mli b/lib/flags.mli index 0ff3e0a81..c4afb8318 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -110,6 +110,15 @@ val warn : bool ref val make_warn : bool -> unit val if_warn : ('a -> unit) -> 'a -> unit +(** [with_modified_ref r nf f x] Temporarily modify a reference in the + call to [f x] . Be very careful with these functions, it is very + easy to fall in the typical problem with effects: + + with_modified_ref r nf f x y != with_modified_ref r nf (f x) y + +*) +val with_modified_ref : 'c ref -> ('c -> 'c) -> ('a -> 'b) -> 'a -> 'b + (** Temporarily activate an option (to activate option [o] on [f x y z], use [with_option o (f x y) z]) *) val with_option : bool ref -> ('a -> 'b) -> 'a -> 'b diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index d51b8b54e..7f50fd22a 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -440,7 +440,7 @@ let make_act : type r. r target -> _ -> r gen_eval = function CAst.make ~loc @@ CNotation (notation , env) | ForPattern -> fun notation loc env -> let invalid = List.exists (fun (_, b) -> not b) env.binders in - let () = if invalid then Topconstr.error_invalid_pattern_notation ~loc () in + let () = if invalid then Constrexpr_ops.error_invalid_pattern_notation ~loc () in let env = (env.constrs, env.constrlists) in CAst.make ~loc @@ CPatNotation (notation, env, []) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index a5b58b855..82306bb9f 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -129,12 +129,6 @@ let test_plural_form_types loc kwd = function warn_plural_command ~loc:!@loc kwd | _ -> () -let fresh_var env c = - Namegen.next_ident_away (Id.of_string "pat") - (List.fold_left (fun accu id -> Id.Set.add id accu) (Topconstr.free_vars_of_constr_expr c) env) - -let _ = Hook.set Constrexpr_ops.fresh_var_hook fresh_var - (* Gallina declarations *) GEXTEND Gram GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index da8955f0d..a09abfa19 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -200,7 +200,8 @@ module Btauto = struct let assign = List.combine env var in let map_msg (key, v) = let b = if v then str "true" else str "false" in - let term = Printer.pr_constr key in + let sigma, env = Pfedit.get_current_context () in + let term = Printer.pr_constr_env env sigma key in term ++ spc () ++ str ":=" ++ spc () ++ b in let assign = List.map map_msg assign in diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index bd5fb1d92..29e824f44 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -44,6 +44,10 @@ let observe_tac s tac g = observe_tac_stream (str s) tac g *) +let pr_leconstr_fp = + let sigma, env = Pfedit.get_current_context () in + Printer.pr_leconstr_env env sigma + let debug_queue = Stack.create () let rec print_debug_queue e = @@ -172,7 +176,7 @@ let is_incompatible_eq sigma t = | _ -> false with e when CErrors.noncritical e -> false in - if res then observe (str "is_incompatible_eq " ++ Printer.pr_leconstr t); + if res then observe (str "is_incompatible_eq " ++ pr_leconstr_fp t); res let change_hyp_with_using msg hyp_id t tac : tactic = @@ -220,7 +224,8 @@ let find_rectype env sigma c = let isAppConstruct ?(env=Global.env ()) sigma t = try let t',l = find_rectype env sigma t in - observe (str "isAppConstruct : " ++ Printer.pr_leconstr t ++ str " -> " ++ Printer.pr_leconstr (applist (t',l))); + observe (str "isAppConstruct : " ++ Printer.pr_leconstr_env env sigma t ++ str " -> " ++ + Printer.pr_leconstr_env env sigma (applist (t',l))); true with Not_found -> false @@ -233,7 +238,8 @@ exception NoChange let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = let nochange ?t' msg = begin - observe (str ("Not treating ( "^msg^" )") ++ pr_leconstr t ++ str " " ++ match t' with None -> str "" | Some t -> Printer.pr_leconstr t ); + observe (str ("Not treating ( "^msg^" )") ++ pr_leconstr_env env sigma t ++ str " " ++ + match t' with None -> str "" | Some t -> Printer.pr_leconstr_env env sigma t ); raise NoChange; end in @@ -841,7 +847,7 @@ let build_proof | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!") and build_proof do_finalize dyn_infos g = (* observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *) - observe_tac_stream (str "build_proof with " ++ Printer.pr_leconstr dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g + observe_tac_stream (str "build_proof with " ++ pr_leconstr_fp dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g and build_proof_args do_finalize dyn_infos (* f_args' args *) :tactic = fun g -> let (f_args',args) = dyn_infos.info in @@ -1135,7 +1141,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam princ_params ); observe (str "fbody_with_full_params := " ++ - pr_leconstr fbody_with_full_params + pr_leconstr_env (Global.env ()) !evd fbody_with_full_params ); let all_funs_with_full_params = Array.map (fun f -> applist(f, List.rev_map var_of_decl full_params)) all_funs diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 722dbc16b..3899bc709 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -115,7 +115,9 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let dummy_var = mkVar (Id.of_string "________") in let mk_replacement c i args = let res = mkApp(rel_to_fun.(i), Array.map pop (array_get_start args)) in - observe (str "replacing " ++ pr_lconstr c ++ str " by " ++ pr_lconstr res); + observe (str "replacing " ++ + pr_lconstr_env env Evd.empty c ++ str " by " ++ + pr_lconstr_env env Evd.empty res); res in let rec compute_new_princ_type remove env pre_princ : types*(constr list) = @@ -565,7 +567,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ List.map (* we can now compute the other principles *) (fun scheme_type -> incr i; - observe (Printer.pr_lconstr scheme_type); + observe (Printer.pr_lconstr_env env sigma scheme_type); let type_concl = (strip_prod_assum scheme_type) in let applied_f = List.hd (List.rev (snd (decompose_app type_concl))) in let f = fst (decompose_app applied_f) in @@ -577,8 +579,8 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ let g = fst (decompose_app applied_g) in if Constr.equal f g then raise (Found_type j); - observe (Printer.pr_lconstr f ++ str " <> " ++ - Printer.pr_lconstr g) + observe (Printer.pr_lconstr_env env sigma f ++ str " <> " ++ + Printer.pr_lconstr_env env sigma g) ) ta; diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 8ab6dbcdf..d04b7a33d 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -379,29 +379,30 @@ let add_pat_variables pat typ env : Environ.env = fst ( Context.Rel.fold_outside (fun decl (env,ctxt) -> - let open Context.Rel.Declaration in - match decl with + let open Context.Rel.Declaration in + let sigma, _ = Pfedit.get_current_context () in + match decl with | LocalAssum (Anonymous,_) | LocalDef (Anonymous,_,_) -> assert false | LocalAssum (Name id, t) -> - let new_t = substl ctxt t in - observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ - str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++ - str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () - ); - let open Context.Named.Declaration in - (Environ.push_named (LocalAssum (id,new_t)) env,mkVar id::ctxt) - | LocalDef (Name id, v, t) -> - let new_t = substl ctxt t in - let new_v = substl ctxt v in - observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ - str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++ - str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () ++ - str "old value := " ++ Printer.pr_lconstr v ++ fnl () ++ - str "new value := " ++ Printer.pr_lconstr new_v ++ fnl () - ); - let open Context.Named.Declaration in - (Environ.push_named (LocalDef (id,new_v,new_t)) env,mkVar id::ctxt) - ) + let new_t = substl ctxt t in + observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ + str "old type := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++ + str "new type := " ++ Printer.pr_lconstr_env env sigma new_t ++ fnl () + ); + let open Context.Named.Declaration in + (Environ.push_named (LocalAssum (id,new_t)) env,mkVar id::ctxt) + | LocalDef (Name id, v, t) -> + let new_t = substl ctxt t in + let new_v = substl ctxt v in + observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ + str "old type := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++ + str "new type := " ++ Printer.pr_lconstr_env env sigma new_t ++ fnl () ++ + str "old value := " ++ Printer.pr_lconstr_env env sigma v ++ fnl () ++ + str "new value := " ++ Printer.pr_lconstr_env env sigma new_v ++ fnl () + ); + let open Context.Named.Declaration in + (Environ.push_named (LocalDef (id,new_v,new_t)) env,mkVar id::ctxt) + ) (Environ.rel_context new_env) ~init:(env,[]) ) @@ -479,7 +480,7 @@ let rec pattern_to_term_and_type env typ = DAst.with_val (function let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = - observe (str " Entering : " ++ Printer.pr_glob_constr rt); + observe (str " Entering : " ++ Printer.pr_glob_constr_env env rt); let open CAst in match DAst.get rt with | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> @@ -652,8 +653,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> user_err (str "Cannot find the inductive associated to " ++ - Printer.pr_glob_constr b ++ str " in " ++ - Printer.pr_glob_constr rt ++ str ". try again with a cast") + Printer.pr_glob_constr_env env b ++ str " in " ++ + Printer.pr_glob_constr_env env rt ++ str ". try again with a cast") in let case_pats = build_constructors_of_type (fst ind) [] in assert (Int.equal (Array.length case_pats) 2); @@ -684,8 +685,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> user_err (str "Cannot find the inductive associated to " ++ - Printer.pr_glob_constr b ++ str " in " ++ - Printer.pr_glob_constr rt ++ str ". try again with a cast") + Printer.pr_glob_constr_env env b ++ str " in " ++ + Printer.pr_glob_constr_env env rt ++ str ". try again with a cast") in let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in assert (Int.equal (Array.length case_pats) 1); @@ -897,24 +898,24 @@ let same_raw_term rt1 rt2 = | GHole _, GHole _ -> true | _ -> false let decompose_raw_eq lhs rhs = - let rec decompose_raw_eq lhs rhs acc = - observe (str "decomposing eq for " ++ pr_glob_constr lhs ++ str " " ++ pr_glob_constr rhs); - let (rhd,lrhs) = glob_decompose_app rhs in - let (lhd,llhs) = glob_decompose_app lhs in - observe (str "lhd := " ++ pr_glob_constr lhd); - observe (str "rhd := " ++ pr_glob_constr rhd); + let _, env = Pfedit.get_current_context () in + let rec decompose_raw_eq lhs rhs acc = + observe (str "decomposing eq for " ++ pr_glob_constr_env env lhs ++ str " " ++ pr_glob_constr_env env rhs); + let (rhd,lrhs) = glob_decompose_app rhs in + let (lhd,llhs) = glob_decompose_app lhs in + observe (str "lhd := " ++ pr_glob_constr_env env lhd); + observe (str "rhd := " ++ pr_glob_constr_env env rhd); observe (str "llhs := " ++ int (List.length llhs)); observe (str "lrhs := " ++ int (List.length lrhs)); - let sllhs = List.length llhs in - let slrhs = List.length lrhs in - if same_raw_term lhd rhd && Int.equal sllhs slrhs + let sllhs = List.length llhs in + let slrhs = List.length lrhs in + if same_raw_term lhd rhd && Int.equal sllhs slrhs then (* let _ = assert false in *) List.fold_right2 decompose_raw_eq llhs lrhs acc else (lhs,rhs)::acc in decompose_raw_eq lhs rhs [] - exception Continue (* @@ -923,7 +924,7 @@ exception Continue eliminates some meaningless equalities, applies some rewrites...... *) let rec rebuild_cons env nb_args relname args crossed_types depth rt = - observe (str "rebuilding : " ++ pr_glob_constr rt); + observe (str "rebuilding : " ++ pr_glob_constr_env env rt); let open Context.Rel.Declaration in let open CAst in match DAst.get rt with @@ -967,7 +968,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let id = match DAst.get id with GVar id -> id | _ -> assert false in begin try - observe (str "computing new type for eq : " ++ pr_glob_constr rt); + observe (str "computing new type for eq : " ++ pr_glob_constr_env env rt); let t' = try fst (Pretyping.understand env (Evd.from_env env) t)(*FIXME*) with e when CErrors.noncritical e -> raise Continue @@ -1012,7 +1013,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let eq' = DAst.make ?loc:loc1 @@ GApp(DAst.make ?loc:loc2 @@GRef(jmeq,None),[ty;DAst.make ?loc:loc3 @@ GVar id;rt_typ;rt]) in - observe (str "computing new type for jmeq : " ++ pr_glob_constr eq'); + observe (str "computing new type for jmeq : " ++ pr_glob_constr_env env eq'); let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in observe (str " computing new type for jmeq : done") ; let new_args = @@ -1099,7 +1100,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = rebuild_cons env nb_args relname args crossed_types depth new_rt else raise Continue with Continue -> - observe (str "computing new type for prod : " ++ pr_glob_constr rt); + observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt); let t',ctx = Pretyping.understand env (Evd.from_env env) t in let new_env = Environ.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = @@ -1115,7 +1116,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude end | _ -> - observe (str "computing new type for prod : " ++ pr_glob_constr rt); + observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt); let t',ctx = Pretyping.understand env (Evd.from_env env) t in let new_env = Environ.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = @@ -1134,7 +1135,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = begin let not_free_in_t id = not (is_free_in id t) in let new_crossed_types = t :: crossed_types in - observe (str "computing new type for lambda : " ++ pr_glob_constr rt); + observe (str "computing new type for lambda : " ++ pr_glob_constr_env env rt); let t',ctx = Pretyping.understand env (Evd.from_env env) t in match n with | Name id -> diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index dab094f91..f01b6669d 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -46,7 +46,7 @@ let functional_induction with_clean c princl pat = try find_Function_infos c' with Not_found -> user_err (str "Cannot find induction information on "++ - Printer.pr_leconstr (mkConst c') ) + Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') ) in match Tacticals.elimination_sort_of_goal g with | InProp -> finfo.prop_lemma @@ -74,7 +74,7 @@ let functional_induction with_clean c princl pat = (* mkConst(const_of_id princ_name ),g (\* FIXME *\) *) with Not_found -> (* This one is neither defined ! *) user_err (str "Cannot find induction principle for " - ++Printer.pr_leconstr (mkConst c') ) + ++ Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') ) in let princ = EConstr.of_constr princ in (princ,NoBindings,Tacmach.pf_unsafe_type_of g' princ,g') @@ -841,12 +841,13 @@ let rec get_args b t : Constrexpr.local_binder_expr list * let make_graph (f_ref:global_reference) = let c,c_body = match f_ref with - | ConstRef c -> - begin try c,Global.lookup_constant c - with Not_found -> - raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr (mkConst c)) ) - end - | _ -> raise (UserError (None, str "Not a function reference") ) + | ConstRef c -> + begin try c,Global.lookup_constant c + with Not_found -> + let sigma, env = Pfedit.get_current_context () in + raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr_env env sigma (mkConst c)) ) + end + | _ -> raise (UserError (None, str "Not a function reference") ) in (match Global.body_of_constant_body c_body with | None -> error "Cannot build a graph over an axiom!" diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index e9102e9c8..8bf6e48fd 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -333,15 +333,17 @@ let discharge_Function (_,finfos) = } let pr_ocst c = - Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) c (mt ()) + let sigma, env = Pfedit.get_current_context () in + Option.fold_right (fun v acc -> Printer.pr_lconstr_env env sigma (mkConst v)) c (mt ()) let pr_info f_info = + let sigma, env = Pfedit.get_current_context () in str "function_constant := " ++ - Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++ + Printer.pr_lconstr_env env sigma (mkConst f_info.function_constant)++ fnl () ++ str "function_constant_type := " ++ (try - Printer.pr_lconstr - (fst (Global.type_of_global_in_context (Global.env ()) (ConstRef f_info.function_constant))) + Printer.pr_lconstr_env env sigma + (fst (Global.type_of_global_in_context env (ConstRef f_info.function_constant))) with e when CErrors.noncritical e -> mt ()) ++ fnl () ++ str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++ str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++ @@ -349,7 +351,7 @@ let pr_info f_info = str "rect_lemma := " ++ pr_ocst f_info.rect_lemma ++ fnl () ++ str "rec_lemma := " ++ pr_ocst f_info.rec_lemma ++ fnl () ++ str "prop_lemma := " ++ pr_ocst f_info.prop_lemma ++ fnl () ++ - str "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl () + str "graph_ind := " ++ Printer.pr_lconstr_env env sigma (mkInd f_info.graph_ind) ++ fnl () let pr_table tb = let l = Cmap_env.fold (fun k v acc -> v::acc) tb [] in @@ -550,11 +552,11 @@ type tcc_lemma_value = | Value of constr | Not_needed -(* We only "purify" on exceptions *) +(* We only "purify" on exceptions. XXX: What is this doing here? *) let funind_purify f x = - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in try f x with e -> let e = CErrors.push e in - Vernacentries.unfreeze_interp_state st; + Vernacstate.unfreeze_interp_state st; Exninfo.iraise e diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 692a874d3..694c80051 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -851,7 +851,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in let type_of_lemma = nf_zeta type_of_lemma in - observe (str "type_of_lemma := " ++ Printer.pr_leconstr type_of_lemma); + observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env env !evd type_of_lemma); type_of_lemma,type_info ) funs_constr diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index b372241d2..9e2774ff3 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -90,20 +90,28 @@ let next_ident_fresh (id:Id.t) = (* comment this line to see debug msgs *) let msg x = () ;; let pr_lconstr c = str "" (* uncomment this to see debugging *) -let prconstr c = msg (str" " ++ Printer.pr_lconstr c) -let prconstrnl c = msg (str" " ++ Printer.pr_lconstr c ++ str"\n") +let prconstr c = + let sigma, env = Pfedit.get_current_context () in + msg (str" " ++ Printer.pr_lconstr_env env sigma c) + +let prconstrnl c = + let sigma, env = Pfedit.get_current_context () in + msg (str" " ++ Printer.pr_lconstr_env env sigma c ++ str"\n") + let prlistconstr lc = List.iter prconstr lc let prstr s = msg(str s) let prNamedConstr s c = + let sigma, env = Pfedit.get_current_context () in begin msg(str ""); - msg(str(s^" {§ ") ++ Printer.pr_lconstr c ++ str " §} "); + msg(str(s^" {§ ") ++ Printer.pr_lconstr_env env sigma c ++ str " §} "); msg(str ""); end let prNamedRConstr s c = + let sigma, env = Pfedit.get_current_context () in begin msg(str ""); - msg(str(s^" {§ ") ++ Printer.pr_glob_constr c ++ str " §} "); + msg(str(s^" {§ ") ++ Printer.pr_glob_constr_env env c ++ str " §} "); msg(str ""); end let prNamedLConstr_aux lc = List.iter (prNamedConstr "\n") lc diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 2fdc3bc37..04d729b10 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -54,6 +54,10 @@ let coq_constant m s = EConstr.of_constr @@ Universes.constr_of_global @@ let arith_Nat = ["Arith";"PeanoNat";"Nat"] let arith_Lt = ["Arith";"Lt"] +let pr_leconstr_rd = + let sigma, env = Pfedit.get_current_context () in + Printer.pr_leconstr_env env sigma + let coq_init_constant s = EConstr.of_constr ( Universes.constr_of_global @@ @@ -337,7 +341,8 @@ let check_not_nested sigma forbidden e = try check_not_nested e with UserError(_,p) -> - user_err ~hdr:"_" (str "on expr : " ++ Printer.pr_leconstr e ++ str " " ++ p) + let _, env = Pfedit.get_current_context () in + user_err ~hdr:"_" (str "on expr : " ++ Printer.pr_leconstr_env env sigma e ++ str " " ++ p) (* ['a info] contains the local information for traveling *) type 'a infos = @@ -455,7 +460,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; jinfo.otherS () expr_info continuation_tac expr_info g with e when CErrors.noncritical e -> - user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) + user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) end | Lambda(n,t,b) -> begin @@ -463,7 +468,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; jinfo.otherS () expr_info continuation_tac expr_info g with e when CErrors.noncritical e -> - user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) + user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) end | Case(ci,t,a,l) -> begin @@ -491,8 +496,8 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = jinfo.apP (f,args) expr_info continuation_tac in travel_args jinfo expr_info.is_main_branch new_continuation_tac new_infos g - | Case _ -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)") - | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr expr_info.info ++ Pp.str ".") + | Case _ -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)") + | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ Pp.str ".") end | Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} g | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ -> @@ -515,7 +520,7 @@ and travel_args jinfo is_final continuation_tac infos = {infos with info=arg;is_final=false} and travel jinfo continuation_tac expr_info = observe_tac - (str jinfo.message ++ Printer.pr_leconstr expr_info.info) + (str jinfo.message ++ pr_leconstr_rd expr_info.info) (travel_aux jinfo continuation_tac expr_info) (* Termination proof *) @@ -731,7 +736,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = let destruct_tac,rev_to_thin_intro = mkDestructEq [expr_info.rec_arg_id] a' g in let to_thin_intro = List.rev rev_to_thin_intro in - observe_tac (str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_leconstr a') + observe_tac (str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_leconstr_env (pf_env g) sigma a') (try (tclTHENS destruct_tac @@ -740,7 +745,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = with | UserError(Some "Refiner.thensn_tac3",_) | UserError(Some "Refiner.tclFAIL_s",_) -> - (observe_tac (str "is computable " ++ Printer.pr_leconstr new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} ) + (observe_tac (str "is computable " ++ Printer.pr_leconstr_env (pf_env g) sigma new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} ) )) g @@ -991,11 +996,11 @@ let rec intros_values_eq expr_info acc = let equation_others _ expr_info continuation_tac infos = if expr_info.is_final && expr_info.is_main_branch then - observe_tac (str "equation_others (cont_tac +intros) " ++ Printer.pr_leconstr expr_info.info) + observe_tac (str "equation_others (cont_tac +intros) " ++ pr_leconstr_rd expr_info.info) (tclTHEN (continuation_tac infos) - (observe_tac (str "intros_values_eq equation_others " ++ Printer.pr_leconstr expr_info.info) (intros_values_eq expr_info []))) - else observe_tac (str "equation_others (cont_tac) " ++ Printer.pr_leconstr expr_info.info) (continuation_tac infos) + (observe_tac (str "intros_values_eq equation_others " ++ pr_leconstr_rd expr_info.info) (intros_values_eq expr_info []))) + else observe_tac (str "equation_others (cont_tac) " ++ pr_leconstr_rd expr_info.info) (continuation_tac infos) let equation_app f_and_args expr_info continuation_tac infos = if expr_info.is_final && expr_info.is_main_branch @@ -1225,8 +1230,8 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a let get_current_subgoals_types () = let p = Proof_global.give_me_the_proof () in - let { Evd.it=sgs ; sigma=sigma } = Proof.V82.subgoals p in - sigma, List.map (Goal.V82.abstract_type sigma) sgs + let sgs,_,_,_,sigma = Proof.proof p in + sigma, List.map (Goal.V82.abstract_type sigma) sgs exception EmptySubgoals let build_and_l sigma l = @@ -1419,7 +1424,7 @@ let com_terminate nb_args ctx hook = let start_proof ctx (tac_start:tactic) (tac_end:tactic) = - let (evmap, env) = Lemmas.get_current_context() in + let evmap, env = Pfedit.get_current_context () in Lemmas.start_proof thm_name (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env) ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) hook; @@ -1471,7 +1476,7 @@ let (com_eqn : int -> Id.t -> | ConstRef c -> is_opaque_constant c | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.") in - let (evmap, env) = Lemmas.get_current_context() in + let evmap, env = Pfedit.get_current_context () in let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in let f_constr = constr_of_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index 89feea8dc..bb01aca55 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -133,7 +133,9 @@ let pr_occurrences = pr_occurrences () () () let pr_gen prc _prlc _prtac c = prc c -let pr_globc _prc _prlc _prtac (_,glob) = Printer.pr_glob_constr glob +let pr_globc _prc _prlc _prtac (_,glob) = + let _, env = Pfedit.get_current_context () in + Printer.pr_glob_constr_env env glob let interp_glob ist gl (t,_) = Tacmach.project gl , (ist,t) diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 4b1555e55..71db919ef 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -315,7 +315,8 @@ let project_hint pri l2r r = in let ctx = Evd.universe_context_set sigma in let c = EConstr.to_constr sigma c in - let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in + let poly = Flags.use_polymorphic_flag () in + let c = Declare.declare_definition ~poly ~internal:Declare.InternalTacticRequest id (c,ctx) in let info = {Vernacexpr.hint_priority = pri; hint_pattern = None} in (info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c)) diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 5baa0d5c1..84e79d8ab 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -51,8 +51,12 @@ let eval_uconstrs ist cs = List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs let pr_auto_using_raw _ _ _ = Pptactic.pr_auto_using Ppconstr.pr_constr_expr -let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> Printer.pr_glob_constr c) -let pr_auto_using _ _ _ = Pptactic.pr_auto_using Printer.pr_closed_glob +let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> + let _, env = Pfedit.get_current_context () in + Printer.pr_glob_constr_env env c) +let pr_auto_using _ _ _ = Pptactic.pr_auto_using + (let sigma, env = Pfedit.get_current_context () in + Printer.pr_closed_glob_env env sigma) ARGUMENT EXTEND auto_using TYPED AS uconstr_list diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index b148d962e..91abe1019 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -31,8 +31,12 @@ type constr_expr_with_bindings = constr_expr with_bindings type glob_constr_with_bindings = Tacexpr.glob_constr_and_expr with_bindings type glob_constr_with_bindings_sign = interp_sign * Tacexpr.glob_constr_and_expr with_bindings -let pr_glob_constr_with_bindings_sign _ _ _ (ge : glob_constr_with_bindings_sign) = Printer.pr_glob_constr (fst (fst (snd ge))) -let pr_glob_constr_with_bindings _ _ _ (ge : glob_constr_with_bindings) = Printer.pr_glob_constr (fst (fst ge)) +let pr_glob_constr_with_bindings_sign _ _ _ (ge : glob_constr_with_bindings_sign) = + let _, env = Pfedit.get_current_context () in + Printer.pr_glob_constr_env env (fst (fst (snd ge))) +let pr_glob_constr_with_bindings _ _ _ (ge : glob_constr_with_bindings) = + let _, env = Pfedit.get_current_context () in + Printer.pr_glob_constr_env env (fst (fst ge)) let pr_constr_expr_with_bindings prc _ _ (ge : constr_expr_with_bindings) = prc (fst ge) let interp_glob_constr_with_bindings ist gl c = Tacmach.project gl , (ist, c) let glob_glob_constr_with_bindings ist l = Tacintern.intern_constr_with_bindings ist l @@ -272,5 +276,7 @@ TACTIC EXTEND setoid_transitivity END VERNAC COMMAND EXTEND PrintRewriteHintDb CLASSIFIED AS QUERY - [ "Print" "Rewrite" "HintDb" preident(s) ] -> [ Feedback.msg_notice (Autorewrite.print_rewrite_hintdb s) ] + [ "Print" "Rewrite" "HintDb" preident(s) ] -> + [ let sigma, env = Pfedit.get_current_context () in + Feedback.msg_notice (Autorewrite.print_rewrite_hintdb env sigma s) ] END diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 38460c669..d70751245 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -84,6 +84,14 @@ type 'a extra_genarg_printer = (tolerability -> Val.t -> Pp.t) -> 'a -> Pp.t +let string_of_genarg_arg (ArgumentType arg) = + let rec aux : type a b c. (a, b, c) genarg_type -> string = function + | ListArg t -> aux t ^ "_list" + | OptArg t -> aux t ^ "_opt" + | PairArg (t1, t2) -> assert false (* No parsing/printing rule for it *) + | ExtraArg s -> ArgT.repr s in + aux arg + let keyword x = tag_keyword (str x) let primitive x = tag_primitive (str x) @@ -536,15 +544,24 @@ let pr_goal_selector ~toplevel s = let pr_funvar n = spc () ++ Name.print n - let pr_let_clause k pr (na,(bl,t)) = + let pr_let_clause k pr_gen pr_arg (na,(bl,t)) = + let pr = function + | TacGeneric arg -> + let name = string_of_genarg_arg (genarg_tag arg) in + if name = "unit" || name = "int" then + (* Hard-wired parsing rules *) + pr_gen arg + else + str name ++ str ":" ++ surround (pr_gen arg) + | _ -> pr_arg (TacArg (Loc.tag t)) in hov 0 (keyword k ++ spc () ++ pr_lname na ++ prlist pr_funvar bl ++ - str " :=" ++ brk (1,1) ++ pr (TacArg (Loc.tag t))) + str " :=" ++ brk (1,1) ++ pr t) - let pr_let_clauses recflag pr = function + let pr_let_clauses recflag pr_gen pr = function | hd::tl -> hv 0 - (pr_let_clause (if recflag then "let rec" else "let") pr hd ++ - prlist (fun t -> spc () ++ pr_let_clause "with" pr t) tl) + (pr_let_clause (if recflag then "let rec" else "let") pr_gen pr hd ++ + prlist (fun t -> spc () ++ pr_let_clause "with" pr_gen pr t) tl) | [] -> anomaly (Pp.str "LetIn must declare at least one binding.") let pr_seq_body pr tl = @@ -858,7 +875,7 @@ let pr_goal_selector ~toplevel s = let llc = List.map (fun (id,t) -> (id,extract_binders t)) llc in v 0 (hv 0 ( - pr_let_clauses recflag (pr_tac ltop) llc + pr_let_clauses recflag pr.pr_generic (pr_tac ltop) llc ++ spc () ++ keyword "in" ) ++ fnl () ++ pr_tac (llet,E) u), llet @@ -1003,7 +1020,7 @@ let pr_goal_selector ~toplevel s = | TacAtom (loc,t) -> pr_with_comments ?loc (hov 1 (pr_atom pr strip_prod_binders tag_atom t)), ltatom | TacArg(_,Tacexp e) -> - pr.pr_tactic (latom,E) e, latom + pr_tac inherited e, latom | TacArg(_,ConstrMayEval (ConstrTerm c)) -> keyword "constr:" ++ pr.pr_constr c, latom | TacArg(_,ConstrMayEval c) -> @@ -1226,6 +1243,15 @@ let make_constr_printer f c = let lift f a = Genprint.PrinterBasic (fun () -> f a) + +let pr_glob_constr_pptac c = + let _, env = Pfedit.get_current_context () in + pr_glob_constr_env env c + +let pr_lglob_constr_pptac c = + let _, env = Pfedit.get_current_context () in + pr_lglob_constr_env env c + let () = let pr_bool b = if b then str "true" else str "false" in let pr_unit _ = str "()" in @@ -1240,7 +1266,7 @@ let () = Genprint.register_print0 wit_intro_pattern (Miscprint.pr_intro_pattern pr_constr_expr) - (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c)) + (Miscprint.pr_intro_pattern (fun (c, _) -> pr_glob_constr_pptac c)) pr_intro_pattern_env; Genprint.register_print0 wit_clause_dft_concl @@ -1251,45 +1277,45 @@ let () = Genprint.register_print0 wit_constr Ppconstr.pr_constr_expr - (fun (c, _) -> Printer.pr_glob_constr c) + (fun (c, _) -> pr_glob_constr_pptac c) (make_constr_printer Printer.pr_econstr_n_env) ; Genprint.register_print0 wit_uconstr Ppconstr.pr_constr_expr - (fun (c,_) -> Printer.pr_glob_constr c) + (fun (c, _) -> pr_glob_constr_pptac c) (make_constr_printer Printer.pr_closed_glob_n_env) ; Genprint.register_print0 wit_open_constr Ppconstr.pr_constr_expr - (fun (c, _) -> Printer.pr_glob_constr c) + (fun (c, _) -> pr_glob_constr_pptac c) (make_constr_printer Printer.pr_econstr_n_env) ; Genprint.register_print0 wit_red_expr (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr)) - (pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_and_constr_expr pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr)) + (pr_red_expr (pr_and_constr_expr pr_glob_constr_pptac, pr_and_constr_expr pr_lglob_constr_pptac, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr_pptac)) pr_red_expr_env ; Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis (lift pr_quantified_hypothesis); Genprint.register_print0 wit_bindings (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr) - (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) pr_bindings_env ; Genprint.register_print0 wit_constr_with_bindings (pr_with_bindings pr_constr_expr pr_lconstr_expr) - (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) pr_with_bindings_env ; Genprint.register_print0 wit_open_constr_with_bindings (pr_with_bindings pr_constr_expr pr_lconstr_expr) - (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) pr_with_bindings_env ; Genprint.register_print0 Tacarg.wit_destruction_arg (pr_destruction_arg pr_constr_expr pr_lconstr_expr) - (pr_destruction_arg (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + (pr_destruction_arg (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) pr_destruction_arg_env ; Genprint.register_print0 Stdarg.wit_int int int (lift int); diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 180fb2db4..918d1faeb 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -91,9 +91,10 @@ let subst_global_reference subst = let subst_global ref = let ref',t' = subst_global subst ref in if not (is_global ref' t') then - Feedback.msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++ - str " expanded to \"" ++ pr_lconstr t' ++ str "\", but to " ++ - pr_global ref') ; + (let sigma, env = Pfedit.get_current_context () in + Feedback.msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++ + str " expanded to \"" ++ pr_lconstr_env env sigma t' ++ str "\", but to " ++ + pr_global ref')); ref' in subst_or_var (subst_located subst_global) diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index a669692fc..2dd7c9a74 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -20,7 +20,9 @@ let prmatchpatt env sigma hyp = Pptactic.pr_match_pattern (Printer.pr_constr_pattern_env env sigma) hyp let prmatchrl rl = Pptactic.pr_match_rule false (Pptactic.pr_glob_tactic (Global.env())) - (fun (_,p) -> Printer.pr_constr_pattern p) rl + (fun (_,p) -> + let sigma, env = Pfedit.get_current_context () in + Printer.pr_constr_pattern_env env sigma p) rl (* This module intends to be a beginning of debugger for tactic expressions. Currently, it is quite simple and we can hope to have, in the future, a more @@ -369,7 +371,8 @@ let explain_ltac_call_trace last trace loc = strbrk " (with " ++ prlist_with_sep pr_comma (fun (id,c) -> - Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders c) + let sigma, env = Pfedit.get_current_context () in + Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders_env env sigma c) (List.rev (Id.Map.bindings vars)) ++ str ")" else mt()) in diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 218342efe..cb54cac3f 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -984,7 +984,9 @@ struct let parse_expr sigma parse_constant parse_exp ops_spec env term = if debug - then Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr term); + then ( + let _, env = Pfedit.get_current_context () in + Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env env sigma term)); (* let constant_or_variable env term = @@ -1103,9 +1105,10 @@ struct | _ -> raise ParseError - let rconstant sigma term = + let rconstant sigma term = + let _, env = Pfedit.get_current_context () in if debug - then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.pr_leconstr term ++ fnl ()); + then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.pr_leconstr_env env sigma term ++ fnl ()); let res = rconstant sigma term in if debug then (Printf.printf "rconstant -> %a\n" pp_Rcst res ; flush stdout) ; @@ -1145,9 +1148,9 @@ struct let parse_arith parse_op parse_expr env cstr gl = let sigma = gl.sigma in - if debug - then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr cstr ++ fnl ()); - match EConstr.kind sigma cstr with + if debug + then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr_env gl.env sigma cstr ++ fnl ()); + match EConstr.kind sigma cstr with | Term.App(op,args) -> let (op,lhs,rhs) = parse_op gl (op,args) in let (e1,env) = parse_expr sigma env lhs in @@ -1908,7 +1911,7 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2 let formula_typ = (EConstr.mkApp(Lazy.force coq_Cstr, [|spec.coeff|])) in let ff = dump_formula formula_typ (dump_cstr spec.typ spec.dump_coeff) ff in - Feedback.msg_notice (Printer.pr_leconstr ff); + Feedback.msg_notice (Printer.pr_leconstr_env gl.env gl.sigma ff); Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff end; @@ -1932,9 +1935,9 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2 Feedback.msg_notice (Pp.str "\nAFormula\n") ; let formula_typ = (EConstr.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in let ff' = dump_formula formula_typ - (dump_cstr spec.typ spec.dump_coeff) ff' in - Feedback.msg_notice (Printer.pr_leconstr ff'); - Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff' + (dump_cstr spec.typ spec.dump_coeff) ff' in + Feedback.msg_notice (Printer.pr_leconstr_env gl.env gl.sigma ff'); + Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff' end; (* Even if it does not work, this does not mean it is not provable diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml index 7da4a3b82..52c6ef983 100644 --- a/plugins/micromega/micromega.ml +++ b/plugins/micromega/micromega.ml @@ -981,8 +981,8 @@ let rec or_cnf unsat deduce f f' = (** val and_cnf : 'a1 cnf -> 'a1 cnf -> 'a1 cnf **) -let and_cnf f1 f2 = - app f1 f2 +let and_cnf = + app (** val xcnf : ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> ('a1 @@ -1204,22 +1204,22 @@ type 't formula = { flhs : 't pExpr; fop : op2; frhs : 't pExpr } 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol **) -let norm cO cI cplus ctimes cminus copp ceqb = - norm_aux cO cI cplus ctimes cminus copp ceqb +let norm = + norm_aux (** val psub0 : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **) -let psub0 cO cplus cminus copp ceqb = - psub cO cplus cminus copp ceqb +let psub0 = + psub (** val padd0 : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **) -let padd0 cO cplus ceqb = - padd cO cplus ceqb +let padd0 = + padd (** val xnormalise : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 430b608f4..54ff44fbd 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -183,8 +183,9 @@ let print_env_reification env = let rec loop c i = function [] -> str " ===============================\n\n" | t :: l -> + let sigma, env = Pfedit.get_current_context () in let s = Printf.sprintf "(%c%02d)" c i in - spc () ++ str s ++ str " := " ++ Printer.pr_lconstr t ++ fnl () ++ + spc () ++ str s ++ str " := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++ loop c (succ i) l in let prop_info = str "ENVIRONMENT OF PROPOSITIONS :" ++ fnl () ++ loop 'P' 0 env.props in diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index 05ab8ab32..a7d6d5bb2 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -82,10 +82,11 @@ VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF | [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [ Feedback.msg_notice (strbrk "The following ring structures have been declared:"); Spmap.iter (fun fn fi -> + let sigma, env = Pfedit.get_current_context () in Feedback.msg_notice (hov 2 (Ppconstr.pr_id (Libnames.basename fn)++spc()++ - str"with carrier "++ pr_constr fi.ring_carrier++spc()++ - str"and equivalence relation "++ pr_constr fi.ring_req)) + str"with carrier "++ pr_constr_env env sigma fi.ring_carrier++spc()++ + str"and equivalence relation "++ pr_constr_env env sigma fi.ring_req)) ) !from_name ] END @@ -117,10 +118,11 @@ VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF | [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [ Feedback.msg_notice (strbrk "The following field structures have been declared:"); Spmap.iter (fun fn fi -> + let sigma, env = Pfedit.get_current_context () in Feedback.msg_notice (hov 2 (Ppconstr.pr_id (Libnames.basename fn)++spc()++ - str"with carrier "++ pr_constr fi.field_carrier++spc()++ - str"and equivalence relation "++ pr_constr fi.field_req)) + str"with carrier "++ pr_constr_env env sigma fi.field_carrier++spc()++ + str"and equivalence relation "++ pr_constr_env env sigma fi.field_req)) ) !field_from_name ] END diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 9e4b896f8..1c3bdb958 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -344,8 +344,6 @@ let _ = add_map "ring" (****************************************************************************) (* Ring database *) -let pr_constr c = pr_econstr c - module Cmap = Map.Make(Constr) let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table" @@ -368,7 +366,7 @@ let find_ring_structure env sigma l = with Not_found -> CErrors.user_err ~hdr:"ring" (str"cannot find a declared ring structure over"++ - spc()++str"\""++pr_constr ty++str"\"")) + spc() ++ str"\"" ++ pr_econstr_env env sigma ty ++ str"\"")) | [] -> assert false let add_entry (sp,_kn) e = @@ -529,19 +527,19 @@ let ring_equality env evd (r,add,mul,opp,req) = op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in Flags.if_verbose Feedback.msg_info - (str"Using setoid \""++pr_constr req++str"\""++spc()++ - str"and morphisms \""++pr_constr add_m_lem ++ - str"\","++spc()++ str"\""++pr_constr mul_m_lem++ - str"\""++spc()++str"and \""++pr_constr opp_m_lem++ + (str"Using setoid \""++ pr_econstr_env env !evd req++str"\""++spc()++ + str"and morphisms \""++pr_econstr_env env !evd add_m_lem ++ + str"\","++spc()++ str"\""++pr_econstr_env env !evd mul_m_lem++ + str"\""++spc()++str"and \""++pr_econstr_env env !evd opp_m_lem++ str"\""); op_morph) | None -> (Flags.if_verbose Feedback.msg_info - (str"Using setoid \""++pr_constr req ++str"\"" ++ spc() ++ - str"and morphisms \""++pr_constr add_m_lem ++ + (str"Using setoid \""++pr_econstr_env env !evd req ++str"\"" ++ spc() ++ + str"and morphisms \""++pr_econstr_env env !evd add_m_lem ++ str"\""++spc()++str"and \""++ - pr_constr mul_m_lem++str"\""); + pr_econstr_env env !evd mul_m_lem++str"\""); op_smorph r add mul req add_m_lem mul_m_lem) in (setoid,op_morph) @@ -861,7 +859,7 @@ let find_field_structure env sigma l = with Not_found -> CErrors.user_err ~hdr:"field" (str"cannot find a declared field structure over"++ - spc()++str"\""++pr_constr ty++str"\"")) + spc()++str"\""++pr_econstr_env env sigma ty++str"\"")) | [] -> assert false let add_field_entry (sp,_kn) e = diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index c1d7e6278..83b454769 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -240,7 +240,7 @@ let interp_refine ist gl rc = in let sigma, c = Pretyping.understand_ltac flags (pf_env gl) (project gl) vars kind rc in (* ppdebug(lazy(str"sigma@interp_refine=" ++ pr_evar_map None sigma)); *) - ppdebug(lazy(str"c@interp_refine=" ++ Printer.pr_econstr c)); + ppdebug(lazy(str"c@interp_refine=" ++ Printer.pr_econstr_env (pf_env gl) sigma c)); (sigma, (sigma, c)) @@ -539,7 +539,7 @@ module Intset = Evar.Set let pf_abs_evars_pirrel gl (sigma, c0) = pp(lazy(str"==PF_ABS_EVARS_PIRREL==")); - pp(lazy(str"c0= " ++ Printer.pr_constr c0)); + pp(lazy(str"c0= " ++ Printer.pr_constr_env (pf_env gl) sigma c0)); let sigma0 = project gl in let c0 = nf_evar sigma0 (nf_evar sigma c0) in let nenv = env_size (pf_env gl) in @@ -563,7 +563,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) = | _ -> Constr.fold put evlist c in let evlist = put [] c0 in if evlist = [] then 0, c0 else - let pr_constr t = Printer.pr_econstr (Reductionops.nf_beta (project gl) (EConstr.of_constr t)) in + let pr_constr t = Printer.pr_econstr_env (pf_env gl) sigma (Reductionops.nf_beta (project gl) (EConstr.of_constr t)) in pp(lazy(str"evlist=" ++ pr_list (fun () -> str";") (fun (k,_) -> str(Evd.string_of_existential k)) evlist)); let evplist = @@ -959,7 +959,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl = loop (meta_declare m (EConstr.Unsafe.to_constr ty) sigma) bo ((EConstr.mkMeta m)::args) (n-1) | _ -> assert false in loop sigma t [] n in - pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr t)); + pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t)); Tacmach.refine_no_check t gl let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl = @@ -973,7 +973,7 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl = compose_lam (let xs,y = List.chop (n-1) l in y @ xs) (mkApp (compose_lam l c, Array.of_list (mkRel 1 :: mkRels n))) in - pp(lazy(str"after: " ++ Printer.pr_constr oc)); + pp(lazy(str"after: " ++ Printer.pr_constr_env (pf_env gl) (project gl) oc)); try applyn ~with_evars ~with_shelve:true ?beta n (EConstr.of_constr oc) gl with e when CErrors.noncritical e -> raise dependent_apply_error @@ -1202,7 +1202,7 @@ let genclrtac cl cs clr = let gentac ist gen gl = (* ppdebug(lazy(str"sigma@gentac=" ++ pr_evar_map None (project gl))); *) let conv, _, cl, c, clr, ucst,gl = pf_interp_gen_aux ist gl false gen in - ppdebug(lazy(str"c@gentac=" ++ pr_econstr c)); + ppdebug(lazy(str"c@gentac=" ++ pr_econstr_env (pf_env gl) (project gl) c)); let gl = pf_merge_uc ucst gl in if conv then tclTHEN (Proofview.V82.of_tactic (convert_concl cl)) (cleartac clr) gl diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 26b5c5767..4e0b44a44 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -46,7 +46,7 @@ let analyze_eliminator elimty env sigma = if not (EConstr.eq_constr sigma t t') then loop ctx t' else errorstrm Pp.(str"The eliminator has the wrong shape."++spc()++ str"A (applied) bound variable was expected as the conclusion of "++ - str"the eliminator's"++Pp.cut()++str"type:"++spc()++pr_econstr elimty) in + str"the eliminator's"++Pp.cut()++str"type:"++spc()++pr_econstr_env env' sigma elimty) in let ctx, pred_id, elim_is_dep, n_pred_args,concl = loop [] elimty in let n_elim_args = Context.Rel.nhyps ctx in let is_rec_elim = @@ -126,7 +126,7 @@ let ssrelim ?(ind=ref None) ?(is_case=false) ?ist deps what ?elim eqid elim_intr ppdebug(lazy Pp.(str"matching: " ++ pr_occ occ ++ pp_pattern p)); let (c,ucst), cl = fill_occ_pattern ~raise_NoMatch:true env sigma0 (EConstr.Unsafe.to_constr cl) p occ h in - ppdebug(lazy Pp.(str" got: " ++ pr_constr c)); + ppdebug(lazy Pp.(str" got: " ++ pr_constr_env env sigma0 c)); c, EConstr.of_constr cl, ucst in let mkTpat gl t = (* takes a term, refreshes it and makes a T pattern *) let n, t, _, ucst = pf_abs_evars orig_gl (project gl, fire_subst gl t) in @@ -239,8 +239,8 @@ let ssrelim ?(ind=ref None) ?(is_case=false) ?ist deps what ?elim eqid elim_intr | Some (c, _, _,gl) -> true, gl | None -> errorstrm Pp.(str"Unable to apply the eliminator to the term"++ - spc()++pr_econstr c++spc()++str"or to unify it's type with"++ - pr_econstr inf_arg_ty) in + spc()++pr_econstr_env env (project gl) c++spc()++str"or to unify it's type with"++ + pr_econstr_env env (project gl) inf_arg_ty) in ppdebug(lazy Pp.(str"c_is_head_p= " ++ bool c_is_head_p)); let gl, predty = pfe_type_of gl pred in (* Patterns for the inductive types indexes to be bound in pred are computed diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index e82f222b9..274c7110c 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -77,7 +77,7 @@ let interp_congrarg_at ist gl n rf ty m = if i + n > m then None else try let rt = mkRApp congrn (args1 @ mkRApp rf (mkRHoles i) :: args2) in - ppdebug(lazy Pp.(str"rt=" ++ Printer.pr_glob_constr rt)); + ppdebug(lazy Pp.(str"rt=" ++ Printer.pr_glob_constr_env (pf_env gl) rt)); Some (interp_refine ist gl rt) with _ -> loop (i + 1) in loop 0 @@ -86,7 +86,7 @@ let pattern_id = mk_internal_id "pattern value" let congrtac ((n, t), ty) ist gl = ppdebug(lazy (Pp.str"===congr===")); - ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr (Tacmach.pf_concl gl))); + ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (Tacmach.pf_concl gl))); let sigma, _ as it = interp_term ist gl t in let gl = pf_merge_uc_of sigma gl in let _, f, _, _ucst = pf_abs_evars gl it in @@ -109,7 +109,7 @@ let congrtac ((n, t), ty) ist gl = let newssrcongrtac arg ist gl = ppdebug(lazy Pp.(str"===newcongr===")); - ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr (pf_concl gl))); + ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (pf_concl gl))); (* utils *) let fs gl t = Reductionops.nf_evar (project gl) t in let tclMATCH_GOAL (c, gl_c) proj t_ok t_fail gl = @@ -247,7 +247,7 @@ let unfoldintac occ rdx t (kt,_) gl = try find_T env c h ~k:(fun env c _ _ -> EConstr.Unsafe.to_constr (body env t (EConstr.of_constr c))) with NoMatch when easy -> c | NoMatch | NoProgress -> errorstrm Pp.(str"No occurrence of " - ++ pr_constr_pat (EConstr.Unsafe.to_constr t) ++ spc() ++ str "in " ++ Printer.pr_constr c)), + ++ pr_constr_pat (EConstr.Unsafe.to_constr t) ++ spc() ++ str "in " ++ Printer.pr_constr_env env sigma c)), (fun () -> try end_T () with | NoMatch when easy -> fake_pmatcher_end () | NoMatch -> anomaly "unfoldintac") @@ -267,13 +267,13 @@ let unfoldintac occ rdx t (kt,_) gl = | Proj _ when same_proj sigma0 c t -> body env t c | Const f -> aux (body env c c) | App (f, a) -> aux (EConstr.mkApp (body env f f, a)) - | _ -> errorstrm Pp.(str "The term "++pr_constr orig_c++ - str" contains no " ++ pr_econstr t ++ str" even after unfolding") + | _ -> errorstrm Pp.(str "The term "++ pr_constr_env env sigma orig_c++ + str" contains no " ++ pr_econstr_env env sigma t ++ str" even after unfolding") in EConstr.Unsafe.to_constr @@ aux (EConstr.of_constr c) else try EConstr.Unsafe.to_constr @@ body env t (fs (unify_HO env sigma (EConstr.of_constr c) t) t) with _ -> errorstrm Pp.(str "The term " ++ - pr_constr c ++spc()++ str "does not unify with " ++ pr_constr_pat (EConstr.Unsafe.to_constr t))), + pr_constr_env env sigma c ++spc()++ str "does not unify with " ++ pr_constr_pat (EConstr.Unsafe.to_constr t))), fake_pmatcher_end in let concl = let concl0 = EConstr.Unsafe.to_constr concl0 in @@ -352,7 +352,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = (* We check the proof is well typed *) let sigma, proof_ty = try Typing.type_of env sigma proof with _ -> raise PRtype_error in - ppdebug(lazy Pp.(str"pirrel_rewrite proof term of type: " ++ pr_econstr proof_ty)); + ppdebug(lazy Pp.(str"pirrel_rewrite proof term of type: " ++ pr_econstr_env env sigma proof_ty)); try refine_with ~first_goes_last:(not !ssroldreworder) ~with_evars:false (sigma, proof) gl with _ -> @@ -374,8 +374,8 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = if open_evs <> [] then Some name else None) (List.combine (Array.to_list args) names) | _ -> anomaly "rewrite rule not an application" in - errorstrm Pp.(Himsg.explain_refiner_error (Logic.UnresolvedBindings miss)++ - (Pp.fnl()++str"Rule's type:" ++ spc() ++ pr_econstr hd_ty)) + errorstrm Pp.(Himsg.explain_refiner_error env sigma (Logic.UnresolvedBindings miss)++ + (Pp.fnl()++str"Rule's type:" ++ spc() ++ pr_econstr_env env sigma hd_ty)) ;; let is_construct_ref sigma c r = @@ -391,12 +391,12 @@ let rwcltac cl rdx dir sr gl = let gl = pf_unsafe_merge_uc ucst gl in let rdxt = Retyping.get_type_of (pf_env gl) (fst sr) rdx in (* ppdebug(lazy(str"sigma@rwcltac=" ++ pr_evar_map None (fst sr))); *) - ppdebug(lazy Pp.(str"r@rwcltac=" ++ pr_econstr (snd sr))); + ppdebug(lazy Pp.(str"r@rwcltac=" ++ pr_econstr_env (pf_env gl) (project gl) (snd sr))); let cvtac, rwtac, gl = if EConstr.Vars.closed0 (project gl) r' then let env, sigma, c, c_eq = pf_env gl, fst sr, snd sr, Coqlib.build_coq_eq () in let sigma, c_ty = Typing.type_of env sigma c in - ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr c_ty)); + ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty)); match EConstr.kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with | AtomicType(e, a) when is_ind_ref sigma e c_eq -> let new_rdx = if dir = L2R then a.(2) else a.(1) in @@ -411,7 +411,7 @@ let rwcltac cl rdx dir sr gl = let r3, _, r3t = try EConstr.destCast (project gl) r2 with _ -> errorstrm Pp.(str "no cast from " ++ pr_constr_pat (EConstr.Unsafe.to_constr (snd sr)) - ++ str " to " ++ pr_econstr r2) in + ++ str " to " ++ pr_econstr_env (pf_env gl) (project gl) r2) in let cl' = EConstr.mkNamedProd rule_id (EConstr.it_mkProd_or_LetIn r3t dc) (EConstr.Vars.lift 1 cl) in let cl'' = EConstr.mkNamedProd pattern_id rdxt cl' in let itacs = [introid pattern_id; introid rule_id] in @@ -605,7 +605,7 @@ let ssrinstancesofrule ist dir arg gl = sigma, pats @ [pat] in let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true sigma0 None ~upats_origin rpats in - let print env p c _ = Feedback.msg_info Pp.(hov 1 (str"instance:" ++ spc() ++ pr_constr p ++ spc() ++ str "matches:" ++ spc() ++ pr_constr c)); c in + let print env p c _ = Feedback.msg_info Pp.(hov 1 (str"instance:" ++ spc() ++ pr_constr_env env r_sigma p ++ spc() ++ str "matches:" ++ spc() ++ pr_constr_env env r_sigma c)); c in Feedback.msg_info Pp.(str"BEGIN INSTANCES"); try while true do diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 29e96ec59..a707226cd 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -72,13 +72,14 @@ let examine_abstract id gl = let gl, tid = pfe_type_of gl id in let abstract, gl = pf_mkSsrConst "abstract" gl in let sigma = project gl in + let env = pf_env gl in if not (EConstr.isApp sigma tid) || not (EConstr.eq_constr sigma (fst(EConstr.destApp sigma tid)) abstract) then - errorstrm(strbrk"not an abstract constant: "++pr_econstr id); + errorstrm(strbrk"not an abstract constant: "++ pr_econstr_env env sigma id); let _, args_id = EConstr.destApp sigma tid in if Array.length args_id <> 3 then - errorstrm(strbrk"not a proper abstract constant: "++pr_econstr id); + errorstrm(strbrk"not a proper abstract constant: "++ pr_econstr_env env sigma id); if not (is_Evar_or_CastedMeta sigma args_id.(2)) then - errorstrm(strbrk"abstract constant "++pr_econstr id++str" already used"); + errorstrm(strbrk"abstract constant "++ pr_econstr_env env sigma id++str" already used"); tid, args_id let pf_find_abstract_proof check_lock gl abstract_n = @@ -94,7 +95,7 @@ let pf_find_abstract_proof check_lock gl abstract_n = | _ -> l) (project gl) [] in match l with | [e] -> e - | _ -> errorstrm(strbrk"abstract constant "++pr_constr abstract_n++ + | _ -> errorstrm(strbrk"abstract constant "++ pr_constr_env (pf_env gl) (project gl) abstract_n ++ strbrk" not found in the evar map exactly once. "++ strbrk"Did you tamper with it?") @@ -205,7 +206,7 @@ let havetac ist let assert_is_conv gl = try Proofview.V82.of_tactic (convert_concl (EConstr.it_mkProd_or_LetIn concl ctx)) gl with _ -> errorstrm (str "Given proof term is not of type " ++ - pr_econstr (EConstr.mkArrow (EConstr.mkVar (Id.of_string "_")) concl)) in + pr_econstr_env (pf_env gl) (project gl) (EConstr.mkArrow (EConstr.mkVar (Id.of_string "_")) concl)) in gl, ty, Tacticals.tclTHEN assert_is_conv (Proofview.V82.of_tactic (Tactics.apply t)), id, itac_c | FwdHave, false, false -> let skols = List.flatten (List.map (function @@ -271,7 +272,7 @@ let ssrabstract ist gens (*last*) gl = let gl, proof = let pf_unify_HO gl a b = try pf_unify_HO gl a b - with _ -> errorstrm(strbrk"The abstract variable "++pr_econstr id++ + with _ -> errorstrm(strbrk"The abstract variable "++ pr_econstr_env env (project gl) id++ strbrk" cannot abstract this goal. Did you generalize it?") in let find_hole p t = match EConstr.kind (project gl) t with @@ -290,7 +291,7 @@ let ssrabstract ist gens (*last*) gl = | App(hd, [|left; right|]) when Term.Constr.equal hd prod -> find_hole (mkApp (proj1,[|left;right;p|])) left *) - | _ -> errorstrm(strbrk"abstract constant "++pr_econstr abstract_n++ + | _ -> errorstrm(strbrk"abstract constant "++ pr_econstr_env env (project gl) abstract_n++ strbrk" has an unexpected shape. Did you tamper with it?") in find_hole @@ -361,14 +362,14 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = | Sort _, [] -> EConstr.Vars.subst_vars s ct | LetIn(Name id as n,b,ty,c), _::g -> EConstr.mkLetIn (n,b,ty,var2rel c g (id::s)) | Prod(Name id as n,ty,c), _::g -> EConstr.mkProd (n,ty,var2rel c g (id::s)) - | _ -> CErrors.anomaly(str"SSR: wlog: var2rel: " ++ pr_econstr c) in + | _ -> CErrors.anomaly(str"SSR: wlog: var2rel: " ++ pr_econstr_env env sigma c) in let c = var2rel c gens [] in let rec pired c = function | [] -> c | t::ts as args -> match EConstr.kind sigma c with | Prod(_,_,c) -> pired (EConstr.Vars.subst1 t c) ts | LetIn(id,b,ty,c) -> EConstr.mkLetIn (id,b,ty,pired c args) - | _ -> CErrors.anomaly(str"SSR: wlog: pired: " ++ pr_econstr c) in + | _ -> CErrors.anomaly(str"SSR: wlog: pired: " ++ pr_econstr_env env sigma c) in c, args, pired c args, pf_merge_uc uc gl in let tacipat pats = introstac ~ist pats in let tacigens = @@ -396,8 +397,8 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = | Some id -> if pats = [] then Tacticals.tclIDTAC else let args = Array.of_list args in - ppdebug(lazy(str"specialized="++pr_econstr EConstr.(mkApp (mkVar id,args)))); - ppdebug(lazy(str"specialized_ty="++pr_econstr ct)); + ppdebug(lazy(str"specialized="++ pr_econstr_env (pf_env gl) (project gl) EConstr.(mkApp (mkVar id,args)))); + ppdebug(lazy(str"specialized_ty="++ pr_econstr_env (pf_env gl) (project gl) ct)); Tacticals.tclTHENS (basecuttac "ssr_have" ct) [Proofview.V82.of_tactic (Tactics.apply EConstr.(mkApp (mkVar id,args))); Tacticals.tclIDTAC] in "ssr_have", diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 023778fdb..6c325cce4 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -272,7 +272,7 @@ let (introstac : ?ist:Tacinterp.interp_sign -> ssripats -> Tacmach.tactic), let elim_intro_tac ipats ?ist what eqid ssrelim is_rec clr gl = (* Utils of local interest only *) let iD s ?t gl = let t = match t with None -> pf_concl gl | Some x -> x in - ppdebug(lazy Pp.(str s ++ pr_econstr t)); Tacticals.tclIDTAC gl in + ppdebug(lazy Pp.(str s ++ pr_econstr_env (pf_env gl) (project gl) t)); Tacticals.tclIDTAC gl in let protectC, gl = pf_mkSsrConst "protect_term" gl in let eq, gl = pf_fresh_global (Coqlib.build_coq_eq ()) gl in let eq = EConstr.of_constr eq in diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 7b591fead..46403aef3 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -1131,7 +1131,7 @@ let pr_fwd_guarded prval prval' = function | (fk, h), (_, (_, Some c)) -> pr_gen_fwd prval pr_constr_expr prl_constr_expr fk (format_constr_expr h c) | (fk, h), (_, (c, None)) -> - pr_gen_fwd prval' pr_glob_constr prl_glob_constr fk (format_glob_constr h c) + pr_gen_fwd prval' pr_glob_constr_env prl_glob_constr fk (format_glob_constr h c) let pr_unguarded prc prlc = prlc diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index e865ef706..4b2fab6d1 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -24,7 +24,7 @@ let pp_concat hd ?(sep=str", ") = function [] -> hd | x :: xs -> hd ++ List.fold_left (fun acc x -> acc ++ sep ++ x) x xs let pp_term gl t = - let t = Reductionops.nf_evar (project gl) t in pr_econstr t + let t = Reductionops.nf_evar (project gl) t in pr_econstr_env (pf_env gl) (project gl) t (* FIXME *) (* terms are pre constr, the kind is parsing/printing flag to distinguish diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 36dce37ae..cd614fee9 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -343,7 +343,7 @@ let coerce_search_pattern_to_sort hpat = let hpat' = if np = na then hpat else mkPApp hpat (np - na) [||] in let warn () = Feedback.msg_warning (str "Listing only lemmas with conclusion matching " ++ - pr_constr_pattern hpat') in + pr_constr_pattern_env env sigma hpat') in if EConstr.isSort sigma ht then begin warn (); true, hpat' end else let filter_head, coe_path = try @@ -359,7 +359,7 @@ let coerce_search_pattern_to_sort hpat = let n_imps = Option.get (Classops.hide_coercion coe_ref) in mkPApp (Pattern.PRef coe_ref) n_imps [|hp|] with _ -> - errorstrm (str "need explicit coercion " ++ pr_constr coe ++ spc () + errorstrm (str "need explicit coercion " ++ pr_constr_env env sigma coe ++ spc () ++ str "to interpret head search pattern as type") in filter_head, List.fold_left coerce hpat' coe_path @@ -468,10 +468,12 @@ let pr_raw_ssrhintref prc _ _ = let open CAst in function prc c ++ str "|" ++ int (List.length args) | c -> prc c -let pr_rawhintref c = match DAst.get c with +let pr_rawhintref c = + let _, env = Pfedit.get_current_context () in + match DAst.get c with | GApp (f, args) when isRHoles args -> - pr_glob_constr f ++ str "|" ++ int (List.length args) - | _ -> pr_glob_constr c + pr_glob_constr_env env f ++ str "|" ++ int (List.length args) + | _ -> pr_glob_constr_env env c let pr_glob_ssrhintref _ _ _ (c, _) = pr_rawhintref c diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index d5c9e4988..276b7c8ab 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -100,7 +100,6 @@ let pr_guarded guard prc c = let s = Pp.string_of_ppcmds (prc c) ^ "$" in if guard s (skip_wschars s 0) then pr_paren prc c else prc c (* More sensible names for constr printers *) -let pr_constr = pr_constr let prl_glob_constr c = pr_lglob_constr_env (Global.env ()) c let pr_glob_constr c = pr_glob_constr_env (Global.env ()) c let prl_constr_expr = pr_lconstr_expr @@ -427,7 +426,8 @@ let hole_var = mkVar (Id.of_string "_") let pr_constr_pat c0 = let rec wipe_evar c = if isEvar c then hole_var else map wipe_evar c in - pr_constr (wipe_evar c0) + let sigma, env = Pfedit.get_current_context () in + pr_constr_env env sigma (wipe_evar c0) (* Turn (new) evars into metas *) let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 = @@ -1215,7 +1215,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let pop_evar sigma e p = let { Evd.evar_body = e_body } as e_def = Evd.find sigma e in let e_body = match e_body with Evar_defined c -> c - | _ -> errorstrm (str "Matching the pattern " ++ pr_constr p ++ + | _ -> errorstrm (str "Matching the pattern " ++ pr_constr_env env0 sigma0 p ++ str " did not instantiate ?" ++ int (Evar.repr e) ++ spc () ++ str "Does the variable bound by the \"in\" construct occur "++ str "in the pattern?") in @@ -1417,7 +1417,8 @@ let ssrinstancesof ist arg gl = let find, conclude = mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true sigma None (etpat,[tpat]) in - let print env p c _ = ppnl (hov 1 (str"instance:" ++ spc() ++ pr_constr p ++ spc() ++ str "matches:" ++ spc() ++ pr_constr c)); c in + let print env p c _ = ppnl (hov 1 (str"instance:" ++ spc() ++ pr_constr_env (pf_env gl) (gl.sigma) p ++ spc() + ++ str "matches:" ++ spc() ++ pr_constr_env (pf_env gl) (gl.sigma) c)); c in ppnl (str"BEGIN INSTANCES"); try while true do diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 3a2eac7e7..95de96926 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -208,25 +208,32 @@ and reify_value = function (* reduction under binders *) | STACK (n,v,stk) -> lift n (reify_stack (reify_value v) stk) | CBN(t,env) -> - t - (* map_constr_with_binders subs_lift (cbv_norm_term) env t *) - | LAM (n,ctxt,b,env) -> - List.fold_left (fun c (n,t) -> mkLambda (n, t, c)) b ctxt + apply_env env t + | LAM (k,ctxt,b,env) -> + apply_env env @@ + List.fold_left (fun c (n,t) -> + mkLambda (n, t, c)) b ctxt | FIXP ((lij,(names,lty,bds)),env,args) -> - mkApp - (mkFix (lij, - (names, - lty, - bds)), - Array.map reify_value args) + let fix = mkFix (lij, (names, lty, bds)) in + mkApp (apply_env env fix, Array.map reify_value args) | COFIXP ((j,(names,lty,bds)),env,args) -> - mkApp - (mkCoFix (j, - (names,lty,bds)), - Array.map reify_value args) + let cofix = mkCoFix (j, (names,lty,bds)) in + mkApp (apply_env env cofix, Array.map reify_value args) | CONSTR (c,args) -> mkApp(mkConstructU c, Array.map reify_value args) +and apply_env env t = + match kind t with + | Rel i -> + begin match expand_rel i env with + | Inl (k, v) -> + reify_value (shift_value k v) + | Inr (k,_) -> + mkRel k + end + | _ -> + map_with_binders subs_lift apply_env env t + (* The main recursive functions * * Go under applications and cases/projections (pushed in the stack), @@ -290,7 +297,10 @@ let rec norm_head info env t stack = | Evar ev -> (match evar_value info.infos.i_cache ev with Some c -> norm_head info env c stack - | None -> (VAL(0, t), stack)) + | None -> + let e, xs = ev in + let xs' = Array.map (apply_env env) xs in + (VAL(0, mkEvar (e,xs')), stack)) (* non-neutral cases *) | Lambda _ -> diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 0f6452de6..bce5710d6 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -396,7 +396,7 @@ let tag_var = tag Tag.variable extract_prod_binders c | { loc; v = CProdN ([[_,Name id],bk,t], { v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([_,[p]],b))])} ) } - when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) -> + when Id.equal id id' && not (Id.Set.mem id (free_vars_of_constr_expr b)) -> let bl,c = extract_prod_binders b in CLocalPattern (loc, (p,None)) :: bl, c | { loc; v = CProdN ((nal,bk,t)::bl,c) } -> @@ -412,7 +412,7 @@ let tag_var = tag Tag.variable extract_lam_binders c | CLambdaN ([[_,Name id],bk,t], { v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([_,[p]],b))])} ) - when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) -> + when Id.equal id id' && not (Id.Set.mem id (free_vars_of_constr_expr b)) -> let bl,c = extract_lam_binders b in CLocalPattern (ce.loc,(p,None)) :: bl, c | CLambdaN ((nal,bk,t)::bl,c) -> @@ -430,7 +430,7 @@ let tag_var = tag Tag.variable let rename na na' t c = match (na,na') with | (_,Name id), (_,Name id') -> - (na',t,Topconstr.replace_vars_constr_expr (Id.Map.singleton id id') c) + (na',t,replace_vars_constr_expr (Id.Map.singleton id id') c) | (_,Name id), (_,Anonymous) -> (na,t,c) | _ -> (na',t,c) diff --git a/printing/pputils.ml b/printing/pputils.ml index 3cc7a3e6b..12d5338ad 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -103,6 +103,9 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) keyword = function | CbvNative o -> keyword "native_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o +let pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_ref,pr_pattern) = + pr_red_expr (pr_constr env sigma, pr_lconstr env sigma, pr_ref, pr_pattern env sigma) + let pr_or_by_notation f = function | AN v -> f v | ByNotation (_,(s,sc)) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc diff --git a/printing/pputils.mli b/printing/pputils.mli index 1f4fa1390..f7f586b77 100644 --- a/printing/pputils.mli +++ b/printing/pputils.mli @@ -21,8 +21,16 @@ val pr_with_occurrences : val pr_short_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t val pr_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t + val pr_red_expr : ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) -> + (string -> Pp.t) -> ('a,'b,'c) red_expr_gen -> Pp.t + +val pr_red_expr_env : Environ.env -> Evd.evar_map -> + (Environ.env -> Evd.evar_map -> 'a -> Pp.t) * + (Environ.env -> Evd.evar_map -> 'a -> Pp.t) * + ('b -> Pp.t) * + (Environ.env -> Evd.evar_map -> 'c -> Pp.t) -> (string -> Pp.t) -> ('a,'b,'c) red_expr_gen -> Pp.t diff --git a/printing/prettyp.ml b/printing/prettyp.ml index acbd2d5d2..e2d23ce7b 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -35,13 +35,13 @@ module NamedDecl = Context.Named.Declaration type object_pr = { print_inductive : MutInd.t -> Pp.t; print_constant_with_infos : Constant.t -> Pp.t; - print_section_variable : variable -> Pp.t; - print_syntactic_def : KerName.t -> Pp.t; + print_section_variable : env -> Evd.evar_map -> variable -> Pp.t; + print_syntactic_def : env -> KerName.t -> Pp.t; print_module : bool -> ModPath.t -> Pp.t; print_modtype : ModPath.t -> Pp.t; - print_named_decl : Context.Named.Declaration.t -> Pp.t; - print_library_entry : bool -> (object_name * Lib.node) -> Pp.t option; - print_context : bool -> int option -> Lib.library_segment -> Pp.t; + print_named_decl : env -> Evd.evar_map -> Context.Named.Declaration.t -> Pp.t; + print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; + print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; } @@ -487,25 +487,25 @@ let gallina_print_typed_value_in_env env sigma (trm,typ) = the pretty-print of a proposition (P:(nat->nat)->Prop)(P [u]u) synthesizes the type nat of the abstraction on u *) -let print_named_def name body typ = - let pbody = pr_lconstr body in - let ptyp = pr_ltype typ in +let print_named_def env sigma name body typ = + let pbody = pr_lconstr_env env sigma body in + let ptyp = pr_ltype_env env sigma typ in let pbody = if isCast body then surround pbody else pbody in (str "*** [" ++ str name ++ str " " ++ hov 0 (str ":=" ++ brk (1,2) ++ pbody ++ spc () ++ str ":" ++ brk (1,2) ++ ptyp) ++ str "]") -let print_named_assum name typ = - str "*** [" ++ str name ++ str " : " ++ pr_ltype typ ++ str "]" +let print_named_assum env sigma name typ = + str "*** [" ++ str name ++ str " : " ++ pr_ltype_env env sigma typ ++ str "]" -let gallina_print_named_decl = +let gallina_print_named_decl env sigma = let open Context.Named.Declaration in function | LocalAssum (id, typ) -> - print_named_assum (Id.to_string id) typ + print_named_assum env sigma (Id.to_string id) typ | LocalDef (id, body, typ) -> - print_named_def (Id.to_string id) body typ + print_named_def env sigma (Id.to_string id) body typ let assumptions_for_print lna = List.fold_right (fun na env -> add_name na env) lna empty_names_context @@ -524,11 +524,11 @@ let gallina_print_inductive sp = print_inductive_implicit_args sp mipv @ print_inductive_argument_scopes sp mipv) -let print_named_decl id = - gallina_print_named_decl (Global.lookup_named id) ++ fnl () +let print_named_decl env sigma id = + gallina_print_named_decl env sigma (Global.lookup_named id) ++ fnl () -let gallina_print_section_variable id = - print_named_decl id ++ +let gallina_print_section_variable env sigma id = + print_named_decl env sigma id ++ with_line_skip (print_name_infos (VarRef id)) let print_body env evd = function @@ -601,7 +601,7 @@ let gallina_print_constant_with_infos sp = print_constant true " = " sp ++ with_line_skip (print_name_infos (ConstRef sp)) -let gallina_print_syntactic_def kn = +let gallina_print_syntactic_def env kn = let qid = Nametab.shortest_qualid_of_syndef Id.Set.empty kn and (vars,a) = Syntax_def.search_syntactic_definition kn in let c = Notation_ops.glob_constr_of_notation_constr a in @@ -612,16 +612,16 @@ let gallina_print_syntactic_def kn = spc () ++ str ":=") ++ spc () ++ Constrextern.without_specific_symbols - [Notation.SynDefRule kn] pr_glob_constr c) + [Notation.SynDefRule kn] (pr_glob_constr_env env) c) -let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) = +let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) = let sep = if with_values then " = " else " : " and tag = object_tag lobj in match (oname,tag) with | (_,"VARIABLE") -> (* Outside sections, VARIABLES still exist but only with universes constraints *) - (try Some(print_named_decl (basename sp)) with Not_found -> None) + (try Some(print_named_decl env sigma (basename sp)) with Not_found -> None) | (_,"CONSTANT") -> Some (print_constant with_values sep (Constant.make1 kn)) | (_,"INDUCTIVE") -> @@ -637,11 +637,11 @@ let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) = (* To deal with forgotten cases... *) | (_,s) -> None -let gallina_print_library_entry with_values ent = +let gallina_print_library_entry env sigma with_values ent = let pr_name (sp,_) = Id.print (basename sp) in match ent with | (oname,Lib.Leaf lobj) -> - gallina_print_leaf_entry with_values (oname,lobj) + gallina_print_leaf_entry env sigma with_values (oname,lobj) | (oname,Lib.OpenedSection (dir,_)) -> Some (str " >>>>>>> Section " ++ pr_name oname) | (oname,Lib.ClosedSection _) -> @@ -653,10 +653,10 @@ let gallina_print_library_entry with_values ent = | (oname,Lib.ClosedModule _) -> Some (str " >>>>>>> Closed Module " ++ pr_name oname) -let gallina_print_context with_values = +let gallina_print_context env sigma with_values = let rec prec n = function | h::rest when Option.is_empty n || Option.get n > 0 -> - (match gallina_print_library_entry with_values h with + (match gallina_print_library_entry env sigma with_values h with | None -> prec n rest | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ()) | _ -> mt () @@ -718,10 +718,10 @@ let print_safe_judgment env sigma j = (*********************) (* *) -let print_full_context () = print_context true None (Lib.contents ()) -let print_full_context_typ () = print_context false None (Lib.contents ()) +let print_full_context env sigma = print_context env sigma true None (Lib.contents ()) +let print_full_context_typ env sigma = print_context env sigma false None (Lib.contents ()) -let print_full_pure_context () = +let print_full_pure_context env sigma = let rec prec = function | ((_,kn),Lib.Leaf lobj)::rest -> let pp = match object_tag lobj with @@ -733,15 +733,15 @@ let print_full_pure_context () = match cb.const_body with | Undef _ -> str "Parameter " ++ - print_basename con ++ str " : " ++ cut () ++ pr_ltype typ + print_basename con ++ str " : " ++ cut () ++ pr_ltype_env env sigma typ | OpaqueDef lc -> str "Theorem " ++ print_basename con ++ cut () ++ - str " : " ++ pr_ltype typ ++ str "." ++ fnl () ++ - str "Proof " ++ pr_lconstr (Opaqueproof.force_proof (Global.opaque_tables ()) lc) + str " : " ++ pr_ltype_env env sigma typ ++ str "." ++ fnl () ++ + str "Proof " ++ pr_lconstr_env env sigma (Opaqueproof.force_proof (Global.opaque_tables ()) lc) | Def c -> str "Definition " ++ print_basename con ++ cut () ++ - str " : " ++ pr_ltype typ ++ cut () ++ str " := " ++ - pr_lconstr (Mod_subst.force_constr c)) + str " : " ++ pr_ltype_env env sigma typ ++ cut () ++ str " := " ++ + pr_lconstr_env env sigma (Mod_subst.force_constr c)) ++ str "." ++ fnl () ++ fnl () | "INDUCTIVE" -> let mind = Global.mind_of_delta_kn kn in @@ -787,18 +787,18 @@ let read_sec_context r = let cxt = Lib.contents () in List.rev (get_cxt [] cxt) -let print_sec_context sec = - print_context true None (read_sec_context sec) +let print_sec_context env sigma sec = + print_context env sigma true None (read_sec_context sec) -let print_sec_context_typ sec = - print_context false None (read_sec_context sec) +let print_sec_context_typ env sigma sec = + print_context env sigma false None (read_sec_context sec) -let print_any_name = function +let print_any_name env sigma = function | Term (ConstRef sp) -> print_constant_with_infos sp | Term (IndRef (sp,_)) -> print_inductive sp | Term (ConstructRef ((sp,_),_)) -> print_inductive sp - | Term (VarRef sp) -> print_section_variable sp - | Syntactic kn -> print_syntactic_def kn + | Term (VarRef sp) -> print_section_variable env sigma sp + | Syntactic kn -> print_syntactic_def env kn | Dir (DirModule(dirpath,(mp,_))) -> print_module (printable_body dirpath) mp | Dir _ -> mt () | ModuleType mp -> print_modtype mp @@ -807,22 +807,21 @@ let print_any_name = function try (* Var locale de but, pas var de section... donc pas d'implicits *) let dir,str = repr_qualid qid in if not (DirPath.is_empty dir) then raise Not_found; - str |> Global.lookup_named |> print_named_decl + str |> Global.lookup_named |> print_named_decl env sigma with Not_found -> user_err ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") -let print_name = function +let print_name env sigma = function | ByNotation (loc,(ntn,sc)) -> - print_any_name + print_any_name env sigma (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)) | AN ref -> - print_any_name (locate_any_name ref) + print_any_name env sigma (locate_any_name ref) -let print_opaque_name qid = - let env = Global.env () in +let print_opaque_name env sigma qid = match Nametab.global qid with | ConstRef cst -> let cb = Global.lookup_constant cst in @@ -840,9 +839,9 @@ let print_opaque_name qid = let open EConstr in print_typed_value (mkConstruct cstr, ty) | VarRef id -> - env |> lookup_named id |> print_named_decl + env |> lookup_named id |> print_named_decl env sigma -let print_about_any ?loc k = +let print_about_any ?loc env sigma k = match k with | Term ref -> let rb = Reductionops.ReductionBehaviour.print ref in @@ -858,23 +857,23 @@ let print_about_any ?loc k = | [],Notation_term.NRef ref -> Dumpglob.add_glob ?loc ref | _ -> () in v 0 ( - print_syntactic_def kn ++ fnl () ++ + print_syntactic_def env kn ++ fnl () ++ hov 0 (str "Expands to: " ++ pr_located_qualid k)) | Dir _ | ModuleType _ | Undefined _ -> hov 0 (pr_located_qualid k) | Other (obj, info) -> hov 0 (info.about obj) -let print_about = function +let print_about env sigma = function | ByNotation (loc,(ntn,sc)) -> - print_about_any ?loc + print_about_any ?loc env sigma (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)) | AN ref -> - print_about_any ?loc:(loc_of_reference ref) (locate_any_name ref) + print_about_any ?loc:(loc_of_reference ref) env sigma (locate_any_name ref) (* for debug *) -let inspect depth = - print_context false (Some depth) (Lib.contents ()) +let inspect env sigma depth = + print_context env sigma false (Some depth) (Lib.contents ()) (*************************************************************************) @@ -882,18 +881,20 @@ let inspect depth = open Classops -let print_coercion_value v = pr_lconstr (get_coercion_value v) +let print_coercion_value env sigma v = pr_lconstr_env env sigma (get_coercion_value v) let print_class i = let cl,_ = class_info_from_index i in pr_class cl let print_path ((i,j),p) = + let sigma, env = Pfedit.get_current_context () in hov 2 ( - str"[" ++ hov 0 (prlist_with_sep pr_semicolon print_coercion_value p) ++ + str"[" ++ hov 0 (prlist_with_sep pr_semicolon (print_coercion_value env sigma) p) ++ str"] : ") ++ print_class i ++ str" >-> " ++ print_class j +(* XXX: This is suspicious!!! *) let _ = Classops.install_path_printer print_path let print_graph () = @@ -902,8 +903,8 @@ let print_graph () = let print_classes () = pr_sequence pr_class (classes()) -let print_coercions () = - pr_sequence print_coercion_value (coercions()) +let print_coercions env sigma = + pr_sequence (print_coercion_value env sigma) (coercions()) let index_of_class cl = try @@ -925,11 +926,11 @@ let print_path_between cls clt = in print_path ((i,j),p) -let print_canonical_projections () = +let print_canonical_projections env sigma = prlist_with_sep fnl (fun ((r1,r2),o) -> pr_cs_pattern r2 ++ str " <- " ++ - pr_global r1 ++ str " ( " ++ pr_lconstr o.o_DEF ++ str " )") + pr_global r1 ++ str " ( " ++ pr_lconstr_env env sigma o.o_DEF ++ str " )") (canonical_projections ()) (*************************************************************************) diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 31fd766ea..89099a043 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -18,37 +18,37 @@ open Misctypes val assumptions_for_print : Name.t list -> Termops.names_context val print_closed_sections : bool ref -val print_context : bool -> int option -> Lib.library_segment -> Pp.t -val print_library_entry : bool -> (object_name * Lib.node) -> Pp.t option -val print_full_context : unit -> Pp.t -val print_full_context_typ : unit -> Pp.t -val print_full_pure_context : unit -> Pp.t -val print_sec_context : reference -> Pp.t -val print_sec_context_typ : reference -> Pp.t +val print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t +val print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option +val print_full_context : env -> Evd.evar_map -> Pp.t +val print_full_context_typ : env -> Evd.evar_map -> Pp.t +val print_full_pure_context : env -> Evd.evar_map -> Pp.t +val print_sec_context : env -> Evd.evar_map -> reference -> Pp.t +val print_sec_context_typ : env -> Evd.evar_map -> reference -> Pp.t val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> Pp.t val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> Pp.t val print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t -val print_name : reference or_by_notation -> Pp.t -val print_opaque_name : reference -> Pp.t -val print_about : reference or_by_notation -> Pp.t +val print_name : env -> Evd.evar_map -> reference or_by_notation -> Pp.t +val print_opaque_name : env -> Evd.evar_map -> reference -> Pp.t +val print_about : env -> Evd.evar_map -> reference or_by_notation -> Pp.t val print_impargs : reference or_by_notation -> Pp.t (** Pretty-printing functions for classes and coercions *) val print_graph : unit -> Pp.t val print_classes : unit -> Pp.t -val print_coercions : unit -> Pp.t +val print_coercions : env -> Evd.evar_map -> Pp.t val print_path_between : Classops.cl_typ -> Classops.cl_typ -> Pp.t -val print_canonical_projections : unit -> Pp.t +val print_canonical_projections : env -> Evd.evar_map -> Pp.t (** Pretty-printing functions for type classes and instances *) val print_typeclasses : unit -> Pp.t val print_instances : global_reference -> Pp.t val print_all_instances : unit -> Pp.t -val inspect : int -> Pp.t +val inspect : env -> Evd.evar_map -> int -> Pp.t (** {5 Locate} *) @@ -82,15 +82,15 @@ val print_located_other : string -> reference -> Pp.t type object_pr = { print_inductive : MutInd.t -> Pp.t; print_constant_with_infos : Constant.t -> Pp.t; - print_section_variable : variable -> Pp.t; - print_syntactic_def : KerName.t -> Pp.t; + print_section_variable : env -> Evd.evar_map -> variable -> Pp.t; + print_syntactic_def : env -> KerName.t -> Pp.t; print_module : bool -> ModPath.t -> Pp.t; print_modtype : ModPath.t -> Pp.t; - print_named_decl : Context.Named.Declaration.t -> Pp.t; - print_library_entry : bool -> (object_name * Lib.node) -> Pp.t option; - print_context : bool -> int option -> Lib.library_segment -> Pp.t; + print_named_decl : env -> Evd.evar_map -> Context.Named.Declaration.t -> Pp.t; + print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; + print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; - print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t + print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; } val set_object_pr : object_pr -> unit diff --git a/printing/printer.ml b/printing/printer.ml index 075b03b7d..377a6b4e1 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -26,9 +26,6 @@ module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration module CompactedDecl = Context.Compacted.Declaration -let get_current_context () = - Pfedit.get_current_context () - let enable_unfocused_goal_printing = ref false let enable_goal_tags_printing = ref false let enable_goal_names_printing = ref false @@ -104,10 +101,10 @@ let pr_econstr_env env sigma c = pr_econstr_core false env sigma c (* NB do not remove the eta-redexes! Global.env() has side-effects... *) let pr_lconstr t = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in pr_lconstr_env env sigma t let pr_constr t = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in pr_constr_env env sigma t let pr_open_lconstr (_,c) = pr_lconstr c @@ -127,10 +124,10 @@ let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_econstr_env let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_leconstr_env let pr_constr_under_binders c = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in pr_constr_under_binders_env env sigma c let pr_lconstr_under_binders c = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in pr_lconstr_under_binders_env env sigma c let pr_etype_core goal_concl_style env sigma t = @@ -142,10 +139,10 @@ let pr_ltype_env env sigma c = pr_letype_core false env sigma (EConstr.of_constr let pr_type_env env sigma c = pr_etype_core false env sigma (EConstr.of_constr c) let pr_ltype t = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in pr_ltype_env env sigma t let pr_type t = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in pr_type_env env sigma t let pr_etype_env env sigma c = pr_etype_core false env sigma c @@ -156,7 +153,7 @@ let pr_ljudge_env env sigma j = (pr_leconstr_env env sigma j.uj_val, pr_leconstr_env env sigma j.uj_type) let pr_ljudge j = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in pr_ljudge_env env sigma j let pr_lglob_constr_env env c = @@ -165,10 +162,10 @@ let pr_glob_constr_env env c = pr_constr_expr (extern_glob_constr (Termops.vars_of_env env) c) let pr_lglob_constr c = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in pr_lglob_constr_env env c let pr_glob_constr c = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in pr_glob_constr_env env c let pr_closed_glob_n_env env sigma n c = @@ -176,7 +173,7 @@ let pr_closed_glob_n_env env sigma n c = let pr_closed_glob_env env sigma c = pr_constr_expr (extern_closed_glob false env sigma c) let pr_closed_glob c = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in pr_closed_glob_env env sigma c let pr_lconstr_pattern_env env sigma c = @@ -188,10 +185,10 @@ let pr_cases_pattern t = pr_cases_pattern_expr (extern_cases_pattern Names.Id.Set.empty t) let pr_lconstr_pattern t = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in pr_lconstr_pattern_env env sigma t let pr_constr_pattern t = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in pr_constr_pattern_env env sigma t let pr_sort sigma s = pr_glob_sort (extern_sort sigma s) @@ -253,11 +250,11 @@ let safe_gen f env sigma c = let safe_pr_lconstr_env = safe_gen pr_lconstr_env let safe_pr_constr_env = safe_gen pr_constr_env let safe_pr_lconstr t = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in safe_pr_lconstr_env env sigma t let safe_pr_constr t = - let (sigma, env) = get_current_context () in + let (sigma, env) = Pfedit.get_current_context () in safe_pr_constr_env env sigma t let pr_universe_ctx sigma c = @@ -788,7 +785,7 @@ let pr_goal x = !printer_pr.pr_goal x (* End abstraction layer *) (**********************************************************************) -let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = +let pr_open_subgoals ~proof = (* spiwack: it shouldn't be the job of the printer to look up stuff in the [evar_map], I did stuff that way because it was more straightforward, but seriously, [Proof.proof] should return @@ -826,15 +823,13 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = pr_subgoals ~pr_first:true None bsigma seeds shelf [] unfocused_if_needed bgoals_focused end -let pr_nth_open_subgoal n = - let pf = Proof_global.give_me_the_proof () in - let { it=gls ; sigma=sigma } = Proof.V82.subgoals pf in +let pr_nth_open_subgoal ~proof n = + let gls,_,_,_,sigma = Proof.proof proof in pr_subgoal n sigma gls -let pr_goal_by_id id = - let p = Proof_global.give_me_the_proof () in +let pr_goal_by_id ~proof id = try - Proof.in_proof p (fun sigma -> + Proof.in_proof proof (fun sigma -> let g = Evd.evar_key id sigma in pr_selected_subgoal (pr_id id) sigma g) with Not_found -> user_err Pp.(str "No such goal.") @@ -916,7 +911,7 @@ let pr_assumptionset env s = with e when CErrors.noncritical e -> mt () in let safe_pr_ltype_relctx (rctx, typ) = - let sigma, env = get_current_context () in + let sigma, env = Pfedit.get_current_context () in let env = Environ.push_rel_context rctx env in try str " " ++ pr_ltype_env env sigma typ with e when CErrors.noncritical e -> mt () diff --git a/printing/printer.mli b/printing/printer.mli index fbba14ede..e014baa2c 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -27,10 +27,12 @@ val enable_goal_names_printing : bool ref val pr_lconstr_env : env -> evar_map -> constr -> Pp.t val pr_lconstr : constr -> Pp.t +[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_lconstr_goal_style_env : env -> evar_map -> constr -> Pp.t val pr_constr_env : env -> evar_map -> constr -> Pp.t val pr_constr : constr -> Pp.t +[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_constr_goal_style_env : env -> evar_map -> constr -> Pp.t val pr_constr_n_env : env -> evar_map -> Notation_term.tolerability -> constr -> Pp.t @@ -41,14 +43,18 @@ val pr_constr_n_env : env -> evar_map -> Notation_term.tolerability -> co val safe_pr_lconstr_env : env -> evar_map -> constr -> Pp.t val safe_pr_lconstr : constr -> Pp.t +[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val safe_pr_constr_env : env -> evar_map -> constr -> Pp.t val safe_pr_constr : constr -> Pp.t +[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_econstr_env : env -> evar_map -> EConstr.t -> Pp.t val pr_econstr : EConstr.t -> Pp.t +[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_leconstr_env : env -> evar_map -> EConstr.t -> Pp.t val pr_leconstr : EConstr.t -> Pp.t +[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_econstr_n_env : env -> evar_map -> Notation_term.tolerability -> EConstr.t -> Pp.t @@ -57,41 +63,53 @@ val pr_letype_env : env -> evar_map -> EConstr.types -> Pp.t val pr_open_constr_env : env -> evar_map -> open_constr -> Pp.t val pr_open_constr : open_constr -> Pp.t +[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_open_lconstr_env : env -> evar_map -> open_constr -> Pp.t val pr_open_lconstr : open_constr -> Pp.t +[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_constr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp.t val pr_constr_under_binders : constr_under_binders -> Pp.t +[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp.t val pr_lconstr_under_binders : constr_under_binders -> Pp.t +[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_goal_concl_style_env : env -> evar_map -> EConstr.types -> Pp.t val pr_ltype_env : env -> evar_map -> types -> Pp.t val pr_ltype : types -> Pp.t +[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_type_env : env -> evar_map -> types -> Pp.t val pr_type : types -> Pp.t +[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_closed_glob_n_env : env -> evar_map -> Notation_term.tolerability -> closed_glob_constr -> Pp.t val pr_closed_glob_env : env -> evar_map -> closed_glob_constr -> Pp.t val pr_closed_glob : closed_glob_constr -> Pp.t +[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_ljudge_env : env -> evar_map -> EConstr.unsafe_judgment -> Pp.t * Pp.t val pr_ljudge : EConstr.unsafe_judgment -> Pp.t * Pp.t +[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_lglob_constr_env : env -> 'a glob_constr_g -> Pp.t val pr_lglob_constr : 'a glob_constr_g -> Pp.t +[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_glob_constr_env : env -> 'a glob_constr_g -> Pp.t val pr_glob_constr : 'a glob_constr_g -> Pp.t +[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_lconstr_pattern_env : env -> evar_map -> constr_pattern -> Pp.t val pr_lconstr_pattern : constr_pattern -> Pp.t +[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_constr_pattern_env : env -> evar_map -> constr_pattern -> Pp.t val pr_constr_pattern : constr_pattern -> Pp.t +[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_cases_pattern : cases_pattern -> Pp.t @@ -166,8 +184,8 @@ val pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> evar l val pr_subgoal : int -> evar_map -> goal list -> Pp.t val pr_concl : int -> evar_map -> goal -> Pp.t -val pr_open_subgoals : ?proof:Proof.proof -> unit -> Pp.t -val pr_nth_open_subgoal : int -> Pp.t +val pr_open_subgoals : proof:Proof.proof -> Pp.t +val pr_nth_open_subgoal : proof:Proof.proof -> int -> Pp.t val pr_evar : evar_map -> (evar * evar_info) -> Pp.t val pr_evars_int : evar_map -> int -> evar_info Evar.Map.t -> Pp.t val pr_evars : evar_map -> evar_info Evar.Map.t -> Pp.t @@ -200,13 +218,13 @@ module ContextObjectMap : CMap.ExtS val pr_assumptionset : env -> types ContextObjectMap.t -> Pp.t -val pr_goal_by_id : Id.t -> Pp.t +val pr_goal_by_id : proof:Proof.proof -> Id.t -> Pp.t type printer_pr = { pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t; pr_subgoal : int -> evar_map -> goal list -> Pp.t; pr_goal : goal sigma -> Pp.t; -};; +} val set_printer_pr : printer_pr -> unit diff --git a/printing/printmod.ml b/printing/printmod.ml index 0abca0160..13a03e9b4 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -374,9 +374,12 @@ let rec print_typ_expr env mp locals mty = | MEwith(me,WithDef(idl,(c, _)))-> let env' = None in (* TODO: build a proper environment if env <> None *) let s = String.concat "." (List.map Id.to_string idl) in + (* XXX: What should env and sigma be here? *) + let env = Global.env () in + let sigma = Evd.empty in hov 2 (print_typ_expr env' mp locals me ++ spc() ++ str "with" ++ spc() ++ def "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc() - ++ Printer.pr_lconstr c) + ++ Printer.pr_lconstr_env env sigma c) | MEwith(me,WithMod(idl,mp'))-> let s = String.concat "." (List.map Id.to_string idl) in hov 2 (print_typ_expr env mp locals me ++ spc() ++ str "with" ++ spc() ++ diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 2d4aba17c..c526ae000 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -51,9 +51,8 @@ end let get_nth_V82_goal i = let p = Proof_global.give_me_the_proof () in - let { it=goals ; sigma = sigma; } = Proof.V82.subgoals p in - try - { it=(List.nth goals (i-1)) ; sigma=sigma; } + let goals,_,_,_,sigma = Proof.proof p in + try { it = List.nth goals (i-1) ; sigma } with Failure _ -> raise NoSuchGoal let get_goal_context_gen i = diff --git a/proofs/proof.ml b/proofs/proof.ml index e24d57f08..413b5fdd7 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -163,6 +163,7 @@ let map_structured_proof pfts process_goal: 'a pre_goals = let rec unroll_focus pv = function | (_,_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk | [] -> pv + (* spiwack: a proof is considered completed even if its still focused, if the focus doesn't hide any goal. Unfocusing is handled in {!return}. *) @@ -391,10 +392,12 @@ let pr_proof p = (*** Compatibility layer with <=v8.2 ***) module V82 = struct let subgoals p = - Proofview.V82.goals p.proofview + let it, sigma = Proofview.proofview p.proofview in + Evd.{ it; sigma } let background_subgoals p = - Proofview.V82.goals (unroll_focus p.proofview p.focus_stack) + let it, sigma = Proofview.proofview (unroll_focus p.proofview p.focus_stack) in + Evd.{ it; sigma } let top_goal p = let { Evd.it=gls ; sigma=sigma; } = diff --git a/proofs/proof.mli b/proofs/proof.mli index 48aed8225..5756d06b6 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -65,7 +65,6 @@ val map_structured_proof : proof -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre (*** General proof functions ***) - val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> proof val dependent_start : Proofview.telescope -> proof val initial_goals : proof -> (EConstr.constr * EConstr.types) list @@ -187,6 +186,7 @@ val pr_proof : proof -> Pp.t (*** Compatibility layer with <=v8.2 ***) module V82 : sig val subgoals : proof -> Goal.goal list Evd.sigma + [@@ocaml.deprecated "Use the first and fifth argument of [Proof.proof]"] (* All the subgoals of the proof, including those which are not focused. *) val background_subgoals : proof -> Goal.goal list Evd.sigma diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index 01b75e496..77642946c 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -46,7 +46,7 @@ let simple_goal sigma g gs = let is_focused_goal_simple ~doc id = match state_of_id ~doc id with | `Expired | `Error _ | `Valid None -> `Not - | `Valid (Some { Vernacentries.proof }) -> + | `Valid (Some { Vernacstate.proof }) -> let proof = Proof_global.proof_of_state proof in let focused, r1, r2, r3, sigma = Proof.proof proof in let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in diff --git a/stm/stm.ml b/stm/stm.ml index b394c3a13..a9cbcc9a6 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -25,14 +25,14 @@ open Vernacexpr (* Protect against state changes *) let stm_purify f x = - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in try let res = f x in - Vernacentries.unfreeze_interp_state st; + Vernacstate.unfreeze_interp_state st; res with e -> let e = CErrors.push e in - Vernacentries.unfreeze_interp_state st; + Vernacstate.unfreeze_interp_state st; Exninfo.iraise e let execution_error ?loc state_id msg = @@ -165,7 +165,7 @@ let summary_pstate = [ Evarutil.meta_counter_summary_name; type cached_state = | Empty | Error of Exninfo.iexn - | Valid of Vernacentries.interp_state + | Valid of Vernacstate.t type branch = Vcs_.Branch.t * branch_type Vcs_.branch_info type backup = { mine : branch; others : branch list } @@ -735,16 +735,16 @@ module State : sig val exn_on : Stateid.t -> valid:Stateid.t -> Exninfo.iexn -> Exninfo.iexn (* to send states across worker/master *) - val get_cached : Stateid.t -> Vernacentries.interp_state - val same_env : Vernacentries.interp_state -> Vernacentries.interp_state -> bool + val get_cached : Stateid.t -> Vernacstate.t + val same_env : Vernacstate.t -> Vernacstate.t -> bool type proof_part type partial_state = - [ `Full of Vernacentries.interp_state + [ `Full of Vernacstate.t | `ProofOnly of Stateid.t * proof_part ] - val proof_part_of_frozen : Vernacentries.interp_state -> proof_part + val proof_part_of_frozen : Vernacstate.t -> proof_part val assign : Stateid.t -> partial_state -> unit (* Handlers for initial state, prior to document creation. *) @@ -757,8 +757,6 @@ module State : sig end = struct (* {{{ *) - open Vernacentries - (* cur_id holds Stateid.dummy in case the last attempt to define a state * failed, so the global state may contain garbage *) let cur_id = ref Stateid.dummy @@ -768,15 +766,15 @@ end = struct (* {{{ *) Proof_global.state * Summary.frozen_bits (* only meta counters *) type partial_state = - [ `Full of Vernacentries.interp_state + [ `Full of Vernacstate.t | `ProofOnly of Stateid.t * proof_part ] - let proof_part_of_frozen { Vernacentries.proof; system } = + let proof_part_of_frozen { Vernacstate.proof; system } = proof, Summary.project_summary (States.summary_of_state system) summary_pstate let freeze marshallable id = - VCS.set_state id (Valid (Vernacentries.freeze_interp_state marshallable)) + VCS.set_state id (Valid (Vernacstate.freeze_interp_state marshallable)) let freeze_invalid id iexn = VCS.set_state id (Error iexn) @@ -800,7 +798,7 @@ end = struct (* {{{ *) let install_cached id = match VCS.get_info id with | { state = Valid s } -> - Vernacentries.unfreeze_interp_state s; + Vernacstate.unfreeze_interp_state s; cur_id := id | { state = Error ie } -> @@ -819,6 +817,7 @@ end = struct (* {{{ *) with VCS.Expired -> anomaly Pp.(str "not a cached state (expired).") let assign id what = + let open Vernacstate in if VCS.get_state id <> Empty then () else try match what with | `Full s -> @@ -826,7 +825,7 @@ end = struct (* {{{ *) try let prev = (VCS.visit id).next in if is_cached_and_valid prev - then { s with Vernacentries.proof = + then { s with proof = Proof_global.copy_terminators ~src:(get_cached prev).proof ~tgt:s.proof } else s @@ -854,7 +853,7 @@ end = struct (* {{{ *) execution_error ?loc id (iprint (e, info)); (e, Stateid.add info ~valid id) - let same_env { system = s1 } { system = s2 } = + let same_env { Vernacstate.system = s1 } { Vernacstate.system = s2 } = let s1 = States.summary_of_state s1 in let e1 = Summary.project_summary s1 [Global.global_env_summary_name] in let s2 = States.summary_of_state s2 in @@ -902,11 +901,11 @@ end = struct (* {{{ *) let init_state = ref None let register_root_state () = - init_state := Some (Vernacentries.freeze_interp_state `No) + init_state := Some (Vernacstate.freeze_interp_state `No) let restore_root_state () = cur_id := Stateid.dummy; - Vernacentries.unfreeze_interp_state (Option.get !init_state); + Vernacstate.unfreeze_interp_state (Option.get !init_state); end (* }}} *) @@ -1001,7 +1000,7 @@ end (* Wrapper for Vernacentries.interp to set the feedback id *) (* It is currently called 19 times, this number should be certainly reduced... *) -let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacentries.interp_state = +let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t = (* The Stm will gain the capability to interpret commmads affecting the whole document state, such as backtrack, etc... so we start to design the stm command interpreter now *) @@ -1437,19 +1436,19 @@ end = struct (* {{{ *) * a bad fixpoint *) let fix_exn = Future.fix_exn_of future_proof in (* STATE: We use the current installed imperative state *) - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in if not drop then begin let checked_proof = Future.chain future_proof (fun p -> (* Unfortunately close_future_proof and friends are not pure so we need to set the state manually here *) - Vernacentries.unfreeze_interp_state st; + Vernacstate.unfreeze_interp_state st; let pobject, _ = Proof_global.close_future_proof ~feedback_id:stop (Future.from_val ~fix_exn p) in let terminator = (* The one sent by master is an InvalidKey *) Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in stm_vernac_interp stop ~proof:(pobject, terminator) st { verbose = false; loc; indentation = 0; strlen = 0; @@ -1457,7 +1456,7 @@ end = struct (* {{{ *) ignore(Future.join checked_proof); end; (* STATE: Restore the state XXX: handle exn *) - Vernacentries.unfreeze_interp_state st; + Vernacstate.unfreeze_interp_state st; RespBuiltProof(proof,time) with | e when CErrors.noncritical e || e = Stack_overflow -> @@ -1598,7 +1597,7 @@ end = struct (* {{{ *) * => takes nothing from the itermediate states. *) (* STATE We use the state resulting from reaching start. *) - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp stop ~proof st { verbose = false; loc; indentation = 0; strlen = 0; expr = (VernacEndProof (Proved (Opaque,None))) }); @@ -1855,7 +1854,7 @@ end = struct (* {{{ *) * => captures state id in a future closure, which will discard execution state but for the proof + univs. *) - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp r_state_fb st ast); let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in match Evd.(evar_body (find sigma r_goal)) with @@ -1895,7 +1894,7 @@ end = struct (* {{{ *) | VernacRedirect (_,(_,e)) -> find ~time ~fail e | VernacFail e -> find ~time ~fail:true e | e -> e, time, fail in find ~time:false ~fail:false e in - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in Vernacentries.with_fail st fail (fun () -> (if time then System.with_time !Flags.time else (fun x -> x)) (fun () -> ignore(TaskQueue.with_n_workers nworkers (fun queue -> @@ -1932,9 +1931,10 @@ end = struct (* {{{ *) let open Notations in match Future.join f with | Some (pt, uc) -> + let sigma, env = Pfedit.get_current_context () in stm_pperr_endline (fun () -> hov 0 ( str"g=" ++ int (Evar.repr gid) ++ spc () ++ - str"t=" ++ (Printer.pr_constr pt) ++ spc () ++ + str"t=" ++ (Printer.pr_constr_env env sigma pt) ++ spc () ++ str"uc=" ++ Termops.pr_evar_universe_context uc)); (if abstract then Tactics.tclABSTRACT None else (fun x -> x)) (V82.tactic (Refiner.tclPUSHEVARUNIVCONTEXT uc) <*> @@ -1989,7 +1989,7 @@ end = struct (* {{{ *) VCS.print (); Reach.known_state ~cache:`No r_where; (* STATE *) - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in try (* STATE SPEC: * - start: r_where @@ -2065,6 +2065,7 @@ let collect_proof keep cur hd brkind id = | id :: _ -> Names.Id.to_string id in let loc = (snd cur).loc in let rec is_defined_expr = function + | VernacEndProof (Proved (Transparent,_)) -> true | VernacTime (_, e) -> is_defined_expr e | VernacRedirect (_, (_, e)) -> is_defined_expr e | VernacTimeout (_, e) -> is_defined_expr e @@ -2203,7 +2204,7 @@ let known_state ?(redefine_qed=false) ~cache id = Proofview.give_up else Proofview.tclUNIT () end in match (VCS.get_info base_state).state with - | Valid { Vernacentries.proof } -> + | Valid { Vernacstate.proof } -> Proof_global.unfreeze proof; Proof_global.with_current_proof (fun _ p -> feedback ~id:id Feedback.AddedAxiom; @@ -2213,7 +2214,7 @@ let known_state ?(redefine_qed=false) ~cache id = * - end : maybe after recovery command. *) (* STATE: We use an updated state with proof *) - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in Option.iter (fun expr -> ignore(stm_vernac_interp id st { verbose = true; loc = None; expr; indentation = 0; strlen = 0 } )) @@ -2293,7 +2294,7 @@ let known_state ?(redefine_qed=false) ~cache id = resilient_tactic id cblock (fun () -> reach view.next; (* State resulting from reach *) - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x) ); if eff then update_global_env () @@ -2303,13 +2304,13 @@ let known_state ?(redefine_qed=false) ~cache id = | Flags.APon | Flags.APonLazy -> resilient_command reach view.next | Flags.APoff -> reach view.next); - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x); if eff then update_global_env () ), (if eff then `Yes else cache), true | `Fork ((x,_,_,_), None) -> (fun () -> resilient_command reach view.next; - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x); wall_clock_last_fork := Unix.gettimeofday () ), `Yes, true @@ -2318,7 +2319,7 @@ let known_state ?(redefine_qed=false) ~cache id = reach view.next; (try - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x); with e when CErrors.noncritical e -> let (e, info) = CErrors.push e in @@ -2369,7 +2370,7 @@ let known_state ?(redefine_qed=false) ~cache id = Proof_global.close_future_proof ~feedback_id:id fp in if not delegate then ignore(Future.compute fp); reach view.next; - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id ~proof st x); feedback ~id:id Incomplete | { VCS.kind = `Master }, _ -> assert false @@ -2378,7 +2379,7 @@ let known_state ?(redefine_qed=false) ~cache id = ), (if redefine_qed then `No else `Yes), true | `Sync (name, `Immediate) -> (fun () -> reach eop; - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x); Proof_global.discard_all () ), `Yes, true @@ -2401,7 +2402,7 @@ let known_state ?(redefine_qed=false) ~cache id = if keep != VtKeepAsAxiom then reach view.next; let wall_clock2 = Unix.gettimeofday () in - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id ?proof st x); let wall_clock3 = Unix.gettimeofday () in Aux_file.record_in_aux_at ?loc:x.loc "proof_check_time" @@ -2419,7 +2420,7 @@ let known_state ?(redefine_qed=false) ~cache id = aux (collect_proof keep (view.next, x) brname brinfo eop) | `Sideff (ReplayCommand x,_) -> (fun () -> reach view.next; - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x); update_global_env () ), cache, true @@ -2688,7 +2689,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) | VtQuery (false,route), VtNow -> let query_sid = VCS.cur_tip () in (try - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp ~route query_sid st x) with e -> let e = CErrors.push e in @@ -2762,7 +2763,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) (* Side effect on all branches *) | VtUnknown, _ when expr = VernacToplevelControl Drop -> - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp (VCS.get_branch_pos head) st x); `Ok @@ -2790,7 +2791,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) VCS.checkout VCS.Branch.master; let mid = VCS.get_branch_pos VCS.Branch.master in let _st' = Reach.known_state ~cache:(VCS.is_interactive ()) mid in - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x); (* Vernac x may or may not start a proof *) if not in_proof && Proof_global.there_are_pending_proofs () then diff --git a/stm/stm.mli b/stm/stm.mli index 31f4599d3..9fd35a0d3 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -220,7 +220,7 @@ val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t val get_doc : Feedback.doc_id -> doc val state_of_id : doc:doc -> - Stateid.t -> [ `Valid of Vernacentries.interp_state option | `Expired | `Error of exn ] + Stateid.t -> [ `Valid of Vernacstate.t option | `Expired | `Error of exn ] (* Queries for backward compatibility *) val current_proof_depth : doc:doc -> int diff --git a/tactics/auto.ml b/tactics/auto.ml index d0424eb89..fa8435d1f 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -388,7 +388,7 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db= Tacticals.New.tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl) else Tacticals.New.tclFAIL 0 (str"Unbound reference") end - | Extern tacast -> + | Extern tacast -> conclPattern concl p tacast in let pr_hint () = @@ -396,7 +396,8 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db= | None -> mt () | Some n -> str " (in " ++ str n ++ str ")" in - pr_hint t ++ origin + let sigma, env = Pfedit.get_current_context () in + pr_hint env sigma t ++ origin in tclLOG dbg pr_hint (run_hint t tactic) diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index e68087f14..6a9cd7e20 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -74,12 +74,12 @@ let find_matches bas pat = let res = HintDN.search_pattern base pat in List.map snd res -let print_rewrite_hintdb bas = +let print_rewrite_hintdb env sigma bas = (str "Database " ++ str bas ++ fnl () ++ prlist_with_sep fnl (fun h -> str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++ - Printer.pr_lconstr h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr h.rew_type ++ + Printer.pr_lconstr_env env sigma h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr_env env sigma h.rew_type ++ Option.cata (fun tac -> str " then use tactic " ++ Pputils.pr_glb_generic (Global.env()) tac) (mt ()) h.rew_tac) (find_rewrites bas)) diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index d2b5e070b..44acf3c01 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -40,7 +40,7 @@ val auto_multi_rewrite : ?conds:conditions -> string list -> Locus.clause -> uni val auto_multi_rewrite_with : ?conds:conditions -> unit Proofview.tactic -> string list -> Locus.clause -> unit Proofview.tactic -val print_rewrite_hintdb : string -> Pp.t +val print_rewrite_hintdb : Environ.env -> Evd.evar_map -> string -> Pp.t open Clenv diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index b98b10315..cee6d4bea 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -464,15 +464,16 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co in let tac = run_hint t tac in let tac = if complete then Tacticals.New.tclCOMPLETE tac else tac in + let _, env = Pfedit.get_current_context () in let pp = match p with | Some pat when get_typeclasses_filtered_unification () -> - str " with pattern " ++ Printer.pr_constr_pattern pat + str " with pattern " ++ Printer.pr_constr_pattern_env env sigma pat | _ -> mt () in match repr_hint t with - | Extern _ -> (tac, b, true, name, lazy (pr_hint t ++ pp)) - | _ -> (tac, b, false, name, lazy (pr_hint t ++ pp)) + | Extern _ -> (tac, b, true, name, lazy (pr_hint env sigma t ++ pp)) + | _ -> (tac, b, false, name, lazy (pr_hint env sigma t ++ pp)) in List.map tac_of_hint hintl and e_trivial_resolve db_list local_db secvars only_classes sigma concl = diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 239661498..f5c6ab879 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -178,7 +178,8 @@ and e_my_find_search sigma db_list local_db secvars hdc concl = | Extern tacast -> conclPattern concl p tacast in let tac = run_hint t tac in - (tac, lazy (pr_hint t))) + let sigma, env = Pfedit.get_current_context () in + (tac, lazy (pr_hint env sigma t))) in List.map tac_of_hint hintl diff --git a/tactics/hints.ml b/tactics/hints.ml index c7c53b393..70e84013b 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1392,14 +1392,14 @@ let make_db_list dbnames = (* Functions for printing the hints *) (**************************************************************************) -let pr_hint_elt (c, _, _) = pr_econstr c +let pr_hint_elt env sigma (c, _, _) = pr_econstr_env env sigma c -let pr_hint h = match h.obj with - | Res_pf (c, _) -> (str"simple apply " ++ pr_hint_elt c) - | ERes_pf (c, _) -> (str"simple eapply " ++ pr_hint_elt c) - | Give_exact (c, _) -> (str"exact " ++ pr_hint_elt c) +let pr_hint env sigma h = match h.obj with + | Res_pf (c, _) -> (str"simple apply " ++ pr_hint_elt env sigma c) + | ERes_pf (c, _) -> (str"simple eapply " ++ pr_hint_elt env sigma c) + | Give_exact (c, _) -> (str"exact " ++ pr_hint_elt env sigma c) | Res_pf_THEN_trivial_fail (c, _) -> - (str"simple apply " ++ pr_hint_elt c ++ str" ; trivial") + (str"simple apply " ++ pr_hint_elt env sigma c ++ str" ; trivial") | Unfold_nth c -> (str"unfold " ++ pr_evaluable_reference c) | Extern tac -> let env = @@ -1410,21 +1410,21 @@ let pr_hint h = match h.obj with in (str "(*external*) " ++ Pputils.pr_glb_generic env tac) -let pr_id_hint (id, v) = - let pr_pat p = str", pattern " ++ pr_lconstr_pattern p in - (pr_hint v.code ++ str"(level " ++ int v.pri ++ pr_opt_no_spc pr_pat v.pat +let pr_id_hint env sigma (id, v) = + let pr_pat p = str", pattern " ++ pr_lconstr_pattern_env env sigma p in + (pr_hint env sigma v.code ++ str"(level " ++ int v.pri ++ pr_opt_no_spc pr_pat v.pat ++ str", id " ++ int id ++ str ")" ++ spc ()) -let pr_hint_list hintlist = - (str " " ++ hov 0 (prlist pr_id_hint hintlist) ++ fnl ()) +let pr_hint_list env sigma hintlist = + (str " " ++ hov 0 (prlist (pr_id_hint env sigma) hintlist) ++ fnl ()) -let pr_hints_db (name,db,hintlist) = +let pr_hints_db env sigma (name,db,hintlist) = (str "In the database " ++ str name ++ str ":" ++ if List.is_empty hintlist then (str " nothing" ++ fnl ()) - else (fnl () ++ pr_hint_list hintlist)) + else (fnl () ++ pr_hint_list env sigma hintlist)) (* Print all hints associated to head c in any database *) -let pr_hint_list_for_head c = +let pr_hint_list_for_head env sigma c = let dbs = current_db () in let validate (name, db) = let hints = List.map (fun v -> 0, v) (Hint_db.map_all ~secvars:Id.Pred.full c db) in @@ -1436,13 +1436,13 @@ let pr_hint_list_for_head c = else hov 0 (str"For " ++ pr_global c ++ str" -> " ++ fnl () ++ - hov 0 (prlist pr_hints_db valid_dbs)) + hov 0 (prlist (pr_hints_db env sigma) valid_dbs)) let pr_hint_ref ref = pr_hint_list_for_head ref (* Print all hints associated to head id in any database *) -let pr_hint_term sigma cl = +let pr_hint_term env sigma cl = try let dbs = current_db () in let valid_dbs = @@ -1460,18 +1460,19 @@ let pr_hint_term sigma cl = (str "No hint applicable for current goal") else (str "Applicable Hints :" ++ fnl () ++ - hov 0 (prlist pr_hints_db valid_dbs)) + hov 0 (prlist (pr_hints_db env sigma) valid_dbs)) with Match_failure _ | Failure _ -> (str "No hint applicable for current goal") (* print all hints that apply to the concl of the current goal *) let pr_applicable_hint () = + let env = Global.env () in let pts = Proof_global.give_me_the_proof () in - let glss = Proof.V82.subgoals pts in - match glss.Evd.it with + let glss,_,_,_,sigma = Proof.proof pts in + match glss with | [] -> CErrors.user_err Pp.(str "No focused goal.") | g::_ -> - pr_hint_term glss.Evd.sigma (Goal.V82.concl glss.Evd.sigma g) + pr_hint_term env sigma (Goal.V82.concl sigma g) let pp_hint_mode = function | ModeInput -> str"+" @@ -1479,9 +1480,9 @@ let pp_hint_mode = function | ModeOutput -> str"-" (* displays the whole hint database db *) -let pr_hint_db db = +let pr_hint_db_env env sigma db = let pr_mode = prvect_with_sep spc pp_hint_mode in - let pr_modes l = + let pr_modes l = if List.is_empty l then mt () else str" (modes " ++ prlist_with_sep pr_comma pr_mode l ++ str")" in @@ -1491,7 +1492,7 @@ let pr_hint_db db = | None -> str "For any goal" | Some head -> str "For " ++ pr_global head ++ pr_modes modes in - let hints = pr_hint_list (List.map (fun x -> (0, x)) hintlist) in + let hints = pr_hint_list env sigma (List.map (fun x -> (0, x)) hintlist) in let hint_descr = hov 0 (goal_descr ++ str " -> " ++ hints) in accu ++ hint_descr in @@ -1506,17 +1507,21 @@ let pr_hint_db db = hov 2 (str"Cut: " ++ pp_hints_path (Hint_db.cut db)) ++ fnl () ++ content -let pr_hint_db_by_name dbname = +let pr_hint_db db = + let sigma, env = Pfedit.get_current_context () in + pr_hint_db_env env sigma db + +let pr_hint_db_by_name env sigma dbname = try - let db = searchtable_map dbname in pr_hint_db db + let db = searchtable_map dbname in pr_hint_db_env env sigma db with Not_found -> error_no_such_hint_database dbname (* displays all the hints of all databases *) -let pr_searchtable () = +let pr_searchtable env sigma = let fold name db accu = accu ++ str "In the database " ++ str name ++ str ":" ++ fnl () ++ - pr_hint_db db ++ fnl () + pr_hint_db_env env sigma db ++ fnl () in Hintdbmap.fold fold !searchtable (mt ()) @@ -1534,10 +1539,13 @@ let warn_non_imported_hint = strbrk "Hint used but not imported: " ++ hint ++ print_mp mp) let warn h x = - let hint = pr_hint h in - let (mp, _, _) = KerName.repr h.uid in - warn_non_imported_hint (hint,mp); - Proofview.tclUNIT x + let open Proofview in + tclBIND tclENV (fun env -> + tclBIND tclEVARMAP (fun sigma -> + let hint = pr_hint env sigma h in + let (mp, _, _) = KerName.repr h.uid in + warn_non_imported_hint (hint,mp); + Proofview.tclUNIT x)) let run_hint tac k = match !warn_hint with | `LAX -> k tac.obj diff --git a/tactics/hints.mli b/tactics/hints.mli index 22df29b80..cbf204981 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -260,14 +260,15 @@ val rewrite_db : hint_db_name (** Printing hints *) -val pr_searchtable : unit -> Pp.t +val pr_searchtable : env -> evar_map -> Pp.t val pr_applicable_hint : unit -> Pp.t -val pr_hint_ref : global_reference -> Pp.t -val pr_hint_db_by_name : hint_db_name -> Pp.t +val pr_hint_ref : env -> evar_map -> global_reference -> Pp.t +val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t +val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t val pr_hint_db : Hint_db.t -> Pp.t -val pr_hint : hint -> Pp.t +[@@ocaml.deprecated "please used pr_hint_db_env"] +val pr_hint : env -> evar_map -> hint -> Pp.t (** Hook for changing the initialization of auto *) - val add_hints_init : (unit -> unit) -> unit diff --git a/tactics/inv.ml b/tactics/inv.ml index 8648dfb90..46b10bf33 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -282,10 +282,11 @@ let generalizeRewriteIntros as_mode tac depids id = let error_too_many_names pats = let loc = Loc.merge_opt (fst (List.hd pats)) (fst (List.last pats)) in Proofview.tclENV >>= fun env -> + Proofview.tclEVARMAP >>= fun sigma -> tclZEROMSG ?loc ( str "Unexpected " ++ str (String.plural (List.length pats) "introduction pattern") ++ - str ": " ++ pr_enum (Miscprint.pr_intro_pattern (fun c -> Printer.pr_constr (EConstr.Unsafe.to_constr (snd (c env Evd.empty))))) pats ++ + str ": " ++ pr_enum (Miscprint.pr_intro_pattern (fun c -> Printer.pr_constr_env env sigma (EConstr.Unsafe.to_constr (snd (c env Evd.empty))))) pats ++ str ".") let get_names (allow_conj,issimple) (loc, pat as x) = match pat with diff --git a/tactics/leminv.ml b/tactics/leminv.ml index cc9d98f6f..62f3866de 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -215,7 +215,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = invEnv ~init:Context.Named.empty end in let avoid = ref Id.Set.empty in - let { sigma=sigma } = Proof.V82.subgoals pf in + let _,_,_,_,sigma = Proof.proof pf in let sigma = Evd.nf_constraints sigma in let rec fill_holes c = match EConstr.kind sigma c with diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 15c25b346..e072bd95f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -945,10 +945,14 @@ let reduction_clause redexp cl = (None, bind_red_expr_occurrences occs nbcl redexp)) cl let reduce redexp cl = - let trace () = + let trace env sigma = let open Printer in - let pr = (pr_econstr, pr_leconstr, pr_evaluable_reference, pr_constr_pattern) in - Pp.(hov 2 (Pputils.pr_red_expr pr str redexp)) + let pr = (pr_econstr_env, pr_leconstr_env, pr_evaluable_reference, pr_constr_pattern_env) in + Pp.(hov 2 (Pputils.pr_red_expr_env env sigma pr str redexp)) + in + let trace () = + let sigma, env = Pfedit.get_current_context () in + trace env sigma in Proofview.Trace.name_tactic trace begin Proofview.Goal.enter begin fun gl -> @@ -3128,11 +3132,11 @@ let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id] let warn_unused_intro_pattern env sigma = CWarnings.create ~name:"unused-intro-pattern" ~category:"tactics" - (fun names -> - strbrk"Unused introduction " ++ str (String.plural (List.length names) "pattern") - ++ str": " ++ prlist_with_sep spc - (Miscprint.pr_intro_pattern - (fun c -> Printer.pr_econstr (snd (c env sigma)))) names) + (fun names -> + strbrk"Unused introduction " ++ str (String.plural (List.length names) "pattern") ++ + str": " ++ prlist_with_sep spc + (Miscprint.pr_intro_pattern + (fun c -> Printer.pr_econstr_env env sigma (snd (c env sigma)))) names) let check_unused_names env sigma names = if not (List.is_empty names) then diff --git a/test-suite/bugs/closed/5761.v b/test-suite/bugs/closed/5761.v new file mode 100644 index 000000000..6f28d1981 --- /dev/null +++ b/test-suite/bugs/closed/5761.v @@ -0,0 +1,126 @@ +Set Primitive Projections. +Record mix := { a : nat ; b : a = a ; c : nat ; d : a = c ; e : nat ; f : nat }. +Ltac strip_args T ctor := + lazymatch type of ctor with + | context[T] + => match eval cbv beta in ctor with + | ?ctor _ => strip_args T ctor + | _ => ctor + end + end. +Ltac get_ctor T := + let full_ctor := constr:(ltac:(let x := fresh in intro x; econstructor; apply +x) : T -> T) in + let ctor := constr:(fun x : T => ltac:(let v := strip_args T (full_ctor x) in +exact v)) in + lazymatch ctor with + | fun _ => ?ctor => ctor + end. +Ltac uncurry_domain f := + lazymatch type of f with + | forall (a : ?A) (b : @ ?B a), _ + => uncurry_domain (fun ab : { a : A & B a } => f (projT1 ab) (projT2 ab)) + | _ => eval cbv beta in f + end. +Ltac get_of_sigma T := + let ctor := get_ctor T in + uncurry_domain ctor. +Ltac repeat_existT := + lazymatch goal with + | [ |- sigT _ ] => simple refine (existT _ _ _); [ repeat_existT | shelve ] + | _ => shelve + end. + Ltac prove_to_of_sigma_goal of_sigma := + let v := fresh "v" in + simple refine (exist _ _ (fun v => _ : id _ (of_sigma v) = v)); + try unfold of_sigma; + [ intro v; destruct v; repeat_existT + | cbv beta; + repeat match goal with + | [ |- context[projT2 ?k] ] + => let x := fresh "x" in + is_var k; + destruct k as [k x]; cbn [projT1 projT2] + end; + unfold id; reflexivity ]. +Ltac prove_to_of_sigma of_sigma := + constr:( + ltac:(prove_to_of_sigma_goal of_sigma) + : { to_sigma : _ | forall v, id to_sigma (of_sigma v) = v }). +Ltac get_to_sigma_gen of_sigma := + let v := prove_to_of_sigma of_sigma in + eval hnf in (proj1_sig v). +Ltac get_to_sigma T := + let of_sigma := get_of_sigma T in + get_to_sigma_gen of_sigma. +Definition to_sigma := ltac:(let v := get_to_sigma mix in exact v). +(* Error: +In nested Ltac calls to "get_to_sigma", "get_to_sigma_gen", +"prove_to_of_sigma", +"(_ : {to_sigma : _ | forall v, id to_sigma (of_sigma v) = v})" (with +of_sigma:=fun + ab : {_ + : {_ + : {ab : {_ : {a : nat & a = a} & nat} & + projT1 (projT1 ab) = projT2 ab} & nat} & nat} => + {| + a := projT1 (projT1 (projT1 (projT1 (projT1 ab)))); + b := projT2 (projT1 (projT1 (projT1 (projT1 ab)))); + c := projT2 (projT1 (projT1 (projT1 ab))); + d := projT2 (projT1 (projT1 ab)); + e := projT2 (projT1 ab); + f := projT2 ab |}) and "prove_to_of_sigma_goal", last call failed. +Anomaly "Uncaught exception Not_found." Please report at +http://coq.inria.fr/bugs/. +frame @ file "toplevel/coqtop.ml", line 640, characters 6-22 +frame @ file "list.ml", line 73, characters 12-15 +frame @ file "toplevel/vernac.ml", line 344, characters 2-13 +frame @ file "toplevel/vernac.ml", line 308, characters 14-75 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "lib/flags.ml", line 141, characters 19-40 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "lib/flags.ml", line 11, characters 15-18 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "toplevel/vernac.ml", line 167, characters 6-16 +frame @ file "toplevel/vernac.ml", line 151, characters 26-39 +frame @ file "stm/stm.ml", line 2365, characters 2-35 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "stm/stm.ml", line 2355, characters 4-48 +frame @ file "stm/stm.ml", line 2321, characters 4-100 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "stm/stm.ml", line 832, characters 6-10 +frame @ file "stm/stm.ml", line 2206, characters 10-32 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "stm/stm.ml", line 975, characters 8-81 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "vernac/vernacentries.ml", line 2216, characters 10-389 +frame @ file "lib/flags.ml", line 141, characters 19-40 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "lib/flags.ml", line 11, characters 15-18 +frame @ file "vernac/command.ml", line 150, characters 4-56 +frame @ file "interp/constrintern.ml", line 2046, characters 2-73 +frame @ file "pretyping/pretyping.ml", line 1194, characters 19-77 +frame @ file "pretyping/pretyping.ml", line 1155, characters 8-72 +frame @ file "pretyping/pretyping.ml", line 628, characters 23-65 +frame @ file "plugins/ltac/tacinterp.ml", line 2095, characters 21-61 +frame @ file "proofs/pfedit.ml", line 178, characters 6-22 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "proofs/pfedit.ml", line 174, characters 8-36 +frame @ file "proofs/proof.ml", line 351, characters 4-30 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "engine/proofview.ml", line 1222, characters 8-12 +frame @ file "plugins/ltac/tacinterp.ml", line 2020, characters 19-36 +frame @ file "plugins/ltac/tacinterp.ml", line 618, characters 4-70 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "plugins/ltac/tacinterp.ml", line 214, characters 6-9 +frame @ file "pretyping/pretyping.ml", line 1198, characters 19-62 +frame @ file "pretyping/pretyping.ml", line 1155, characters 8-72 +raise @ unknown +frame @ file "pretyping/pretyping.ml", line 628, characters 23-65 +frame @ file "plugins/ltac/tacinterp.ml", line 2095, characters 21-61 +frame @ file "proofs/pfedit.ml", line 178, characters 6-22 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "proofs/pfedit.ml", line 174, characters 8-36 +frame @ file "proofs/proof.ml", line 351, characters 4-30 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 + *) diff --git a/test-suite/bugs/closed/5762.v b/test-suite/bugs/closed/5762.v index edd5c8d73..55d36bd72 100644 --- a/test-suite/bugs/closed/5762.v +++ b/test-suite/bugs/closed/5762.v @@ -26,3 +26,9 @@ Reserved Notation "%% a" (at level 70). Record R := {g : forall {A} (a:A), a=a where "%% x" := (g x); k : %% 0 = eq_refl}. + +(* An extra example *) + +Module A. +Inductive I {A:Type} := C : # 0 -> I where "# I" := (I = I) : I_scope. +End A. diff --git a/test-suite/bugs/closed/5790.v b/test-suite/bugs/closed/5790.v new file mode 100644 index 000000000..6c93a3906 --- /dev/null +++ b/test-suite/bugs/closed/5790.v @@ -0,0 +1,7 @@ +Set Universe Polymorphism. +Section foo. +Context (v : Type). +Axiom a : True <-> False. + +Hint Resolve -> a. +End foo. diff --git a/test-suite/bugs/closed/gh6165.v b/test-suite/bugs/closed/gh6165.v new file mode 100644 index 000000000..b87a7caaf --- /dev/null +++ b/test-suite/bugs/closed/gh6165.v @@ -0,0 +1,5 @@ +(* -*- mode: coq; coq-prog-args: ("-quick") -*- *) + +Goal True. + abstract exact I. +Timeout 1 Defined. diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh index 7e0baaa8f..2428da731 100755 --- a/test-suite/coq-makefile/timing/run.sh +++ b/test-suite/coq-makefile/timing/run.sh @@ -41,6 +41,9 @@ for ext in "" .desired; do done done for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do + echo "cat $file" + cat "$file" + echo diff -u $file.desired.processed $file.processed || exit $? done @@ -56,6 +59,13 @@ make all TIMING=after -j2 || exit $? find ../per-file-before/ -name "*.before-timing" -exec 'cp' '{}' './' ';' make all.timing.diff -j2 || exit $? +echo "cat A.v.before-timing" +cat A.v.before-timing +echo +echo "cat A.v.after-timing" +cat A.v.after-timing +echo +echo "cat A.v.timing.diff" cat A.v.timing.diff echo diff --git a/test-suite/coqdoc/links.html.out b/test-suite/coqdoc/links.html.out index 70cbe5065..5e4b676c2 100644 --- a/test-suite/coqdoc/links.html.out +++ b/test-suite/coqdoc/links.html.out @@ -76,7 +76,7 @@ Various checks for coqdoc <br/> <span class="id" title="keyword">Inductive</span> <a name="eq"><span class="id" title="inductive">eq</span></a> (<span class="id" title="var">A</span>:<span class="id" title="keyword">Type</span>) (<span class="id" title="var">x</span>:<a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a>) : <span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> := <a name="eq_refl"><span class="id" title="constructor">eq_refl</span></a> : <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:></span></a><a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a><br/> <br/> -<span class="id" title="keyword">where</span> <a name="8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">"</span></a>x = y :> A" := (@<a class="idref" href="Coqdoc.links.html#eq"><span class="id" title="inductive">eq</span></a> <a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <span class="id" title="var">y</span>) : <span class="id" title="var">type_scope</span>.<br/> +<span class="id" title="keyword">where</span> <a name="8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">"</span></a>x = y :> A" := (@<a class="idref" href="Coqdoc.links.html#eq"><span class="id" title="inductive">eq</span></a> <span class="id" title="var">A</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) : <span class="id" title="var">type_scope</span>.<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="eq0"><span class="id" title="definition">eq0</span></a> := 0 <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:></span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> diff --git a/test-suite/coqdoc/links.tex.out b/test-suite/coqdoc/links.tex.out index 7d93189ae..f42db99dc 100644 --- a/test-suite/coqdoc/links.tex.out +++ b/test-suite/coqdoc/links.tex.out @@ -69,7 +69,7 @@ Various checks for coqdoc \coqdocnoindent \coqdoceol \coqdocnoindent -\coqdockw{where} \coqdef{Coqdoc.links.:type scope:x '=' x ':>' x}{"}{"}x = y :> A" := (@\coqref{Coqdoc.links.eq}{\coqdocinductive{eq}} \coqdocvariable{A} \coqdocvariable{x} \coqdocvar{y}) : \coqdocvar{type\_scope}.\coqdoceol +\coqdockw{where} \coqdef{Coqdoc.links.:type scope:x '=' x ':>' x}{"}{"}x = y :> A" := (@\coqref{Coqdoc.links.eq}{\coqdocinductive{eq}} \coqdocvar{A} \coqdocvar{x} \coqdocvar{y}) : \coqdocvar{type\_scope}.\coqdoceol \coqdocemptyline \coqdocnoindent \coqdockw{Definition} \coqdef{Coqdoc.links.eq0}{eq0}{\coqdocdefinition{eq0}} := 0 \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{=}} 0 \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{:>}} \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index 35c3057d8..c5d58ec1e 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -31,3 +31,10 @@ nat nat 0 0 +Ltac foo := + let x := intros ** in + let y := intros -> in + let v := constr:(nil) in + let w := () in + let z := 1 in + pose v diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v index 76c37625a..6adbe95dd 100644 --- a/test-suite/output/ltac.v +++ b/test-suite/output/ltac.v @@ -57,3 +57,14 @@ match goal with |- ?x*?y => idtac x end. match goal with H: context [?x*?y] |- _ => idtac x end. match goal with |- context [?x*?y] => idtac x end. Abort. + +(* Check printing of let in Ltac and Tactic Notation *) + +Ltac foo := + let x := intros in + let y := intros -> in + let v := constr:(@ nil True) in + let w := () in + let z := 1 in + pose v. +Print Ltac foo. diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index 9505a56e3..e86b3edb8 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -90,3 +90,9 @@ Check fun A (x :prod' bool A) => match x with #### 0 y 0 => 2 | _ => 1 end. Notation "##### x" := (pair' x) (at level 0, x at level 1). Check ##### 0 _ 0%bool 0%bool : prod' bool bool. Check fun A (x :prod' bool A) => match x with ##### 0 _ y 0%bool => 2 | _ => 1 end. + +(* 10. Check computation of binding variable through other notations *) +(* i should be detected as binding variable and the scopes not being checked *) + +Notation "'FUNNAT' i => t" := (fun i : nat => i = t) (at level 200). +Notation "'Funnat' i => t" := (FUNNAT i => t + i%nat) (at level 200). diff --git a/tools/coq-inferior.el b/tools/inferior-coq.el index b79d97d66..b79d97d66 100644 --- a/tools/coq-inferior.el +++ b/tools/inferior-coq.el diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index f3d5d9b85..c61a1fd41 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -844,8 +844,10 @@ let start () = exit 1 | _ -> flush_all(); - if !output_context then - Feedback.msg_notice Flags.(with_option raw_print Prettyp.print_full_pure_context () ++ fnl ()); + if !output_context then begin + let sigma, env = Pfedit.get_current_context () in + Feedback.msg_notice (Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ()) + end; Profile.print_profile (); exit 0 diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index cf63fbdc3..8fdaedbaf 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -100,7 +100,9 @@ let print_cmd_header ?loc com = Format.pp_print_flush !Topfmt.std_ft () let pr_open_cur_subgoals () = - try Printer.pr_open_subgoals () + try + let proof = Proof_global.give_me_the_proof () in + Printer.pr_open_subgoals ~proof with Proof_global.NoCurrentProof -> Pp.str "" (* Reenable when we get back to feedback printing *) diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 9e63df51d..51dd5cd4f 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -377,6 +377,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = Proofview.Goal.enter begin fun gl -> let type_of_pq = Tacmach.New.pf_unsafe_type_of gl p in let sigma = Tacmach.New.project gl in + let env = Tacmach.New.pf_env gl in let u,v = destruct_ind sigma type_of_pq in let lb_type_of_p = try @@ -389,7 +390,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = (str "Leibniz->boolean:" ++ str "You have to declare the" ++ str "decidability over " ++ - Printer.pr_econstr type_of_pq ++ + Printer.pr_econstr_env env sigma type_of_pq ++ str " first.") in Tacticals.New.tclZEROMSG err_msg @@ -442,6 +443,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = Proofview.Goal.enter begin fun gl -> let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in let sigma = Tacmach.New.project gl in + let env = Tacmach.New.pf_env gl in if EConstr.eq_constr sigma t1 t2 then aux q1 q2 else ( let u,v = try destruct_ind sigma tt1 @@ -461,7 +463,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = (str "boolean->Leibniz:" ++ str "You have to declare the" ++ str "decidability over " ++ - Printer.pr_econstr tt1 ++ + Printer.pr_econstr_env env sigma tt1 ++ str " first.") in user_err err_msg diff --git a/vernac/command.ml b/vernac/command.ml index be54f97b7..fd0027c40 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -22,7 +22,6 @@ open Globnames open Nameops open Constrexpr open Constrexpr_ops -open Topconstr open Constrintern open Nametab open Impargs @@ -551,12 +550,13 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in let impls = compute_internalization_env env0 ~impls (Inductive (params,true)) indnames fullarities indimpls in + let ntn_impls = compute_internalization_env env0 (Inductive (params,true)) indnames fullarities indimpls in let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in let constructors = Metasyntax.with_syntax_protection (fun () -> (* Temporary declaration of notations and scopes *) - List.iter (Metasyntax.set_notation_for_interpretation env_params impls) notations; + List.iter (Metasyntax.set_notation_for_interpretation env_params ntn_impls) notations; (* Interpret the constructor types *) List.map3 (interp_cstrs env_ar_params evdref impls) mldatas arities indl) () in diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index 2178a7caa..3a8e8fb43 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -76,7 +76,8 @@ let process_vernac_interp_error exn = match fst exn with | Tacred.ReductionTacticError e -> wrap_vernac_error exn (Himsg.explain_reduction_tactic_error e) | Logic.RefinerError e -> - wrap_vernac_error exn (Himsg.explain_refiner_error e) + let sigma, env = Pfedit.get_current_context () in + wrap_vernac_error exn (Himsg.explain_refiner_error env sigma e) | Nametab.GlobalizationError q -> wrap_vernac_error exn (str "The reference" ++ spc () ++ Libnames.pr_qualid q ++ diff --git a/vernac/himsg.ml b/vernac/himsg.ml index d15a811ba..839064aa0 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -92,9 +92,7 @@ let jv_nf_betaiotaevar sigma jl = (** Printers *) -let pr_lconstr c = quote (pr_lconstr c) let pr_lconstr_env e s c = quote (pr_lconstr_env e s c) -let pr_leconstr c = quote (pr_leconstr c) let pr_leconstr_env e s c = quote (pr_leconstr_env e s c) let pr_ljudge_env e s c = let v,t = pr_ljudge_env e s c in (quote v,quote t) @@ -1037,52 +1035,52 @@ let explain_typeclass_error env = function (* Refiner errors *) -let explain_refiner_bad_type arg ty conclty = +let explain_refiner_bad_type env sigma arg ty conclty = str "Refiner was given an argument" ++ brk(1,1) ++ - pr_lconstr arg ++ spc () ++ - str "of type" ++ brk(1,1) ++ pr_lconstr ty ++ spc () ++ - str "instead of" ++ brk(1,1) ++ pr_lconstr conclty ++ str "." + pr_lconstr_env env sigma arg ++ spc () ++ + str "of type" ++ brk(1,1) ++ pr_lconstr_env env sigma ty ++ spc () ++ + str "instead of" ++ brk(1,1) ++ pr_lconstr_env env sigma conclty ++ str "." let explain_refiner_unresolved_bindings l = str "Unable to find an instance for the " ++ str (String.plural (List.length l) "variable") ++ spc () ++ prlist_with_sep pr_comma Name.print l ++ str"." -let explain_refiner_cannot_apply t harg = +let explain_refiner_cannot_apply env sigma t harg = str "In refiner, a term of type" ++ brk(1,1) ++ - pr_lconstr t ++ spc () ++ str "could not be applied to" ++ brk(1,1) ++ - pr_lconstr harg ++ str "." + pr_lconstr_env env sigma t ++ spc () ++ str "could not be applied to" ++ brk(1,1) ++ + pr_lconstr_env env sigma harg ++ str "." -let explain_refiner_not_well_typed c = - str "The term " ++ pr_lconstr c ++ str " is not well-typed." +let explain_refiner_not_well_typed env sigma c = + str "The term " ++ pr_lconstr_env env sigma c ++ str " is not well-typed." let explain_intro_needs_product () = str "Introduction tactics needs products." -let explain_does_not_occur_in c hyp = - str "The term" ++ spc () ++ pr_lconstr c ++ spc () ++ +let explain_does_not_occur_in env sigma c hyp = + str "The term" ++ spc () ++ pr_lconstr_env env sigma c ++ spc () ++ str "does not occur in" ++ spc () ++ Id.print hyp ++ str "." -let explain_non_linear_proof c = - str "Cannot refine with term" ++ brk(1,1) ++ pr_lconstr c ++ +let explain_non_linear_proof env sigma c = + str "Cannot refine with term" ++ brk(1,1) ++ pr_lconstr_env env sigma c ++ spc () ++ str "because a metavariable has several occurrences." -let explain_meta_in_type c = - str "In refiner, a meta appears in the type " ++ brk(1,1) ++ pr_leconstr c ++ +let explain_meta_in_type env sigma c = + str "In refiner, a meta appears in the type " ++ brk(1,1) ++ pr_leconstr_env env sigma c ++ str " of another meta" let explain_no_such_hyp id = str "No such hypothesis: " ++ Id.print id -let explain_refiner_error = function - | BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty +let explain_refiner_error env sigma = function + | BadType (arg,ty,conclty) -> explain_refiner_bad_type env sigma arg ty conclty | UnresolvedBindings t -> explain_refiner_unresolved_bindings t - | CannotApply (t,harg) -> explain_refiner_cannot_apply t harg - | NotWellTyped c -> explain_refiner_not_well_typed c + | CannotApply (t,harg) -> explain_refiner_cannot_apply env sigma t harg + | NotWellTyped c -> explain_refiner_not_well_typed env sigma c | IntroNeedsProduct -> explain_intro_needs_product () - | DoesNotOccurIn (c,hyp) -> explain_does_not_occur_in c hyp - | NonLinearProof c -> explain_non_linear_proof c - | MetaInType c -> explain_meta_in_type c + | DoesNotOccurIn (c,hyp) -> explain_does_not_occur_in env sigma c hyp + | NonLinearProof c -> explain_non_linear_proof env sigma c + | MetaInType c -> explain_meta_in_type env sigma c | NoSuchHyp id -> explain_no_such_hyp id (* Inductive errors *) diff --git a/vernac/himsg.mli b/vernac/himsg.mli index 5b91f9e68..8945ebadb 100644 --- a/vernac/himsg.mli +++ b/vernac/himsg.mli @@ -27,7 +27,7 @@ val explain_typeclass_error : env -> typeclass_error -> Pp.t val explain_recursion_scheme_error : recursion_scheme_error -> Pp.t -val explain_refiner_error : refiner_error -> Pp.t +val explain_refiner_error : env -> Evd.evar_map -> refiner_error -> Pp.t val explain_pattern_matching_error : env -> Evd.evar_map -> pattern_matching_error -> Pp.t diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 7b8a38d5f..a025bfff8 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -253,7 +253,9 @@ let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2) | Lambda(na,ty,t) -> mkLambda(na,ty,body_i t) | App (t, args) -> mkApp (body_i t, args) - | _ -> anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr body ++ str ".") in + | _ -> + let sigma, env = Pfedit.get_current_context () in + anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr_env env sigma body ++ str ".") in let body_i = body_i body in match locality with | Discharge -> @@ -530,7 +532,5 @@ let save_proof ?proof = function Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj))) (* Miscellaneous *) +let get_current_context () = Pfedit.get_current_context () -let get_current_context () = - Pfedit.get_current_context () - diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 6972edd52..1b1304db5 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -66,3 +66,4 @@ val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> uni and the current global env *) val get_current_context : unit -> Evd.evar_map * Environ.env +[@@ocaml.deprecated "please use [Pfedit.get_current_context]"] diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 850902d6b..8673155e2 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -15,6 +15,7 @@ Command Classes Record Assumptions +Vernacstate Vernacinterp Mltop Topfmt diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 5bcb3b1e1..10c139e5a 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -56,20 +56,19 @@ let scope_class_of_qualid qid = let show_proof () = (* spiwack: this would probably be cooler with a bit of polishing. *) let p = Proof_global.give_me_the_proof () in + let sigma, env = Pfedit.get_current_context () in let pprf = Proof.partial_proof p in - Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl Printer.pr_econstr pprf) + Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf) 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 = Proof.V82.subgoals pfts in - let sigma = gls.Evd.sigma in + let gls,_,_,_,sigma = Proof.proof pfts in Feedback.msg_notice (pr_evars_int sigma 1 (Evd.undefined_map sigma)) let show_universes () = let pfts = Proof_global.give_me_the_proof () in - let gls = Proof.V82.subgoals pfts in - let sigma = gls.Evd.sigma in + let gls,_,_,_,sigma = Proof.proof pfts in let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in Feedback.msg_notice (Termops.pr_evar_universe_context (Evd.evar_universe_context sigma)); Feedback.msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx) @@ -78,7 +77,7 @@ let show_universes () = let show_intro all = let open EConstr in let pf = Proof_global.give_me_the_proof() in - let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in + let gls,_,_,_,sigma = Proof.proof pf in if not (List.is_empty gls) then begin let gl = {Evd.it=List.hd gls ; sigma = sigma; } in let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (pf_concl gl)) in @@ -257,7 +256,8 @@ let print_namespace ns = let print_constant k body = (* FIXME: universes *) let t = body.Declarations.const_type in - print_kn k ++ str":" ++ spc() ++ Printer.pr_type t + let sigma, env = Pfedit.get_current_context () in + print_kn k ++ str":" ++ spc() ++ Printer.pr_type_env env sigma t in let matches mp = match match_modulepath ns mp with | Some [] -> true @@ -486,8 +486,8 @@ let vernac_definition locality p (local,k) ((loc,id as lid),pl) def = let red_option = match red_option with | None -> None | Some r -> - let (evc,env)= get_current_context () in - Some (snd (Hook.get f_interp_redexp env evc r)) in + let sigma, env= Pfedit.get_current_context () in + Some (snd (Hook.get f_interp_redexp env sigma r)) in do_definition id (local,p,k) pl bl red_option c typ_opt hook) let vernac_start_proof locality p kind l = @@ -1539,7 +1539,7 @@ let vernac_print_option key = let get_current_context_of_args = function | Some n -> Pfedit.get_goal_context n - | None -> get_current_context () + | None -> Pfedit.get_current_context () let query_command_selector ?loc = function | None -> None @@ -1601,7 +1601,7 @@ let vernac_global_check c = let get_nth_goal n = let pf = Proof_global.give_me_the_proof() in - let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in + let gls,_,_,_,sigma = Proof.proof pf in let gl = {Evd.it=List.nth gls (n-1) ; sigma = sigma; } in gl @@ -1628,17 +1628,20 @@ let print_about_hyp_globs ?loc ref_or_by_not glopt = let natureofid = match decl with | LocalAssum _ -> "Hypothesis" | LocalDef (_,bdy,_) ->"Constant (let in)" in - v 0 (Id.print id ++ str":" ++ pr_econstr (NamedDecl.get_type decl) ++ fnl() ++ fnl() + let sigma, env = Pfedit.get_current_context () in + v 0 (Id.print id ++ str":" ++ pr_econstr_env env sigma (NamedDecl.get_type decl) ++ fnl() ++ fnl() ++ str natureofid ++ str " of the goal context.") with (* fallback to globals *) - | NoHyp | Not_found -> print_about ref_or_by_not + | NoHyp | Not_found -> + let sigma, env = Pfedit.get_current_context () in + print_about env sigma ref_or_by_not - -let vernac_print ?loc = let open Feedback in function + +let vernac_print ?loc env sigma = let open Feedback in function | PrintTables -> msg_notice (print_tables ()) - | PrintFullContext-> msg_notice (print_full_context_typ ()) - | PrintSectionContext qid -> msg_notice (print_sec_context_typ qid) - | PrintInspect n -> msg_notice (inspect n) + | PrintFullContext-> msg_notice (print_full_context_typ env sigma) + | PrintSectionContext qid -> msg_notice (print_sec_context_typ env sigma qid) + | PrintInspect n -> msg_notice (inspect env sigma n) | PrintGrammar ent -> msg_notice (Metasyntax.pr_grammar ent) | PrintLoadPath dir -> (* For compatibility ? *) msg_notice (print_loadpath dir) | PrintModules -> msg_notice (print_modules ()) @@ -1648,15 +1651,15 @@ let vernac_print ?loc = let open Feedback in function | PrintMLLoadPath -> msg_notice (Mltop.print_ml_path ()) | PrintMLModules -> msg_notice (Mltop.print_ml_modules ()) | PrintDebugGC -> msg_notice (Mltop.print_gc ()) - | PrintName qid -> dump_global qid; msg_notice (print_name qid) + | PrintName qid -> dump_global qid; msg_notice (print_name env sigma qid) | PrintGraph -> msg_notice (Prettyp.print_graph()) | PrintClasses -> msg_notice (Prettyp.print_classes()) | PrintTypeClasses -> msg_notice (Prettyp.print_typeclasses()) | PrintInstances c -> msg_notice (Prettyp.print_instances (smart_global c)) - | PrintCoercions -> msg_notice (Prettyp.print_coercions()) + | PrintCoercions -> msg_notice (Prettyp.print_coercions env sigma) | PrintCoercionPaths (cls,clt) -> msg_notice (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt)) - | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections ()) + | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections env sigma) | PrintUniverses (b, dst) -> let univ = Global.universes () in let univ = if b then UGraph.sort_universes univ else univ in @@ -1668,16 +1671,16 @@ let vernac_print ?loc = let open Feedback in function | None -> msg_notice (UGraph.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining) | Some s -> dump_universes_gen univ s end - | PrintHint r -> msg_notice (Hints.pr_hint_ref (smart_global r)) + | PrintHint r -> msg_notice (Hints.pr_hint_ref env sigma (smart_global r)) | PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ()) - | PrintHintDbName s -> msg_notice (Hints.pr_hint_db_by_name s) - | PrintHintDb -> msg_notice (Hints.pr_searchtable ()) + | PrintHintDbName s -> msg_notice (Hints.pr_hint_db_by_name env sigma s) + | PrintHintDb -> msg_notice (Hints.pr_searchtable env sigma) | PrintScopes -> - msg_notice (Notation.pr_scopes (Constrextern.without_symbols pr_lglob_constr)) + msg_notice (Notation.pr_scopes (Constrextern.without_symbols (pr_lglob_constr_env env))) | PrintScope s -> - msg_notice (Notation.pr_scope (Constrextern.without_symbols pr_lglob_constr) s) + msg_notice (Notation.pr_scope (Constrextern.without_symbols (pr_lglob_constr_env env)) s) | PrintVisibility s -> - msg_notice (Notation.pr_visibility (Constrextern.without_symbols pr_lglob_constr) s) + msg_notice (Notation.pr_visibility (Constrextern.without_symbols (pr_lglob_constr_env env)) s) | PrintAbout (ref_or_by_not,glnumopt) -> msg_notice (print_about_hyp_globs ?loc ref_or_by_not glnumopt) | PrintImplicit qid -> @@ -1780,9 +1783,10 @@ let vernac_locate = let open Feedback in function | LocateTerm (AN qid) -> msg_notice (print_located_term qid) | LocateAny (ByNotation (_, (ntn, sc))) (** TODO : handle Ltac notations *) | LocateTerm (ByNotation (_, (ntn, sc))) -> - msg_notice - (Notation.locate_notation - (Constrextern.without_symbols pr_lglob_constr) ntn sc) + let _, env = Pfedit.get_current_context () in + msg_notice + (Notation.locate_notation + (Constrextern.without_symbols (pr_lglob_constr_env env)) ntn sc) | LocateLibrary qid -> print_located_library qid | LocateModule qid -> msg_notice (print_located_module qid) | LocateOther (s, qid) -> msg_notice (print_located_other s qid) @@ -1849,10 +1853,11 @@ let vernac_bullet (bullet : Proof_bullet.t) = let vernac_show = let open Feedback in function | ShowScript -> assert false (* Only the stm knows the script *) | ShowGoal goalref -> + let proof = Proof_global.give_me_the_proof () in let info = match goalref with - | OpenSubgoals -> pr_open_subgoals () - | NthGoal n -> pr_nth_open_subgoal n - | GoalId id -> pr_goal_by_id id + | OpenSubgoals -> pr_open_subgoals ~proof + | NthGoal n -> pr_nth_open_subgoal ~proof n + | GoalId id -> pr_goal_by_id ~proof id in msg_notice info | ShowProof -> show_proof () @@ -1909,7 +1914,7 @@ let vernac_load interp fname = * is the outdated/deprecated "Local" attribute of some vernacular commands * still parsed as the obsolete_locality grammar entry for retrocompatibility. * loc is the Loc.t of the vernacular command being interpreted. *) -let interp ?proof ?loc locality poly c = +let interp ?proof ?loc locality poly st c = vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac c); match c with (* The below vernac are candidates for removal from the main type @@ -2043,7 +2048,9 @@ let interp ?proof ?loc locality poly c = | VernacCheckMayEval (r,g,c) -> vernac_check_may_eval ?loc r g c | VernacDeclareReduction (s,r) -> vernac_declare_reduction locality s r | VernacGlobalCheck c -> vernac_global_check c - | VernacPrint p -> vernac_print ?loc p + | VernacPrint p -> + let sigma, env = Pfedit.get_current_context () in + vernac_print ?loc env sigma p | VernacSearch (s,g,r) -> vernac_search ?loc s g r | VernacLocate l -> vernac_locate l | VernacRegister (id, r) -> vernac_register id r @@ -2069,7 +2076,10 @@ let interp ?proof ?loc locality poly c = | VernacProofMode mn -> Proof_global.set_proof_mode mn [@ocaml.warning "-3"] (* Extensions *) - | VernacExtend (opn,args) -> Vernacinterp.call ?locality ?loc (opn,args) + | VernacExtend (opn,args) -> + (* XXX: Here we are returning the state! :) *) + let _st : Vernacstate.t = Vernacinterp.call ?locality ?loc (opn,args) st in + () (* Vernaculars that take a locality flag *) let check_vernac_supports_locality c l = @@ -2147,28 +2157,6 @@ let locate_if_not_already ?loc (e, info) = exception HasNotFailed exception HasFailed of Pp.t -type interp_state = { (* TODO: inline records in OCaml 4.03 *) - system : States.state; (* summary + libstack *) - proof : Proof_global.state; (* proof state *) - shallow : bool (* is the state trimmed down (libstack) *) -} - -let s_cache = ref (States.freeze ~marshallable:`No) -let s_proof = ref (Proof_global.freeze ~marshallable:`No) - -let invalidate_cache () = - s_cache := Obj.magic 0; - s_proof := Obj.magic 0 - -let freeze_interp_state marshallable = - { system = (s_cache := States.freeze ~marshallable; !s_cache); - proof = (s_proof := Proof_global.freeze ~marshallable; !s_proof); - shallow = marshallable = `Shallow } - -let unfreeze_interp_state { system; proof } = - if (!s_cache != system) then (s_cache := system; States.unfreeze system); - if (!s_proof != proof) then (s_proof := proof; Proof_global.unfreeze proof) - (* XXX STATE: this type hints that restoring the state should be the caller's responsibility *) let with_fail st b f = @@ -2187,8 +2175,8 @@ let with_fail st b f = (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e))) with e when CErrors.noncritical e -> (* Restore the previous state XXX Careful here with the cache! *) - invalidate_cache (); - unfreeze_interp_state st; + Vernacstate.invalidate_cache (); + Vernacstate.unfreeze_interp_state st; let (e, _) = CErrors.push e in match e with | HasNotFailed -> @@ -2230,8 +2218,8 @@ let interp ?(verbosely=true) ?proof st (loc,c) = try vernac_timeout begin fun () -> if verbosely - then Flags.verbosely (interp ?proof ?loc locality poly) c - else Flags.silently (interp ?proof ?loc locality poly) c; + then Flags.verbosely (interp ?proof ?loc locality poly st) c + else Flags.silently (interp ?proof ?loc locality poly st) c; if orig_program_mode || not !Flags.program_mode || isprogcmd then Flags.program_mode := orig_program_mode; ignore (Flags.use_polymorphic_flag ()) @@ -2252,7 +2240,9 @@ let interp ?(verbosely=true) ?proof st (loc,c) = if verbosely then Flags.verbosely (aux false) c else aux false c +(* XXX: There is a bug here in case of an exception, see @gares + comments on the PR *) let interp ?verbosely ?proof st cmd = - unfreeze_interp_state st; + Vernacstate.unfreeze_interp_state st; interp ?verbosely ?proof st cmd; - freeze_interp_state `No + Vernacstate.freeze_interp_state `No diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 56635c801..67001bc24 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -14,21 +14,11 @@ val dump_global : Libnames.reference or_by_notation -> unit val vernac_require : Libnames.reference option -> bool option -> Libnames.reference list -> unit -type interp_state = { (* TODO: inline records in OCaml 4.03 *) - system : States.state; (* summary + libstack *) - proof : Proof_global.state; (* proof state *) - shallow : bool (* is the state trimmed down (libstack) *) -} - -val freeze_interp_state : Summary.marshallable -> interp_state -val unfreeze_interp_state : interp_state -> unit - (** The main interpretation function of vernacular expressions *) val interp : ?verbosely:bool -> ?proof:Proof_global.closed_proof -> - interp_state -> - Vernacexpr.vernac_expr Loc.located -> interp_state + Vernacstate.t -> Vernacexpr.vernac_expr Loc.located -> Vernacstate.t (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name @@ -40,7 +30,7 @@ val make_cases : string -> string list list (* XXX STATE: this type hints that restoring the state should be the caller's responsibility *) -val with_fail : interp_state -> bool -> (unit -> unit) -> unit +val with_fail : Vernacstate.t -> bool -> (unit -> unit) -> unit val command_focus : unit Proof.focus_kind diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 41fee6bd0..1d024386e 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -11,11 +11,12 @@ open Pp open CErrors type deprecation = bool -type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> unit +type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> + Vernacstate.t -> Vernacstate.t (* Table of vernac entries *) let vernac_tab = - (Hashtbl.create 51 : + (Hashtbl.create 211 : (Vernacexpr.extend_name, deprecation * vernac_command) Hashtbl.t) let vinterp_add depr s f = @@ -66,8 +67,9 @@ let call ?locality ?loc (opn,converted_args) = let hunk = callback converted_args in phase := "Executing command"; Locality.LocalityFixme.set locality; - hunk loc; - Locality.LocalityFixme.assert_consumed() + let res = hunk loc in + Locality.LocalityFixme.assert_consumed (); + res with | Drop -> raise Drop | reraise -> diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli index 84370fdc2..1c66b1c04 100644 --- a/vernac/vernacinterp.mli +++ b/vernac/vernacinterp.mli @@ -9,12 +9,16 @@ (** Interpretation of extended vernac phrases. *) type deprecation = bool -type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> unit -val vinterp_add : deprecation -> Vernacexpr.extend_name -> - vernac_command -> unit -val overwriting_vinterp_add : - Vernacexpr.extend_name -> vernac_command -> unit +type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> + Vernacstate.t -> Vernacstate.t + +val vinterp_add : deprecation -> Vernacexpr.extend_name -> vernac_command -> unit + +val overwriting_vinterp_add : Vernacexpr.extend_name -> vernac_command -> unit val vinterp_init : unit -> unit -val call : ?locality:bool -> ?loc:Loc.t -> Vernacexpr.extend_name * Genarg.raw_generic_argument list -> unit + +val call : ?locality:bool -> ?loc:Loc.t -> + Vernacexpr.extend_name * Genarg.raw_generic_argument list -> + Vernacstate.t -> Vernacstate.t diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml new file mode 100644 index 000000000..9802a03ca --- /dev/null +++ b/vernac/vernacstate.ml @@ -0,0 +1,29 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +type t = { (* TODO: inline records in OCaml 4.03 *) + system : States.state; (* summary + libstack *) + proof : Proof_global.state; (* proof state *) + shallow : bool (* is the state trimmed down (libstack) *) +} + +let s_cache = ref (States.freeze ~marshallable:`No) +let s_proof = ref (Proof_global.freeze ~marshallable:`No) + +let invalidate_cache () = + s_cache := Obj.magic 0; + s_proof := Obj.magic 0 + +let freeze_interp_state marshallable = + { system = (s_cache := States.freeze ~marshallable; !s_cache); + proof = (s_proof := Proof_global.freeze ~marshallable; !s_proof); + shallow = marshallable = `Shallow } + +let unfreeze_interp_state { system; proof } = + if (!s_cache != system) then (s_cache := system; States.unfreeze system); + if (!s_proof != proof) then (s_proof := proof; Proof_global.unfreeze proof) diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli new file mode 100644 index 000000000..63a5b3b1e --- /dev/null +++ b/vernac/vernacstate.mli @@ -0,0 +1,19 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +type t = { (* TODO: inline records in OCaml 4.03 *) + system : States.state; (* summary + libstack *) + proof : Proof_global.state; (* proof state *) + shallow : bool (* is the state trimmed down (libstack) *) +} + +val freeze_interp_state : Summary.marshallable -> t +val unfreeze_interp_state : t -> unit + +(* WARNING: Do not use, it will go away in future releases *) +val invalidate_cache : unit -> unit |