diff options
-rw-r--r-- | ide/coq.ml | 1 | ||||
-rw-r--r-- | interp/implicit_quantifiers.ml | 56 | ||||
-rw-r--r-- | interp/implicit_quantifiers.mli | 2 | ||||
-rw-r--r-- | parsing/g_vernac.ml4 | 9 | ||||
-rw-r--r-- | parsing/ppvernac.ml | 11 | ||||
-rw-r--r-- | plugins/interface/xlate.ml | 1 | ||||
-rw-r--r-- | theories/Classes/EquivDec.v | 2 | ||||
-rw-r--r-- | theories/Classes/Equivalence.v | 2 | ||||
-rw-r--r-- | theories/Classes/Functions.v | 2 | ||||
-rw-r--r-- | theories/Classes/Morphisms.v | 2 | ||||
-rw-r--r-- | theories/Classes/RelationClasses.v | 2 | ||||
-rw-r--r-- | theories/Classes/SetoidAxioms.v | 2 | ||||
-rw-r--r-- | theories/Classes/SetoidClass.v | 2 | ||||
-rw-r--r-- | theories/Classes/SetoidDec.v | 2 | ||||
-rw-r--r-- | theories/Classes/SetoidTactics.v | 4 | ||||
-rw-r--r-- | theories/Logic/Diaconescu.v | 2 | ||||
-rw-r--r-- | theories/MSets/MSetFacts.v | 2 | ||||
-rw-r--r-- | theories/Structures/OrderedType2.v | 2 | ||||
-rw-r--r-- | tools/coq_makefile.ml4 | 4 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 3 | ||||
-rw-r--r-- | toplevel/vernacexpr.ml | 1 |
21 files changed, 102 insertions, 12 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index eb410b1e3..11d8a3061 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -274,6 +274,7 @@ let rec attribute_of_vernac_command = function | VernacSyntacticDefinition _ -> [] | VernacDeclareImplicits _ -> [] | VernacReserve _ -> [] + | VernacGeneralizable _ -> [] | VernacSetOpacity _ -> [] | VernacSetOption (_,["Ltac";"Debug"], _) -> [DebugCommand] | VernacSetOption (_,o,BoolValue true) | VernacUnsetOption (_,o) -> diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index a55daff36..93f4eedff 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -24,8 +24,49 @@ open Libnames open Typeclasses open Typeclasses_errors open Pp +open Libobject +open Nameops (*i*) +let generalizable_table = ref Idpred.empty + +let _ = + Summary.declare_summary "generalizable-ident" + { Summary.freeze_function = (fun () -> !generalizable_table); + Summary.unfreeze_function = (fun r -> generalizable_table := r); + Summary.init_function = (fun () -> generalizable_table := Idpred.empty) } + +let declare_generalizable_ident table (loc,id) = + if id <> root_of_id id then + user_err_loc(loc,"declare_generalizable_ident", + (pr_id id ++ str + " is not declarable as generalizable identifier: it must have no trailing digits, quote, or _")); + if Idpred.mem id table then + user_err_loc(loc,"declare_generalizable_ident", + (pr_id id++str" is already declared as a generalizable identifier")) + else Idpred.add id table + +let add_generalizable gen table = + match gen with + | None -> Idpred.empty + | Some [] -> Idpred.full + | Some l -> List.fold_left (fun table lid -> declare_generalizable_ident table lid) + table l + +let cache_generalizable_type (_,(local,cmd)) = + generalizable_table := add_generalizable cmd !generalizable_table + +let (in_generalizable, _) = + declare_object {(default_object "GENERALIZED-IDENT") with + cache_function = cache_generalizable_type; + classify_function = (fun (local, _ as obj) -> if local then Dispose else Keep obj) + } + +let declare_generalizable local gen = + Lib.add_anonymous_leaf (in_generalizable (local, gen)) + +let find_generalizable_ident id = Idpred.mem (root_of_id id) !generalizable_table + let ids_of_list l = List.fold_right Idset.add l Idset.empty @@ -51,13 +92,16 @@ let is_freevar ids env x = (* Auxilliary functions for the inference of implicitly quantified variables. *) let free_vars_of_constr_expr c ?(bound=Idset.empty) l = - let found id bdvars l = + let found loc id bdvars l = if List.mem id l then l - else if not (is_freevar bdvars (Global.env ()) id) - then l else id :: l + else if is_freevar bdvars (Global.env ()) id + then + if find_generalizable_ident id then id :: l + else user_err_loc (loc, "Generalization", str "Unbound and ungeneralizable variable " ++ pr_id id) + else l in let rec aux bdvars l c = match c with - | CRef (Ident (_,id)) -> found id bdvars l + | CRef (Ident (loc,id)) -> found loc id bdvars l | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id)) :: _, [])) when not (Idset.mem id bdvars) -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c | c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c @@ -204,14 +248,14 @@ let combine_params_freevar = let destClassApp cl = match cl with - | CApp (loc, (None,CRef ref), l) -> loc, ref, List.map fst l + | CApp (loc, (None, CRef ref), l) -> loc, ref, List.map fst l | CAppExpl (loc, (None, ref), l) -> loc, ref, l | CRef ref -> loc_of_reference ref, ref, [] | _ -> raise Not_found let destClassAppExpl cl = match cl with - | CApp (loc, (None,CRef ref), l) -> loc, ref, l + | CApp (loc, (None, CRef ref), l) -> loc, ref, l | CRef ref -> loc_of_reference ref, ref, [] | _ -> raise Not_found diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 0d28eccad..8f02eb765 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -24,6 +24,8 @@ open Libnames open Typeclasses (*i*) +val declare_generalizable : Vernacexpr.locality_flag -> (identifier located) list option -> unit + val ids_of_list : identifier list -> Idset.t val destClassApp : constr_expr -> loc * reference * constr_expr list val destClassAppExpl : constr_expr -> loc * reference * (constr_expr * explicitation located option) list diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index e1a71ff23..52cb3d898 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -518,7 +518,7 @@ GEXTEND Gram pri = OPT [ "|"; i = natural -> i ] ; props = [ ":="; "{"; r = record_declaration; "}" -> r | ":="; c = lconstr -> c | -> CRecord (loc, None, []) ] -> - VernacInstance (not (use_non_locality ()), [], ((loc,Anonymous), expl, t), props, pri) + VernacInstance (not (use_section_locality ()), [], ((loc,Anonymous), expl, t), props, pri) | IDENT "Instance"; name = identref; sup = OPT binders_let; ":"; expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200"; @@ -545,7 +545,12 @@ GEXTEND Gram VernacDeclareImplicits (use_section_locality (),qid,pos) | IDENT "Implicit"; ["Type" | IDENT "Types"]; - idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c) ] ] + idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c) + + | IDENT "Generalizable"; ["Variable" | IDENT "Variables"]; + gen = [ IDENT "none" -> None | IDENT "all" -> Some [] | + idl = LIST1 identref -> Some idl ] -> + VernacGeneralizable (use_section_locality (), gen) ] ] ; implicit_name: [ [ "!"; id = ident -> (id, false, true) diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 76098e4fb..8a8248bf4 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -831,7 +831,8 @@ let rec pr_vernac = function (pr_locality local ++ str "Ltac " ++ prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l) | VernacCreateHintDb (local,dbname,b) -> - hov 1 (pr_locality local ++ str "Create " ++ str "HintDb " ++ str dbname ++ (if b then str" discriminated" else mt ())) + hov 1 (pr_locality local ++ str "Create " ++ str "HintDb " ++ + str dbname ++ (if b then str" discriminated" else mt ())) | VernacHints (local,dbnames,h) -> pr_hints local dbnames h pr_constr pr_constr_pattern_expr | VernacSyntacticDefinition (id,(ids,c),local,onlyparsing) -> @@ -851,6 +852,14 @@ let rec pr_vernac = function str (if List.length idl > 1 then "s " else " ") ++ prlist_with_sep spc pr_lident idl ++ str " :" ++ spc () ++ pr_lconstr c) + | VernacGeneralizable (local, g) -> + hov 1 (pr_locality local ++ str"Generalizable Variable" ++ + match g with + | None -> str "s none" + | Some [] -> str "s all" + | Some idl -> + str (if List.length idl > 1 then "s " else " ") ++ + prlist_with_sep spc pr_lident idl) | VernacSetOpacity(b,[k,l]) when k=Conv_oracle.transparent -> hov 1 (str"Transparent" ++ pr_non_locality b ++ spc() ++ prlist_with_sep sep pr_smart_global l) diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml index b4e0e69bb..627cd517c 100644 --- a/plugins/interface/xlate.ml +++ b/plugins/interface/xlate.ml @@ -2183,6 +2183,7 @@ let rec xlate_vernac = List.map (fun (_,x) -> xlate_ident x) l), xlate_formula f) | VernacReserve([], _) -> assert false + | VernacGeneralizable (_, _) -> xlate_error "TODO: Generalizable" | VernacLocate(LocateTerm id) -> CT_locate(loc_smart_global_to_ct_ID id) | VernacLocate(LocateLibrary id) -> CT_locate_lib(reference_to_ct_ID id) | VernacLocate(LocateModule _) -> xlate_error "TODO: Locate Module" diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index e87482d84..bafbac3f1 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -26,6 +26,8 @@ Require Import Coq.Bool.Bool. Require Import Coq.Arith.Peano_dec. Require Import Coq.Program.Program. +Generalizable Variables A B R. + Open Scope equiv_scope. Class DecidableEquivalence `(equiv : Equivalence A) := diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index 78e66d374..cc8d79c03 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -25,6 +25,8 @@ Require Import Coq.Classes.Morphisms. Set Implicit Arguments. Unset Strict Implicit. +Generalizable Variables A R eqA B S eqB. + Open Local Scope signature_scope. Definition equiv `{Equivalence A R} : relation A := R. diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v index 8c6161036..5efa4fa8f 100644 --- a/theories/Classes/Functions.v +++ b/theories/Classes/Functions.v @@ -17,6 +17,8 @@ Require Import Coq.Classes.RelationClasses. Require Import Coq.Classes.Morphisms. +Generalizable Variables A B eqA eqB RA RB f. + Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 76da120e0..ac455415e 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -20,6 +20,8 @@ Require Import Coq.Program.Tactics. Require Import Coq.Relations.Relation_Definitions. Require Export Coq.Classes.RelationClasses. +Generalizable Variables all. + (** * Morphisms. We now turn to the definition of [Proper] and declare standard instances. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 0d6130263..cc3cae4da 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -74,6 +74,8 @@ Hint Extern 4 => solve_relation : relations. (** We can already dualize all these properties. *) +Generalizable Variables A B C D R S T U eqA eqB eqC eqD. + Program Lemma flip_Reflexive `(Reflexive A R) : Reflexive (flip R). Proof. tauto. Qed. diff --git a/theories/Classes/SetoidAxioms.v b/theories/Classes/SetoidAxioms.v index ef115b2ed..3789bb66f 100644 --- a/theories/Classes/SetoidAxioms.v +++ b/theories/Classes/SetoidAxioms.v @@ -19,6 +19,8 @@ Require Import Coq.Program.Program. Set Implicit Arguments. Unset Strict Implicit. +Generalizable Variables a. + Require Export Coq.Classes.SetoidClass. (** Application of the extensionality axiom to turn a goal on diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index 33d98548d..995b37185 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -17,6 +17,8 @@ Set Implicit Arguments. Unset Strict Implicit. +Generalizable Variables A. + Require Import Coq.Program.Program. Require Import Relation_Definitions. diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index 32e75adae..33b4350f8 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -18,6 +18,8 @@ Set Implicit Arguments. Unset Strict Implicit. +Generalizable Variables A B . + (** Export notations. *) Require Export Coq.Classes.SetoidClass. diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index c40e37e24..669be8b0f 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -18,6 +18,8 @@ Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop. Require Export Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions. Require Import Coq.Classes.Equivalence Coq.Program.Basics. +Generalizable Variables A R. + Export ProperNotations. Set Implicit Arguments. @@ -177,3 +179,5 @@ Ltac default_add_morphism_tactic := Ltac add_morphism_tactic := default_add_morphism_tactic. Obligation Tactic := program_simpl. + +(* Notation "'Morphism' s t " := (@Proper _ (s%signature) t) (at level 10, s at next level, t at next level). *) diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index 22c838c26..18f3181b6 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -39,7 +39,7 @@ [Bell93] John L. Bell, Hilbert's epsilon operator and classical logic, Journal of Philosophical Logic, 22: 1-18, 1993 - [Carlström04] Jesper Carlström, [EM + Ext_ + AC_int <-> AC_ext], + [Carlström04] Jesper Carlström, EM + Ext_ + AC_int <-> AC_ext, Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004. *) diff --git a/theories/MSets/MSetFacts.v b/theories/MSets/MSetFacts.v index 2ba969217..bd99198f4 100644 --- a/theories/MSets/MSetFacts.v +++ b/theories/MSets/MSetFacts.v @@ -489,6 +489,8 @@ Qed. (* [fold], [filter], [for_all], [exists_] and [partition] requires some knowledge on [f] in order to be known as morphisms. *) +Generalizable Variables f. + Instance filter_equal `(Proper _ (E.eq==>Logic.eq) f) : Proper (Equal==>Equal) (filter f). Proof. diff --git a/theories/Structures/OrderedType2.v b/theories/Structures/OrderedType2.v index fdb1ccc24..c72d3a79d 100644 --- a/theories/Structures/OrderedType2.v +++ b/theories/Structures/OrderedType2.v @@ -270,6 +270,8 @@ Definition FstRel {A B}(R:relation A) : relation (A*B) := Definition SndRel {A B}(R:relation B) : relation (A*B) := fun p p' => R (snd p) (snd p'). +Generalizable Variables A B RA RB Ri Ro. + Instance ProdRel_equiv {A B} `(Equivalence A RA)`(Equivalence B RB) : Equivalence (ProdRel RA RB). Proof. firstorder. Qed. diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index 486c8804f..31af75fee 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -402,10 +402,10 @@ let main_targets vfiles mlfiles other_targets inc = print "spec: $(VIFILES)\n\n"; print "gallina: $(GFILES)\n\n"; print "html: $(GLOBFILES) $(VFILES)\n"; - print "\t- mkdir html\n"; + print "\t- mkdir -p html\n"; print "\t$(COQDOC) -toc -html $(COQDOCLIBS) -d html $(VFILES)\n\n"; print "gallinahtml: $(GLOBFILES) $(VFILES)\n"; - print "\t- mkdir html\n"; + print "\t- mkdir -p html\n"; print "\t$(COQDOC) -toc -html -g $(COQDOCLIBS) -d html $(VFILES)\n\n"; print "all.ps: $(VFILES)\n"; print "\t$(COQDOC) -toc -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n"; diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 754f58a9c..70feb6ceb 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -771,6 +771,8 @@ let vernac_reserve idl c = let t = Detyping.detype false [] [] t in List.iter (fun id -> Reserve.declare_reserved_type id t) idl +let vernac_generalizable = Implicit_quantifiers.declare_generalizable + let make_silent_if_not_pcoq b = if !pcoq <> None then error "Turning on/off silent flag is not supported in Pcoq mode." @@ -1375,6 +1377,7 @@ let interp c = match c with | VernacSyntacticDefinition (id,c,l,b) ->vernac_syntactic_definition id c l b | VernacDeclareImplicits (local,qid,l) ->vernac_declare_implicits local qid l | VernacReserve (idl,c) -> vernac_reserve idl c + | VernacGeneralizable (local,gen) -> vernac_generalizable local gen | VernacSetOpacity (local,qidl) -> vernac_set_opacity local qidl | VernacSetOption (locality,key,v) -> vernac_set_option locality key v | VernacUnsetOption (locality,key) -> vernac_unset_option locality key diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 25642bdc7..2e73767c5 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -301,6 +301,7 @@ type vernac_expr = | VernacDeclareImplicits of locality_flag * reference or_by_notation * (explicitation * bool * bool) list option | VernacReserve of lident list * constr_expr + | VernacGeneralizable of locality_flag * (lident list) option | VernacSetOpacity of locality_flag * (Conv_oracle.level * reference or_by_notation list) list | VernacUnsetOption of full_locality_flag * Goptions.option_name |