From 2defd4c15467736b73f69adb501e3a4fe2111ce5 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 29 Jun 2015 21:30:19 +0200 Subject: Assumptions: more informative print for False axiom (Close: #4054) When an axiom of an empty type is matched in order to inhabit a type, do print that type (as if each use of that axiom was a distinct foo_subproof). E.g. Lemma w : True. Proof. case demon. Qed. Lemma x y : y = 0 /\ True /\ forall w, w = y. Proof. split. case demon. split; [ exact w | case demon ]. Qed. Print Assumptions x. Prints: Axioms: demon : False used in x to prove: forall w : nat, w = y used in w to prove: True used in x to prove: y = 0 --- dev/printers.mllib | 2 +- library/assumptions.ml | 225 --------------------------------------------- library/assumptions.mli | 41 --------- library/library.mllib | 1 - pretyping/termops.ml | 15 +-- pretyping/termops.mli | 4 + printing/printer.ml | 44 ++++++++- printing/printer.mli | 16 +++- toplevel/assumptions.ml | 228 ++++++++++++++++++++++++++++++++++++++++++++++ toplevel/assumptions.mli | 32 +++++++ toplevel/toplevel.mllib | 1 + toplevel/vernacentries.ml | 5 +- 12 files changed, 333 insertions(+), 281 deletions(-) delete mode 100644 library/assumptions.ml delete mode 100644 library/assumptions.mli create mode 100644 toplevel/assumptions.ml create mode 100644 toplevel/assumptions.mli diff --git a/dev/printers.mllib b/dev/printers.mllib index 74f36f6f5..07b48ed57 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -110,7 +110,6 @@ Loadpath Goptions Decls Heads -Assumptions Keys Locusops Miscops @@ -204,6 +203,7 @@ Hints Himsg Cerrors Locality +Assumptions Vernacinterp Dischargedhypsmap Discharge diff --git a/library/assumptions.ml b/library/assumptions.ml deleted file mode 100644 index 62645b236..000000000 --- a/library/assumptions.ml +++ /dev/null @@ -1,225 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Id.compare i1 i2 - | Axiom k1 , Axiom k2 -> con_ord k1 k2 - | Opaque k1 , Opaque k2 -> con_ord k1 k2 - | Transparent k1 , Transparent k2 -> con_ord k1 k2 - | Axiom _ , Variable _ -> 1 - | Opaque _ , Variable _ - | Opaque _ , Axiom _ -> 1 - | Transparent _ , Variable _ - | Transparent _ , Axiom _ - | Transparent _ , Opaque _ -> 1 - | _ , _ -> -1 -end - -module ContextObjectSet = Set.Make (OrderedContextObject) -module ContextObjectMap = Map.Make (OrderedContextObject) - -(** For a constant c in a module sealed by an interface (M:T and - not M<:T), [Global.lookup_constant] may return a [constant_body] - without body. We fix this by looking in the implementation - of the module *) - -let modcache = ref (MPmap.empty : structure_body MPmap.t) - -let rec search_mod_label lab = function - | [] -> raise Not_found - | (l, SFBmodule mb) :: _ when Label.equal l lab -> mb - | _ :: fields -> search_mod_label lab fields - -let rec search_cst_label lab = function - | [] -> raise Not_found - | (l, SFBconst cb) :: _ when Label.equal l lab -> cb - | _ :: fields -> search_cst_label lab fields - -(* TODO: using [empty_delta_resolver] below is probably slightly incorrect. But: - a) I don't see currently what should be used instead - b) this shouldn't be critical for Print Assumption. At worse some - constants will have a canonical name which is non-canonical, - leading to failures in [Global.lookup_constant], but our own - [lookup_constant] should work. -*) - -let rec fields_of_functor f subs mp0 args = function - |NoFunctor a -> f subs mp0 args a - |MoreFunctor (mbid,_,e) -> - match args with - | [] -> assert false (* we should only encounter applied functors *) - | mpa :: args -> - let subs = add_mbid mbid mpa empty_delta_resolver (*TODO*) subs in - fields_of_functor f subs mp0 args e - -let rec lookup_module_in_impl mp = - try Global.lookup_module mp - with Not_found -> - (* The module we search might not be exported by its englobing module(s). - We access the upper layer, and then do a manual search *) - match mp with - | MPfile _ | MPbound _ -> - raise Not_found (* should have been found by [lookup_module] *) - | MPdot (mp',lab') -> - let fields = memoize_fields_of_mp mp' in - search_mod_label lab' fields - -and memoize_fields_of_mp mp = - try MPmap.find mp !modcache - with Not_found -> - let l = fields_of_mp mp in - modcache := MPmap.add mp l !modcache; - l - -and fields_of_mp mp = - let mb = lookup_module_in_impl mp in - let fields,inner_mp,subs = fields_of_mb empty_subst mb [] in - let subs = - if mp_eq inner_mp mp then subs - else add_mp inner_mp mp mb.mod_delta subs - in - Modops.subst_structure subs fields - -and fields_of_mb subs mb args = match mb.mod_expr with - |Algebraic expr -> fields_of_expression subs mb.mod_mp args expr - |Struct sign -> fields_of_signature subs mb.mod_mp args sign - |Abstract|FullStruct -> fields_of_signature subs mb.mod_mp args mb.mod_type - -(** The Abstract case above corresponds to [Declare Module] *) - -and fields_of_signature x = - fields_of_functor - (fun subs mp0 args struc -> - assert (List.is_empty args); - (struc, mp0, subs)) x - -and fields_of_expr subs mp0 args = function - |MEident mp -> - let mb = lookup_module_in_impl (subst_mp subs mp) in - fields_of_mb subs mb args - |MEapply (me1,mp2) -> fields_of_expr subs mp0 (mp2::args) me1 - |MEwith _ -> assert false (* no 'with' in [mod_expr] *) - -and fields_of_expression x = fields_of_functor fields_of_expr x - -let lookup_constant_in_impl cst fallback = - try - let mp,dp,lab = repr_kn (canonical_con cst) in - let fields = memoize_fields_of_mp mp in - (* A module found this way is necessarily closed, in particular - our constant cannot be in an opened section : *) - search_cst_label lab fields - with Not_found -> - (* Either: - - The module part of the constant isn't registered yet : - we're still in it, so the [constant_body] found earlier - (if any) was a true axiom. - - The label has not been found in the structure. This is an error *) - match fallback with - | Some cb -> cb - | None -> anomaly (str "Print Assumption: unknown constant " ++ pr_con cst) - -let lookup_constant cst = - try - let cb = Global.lookup_constant cst in - if Declareops.constant_has_body cb then cb - else lookup_constant_in_impl cst (Some cb) - with Not_found -> lookup_constant_in_impl cst None - -(** Graph traversal of an object, collecting on the way the dependencies of - traversed objects *) -let rec traverse accu t = match kind_of_term t with -| Var id -> - let body () = match Global.lookup_named id with (_, body, _) -> body in - traverse_object accu body (VarRef id) -| Const (kn, _) -> - let body () = Global.body_of_constant_body (lookup_constant kn) in - traverse_object accu body (ConstRef kn) -| Ind (ind, _) -> - traverse_object accu (fun () -> None) (IndRef ind) -| Construct (cst, _) -> - traverse_object accu (fun () -> None) (ConstructRef cst) -| Meta _ | Evar _ -> assert false -| _ -> Constr.fold traverse accu t - -and traverse_object (curr, data) body obj = - let data = - if Refmap.mem obj data then data - else match body () with - | None -> Refmap.add obj Refset.empty data - | Some body -> - let (contents, data) = traverse (Refset.empty, data) body in - Refmap.add obj contents data - in - (Refset.add obj curr, data) - -let traverse t = - let () = modcache := MPmap.empty in - traverse (Refset.empty, Refmap.empty) t - -(** Hopefully bullet-proof function to recover the type of a constant. It just - ignores all the universe stuff. There are many issues that can arise when - considering terms out of any valid environment, so use with caution. *) -let type_of_constant cb = match cb.Declarations.const_type with -| Declarations.RegularArity ty -> ty -| Declarations.TemplateArity (ctx, arity) -> - Term.mkArity (ctx, Sorts.sort_of_univ arity.Declarations.template_level) - -let assumptions ?(add_opaque=false) ?(add_transparent=false) st t = - let (idts, knst) = st in - (** Only keep the transitive dependencies *) - let (_, graph) = traverse t in - let fold obj _ accu = match obj with - | VarRef id -> - let (_, body, t) = Global.lookup_named id in - if Option.is_empty body then ContextObjectMap.add (Variable id) t accu - else accu - | ConstRef kn -> - let cb = lookup_constant kn in - if not (Declareops.constant_has_body cb) then - let t = type_of_constant cb in - ContextObjectMap.add (Axiom kn) t accu - else if add_opaque && (Declareops.is_opaque cb || not (Cpred.mem kn knst)) then - let t = type_of_constant cb in - ContextObjectMap.add (Opaque kn) t accu - else if add_transparent then - let t = type_of_constant cb in - ContextObjectMap.add (Transparent kn) t accu - else - accu - | IndRef _ | ConstructRef _ -> accu - in - Refmap.fold fold graph ContextObjectMap.empty diff --git a/library/assumptions.mli b/library/assumptions.mli deleted file mode 100644 index bb36a9725..000000000 --- a/library/assumptions.mli +++ /dev/null @@ -1,41 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* (Refset.t * Refset.t Refmap.t) - -(** Collects all the assumptions (optionally including opaque definitions) - on which a term relies (together with their type). The above warning of - {!traverse} also applies. *) -val assumptions : - ?add_opaque:bool -> ?add_transparent:bool -> transparent_state -> constr -> - Term.types ContextObjectMap.t diff --git a/library/library.mllib b/library/library.mllib index eca28c822..920657365 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -16,5 +16,4 @@ Dischargedhypsmap Goptions Decls Heads -Assumptions Keys diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 9f04faa83..937471cf7 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -453,26 +453,29 @@ let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with index) which is processed by [g] (which typically add 1 to [n]) at each binder traversal; it is not recursive *) -let fold_constr_with_binders g f n acc c = match kind_of_term c with +let fold_constr_with_full_binders g f n acc c = match kind_of_term c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> acc | Cast (c,_, t) -> f n (f n acc c) t - | Prod (_,t,c) -> f (g n) (f n acc t) c - | Lambda (_,t,c) -> f (g n) (f n acc t) c - | LetIn (_,b,t,c) -> f (g n) (f n (f n acc b) t) c + | Prod (na,t,c) -> f (g (na,None,t) n) (f n acc t) c + | Lambda (na,t,c) -> f (g (na,None,t) n) (f n acc t) c + | LetIn (na,b,t,c) -> f (g (na,Some b,t) n) (f n (f n acc b) t) c | App (c,l) -> Array.fold_left (f n) (f n acc c) l | Proj (p,c) -> f n acc c | Evar (_,l) -> Array.fold_left (f n) acc l | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl | Fix (_,(lna,tl,bl)) -> - let n' = iterate g (Array.length tl) n in + let n' = CArray.fold_left2 (fun c n t -> g (n,None,t) c) n lna tl in let fd = Array.map2 (fun t b -> (t,b)) tl bl in Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd | CoFix (_,(lna,tl,bl)) -> - let n' = iterate g (Array.length tl) n in + let n' = CArray.fold_left2 (fun c n t -> g (n,None,t) c) n lna tl in let fd = Array.map2 (fun t b -> (t,b)) tl bl in Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd +let fold_constr_with_binders g f n acc c = + fold_constr_with_full_binders (fun _ x -> g x) f n acc c + (* [iter_constr_with_full_binders g f acc c] iters [f acc] on the immediate subterms of [c]; it carries an extra data [acc] which is processed by [g] at each binder traversal; it is not recursive and the order with which diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 2552c67e6..4581e2310 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -84,6 +84,10 @@ val map_constr_with_full_binders : val fold_constr_with_binders : ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b +val fold_constr_with_full_binders : + (rel_declaration -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) -> + 'a -> 'b -> constr -> 'b + val iter_constr_with_full_binders : (rel_declaration -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit diff --git a/printing/printer.ml b/printing/printer.ml index 652542825..33b95c2f5 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -713,7 +713,33 @@ let prterm = pr_lconstr (* Printer function for sets of Assumptions.assumptions. It is used primarily by the Print Assumptions command. *) -open Assumptions +type context_object = + | Variable of Id.t (* A section variable or a Let definition *) + | Axiom of constant * (Label.t * Context.rel_context * types) list + | Opaque of constant (* An opaque constant. *) + | Transparent of constant + +(* Defines a set of [assumption] *) +module OrderedContextObject = +struct + type t = context_object + let compare x y = + match x , y with + | Variable i1 , Variable i2 -> Id.compare i1 i2 + | Axiom (k1,_) , Axiom (k2, _) -> con_ord k1 k2 + | Opaque k1 , Opaque k2 -> con_ord k1 k2 + | Transparent k1 , Transparent k2 -> con_ord k1 k2 + | Axiom _ , Variable _ -> 1 + | Opaque _ , Variable _ + | Opaque _ , Axiom _ -> 1 + | Transparent _ , Variable _ + | Transparent _ , Axiom _ + | Transparent _ , Opaque _ -> 1 + | _ , _ -> -1 +end + +module ContextObjectSet = Set.Make (OrderedContextObject) +module ContextObjectMap = Map.Make (OrderedContextObject) let pr_assumptionset env s = if ContextObjectMap.is_empty s then @@ -729,15 +755,29 @@ let pr_assumptionset env s = try str " : " ++ pr_ltype typ with e when Errors.noncritical e -> mt () in + let safe_pr_ltype_relctx (rctx, typ) = + let sigma, env = get_current_context () in + let env = Environ.push_rel_context rctx env in + try str " " ++ pr_ltype_env env sigma typ + with e when Errors.noncritical e -> mt () + in let fold t typ accu = let (v, a, o, tr) = accu in match t with | Variable id -> let var = str (Id.to_string id) ++ str " : " ++ pr_ltype typ in (var :: v, a, o, tr) - | Axiom kn -> + | Axiom (kn,[]) -> let ax = safe_pr_constant env kn ++ safe_pr_ltype typ in (v, ax :: a, o, tr) + | Axiom (kn,l) -> + let ax = safe_pr_constant env kn ++ safe_pr_ltype typ ++ + cut() ++ + prlist_with_sep cut (fun (lbl, ctx, ty) -> + str " used in " ++ str (Names.Label.to_string lbl) ++ + str " to prove:" ++ safe_pr_ltype_relctx (ctx,ty)) + l in + (v, ax :: a, o, tr) | Opaque kn -> let opq = safe_pr_constant env kn ++ safe_pr_ltype typ in (v, a, opq :: o, tr) diff --git a/printing/printer.mli b/printing/printer.mli index a469a8dbe..5f56adbe6 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -160,10 +160,20 @@ val emacs_str : string -> string val prterm : constr -> std_ppcmds (** = pr_lconstr *) -(** spiwack: printer function for sets of Environ.assumption. - It is used primarily by the Print Assumption command. *) +(** Declarations for the "Print Assumption" command *) +type context_object = + | Variable of Id.t (** A section variable or a Let definition *) + (** An axiom and the type it inhabits (if an axiom of the empty type) *) + | Axiom of constant * (Label.t * Context.rel_context * types) list + | Opaque of constant (** An opaque constant. *) + | Transparent of constant (** A transparent constant *) + +module ContextObjectSet : Set.S with type elt = context_object +module ContextObjectMap : CMap.ExtS + with type key = context_object and module Set := ContextObjectSet + val pr_assumptionset : - env -> Term.types Assumptions.ContextObjectMap.t ->std_ppcmds + env -> Term.types ContextObjectMap.t -> std_ppcmds val pr_goal_by_id : string -> std_ppcmds diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml new file mode 100644 index 000000000..fff7e2e21 --- /dev/null +++ b/toplevel/assumptions.ml @@ -0,0 +1,228 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* raise Not_found + | (l, SFBmodule mb) :: _ when Label.equal l lab -> mb + | _ :: fields -> search_mod_label lab fields + +let rec search_cst_label lab = function + | [] -> raise Not_found + | (l, SFBconst cb) :: _ when Label.equal l lab -> cb + | _ :: fields -> search_cst_label lab fields + +(* TODO: using [empty_delta_resolver] below is probably slightly incorrect. But: + a) I don't see currently what should be used instead + b) this shouldn't be critical for Print Assumption. At worse some + constants will have a canonical name which is non-canonical, + leading to failures in [Global.lookup_constant], but our own + [lookup_constant] should work. +*) + +let rec fields_of_functor f subs mp0 args = function + |NoFunctor a -> f subs mp0 args a + |MoreFunctor (mbid,_,e) -> + match args with + | [] -> assert false (* we should only encounter applied functors *) + | mpa :: args -> + let subs = add_mbid mbid mpa empty_delta_resolver (*TODO*) subs in + fields_of_functor f subs mp0 args e + +let rec lookup_module_in_impl mp = + try Global.lookup_module mp + with Not_found -> + (* The module we search might not be exported by its englobing module(s). + We access the upper layer, and then do a manual search *) + match mp with + | MPfile _ | MPbound _ -> + raise Not_found (* should have been found by [lookup_module] *) + | MPdot (mp',lab') -> + let fields = memoize_fields_of_mp mp' in + search_mod_label lab' fields + +and memoize_fields_of_mp mp = + try MPmap.find mp !modcache + with Not_found -> + let l = fields_of_mp mp in + modcache := MPmap.add mp l !modcache; + l + +and fields_of_mp mp = + let mb = lookup_module_in_impl mp in + let fields,inner_mp,subs = fields_of_mb empty_subst mb [] in + let subs = + if mp_eq inner_mp mp then subs + else add_mp inner_mp mp mb.mod_delta subs + in + Modops.subst_structure subs fields + +and fields_of_mb subs mb args = match mb.mod_expr with + |Algebraic expr -> fields_of_expression subs mb.mod_mp args expr + |Struct sign -> fields_of_signature subs mb.mod_mp args sign + |Abstract|FullStruct -> fields_of_signature subs mb.mod_mp args mb.mod_type + +(** The Abstract case above corresponds to [Declare Module] *) + +and fields_of_signature x = + fields_of_functor + (fun subs mp0 args struc -> + assert (List.is_empty args); + (struc, mp0, subs)) x + +and fields_of_expr subs mp0 args = function + |MEident mp -> + let mb = lookup_module_in_impl (subst_mp subs mp) in + fields_of_mb subs mb args + |MEapply (me1,mp2) -> fields_of_expr subs mp0 (mp2::args) me1 + |MEwith _ -> assert false (* no 'with' in [mod_expr] *) + +and fields_of_expression x = fields_of_functor fields_of_expr x + +let lookup_constant_in_impl cst fallback = + try + let mp,dp,lab = repr_kn (canonical_con cst) in + let fields = memoize_fields_of_mp mp in + (* A module found this way is necessarily closed, in particular + our constant cannot be in an opened section : *) + search_cst_label lab fields + with Not_found -> + (* Either: + - The module part of the constant isn't registered yet : + we're still in it, so the [constant_body] found earlier + (if any) was a true axiom. + - The label has not been found in the structure. This is an error *) + match fallback with + | Some cb -> cb + | None -> anomaly (str "Print Assumption: unknown constant " ++ pr_con cst) + +let lookup_constant cst = + try + let cb = Global.lookup_constant cst in + if Declareops.constant_has_body cb then cb + else lookup_constant_in_impl cst (Some cb) + with Not_found -> lookup_constant_in_impl cst None + +(** Graph traversal of an object, collecting on the way the dependencies of + traversed objects *) + +let label_of = function + | ConstRef kn -> pi3 (repr_con kn) + | IndRef (kn,_) + | ConstructRef ((kn,_),_) -> pi3 (repr_mind kn) + | VarRef id -> Label.of_id id + +let push (r : Context.rel_declaration) (ctx : Context.rel_context) = r :: ctx + +let rec traverse current ctx accu t = match kind_of_term t with +| Var id -> + let body () = match Global.lookup_named id with (_, body, _) -> body in + traverse_object accu body (VarRef id) +| Const (kn, _) -> + let body () = Global.body_of_constant_body (lookup_constant kn) in + traverse_object accu body (ConstRef kn) +| Ind (ind, _) -> + traverse_object accu (fun () -> None) (IndRef ind) +| Construct (cst, _) -> + traverse_object accu (fun () -> None) (ConstructRef cst) +| Meta _ | Evar _ -> assert false +| Case (_,oty,c,[||]) -> + (* non dependent match on an inductive with no constructors *) + begin match Constr.(kind oty, kind c) with + | Lambda(Anonymous,_,oty), Const (kn, _) + when Vars.noccurn 1 oty && + not (Declareops.constant_has_body (lookup_constant kn)) -> + let body () = Global.body_of_constant_body (lookup_constant kn) in + traverse_object + ~inhabits:(current,ctx,Vars.subst1 mkProp oty) accu body (ConstRef kn) + | _ -> Termops.fold_constr_with_full_binders push (traverse current) ctx accu t + end +| _ -> Termops.fold_constr_with_full_binders push (traverse current) ctx accu t + +and traverse_object ?inhabits (curr, data, ax2ty) body obj = + let data, ax2ty = + let already_in = Refmap.mem obj data in + match body () with + | None -> + let data = + if not already_in then Refmap.add obj Refset.empty data else data in + let ax2ty = + if Option.is_empty inhabits then ax2ty else + let ty = Option.get inhabits in + try let l = Refmap.find obj ax2ty in Refmap.add obj (ty::l) ax2ty + with Not_found -> Refmap.add obj [ty] ax2ty in + data, ax2ty + | Some body -> + let contents,data,ax2ty = + traverse (label_of obj) [] (Refset.empty,data,ax2ty) body in + Refmap.add obj contents data, ax2ty + in + (Refset.add obj curr, data, ax2ty) + +let traverse current t = + let () = modcache := MPmap.empty in + traverse current [] (Refset.empty, Refmap.empty, Refmap.empty) t + +(** Hopefully bullet-proof function to recover the type of a constant. It just + ignores all the universe stuff. There are many issues that can arise when + considering terms out of any valid environment, so use with caution. *) +let type_of_constant cb = match cb.Declarations.const_type with +| Declarations.RegularArity ty -> ty +| Declarations.TemplateArity (ctx, arity) -> + Term.mkArity (ctx, Sorts.sort_of_univ arity.Declarations.template_level) + +let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = + let (idts, knst) = st in + (** Only keep the transitive dependencies *) + let (_, graph, ax2ty) = traverse (label_of gr) t in + let fold obj _ accu = match obj with + | VarRef id -> + let (_, body, t) = Global.lookup_named id in + if Option.is_empty body then ContextObjectMap.add (Variable id) t accu + else accu + | ConstRef kn -> + let cb = lookup_constant kn in + if not (Declareops.constant_has_body cb) then + let t = type_of_constant cb in + let l = try Refmap.find obj ax2ty with Not_found -> [] in + ContextObjectMap.add (Axiom (kn,l)) t accu + else if add_opaque && (Declareops.is_opaque cb || not (Cpred.mem kn knst)) then + let t = type_of_constant cb in + ContextObjectMap.add (Opaque kn) t accu + else if add_transparent then + let t = type_of_constant cb in + ContextObjectMap.add (Transparent kn) t accu + else + accu + | IndRef _ | ConstructRef _ -> accu + in + Refmap.fold fold graph ContextObjectMap.empty diff --git a/toplevel/assumptions.mli b/toplevel/assumptions.mli new file mode 100644 index 000000000..a608fe505 --- /dev/null +++ b/toplevel/assumptions.mli @@ -0,0 +1,32 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* constr -> + (Refset.t * Refset.t Refmap.t * + (label * Context.rel_context * types) list Refmap.t) + +(** Collects all the assumptions (optionally including opaque definitions) + on which a term relies (together with their type). The above warning of + {!traverse} also applies. *) +val assumptions : + ?add_opaque:bool -> ?add_transparent:bool -> transparent_state -> + global_reference -> constr -> Term.types ContextObjectMap.t diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index bf0f305ab..5aa7d428a 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -10,6 +10,7 @@ Obligations Command Classes Record +Assumptions Vernacinterp Mltop Vernacentries diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 2af28de98..6c5f10c20 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1663,10 +1663,11 @@ let vernac_print = function dump_global qid; msg_notice (print_impargs qid) | PrintAssumptions (o,t,r) -> (* Prints all the axioms and section variables used by a term *) - let cstr = printable_constr_of_global (smart_global r) in + let gr = smart_global r in + let cstr = printable_constr_of_global gr in let st = Conv_oracle.get_transp_state (Environ.oracle (Global.env())) in let nassums = - Assumptions.assumptions st ~add_opaque:o ~add_transparent:t cstr in + Assumptions.assumptions st ~add_opaque:o ~add_transparent:t gr cstr in msg_notice (Printer.pr_assumptionset (Global.env ()) nassums) | PrintStrategy r -> print_strategy r -- cgit v1.2.3