diff options
30 files changed, 194 insertions, 130 deletions
diff --git a/Makefile.build b/Makefile.build index c7b0c5262..623428328 100644 --- a/Makefile.build +++ b/Makefile.build @@ -688,13 +688,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= @@ -748,10 +748,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 342ce7727..15ac13ff1 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) lib/system.cmo tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep.cmo diff --git a/dev/make-installer-win32.sh b/dev/make-installer-win32.sh index ec7cd5773..c6ed2f401 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 73e1fdbeb..03fdda4aa 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/*" 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/engine/termops.ml b/engine/termops.ml index 9f04faa83..937471cf7 100644 --- a/engine/termops.ml +++ b/engine/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/engine/termops.mli b/engine/termops.mli index 2552c67e6..4581e2310 100644 --- a/engine/termops.mli +++ b/engine/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/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index f6fd27dd8..2e725b46c 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 9db89308f..03061d8bd 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 86714ca4d..ce53680f3 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 0ca3bb35f..b72577e1e 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 *) diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index b29f06c65..49ab68bea 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 diff --git a/kernel/names.ml b/kernel/names.ml index 480b37e89..f217c932c 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 92ee58f26..7cc444375 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 diff --git a/kernel/univ.ml b/kernel/univ.ml index fce9e28d3..1d82be63b 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 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/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 74f17f9fb..e47e3fb1e 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 54edbb2c8..797b031fe 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/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/tactics/class_tactics.ml b/tactics/class_tactics.ml index e1fe51656..3deb8ad38 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 @@ -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 | _ -> diff --git a/test-suite/bugs/closed/4272.v b/test-suite/bugs/closed/4272.v new file mode 100644 index 000000000..aeb4c9bb9 --- /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. diff --git a/tools/coqdep.ml b/tools/coqdep.ml index dd5593f65..f1a3131dd 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -62,7 +62,6 @@ let sort () = try loop (Hashtbl.find vKnown s) with Not_found -> ()) sl - | RequireString s -> loop s | _ -> () done with Fin_fichier -> @@ -320,9 +319,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 9b7845b09..38e454aef 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -316,17 +316,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 b447030af..c7b9c9a0a 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 8ecc419c8..5692e5b45 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 } | _ diff --git a/library/assumptions.ml b/toplevel/assumptions.ml index 62645b236..a11653a43 100644 --- a/library/assumptions.ml +++ b/toplevel/assumptions.ml @@ -22,34 +22,7 @@ open Term open Declarations open Mod_subst open Globnames - -type context_object = - | Variable of Id.t (* A section variable or a Let definition *) - | Axiom of constant (* An axiom or a constant. *) - | 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) +open Printer (** 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] @@ -161,7 +134,16 @@ let lookup_constant cst = (** 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 + +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) @@ -173,22 +155,44 @@ let rec traverse accu t = match kind_of_term t with | 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 +| 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) = traverse (Refset.empty, data) body in - Refmap.add obj contents data + 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 in - (Refset.add obj curr, data) + (Refset.add obj curr, data, ax2ty) -let traverse t = +let traverse current t = let () = modcache := MPmap.empty in - traverse (Refset.empty, Refmap.empty) t + 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 @@ -198,10 +202,10 @@ let type_of_constant cb = match cb.Declarations.const_type with | 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 assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = let (idts, knst) = st in (** Only keep the transitive dependencies *) - let (_, graph) = traverse t in + 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 @@ -211,7 +215,8 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st t = 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 + 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 diff --git a/library/assumptions.mli b/toplevel/assumptions.mli index bb36a9725..a608fe505 100644 --- a/library/assumptions.mli +++ b/toplevel/assumptions.mli @@ -10,19 +10,7 @@ open Util open Names open Term open Globnames - -(** A few declarations for the "Print Assumption" command - @author spiwack *) -type context_object = - | Variable of Id.t (** A section variable or a Let definition *) - | Axiom of constant (** An axiom or a constant. *) - | Opaque of constant (** An opaque constant. *) - | Transparent of constant (** A transparent constant *) - -(** AssumptionSet.t is a set of [assumption] *) -module ContextObjectSet : Set.S with type elt = context_object -module ContextObjectMap : Map.ExtS - with type key = context_object and module Set := ContextObjectSet +open Printer (** Collects all the objects on which a term directly relies, bypassing kernel opacity, together with the recursive dependence DAG of objects. @@ -31,11 +19,14 @@ module ContextObjectMap : Map.ExtS sealed inside opaque modules. Do not try to do anything fancy with those terms apart from printing them, otherwise demons may fly out of your nose. *) -val traverse : constr -> (Refset.t * Refset.t Refmap.t) +val traverse : + Label.t -> 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 -> constr -> - Term.types ContextObjectMap.t + ?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 |