From 75e7c5b596d2a3e9b54e84788a15299568792584 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 11 Jun 2019 02:16:51 +0200 Subject: [equations] [proof] Remove duplicate shrink function. Equation's terminator had exactly duplicated the shrink function used in `Abstract`, we remove this duplicity. --- tactics/abstract.mli | 8 +++++ vernac/declareObl.ml | 1 + vernac/lemmas.ml | 99 +++++++++++++--------------------------------------- 3 files changed, 33 insertions(+), 75 deletions(-) diff --git a/tactics/abstract.mli b/tactics/abstract.mli index 9d4f3cfb27..0c74e898d2 100644 --- a/tactics/abstract.mli +++ b/tactics/abstract.mli @@ -20,3 +20,11 @@ val cache_term_by_tactic_then -> unit Proofview.tactic val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic + +(* Internal but used in a few places; should likely be made intro a + proper library function, or incorporated into the generic constant + save path *) +val shrink_entry + : ('a, 'b) Context.Named.Declaration.pt list + -> 'c Entries.definition_entry + -> 'c Entries.definition_entry * Constr.t list diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index 71215d2a3e..30aa347692 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -95,6 +95,7 @@ let decompose_lam_prod c ty = in aux Context.Rel.empty c ty +(* XXX: What's the relation of this with Abstract.shrink ? *) let shrink_body c ty = let ctx, b, ty = match ty with diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 091ff32009..a1345f444b 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -581,81 +581,30 @@ let finish_derived ~f ~name ~idopt ~opaque ~entries = in ignore (Declare.declare_constant name lemma_def) -(* XXX several versions of shrink do appear in abstract, declareobl and here *) -module Equations = struct - let rec decompose len c t accu = - let open Constr in - let open Context.Rel.Declaration in - if len = 0 then (c, t, accu) - else match kind c, kind t with - | Lambda (na, u, c), Prod (_, _, t) -> - decompose (pred len) c t (LocalAssum (na, u) :: accu) - | LetIn (na, b, u, c), LetIn (_, _, _, t) -> - decompose (pred len) c t (LocalDef (na, b, u) :: accu) - | _ -> assert false - - let rec shrink ctx sign c t accu = - let open Constr in - let open Vars in - match ctx, sign with - | [], [] -> (c, t, accu) - | p :: ctx, decl :: sign -> - if noccurn 1 c && noccurn 1 t then - let c = subst1 mkProp c in - let t = subst1 mkProp t in - shrink ctx sign c t accu - else - let c = Term.mkLambda_or_LetIn p c in - let t = Term.mkProd_or_LetIn p t in - let accu = if RelDecl.is_local_assum p - then mkVar (NamedDecl.get_id decl) :: accu - else accu - in - shrink ctx sign c t accu - | _ -> assert false +let finish_proved_equations opaque lid proof_obj hook i types wits sigma = - let shrink_entry sign const = - let open Entries in - let typ = match const.const_entry_type with - | None -> assert false - | Some t -> t - in - (* The body has been forced by the call to [build_constant_by_tactic] *) - (* let () = assert (Future.is_over const.const_entry_body) in *) - let ((body, uctx), eff) = Future.force const.const_entry_body in - let (body, typ, ctx) = decompose (List.length sign) body typ [] in - let (body, typ, args) = shrink ctx sign body typ [] in - let const = { const with - const_entry_body = Future.from_val ((body, uctx), eff); - const_entry_type = Some typ; - } in - (const, args) - - let finish_proved opaque lid proof_obj hook i types wits sigma = - - let open Decl_kinds in - let obls = ref 1 in - let kind = match pi3 proof_obj.Proof_global.persistence with - | DefinitionBody d -> IsDefinition d - | Proof p -> IsProof p - in - let evd = ref sigma in - let recobls = - CList.map2 (fun (wit, (evar_env, ev, evi, local_context, type_)) entry -> - let id = - match Evd.evar_ident ev sigma with - | Some id -> id - | None -> let n = !obls in incr obls; add_suffix i ("_obligation_" ^ string_of_int n) - in - let entry, args = shrink_entry local_context entry in - let cst = Declare.declare_constant id (Entries.DefinitionEntry entry, kind) in - let sigma, app = Evarutil.new_global !evd (ConstRef cst) in - evd := Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma; - cst) - (CList.combine (List.rev !wits) types) proof_obj.Proof_global.entries - in - hook recobls !evd -end + let open Decl_kinds in + let obls = ref 1 in + let kind = match pi3 proof_obj.Proof_global.persistence with + | DefinitionBody d -> IsDefinition d + | Proof p -> IsProof p + in + let evd = ref sigma in + let recobls = + CList.map2 (fun (wit, (evar_env, ev, evi, local_context, type_)) entry -> + let id = + match Evd.evar_ident ev sigma with + | Some id -> id + | None -> let n = !obls in incr obls; add_suffix i ("_obligation_" ^ string_of_int n) + in + let entry, args = Abstract.shrink_entry local_context entry in + let cst = Declare.declare_constant id (Entries.DefinitionEntry entry, kind) in + let sigma, app = Evarutil.new_global !evd (ConstRef cst) in + evd := Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma; + cst) + (CList.combine (List.rev !wits) types) proof_obj.Proof_global.entries + in + hook recobls !evd let save_lemma_proved ?proof ?lemma ~opaque ~idopt = (* Invariant (uh) *) @@ -682,4 +631,4 @@ let save_lemma_proved ?proof ?lemma ~opaque ~idopt = | End_derive { f ; name } -> finish_derived ~f ~name ~idopt ~opaque ~entries:proof_obj.entries | End_equations { hook; i; types; wits; sigma } -> - Equations.finish_proved opaque idopt proof_obj hook i types wits sigma + finish_proved_equations opaque idopt proof_obj hook i types wits sigma -- cgit v1.2.3