From e39b5b8eaa89950216bca646b5e9ef9b56bea7be Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Jun 2015 14:19:31 +0200 Subject: Code documentation of the TACTIC/VERNAC EXTEND macros. --- grammar/tacextend.ml4 | 2 ++ grammar/vernacextend.ml4 | 2 ++ intf/tacexpr.mli | 5 +++++ intf/vernacexpr.mli | 9 ++++++++- 4 files changed, 17 insertions(+), 1 deletion(-) diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index f5f11e30a8..66f82fcdfc 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -8,6 +8,8 @@ (*i camlp4deps: "tools/compat5b.cmo" i*) +(** Implementation of the TACTIC EXTEND macro. *) + open Util open Pp open Names diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index 9db89308fb..03061d8bde 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -8,6 +8,8 @@ (*i camlp4deps: "tools/compat5b.cmo" i*) +(** Implementation of the VERNAC EXTEND macro. *) + open Pp open Util open Q_util diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index ff090ca844..2b37c580ea 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -94,8 +94,13 @@ type ('a,'t) match_rule = | Pat of 'a match_context_hyps list * 'a match_pattern * 't | All of 't +(** Extension indentifiers for the TACTIC EXTEND mechanism. *) type ml_tactic_name = { + (** Name of the plugin where the tactic is defined, typically coming from a + DECLARE PLUGIN statement in the source. *) mltac_plugin : string; + (** Name of the tactic entry where the tactic is defined, typically found + after the TACTIC EXTEND statement in the source. *) mltac_tactic : string; } diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 0ca3bb35f6..b72577e1e0 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -225,7 +225,14 @@ type section_subset_expr = type section_subset_descr = SsAll | SsType | SsExpr of section_subset_expr -type extend_name = string * int +(** Extension identifiers for the VERNAC EXTEND mechanism. *) +type extend_name = + (** Name of the vernac entry where the tactic is defined, typically found + after the VERNAC EXTEND statement in the source. *) + string * + (** Index of the extension in the VERNAC EXTEND statement. Each parsing branch + is given an offset, starting from zero. *) + int (* This type allows registering the inlining of constants in native compiler. It will be extended with primitive inductive types and operators *) -- cgit v1.2.3 From 671e556453c1eee335cf788ebc72675f5a7483d8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 29 Jun 2015 21:34:11 +0200 Subject: win: compile with -debug --- dev/make-installer-win32.sh | 2 +- dev/make-installer-win64.sh | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/dev/make-installer-win32.sh b/dev/make-installer-win32.sh index ec7cd5773a..c6ed2f401d 100755 --- a/dev/make-installer-win32.sh +++ b/dev/make-installer-win32.sh @@ -5,7 +5,7 @@ ZIP=_make.zip URL1=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-bin.zip/download URL2=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-dep.zip/download -[ -e config/Makefile ] || ./configure -prefix ./ -with-doc no +[ -e config/Makefile ] || ./configure -debug -prefix ./ -with-doc no make -j2 if [ ! -e bin/make.exe ]; then wget -O $ZIP $URL1 && 7z x $ZIP "bin/*" diff --git a/dev/make-installer-win64.sh b/dev/make-installer-win64.sh index 73e1fdbeb2..03fdda4aa1 100755 --- a/dev/make-installer-win64.sh +++ b/dev/make-installer-win64.sh @@ -5,13 +5,13 @@ ZIP=_make.zip URL1=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-bin.zip/download URL2=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-dep.zip/download -[ -e config/Makefile ] || ./configure -prefix ./ -with-doc no +[ -e config/Makefile ] || ./configure -debug -prefix ./ -with-doc no make -j2 coqide mkdir -p bin32 cp bin/* bin32/ make clean make archclean -( . ${BASE}_64/environ; ./configure -prefix ./ -with-doc no; make -j2; make ide/coqidetop.cmxs ) +( . ${BASE}_64/environ; ./configure -debug -prefix ./ -with-doc no; make -j2; make ide/coqidetop.cmxs ) cp bin32/coqide* bin/ if [ ! -e bin/make.exe ]; then wget -O $ZIP $URL1 && 7z x $ZIP "bin/*" -- cgit v1.2.3 From 38da14404781843a6143fc4af9d503e05d8d7dd6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 25 Jun 2015 14:04:49 +0200 Subject: class_tactics: remove catch-all, use Errors.noncritical --- tactics/class_tactics.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index ef78a953ac..09cf4b0498 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -205,7 +205,7 @@ and e_my_find_search db_list local_db hdc complete sigma concl = if cl.cl_strict then Evd.evars_of_term concl else Evar.Set.empty - with _ -> Evar.Set.empty + with e when Errors.noncritical e -> Evar.Set.empty in let hintl = List.map_append @@ -397,7 +397,7 @@ let is_unique env concl = try let (cl,u), args = dest_class_app env concl in cl.cl_unique - with _ -> false + with e when Errors.noncritical e -> false let needs_backtrack env evd oev concl = if Option.is_empty oev || is_Prop env evd concl then -- cgit v1.2.3 From 799f27ae19d6d2d16ade15bbdab83bd9acb0035f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 29 Jun 2015 21:33:50 +0200 Subject: class_tactics: make interruptible Tracing with gdb by Alec Faithfull --- tactics/class_tactics.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 09cf4b0498..80f47c680f 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -490,6 +490,7 @@ let hints_tac hints = let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk = let rec aux s (acc : autogoal list list) fk = function | (gl,info) :: gls -> + Control.check_for_interrupt (); (match info.is_evar with | Some ev when Evd.is_defined s ev -> aux s acc fk gls | _ -> -- cgit v1.2.3 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 74f36f6f5a..07b48ed573 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 62645b2365..0000000000 --- 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 bb36a97259..0000000000 --- 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 eca28c8222..9206573658 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 9f04faa839..937471cf76 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 2552c67e61..4581e23100 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 6525428254..33b95c2f56 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 a469a8dbed..5f56adbe6f 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 0000000000..fff7e2e21e --- /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 0000000000..a608fe5050 --- /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 bf0f305abd..5aa7d428a4 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 2af28de982..6c5f10c20a 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 From 72f128af5a00e5509239e46b395c9cd10e53b36a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 30 Jun 2015 16:47:28 +0200 Subject: Removing dead code in coqdep. Since commit 2f521670fbd, the Require "file" syntax was not used anymore by coqtop but the code handling it was still there in coqdep. We finish the work by erasing the remnant code. --- tools/coqdep.ml | 4 ---- tools/coqdep_common.ml | 11 ----------- tools/coqdep_lexer.mli | 1 - tools/coqdep_lexer.mll | 5 ----- 4 files changed, 21 deletions(-) diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 2e0cce6e53..f246dc69c4 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -61,7 +61,6 @@ let sort () = try loop (Hashtbl.find vKnown s) with Not_found -> ()) sl - | RequireString s -> loop s | _ -> () done with Fin_fichier -> @@ -319,9 +318,6 @@ let treat_coq_file chan = let acc = match action with | Require strl -> List.fold_left mark_v_done acc strl - | RequireString s -> - let str = Filename.basename s in - mark_v_done acc [str] | Declare sl -> let declare suff dir s = let base = file_name s dir in diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index d86e05d8cf..743853738a 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -326,17 +326,6 @@ let rec traite_fichier_Coq suffixe verbose f = if verbose && not (Hashtbl.mem coqlibKnown str) then warning_module_notfound f str end) strl - | RequireString s -> - let str = Filename.basename s in - if not (List.mem [str] !deja_vu_v) then begin - addQueue deja_vu_v [str]; - try - let file_str = Hashtbl.find vKnown [str] in - printf " %s%s" (canonize file_str) suffixe - with Not_found -> - if not (Hashtbl.mem coqlibKnown [str]) then - warning_notfound f s - end | Declare sl -> let declare suff dir s = let base = file_name s dir in diff --git a/tools/coqdep_lexer.mli b/tools/coqdep_lexer.mli index b447030afd..c7b9c9a0a8 100644 --- a/tools/coqdep_lexer.mli +++ b/tools/coqdep_lexer.mli @@ -12,7 +12,6 @@ type qualid = string list type coq_token = Require of qualid list - | RequireString of string | Declare of string list | Load of string | AddLoadPath of string diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll index 8ecc419c87..5692e5b45f 100644 --- a/tools/coqdep_lexer.mll +++ b/tools/coqdep_lexer.mll @@ -17,7 +17,6 @@ type coq_token = | Require of qualid list - | RequireString of string | Declare of string list | Load of string | AddLoadPath of string @@ -277,10 +276,6 @@ and require_file = parse | Some from -> (from_pre_ident := None ; Require (List.map (fun x -> from @ x) qid)) } - | '"' [^'"']* '"' (*'"'*) - { let s = Lexing.lexeme lexbuf in - parse_dot lexbuf; - RequireString (unquote_vfile_string s) } | eof { syntax_error lexbuf } | _ -- cgit v1.2.3 From 0917ce7cf48cadacc6fca48ba18b395740cccbe2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 1 Jul 2015 11:25:47 +0200 Subject: Notation: use same level for "@" in constr: and pattern: (Close: #4272) A possible script breakage can occur if one has a notation at level 11 that is also right associative (now 11 is left associative). Thanks Georges for debugging that. --- parsing/g_constr.ml4 | 4 ++-- parsing/pcoq.ml4 | 4 ++-- test-suite/bugs/closed/4272.v | 12 ++++++++++++ 3 files changed, 16 insertions(+), 4 deletions(-) create mode 100644 test-suite/bugs/closed/4272.v diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 74f17f9fb6..e47e3fb1e6 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -364,10 +364,10 @@ GEXTEND Gram | "100" RIGHTA [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CPatOr (!@loc,p::pl) ] | "99" RIGHTA [ ] - | "10" LEFTA + | "11" LEFTA [ p = pattern; "as"; id = ident -> CPatAlias (!@loc, p, id) ] - | "9" RIGHTA + | "10" RIGHTA [ p = pattern; lp = LIST1 NEXT -> (match p with | CPatAtom (_, Some r) -> CPatCstr (!@loc, r, [], lp) diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 54edbb2c88..797b031fe4 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -459,8 +459,8 @@ let default_pattern_levels = [200,Extend.RightA,true; 100,Extend.RightA,false; 99,Extend.RightA,true; - 10,Extend.LeftA,false; - 9,Extend.RightA,false; + 11,Extend.LeftA,false; + 10,Extend.RightA,false; 1,Extend.LeftA,false; 0,Extend.RightA,false] diff --git a/test-suite/bugs/closed/4272.v b/test-suite/bugs/closed/4272.v new file mode 100644 index 0000000000..aeb4c9bb95 --- /dev/null +++ b/test-suite/bugs/closed/4272.v @@ -0,0 +1,12 @@ +Set Implicit Arguments. + +Record foo := Foo { p1 : Type; p2 : p1 }. + +Variable x : foo. + +Let p := match x with @Foo a b => a end. + +Notation "@ 'id'" := 3 (at level 10). +Notation "@ 'sval'" := 3 (at level 10). + +Let q := match x with @Foo a b => a end. -- cgit v1.2.3 From dab5c4c642ee9b25d488c476d55db232cf74006b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 30 Jun 2015 15:43:14 +0200 Subject: Further simplification of the graph traversal in Univ. We passed the arc to be marked as visited to the functions pushing the neighbours on the remaining stack, but this can be actually done before pushing them, as the [process_le] and [process_lt] functions do not rely on the visited flag. This exposes more clearly the invariants of the algorithm. --- kernel/univ.ml | 25 ++++++++++++------------- 1 file changed, 12 insertions(+), 13 deletions(-) diff --git a/kernel/univ.ml b/kernel/univ.ml index fce9e28d36..1d82be63b9 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -925,7 +925,8 @@ let fast_compare_neq strict g arcu arcv = if arc_is_lt arc then cmp c to_revert lt_todo le_todo else - process_lt c to_revert lt_todo le_todo arc arc.lt arc.le + let () = arc.status <- SetLt in + process_lt c (arc :: to_revert) lt_todo le_todo arc.lt arc.le | [], arc::le_todo -> if arc == arcv then (* No need to continue inspecting universes above arc: @@ -937,40 +938,38 @@ let fast_compare_neq strict g arcu arcv = if arc_is_le arc then cmp c to_revert [] le_todo else - process_le c to_revert [] le_todo arc arc.lt + let () = arc.status <- SetLe in + process_le c (arc :: to_revert) [] le_todo arc.lt arc.le - and process_lt c to_revert lt_todo le_todo arc0 lt le = match le with + and process_lt c to_revert lt_todo le_todo lt le = match le with | [] -> begin match lt with - | [] -> - let () = arc0.status <- SetLt in - cmp c (arc0 :: to_revert) lt_todo le_todo + | [] -> cmp c to_revert lt_todo le_todo | u :: lt -> let arc = repr g u in if arc == arcv then if strict then (to_revert, FastLT) else (to_revert, FastLE) - else process_lt c to_revert (arc :: lt_todo) le_todo arc0 lt le + else process_lt c to_revert (arc :: lt_todo) le_todo lt le end | u :: le -> let arc = repr g u in if arc == arcv then if strict then (to_revert, FastLT) else (to_revert, FastLE) - else process_lt c to_revert (arc :: lt_todo) le_todo arc0 lt le + else process_lt c to_revert (arc :: lt_todo) le_todo lt le - and process_le c to_revert lt_todo le_todo arc0 lt = match lt with + and process_le c to_revert lt_todo le_todo lt le = match lt with | [] -> let fold accu u = let node = repr g u in node :: accu in - let le_new = List.fold_left fold le_todo arc0.le in - let () = arc0.status <- SetLe in - cmp c (arc0 :: to_revert) lt_todo le_new + let le_new = List.fold_left fold le_todo le in + cmp c to_revert lt_todo le_new | u :: lt -> let arc = repr g u in if arc == arcv then if strict then (to_revert, FastLT) else (to_revert, FastLE) - else process_le c to_revert (arc :: lt_todo) le_todo arc0 lt + else process_le c to_revert (arc :: lt_todo) le_todo lt le in -- cgit v1.2.3 From a9665989a93014355ab152920c0a0e58cf0a7dfe Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 1 Jul 2015 12:39:57 +0200 Subject: Display functions for primitive projections. --- kernel/names.ml | 4 ++++ kernel/names.mli | 4 ++++ 2 files changed, 8 insertions(+) diff --git a/kernel/names.ml b/kernel/names.ml index 480b37e897..f217c932cc 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -819,6 +819,10 @@ struct let map f (c, b as x) = let c' = f c in if c' == c then x else (c', b) + + let to_string p = Constant.to_string (constant p) + let print p = Constant.print (constant p) + end type projection = Projection.t diff --git a/kernel/names.mli b/kernel/names.mli index 92ee58f260..7cc4443752 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -652,6 +652,10 @@ module Projection : sig val compare : t -> t -> int val map : (constant -> constant) -> t -> t + + val to_string : t -> string + val print : t -> Pp.std_ppcmds + end type projection = Projection.t -- cgit v1.2.3 From 7dd0c2875b4986d5bfb7615f9cd0c145b6609fe3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 2 Jul 2015 09:24:42 +0200 Subject: Fix loop in assumptions (Close: #4275) --- toplevel/assumptions.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml index fff7e2e21e..a11653a43b 100644 --- a/toplevel/assumptions.ml +++ b/toplevel/assumptions.ml @@ -164,7 +164,8 @@ let rec traverse current ctx accu t = match kind_of_term t with 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 + | _ -> + 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 @@ -182,6 +183,7 @@ and traverse_object ?inhabits (curr, data, ax2ty) body obj = with Not_found -> Refmap.add obj [ty] ax2ty in data, ax2ty | Some body -> + if already_in then data, ax2ty else let contents,data,ax2ty = traverse (label_of obj) [] (Refset.empty,data,ax2ty) body in Refmap.add obj contents data, ax2ty -- cgit v1.2.3 From b6320588bdc54f0239a537339a359baa5e4d07d4 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 2 Jul 2015 14:32:11 +0200 Subject: Revert "Add target to install dev files." Broke the build. This reverts commit ef6459b00999a29183edc09de9035795ff7912e9. --- Makefile.build | 8 ++------ Makefile.common | 4 ---- 2 files changed, 2 insertions(+), 10 deletions(-) diff --git a/Makefile.build b/Makefile.build index 71fd8fb544..16c5730865 100644 --- a/Makefile.build +++ b/Makefile.build @@ -690,13 +690,13 @@ ifeq ($(LOCAL),true) install: @echo "Nothing to install in a local build!" else -install: install-coq install-coqide install-doc-$(WITHDOC) install-dev +install: install-coq install-coqide install-doc-$(WITHDOC) endif install-doc-all: install-doc install-doc-no: -.PHONY: install install-doc-all install-doc-no install-dev +.PHONY: install install-doc-all install-doc-no #These variables are intended to be set by the caller to make #COQINSTALLPREFIX= @@ -750,10 +750,6 @@ install-tools: $(INSTALLLIB) tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc $(INSTALLBIN) $(TOOLS) $(FULLBINDIR) -install-dev: $(DEVFILES) $(DEVPRINTERS) - $(foreach devf, $(DEVFILES), sed -i -e /\".\"/\"$(FULLCOQLIB)\"/g $(devf)) - $(INSTALLLIB) $(DEVFILES) $(DEVPRINTERS) $(FULLCOQLIB)/dev - # The list of .cmi to install, including the ones obtained # from .mli without .ml, and the ones obtained from .ml without .mli diff --git a/Makefile.common b/Makefile.common index 5a81dcfbb2..07df8bb157 100644 --- a/Makefile.common +++ b/Makefile.common @@ -253,10 +253,6 @@ CSDPCERTCMO:=$(addprefix plugins/micromega/, \ mutils.cmo micromega.cmo \ sos_types.cmo sos_lib.cmo sos.cmo csdpcert.cmo ) -DEVPRINTERS:=dev/vm_printers.ml dev/top_printers.ml - -DEVFILES:=dev/base_include dev/include - DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma COQDEPCMO:=$(COQENVCMO) tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep.cmo -- cgit v1.2.3 From 44f45f58dc0a169286c9fcfa7d2edbc8bc04673b Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 2 Jul 2015 15:39:12 +0200 Subject: More robust pattern matching on structured constants in VM. --- kernel/csymtable.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index b29f06c652..49ab68beae 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -57,11 +57,14 @@ let set_global v = let rec eq_structured_constant c1 c2 = match c1, c2 with | Const_sorts s1, Const_sorts s2 -> Sorts.equal s1 s2 +| Const_sorts _, _ -> false | Const_ind i1, Const_ind i2 -> Univ.eq_puniverses eq_ind i1 i2 +| Const_ind _, _ -> false | Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2 +| Const_b0 _, _ -> false | Const_bn (t1, a1), Const_bn (t2, a2) -> Int.equal t1 t2 && Array.equal eq_structured_constant a1 a2 -| _ -> false +| Const_bn _, _ -> false let rec hash_structured_constant c = let open Hashset.Combine in -- cgit v1.2.3