From 05fc0542f6c7a15b9187a2a91beb0aa7a42bb2fa Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 12 Dec 2017 19:36:15 +0100 Subject: Remove the local polymorphic flag hack. Some code in typeclasses was even breaking the invariant that use_polymorphic_flag should not be called twice, but that code was morally dead it seems, so we remove it. --- API/API.mli | 4 +-- lib/flags.ml | 8 ----- lib/flags.mli | 4 --- plugins/ltac/extratactics.ml4 | 70 ++++++++++++++++++++++++------------------- plugins/ltac/rewrite.ml | 5 ++-- pretyping/typeclasses.ml | 6 ++-- pretyping/typeclasses.mli | 2 +- tactics/leminv.ml | 7 ++--- tactics/leminv.mli | 2 +- vernac/classes.ml | 6 ++-- vernac/vernacentries.ml | 15 +++++----- 11 files changed, 60 insertions(+), 69 deletions(-) diff --git a/API/API.mli b/API/API.mli index def60ec26..682fef1fc 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4331,7 +4331,7 @@ sig val class_info : Globnames.global_reference -> typeclass val mark_resolvables : ?filter:evar_filter -> Evd.evar_map -> Evd.evar_map val add_instance : instance -> unit - val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool -> Decl_kinds.polymorphic -> + val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool -> Globnames.global_reference -> instance end @@ -5798,7 +5798,7 @@ sig val lemInv_clause : Misctypes.quantified_hypothesis -> EConstr.constr -> Names.Id.t list -> unit Proofview.tactic val add_inversion_lemma_exn : - Names.Id.t -> Constrexpr.constr_expr -> Sorts.family -> bool -> (Names.Id.t -> unit Proofview.tactic) -> + poly:bool -> Names.Id.t -> Constrexpr.constr_expr -> Sorts.family -> bool -> (Names.Id.t -> unit Proofview.tactic) -> unit end diff --git a/lib/flags.ml b/lib/flags.ml index 644f66d02..eca9a69de 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -110,14 +110,6 @@ let universe_polymorphism = ref false let make_universe_polymorphism b = universe_polymorphism := b let is_universe_polymorphism () = !universe_polymorphism -let local_polymorphic_flag = ref None -let use_polymorphic_flag () = - match !local_polymorphic_flag with - | Some p -> local_polymorphic_flag := None; p - | None -> is_universe_polymorphism () -let make_polymorphic_flag b = - local_polymorphic_flag := Some b - let polymorphic_inductive_cumulativity = ref false let make_polymorphic_inductive_cumulativity b = polymorphic_inductive_cumulativity := b let is_polymorphic_inductive_cumulativity () = !polymorphic_inductive_cumulativity diff --git a/lib/flags.mli b/lib/flags.mli index 000862b2c..95916d3ab 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -77,10 +77,6 @@ val is_program_mode : unit -> bool val make_universe_polymorphism : bool -> unit val is_universe_polymorphism : unit -> bool -(** Local universe polymorphism flag. *) -val make_polymorphic_flag : bool -> unit -val use_polymorphic_flag : unit -> bool - (** Global polymorphic inductive cumulativity flag. *) val make_polymorphic_inductive_cumulativity : bool -> unit val is_polymorphic_inductive_cumulativity : unit -> bool diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 982fc7cc3..cf5125757 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -25,6 +25,7 @@ open Termops open Equality open Misctypes open Proofview.Notations +open Vernacinterp DECLARE PLUGIN "ltac_plugin" @@ -249,11 +250,10 @@ TACTIC EXTEND rewrite_star (**********************************************************************) (* Hint Rewrite *) -let add_rewrite_hint bases ort t lcsr = +let add_rewrite_hint ~poly bases ort t lcsr = let env = Global.env() in let sigma = Evd.from_env env in - let poly = Flags.use_polymorphic_flag () in - let f ce = + let f ce = let c, ctx = Constrintern.interp_constr env sigma ce in let ctx = let ctx = UState.context_set ctx in @@ -270,16 +270,16 @@ let add_rewrite_hint bases ort t lcsr = let classify_hint _ = Vernacexpr.VtSideff [], Vernacexpr.VtLater -VERNAC COMMAND EXTEND HintRewrite CLASSIFIED BY classify_hint +VERNAC COMMAND FUNCTIONAL EXTEND HintRewrite CLASSIFIED BY classify_hint [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] -> - [ add_rewrite_hint bl o None l ] + [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic bl o None l; st ] | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ":" preident_list(bl) ] -> - [ add_rewrite_hint bl o (Some t) l ] + [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic bl o (Some t) l; st ] | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] -> - [ add_rewrite_hint ["core"] o None l ] + [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic ["core"] o None l; st ] | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] -> - [ add_rewrite_hint ["core"] o (Some t) l ] + [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic ["core"] o (Some t) l; st ] END (**********************************************************************) @@ -290,7 +290,7 @@ open EConstr open Vars open Coqlib -let project_hint pri l2r r = +let project_hint ~poly pri l2r r = let gr = Smartlocate.global_with_alias r in let env = Global.env() in let sigma = Evd.from_env env in @@ -313,30 +313,28 @@ let project_hint pri l2r r = let id = Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l")) in - let poly = Flags.use_polymorphic_flag () in let ctx = Evd.const_univ_entry ~poly sigma in let c = EConstr.to_constr sigma c in let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in let info = {Vernacexpr.hint_priority = pri; hint_pattern = None} in (info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c)) -let add_hints_iff ?locality l2r lc n bl = - Hints.add_hints (Locality.make_module_locality locality) bl - (Hints.HintsResolveEntry (List.map (project_hint n l2r) lc)) +let add_hints_iff ~atts l2r lc n bl = + let open Vernacinterp in + Hints.add_hints (Locality.make_module_locality atts.locality) bl + (Hints.HintsResolveEntry (List.map (project_hint ~poly:atts.polymorphic n l2r) lc)) VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) ":" preident_list(bl) ] -> [ fun ~atts ~st -> begin - let open Vernacinterp in - add_hints_iff ?locality:atts.locality true lc n bl; + add_hints_iff ~atts true lc n bl; st end ] | [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) ] -> [ fun ~atts ~st -> begin - let open Vernacinterp in - add_hints_iff ?locality:atts.locality true lc n ["core"]; + add_hints_iff ~atts true lc n ["core"]; st end ] @@ -346,15 +344,13 @@ VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffRL CLASSIFIED AS SIDEFF [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n) ":" preident_list(bl) ] -> [ fun ~atts ~st -> begin - let open Vernacinterp in - add_hints_iff ?locality:atts.locality false lc n bl; + add_hints_iff ~atts false lc n bl; st end ] | [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n) ] -> [ fun ~atts ~st -> begin - let open Vernacinterp in - add_hints_iff ?locality:atts.locality false lc n ["core"]; + add_hints_iff ~atts false lc n ["core"]; st end ] @@ -430,34 +426,46 @@ let seff id = Vernacexpr.VtSideff [id], Vernacexpr.VtLater | [ "Type" ] -> [ InType ] END*) -VERNAC COMMAND EXTEND DeriveInversionClear +VERNAC COMMAND FUNCTIONAL EXTEND DeriveInversionClear | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ] => [ seff na ] - -> [ add_inversion_lemma_exn na c s false inv_clear_tac ] + -> [ fun ~atts ~st -> + let open Vernacinterp in + add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_clear_tac; st ] | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => [ seff na ] - -> [ add_inversion_lemma_exn na c Sorts.InProp false inv_clear_tac ] + -> [ fun ~atts ~st -> + let open Vernacinterp in + add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_clear_tac; st ] END -VERNAC COMMAND EXTEND DeriveInversion +VERNAC COMMAND FUNCTIONAL EXTEND DeriveInversion | [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ] => [ seff na ] - -> [ add_inversion_lemma_exn na c s false inv_tac ] + -> [ fun ~atts ~st -> + let open Vernacinterp in + add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_tac; st ] | [ "Derive" "Inversion" ident(na) "with" constr(c) ] => [ seff na ] - -> [ add_inversion_lemma_exn na c Sorts.InProp false inv_tac ] + -> [ fun ~atts ~st -> + let open Vernacinterp in + add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_tac; st ] END -VERNAC COMMAND EXTEND DeriveDependentInversion +VERNAC COMMAND FUNCTIONAL EXTEND DeriveDependentInversion | [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ] => [ seff na ] - -> [ add_inversion_lemma_exn na c s true dinv_tac ] + -> [ fun ~atts ~st -> + let open Vernacinterp in + add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_tac; st ] END -VERNAC COMMAND EXTEND DeriveDependentInversionClear +VERNAC COMMAND FUNCTIONAL EXTEND DeriveDependentInversionClear | [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ] => [ seff na ] - -> [ add_inversion_lemma_exn na c s true dinv_clear_tac ] + -> [ fun ~atts ~st -> + let open Vernacinterp in + add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_clear_tac; st ] END (**********************************************************************) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index a698b05dd..3cbb11001 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1981,8 +1981,7 @@ let add_morphism_infer glob m n = Decl_kinds.IsAssumption Decl_kinds.Logical) in add_instance (Typeclasses.new_instance - (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info glob - poly (ConstRef cst)); + (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info glob (ConstRef cst)); declare_projection n instance_id (ConstRef cst) else let kind = Decl_kinds.Global, poly, @@ -1993,7 +1992,7 @@ let add_morphism_infer glob m n = | Globnames.ConstRef cst -> add_instance (Typeclasses.new_instance (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info - glob poly (ConstRef cst)); + glob (ConstRef cst)); declare_projection n instance_id (ConstRef cst) | _ -> assert false in diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index bc9990d02..f153b6341 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -87,7 +87,6 @@ type instance = { (* Sections where the instance should be redeclared, None for discard, Some 0 for none. *) is_global: int option; - is_poly: bool; is_impl: global_reference; } @@ -97,7 +96,7 @@ let instance_impl is = is.is_impl let hint_priority is = is.is_info.Vernacexpr.hint_priority -let new_instance cl info glob poly impl = +let new_instance cl info glob impl = let global = if glob then Some (Lib.sections_depth ()) else None @@ -107,7 +106,6 @@ let new_instance cl info glob poly impl = { is_class = cl.cl_impl; is_info = info ; is_global = global ; - is_poly = poly; is_impl = impl } (* @@ -420,7 +418,7 @@ let declare_instance info local glob = match class_of_constr Evd.empty (EConstr.of_constr ty) with | Some (rels, ((tc,_), args) as _cl) -> assert (not (isVarRef glob) || local); - add_instance (new_instance tc info (not local) (Flags.use_polymorphic_flag ()) glob) + add_instance (new_instance tc info (not local) glob) | None -> () let add_class cl = diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 0cbe1c71c..ee28ec173 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -53,7 +53,7 @@ val all_instances : unit -> instance list val add_class : typeclass -> unit -val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool -> Decl_kinds.polymorphic -> +val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool -> global_reference -> instance val add_instance : instance -> unit val remove_instance : instance -> unit diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 01065868d..197b3030d 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -234,10 +234,9 @@ let inversion_scheme env sigma t sort dep_option inv_op = let p = Evarutil.nf_evars_universes sigma invProof in p, sigma -let add_inversion_lemma name env sigma t sort dep inv_op = +let add_inversion_lemma ~poly name env sigma t sort dep inv_op = let invProof, sigma = inversion_scheme env sigma t sort dep inv_op in let univs = - let poly = Flags.use_polymorphic_flag () in Evd.const_univ_entry ~poly sigma in let entry = definition_entry ~univs invProof in @@ -247,13 +246,13 @@ let add_inversion_lemma name env sigma t sort dep inv_op = (* inv_op = Inv (derives de complete inv. lemma) * inv_op = InvNoThining (derives de semi inversion lemma) *) -let add_inversion_lemma_exn na com comsort bool tac = +let add_inversion_lemma_exn ~poly na com comsort bool tac = let env = Global.env () in let sigma = Evd.from_env env in let sigma, c = Constrintern.interp_type_evars env sigma com in let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid env sigma comsort in try - add_inversion_lemma na env sigma c sort bool tac + add_inversion_lemma ~poly na env sigma c sort bool tac with | UserError (Some "Case analysis",s) -> (* Reference to Indrec *) user_err ~hdr:"Inv needs Nodep Prop Set" s diff --git a/tactics/leminv.mli b/tactics/leminv.mli index 8745ad397..f221b1fd9 100644 --- a/tactics/leminv.mli +++ b/tactics/leminv.mli @@ -14,6 +14,6 @@ open Misctypes val lemInv_clause : quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic -val add_inversion_lemma_exn : +val add_inversion_lemma_exn : poly:bool -> Id.t -> constr_expr -> Sorts.family -> bool -> (Id.t -> unit Proofview.tactic) -> unit diff --git a/vernac/classes.ml b/vernac/classes.ml index 6914f899b..4a2dba859 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -69,8 +69,7 @@ let existing_instance glob g info = let instance, _ = Global.type_of_global_in_context (Global.env ()) c in let _, r = Term.decompose_prod_assum instance in match class_of_constr Evd.empty (EConstr.of_constr r) with - | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob - (*FIXME*) (Flags.use_polymorphic_flag ()) c) + | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob c) | None -> user_err ?loc:(loc_of_reference g) ~hdr:"declare_instance" (Pp.str "Constant does not build instances of a declared type class.") @@ -393,8 +392,7 @@ let context poly l = let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in match class_of_constr sigma (of_constr t) with | Some (rels, ((tc,_), args) as _cl) -> - add_instance (Typeclasses.new_instance tc Hints.empty_hint_info false (*FIXME*) - poly (ConstRef cst)); + add_instance (Typeclasses.new_instance tc Hints.empty_hint_info false (ConstRef cst)); status (* declare_subclasses (ConstRef cst) cl *) | None -> status diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index aa6121c39..270e440e1 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2132,10 +2132,6 @@ let check_vernac_supports_polymorphism c p = | VernacExtend _ | VernacUniverse _ | VernacConstraint _) -> () | Some _, _ -> user_err Pp.(str "This command does not support Polymorphism") -let enforce_polymorphism = function - | None -> Flags.is_universe_polymorphism () - | Some b -> Flags.make_polymorphic_flag b; b - (** A global default timeout, controlled by option "Set Default Timeout n". Use "Unset Default Timeout" to deactivate it (or set it to 0). *) @@ -2202,6 +2198,7 @@ let with_fail st b f = end let interp ?(verbosely=true) ?proof ~st (loc,c) = + let orig_univ_poly = Flags.is_universe_polymorphism () in let orig_program_mode = Flags.is_program_mode () in let rec control = function | VernacExpr v -> @@ -2241,7 +2238,8 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = | c -> check_vernac_supports_locality c atts.locality; check_vernac_supports_polymorphism c polymorphism; - let polymorphic = enforce_polymorphism polymorphism in + let polymorphic = Option.default (Flags.is_universe_polymorphism ()) polymorphism in + Flags.make_universe_polymorphism polymorphic; Obligations.set_program_mode isprogcmd; try vernac_timeout begin fun () -> @@ -2249,9 +2247,12 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = if verbosely then Flags.verbosely (interp ?proof ~atts ~st) c else Flags.silently (interp ?proof ~atts ~st) c; + (* If the command is `(Un)Set Program Mode` or `(Un)Set Universe Polymorphism`, + we should not restore the previous state of the flag... *) if orig_program_mode || not !Flags.program_mode || isprogcmd then Flags.program_mode := orig_program_mode; - ignore (Flags.use_polymorphic_flag ()) + if (Flags.is_universe_polymorphism() = polymorphic) then + Flags.make_universe_polymorphism orig_univ_poly; end with | reraise when @@ -2262,8 +2263,8 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = let e = CErrors.push reraise in let e = locate_if_not_already ?loc e in let () = restore_timeout () in + Flags.make_universe_polymorphism orig_univ_poly; Flags.program_mode := orig_program_mode; - ignore (Flags.use_polymorphic_flag ()); iraise e in if verbosely -- cgit v1.2.3 From 1e1d8d67442dc3cdd248b7f5e027b9d6bf998ba3 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 27 Dec 2017 12:25:22 +0100 Subject: Add equations overlay. --- dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh diff --git a/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh b/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh new file mode 100644 index 000000000..c2e367038 --- /dev/null +++ b/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh @@ -0,0 +1,4 @@ +if [ "$CI_PULL_REQUEST" = "6405" ] || [ "$CI_BRANCH" = "rm-local-polymorphic-flag" ]; then + Equations_CI_BRANCH=rm-local-polymorphic-flag + Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations +fi -- cgit v1.2.3