diff options
| -rw-r--r-- | vernac/comFixpoint.ml | 4 | ||||
| -rw-r--r-- | vernac/declare.ml | 27 | ||||
| -rw-r--r-- | vernac/declare.mli | 17 | ||||
| -rw-r--r-- | vernac/recLemmas.ml | 21 | ||||
| -rw-r--r-- | vernac/recLemmas.mli | 13 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 37 |
6 files changed, 85 insertions, 34 deletions
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 99db8df803..304df6fe93 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -271,8 +271,8 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs let init_terms = Some fixdefs in let evd = Evd.from_ctx ctx in let lemma = - Declare.Proof.start_with_initialization ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl - evd (Some(cofix,indexes,init_terms)) thms None in + Declare.Proof.start_mutual_with_initialization ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl + evd ~mutual_info:(cofix,indexes,init_terms) thms None in (* Declare notations *) List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; lemma diff --git a/vernac/declare.ml b/vernac/declare.ml index 011e00eb2d..e9735eeb7d 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -92,6 +92,7 @@ module Info = struct ; udecl: UState.universe_decl (** Initial universe declarations *) ; thms : Recthm.t list + (** thms contains each individual constant info in a mutual decl *) ; compute_guard : lemma_possible_guards (** thms and compute guard are specific only to start_lemma_with_initialization + regular terminator *) @@ -216,10 +217,24 @@ let rec_tac_initializer finite guard thms snl = | (id,n,_)::l -> Tactics.mutual_fix id n l 0 | _ -> assert false -let start_proof_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recguard thms snl = +let start_proof_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma thm = let intro_tac { Recthm.args; _ } = Tactics.auto_intros_tac args in - let init_tac, compute_guard = match recguard with - | Some (finite,guard,init_terms) -> + let init_tac = intro_tac thm in + let { Recthm.name; typ; impargs; _} = thm in + let info = Info.make ?hook ~scope ~kind ~udecl () in + let info = { info with Info.thms = [] } in + (* start_lemma has the responsibility to add (name, impargs, typ) + to thms, once Info.t is more refined this won't be necessary *) + let lemma = start_proof ~name ~impargs ~poly ~info sigma (EConstr.of_constr typ) in + map_proof (fun p -> + pi1 @@ Proof.run_tactic Global.(env ()) init_tac p) lemma + +type mutual_info = (bool * lemma_possible_guards * Constr.t option list option) + +let start_mutual_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma ~mutual_info thms snl = + let intro_tac { Recthm.args; _ } = Tactics.auto_intros_tac args in + let init_tac, compute_guard = + let (finite,guard,init_terms) = mutual_info in let rec_tac = rec_tac_initializer finite guard thms snl in let term_tac = match init_terms with @@ -232,9 +247,7 @@ let start_proof_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua List.map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms in Tacticals.New.tclTHENS rec_tac term_tac, guard - | None -> - let () = match thms with [_] -> () | _ -> assert false in - intro_tac (List.hd thms), [] in + in match thms with | [] -> CErrors.anomaly (Pp.str "No proof to start.") | { Recthm.name; typ; impargs; _} :: thms -> @@ -2079,6 +2092,8 @@ module Proof = struct let start = start_proof let start_dependent = start_dependent_proof let start_with_initialization = start_proof_with_initialization + type nonrec mutual_info = mutual_info + let start_mutual_with_initialization = start_mutual_with_initialization let save = save_lemma_proved let save_admitted = save_lemma_admitted let by = by diff --git a/vernac/declare.mli b/vernac/declare.mli index 91950a264a..386635cb3f 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -213,7 +213,7 @@ module Proof : sig -> Proofview.telescope -> t - (** Pretty much internal, used by the Lemma / Fixpoint vernaculars *) + (** Pretty much internal, used by the Lemmavernaculars *) val start_with_initialization : ?hook:Hook.t -> poly:bool @@ -221,7 +221,20 @@ module Proof : sig -> kind:Decls.logical_kind -> udecl:UState.universe_decl -> Evd.evar_map - -> (bool * lemma_possible_guards * Constr.t option list option) option + -> Recthm.t + -> t + + type mutual_info = (bool * lemma_possible_guards * Constr.t option list option) + + (** Pretty much internal, used by mutual Lemma / Fixpoint vernaculars *) + val start_mutual_with_initialization + : ?hook:Hook.t + -> poly:bool + -> scope:Locality.locality + -> kind:Decls.logical_kind + -> udecl:UState.universe_decl + -> Evd.evar_map + -> mutual_info:mutual_info -> Recthm.t list -> int list option -> t diff --git a/vernac/recLemmas.ml b/vernac/recLemmas.ml index eb0e1fb795..797eaa7202 100644 --- a/vernac/recLemmas.ml +++ b/vernac/recLemmas.ml @@ -16,9 +16,9 @@ module RelDecl = Context.Rel.Declaration let find_mutually_recursive_statements sigma thms = let n = List.length thms in - let inds = List.map (fun (id,(t,impls)) -> + let inds = List.map (fun (id,t,args,impls) -> let (hyps,ccl) = EConstr.decompose_prod_assum sigma t in - let x = (id,(t,impls)) in + let x = (id,t,args,impls) in let whnf_hyp_hds = EConstr.map_rel_context_in_env (fun env c -> fst (Reductionops.whd_all_stack env sigma c)) (Global.env()) hyps in @@ -89,14 +89,23 @@ let find_mutually_recursive_statements sigma thms = in (finite,guard,None), ordered_inds -let look_for_possibly_mutual_statements sigma = function - | [id,(t,impls)] -> +type mutual_info = + | NonMutual of Names.Id.t * EConstr.t * Names.Name.t list * Impargs.manual_implicits + | Mutual of + { mutual_info : bool * int list list * Constr.t option list option + ; thms : (Names.Id.t * EConstr.t * Names.Name.t list * Impargs.manual_implicits) list + ; possible_guards : int list + } + +let look_for_possibly_mutual_statements sigma thms : mutual_info = + match thms with + | [id,t,args,impls] -> (* One non recursively proved theorem *) - None,[id,(t,impls)],None + NonMutual (id,t,args,impls) | _::_ as thms -> (* More than one statement and/or an explicit decreasing mark: *) (* we look for a common inductive hyp or a common coinductive conclusion *) let recguard,ordered_inds = find_mutually_recursive_statements sigma thms in let thms = List.map pi2 ordered_inds in - Some recguard,thms, Some (List.map (fun (_,_,i) -> succ i) ordered_inds) + Mutual { mutual_info = recguard; thms; possible_guards = List.map (fun (_,_,i) -> succ i) ordered_inds } | [] -> CErrors.anomaly (Pp.str "Empty list of theorems.") diff --git a/vernac/recLemmas.mli b/vernac/recLemmas.mli index 1a697c1e88..0d297ca9b9 100644 --- a/vernac/recLemmas.mli +++ b/vernac/recLemmas.mli @@ -8,8 +8,15 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +type mutual_info = + | NonMutual of Names.Id.t * EConstr.t * Names.Name.t list * Impargs.manual_implicits + | Mutual of + { mutual_info : bool * int list list * Constr.t option list option + ; thms : (Names.Id.t * EConstr.t * Names.Name.t list * Impargs.manual_implicits) list + ; possible_guards : int list + } + val look_for_possibly_mutual_statements : Evd.evar_map - -> ('a * (EConstr.t * 'b)) list - -> (bool * int list list * 'c option) option * - ('a * (EConstr.t * 'b)) list * int list option + -> (Names.Id.t * EConstr.t * Names.Name.t list * Impargs.manual_implicits) list + -> mutual_info diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 89294fee8c..650fc00e88 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -490,6 +490,16 @@ let program_inference_hook env sigma ev = user_err Pp.(str "The statement obligations could not be resolved \ automatically, write a statement definition first.") +(* Checks for start_lemma_com *) +let post_check_evd ~udecl ~poly evd = + let () = + let open UState in + if not (udecl.univdecl_extensible_instance && udecl.univdecl_extensible_constraints) then + ignore (Evd.check_univ_decl ~poly evd udecl) in + if poly then evd + else (* We fix the variables to ensure they won't be lowered to Set *) + Evd.fix_undefined_variables evd + let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms = let env0 = Global.env () in let flags = Pretyping.{ all_no_fail_flags with program_mode } in @@ -505,23 +515,20 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms = let evd = Pretyping.solve_remaining_evars ?hook:inference_hook flags env evd in let ids = List.map Context.Rel.Declaration.get_name ctx in check_name_freshness scope id; - evd, (id.CAst.v, (EConstr.it_mkProd_or_LetIn t' ctx, (ids, imps @ imps')))) + evd, (id.CAst.v, EConstr.it_mkProd_or_LetIn t' ctx, ids, imps @ imps')) evd thms in - let recguard,thms,snl = RecLemmas.look_for_possibly_mutual_statements evd thms in + let mut_analysis = RecLemmas.look_for_possibly_mutual_statements evd thms in let evd = Evd.minimize_universes evd in - let thms = List.map (fun (name, (typ, (args, impargs))) -> - { Declare.Recthm.name; typ = EConstr.to_constr evd typ; args; impargs} ) thms in - let () = - let open UState in - if not (udecl.univdecl_extensible_instance && udecl.univdecl_extensible_constraints) then - ignore (Evd.check_univ_decl ~poly evd udecl) - in - let evd = - if poly then evd - else (* We fix the variables to ensure they won't be lowered to Set *) - Evd.fix_undefined_variables evd - in - Declare.Proof.start_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl + match mut_analysis with + | RecLemmas.NonMutual (name, typ, args, impargs) -> + let thm = { Declare.Recthm.name; typ = EConstr.to_constr evd typ; args; impargs } in + let evd = post_check_evd ~udecl ~poly evd in + Declare.Proof.start_with_initialization ?hook ~poly ~scope ~kind evd ~udecl thm + | RecLemmas.Mutual { mutual_info; thms ; possible_guards } -> + let thms = List.map (fun (name, typ, args, impargs) -> + { Declare.Recthm.name; typ = EConstr.to_constr evd typ; args; impargs} ) thms in + let evd = post_check_evd ~udecl ~poly evd in + Declare.Proof.start_mutual_with_initialization ?hook ~poly ~scope ~kind evd ~udecl ~mutual_info thms (Some possible_guards) let vernac_definition_hook ~canonical_instance ~local ~poly = let open Decls in function | Coercion -> |