diff options
Diffstat (limited to 'tactics')
40 files changed, 1448 insertions, 1561 deletions
diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 03ab0a1c13..1e18028e7b 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -8,14 +8,11 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -module CVars = Vars - open Util open Termops open EConstr open Evarutil -module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration (* tactical to save as name a subproof such that the generalisation of @@ -23,67 +20,21 @@ module NamedDecl = Context.Named.Declaration is solved by tac *) (** d1 is the section variable in the global context, d2 in the goal context *) -let interpretable_as_section_decl env evd d1 d2 = +let interpretable_as_section_decl env sigma d1 d2 = let open Context.Named.Declaration in - let e_eq_constr_univs sigma c1 c2 = match eq_constr_universes env !sigma c1 c2 with - | None -> false - | Some cstr -> - try ignore (Evd.add_universe_constraints !sigma cstr); true - with UState.UniversesDiffer -> false + let e_eq_constr_univs sigma c1 c2 = match eq_constr_universes env sigma c1 c2 with + | None -> false + | Some cstr -> + try + let _sigma = Evd.add_universe_constraints sigma cstr in + true + with UState.UniversesDiffer -> false in match d2, d1 with | LocalDef _, LocalAssum _ -> false | LocalDef (_,b1,t1), LocalDef (_,b2,t2) -> - e_eq_constr_univs evd b1 b2 && e_eq_constr_univs evd t1 t2 - | LocalAssum (_,t1), d2 -> e_eq_constr_univs evd t1 (NamedDecl.get_type d2) - -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 CVars 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 shrink_entry sign const = - let open Declare in - let typ = match const.proof_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.proof_entry_body) in - let ((body, uctx), eff) = Future.force const.proof_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 - proof_entry_body = Future.from_val ((body, uctx), eff); - proof_entry_type = Some typ; - } in - (const, args) + e_eq_constr_univs sigma b1 b2 && e_eq_constr_univs sigma t1 t2 + | LocalAssum (_,t1), d2 -> e_eq_constr_univs sigma t1 (NamedDecl.get_type d2) let name_op_to_name ~name_op ~name suffix = match name_op with @@ -101,22 +52,22 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = redundancy on constant declaration. This opens up an interesting question, how does abstract behave when discharge is local for example? *) - let suffix = if opaque - then "_subproof" - else "_subterm" in + let suffix, kind = if opaque + then "_subproof", Decls.(IsProof Lemma) + else "_subterm", Decls.(IsDefinition Definition) + in let name = name_op_to_name ~name_op ~name suffix in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let current_sign = Global.named_context_val () and global_sign = Proofview.Goal.hyps gl in - let evdref = ref sigma in let sign,secsign = List.fold_right (fun d (s1,s2) -> let id = NamedDecl.get_id d in if mem_named_context_val id current_sign && - interpretable_as_section_decl env evdref (lookup_named_val id current_sign) d + interpretable_as_section_decl env sigma (lookup_named_val id current_sign) d then (s1,push_named_context_val d s2) else (Context.Named.add d s1,s2)) global_sign (Context.Named.empty, Environ.empty_named_context_val) in @@ -126,21 +77,21 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = | Some ty -> ty in let concl = it_mkNamedProd_or_LetIn concl sign in let concl = - try flush_and_check_evars !evdref concl + try flush_and_check_evars sigma concl with Uninstantiated_evar _ -> CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials.") in - let evd, ctx, concl = + let sigma, ctx, concl = (* FIXME: should be done only if the tactic succeeds *) - let evd = Evd.minimize_universes !evdref in - let ctx = Evd.universe_context_set evd in - evd, ctx, Evarutil.nf_evars_universes evd concl + let sigma = Evd.minimize_universes sigma in + let ctx = Evd.universe_context_set sigma in + sigma, ctx, Evarutil.nf_evars_universes sigma concl in let concl = EConstr.of_constr concl in let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in - let ectx = Evd.evar_universe_context evd in + let ectx = Evd.evar_universe_context sigma in let (const, safe, ectx) = - try Pfedit.build_constant_by_tactic ~poly ~name ectx secsign concl solve_tac + try Pfedit.build_constant_by_tactic ~name ~opaque:Proof_global.Transparent ~poly ectx secsign concl solve_tac with Logic_monad.TacticFailure e as src -> (* if the tactic [tac] fails, it reports a [TacticFailure e], which is an error irrelevant to the proof system (in fact it @@ -151,16 +102,20 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = in let body, effs = Future.force const.Declare.proof_entry_body in (* We drop the side-effects from the entry, they already exist in the ambient environment *) - let const = { const with Declare.proof_entry_body = Future.from_val (body, ()) } in - let const, args = shrink_entry sign const in + let const = Declare.Internal.map_entry_body const ~f:(fun _ -> body, ()) in + (* EJGA: Hack related to the above call to + `build_constant_by_tactic` with `~opaque:Transparent`. Even if + the abstracted term is destined to be opaque, if we trigger the + `if poly && opaque && private_poly_univs ()` in `Proof_global` + kernel will boom. This deserves more investigation. *) + let const = Declare.Internal.set_opacity ~opaque const in + let const, args = Declare.Internal.shrink_entry sign const in let args = List.map EConstr.of_constr args in - let cd = { const with Declare.proof_entry_opaque = opaque } in - let kind = if opaque then Decls.(IsProof Lemma) else Decls.(IsDefinition Definition) in let cst () = (* do not compute the implicit arguments, it may be costly *) let () = Impargs.make_implicit_args false in (* ppedrot: seems legit to have abstracted subproofs as local*) - Declare.declare_private_constant ~local:Declare.ImportNeedQualified ~name ~kind cd + Declare.declare_private_constant ~local:Declare.ImportNeedQualified ~name ~kind const in let cst, eff = Impargs.with_implicit_protection cst () in let inst = match const.Declare.proof_entry_universes with @@ -174,14 +129,14 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = EInstance.make (Univ.UContext.instance ctx) in let lem = mkConstU (cst, inst) in - let evd = Evd.set_universe_context evd ectx in + let sigma = Evd.set_universe_context sigma ectx in let effs = Evd.concat_side_effects eff effs in let solve = Proofview.tclEFFECTS effs <*> tacK lem args in let tac = if not safe then Proofview.mark_as_unsafe <*> solve else solve in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) tac + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) tac end let abstract_subproof ~opaque tac = diff --git a/tactics/abstract.mli b/tactics/abstract.mli index 96ddbea7b2..779e46cd49 100644 --- a/tactics/abstract.mli +++ b/tactics/abstract.mli @@ -20,11 +20,3 @@ 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 Declare.proof_entry - -> 'c Declare.proof_entry * Constr.t list diff --git a/tactics/auto.ml b/tactics/auto.ml index 0b465418f2..9c1a975330 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -135,9 +135,9 @@ let conclPattern concl pat tac = match pat with | None -> Proofview.tclUNIT Id.Map.empty | Some pat -> - try - Proofview.tclUNIT (Constr_matching.matches env sigma pat concl) - with Constr_matching.PatternMatchingFailure -> + try + Proofview.tclUNIT (Constr_matching.matches env sigma pat concl) + with Constr_matching.PatternMatchingFailure -> Tacticals.New.tclZEROMSG (str "pattern-matching failed") in Proofview.Goal.enter begin fun gl -> @@ -323,9 +323,9 @@ let rec trivial_fail_db dbg mod_delta db_list local_db = let nf c = Evarutil.nf_evar sigma c in let decl = Tacmach.New.pf_last_hyp gl in let hyp = Context.Named.Declaration.map_constr nf decl in - let hintl = make_resolve_hyp env sigma hyp - in trivial_fail_db dbg mod_delta db_list - (Hint_db.add_list env sigma hintl local_db) + let hintl = make_resolve_hyp env sigma hyp + in trivial_fail_db dbg mod_delta db_list + (Hint_db.add_list env sigma hintl local_db) end) in Proofview.Goal.enter begin fun gl -> @@ -350,31 +350,31 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl = let f = hintmap_of sigma secvars hdc concl in if occur_existential sigma concl then List.map_append - (fun db -> - if Hint_db.use_dn db then - let flags = flags_of_state (Hint_db.transparent_state db) in - List.map (fun x -> (Some flags,x)) (f db) - else - let flags = auto_flags_of_state (Hint_db.transparent_state db) in - List.map (fun x -> (Some flags,x)) (f db)) - (local_db::db_list) + (fun db -> + if Hint_db.use_dn db then + let flags = flags_of_state (Hint_db.transparent_state db) in + List.map (fun x -> (Some flags,x)) (f db) + else + let flags = auto_flags_of_state (Hint_db.transparent_state db) in + List.map (fun x -> (Some flags,x)) (f db)) + (local_db::db_list) else List.map_append (fun db -> - if Hint_db.use_dn db then - let flags = flags_of_state (Hint_db.transparent_state db) in - List.map (fun x -> (Some flags, x)) (f db) - else + if Hint_db.use_dn db then + let flags = flags_of_state (Hint_db.transparent_state db) in + List.map (fun x -> (Some flags, x)) (f db) + else let st = Hint_db.transparent_state db in - let flags, l = - let l = - match hdc with None -> Hint_db.map_none ~secvars db - | Some hdc -> + let flags, l = + let l = + match hdc with None -> Hint_db.map_none ~secvars db + | Some hdc -> if TransparentState.is_empty st - then Hint_db.map_auto sigma ~secvars hdc concl db - else Hint_db.map_existential sigma ~secvars hdc concl db - in auto_flags_of_state st, l - in List.map (fun x -> (Some flags,x)) l) - (local_db::db_list) + then Hint_db.map_auto sigma ~secvars hdc concl db + else Hint_db.map_existential sigma ~secvars hdc concl db + in auto_flags_of_state st, l + in List.map (fun x -> (Some flags,x)) l) + (local_db::db_list) and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=dbname})) = let tactic = function @@ -384,13 +384,13 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db= | Res_pf_THEN_trivial_fail (c,cl) -> Tacticals.New.tclTHEN (unify_resolve_gen ~poly flags (c,cl)) - (* With "(debug) trivial", we shouldn't end here, and - with "debug auto" we don't display the details of inner trivial *) + (* With "(debug) trivial", we shouldn't end here, and + with "debug auto" we don't display the details of inner trivial *) (trivial_fail_db (no_dbg dbg) (not (Option.is_empty flags)) db_list local_db) | Unfold_nth c -> Proofview.Goal.enter begin fun gl -> if exists_evaluable_reference (Tacmach.New.pf_env gl) c then - Tacticals.New.tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl) + Tacticals.New.tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl) else Tacticals.New.tclFAIL 0 (str"Unbound reference") end | Extern tacast -> @@ -409,12 +409,12 @@ and trivial_resolve sigma dbg mod_delta db_list local_db secvars cl = try let head = try let hdconstr = decompose_app_bound sigma cl in - Some hdconstr + Some hdconstr with Bound -> None in List.map (tac_of_hint dbg db_list local_db cl) - (priority - (my_find_search mod_delta sigma db_list local_db secvars head cl)) + (priority + (my_find_search mod_delta sigma db_list local_db secvars head cl)) with Not_found -> [] (** The use of the "core" database can be de-activated by passing @@ -458,11 +458,11 @@ let possible_resolve sigma dbg mod_delta db_list local_db secvars cl = try let head = try let hdconstr = decompose_app_bound sigma cl in - Some hdconstr + Some hdconstr with Bound -> None in List.map (tac_of_hint dbg db_list local_db cl) - (my_find_search mod_delta sigma db_list local_db secvars head cl) + (my_find_search mod_delta sigma db_list local_db secvars head cl) with Not_found -> [] let extend_local_db decl db gl = @@ -490,16 +490,16 @@ let search d n mod_delta db_list local_db = Proofview.tclEXTEND [] begin if Int.equal n 0 then Tacticals.New.tclZEROMSG (str"BOUND 2") else Tacticals.New.tclORELSE0 (dbg_assumption d) - (Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db) - ( Proofview.Goal.enter begin fun gl -> + (Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db) + ( Proofview.Goal.enter begin fun gl -> let concl = Tacmach.New.pf_concl gl in let sigma = Tacmach.New.project gl in let secvars = compute_secvars gl in - let d' = incr_dbg d in - Tacticals.New.tclFIRST - (List.map - (fun ntac -> Tacticals.New.tclTHEN ntac (search d' (n-1) local_db)) - (possible_resolve sigma d mod_delta db_list local_db secvars concl)) + let d' = incr_dbg d in + Tacticals.New.tclFIRST + (List.map + (fun ntac -> Tacticals.New.tclTHEN ntac (search d' (n-1) local_db)) + (possible_resolve sigma d mod_delta db_list local_db secvars concl)) end)) end [] in @@ -519,7 +519,7 @@ let delta_auto debug mod_delta n lems dbnames = (search d n mod_delta db_list hints) end -let delta_auto = +let delta_auto = if Flags.profile then let key = CProfile.declare_profile "delta_auto" in CProfile.profile5 key delta_auto diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 0bc410010c..cd6f445503 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -20,11 +20,11 @@ open Locus (* Rewriting rules *) type rew_rule = { rew_lemma: constr; - rew_type: types; - rew_pat: constr; - rew_ctx: Univ.ContextSet.t; - rew_l2r: bool; - rew_tac: Genarg.glob_generic_argument option } + rew_type: types; + rew_pat: constr; + rew_ctx: Univ.ContextSet.t; + rew_l2r: bool; + rew_tac: Genarg.glob_generic_argument option } let subst_hint subst hint = let cst' = subst_mps subst hint.rew_lemma in @@ -33,8 +33,8 @@ let subst_hint subst hint = let t' = Option.Smart.map (Genintern.generic_substitute subst) hint.rew_tac in if hint.rew_lemma == cst' && hint.rew_type == typ' && hint.rew_tac == t' then hint else { hint with - rew_lemma = cst'; rew_type = typ'; - rew_pat = pat'; rew_tac = t' } + rew_lemma = cst'; rew_type = typ'; + rew_pat = pat'; rew_tac = t' } module HintIdent = struct @@ -79,13 +79,13 @@ let print_rewrite_hintdb bas = let env = Global.env () in let sigma = Evd.from_env env in (str "Database " ++ str bas ++ fnl () ++ - prlist_with_sep fnl - (fun h -> - str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++ + prlist_with_sep fnl + (fun h -> + str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++ Printer.pr_lconstr_env env sigma h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr_env env sigma h.rew_type ++ - Option.cata (fun tac -> str " then use tactic " ++ + Option.cata (fun tac -> str " then use tactic " ++ Pputils.pr_glb_generic env sigma tac) (mt ()) h.rew_tac) - (find_rewrites bas)) + (find_rewrites bas)) type raw_rew_rule = (constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option) CAst.t @@ -116,7 +116,7 @@ let one_base general_rewrite_maybe_in tac_main bas = Tacticals.New.tclREPEAT_MAIN (Proofview.tclPROGRESS (List.fold_left (fun tac (ctx,csr,dir,tc) -> Tacticals.New.tclTHEN tac (Tacticals.New.tclREPEAT_MAIN - (Tacticals.New.tclTHENFIRST (try_rewrite dir ctx csr tc) tac_main))) + (Tacticals.New.tclTHENFIRST (try_rewrite dir ctx csr tc) tac_main))) (Proofview.tclUNIT()) lrul)) (* The AutoRewrite tactic *) @@ -125,9 +125,9 @@ let autorewrite ?(conds=Naive) tac_main lbas = (List.fold_left (fun tac bas -> Tacticals.New.tclTHEN tac (one_base (fun dir c tac -> - let tac = (tac, conds) in - general_rewrite dir AllOccurrences true false ~tac (EConstr.of_constr c)) - tac_main bas)) + let tac = (tac, conds) in + general_rewrite dir AllOccurrences true false ~tac (EConstr.of_constr c)) + tac_main bas)) (Proofview.tclUNIT()) lbas)) let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas = @@ -158,19 +158,19 @@ let gen_auto_multi_rewrite conds tac_main lbas cl = else let compose_tac t1 t2 = match cl.onhyps with - | Some [] -> t1 - | _ -> Tacticals.New.tclTHENFIRST t1 t2 + | Some [] -> t1 + | _ -> Tacticals.New.tclTHENFIRST t1 t2 in compose_tac - (if cl.concl_occs != NoOccurrences then autorewrite ~conds tac_main lbas else Proofview.tclUNIT ()) - (match cl.onhyps with - | Some l -> try_do_hyps (fun ((_,id),_) -> id) l - | None -> - (* try to rewrite in all hypothesis - (except maybe the rewritten one) *) + (if cl.concl_occs != NoOccurrences then autorewrite ~conds tac_main lbas else Proofview.tclUNIT ()) + (match cl.onhyps with + | Some l -> try_do_hyps (fun ((_,id),_) -> id) l + | None -> + (* try to rewrite in all hypothesis + (except maybe the rewritten one) *) Proofview.Goal.enter begin fun gl -> let ids = Tacmach.New.pf_ids_of_hyps gl in - try_do_hyps (fun id -> id) ids + try_do_hyps (fun id -> id) ids end) let auto_multi_rewrite ?(conds=Naive) lems cl = @@ -180,10 +180,10 @@ let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl = let onconcl = match cl.Locus.concl_occs with NoOccurrences -> false | _ -> true in match onconcl,cl.Locus.onhyps with | false,Some [_] | true,Some [] | false,Some [] -> - (* autorewrite with .... in clause using tac n'est sur que - si clause represente soit le but soit UNE hypothese - *) - Proofview.V82.wrap_exceptions (fun () -> gen_auto_multi_rewrite conds tac_main lbas cl) + (* autorewrite with .... in clause using tac n'est sur que + si clause represente soit le but soit UNE hypothese + *) + Proofview.V82.wrap_exceptions (fun () -> gen_auto_multi_rewrite conds tac_main lbas cl) | _ -> Tacticals.New.tclZEROMSG (strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion.") @@ -233,7 +233,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = let rec split_last_two = function | [c1;c2] -> [],(c1, c2) | x::y::z -> - let l,res = split_last_two (y::z) in x::l, res + let l,res = split_last_two (y::z) in x::l, res | _ -> raise Not_found in try @@ -255,19 +255,19 @@ let decompose_applied_relation metas env sigma c ctype left2right = match find_rel ctype with | Some c -> Some c | None -> - let ctx,t' = Reductionops.splay_prod_assum env sigma ctype in (* Search for underlying eq *) - match find_rel (it_mkProd_or_LetIn t' ctx) with - | Some c -> Some c - | None -> None + let ctx,t' = Reductionops.splay_prod_assum env sigma ctype in (* Search for underlying eq *) + match find_rel (it_mkProd_or_LetIn t' ctx) with + | Some c -> Some c + | None -> None let find_applied_relation ?loc metas env sigma c left2right = let ctype = Typing.unsafe_type_of env sigma (EConstr.of_constr c) in match decompose_applied_relation metas env sigma c ctype left2right with | Some c -> c | None -> - user_err ?loc ~hdr:"decompose_applied_relation" - (str"The type" ++ spc () ++ Printer.pr_econstr_env env sigma ctype ++ - spc () ++ str"of this term does not end with an applied relation.") + user_err ?loc ~hdr:"decompose_applied_relation" + (str"The type" ++ spc () ++ Printer.pr_econstr_env env sigma ctype ++ + spc () ++ str"of this term does not end with an applied relation.") (* To add rewriting rules to a base *) let add_rew_rules base lrul = @@ -279,13 +279,13 @@ let add_rew_rules base lrul = let lrul = List.fold_left (fun dn {CAst.loc;v=((c,ctx),b,t)} -> - let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in - let info = find_applied_relation ?loc false env sigma c b in - let pat = if b then info.hyp_left else info.hyp_right in - let rul = { rew_lemma = c; rew_type = info.hyp_ty; - rew_pat = pat; rew_ctx = ctx; rew_l2r = b; - rew_tac = Option.map intern t} - in incr counter; - HintDN.add pat (!counter, rul) dn) HintDN.empty lrul + let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in + let info = find_applied_relation ?loc false env sigma c b in + let pat = if b then info.hyp_left else info.hyp_right in + let rul = { rew_lemma = c; rew_type = info.hyp_ty; + rew_pat = pat; rew_ctx = ctx; rew_l2r = b; + rew_tac = Option.map intern t} + in incr counter; + HintDN.add pat (!counter, rul) dn) HintDN.empty lrul in Lib.add_anonymous_leaf (inHintRewrite (base,lrul)) diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index e5125ffe50..6df2ea9b12 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -28,11 +28,11 @@ val autorewrite_in : ?conds:conditions -> Names.Id.t -> unit Proofview.tactic -> (** Rewriting rules *) type rew_rule = { rew_lemma: constr; - rew_type: types; - rew_pat: constr; - rew_ctx: Univ.ContextSet.t; - rew_l2r: bool; - rew_tac: Genarg.glob_generic_argument option } + rew_type: types; + rew_pat: constr; + rew_ctx: Univ.ContextSet.t; + rew_l2r: bool; + rew_tac: Genarg.glob_generic_argument option } val find_rewrites : string -> rew_rule list diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index d0816b266f..ae3aea5788 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -80,8 +80,8 @@ let constr_val_discr_st sigma ts t = | Var id when not (TransparentState.is_transparent_variable ts id) -> Label(GRLabel (VarRef id),l) | Prod (n, d, c) -> Label(ProdLabel, [d; c]) | Lambda (n, d, c) -> - if List.is_empty l then - Label(LambdaLabel, [d; c] @ l) + if List.is_empty l then + Label(LambdaLabel, [d; c] @ l) else Everything | Sort _ -> Label(SortLabel, []) | Evar _ -> Everything @@ -154,27 +154,27 @@ struct let add = function | None -> - (fun dn (c,v) -> - Dn.add dn bounded_constr_pat_discr ((c,!dnet_depth),v)) + (fun dn (c,v) -> + Dn.add dn bounded_constr_pat_discr ((c,!dnet_depth),v)) | Some st -> - (fun dn (c,v) -> - Dn.add dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v)) + (fun dn (c,v) -> + Dn.add dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v)) let rmv = function | None -> - (fun dn (c,v) -> - Dn.rmv dn bounded_constr_pat_discr ((c,!dnet_depth),v)) + (fun dn (c,v) -> + Dn.rmv dn bounded_constr_pat_discr ((c,!dnet_depth),v)) | Some st -> - (fun dn (c,v) -> - Dn.rmv dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v)) + (fun dn (c,v) -> + Dn.rmv dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v)) let lookup sigma = function | None -> - (fun dn t -> - Dn.lookup dn (bounded_constr_val_discr sigma) (t,!dnet_depth)) + (fun dn t -> + Dn.lookup dn (bounded_constr_val_discr sigma) (t,!dnet_depth)) | Some st -> - (fun dn t -> - Dn.lookup dn (bounded_constr_val_discr_st sigma st) (t,!dnet_depth)) + (fun dn t -> + Dn.lookup dn (bounded_constr_val_discr_st sigma st) (t,!dnet_depth)) let app f dn = Dn.app f dn diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index cf5c64c3ae..f8cb8870ea 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -457,7 +457,7 @@ let catchable = function | Refiner.FailError _ -> true | e -> Logic.catchable_exception e -let pr_depth l = +let pr_depth l = let rec fmt elts = match elts with | [] -> [] @@ -758,8 +758,8 @@ module Search = struct Feedback.msg_debug (str"Adding shelved subgoals to the search: " ++ prlist_with_sep spc (pr_ev sigma) goals ++ - str" while shelving " ++ - prlist_with_sep spc (pr_ev sigma) shelved); + str" while shelving " ++ + prlist_with_sep spc (pr_ev sigma) shelved); shelve_goals shelved <*> (if List.is_empty goals then tclUNIT () else @@ -776,7 +776,7 @@ module Search = struct (with_shelf tac >>= fun s -> let i = !idx in incr idx; result s i None) (fun e' -> - if CErrors.noncritical (fst e') then + if CErrors.noncritical (fst e') then (pr_error e'; aux (merge_exceptions e e') tl) else iraise e') and aux e = function diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 56e8e7a11f..1f5a6380fd 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -66,10 +66,10 @@ let contradiction_context = | d :: rest -> let id = NamedDecl.get_id d in let typ = nf_evar sigma (NamedDecl.get_type d) in - let typ = whd_all env sigma typ in + let typ = whd_all env sigma typ in if is_empty_type env sigma typ then - simplest_elim (mkVar id) - else match EConstr.kind sigma typ with + simplest_elim (mkVar id) + else match EConstr.kind sigma typ with | Prod (na,t,u) when is_empty_type env sigma u -> let is_unit_or_eq = match_with_unit_or_eq_type env sigma t in Tacticals.New.tclORELSE @@ -84,17 +84,17 @@ let contradiction_context = simplest_elim (mkApp (mkVar id,[|p|])) | None -> Tacticals.New.tclZEROMSG (Pp.str"Not a negated unit type.")) - (Proofview.tclORELSE + (Proofview.tclORELSE (Proofview.Goal.enter begin fun gl -> let is_conv_leq = Tacmach.New.pf_apply is_conv_leq gl in - filter_hyp (fun typ -> is_conv_leq typ t) - (fun id' -> simplest_elim (mkApp (mkVar id,[|mkVar id'|]))) + filter_hyp (fun typ -> is_conv_leq typ t) + (fun id' -> simplest_elim (mkApp (mkVar id,[|mkVar id'|]))) end) begin function (e, info) -> match e with - | Not_found -> seek_neg rest + | Not_found -> seek_neg rest | e -> Proofview.tclZERO ~info e end) - | _ -> seek_neg rest + | _ -> seek_neg rest in let hyps = Proofview.Goal.hyps gl in seek_neg hyps diff --git a/tactics/declare.ml b/tactics/declare.ml index 7d32f1a7e8..da4de3df77 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -56,7 +56,7 @@ let declare_universe_context ~poly ctx = let nas = name_instance (Univ.UContext.instance uctx) in Global.push_section_context (nas, uctx) else - Global.push_context_set false ctx + Global.push_context_set ~strict:true ctx (** Declaration of constants and parameters *) @@ -139,9 +139,6 @@ let (inConstant : constant_obj -> obj) = subst_function = ident_subst_function; discharge_function = discharge_constant } -let declare_scheme = ref (fun _ _ -> assert false) -let set_declare_scheme f = declare_scheme := f - let update_tables c = Impargs.declare_constant_implicits c; Notation.declare_ref_arguments_scope Evd.empty (GlobRef.ConstRef c) @@ -159,7 +156,7 @@ let register_side_effect (c, role) = let () = register_constant c Decls.(IsProof Theorem) ImportDefaultBehavior in match role with | None -> () - | Some (Evd.Schema (ind, kind)) -> !declare_scheme kind [|ind,c|] + | Some (Evd.Schema (ind, kind)) -> DeclareScheme.declare_scheme kind [|ind,c|] let record_aux env s_ty s_bo = let open Environ in @@ -174,6 +171,7 @@ let record_aux env s_ty s_bo = Aux_file.record_in_aux "context_used" v let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty + let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) body = { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); @@ -184,6 +182,26 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types proof_entry_feedback = None; proof_entry_inline_code = inline} +let pure_definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types + ?(univs=default_univ_entry) body = + { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), ()); + proof_entry_secctx = None; + proof_entry_type = types; + proof_entry_universes = univs; + proof_entry_opaque = opaque; + proof_entry_feedback = None; + proof_entry_inline_code = inline} + +let delayed_definition_entry ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?(univs=default_univ_entry) ?types body = + { proof_entry_body = body + ; proof_entry_secctx = section_vars + ; proof_entry_type = types + ; proof_entry_universes = univs + ; proof_entry_opaque = opaque + ; proof_entry_feedback = feedback_id + ; proof_entry_inline_code = inline + } + let cast_proof_entry e = let (body, ctx), () = Future.force e.proof_entry_body in let univs = @@ -266,6 +284,7 @@ let get_roles export eff = List.map map export let feedback_axiom () = Feedback.(feedback AddedAxiom) + let is_unsafe_typing_flags () = let flags = Environ.typing_flags (Global.env()) in not (flags.check_universes && flags.check_guarded && flags.check_positive) @@ -325,6 +344,12 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind let eff = { Evd.seff_private = eff; Evd.seff_roles; } in kn, eff +let inline_private_constants ~univs env ce = + let body, eff = Future.force ce.proof_entry_body in + let cb, ctx = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in + let univs = UState.merge ~sideff:true Evd.univ_rigid univs ctx in + cb, univs + (** Declaration of section variables and local definitions *) type variable_declaration = | SectionLocalDef of Evd.side_effects proof_entry @@ -375,132 +400,6 @@ let declare_variable ~name ~kind d = Impargs.declare_var_implicits ~impl name; Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name) -(** Declaration of inductive blocks *) -let declare_inductive_argument_scopes kn mie = - List.iteri (fun i {mind_entry_consnames=lc} -> - Notation.declare_ref_arguments_scope Evd.empty (GlobRef.IndRef (kn,i)); - for j=1 to List.length lc do - Notation.declare_ref_arguments_scope Evd.empty (GlobRef.ConstructRef ((kn,i),j)); - done) mie.mind_entry_inds - -type inductive_obj = { - ind_names : (Id.t * Id.t list) list - (* For each block, name of the type + name of constructors *) -} - -let inductive_names sp kn obj = - let (dp,_) = Libnames.repr_path sp in - let kn = Global.mind_of_delta_kn kn in - let names, _ = - List.fold_left - (fun (names, n) (typename, consnames) -> - let ind_p = (kn,n) in - let names, _ = - List.fold_left - (fun (names, p) l -> - let sp = - Libnames.make_path dp l - in - ((sp, GlobRef.ConstructRef (ind_p,p)) :: names, p+1)) - (names, 1) consnames in - let sp = Libnames.make_path dp typename - in - ((sp, GlobRef.IndRef ind_p) :: names, n+1)) - ([], 0) obj.ind_names - in names - -let load_inductive i ((sp, kn), names) = - let names = inductive_names sp kn names in - List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names - -let open_inductive i ((sp, kn), names) = - let names = inductive_names sp kn names in - List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names - -let cache_inductive ((sp, kn), names) = - let names = inductive_names sp kn names in - List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names - -let discharge_inductive ((sp, kn), names) = - Some names - -let inInductive : inductive_obj -> obj = - declare_object {(default_object "INDUCTIVE") with - cache_function = cache_inductive; - load_function = load_inductive; - open_function = open_inductive; - classify_function = (fun a -> Substitute a); - subst_function = ident_subst_function; - discharge_function = discharge_inductive; - } - -let cache_prim (_,(p,c)) = Recordops.register_primitive_projection p c - -let load_prim _ p = cache_prim p - -let subst_prim (subst,(p,c)) = Mod_subst.subst_proj_repr subst p, Mod_subst.subst_constant subst c - -let discharge_prim (_,(p,c)) = Some (Lib.discharge_proj_repr p, c) - -let inPrim : (Projection.Repr.t * Constant.t) -> obj = - declare_object { - (default_object "PRIMPROJS") with - cache_function = cache_prim ; - load_function = load_prim; - subst_function = subst_prim; - classify_function = (fun x -> Substitute x); - discharge_function = discharge_prim } - -let declare_primitive_projection p c = Lib.add_anonymous_leaf (inPrim (p,c)) - -let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) = - let name = Label.to_id label in - let univs, u = match univs with - | Monomorphic_entry _ -> - (* Global constraints already defined through the inductive *) - default_univ_entry, Univ.Instance.empty - | Polymorphic_entry (nas, ctx) -> - Polymorphic_entry (nas, ctx), Univ.UContext.instance ctx - in - let term = Vars.subst_instance_constr u term in - let types = Vars.subst_instance_constr u types in - let entry = definition_entry ~types ~univs term in - let cst = declare_constant ~name ~kind:Decls.(IsDefinition StructureComponent) (DefinitionEntry entry) in - let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in - declare_primitive_projection p cst - -let declare_projections univs mind = - let env = Global.env () in - let mib = Environ.lookup_mind mind env in - match mib.mind_record with - | PrimRecord info -> - let iter_ind i (_, labs, _, _) = - let ind = (mind, i) in - let projs = Inductiveops.compute_projections env ind in - Array.iter2_i (declare_one_projection univs ind ~proj_npars:mib.mind_nparams) labs projs - in - let () = Array.iteri iter_ind info in - true - | FakeRecord -> false - | NotRecord -> false - -(* for initial declaration *) -let declare_mind mie = - let id = match mie.mind_entry_inds with - | ind::_ -> ind.mind_entry_typename - | [] -> CErrors.anomaly (Pp.str "cannot declare an empty list of inductives.") in - let map_names mip = (mip.mind_entry_typename, mip.mind_entry_consnames) in - let names = List.map map_names mie.mind_entry_inds in - List.iter (fun (typ, cons) -> check_exists typ; List.iter check_exists cons) names; - let _kn' = Global.add_mind id mie in - let (sp,kn as oname) = add_leaf id (inInductive { ind_names = names }) in - if is_unsafe_typing_flags() then feedback_axiom(); - let mind = Global.mind_of_delta_kn kn in - let isprim = declare_projections mie.mind_entry_universes mind in - Impargs.declare_mib_implicits mind; - declare_inductive_argument_scopes mind mie; - oname, isprim - (* Declaration messages *) let pr_rank i = pr_nth (i+1) @@ -539,105 +438,63 @@ let assumption_message id = discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *) Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared") -(** Global universes are not substitutive objects but global objects - bound at the *library* or *module* level. The polymorphic flag is - used to distinguish universes declared in polymorphic sections, which - are discharged and do not remain in scope. *) - -type universe_source = - | BoundUniv (* polymorphic universe, bound in a function (this will go away someday) *) - | QualifiedUniv of Id.t (* global universe introduced by some global value *) - | UnqualifiedUniv (* other global universe *) - -type universe_name_decl = universe_source * (Id.t * Univ.Level.UGlobal.t) list - -let check_exists_universe sp = - if Nametab.exists_universe sp then - raise (AlreadyDeclared (Some "Universe", Libnames.basename sp)) - else () - -let qualify_univ i dp src id = - match src with - | BoundUniv | UnqualifiedUniv -> - i, Libnames.make_path dp id - | QualifiedUniv l -> - let dp = DirPath.repr dp in - Nametab.map_visibility succ i, Libnames.make_path (DirPath.make (l::dp)) id - -let do_univ_name ~check i dp src (id,univ) = - let i, sp = qualify_univ i dp src id in - if check then check_exists_universe sp; - Nametab.push_universe i sp univ - -let cache_univ_names ((sp, _), (src, univs)) = - let depth = sections_depth () in - let dp = Libnames.pop_dirpath_n depth (Libnames.dirpath sp) in - List.iter (do_univ_name ~check:true (Nametab.Until 1) dp src) univs - -let load_univ_names i ((sp, _), (src, univs)) = - List.iter (do_univ_name ~check:false (Nametab.Until i) (Libnames.dirpath sp) src) univs - -let open_univ_names i ((sp, _), (src, univs)) = - List.iter (do_univ_name ~check:false (Nametab.Exactly i) (Libnames.dirpath sp) src) univs - -let discharge_univ_names = function - | _, (BoundUniv, _) -> None - | _, ((QualifiedUniv _ | UnqualifiedUniv), _ as x) -> Some x - -let input_univ_names : universe_name_decl -> Libobject.obj = - declare_object - { (default_object "Global universe name state") with - cache_function = cache_univ_names; - load_function = load_univ_names; - open_function = open_univ_names; - discharge_function = discharge_univ_names; - subst_function = (fun (subst, a) -> (* Actually the name is generated once and for all. *) a); - classify_function = (fun a -> Substitute a) } - -let declare_univ_binders gr pl = - if Global.is_polymorphic gr then - () - else - let l = let open GlobRef in match gr with - | ConstRef c -> Label.to_id @@ Constant.label c - | IndRef (c, _) -> Label.to_id @@ MutInd.label c - | VarRef id -> - CErrors.anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".") - | ConstructRef _ -> - CErrors.anomaly ~label:"declare_univ_binders" - Pp.(str "declare_univ_binders on an constructor reference") - in - let univs = Id.Map.fold (fun id univ univs -> - match Univ.Level.name univ with - | None -> assert false (* having Prop/Set/Var as binders is nonsense *) - | Some univ -> (id,univ)::univs) pl [] +module Internal = struct + + let map_entry_body ~f entry = + { entry with proof_entry_body = Future.chain entry.proof_entry_body f } + + let map_entry_type ~f entry = + { entry with proof_entry_type = f entry.proof_entry_type } + + let set_opacity ~opaque entry = + { entry with proof_entry_opaque = opaque } + + let get_fix_exn entry = Future.fix_exn_of entry.proof_entry_body + + 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 Context.Rel.Declaration.is_local_assum p + then mkVar (NamedDecl.get_id decl) :: accu + else accu + in + shrink ctx sign c t accu + | _ -> assert false + + let shrink_entry sign const = + let typ = match const.proof_entry_type with + | None -> assert false + | Some t -> t in - Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs)) - -let do_universe ~poly l = - let in_section = Global.sections_are_opened () in - let () = - if poly && not in_section then - CErrors.user_err ~hdr:"Constraint" - (str"Cannot declare polymorphic universes outside sections") - in - let l = List.map (fun {CAst.v=id} -> (id, UnivGen.new_univ_global ())) l in - let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx) - Univ.LSet.empty l, Univ.Constraint.empty - in - let src = if poly then BoundUniv else UnqualifiedUniv in - let () = Lib.add_anonymous_leaf (input_univ_names (src, l)) in - declare_universe_context ~poly ctx - -let do_constraint ~poly l = - let open Univ in - let u_of_id x = - Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x - in - let constraints = List.fold_left (fun acc (l, d, r) -> - let lu = u_of_id l and ru = u_of_id r in - Constraint.add (lu, d, ru) acc) - Constraint.empty l - in - let uctx = ContextSet.add_constraints constraints ContextSet.empty in - declare_universe_context ~poly uctx + (* The body has been forced by the call to [build_constant_by_tactic] *) + let () = assert (Future.is_over const.proof_entry_body) in + let ((body, uctx), eff) = Future.force const.proof_entry_body in + let (body, typ, ctx) = decompose (List.length sign) body typ [] in + let (body, typ, args) = shrink ctx sign body typ [] in + { const with + proof_entry_body = Future.from_val ((body, uctx), eff) + ; proof_entry_type = Some typ + }, args + +end diff --git a/tactics/declare.mli b/tactics/declare.mli index a6c1374a77..c646d2f85b 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -20,7 +20,7 @@ open Entries [Nametab] and [Impargs]. *) (** Proof entries *) -type 'a proof_entry = { +type 'a proof_entry = private { proof_entry_body : 'a Entries.const_entry_body; (* List of section variables *) proof_entry_secctx : Id.Set.t option; @@ -43,6 +43,8 @@ type 'a constant_entry = | ParameterEntry of parameter_entry | PrimitiveEntry of primitive_entry +val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit + val declare_variable : name:variable -> kind:Decls.logical_kind @@ -53,10 +55,35 @@ val declare_variable i.e. Definition/Theorem/Axiom/Parameter/... *) (* Default definition entries, transparent with no secctx or proj information *) -val definition_entry : ?fix_exn:Future.fix_exn -> - ?opaque:bool -> ?inline:bool -> ?types:types -> - ?univs:Entries.universes_entry -> - ?eff:Evd.side_effects -> constr -> Evd.side_effects proof_entry +val definition_entry + : ?fix_exn:Future.fix_exn + -> ?opaque:bool + -> ?inline:bool + -> ?types:types + -> ?univs:Entries.universes_entry + -> ?eff:Evd.side_effects + -> constr + -> Evd.side_effects proof_entry + +val pure_definition_entry + : ?fix_exn:Future.fix_exn + -> ?opaque:bool + -> ?inline:bool + -> ?types:types + -> ?univs:Entries.universes_entry + -> constr + -> unit proof_entry + +(* Delayed definition entries *) +val delayed_definition_entry + : ?opaque:bool + -> ?inline:bool + -> ?feedback_id:Stateid.t + -> ?section_vars:Id.Set.t + -> ?univs:Entries.universes_entry + -> ?types:types + -> 'a Entries.const_entry_body + -> 'a proof_entry type import_status = ImportDefaultBehavior | ImportNeedQualified @@ -81,15 +108,14 @@ val declare_private_constant -> unit proof_entry -> Constant.t * Evd.side_effects -(** Since transparent constants' side effects are globally declared, we - * need that *) -val set_declare_scheme : - (string -> (inductive * Constant.t) array -> unit) -> unit - -(** [declare_mind me] declares a block of inductive types with - their constructors in the current section; it returns the path of - the whole block and a boolean indicating if it is a primitive record. *) -val declare_mind : mutual_inductive_entry -> Libobject.object_name * bool +(** [inline_private_constants ~sideff ~univs env ce] will inline the + constants in [ce]'s body and return the body plus the updated + [UState.t]. *) +val inline_private_constants + : univs:UState.t + -> Environ.env + -> Evd.side_effects proof_entry + -> Constr.t * UState.t (** Declaration messages *) @@ -100,15 +126,23 @@ val cofixpoint_message : Id.t list -> unit val recursive_message : bool (** true = fixpoint *) -> int array option -> Id.t list -> unit -val exists_name : Id.t -> bool +val check_exists : Id.t -> unit + +(* Used outside this module only in indschemes *) +exception AlreadyDeclared of (string option * Id.t) -(** Global universe contexts, names and constraints *) -val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit +(* For legacy support, do not use *) +module Internal : sig -val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit + val map_entry_body : f:('a Entries.proof_output -> 'b Entries.proof_output) -> 'a proof_entry -> 'b proof_entry + val map_entry_type : f:(Constr.t option -> Constr.t option) -> 'a proof_entry -> 'a proof_entry + (* Overriding opacity is indeed really hacky *) + val set_opacity : opaque:bool -> 'a proof_entry -> 'a proof_entry -val do_universe : poly:bool -> lident list -> unit -val do_constraint : poly:bool -> Glob_term.glob_constraint list -> unit + (* TODO: This is only used in DeclareDef to forward the fix to + hooks, should eventually go away *) + val get_fix_exn : 'a proof_entry -> Future.fix_exn -(* Used outside this module only in indschemes *) -exception AlreadyDeclared of (string option * Id.t) + val shrink_entry : EConstr.named_context -> 'a proof_entry -> 'a proof_entry * Constr.constr list + +end diff --git a/tactics/declareScheme.ml b/tactics/declareScheme.ml new file mode 100644 index 0000000000..5f4626fcb2 --- /dev/null +++ b/tactics/declareScheme.ml @@ -0,0 +1,42 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names + +let scheme_map = Summary.ref Indmap.empty ~name:"Schemes" + +let cache_one_scheme kind (ind,const) = + let map = try Indmap.find ind !scheme_map with Not_found -> CString.Map.empty in + scheme_map := Indmap.add ind (CString.Map.add kind const map) !scheme_map + +let cache_scheme (_,(kind,l)) = + Array.iter (cache_one_scheme kind) l + +let subst_one_scheme subst (ind,const) = + (* Remark: const is a def: the result of substitution is a constant *) + (Mod_subst.subst_ind subst ind, Mod_subst.subst_constant subst const) + +let subst_scheme (subst,(kind,l)) = + (kind, CArray.Smart.map (subst_one_scheme subst) l) + +let discharge_scheme (_,(kind,l)) = + Some (kind, l) + +let inScheme : string * (inductive * Constant.t) array -> Libobject.obj = + let open Libobject in + declare_object @@ superglobal_object "SCHEME" + ~cache:cache_scheme + ~subst:(Some subst_scheme) + ~discharge:discharge_scheme + +let declare_scheme kind indcl = + Lib.add_anonymous_leaf (inScheme (kind,indcl)) + +let lookup_scheme kind ind = CString.Map.find kind (Indmap.find ind !scheme_map) diff --git a/tactics/declareScheme.mli b/tactics/declareScheme.mli new file mode 100644 index 0000000000..f2ae5e41c8 --- /dev/null +++ b/tactics/declareScheme.mli @@ -0,0 +1,12 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +val declare_scheme : string -> (Names.inductive * Names.Constant.t) array -> unit +val lookup_scheme : string -> Names.inductive -> Names.Constant.t diff --git a/tactics/dn.ml b/tactics/dn.ml index aed2c28323..e1c9b7c0b5 100644 --- a/tactics/dn.ml +++ b/tactics/dn.ml @@ -11,14 +11,14 @@ struct type t = (Y.t * int) option let compare x y = match x,y with - None,None -> 0 - | Some (l,n),Some (l',n') -> - let m = Y.compare l l' in - if Int.equal m 0 then - n-n' - else m - | Some(l,n),None -> 1 - | None, Some(l,n) -> -1 + None,None -> 0 + | Some (l,n),Some (l',n') -> + let m = Y.compare l l' in + if Int.equal m 0 then + n-n' + else m + | Some(l,n),None -> 1 + | None, Some(l,n) -> -1 end module ZSet = Set.Make(Z) module X_tries = @@ -50,12 +50,12 @@ prefix ordering, [dna] is the function returning the main node of a pattern *) and pathrec deferred t = match dna t with - | None -> - None :: (path_of_deferred deferred) - | Some (lbl,[]) -> - (Some (lbl,0))::(path_of_deferred deferred) - | Some (lbl,(h::def_subl as v)) -> - (Some (lbl,List.length v))::(pathrec (def_subl@deferred) h) + | None -> + None :: (path_of_deferred deferred) + | Some (lbl,[]) -> + (Some (lbl,0))::(path_of_deferred deferred) + | Some (lbl,(h::def_subl as v)) -> + (Some (lbl,List.length v))::(pathrec (def_subl@deferred) h) in pathrec [] @@ -76,16 +76,16 @@ prefix ordering, [dna] is the function returning the main node of a pattern *) let lookup tm dna t = let rec lookrec t tm = match dna t with - | Nothing -> tm_of tm None - | Label(lbl,v) -> - tm_of tm None@ - (List.fold_left - (fun l c -> - List.flatten(List.map (fun (tm, b) -> - if b then lookrec c tm - else [tm,b]) l)) - (tm_of tm (Some(lbl,List.length v))) v) - | Everything -> skip_arg 1 tm + | Nothing -> tm_of tm None + | Label(lbl,v) -> + tm_of tm None@ + (List.fold_left + (fun l c -> + List.flatten(List.map (fun (tm, b) -> + if b then lookrec c tm + else [tm,b]) l)) + (tm_of tm (Some(lbl,List.length v))) v) + | Everything -> skip_arg 1 tm in List.flatten (List.map (fun (tm,b) -> ZSet.elements (Trie.get tm)) (lookrec t tm)) diff --git a/tactics/dnet.ml b/tactics/dnet.ml index 3171bee7ca..389329c19f 100644 --- a/tactics/dnet.ml +++ b/tactics/dnet.ml @@ -62,7 +62,7 @@ struct module Idset = Set.Make(Ident) module Mmap = Map.Make(Meta) module Tmap = Map.Make(struct type t = unit structure - let compare = T.compare end) + let compare = T.compare end) type idset = Idset.t @@ -93,23 +93,23 @@ struct let rec add (Nodes (t,m):t) (w:term_pattern) (id:ident) : t = match w with Term w -> ( try - let (n,tl) = split t w in - let new_node = match n with - | Terminal (e,is) -> Terminal (e,Idset.add id is) - | Node e -> Node (T.map2 (fun t p -> add t p id) e w) in - Nodes ((Tmap.add (head w) new_node tl), m) - with Not_found -> - let new_content = T.map (fun p -> add empty p id) w in - let new_node = - if T.terminal w then - Terminal (new_content, Idset.singleton id) - else Node new_content in - Nodes ((Tmap.add (head w) new_node t), m) ) + let (n,tl) = split t w in + let new_node = match n with + | Terminal (e,is) -> Terminal (e,Idset.add id is) + | Node e -> Node (T.map2 (fun t p -> add t p id) e w) in + Nodes ((Tmap.add (head w) new_node tl), m) + with Not_found -> + let new_content = T.map (fun p -> add empty p id) w in + let new_node = + if T.terminal w then + Terminal (new_content, Idset.singleton id) + else Node new_content in + Nodes ((Tmap.add (head w) new_node t), m) ) | Meta i -> - let m = - try Mmap.add i (Idset.add id (Mmap.find i m)) m - with Not_found -> Mmap.add i (Idset.singleton id) m in - Nodes (t, m) + let m = + try Mmap.add i (Idset.add id (Mmap.find i m)) m + with Not_found -> Mmap.add i (Idset.singleton id) m in + Nodes (t, m) let add t w id = add t w id @@ -117,12 +117,12 @@ struct Idset.union (Mmap.fold (fun _ -> Idset.union) m Idset.empty) (Tmap.fold - ( fun _ n acc -> - let s2 = match n with - | Terminal (_,is) -> is - | Node e -> T.choose find_all e in - Idset.union acc s2 - ) t Idset.empty) + ( fun _ n acc -> + let s2 = match n with + | Terminal (_,is) -> is + | Node e -> T.choose find_all e in + Idset.union acc s2 + ) t Idset.empty) (* (\* optimization hack: Not_found is caught in fold_pattern *\) *) (* let fast_inter s1 s2 = *) @@ -176,13 +176,13 @@ struct let inter s1 s2 : t = match s1,s2 with | (None, a | a, None) -> a | Some a, Some b -> Some (S.inter a b) - let is_empty : t -> bool = function + let is_empty : t -> bool = function | None -> false | Some s -> S.is_empty s (* optimization hack: Not_found is caught in fold_pattern *) let fast_inter s1 s2 = if is_empty s1 || is_empty s2 then raise Not_found - else let r = inter s1 s2 in + else let r = inter s1 s2 in if is_empty r then raise Not_found else r let full = None let empty = Some S.empty @@ -197,29 +197,29 @@ struct let rec fp_rec metas p (Nodes(t,m) as dn:t) = (* TODO gérer les dnets non-linéaires *) let metas = Mmap.fold (fun _ -> Idset.union) m metas in - match p with - | Meta m -> defer (metas,m,dn); OIdset.full - | Term w -> - let curm = Mmap.fold (fun _ -> Idset.union) m Idset.empty in - try match select t w with - | Terminal (_,is) -> Some (Idset.union curm is) - | Node e -> - let ids = if complete then T.fold2 - (fun acc w e -> - OIdset.fast_inter acc (fp_rec metas w e) - ) OIdset.full w e - else - let (all_metas, res) = T.fold2 - (fun (b,acc) w e -> match w with - | Term _ -> false, OIdset.fast_inter acc (fp_rec metas w e) - | Meta _ -> b, acc - ) (true,OIdset.full) w e in - if all_metas then T.choose (T.choose (fp_rec metas) w) e - else res in - OIdset.union ids (Some curm) - with Not_found -> - if Idset.is_empty metas then raise Not_found else Some curm in - let cand = + match p with + | Meta m -> defer (metas,m,dn); OIdset.full + | Term w -> + let curm = Mmap.fold (fun _ -> Idset.union) m Idset.empty in + try match select t w with + | Terminal (_,is) -> Some (Idset.union curm is) + | Node e -> + let ids = if complete then T.fold2 + (fun acc w e -> + OIdset.fast_inter acc (fp_rec metas w e) + ) OIdset.full w e + else + let (all_metas, res) = T.fold2 + (fun (b,acc) w e -> match w with + | Term _ -> false, OIdset.fast_inter acc (fp_rec metas w e) + | Meta _ -> b, acc + ) (true,OIdset.full) w e in + if all_metas then T.choose (T.choose (fp_rec metas) w) e + else res in + OIdset.union ids (Some curm) + with Not_found -> + if Idset.is_empty metas then raise Not_found else Some curm in + let cand = try fp_rec Idset.empty pat dn with Not_found -> OIdset.empty in let res = List.fold_left f acc !deferred in @@ -229,54 +229,54 @@ struct let rec inter (t1:t) (t2:t) : t = let inter_map f (Nodes (t1,m1):t) (Nodes (t2,m2):t) : t = Nodes - (Tmap.fold - ( fun k e acc -> - try Tmap.add k (f e (Tmap.find k t2)) acc - with Not_found -> acc - ) t1 Tmap.empty, - Mmap.fold - ( fun m s acc -> - try Mmap.add m (Idset.inter s (Mmap.find m m2)) acc - with Not_found -> acc - ) m1 Mmap.empty - ) in + (Tmap.fold + ( fun k e acc -> + try Tmap.add k (f e (Tmap.find k t2)) acc + with Not_found -> acc + ) t1 Tmap.empty, + Mmap.fold + ( fun m s acc -> + try Mmap.add m (Idset.inter s (Mmap.find m m2)) acc + with Not_found -> acc + ) m1 Mmap.empty + ) in inter_map (fun n1 n2 -> match n1,n2 with - | Terminal (e1,s1), Terminal (_,s2) -> Terminal (e1,Idset.inter s1 s2) - | Node e1, Node e2 -> Node (T.map2 inter e1 e2) - | _ -> assert false + | Terminal (e1,s1), Terminal (_,s2) -> Terminal (e1,Idset.inter s1 s2) + | Node e1, Node e2 -> Node (T.map2 inter e1 e2) + | _ -> assert false ) t1 t2 let rec union (t1:t) (t2:t) : t = let union_map f (Nodes (t1,m1):t) (Nodes (t2,m2):t) : t = Nodes - (Tmap.fold - ( fun k e acc -> - try Tmap.add k (f e (Tmap.find k acc)) acc - with Not_found -> Tmap.add k e acc - ) t1 t2, - Mmap.fold - ( fun m s acc -> - try Mmap.add m (Idset.inter s (Mmap.find m acc)) acc - with Not_found -> Mmap.add m s acc - ) m1 m2 - ) in + (Tmap.fold + ( fun k e acc -> + try Tmap.add k (f e (Tmap.find k acc)) acc + with Not_found -> Tmap.add k e acc + ) t1 t2, + Mmap.fold + ( fun m s acc -> + try Mmap.add m (Idset.inter s (Mmap.find m acc)) acc + with Not_found -> Mmap.add m s acc + ) m1 m2 + ) in union_map (fun n1 n2 -> match n1,n2 with - | Terminal (e1,s1), Terminal (_,s2) -> Terminal (e1,Idset.union s1 s2) - | Node e1, Node e2 -> Node (T.map2 union e1 e2) - | _ -> assert false + | Terminal (e1,s1), Terminal (_,s2) -> Terminal (e1,Idset.union s1 s2) + | Node e1, Node e2 -> Node (T.map2 union e1 e2) + | _ -> assert false ) t1 t2 let find_match (p:term_pattern) (t:t) : idset = let metas = ref Mmap.empty in let (mset,lset) = fold_pattern ~complete:false (fun acc (mset,m,t) -> - let all = OIdset.fast_inter acc - (Some(let t = try inter t (Mmap.find m !metas) with Not_found -> t in - metas := Mmap.add m t !metas; - find_all t)) in - OIdset.union (Some mset) all + let all = OIdset.fast_inter acc + (Some(let t = try inter t (Mmap.find m !metas) with Not_found -> t in + metas := Mmap.add m t !metas; + find_all t)) in + OIdset.union (Some mset) all ) None p t in Option.get (OIdset.inter mset lset) diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 2ce32b309a..361215bf38 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -86,16 +86,13 @@ let rec prolog l n gl = let prol = (prolog l (n-1)) in (tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl -let out_term env = function - | IsConstr (c, _) -> c - | IsGlobRef gr -> EConstr.of_constr (fst (UnivGen.fresh_global_instance env gr)) - let prolog_tac l n = Proofview.V82.tactic begin fun gl -> let map c = let (sigma, c) = c (pf_env gl) (project gl) in - let c = pf_apply (prepare_hint false (false,true)) gl (sigma, c) in - out_term (pf_env gl) c + (* Dropping the universe context is probably wrong *) + let (c, _) = pf_apply (prepare_hint false) gl (sigma, c) in + c in let l = List.map map l in try (prolog l n gl) @@ -157,8 +154,8 @@ and e_my_find_search env sigma db_list local_db secvars hdc concl = let hint_of_db = hintmap_of sigma secvars hdc concl in let hintl = List.map_append (fun db -> - let flags = auto_flags_of_state (Hint_db.transparent_state db) in - List.map (fun x -> flags, x) (hint_of_db db)) (local_db::db_list) + let flags = auto_flags_of_state (Hint_db.transparent_state db) in + List.map (fun x -> flags, x) (hint_of_db db)) (local_db::db_list) in let tac_of_hint = fun (st, {pri = b; pat = p; code = t; poly = poly}) -> @@ -230,12 +227,12 @@ module SearchProblem = struct let rec aux = function | [] -> [] | (tac, cost, pptac) :: tacl -> - try - let lgls = apply_tac_list (Proofview.V82.of_tactic tac) glls in + try + let lgls = apply_tac_list (Proofview.V82.of_tactic tac) glls in (* let gl = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *) (* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *) - (lgls, cost, pptac) :: aux tacl - with e when CErrors.noncritical e -> + (lgls, cost, pptac) :: aux tacl + with e when CErrors.noncritical e -> let e = CErrors.push e in Refiner.catch_failerror e; aux tacl in aux l @@ -265,60 +262,60 @@ module SearchProblem = struct let assumption_tacs = let tacs = List.map map_assum hyps in let l = filter_tactics s.tacres tacs in - List.map (fun (res, cost, pp) -> { depth = s.depth; priority = cost; tacres = res; - last_tactic = pp; dblist = s.dblist; - localdb = List.tl s.localdb; - prev = ps; local_lemmas = s.local_lemmas}) l + List.map (fun (res, cost, pp) -> { depth = s.depth; priority = cost; tacres = res; + last_tactic = pp; dblist = s.dblist; + localdb = List.tl s.localdb; + prev = ps; local_lemmas = s.local_lemmas}) l in let intro_tac = let l = filter_tactics s.tacres [Tactics.intro, (-1), lazy (str "intro")] in - List.map - (fun (lgls, cost, pp) -> - let g' = first_goal lgls in - let hintl = - make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g') - in + List.map + (fun (lgls, cost, pp) -> + let g' = first_goal lgls in + let hintl = + make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g') + in let ldb = Hint_db.add_list (pf_env g') (project g') - hintl (List.hd s.localdb) in - { depth = s.depth; priority = cost; tacres = lgls; - last_tactic = pp; dblist = s.dblist; - localdb = ldb :: List.tl s.localdb; prev = ps; + hintl (List.hd s.localdb) in + { depth = s.depth; priority = cost; tacres = lgls; + last_tactic = pp; dblist = s.dblist; + localdb = ldb :: List.tl s.localdb; prev = ps; local_lemmas = s.local_lemmas}) - l + l in let rec_tacs = - let l = + let l = let concl = Reductionops.nf_evar (project g) (pf_concl g) in - filter_tactics s.tacres + filter_tactics s.tacres (e_possible_resolve (pf_env g) (project g) s.dblist (List.hd s.localdb) secvars concl) - in - List.map - (fun (lgls, cost, pp) -> - let nbgl' = List.length (sig_it lgls) in - if nbgl' < nbgl then - { depth = s.depth; priority = cost; tacres = lgls; last_tactic = pp; + in + List.map + (fun (lgls, cost, pp) -> + let nbgl' = List.length (sig_it lgls) in + if nbgl' < nbgl then + { depth = s.depth; priority = cost; tacres = lgls; last_tactic = pp; prev = ps; dblist = s.dblist; localdb = List.tl s.localdb; local_lemmas = s.local_lemmas } - else - let newlocal = - let hyps = pf_hyps g in - List.map (fun gl -> - let gls = {Evd.it = gl; sigma = lgls.Evd.sigma } in - let hyps' = pf_hyps gls in - if hyps' == hyps then List.hd s.localdb + else + let newlocal = + let hyps = pf_hyps g in + List.map (fun gl -> + let gls = {Evd.it = gl; sigma = lgls.Evd.sigma } in + let hyps' = pf_hyps gls in + if hyps' == hyps then List.hd s.localdb else make_local_hint_db (pf_env gls) (project gls) ~ts:TransparentState.full true s.local_lemmas) - (List.firstn ((nbgl'-nbgl) + 1) (sig_it lgls)) - in - { depth = pred s.depth; priority = cost; tacres = lgls; - dblist = s.dblist; last_tactic = pp; prev = ps; - localdb = newlocal @ List.tl s.localdb; + (List.firstn ((nbgl'-nbgl) + 1) (sig_it lgls)) + in + { depth = pred s.depth; priority = cost; tacres = lgls; + dblist = s.dblist; last_tactic = pp; prev = ps; + localdb = newlocal @ List.tl s.localdb; local_lemmas = s.local_lemmas }) - l + l in List.sort compare (assumption_tacs @ intro_tac @ rec_tacs) let pp s = hov 0 (str " depth=" ++ int s.depth ++ spc () ++ - (Lazy.force s.last_tactic)) + (Lazy.force s.last_tactic)) end @@ -364,12 +361,12 @@ let pr_info dbg s = else let rec loop s = match s.prev with - | Unknown | Init -> s.depth - | State sp -> - let mindepth = loop sp in - let indent = String.make (mindepth - sp.depth) ' ' in + | Unknown | Init -> s.depth + | State sp -> + let mindepth = loop sp in + let indent = String.make (mindepth - sp.depth) ' ' in Feedback.msg_notice (str indent ++ Lazy.force s.last_tactic ++ str "."); - mindepth + mindepth in ignore (loop s) @@ -433,15 +430,15 @@ let make_dimension n = function let cons a l = a :: l let autounfolds db occs cls gl = - let unfolds = List.concat (List.map (fun dbname -> - let db = try searchtable_map dbname + let unfolds = List.concat (List.map (fun dbname -> + let db = try searchtable_map dbname with Not_found -> user_err ~hdr:"autounfold" (str "Unknown database " ++ str dbname) in let (ids, csts) = Hint_db.unfolds db in let hyps = pf_ids_of_hyps gl in let ids = Id.Set.filter (fun id -> List.mem id hyps) ids in Cset.fold (fun cst -> cons (AllOccurrences, EvalConstRef cst)) csts - (Id.Set.fold (fun id -> cons (AllOccurrences, EvalVarRef id)) ids [])) db) + (Id.Set.fold (fun id -> cons (AllOccurrences, EvalVarRef id)) ids [])) db) in Proofview.V82.of_tactic (unfold_option unfolds cls) gl let autounfold db cls = @@ -464,36 +461,36 @@ let autounfold_tac db cls = autounfold dbs cls let unfold_head env sigma (ids, csts) c = - let rec aux c = + let rec aux c = match EConstr.kind sigma c with | Var id when Id.Set.mem id ids -> - (match Environ.named_body id env with - | Some b -> true, EConstr.of_constr b - | None -> false, c) + (match Environ.named_body id env with + | Some b -> true, EConstr.of_constr b + | None -> false, c) | Const (cst, u) when Cset.mem cst csts -> let u = EInstance.kind sigma u in - true, EConstr.of_constr (Environ.constant_value_in env (cst, u)) + true, EConstr.of_constr (Environ.constant_value_in env (cst, u)) | App (f, args) -> - (match aux f with - | true, f' -> true, Reductionops.whd_betaiota sigma (mkApp (f', args)) - | false, _ -> - let done_, args' = - Array.fold_left_i (fun i (done_, acc) arg -> - if done_ then done_, arg :: acc - else match aux arg with - | true, arg' -> true, arg' :: acc - | false, arg' -> false, arg :: acc) - (false, []) args - in - if done_ then true, mkApp (f, Array.of_list (List.rev args')) - else false, c) - | _ -> - let done_ = ref false in - let c' = EConstr.map sigma (fun c -> - if !done_ then c else - let x, c' = aux c in - done_ := x; c') c - in !done_, c' + (match aux f with + | true, f' -> true, Reductionops.whd_betaiota sigma (mkApp (f', args)) + | false, _ -> + let done_, args' = + Array.fold_left_i (fun i (done_, acc) arg -> + if done_ then done_, arg :: acc + else match aux arg with + | true, arg' -> true, arg' :: acc + | false, arg' -> false, arg :: acc) + (false, []) args + in + if done_ then true, mkApp (f, Array.of_list (List.rev args')) + else false, c) + | _ -> + let done_ = ref false in + let c' = EConstr.map sigma (fun c -> + if !done_ then c else + let x, c' = aux c in + done_ := x; c') c + in !done_, c' in aux c let autounfold_one db cl = @@ -502,15 +499,15 @@ let autounfold_one db cl = let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in let st = - List.fold_left (fun (i,c) dbname -> - let db = try searchtable_map dbname - with Not_found -> user_err ~hdr:"autounfold" (str "Unknown database " ++ str dbname) + List.fold_left (fun (i,c) dbname -> + let db = try searchtable_map dbname + with Not_found -> user_err ~hdr:"autounfold" (str "Unknown database " ++ str dbname) in let (ids, csts) = Hint_db.unfolds db in - (Id.Set.union ids i, Cset.union csts c)) (Id.Set.empty, Cset.empty) db + (Id.Set.union ids i, Cset.union csts c)) (Id.Set.empty, Cset.empty) db in - let did, c' = unfold_head env sigma st - (match cl with Some (id, _) -> Tacmach.New.pf_get_hyp_typ id gl | None -> concl) + let did, c' = unfold_head env sigma st + (match cl with Some (id, _) -> Tacmach.New.pf_get_hyp_typ id gl | None -> concl) in if did then match cl with diff --git a/tactics/elim.ml b/tactics/elim.ml index fcc2a94ef5..ea61b8e4df 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -66,8 +66,8 @@ and general_decompose_aux recognizer id = elimHypThen (introElimAssumsThen (fun bas -> - tclTHEN (clear [id]) - (tclMAP (general_decompose_on_hyp recognizer) + tclTHEN (clear [id]) + (tclMAP (general_decompose_on_hyp recognizer) (ids_of_named_context bas.Tacticals.assums)))) id @@ -88,7 +88,7 @@ let general_decompose recognizer c = [ tclTHEN (intro_using tmphyp_name) (onLastHypId (ifOnHyp (recognizer env sigma) (general_decompose_aux (recognizer env sigma)) - (fun id -> clear [id]))); + (fun id -> clear [id]))); exact_no_check c ] end @@ -136,22 +136,22 @@ let induction_trailer abs_i abs_j bargs = (onLastHypId (fun id -> Proofview.Goal.enter begin fun gl -> - let idty = pf_unsafe_type_of gl (mkVar id) in - let fvty = global_vars (pf_env gl) (project gl) idty in - let possible_bring_hyps = - (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums + let idty = pf_unsafe_type_of gl (mkVar id) in + let fvty = global_vars (pf_env gl) (project gl) idty in + let possible_bring_hyps = + (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums in - let (hyps,_) = + let (hyps,_) = List.fold_left - (fun (bring_ids,leave_ids) d -> + (fun (bring_ids,leave_ids) d -> let cid = NamedDecl.get_id d in if not (List.mem cid leave_ids) then (d::bring_ids,leave_ids) else (bring_ids,cid::leave_ids)) - ([],fvty) possible_bring_hyps - in + ([],fvty) possible_bring_hyps + in let ids = List.rev (ids_of_named_context hyps) in - (tclTHENLIST + (tclTHENLIST [revert ids; simple_elimination (mkVar id)]) end )) @@ -167,7 +167,7 @@ let double_ind h1 h2 = abs >>= fun (abs_i,abs_j) -> (tclTHEN (tclDO abs_i intro) (onLastHypId - (fun id -> + (fun id -> elimination_then (introElimAssumsThen (induction_trailer abs_i abs_j)) (mkVar id)))) end diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 9cd2e7b52c..d6fda00ad8 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -24,34 +24,34 @@ open Ind_tables (* Induction/recursion schemes *) -let optimize_non_type_induction_scheme kind dep sort _ ind = +let optimize_non_type_induction_scheme kind dep sort ind = let env = Global.env () in let sigma = Evd.from_env env in if check_scheme kind ind then (* in case the inductive has a type elimination, generates only one induction scheme, the other ones share the same code with the appropriate type *) - let cte, eff = find_scheme kind ind in + let cte = lookup_scheme kind ind in let sigma, cte = Evd.fresh_constant_instance env sigma cte in let c = mkConstU cte in let t = type_of_constant_in (Global.env()) cte in let (mib,mip) = Global.lookup_inductive ind in let npars = (* if a constructor of [ind] contains a recursive call, the scheme - is generalized only wrt recursively uniform parameters *) + is generalized only wrt recursively uniform parameters *) if (Inductiveops.mis_is_recursive_subset [snd ind] mip.mind_recargs) then - mib.mind_nparams_rec + mib.mind_nparams_rec else - mib.mind_nparams in + mib.mind_nparams in let sigma, sort = Evd.fresh_sort_in_family sigma sort in let sigma, t', c' = weaken_sort_scheme env sigma false sort npars c t in let sigma = Evd.minimize_universes sigma in - (Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma), eff + (Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma) else let sigma, pind = Evd.fresh_inductive_instance env sigma ind in let sigma, c = build_induction_scheme env sigma pind dep sort in - (c, Evd.evar_universe_context sigma), Evd.empty_side_effects + (c, Evd.evar_universe_context sigma) let build_induction_scheme_in_type dep sort ind = let env = Global.env () in @@ -60,17 +60,23 @@ let build_induction_scheme_in_type dep sort ind = let sigma, c = build_induction_scheme env sigma pind dep sort in c, Evd.evar_universe_context sigma +let declare_individual_scheme_object name ?aux f = + let f : individual_scheme_object_function = + fun _ ind -> f ind, Evd.empty_side_effects + in + declare_individual_scheme_object name ?aux f + let rect_scheme_kind_from_type = declare_individual_scheme_object "_rect_nodep" - (fun _ x -> build_induction_scheme_in_type false InType x, Evd.empty_side_effects) + (fun x -> build_induction_scheme_in_type false InType x) let rect_scheme_kind_from_prop = declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop" - (fun _ x -> build_induction_scheme_in_type false InType x, Evd.empty_side_effects) + (fun x -> build_induction_scheme_in_type false InType x) let rect_dep_scheme_kind_from_type = declare_individual_scheme_object "_rect" ~aux:"_rect_from_type" - (fun _ x -> build_induction_scheme_in_type true InType x, Evd.empty_side_effects) + (fun x -> build_induction_scheme_in_type true InType x) let rec_scheme_kind_from_type = declare_individual_scheme_object "_rec_nodep" ~aux:"_rec_nodep_from_type" @@ -90,7 +96,7 @@ let ind_scheme_kind_from_type = let sind_scheme_kind_from_type = declare_individual_scheme_object "_sind_nodep" - (fun _ x -> build_induction_scheme_in_type false InSProp x, Evd.empty_side_effects) + (fun x -> build_induction_scheme_in_type false InSProp x) let ind_dep_scheme_kind_from_type = declare_individual_scheme_object "_ind" ~aux:"_ind_from_type" @@ -98,7 +104,7 @@ let ind_dep_scheme_kind_from_type = let sind_dep_scheme_kind_from_type = declare_individual_scheme_object "_sind" ~aux:"_sind_from_type" - (fun _ x -> build_induction_scheme_in_type true InSProp x, Evd.empty_side_effects) + (fun x -> build_induction_scheme_in_type true InSProp x) let ind_scheme_kind_from_prop = declare_individual_scheme_object "_ind" ~aux:"_ind_from_prop" @@ -106,7 +112,7 @@ let ind_scheme_kind_from_prop = let sind_scheme_kind_from_prop = declare_individual_scheme_object "_sind" ~aux:"_sind_from_prop" - (fun _ x -> build_induction_scheme_in_type false InSProp x, Evd.empty_side_effects) + (fun x -> build_induction_scheme_in_type false InSProp x) let nondep_elim_scheme from_kind to_kind = match from_kind, to_kind with @@ -130,24 +136,24 @@ let build_case_analysis_scheme_in_type dep sort ind = let case_scheme_kind_from_type = declare_individual_scheme_object "_case_nodep" - (fun _ x -> build_case_analysis_scheme_in_type false InType x, Evd.empty_side_effects) + (fun x -> build_case_analysis_scheme_in_type false InType x) let case_scheme_kind_from_prop = declare_individual_scheme_object "_case" ~aux:"_case_from_prop" - (fun _ x -> build_case_analysis_scheme_in_type false InType x, Evd.empty_side_effects) + (fun x -> build_case_analysis_scheme_in_type false InType x) let case_dep_scheme_kind_from_type = declare_individual_scheme_object "_case" ~aux:"_case_from_type" - (fun _ x -> build_case_analysis_scheme_in_type true InType x, Evd.empty_side_effects) + (fun x -> build_case_analysis_scheme_in_type true InType x) let case_dep_scheme_kind_from_type_in_prop = declare_individual_scheme_object "_casep_dep" - (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Evd.empty_side_effects) + (fun x -> build_case_analysis_scheme_in_type true InProp x) let case_dep_scheme_kind_from_prop = declare_individual_scheme_object "_case_dep" - (fun _ x -> build_case_analysis_scheme_in_type true InType x, Evd.empty_side_effects) + (fun x -> build_case_analysis_scheme_in_type true InType x) let case_dep_scheme_kind_from_prop_in_prop = declare_individual_scheme_object "_casep" - (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Evd.empty_side_effects) + (fun x -> build_case_analysis_scheme_in_type true InProp x) diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli index 11dbbc7155..8e167b171c 100644 --- a/tactics/elimschemes.mli +++ b/tactics/elimschemes.mli @@ -12,14 +12,6 @@ open Ind_tables (** Induction/recursion schemes *) -val optimize_non_type_induction_scheme : - 'a Ind_tables.scheme_kind -> - Indrec.dep_flag -> - Sorts.family -> - 'b -> - Names.inductive -> - (Constr.constr * UState.t) * Evd.side_effects - val rect_scheme_kind_from_prop : individual scheme_kind val ind_scheme_kind_from_prop : individual scheme_kind val sind_scheme_kind_from_prop : individual scheme_kind diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index e8782aa674..1df56be0be 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -42,7 +42,7 @@ One may wonder whether these extensions are worth to be done regarding the price we have to pay and regarding the rare - situations where they are needed. However, I believe it meets a + situations where they are needed. However, I believe it meets a natural expectation of the user. *) @@ -69,7 +69,7 @@ let hid = Id.of_string "H" let xid = Id.of_string "X" let default_id_of_sort = function InSProp | InProp | InSet -> hid | InType -> xid let fresh env id = next_global_ident_away id Id.Set.empty -let with_context_set ctx (b, ctx') = +let with_context_set ctx (b, ctx') = (b, Univ.ContextSet.union ctx ctx') let build_dependent_inductive ind (mib,mip) = @@ -88,7 +88,7 @@ let name_context env hyps = snd (List.fold_left (fun (env,hyps) d -> - let d' = name_assumption env d in (push_rel d' env, d' :: hyps)) + let d' = name_assumption env d in (push_rel d' env, d' :: hyps)) (env,[]) (List.rev hyps)) let my_it_mkLambda_or_LetIn s c = it_mkLambda_or_LetIn c s @@ -102,7 +102,7 @@ let get_coq_eq ctx = try let eq = Globnames.destIndRef (Coqlib.lib_ref "core.eq.type") in (* Do not force the lazy if they are not defined *) - let eq, ctx = with_context_set ctx + let eq, ctx = with_context_set ctx (UnivGen.fresh_inductive_instance (Global.env ()) eq) in mkIndU eq, mkConstructUi (eq,1), ctx with Not_found -> @@ -211,16 +211,16 @@ let build_sym_scheme env ind = name_context env ((LocalAssum (make_annot (Name varH) indr,applied_ind))::realsign) in let rci = Sorts.Relevant in (* TODO relevance *) let ci = make_case_info (Global.env()) ind rci RegularStyle in - let c = + let c = (my_it_mkLambda_or_LetIn paramsctxt (my_it_mkLambda_or_LetIn_name realsign_ind (mkCase (ci, my_it_mkLambda_or_LetIn_name (lift_rel_context (nrealargs+1) realsign_ind) (mkApp (mkIndU indu,Array.concat - [Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1; - rel_vect 1 nrealargs; - rel_vect (2*nrealargs+2) nrealargs])), + [Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1; + rel_vect 1 nrealargs; + rel_vect (2*nrealargs+2) nrealargs])), mkRel 1 (* varH *), [|cstr (nrealargs+1)|])))) in c, UState.of_context_set ctx @@ -247,9 +247,9 @@ let sym_scheme_kind = (* *) (**********************************************************************) -let const_of_scheme kind env ind ctx = +let const_of_scheme kind env ind ctx = let sym_scheme, eff = (find_scheme kind ind) in - let sym, ctx = with_context_set ctx + let sym, ctx = with_context_set ctx (UnivGen.fresh_constant_instance (Global.env()) sym_scheme) in mkConstU sym, ctx, eff @@ -273,30 +273,30 @@ let build_sym_involutive_scheme env ind = name_context env ((LocalAssum (make_annot (Name varH) indr,applied_ind))::realsign) in let rci = Sorts.Relevant in (* TODO relevance *) let ci = make_case_info (Global.env()) ind rci RegularStyle in - let c = + let c = (my_it_mkLambda_or_LetIn paramsctxt (my_it_mkLambda_or_LetIn_name realsign_ind (mkCase (ci, - my_it_mkLambda_or_LetIn_name - (lift_rel_context (nrealargs+1) realsign_ind) - (mkApp (eq,[| - mkApp - (mkIndU indu, Array.concat - [Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1; - rel_vect (2*nrealargs+2) nrealargs; - rel_vect 1 nrealargs]); + my_it_mkLambda_or_LetIn_name + (lift_rel_context (nrealargs+1) realsign_ind) + (mkApp (eq,[| + mkApp + (mkIndU indu, Array.concat + [Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1; + rel_vect (2*nrealargs+2) nrealargs; + rel_vect 1 nrealargs]); mkApp (sym,Array.concat - [Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1; - rel_vect 1 nrealargs; - rel_vect (2*nrealargs+2) nrealargs; - [|mkApp (sym,Array.concat - [Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1; - rel_vect (2*nrealargs+2) nrealargs; - rel_vect 1 nrealargs; - [|mkRel 1|]])|]]); - mkRel 1|])), - mkRel 1 (* varH *), - [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|])))) + [Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1; + rel_vect 1 nrealargs; + rel_vect (2*nrealargs+2) nrealargs; + [|mkApp (sym,Array.concat + [Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1; + rel_vect (2*nrealargs+2) nrealargs; + rel_vect 1 nrealargs; + [|mkRel 1|]])|]]); + mkRel 1|])), + mkRel 1 (* varH *), + [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|])))) in (c, UState.of_context_set ctx), eff let sym_involutive_scheme_kind = @@ -405,7 +405,7 @@ let build_l2r_rew_scheme dep env ind kind = Array.concat [Context.Rel.to_extended_vect mkRel (nrealargs*3+4) paramsctxt1; rel_vect (nrealargs+4) nrealargs; rel_vect 1 nrealargs; - [|mkRel 1|]]) in + [|mkRel 1|]]) in let s, ctx' = UnivGen.fresh_sort_in_family kind in let ctx = Univ.ContextSet.union ctx ctx' in let s = mkSort s in @@ -423,20 +423,20 @@ let build_l2r_rew_scheme dep env ind kind = (if dep then [|mkRel 2|] else [||])) in let applied_sym_sym = mkApp (sym,Array.concat - [Context.Rel.to_extended_vect mkRel (2*nrealargs+4) paramsctxt1; + [Context.Rel.to_extended_vect mkRel (2*nrealargs+4) paramsctxt1; rel_vect 4 nrealargs; rel_vect (nrealargs+4) nrealargs; [|mkApp (sym,Array.concat - [Context.Rel.to_extended_vect mkRel (2*nrealargs+4) paramsctxt1; - rel_vect (nrealargs+4) nrealargs; - rel_vect 4 nrealargs; - [|mkRel 2|]])|]]) in + [Context.Rel.to_extended_vect mkRel (2*nrealargs+4) paramsctxt1; + rel_vect (nrealargs+4) nrealargs; + rel_vect 4 nrealargs; + [|mkRel 2|]])|]]) in let main_body = mkCase (ci, my_it_mkLambda_or_LetIn_name realsign_ind_G applied_PG, applied_sym_C 3, [|mkVar varHC|]) in - let c = + let c = (my_it_mkLambda_or_LetIn paramsctxt (my_it_mkLambda_or_LetIn_name realsign (mkNamedLambda (make_annot varP indr) @@ -525,11 +525,11 @@ let build_l2r_forward_rew_scheme dep env ind kind = mkApp (mkVar varP,Array.append (rel_vect (nrealargs+2) nrealargs) (if dep then [|cstr (2*nrealargs+2) (nrealargs+2)|] - else [||])) in + else [||])) in let applied_PG = mkApp (mkVar varP,Array.append (rel_vect 3 nrealargs) (if dep then [|cstr (3*nrealargs+4) 3|] else [||])) in - let c = + let c = (my_it_mkLambda_or_LetIn paramsctxt (my_it_mkLambda_or_LetIn_name realsign (mkNamedLambda (make_annot varH indr) applied_ind @@ -538,14 +538,14 @@ let build_l2r_forward_rew_scheme dep env ind kind = (lift_rel_context (nrealargs+1) realsign_ind) (mkNamedProd (make_annot varP indr) (my_it_mkProd_or_LetIn - (if dep then realsign_ind_P 2 applied_ind_P else realsign_P 2) s) + (if dep then realsign_ind_P 2 applied_ind_P else realsign_P 2) s) (mkNamedProd (make_annot varHC indr) applied_PC applied_PG)), (mkVar varH), [|mkNamedLambda (make_annot varP indr) (my_it_mkProd_or_LetIn - (if dep then realsign_ind_P 1 applied_ind_P' else realsign_P 2) s) + (if dep then realsign_ind_P 1 applied_ind_P' else realsign_P 2) s) (mkNamedLambda (make_annot varHC indr) applied_PC' - (mkVar varHC))|]))))) + (mkVar varHC))|]))))) in c, UState.of_context_set ctx (**********************************************************************) @@ -578,7 +578,7 @@ let build_l2r_forward_rew_scheme dep env ind kind = (* statement but no need for symmetry of the equality. *) (**********************************************************************) -let build_r2l_forward_rew_scheme dep env ind kind = +let build_r2l_forward_rew_scheme dep env ind kind = let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in let ((mib,mip as specif),constrargs,realsign,paramsctxt,nrealargs) = get_non_sym_eq_data env indu in @@ -603,8 +603,8 @@ let build_r2l_forward_rew_scheme dep env ind kind = let applied_PG = mkApp (mkVar varP, if dep then Context.Rel.to_extended_vect mkRel 0 realsign_ind - else Context.Rel.to_extended_vect mkRel 1 realsign) in - let c = + else Context.Rel.to_extended_vect mkRel 1 realsign) in + let c = (my_it_mkLambda_or_LetIn paramsctxt (my_it_mkLambda_or_LetIn_name realsign_ind (mkNamedLambda (make_annot varP indr) @@ -619,8 +619,8 @@ let build_r2l_forward_rew_scheme dep env ind kind = mkRel 3 (* varH *), [|mkLambda (make_annot (Name varHC) indr, - lift (nrealargs+3) applied_PC, - mkRel 1)|]), + lift (nrealargs+3) applied_PC, + mkRel 1)|]), [|mkVar varHC|])))))) in c, UState.of_context_set ctx @@ -648,14 +648,14 @@ let fix_r2l_forward_rew_scheme (c, ctx') = let ctx,_ = decompose_prod_assum t in match ctx with | hp :: p :: ind :: indargs -> - let c' = + let c' = my_it_mkLambda_or_LetIn indargs (mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 1) p) - (mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 2) hp) - (mkLambda_or_LetIn (RelDecl.map_constr (lift 2) ind) + (mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 2) hp) + (mkLambda_or_LetIn (RelDecl.map_constr (lift 2) ind) (EConstr.Unsafe.to_constr (Reductionops.whd_beta sigma - (EConstr.of_constr (applist (c, - Context.Rel.to_extended_list mkRel 3 indargs @ [mkRel 1;mkRel 3;mkRel 2])))))))) + (EConstr.of_constr (applist (c, + Context.Rel.to_extended_list mkRel 3 indargs @ [mkRel 1;mkRel 3;mkRel 2])))))))) in c', ctx' | _ -> anomaly (Pp.str "Ill-formed non-dependent left-to-right rewriting scheme.") @@ -679,7 +679,7 @@ let fix_r2l_forward_rew_scheme (c, ctx') = (* (H:I q1..qm a1..an), *) (* P b1..bn C -> P a1..an H *) (**********************************************************************) - + let build_r2l_rew_scheme dep env ind k = let sigma = Evd.from_env env in let (sigma, indu) = Evd.fresh_inductive_instance env sigma ind in @@ -772,7 +772,7 @@ let rew_r2l_scheme_kind = (* TODO: extend it to types with more than one index *) let build_congr env (eq,refl,ctx) ind = - let (ind,u as indu), ctx = with_context_set ctx + let (ind,u as indu), ctx = with_context_set ctx (UnivGen.fresh_inductive_instance env ind) in let (mib,mip) = lookup_mind_specif env ind in if not (Int.equal (Array.length mib.mind_packets) 1) || not (Int.equal (Array.length mip.mind_nf_lc) 1) then @@ -802,7 +802,7 @@ let build_congr env (eq,refl,ctx) ind = let ci = make_case_info (Global.env()) ind rci RegularStyle in let uni, ctx = Univ.extend_in_context_set (UnivGen.new_global_univ ()) ctx in let ctx = (fst ctx, Univ.enforce_leq uni (univ_of_eq env eq) (snd ctx)) in - let c = + let c = my_it_mkLambda_or_LetIn paramsctxt (mkNamedLambda (make_annot varB Sorts.Relevant) (mkType uni) (mkNamedLambda (make_annot varf Sorts.Relevant) (mkArrow (lift 1 ty) tyr (mkVar varB)) @@ -810,26 +810,26 @@ let build_congr env (eq,refl,ctx) ind = (mkNamedLambda (make_annot varH Sorts.Relevant) (applist (mkIndU indu, - Context.Rel.to_extended_list mkRel (mip.mind_nrealargs+2) paramsctxt @ - Context.Rel.to_extended_list mkRel 0 realsign)) + Context.Rel.to_extended_list mkRel (mip.mind_nrealargs+2) paramsctxt @ + Context.Rel.to_extended_list mkRel 0 realsign)) (mkCase (ci, my_it_mkLambda_or_LetIn_name - (lift_rel_context (mip.mind_nrealargs+3) realsign) + (lift_rel_context (mip.mind_nrealargs+3) realsign) (mkLambda (make_annot Anonymous Sorts.Relevant, applist (mkIndU indu, - Context.Rel.to_extended_list mkRel (2*mip.mind_nrealdecls+3) - paramsctxt - @ Context.Rel.to_extended_list mkRel 0 realsign), + Context.Rel.to_extended_list mkRel (2*mip.mind_nrealdecls+3) + paramsctxt + @ Context.Rel.to_extended_list mkRel 0 realsign), mkApp (eq, - [|mkVar varB; + [|mkVar varB; mkApp (mkVar varf, [|lift (2*mip.mind_nrealdecls+4) b|]); - mkApp (mkVar varf, [|mkRel (mip.mind_nrealargs - i + 2)|])|]))), + mkApp (mkVar varf, [|mkRel (mip.mind_nrealargs - i + 2)|])|]))), mkVar varH, [|mkApp (refl, [|mkVar varB; - mkApp (mkVar varf, [|lift (mip.mind_nrealargs+3) b|])|])|])))))) + mkApp (mkVar varf, [|lift (mip.mind_nrealargs+3) b|])|])|])))))) in c, UState.of_context_set ctx let congr_scheme_kind = declare_individual_scheme_object "_congr" diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli index b3e10013ac..fd4221f7c0 100644 --- a/tactics/eqschemes.mli +++ b/tactics/eqschemes.mli @@ -24,9 +24,9 @@ val rew_l2r_forward_dep_scheme_kind : individual scheme_kind val rew_r2l_dep_scheme_kind : individual scheme_kind val rew_r2l_scheme_kind : individual scheme_kind -val build_r2l_rew_scheme : bool -> env -> inductive -> Sorts.family -> +val build_r2l_rew_scheme : bool -> env -> inductive -> Sorts.family -> constr Evd.in_evar_universe_context -val build_l2r_rew_scheme : bool -> env -> inductive -> Sorts.family -> +val build_l2r_rew_scheme : bool -> env -> inductive -> Sorts.family -> constr Evd.in_evar_universe_context * Evd.side_effects val build_r2l_forward_rew_scheme : bool -> env -> inductive -> Sorts.family -> constr Evd.in_evar_universe_context @@ -38,12 +38,12 @@ val build_l2r_forward_rew_scheme : val build_sym_scheme : env -> inductive -> constr Evd.in_evar_universe_context val sym_scheme_kind : individual scheme_kind -val build_sym_involutive_scheme : env -> inductive -> +val build_sym_involutive_scheme : env -> inductive -> constr Evd.in_evar_universe_context * Evd.side_effects val sym_involutive_scheme_kind : individual scheme_kind (** Builds a congruence scheme for an equality type *) val congr_scheme_kind : individual scheme_kind -val build_congr : env -> constr * constr * Univ.ContextSet.t -> inductive -> +val build_congr : env -> constr * constr * Univ.ContextSet.t -> inductive -> constr Evd.in_evar_universe_context diff --git a/tactics/equality.ml b/tactics/equality.ml index 1f125a3c59..96b61b6994 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -241,7 +241,7 @@ let rewrite_keyed_unif_flags = { let rewrite_elim with_evars frzevars cls c e = Proofview.Goal.enter begin fun gl -> let flags = if Unification.is_keyed_unification () - then rewrite_keyed_unif_flags else rewrite_conv_closed_unif_flags in + then rewrite_keyed_unif_flags else rewrite_conv_closed_unif_flags in let flags = make_flags frzevars (Tacmach.New.project gl) flags c in general_elim_clause with_evars flags cls c e end @@ -366,7 +366,7 @@ let find_elim hdcncl lft2rgt dep cls ot = then let sort = elimination_sort_of_clause cls gl in let c = - match EConstr.kind sigma hdcncl with + match EConstr.kind sigma hdcncl with | Ind (ind_sp,u) -> begin match lft2rgt, cls with | Some true, None @@ -381,19 +381,19 @@ let find_elim hdcncl lft2rgt dep cls ot = try let _ = Global.lookup_constant c1' in c1' with Not_found -> - user_err ~hdr:"Equality.find_elim" + user_err ~hdr:"Equality.find_elim" (str "Cannot find rewrite principle " ++ Label.print l' ++ str ".") - end + end | _ -> begin match if is_eq then eq_elimination_ref false sort else None with | Some r -> destConstRef r | None -> destConstRef (lookup_eliminator env ind_sp sort) end end - | _ -> - (* cannot occur since we checked that we are in presence of - Logic.eq or Jmeq just before *) - assert false + | _ -> + (* cannot occur since we checked that we are in presence of + Logic.eq or Jmeq just before *) + assert false in pf_constr_of_global (GlobRef.ConstRef c) else @@ -410,9 +410,9 @@ let find_elim hdcncl lft2rgt dep cls ot = | true, _, false -> rew_r2l_forward_dep_scheme_kind in match EConstr.kind sigma hdcncl with - | Ind (ind,u) -> - - let c, eff = find_scheme scheme_name ind in + | Ind (ind,u) -> + + let c, eff = find_scheme scheme_name ind in Proofview.tclEFFECTS eff <*> pf_constr_of_global (GlobRef.ConstRef c) | _ -> assert false @@ -463,27 +463,27 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac let rels, t = decompose_prod_assum sigma (whd_betaiotazeta sigma ctype) in match match_with_equality_type env sigma t with | Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *) - let lft2rgt = adjust_rewriting_direction args lft2rgt in + let lft2rgt = adjust_rewriting_direction args lft2rgt in leibniz_rewrite_ebindings_clause cls lft2rgt tac c (it_mkProd_or_LetIn t rels) - l with_evars frzevars dep_proof_ok hdcncl + l with_evars frzevars dep_proof_ok hdcncl | None -> - Proofview.tclORELSE + Proofview.tclORELSE begin - rewrite_side_tac (Hook.get forward_general_setoid_rewrite_clause cls - lft2rgt occs (c,l) ~new_goals:[]) tac + rewrite_side_tac (Hook.get forward_general_setoid_rewrite_clause cls + lft2rgt occs (c,l) ~new_goals:[]) tac end begin function | (e, info) -> Proofview.tclEVARMAP >>= fun sigma -> - let env' = push_rel_context rels env in - let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *) + let env' = push_rel_context rels env in + let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *) match match_with_equality_type env sigma t' with - | Some (hdcncl,args) -> - let lft2rgt = adjust_rewriting_direction args lft2rgt in - leibniz_rewrite_ebindings_clause cls lft2rgt tac c - (it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars frzevars dep_proof_ok hdcncl - | None -> Proofview.tclZERO ~info e - (* error "The provided term does not end with an equality or a declared rewrite relation." *) + | Some (hdcncl,args) -> + let lft2rgt = adjust_rewriting_direction args lft2rgt in + leibniz_rewrite_ebindings_clause cls lft2rgt tac c + (it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars frzevars dep_proof_ok hdcncl + | None -> Proofview.tclZERO ~info e + (* error "The provided term does not end with an equality or a declared rewrite relation." *) end end @@ -517,44 +517,44 @@ let general_rewrite_clause l2r with_evars ?tac c cl = in match cl.onhyps with | Some l -> - (* If a precise list of locations is given, success is mandatory for - each of these locations. *) - let rec do_hyps = function - | [] -> Proofview.tclUNIT () - | ((occs,id),_) :: l -> - tclTHENFIRST - (general_rewrite_ebindings_in l2r (occs_of occs) false true ?tac id c with_evars) - (do_hyps l) - in - if cl.concl_occs == NoOccurrences then do_hyps l else - tclTHENFIRST - (general_rewrite_ebindings l2r (occs_of cl.concl_occs) false true ?tac c with_evars) + (* If a precise list of locations is given, success is mandatory for + each of these locations. *) + let rec do_hyps = function + | [] -> Proofview.tclUNIT () + | ((occs,id),_) :: l -> + tclTHENFIRST + (general_rewrite_ebindings_in l2r (occs_of occs) false true ?tac id c with_evars) + (do_hyps l) + in + if cl.concl_occs == NoOccurrences then do_hyps l else + tclTHENFIRST + (general_rewrite_ebindings l2r (occs_of cl.concl_occs) false true ?tac c with_evars) (do_hyps l) | None -> - (* Otherwise, if we are told to rewrite in all hypothesis via the + (* Otherwise, if we are told to rewrite in all hypothesis via the syntax "* |-", we fail iff all the different rewrites fail *) - let rec do_hyps_atleastonce = function - | [] -> tclZEROMSG (Pp.str"Nothing to rewrite.") - | id :: l -> + let rec do_hyps_atleastonce = function + | [] -> tclZEROMSG (Pp.str"Nothing to rewrite.") + | id :: l -> tclIFTHENFIRSTTRYELSEMUST - (general_rewrite_ebindings_in l2r AllOccurrences false true ?tac id c with_evars) - (do_hyps_atleastonce l) - in - let do_hyps = - (* If the term to rewrite uses an hypothesis H, don't rewrite in H *) - let ids gl = - let ids_in_c = Termops.global_vars_set (Proofview.Goal.env gl) (project gl) (fst c) in + (general_rewrite_ebindings_in l2r AllOccurrences false true ?tac id c with_evars) + (do_hyps_atleastonce l) + in + let do_hyps = + (* If the term to rewrite uses an hypothesis H, don't rewrite in H *) + let ids gl = + let ids_in_c = Termops.global_vars_set (Proofview.Goal.env gl) (project gl) (fst c) in let ids_of_hyps = pf_ids_of_hyps gl in - Id.Set.fold (fun id l -> List.remove Id.equal id l) ids_in_c ids_of_hyps - in + Id.Set.fold (fun id l -> List.remove Id.equal id l) ids_in_c ids_of_hyps + in Proofview.Goal.enter begin fun gl -> do_hyps_atleastonce (ids gl) end - in - if cl.concl_occs == NoOccurrences then do_hyps else + in + if cl.concl_occs == NoOccurrences then do_hyps else tclIFTHENFIRSTTRYELSEMUST - (general_rewrite_ebindings l2r (occs_of cl.concl_occs) false true ?tac c with_evars) - do_hyps + (general_rewrite_ebindings l2r (occs_of cl.concl_occs) false true ?tac c with_evars) + do_hyps let apply_special_clear_request clear_flag f = Proofview.Goal.enter begin fun gl -> @@ -615,9 +615,9 @@ let check_setoid cl = let concloccs = Locusops.occurrences_map (fun x -> x) cl.concl_occs in Option.fold_left (List.fold_left - (fun b ((occ,_),_) -> + (fun b ((occ,_),_) -> b||(not (Locusops.is_all_occurrences (Locusops.occurrences_map (fun x -> x) occ))) - ) + ) ) (not (Locusops.is_all_occurrences concloccs) && (concloccs <> NoOccurrences)) @@ -631,7 +631,7 @@ let replace_core clause l2r eq = (onLastHypId (fun id -> tclTHEN (tclTRY (general_rewrite_clause l2r false (mkVar id,NoBindings) clause)) - (clear [id]))) + (clear [id]))) (* eq,sym_eq : equality on Type and its symmetry theorem c1 c2 : c1 is to be replaced by c2 @@ -649,7 +649,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt = let get_type_of = pf_apply get_type_of gl in let t1 = get_type_of c1 and t2 = get_type_of c2 in - let evd = + let evd = if unsafe then Some (Tacmach.New.project gl) else try Some (Evarconv.unify_delay (Proofview.Goal.env gl) (Tacmach.New.project gl) t1 t2) @@ -760,37 +760,37 @@ let find_positions env sigma ~keep_proofs ~no_discr t1 t2 = | Construct ((ind1,i1 as sp1),u1), Construct (sp2,_) when Int.equal (List.length args1) (constructor_nallargs env sp1) -> - let sorts' = + let sorts' = CList.intersect Sorts.family_equal sorts (sorts_below (top_allowed_sort env (fst sp1))) in (* both sides are fully applied constructors, so either we descend, or we can discriminate here. *) - if eq_constructor sp1 sp2 then + if eq_constructor sp1 sp2 then let nparams = inductive_nparams env ind1 in - let params1,rargs1 = List.chop nparams args1 in - let _,rargs2 = List.chop nparams args2 in + let params1,rargs1 = List.chop nparams args1 in + let _,rargs2 = List.chop nparams args2 in let (mib,mip) = lookup_mind_specif env ind1 in let params1 = List.map EConstr.Unsafe.to_constr params1 in let u1 = EInstance.kind sigma u1 in let ctxt = (get_constructor ((ind1,u1),mib,mip,params1) i1).cs_args in let adjust i = CVars.adjust_rel_to_rel_context ctxt (i+1) - 1 in List.flatten - (List.map2_i (fun i -> findrec sorts' ((sp1,adjust i)::posn)) - 0 rargs1 rargs2) + (List.map2_i (fun i -> findrec sorts' ((sp1,adjust i)::posn)) + 0 rargs1 rargs2) else if List.mem_f Sorts.family_equal InType sorts' && not no_discr then (* see build_discriminator *) - raise (DiscrFound (List.rev posn,sp1,sp2)) - else + raise (DiscrFound (List.rev posn,sp1,sp2)) + else (* if we cannot eliminate to Type, we cannot discriminate but we - may still try to project *) - project env sorts posn (applist (hd1,args1)) (applist (hd2,args2)) + may still try to project *) + project env sorts posn (applist (hd1,args1)) (applist (hd2,args2)) | _ -> - let t1_0 = applist (hd1,args1) + let t1_0 = applist (hd1,args1) and t2_0 = applist (hd2,args2) in if is_conv env sigma t1_0 t2_0 then - [] + [] else - project env sorts posn t1_0 t2_0 + project env sorts posn t1_0 t2_0 in try let sorts = if keep_proofs then [InSet;InType;InProp] else [InSet;InType] in @@ -881,7 +881,7 @@ let descend_then env sigma head dirn = let IndType (indf,_) = try find_rectype env sigma (get_type_of env sigma head) with Not_found -> - user_err Pp.(str "Cannot project on an inductive type derived from a dependency.") + user_err Pp.(str "Cannot project on an inductive type derived from a dependency.") in let indp,_ = (dest_ind_family indf) in let ind, _ = check_privacy env indp in @@ -894,12 +894,12 @@ let descend_then env sigma head dirn = (fun sigma dirnval (dfltval,resty) -> let deparsign = make_arity_signature env sigma true indf in let p = - it_mkLambda_or_LetIn (lift (mip.mind_nrealargs+1) resty) deparsign in + it_mkLambda_or_LetIn (lift (mip.mind_nrealargs+1) resty) deparsign in let build_branch i = - let result = if Int.equal i dirn then dirnval else dfltval in - let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cstr.(i-1).cs_args in - let args = name_context env sigma cs_args in - it_mkLambda_or_LetIn result args in + let result = if Int.equal i dirn then dirnval else dfltval in + let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cstr.(i-1).cs_args in + let args = name_context env sigma cs_args in + it_mkLambda_or_LetIn result args in let brl = List.map build_branch (List.interval 1 (Array.length mip.mind_consnames)) in @@ -934,8 +934,8 @@ let build_selector env sigma dirn c ind special default = CP : changed assert false in a more informative error *) user_err ~hdr:"Equality.construct_discriminator" - (str "Cannot discriminate on inductive constructors with \ - dependent types.") in + (str "Cannot discriminate on inductive constructors with \ + dependent types.") in let (indp,_) = dest_ind_family indf in let ind, _ = check_privacy env indp in let typ = Retyping.get_type_of env sigma default in @@ -1055,9 +1055,9 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let env = Proofview.Goal.env gl in match find_positions env sigma ~keep_proofs:false ~no_discr:false t1 t2 with | Inr _ -> - tclZEROMSG (str"Not a discriminable equality.") + tclZEROMSG (str"Not a discriminable equality.") | Inl (cpath, (_,dirn), _) -> - discr_positions env sigma u eq_clause cpath dirn + discr_positions env sigma u eq_clause cpath dirn end let onEquality with_evars tac (c,lbindc) = @@ -1216,17 +1216,17 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in sigma, dflt with Evarconv.UnableToUnify _ -> - user_err Pp.(str "Cannot solve a unification problem.") + user_err Pp.(str "Cannot solve a unification problem.") else let (a,p_i_minus_1) = match whd_beta_stack sigma p_i with - | (_sigS,[a;p]) -> (a, p) - | _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type.") in + | (_sigS,[a;p]) -> (a, p) + | _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type.") in let sigma, ev = Evarutil.new_evar env sigma a in let rty = beta_applist sigma (p_i_minus_1,[ev]) in let sigma, tuple_tail = sigrec_clausal_form sigma (siglen-1) rty in let evopt = match EConstr.kind sigma ev with Evar _ -> None | _ -> Some ev in match evopt with - | Some w -> + | Some w -> let w_type = unsafe_type_of env sigma w in begin match Evarconv.unify_leq_delay env sigma w_type a with | sigma -> @@ -1235,14 +1235,14 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = | exception Evarconv.UnableToUnify _ -> user_err Pp.(str "Cannot solve a unification problem.") end - | None -> + | None -> (* This at least happens if what has been detected as a dependency is not one; use an evasive error message; even if the problem is upwards: unification should be tried in the first place in make_iterated_tuple instead of approximatively computing the free rels; then unsolved evars would mean not binding rel *) - user_err Pp.(str "Cannot solve a unification problem.") + user_err Pp.(str "Cannot solve a unification problem.") in let sigma = Evd.clear_metas sigma in let sigma, scf = sigrec_clausal_form sigma siglen ty in @@ -1328,7 +1328,7 @@ let rec build_injrec env sigma dflt c = function let res = kont sigma subval (dfltval,tuplety) in sigma, (res, tuplety,dfltval) with - UserError _ -> failwith "caught" + UserError _ -> failwith "caught" let build_injector env sigma dflt c cpath = let sigma, (injcode,resty,_) = build_injrec env sigma dflt c cpath in @@ -1405,8 +1405,8 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in let pf = Clenvtac.clenv_value_cast_meta inj_clause in let ty = simplify_args env sigma (clenv_type inj_clause) in - evdref := sigma; - Some (pf, ty) + evdref := sigma; + Some (pf, ty) with Failure _ -> None in let injectors = List.map_filter filter posns in @@ -1438,7 +1438,7 @@ let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause = tclZEROMSG (str"Nothing to inject.") | Inr posns -> inject_at_positions env sigma l2r u eq_clause posns - (tac (clenv_value eq_clause)) + (tac (clenv_value eq_clause)) let get_previous_hyp_position id gl = let env, sigma = Proofview.Goal.(env gl, sigma gl) in @@ -1497,11 +1497,11 @@ let decompEqThen keep_proofs ntac (lbeq,_,(t,t1,t2) as u) clause = let env = Proofview.Goal.env gl in match find_positions env sigma ~keep_proofs ~no_discr:false t1 t2 with | Inl (cpath, (_,dirn), _) -> - discr_positions env sigma u clause cpath dirn + discr_positions env sigma u clause cpath dirn | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *) ntac (clenv_value clause) 0 | Inr posns -> - inject_at_positions env sigma true u clause posns + inject_at_positions env sigma true u clause posns (ntac (clenv_value clause)) end @@ -1636,9 +1636,9 @@ let cutSubstInHyp l2r eqn id = let try_rewrite tac = Proofview.tclORELSE tac begin function (e, info) -> match e with | Constr_matching.PatternMatchingFailure -> - tclZEROMSG (str "Not a primitive equality here.") + tclZEROMSG (str "Not a primitive equality here.") | e when catchable_exception e -> - tclZEROMSG + tclZEROMSG (strbrk "Cannot find a well-typed generalization of the goal that makes the proof progress.") | e -> Proofview.tclZERO ~info e end @@ -1648,7 +1648,14 @@ let cutSubstClause l2r eqn cls = | None -> cutSubstInConcl l2r eqn | Some id -> cutSubstInHyp l2r eqn id -let cutRewriteClause l2r eqn cls = try_rewrite (cutSubstClause l2r eqn cls) +let warn_deprecated_cutrewrite = + CWarnings.create ~name:"deprecated-cutrewrite" ~category:"deprecated" + (fun () -> strbrk"\"cutrewrite\" is deprecated. See documentation for proposed replacement.") + +let cutRewriteClause l2r eqn cls = + warn_deprecated_cutrewrite (); + try_rewrite (cutSubstClause l2r eqn cls) + let cutRewriteInHyp l2r eqn id = cutRewriteClause l2r eqn (Some id) let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None @@ -1766,7 +1773,7 @@ let subst_one_var dep_proof_ok x = Context.Named.fold_outside test ~init:() hyps; user_err ~hdr:"Subst" (str "Cannot find any non-recursive equality over " ++ Id.print x ++ - str".") + str".") with FoundHyp res -> res in subst_one dep_proof_ok x res end @@ -1903,12 +1910,12 @@ let rewrite_assumption_cond cond_eq_term cl = | [] -> user_err Pp.(str "No such assumption.") | hyp ::rest -> let id = NamedDecl.get_id hyp in - begin - try + begin + try let dir = cond_eq_term (NamedDecl.get_type hyp) gl in - general_rewrite_clause dir false (mkVar id,NoBindings) cl - with | Failure _ | UserError _ -> arec rest gl - end + general_rewrite_clause dir false (mkVar id,NoBindings) cl + with | Failure _ | UserError _ -> arec rest gl + end in Proofview.Goal.enter begin fun gl -> let hyps = Proofview.Goal.hyps gl in diff --git a/tactics/equality.mli b/tactics/equality.mli index 8225195ca7..a9ccadf53a 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -57,7 +57,7 @@ val general_rewrite_bindings_in : ?tac:(unit Proofview.tactic * conditions) -> Id.t -> constr with_bindings -> evars_flag -> unit Proofview.tactic val general_rewrite_in : - orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag -> + orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag -> ?tac:(unit Proofview.tactic * conditions) -> Id.t -> constr -> evars_flag -> unit Proofview.tactic val general_rewrite_clause : diff --git a/tactics/hints.ml b/tactics/hints.ml index 131832be89..7b3797119a 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -253,9 +253,9 @@ type stored_data = int * full_hint (* First component is the index of insertion in the table, to keep most recent first semantics. *) module Bounded_net = Btermdn.Make(struct - type t = stored_data - let compare = pri_order_int - end) + type t = stored_data + let compare = pri_order_int + end) type search_entry = { sentry_nopat : stored_data list; @@ -275,18 +275,18 @@ let eq_pri_auto_tactic (_, x) (_, y) = KerName.equal x.code.uid y.code.uid let add_tac pat t st se = match pat with - | None -> + | None -> if List.exists (eq_pri_auto_tactic t) se.sentry_nopat then se else { se with sentry_nopat = List.insert pri_order t se.sentry_nopat } - | Some pat -> + | Some pat -> if List.exists (eq_pri_auto_tactic t) se.sentry_pat then se else { se with sentry_pat = List.insert pri_order t se.sentry_pat; sentry_bnet = Bounded_net.add st se.sentry_bnet (pat, t); } let rebuild_dn st se = - let dn' = - List.fold_left + let dn' = + List.fold_left (fun dn (id, t) -> Bounded_net.add (Some st) dn (Option.get t.pat, (id, t))) Bounded_net.empty se.sentry_pat in @@ -302,9 +302,9 @@ let is_transparent_gr ts = let open GlobRef in function | ConstRef cst -> TransparentState.is_transparent_constant ts cst | IndRef _ | ConstructRef _ -> false -let strip_params env sigma c = +let strip_params env sigma c = match EConstr.kind sigma c with - | App (f, args) -> + | App (f, args) -> (match EConstr.kind sigma f with | Const (cst,_) -> (match Recordops.find_primitive_projection cst with @@ -322,10 +322,10 @@ let strip_params env sigma c = let instantiate_hint env sigma p = let mk_clenv (c, cty, ctx) = let sigma = Evd.merge_context_set univ_flexible sigma ctx in - let cl = mk_clenv_from_env env sigma None (c,cty) in - {cl with templval = - { cl.templval with rebus = strip_params env sigma cl.templval.rebus }; - env = empty_env} + let cl = mk_clenv_from_env env sigma None (c,cty) in + {cl with templval = + { cl.templval with rebus = strip_params env sigma cl.templval.rebus }; + env = empty_env} in let code = match p.code.obj with | Res_pf c -> Res_pf (c, mk_clenv c) @@ -359,11 +359,11 @@ let path_matches hp hints = match hp, hints with | PathAtom _, [] -> false | PathAtom PathAny, (_ :: hints') -> k hints' - | PathAtom p, (h :: hints') -> + | PathAtom p, (h :: hints') -> if hints_path_atom_eq p h then k hints' else false - | PathStar hp', hints -> + | PathStar hp', hints -> k hints || aux hp' hints (fun hints' -> aux hp hints' k) - | PathSeq (hp, hp'), hints -> + | PathSeq (hp, hp'), hints -> aux hp hints (fun hints' -> aux hp' hints' k) | PathOr (hp, hp'), hints -> aux hp hints k || aux hp' hints k @@ -392,7 +392,7 @@ let path_seq p p' = | PathEpsilon, p' -> p' | p, PathEpsilon -> p | p, p' -> PathSeq (p, p') - + let rec path_derivate hp hint = let rec derivate_atoms hints hints' = match hints, hints' with @@ -404,7 +404,7 @@ let rec path_derivate hp hint = in match hp with | PathAtom PathAny -> PathEpsilon - | PathAtom (PathHints grs) -> + | PathAtom (PathHints grs) -> (match grs, hint with | h :: _, PathAny -> PathEmpty | hints, PathHints hints' -> derivate_atoms hints hints' @@ -412,9 +412,9 @@ let rec path_derivate hp hint = | PathStar p -> if path_matches p [hint] then hp else PathEpsilon | PathSeq (hp, hp') -> let hpder = path_derivate hp hint in - if matches_epsilon hp then + if matches_epsilon hp then PathOr (path_seq hpder hp', path_derivate hp' hint) - else if is_empty hpder then PathEmpty + else if is_empty hpder then PathEmpty else path_seq hpder hp' | PathOr (hp, hp') -> PathOr (path_derivate hp hint, path_derivate hp' hint) @@ -427,11 +427,11 @@ let rec normalize_path h = | PathSeq (PathEmpty, _) | PathSeq (_, PathEmpty) -> PathEmpty | PathSeq (PathEpsilon, p) | PathSeq (p, PathEpsilon) -> normalize_path p | PathOr (PathEmpty, p) | PathOr (p, PathEmpty) -> normalize_path p - | PathOr (p, q) -> + | PathOr (p, q) -> let p', q' = normalize_path p, normalize_path q in if hints_path_eq p p' && hints_path_eq q q' then h else normalize_path (PathOr (p', q')) - | PathSeq (p, q) -> + | PathSeq (p, q) -> let p', q' = normalize_path p, normalize_path q in if hints_path_eq p p' && hints_path_eq q q' then h else normalize_path (PathSeq (p', q')) @@ -450,13 +450,13 @@ let pp_hints_path_gen prg = | PathStar (PathAtom PathAny) -> str"_*" | PathStar p -> str "(" ++ aux p ++ str")*" | PathSeq (p, p') -> aux p ++ spc () ++ aux p' - | PathOr (p, p') -> + | PathOr (p, p') -> str "(" ++ aux p ++ spc () ++ str"|" ++ cut () ++ spc () ++ aux p' ++ str ")" | PathEmpty -> str"emp" | PathEpsilon -> str"eps" in aux - + let pp_hints_path = pp_hints_path_gen pr_global let glob_hints_path_atom p = @@ -552,18 +552,18 @@ struct { db with hintdb_max_id = succ db.hintdb_max_id }, h let empty ?name st use_dn = { hintdb_state = st; - hintdb_cut = PathEmpty; - hintdb_unfolds = (Id.Set.empty, Cset.empty); - hintdb_max_id = 0; - use_dn = use_dn; + hintdb_cut = PathEmpty; + hintdb_unfolds = (Id.Set.empty, Cset.empty); + hintdb_max_id = 0; + use_dn = use_dn; hintdb_map = GlobRef.Map.empty; - hintdb_nopat = []; - hintdb_name = name; } + hintdb_nopat = []; + hintdb_name = name; } let find key db = try GlobRef.Map.find key db.hintdb_map with Not_found -> empty_se - + let realize_tac secvars (id,tac) = if Id.Pred.subset tac.secvars secvars then Some tac else @@ -588,11 +588,11 @@ struct (try ignore(head_evar sigma arg); false with Evarutil.NoHeadEvar -> true) | ModeOutput -> true - + let matches_mode sigma args mode = Array.length mode == Array.length args && Array.for_all2 (match_mode sigma) mode args - + let matches_modes sigma args modes = if List.is_empty modes then true else List.exists (matches_mode sigma args) modes @@ -609,7 +609,7 @@ struct let map_all ~secvars k db = let se = find k db in merge_entry secvars db se.sentry_nopat se.sentry_pat - + (* Precondition: concl has no existentials *) let map_auto sigma ~secvars (k,args) concl db = let se = find k db in @@ -644,7 +644,7 @@ struct let idv = id, { v with db = db.hintdb_name } in let k = match gr with | Some gr -> if db.use_dn && is_transparent_gr db.hintdb_state gr && - is_unfold v.code.obj then None else Some gr + is_unfold v.code.obj then None else Some gr | None -> None in let dnst = if db.use_dn then Some db.hintdb_state else None in @@ -652,18 +652,18 @@ struct match k with | None -> let is_present (_, (_, v')) = KerName.equal v.code.uid v'.code.uid in - if not (List.exists is_present db.hintdb_nopat) then + if not (List.exists is_present db.hintdb_nopat) then (* FIXME *) - { db with hintdb_nopat = (gr,idv) :: db.hintdb_nopat } - else db + { db with hintdb_nopat = (gr,idv) :: db.hintdb_nopat } + else db | Some gr -> - let oval = find gr db in + let oval = find gr db in { db with hintdb_map = GlobRef.Map.add gr (add_tac pat idv dnst oval) db.hintdb_map } let rebuild_db st' db = let db' = { db with hintdb_map = GlobRef.Map.map (rebuild_dn st') db.hintdb_map; - hintdb_state = st'; hintdb_nopat = [] } + hintdb_state = st'; hintdb_nopat = [] } in List.fold_left (fun db (gr,(id,v)) -> addkv gr id v db) db' db.hintdb_nopat @@ -674,14 +674,14 @@ struct | Unfold_nth egr -> let addunf ts (ids, csts) = let open TransparentState in - match egr with + match egr with | EvalVarRef id -> { ts with tr_var = Id.Pred.add id ts.tr_var }, (Id.Set.add id ids, csts) | EvalConstRef cst -> { ts with tr_cst = Cpred.add cst ts.tr_cst }, (ids, Cset.add cst csts) - in - let state, unfs = addunf db.hintdb_state db.hintdb_unfolds in - state, { db with hintdb_unfolds = unfs }, true + in + let state, unfs = addunf db.hintdb_state db.hintdb_unfolds in + state, { db with hintdb_unfolds = unfs }, true | _ -> db.hintdb_state, db, false in let db = if db.use_dn && rebuild then rebuild_db st' db else db in @@ -807,19 +807,19 @@ let make_exact_entry env sigma info ~poly ?(name=PathAny) (c, cty, ctx) = | Prod _ -> failwith "make_exact_entry" | _ -> let pat = Patternops.pattern_of_constr env sigma (EConstr.to_constr ~abort_on_undefined_evars:false sigma cty) in - let hd = - try head_pattern_bound pat - with BoundPattern -> failwith "make_exact_entry" - in - let pri = match info.hint_priority with None -> 0 | Some p -> p in - let pat = match info.hint_pattern with - | Some pat -> snd pat - | None -> pat - in + let hd = + try head_pattern_bound pat + with BoundPattern -> failwith "make_exact_entry" + in + let pri = match info.hint_priority with None -> 0 | Some p -> p in + let pat = match info.hint_pattern with + | Some pat -> snd pat + | None -> pat + in (Some hd, - { pri; poly; pat = Some pat; name; - db = None; secvars; - code = with_uid (Give_exact (c, cty, ctx)); }) + { pri; poly; pat = Some pat; name; + db = None; secvars; + code = with_uid (Give_exact (c, cty, ctx)); }) let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) (c, cty, ctx) = let cty = if hnf then hnf_constr env sigma cty else cty in @@ -912,7 +912,7 @@ let make_resolves env sigma flags info ~poly ?name cr = user_err ~hdr:"Hint" (pr_leconstr_env env sigma c ++ spc() ++ (if pi1 flags then str"cannot be used as a hint." - else str "can be used as a hint only for eauto.")); + else str "can be used as a hint only for eauto.")); ents (* used to add an hypothesis to the local hint database *) @@ -949,9 +949,9 @@ let make_extern pri pat tacast = name = PathAny; db = None; secvars = Id.Pred.empty; (* Approximation *) - code = with_uid (Extern tacast) }) + code = with_uid (Extern tacast) }) -let make_mode ref m = +let make_mode ref m = let open Term in let ty, _ = Typeops.type_of_global_in_context (Global.env ()) ref in let ctx, t = decompose_prod ty in @@ -959,10 +959,10 @@ let make_mode ref m = let m' = Array.of_list m in if not (n == Array.length m') then user_err ~hdr:"Hint" - (pr_global ref ++ str" has " ++ int n ++ - str" arguments while the mode declares " ++ int (Array.length m')) + (pr_global ref ++ str" has " ++ int n ++ + str" arguments while the mode declares " ++ int (Array.length m')) else m' - + let make_trivial env sigma poly ?(name=PathAny) r = let c,ctx = fresh_global_or_constr env sigma poly r in let sigma = Evd.merge_context_set univ_flexible sigma ctx in @@ -970,9 +970,9 @@ let make_trivial env sigma poly ?(name=PathAny) r = let hd = head_constr sigma t in let ce = mk_clenv_from_env env sigma None (c,t) in (Some hd, { pri=1; - poly = poly; + poly = poly; pat = Some (Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma (clenv_type ce))); - name = name; + name = name; db = None; secvars = secvars_of_constr env sigma c; code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) }) @@ -1096,7 +1096,7 @@ let subst_autohint (subst, obj) = if c==c' && t'==t then data.code.obj else ERes_pf (c',t',ctx) | Give_exact (c,t,ctx) -> let c' = subst_mps subst c in - let t' = subst_mps subst t in + let t' = subst_mps subst t in if c==c' && t'== t then data.code.obj else Give_exact (c',t',ctx) | Res_pf_THEN_trivial_fail (c,t,ctx) -> let c' = subst_mps subst c in @@ -1106,8 +1106,8 @@ let subst_autohint (subst, obj) = let ref' = subst_evaluable_reference subst ref in if ref==ref' then data.code.obj else Unfold_nth ref' | Extern tac -> - let tac' = Genintern.generic_substitute subst tac in - if tac==tac' then data.code.obj else Extern tac' + let tac' = Genintern.generic_substitute subst tac in + if tac==tac' then data.code.obj else Extern tac' in let name' = subst_path_atom subst data.name in let uid' = subst_kn subst data.code.uid in @@ -1154,10 +1154,10 @@ let classify_autohint obj = let inAutoHint : hint_obj -> obj = declare_object {(default_object "AUTOHINT") with cache_function = cache_autohint; - load_function = load_autohint; - open_function = open_autohint; - subst_function = subst_autohint; - classify_function = classify_autohint; } + load_function = load_autohint; + open_function = open_autohint; + subst_function = subst_autohint; + classify_function = classify_autohint; } let make_hint ?(local = false) name action = { hint_local = local; @@ -1227,7 +1227,7 @@ let add_extern info tacast local dbname = | Some (_, pat) -> Some pat in let hint = make_hint ~local dbname - (AddHints [make_extern (Option.get info.hint_priority) pat tacast]) in + (AddHints [make_extern (Option.get info.hint_priority) pat tacast]) in Lib.add_anonymous_leaf (inAutoHint hint) let add_externs info tacast local dbnames = @@ -1258,7 +1258,7 @@ let default_prepare_hint_ident = Id.of_string "H" exception Found of constr * types -let prepare_hint check (poly,local) env init (sigma,c) = +let prepare_hint check env init (sigma,c) = let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in (* We re-abstract over uninstantiated evars and universes. It is actually a bit stupid to generalize over evars since the first @@ -1274,10 +1274,10 @@ let prepare_hint check (poly,local) env init (sigma,c) = let t = Evarutil.nf_evar sigma (existential_type sigma ev) in let t = List.fold_right (fun (e,id) c -> replace_term sigma e id c) !subst t in if not (closed0 sigma c) then - user_err Pp.(str "Hints with holes dependent on a bound variable not supported."); + user_err Pp.(str "Hints with holes dependent on a bound variable not supported."); if occur_existential sigma t then - (* Not clever enough to construct dependency graph of evars *) - user_err Pp.(str "Not clever enough to deal with evars dependent in other evars."); + (* Not clever enough to construct dependency graph of evars *) + user_err Pp.(str "Not clever enough to deal with evars dependent in other evars."); raise (Found (c,t)) | _ -> EConstr.iter sigma find_next_evar c in let rec iter c = @@ -1289,13 +1289,9 @@ let prepare_hint check (poly,local) env init (sigma,c) = mkNamedLambda (make_annot id Sorts.Relevant) t (iter (replace_term sigma evar (mkVar id) c)) in let c' = iter c in let env = Global.env () in - let empty_sigma = Evd.from_env env in - if check then Pretyping.check_evars env empty_sigma sigma c'; + if check then Pretyping.check_evars env sigma c'; let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in - if poly then IsConstr (c', diff) - else if local then IsConstr (c', diff) - else (Declare.declare_universe_context ~poly:false diff; - IsConstr (c', Univ.ContextSet.empty)) + (c', diff) let project_hint ~poly pri l2r r = let open EConstr in @@ -1338,7 +1334,12 @@ let interp_hints ~poly = let evd,c = Constrintern.interp_open_constr env sigma c in let env = Global.env () in let sigma = Evd.from_env env in - prepare_hint true (poly,false) env sigma (evd,c) in + let (c, diff) = prepare_hint true env sigma (evd,c) in + if poly then IsConstr (c, diff) + else + let () = Declare.declare_universe_context ~poly:false diff in + IsConstr (c, Univ.ContextSet.empty) + in let fref r = let gr = global_with_alias r in Dumpglob.add_glob ?loc:r.CAst.loc gr; @@ -1348,7 +1349,7 @@ let interp_hints ~poly = match c with | HintsReference c -> let gr = global_with_alias c in - (PathHints [gr], poly, IsGlobRef gr) + (PathHints [gr], poly, IsGlobRef gr) | HintsConstr c -> (PathAny, poly, f poly c) in let fp = Constrintern.intern_constr_pattern env sigma in @@ -1374,14 +1375,14 @@ let interp_hints ~poly = | HintsConstructors lqid -> let constr_hints_of_ind qid = let ind = global_inductive_with_alias qid in - let mib,_ = Global.lookup_inductive ind in + let mib,_ = Global.lookup_inductive ind in Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" (string_of_qualid qid) "ind"; List.init (nconstructors env ind) - (fun i -> let c = (ind,i+1) in + (fun i -> let c = (ind,i+1) in let gr = GlobRef.ConstructRef c in - empty_hint_info, + empty_hint_info, (Declareops.inductive_is_polymorphic mib), true, - PathHints [gr], IsGlobRef gr) + PathHints [gr], IsGlobRef gr) in HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid)) | HintsExtern (pri, patcom, tacexp) -> let pat = Option.map (fp sigma) patcom in @@ -1413,16 +1414,14 @@ let expand_constructor_hints env sigma lems = match EConstr.kind sigma lem with | Ind (ind,u) -> List.init (nconstructors env ind) - (fun i -> - let ctx = Univ.ContextSet.diff (Evd.universe_context_set evd) - (Evd.universe_context_set sigma) in - not (Univ.ContextSet.is_empty ctx), - IsConstr (mkConstructU ((ind,i+1),u),ctx)) + (fun i -> + let ctx = Univ.ContextSet.diff (Evd.universe_context_set evd) + (Evd.universe_context_set sigma) in + not (Univ.ContextSet.is_empty ctx), + IsConstr (mkConstructU ((ind,i+1),u),ctx)) | _ -> - [match prepare_hint false (false,true) env sigma (evd,lem) with - | IsConstr (c, ctx) -> - not (Univ.ContextSet.is_empty ctx), IsConstr (c, ctx) - | IsGlobRef _ -> assert false (* Impossible return value *) ]) lems + let (c, ctx) = prepare_hint false env sigma (evd,lem) in + [not (Univ.ContextSet.is_empty ctx), IsConstr (c, ctx)]) lems (* builds a hint database from a constr signature *) (* typically used with (lid, ltyp) = pf_hyps_types <some goal> *) @@ -1436,7 +1435,7 @@ let make_local_hint_db env sigma ts eapply lems = let lems = List.map map lems in let sign = EConstr.named_context env in let ts = match ts with - | None -> Hint_db.transparent_state (searchtable_map "core") + | None -> Hint_db.transparent_state (searchtable_map "core") | Some ts -> ts in let hintlist = List.map_append (make_resolve_hyp env sigma) sign in @@ -1510,19 +1509,19 @@ let pr_hint_term env sigma cl = let dbs = current_db () in let valid_dbs = let fn = try - let hdc = decompose_app_bound sigma cl in - if occur_existential sigma cl then - Hint_db.map_existential sigma ~secvars:Id.Pred.full hdc cl - else Hint_db.map_auto sigma ~secvars:Id.Pred.full hdc cl - with Bound -> Hint_db.map_none ~secvars:Id.Pred.full + let hdc = decompose_app_bound sigma cl in + if occur_existential sigma cl then + Hint_db.map_existential sigma ~secvars:Id.Pred.full hdc cl + else Hint_db.map_auto sigma ~secvars:Id.Pred.full hdc cl + with Bound -> Hint_db.map_none ~secvars:Id.Pred.full in let fn db = List.map (fun x -> 0, x) (fn db) in List.map (fun (name, db) -> (name, db, fn db)) dbs in if List.is_empty valid_dbs then - (str "No hint applicable for current goal") + (str "No hint applicable for current goal") else - (str "Applicable Hints :" ++ fnl () ++ + (str "Applicable Hints :" ++ fnl () ++ hov 0 (prlist (pr_hints_db env sigma) valid_dbs)) with Match_failure _ | Failure _ -> (str "No hint applicable for current goal") diff --git a/tactics/hints.mli b/tactics/hints.mli index 4c82a068b1..2a9b71387e 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -112,7 +112,7 @@ type 'a hints_path_gen = type pre_hints_path = Libnames.qualid hints_path_gen type hints_path = GlobRef.t hints_path_gen - + val normalize_path : hints_path -> hints_path val path_matches : hints_path -> hints_path_atom list -> bool val path_derivate : hints_path -> hints_path_atom -> hints_path @@ -139,17 +139,17 @@ module Hint_db : (** All hints associated to the reference *) val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list - (** All hints associated to the reference, respecting modes if evars appear in the - arguments, _not_ using the discrimination net. *) + (** All hints associated to the reference, respecting modes if evars appear in the + arguments, _not_ using the discrimination net. *) val map_existential : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> full_hint list - (** All hints associated to the reference, respecting modes if evars appear in the - arguments and using the discrimination net. *) + (** All hints associated to the reference, respecting modes if evars appear in the + arguments and using the discrimination net. *) val map_eauto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> full_hint list - (** All hints associated to the reference, respecting modes if evars appear in the - arguments. *) + (** All hints associated to the reference, respecting modes if evars appear in the + arguments. *) val map_auto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> full_hint list @@ -212,13 +212,12 @@ val interp_hints : poly:bool -> hints_expr -> hints_entry val add_hints : local:bool -> hint_db_name list -> hints_entry -> unit val prepare_hint : bool (* Check no remaining evars *) -> - (bool * bool) (* polymorphic or monomorphic, local or global *) -> - env -> evar_map -> evar_map * constr -> hint_term + env -> evar_map -> evar_map * constr -> (constr * Univ.ContextSet.t) (** [make_exact_entry info (c, ctyp, ctx)]. [c] is the term given as an exact proof to solve the goal; [ctyp] is the type of [c]. - [ctx] is its (refreshable) universe context. + [ctx] is its (refreshable) universe context. In info: [hint_priority] is the hint's desired priority, it is 0 if unspecified [hint_pattern] is the hint's desired pattern, it is inferred if not specified @@ -233,7 +232,7 @@ val make_exact_entry : env -> evar_map -> hint_info -> poly:bool -> ?name:hints_ products; [c] is the term given as an exact proof to solve the goal; [cty] is the type of [c]. - [ctx] is its (refreshable) universe context. + [ctx] is its (refreshable) universe context. In info: [hint_priority] is the hint's desired priority, it is computed as the number of products in [cty] if unspecified diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 61e0e41eb9..90a9a7acd9 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -49,9 +49,9 @@ let match_with_non_recursive_type env sigma t = (match EConstr.kind sigma hdapp with | Ind (ind,u) -> if (Environ.lookup_mind (fst ind) env).mind_finite == CoFinite then - Some (hdapp,args) - else - None + Some (hdapp,args) + else + None | _ -> None) | _ -> None @@ -65,7 +65,7 @@ let is_non_recursive_type env sigma t = Option.has_some (match_with_non_recursiv let rec has_nodep_prod_after n env sigma c = match EConstr.kind sigma c with | Prod (_,_,b) | LetIn (_,_,_,b) -> - ( n>0 || Vars.noccurn sigma 1 b) + ( n>0 || Vars.noccurn sigma 1 b) && (has_nodep_prod_after (n-1) env sigma b) | _ -> true @@ -100,36 +100,36 @@ let match_with_one_constructor env sigma style onlybinary allow_rec t = | Ind ind -> let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in if Int.equal (Array.length mip.mind_consnames) 1 - && (allow_rec || not (mis_is_recursive (fst ind,mib,mip))) + && (allow_rec || not (mis_is_recursive (fst ind,mib,mip))) && (Int.equal mip.mind_nrealargs 0) then - if is_strict_conjunction style (* strict conjunction *) then + if is_strict_conjunction style (* strict conjunction *) then let (ctx, _) = mip.mind_nf_lc.(0) in let ctx = List.skipn (Context.Rel.length mib.mind_params_ctxt) (List.rev ctx) in - if + if (* Constructor has a type of the form c : forall (a_0 ... a_n : Type) (x_0 : A_0) ... (x_n : A_n). T **) - List.for_all - (fun decl -> let c = RelDecl.get_type decl in - is_local_assum decl && + List.for_all + (fun decl -> let c = RelDecl.get_type decl in + is_local_assum decl && Constr.isRel c && Int.equal (Constr.destRel c) mib.mind_nparams) ctx - then - Some (hdapp,args) - else None - else + then + Some (hdapp,args) + else None + else let ctx, cty = mip.mind_nf_lc.(0) in let cty = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in let ctyp = whd_beta_prod sigma (Termops.prod_applist_assum sigma (Context.Rel.length mib.mind_params_ctxt) cty args) in - let cargs = List.map RelDecl.get_type (prod_assum sigma ctyp) in + let cargs = List.map RelDecl.get_type (prod_assum sigma ctyp) in if not (is_lax_conjunction style) || has_nodep_prod env sigma ctyp then - (* Record or non strict conjunction *) - Some (hdapp,List.rev cargs) - else - None + (* Record or non strict conjunction *) + Some (hdapp,List.rev cargs) + else + None else - None + None | _ -> None in match res with | Some (hdapp, args) when not onlybinary -> res @@ -185,10 +185,10 @@ let match_with_disjunction ?(strict=false) ?(onlybinary=false) env sigma t = then if strict then if test_strict_disjunction (mib, mip) then - Some (hdapp,args) - else - None - else + Some (hdapp,args) + else + None + else let map (ctx, cty) = let ar = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in pi2 (destProd sigma (prod_applist sigma ar args)) @@ -196,7 +196,7 @@ let match_with_disjunction ?(strict=false) ?(onlybinary=false) env sigma t = let cargs = Array.map map mip.mind_nf_lc in Some (hdapp,Array.to_list cargs) else - None + None | _ -> None in match res with | Some (hdapp,args) when not onlybinary -> res @@ -215,7 +215,7 @@ let match_with_empty_type env sigma t = | Ind (ind, _) -> let (mib,mip) = Inductive.lookup_mind_specif env ind in let nconstr = Array.length mip.mind_consnames in - if Int.equal nconstr 0 then Some hdapp else None + if Int.equal nconstr 0 then Some hdapp else None | _ -> None let is_empty_type env sigma t = Option.has_some (match_with_empty_type env sigma t) @@ -230,9 +230,9 @@ let match_with_unit_or_eq_type env sigma t = let (mib,mip) = Inductive.lookup_mind_specif env ind in let nconstr = Array.length mip.mind_consnames in if Int.equal nconstr 1 && Int.equal mip.mind_consnrealargs.(0) 0 then - Some hdapp - else - None + Some hdapp + else + None | _ -> None let is_unit_or_eq_type env sigma t = Option.has_some (match_with_unit_or_eq_type env sigma t) @@ -307,16 +307,16 @@ let match_with_equation env sigma t = let (mib,mip) = Global.lookup_inductive ind in let constr_types = mip.mind_nf_lc in let nconstr = Array.length mip.mind_consnames in - if Int.equal nconstr 1 then + if Int.equal nconstr 1 then let (ctx, cty) = constr_types.(0) in let cty = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in if is_matching env sigma coq_refl_leibniz1_pattern cty then - None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1)) + None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1)) else if is_matching env sigma coq_refl_leibniz2_pattern cty then - None, hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) + None, hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) else if is_matching env sigma coq_refl_jm_pattern cty then - None, hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3)) - else raise NoEquationFound + None, hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3)) + else raise NoEquationFound else raise NoEquationFound | _ -> raise NoEquationFound @@ -485,7 +485,7 @@ let match_sigma env sigma ex = | App (f, [| a; p; car; cdr |]) when Termops.is_global sigma (lib_ref "core.sigT.intro") f -> build_sigma_type (), (snd (destConstruct sigma f), a, p, car, cdr) | _ -> raise PatternMatchingFailure - + let find_sigma_data_decompose env ex = (* fails with PatternMatchingFailure *) match_sigma env ex diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 5ff257fbfe..803305a1ca 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -120,7 +120,7 @@ val match_with_equation: (***** Destructing patterns bound to some theory *) -(** Match terms [eq A t u], [identity A t u] or [JMeq A t A u] +(** Match terms [eq A t u], [identity A t u] or [JMeq A t A u] Returns associated lemmas and [A,t,u] or fails PatternMatchingFailure *) val find_eq_data_decompose : Proofview.Goal.t -> constr -> coq_eq_data * EInstance.t * (types * constr * constr) @@ -132,7 +132,7 @@ val find_this_eq_data_decompose : Proofview.Goal.t -> constr -> (** A variant that returns more informative structure on the equality found *) val find_eq_data : evar_map -> constr -> coq_eq_data * EInstance.t * equation_kind -(** Match a term of the form [(existT A P t p)] +(** Match a term of the form [(existT A P t p)] Returns associated lemmas and [A,P,t,p] *) val find_sigma_data_decompose : Environ.env -> evar_map -> constr -> coq_sigma_data * (EInstance.t * constr * constr * constr * constr) diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 3f824a94bf..517ccfaf53 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -15,8 +15,6 @@ declaring schemes and generating schemes on demand *) open Names -open Mod_subst -open Libobject open Nameops open Declarations open Constr @@ -40,33 +38,8 @@ type individual_scheme_object_function = type 'a scheme_kind = string -let scheme_map = Summary.ref Indmap.empty ~name:"Schemes" - let pr_scheme_kind = Pp.str -let cache_one_scheme kind (ind,const) = - let map = try Indmap.find ind !scheme_map with Not_found -> String.Map.empty in - scheme_map := Indmap.add ind (String.Map.add kind const map) !scheme_map - -let cache_scheme (_,(kind,l)) = - Array.iter (cache_one_scheme kind) l - -let subst_one_scheme subst (ind,const) = - (* Remark: const is a def: the result of substitution is a constant *) - (subst_ind subst ind,subst_constant subst const) - -let subst_scheme (subst,(kind,l)) = - (kind,Array.Smart.map (subst_one_scheme subst) l) - -let discharge_scheme (_,(kind,l)) = - Some (kind, l) - -let inScheme : string * (inductive * Constant.t) array -> obj = - declare_object @@ superglobal_object "SCHEME" - ~cache:cache_scheme - ~subst:(Some subst_scheme) - ~discharge:discharge_scheme - (**********************************************************************) (* The table of scheme building functions *) @@ -104,41 +77,23 @@ let declare_individual_scheme_object s ?(aux="") f = (**********************************************************************) (* Defining/retrieving schemes *) -let declare_scheme kind indcl = - Lib.add_anonymous_leaf (inScheme (kind,indcl)) - -let () = Declare.set_declare_scheme declare_scheme - let is_visible_name id = try ignore (Nametab.locate (Libnames.qualid_of_ident id)); true with Not_found -> false let compute_name internal id = - match internal with - | UserAutomaticRequest | UserIndividualRequest -> id - | InternalTacticRequest -> - Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name + if internal then + Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name + else id let define internal role id c poly univs = let id = compute_name internal id in let ctx = UState.minimize univs in let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in let univs = UState.univ_entry ~poly ctx in - let entry = { - Declare.proof_entry_body = - Future.from_val ((c,Univ.ContextSet.empty), ()); - proof_entry_secctx = None; - proof_entry_type = None; - proof_entry_universes = univs; - proof_entry_opaque = false; - proof_entry_inline_code = false; - proof_entry_feedback = None; - } in + let entry = Declare.pure_definition_entry ~univs c in let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id entry in - let () = match internal with - | InternalTacticRequest -> () - | _-> Declare.definition_message id - in + let () = if internal then () else Declare.definition_message id in kn, eff let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = @@ -148,8 +103,9 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = | Some id -> id | None -> add_suffix mib.mind_packets.(i).mind_typename suff in let role = Evd.Schema (ind, kind) in - let const, neff = define mode role id c (Declareops.inductive_is_polymorphic mib) ctx in - declare_scheme kind [|ind,const|]; + let internal = mode == InternalTacticRequest in + let const, neff = define internal role id c (Declareops.inductive_is_polymorphic mib) ctx in + DeclareScheme.declare_scheme kind [|ind,const|]; const, Evd.concat_side_effects neff eff let define_individual_scheme kind mode names (mind,i as ind) = @@ -166,12 +122,13 @@ let define_mutual_scheme_base kind suff f mode names mind = with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in let fold i effs id cl = let role = Evd.Schema ((mind, i), kind)in - let cst, neff = define mode role id cl (Declareops.inductive_is_polymorphic mib) ctx in + let internal = mode == InternalTacticRequest in + let cst, neff = define internal role id cl (Declareops.inductive_is_polymorphic mib) ctx in (Evd.concat_side_effects neff effs, cst) in let (eff, consts) = Array.fold_left2_map_i fold eff ids cl in let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in - declare_scheme kind schemes; + DeclareScheme.declare_scheme kind schemes; consts, eff let define_mutual_scheme kind mode names mind = @@ -181,7 +138,7 @@ let define_mutual_scheme kind mode names mind = define_mutual_scheme_base kind s f mode names mind let find_scheme_on_env_too kind ind = - let s = String.Map.find kind (Indmap.find ind !scheme_map) in + let s = DeclareScheme.lookup_scheme kind ind in s, Evd.empty_side_effects let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) = @@ -194,6 +151,14 @@ let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) = let ca, eff = define_mutual_scheme_base kind s f mode [] mind in ca.(i), eff +let define_individual_scheme kind mode names ind = + ignore (define_individual_scheme kind mode names ind) + +let define_mutual_scheme kind mode names mind = + ignore (define_mutual_scheme kind mode names mind) + let check_scheme kind ind = try let _ = find_scheme_on_env_too kind ind in true with Not_found -> false + +let lookup_scheme = DeclareScheme.lookup_scheme diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli index 17e9c7ef42..d886fb67d3 100644 --- a/tactics/ind_tables.mli +++ b/tactics/ind_tables.mli @@ -30,7 +30,9 @@ type mutual_scheme_object_function = type individual_scheme_object_function = internal_flag -> inductive -> constr Evd.in_evar_universe_context * Evd.side_effects -(** Main functions to register a scheme builder *) +(** Main functions to register a scheme builder. Note these functions + are not safe to be used by plugins as their effects won't be undone + on backtracking *) val declare_mutual_scheme_object : string -> ?aux:string -> mutual_scheme_object_function -> mutual scheme_kind @@ -41,17 +43,19 @@ val declare_individual_scheme_object : string -> ?aux:string -> (** Force generation of a (mutually) scheme with possibly user-level names *) -val define_individual_scheme : individual scheme_kind -> +val define_individual_scheme : individual scheme_kind -> internal_flag (** internal *) -> - Id.t option -> inductive -> Constant.t * Evd.side_effects + Id.t option -> inductive -> unit val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) -> - (int * Id.t) list -> MutInd.t -> Constant.t array * Evd.side_effects + (int * Id.t) list -> MutInd.t -> unit (** Main function to retrieve a scheme in the cache or to generate it *) val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> Constant.t * Evd.side_effects val check_scheme : 'a scheme_kind -> inductive -> bool +(** Like [find_scheme] but fails when the scheme is not already in the cache *) +val lookup_scheme : 'a scheme_kind -> inductive -> Constant.t val pr_scheme_kind : 'a scheme_kind -> Pp.t diff --git a/tactics/inv.ml b/tactics/inv.ml index 49d0428a6f..be0421d42d 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -84,30 +84,30 @@ let make_inv_predicate env evd indf realargs id status concl = let (hyps,concl) = match status with | NoDep -> - (* We push the arity and leave concl unchanged *) - let hyps_arity,_ = get_arity env indf in - let hyps_arity = List.map (fun d -> map_rel_decl EConstr.of_constr d) hyps_arity in - (hyps_arity,concl) + (* We push the arity and leave concl unchanged *) + let hyps_arity,_ = get_arity env indf in + let hyps_arity = List.map (fun d -> map_rel_decl EConstr.of_constr d) hyps_arity in + (hyps_arity,concl) | Dep dflt_concl -> - if not (occur_var env !evd id concl) then - user_err ~hdr:"make_inv_predicate" + if not (occur_var env !evd id concl) then + user_err ~hdr:"make_inv_predicate" (str "Current goal does not depend on " ++ Id.print id ++ str"."); (* We abstract the conclusion of goal with respect to realargs and c to * be concl in order to rewrite and have c also rewritten when the case * will be done *) - let pred = + let pred = match dflt_concl with | Some concl -> concl (*assumed it's some [x1..xn,H:I(x1..xn)]C*) | None -> - let sort = get_sort_family_of env !evd concl in + let sort = get_sort_family_of env !evd concl in let sort = evd_comb1 Evd.fresh_sort_in_family evd sort in - let p = make_arity env !evd true indf sort in - let evd',(p,ptyp) = Unification.abstract_list_all env + let p = make_arity env !evd true indf sort in + let evd',(p,ptyp) = Unification.abstract_list_all env !evd p concl (realargs@[mkVar id]) - in evd := evd'; p in - let hyps,bodypred = decompose_lam_n_assum !evd (nrealargs+1) pred in - (* We lift to make room for the equations *) - (hyps,lift nrealargs bodypred) + in evd := evd'; p in + let hyps,bodypred = decompose_lam_n_assum !evd (nrealargs+1) pred in + (* We lift to make room for the equations *) + (hyps,lift nrealargs bodypred) in let nhyps = Context.Rel.length hyps in let env' = push_rel_context hyps env in @@ -124,11 +124,11 @@ let make_inv_predicate env evd indf realargs id status concl = let (xi, ti) = compute_eqn env' !evd nhyps n ai in let (lhs,eqnty,rhs) = if closed0 !evd ti then - (xi,ti,ai) + (xi,ti,ai) else - let sigma, res = make_iterated_tuple env' !evd ai (xi,ti) in - evd := sigma; res - in + let sigma, res = make_iterated_tuple env' !evd ai (xi,ti) in + evd := sigma; res + in let eq_term = eqdata.Coqlib.eq in let eq = evd_comb1 (Evd.fresh_global env) evd eq_term in let eqn = applist (eq,[eqnty;lhs;rhs]) in @@ -195,9 +195,9 @@ let dependent_hyps env id idlist gl = let rec dep_rec =function | [] -> [] | d::l -> - (* Update the type of id1: it may have been subject to rewriting *) - let d = pf_get_hyp (NamedDecl.get_id d) gl in - if occur_var_in_decl env (project gl) id d + (* Update the type of id1: it may have been subject to rewriting *) + let d = pf_get_hyp (NamedDecl.get_id d) gl in + if occur_var_in_decl env (project gl) id d then d :: dep_rec l else dep_rec l in @@ -380,14 +380,14 @@ let projectAndApply as_mode thin avoid id eqname names depids = tclTHENLIST [if as_mode then clear [id] else tclIDTAC; (tclMAP_i (false,false) neqns (function (idopt,_) -> - tclTRY (tclTHEN + tclTRY (tclTHEN (intro_move_avoid idopt avoid Logic.MoveLast) - (* try again to substitute and if still not a variable after *) - (* decomposition, arbitrarily try to rewrite RL !? *) - (tclTRY (onLastHypId (substHypIfVariable (fun id -> subst_hyp false id)))))) - names); + (* try again to substitute and if still not a variable after *) + (* decomposition, arbitrarily try to rewrite RL !? *) + (tclTRY (onLastHypId (substHypIfVariable (fun id -> subst_hyp false id)))))) + names); (if as_mode then tclIDTAC else clear [id])] - (* Doing the above late breaks the computation of dids in + (* Doing the above late breaks the computation of dids in generalizeRewriteIntros, and hence breaks proper intros_replacing but it is needed for compatibility *) in @@ -396,7 +396,7 @@ let projectAndApply as_mode thin avoid id eqname names depids = (* and apply a trailer which again try to substitute *) (fun id -> dEqThen ~keep_proofs:None false (deq_trailer id) - (Some (None,ElimOnConstr (EConstr.mkVar id,NoBindings)))) + (Some (None,ElimOnConstr (EConstr.mkVar id,NoBindings)))) id let nLastDecls i tac = @@ -420,17 +420,17 @@ let rewrite_equations as_mode othin neqns names ba = clear (ids_of_named_context nodepids); (nLastDecls neqns (fun ctx -> bring_hyps (List.rev ctx))); (nLastDecls neqns (fun ctx -> clear (ids_of_named_context ctx))); - tclMAP_i (true,false) neqns (fun (idopt,names) -> + tclMAP_i (true,false) neqns (fun (idopt,names) -> (tclTHEN (intro_move_avoid idopt avoid Logic.MoveLast) - (onLastHypId (fun id -> - tclTRY (projectAndApply as_mode thin avoid id first_eq names depids))))) - names; - tclMAP (fun d -> tclIDTAC >>= fun () -> (* delay for [first_eq]. *) + (onLastHypId (fun id -> + tclTRY (projectAndApply as_mode thin avoid id first_eq names depids))))) + names; + tclMAP (fun d -> tclIDTAC >>= fun () -> (* delay for [first_eq]. *) let idopt = if as_mode then Some (NamedDecl.get_id d) else None in intro_move idopt (if thin then Logic.MoveLast else !first_eq)) - nodepids; - (tclMAP (fun d -> tclTRY (clear [NamedDecl.get_id d])) depids)] + nodepids; + (tclMAP (fun d -> tclTRY (clear [NamedDecl.get_id d])) depids)] | None -> (* simple inversion *) if as_mode then @@ -505,10 +505,10 @@ let wrap_inv_error id = function (e, info) -> match e with Proofview.tclENV >>= fun env -> Proofview.tclEVARMAP >>= fun sigma -> tclZEROMSG ( - (strbrk "Inversion would require case analysis on sort " ++ + (strbrk "Inversion would require case analysis on sort " ++ pr_sort sigma k ++ - strbrk " which is not allowed for inductive definition " ++ - pr_inductive env (fst i) ++ str ".")) + strbrk " which is not allowed for inductive definition " ++ + pr_inductive env (fst i) ++ str ".")) | e -> Proofview.tclZERO ~info e (* The most general inversion tactic *) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 2af3947dd1..cf58c9306c 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -105,11 +105,11 @@ let max_prefix_sign lid sign = let rec max_rec (resid,prefix) = function | [] -> (resid,prefix) | (id::l) -> - let pre = sign_prefix id sign in - if sign_length pre > sign_length prefix then + let pre = sign_prefix id sign in + if sign_length pre > sign_length prefix then max_rec (id,pre) l else - max_rec (resid,prefix) l + max_rec (resid,prefix) l in match lid with | [] -> nil_sign @@ -119,11 +119,11 @@ let rec add_prods_sign env sigma t = match EConstr.kind sigma (whd_all env sigma t) with | Prod (na,c1,b) -> let id = id_of_name_using_hdchar env sigma t na.binder_name in - let b'= subst1 (mkVar id) b in + let b'= subst1 (mkVar id) b in add_prods_sign (push_named (LocalAssum ({na with binder_name=id},c1)) env) sigma b' | LetIn (na,c1,t1,b) -> let id = id_of_name_using_hdchar env sigma t na.binder_name in - let b'= subst1 (mkVar id) b in + let b'= subst1 (mkVar id) b in add_prods_sign (push_named (LocalDef ({na with binder_name=id},c1,t1)) env) sigma b' | _ -> (env,t) @@ -149,7 +149,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option = let pty = make_arity env sigma true indf sort in let r = relevance_of_inductive_type env ind in let goal = - mkProd + mkProd (make_annot Anonymous r, mkAppliedInd ind, applist(mkVar p,realargs@[mkRel 1])) in pty,goal @@ -157,14 +157,14 @@ let compute_first_inversion_scheme env sigma ind sort dep_option = let i = mkAppliedInd ind in let ivars = global_vars env sigma i in let revargs,ownsign = - fold_named_context - (fun env d (revargs,hyps) -> + fold_named_context + (fun env d (revargs,hyps) -> let d = map_named_decl EConstr.of_constr d in let id = NamedDecl.get_id d in if Id.List.mem id ivars then - ((mkVar id)::revargs, Context.Named.add d hyps) - else - (revargs,hyps)) + ((mkVar id)::revargs, Context.Named.add d hyps) + else + (revargs,hyps)) env ~init:([],[]) in let pty = it_mkNamedProd_or_LetIn (mkSort sort) ownsign in @@ -209,7 +209,7 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op = (fun env d sign -> let d = map_named_decl EConstr.of_constr d in if mem_named_context_val (NamedDecl.get_id d) global_named_context then sign - else Context.Named.add d sign) + else Context.Named.add d sign) invEnv ~init:Context.Named.empty end in let avoid = ref Id.Set.empty in @@ -218,11 +218,11 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op = let rec fill_holes c = match EConstr.kind sigma c with | Evar (e,args) -> - let h = next_ident_away (Id.of_string "H") !avoid in - let ty,inst = Evarutil.generalize_evar_over_rels sigma (e,args) in - avoid := Id.Set.add h !avoid; + let h = next_ident_away (Id.of_string "H") !avoid in + let ty,inst = Evarutil.generalize_evar_over_rels sigma (e,args) in + avoid := Id.Set.add h !avoid; ownSign := Context.Named.add (LocalAssum (make_annot h Sorts.Relevant,ty)) !ownSign; - applist (mkVar h, inst) + applist (mkVar h, inst) | _ -> EConstr.map sigma fill_holes c in let c = fill_holes pfterm in @@ -250,7 +250,7 @@ let add_inversion_lemma_exn ~poly na com comsort 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 + user_err ~hdr:"Inv needs Nodep Prop Set" s (* ================================= *) (* Applying a given inversion lemma *) @@ -264,12 +264,12 @@ let lemInv id c = Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false with | NoSuchBinding -> - user_err - (hov 0 (pr_econstr_env (pf_env gls) (project gls) c ++ spc () ++ str "does not refer to an inversion lemma.")) + user_err + (hov 0 (pr_econstr_env (pf_env gls) (project gls) c ++ spc () ++ str "does not refer to an inversion lemma.")) | UserError (a,b) -> - user_err ~hdr:"LemInv" - (str "Cannot refine current goal with the lemma " ++ - pr_leconstr_env (pf_env gls) (project gls) c) + user_err ~hdr:"LemInv" + (str "Cannot refine current goal with the lemma " ++ + pr_leconstr_env (pf_env gls) (project gls) c) end let lemInv_gen id c = try_intros_until (fun id -> lemInv id c) id diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml index 413c6540a3..3c9803432a 100644 --- a/tactics/pfedit.ml +++ b/tactics/pfedit.ml @@ -55,8 +55,7 @@ let get_current_goal_context pf = let env = Global.env () in Evd.from_env env, env -let get_current_context pf = - let p = Proof_global.get_proof pf in +let get_proof_context p = try get_goal_context_gen p 1 with | NoSuchGoal -> @@ -64,6 +63,10 @@ let get_current_context pf = let { Proof.sigma } = Proof.data p in sigma, Global.env () +let get_current_context pf = + let p = Proof_global.get_proof pf in + get_proof_context p + let solve ?with_end_tac gi info_lvl tac pr = let tac = match with_end_tac with | None -> tac @@ -114,14 +117,14 @@ let by tac = Proof_global.map_fold_proof (solve (Goal_select.SelectNth 1) None t let next = let n = ref 0 in fun () -> incr n; !n -let build_constant_by_tactic ~name ctx sign ~poly typ tac = +let build_constant_by_tactic ~name ?(opaque=Proof_global.Transparent) ctx sign ~poly typ tac = let evd = Evd.from_ctx ctx in let goals = [ (Global.env_of_context sign , typ) ] in let pf = Proof_global.start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in try let pf, status = by tac pf in let open Proof_global in - let { entries; universes } = close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pf in + let { entries; universes } = close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pf in match entries with | [entry] -> entry, status, universes @@ -135,12 +138,13 @@ let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac = let name = Id.of_string ("temporary_proof"^string_of_int (next())) in let sign = val_of_named_context (named_context env) in let ce, status, univs = build_constant_by_tactic ~name sigma sign ~poly typ tac in - let body, eff = Future.force ce.Declare.proof_entry_body in - let (cb, ctx) = - if side_eff then Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) - else body + let cb, univs = + if side_eff then Declare.inline_private_constants ~univs env ce + else + (* GG: side effects won't get reset: no need to treat their universes specially *) + let (cb, ctx), _eff = Future.force ce.Declare.proof_entry_body in + cb, UState.merge ~sideff:false Evd.univ_rigid univs ctx in - let univs = UState.merge ~sideff:side_eff Evd.univ_rigid univs ctx in cb, status, univs let refine_by_tactic ~name ~poly env sigma ty tac = diff --git a/tactics/pfedit.mli b/tactics/pfedit.mli index 30514191fa..a2e742c0d7 100644 --- a/tactics/pfedit.mli +++ b/tactics/pfedit.mli @@ -27,6 +27,10 @@ val get_goal_context : Proof_global.t -> int -> Evd.evar_map * env (** [get_current_goal_context ()] works as [get_goal_context 1] *) val get_current_goal_context : Proof_global.t -> Evd.evar_map * env +(** [get_proof_context ()] gets the goal context for the first subgoal + of the proof *) +val get_proof_context : Proof.t -> Evd.evar_map * env + (** [get_current_context ()] returns the context of the current focused goal. If there is no focused goal but there is a proof in progress, it returns the corresponding evar_map. @@ -59,6 +63,7 @@ val use_unification_heuristics : unit -> bool val build_constant_by_tactic : name:Id.t + -> ?opaque:Proof_global.opacity_flag -> UState.t -> named_context_val -> poly:bool diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml index b723922642..b1fd34e43c 100644 --- a/tactics/proof_global.ml +++ b/tactics/proof_global.ml @@ -238,18 +238,10 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now let t = EConstr.Unsafe.to_constr t in let univstyp, body = make_body t p in let univs, typ = Future.force univstyp in - let open Declare in - { - proof_entry_body = body; - proof_entry_secctx = section_vars; - proof_entry_feedback = feedback_id; - proof_entry_type = Some typ; - proof_entry_inline_code = false; - proof_entry_opaque = opaque; - proof_entry_universes = univs; } + Declare.delayed_definition_entry ~opaque ?feedback_id ?section_vars ~univs ~types:typ body in - let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in - { name; entries = entries; poly; universes; udecl } + let entries = Future.map2 entry_fn fpl (Proofview.initial_goals entry) in + { name; entries; poly; universes; udecl } let return_proof ?(allow_partial=false) ps = let { proof } = ps in diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli index b9d1b37a11..9161eae82f 100644 --- a/tactics/proof_global.mli +++ b/tactics/proof_global.mli @@ -79,7 +79,7 @@ val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future. * Both access the current proof state. The former is supposed to be * chained with a computation that completed the proof *) -type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t +type closed_proof_output (* If allow_partial is set (default no) then an incomplete proof * is allowed (no error), and a warn is given if the proof is complete. *) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index b93c4a176f..ed7ab9164a 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -166,7 +166,7 @@ let check_or_and_pattern_size ?loc check_and names branchsigns = user_err ?loc (str "Expects " ++ msg p1 p2 ++ str ".") in let errn n = user_err ?loc (str "Expects a disjunctive pattern with " ++ int n - ++ str " branches.") in + ++ str " branches.") in let err1' p1 p2 = user_err ?loc (strbrk "Expects a disjunctive pattern with 1 branch or " ++ msg p1 p2 ++ str ".") in let errforthcoming ?loc = @@ -246,7 +246,7 @@ let elimination_sort_of_clause = function | Some id -> elimination_sort_of_hyp id -let pf_with_evars glsev k gls = +let pf_with_evars glsev k gls = let evd, a = glsev gls in tclTHEN (Refiner.tclEVARS evd) (k a) gls @@ -411,7 +411,7 @@ module New = struct let tclTRY t = tclORELSE0 t (tclUNIT ()) - + let tclTRYb t = tclORELSE0L (t <*> tclUNIT true) (tclUNIT false) @@ -498,7 +498,7 @@ module New = struct | Evd.Evar_empty -> Some (evk,evi) | Evd.Evar_defined c -> match Constr.kind (EConstr.Unsafe.to_constr c) with | Evar (evk,l) -> is_undefined_up_to_restriction sigma evk - | _ -> + | _ -> (* We make the assumption that there is no way to refine an evar remaining after typing from the initial term given to apply/elim and co tactics, is it correct? *) @@ -567,11 +567,11 @@ module New = struct let nthHypId m gl = (* We only use [id] *) nthDecl m gl |> NamedDecl.get_id - let nthHyp m gl = + let nthHyp m gl = mkVar (nthHypId m gl) let onNthHypId m tac = - Proofview.Goal.enter begin fun gl -> tac (nthHypId m gl) end + Proofview.Goal.enter begin fun gl -> tac (nthHypId m gl) end let onNthHyp m tac = Proofview.Goal.enter begin fun gl -> tac (nthHyp m gl) end @@ -644,12 +644,12 @@ module New = struct match EConstr.kind elimclause.evd p with | Meta p -> p | _ -> - let name_elim = - match EConstr.kind sigma elim with + let name_elim = + match EConstr.kind sigma elim with | Const _ | Var _ -> str " " ++ Printer.pr_econstr_env (pf_env gl) sigma elim | _ -> mt () - in - user_err ~hdr:"Tacticals.general_elim_then_using" + in + user_err ~hdr:"Tacticals.general_elim_then_using" (str "The elimination combinator " ++ name_elim ++ str " is unknown.") in let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in @@ -733,7 +733,7 @@ module New = struct tac branches end - let case_on_ba tac ba = + let case_on_ba tac ba = Proofview.Goal.enter begin fun gl -> let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in tac branches diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index c6aef6a554..31d26834d6 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -68,7 +68,7 @@ val afterHyp : Id.t -> Goal.goal sigma -> named_context val ifOnHyp : (Id.t * types -> bool) -> (Id.t -> tactic) -> (Id.t -> tactic) -> - Id.t -> tactic + Id.t -> tactic val onHyps : (Goal.goal sigma -> named_context) -> (named_context -> tactic) -> tactic @@ -109,7 +109,7 @@ val get_and_check_or_and_pattern : bool list array -> intro_patterns array (** Tolerate "[]" to mean a disjunctive pattern of any length *) -val fix_empty_or_and_pattern : int -> +val fix_empty_or_and_pattern : int -> delayed_open_constr or_and_intro_pattern_expr -> delayed_open_constr or_and_intro_pattern_expr diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 6fd18b83d1..9258a75461 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -446,7 +446,7 @@ let internal_cut_gen ?(check=true) dir replace id t = sign',t,concl,sigma else (if check && mem_named_context_val id sign then - user_err (str "Variable " ++ Id.print id ++ str " is already declared."); + user_err (str "Variable " ++ Id.print id ++ str " is already declared."); push_named_context_val (LocalAssum (make_annot id r,t)) sign,t,concl,sigma) in let nf_t = nf_betaiota env sigma t in Proofview.tclTHEN @@ -660,24 +660,24 @@ let bind_red_expr_occurrences occs nbcl redexp = else match redexp with | Unfold (_::_::_) -> - error_illegal_clause () + error_illegal_clause () | Unfold [(occl,c)] -> - if occl != AllOccurrences then - error_illegal_clause () - else - Unfold [(occs,c)] + if occl != AllOccurrences then + error_illegal_clause () + else + Unfold [(occs,c)] | Pattern (_::_::_) -> - error_illegal_clause () + error_illegal_clause () | Pattern [(occl,c)] -> - if occl != AllOccurrences then - error_illegal_clause () - else - Pattern [(occs,c)] + if occl != AllOccurrences then + error_illegal_clause () + else + Pattern [(occs,c)] | Simpl (f,Some (occl,c)) -> - if occl != AllOccurrences then - error_illegal_clause () - else - Simpl (f,Some (occs,c)) + if occl != AllOccurrences then + error_illegal_clause () + else + Simpl (f,Some (occs,c)) | CbvVm (Some (occl,c)) -> if occl != AllOccurrences then error_illegal_clause () @@ -690,9 +690,9 @@ let bind_red_expr_occurrences occs nbcl redexp = CbvNative (Some (occs,c)) | Red _ | Hnf | Cbv _ | Lazy _ | Cbn _ | ExtraRedExpr _ | Fold _ | Simpl (_,None) | CbvVm None | CbvNative None -> - error_occurrences_not_unsupported () + error_occurrences_not_unsupported () | Unfold [] | Pattern [] -> - assert false + assert false (* The following two tactics apply an arbitrary reduction function either to the conclusion or to a @@ -809,7 +809,7 @@ let check_types env sigma mayneedglobalcheck deep newc origc = if deep then begin let t2 = Retyping.get_type_of env sigma origc in let sigma, t2 = Evarsolve.refresh_universes - ~onlyalg:true (Some false) env sigma t2 in + ~onlyalg:true (Some false) env sigma t2 in match infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 with | None -> if @@ -891,7 +891,7 @@ let change ~check chg c cls = e_change_in_hyps ~check:false ~reorder f hyps end -let change_concl t = +let change_concl t = change_in_concl ~check:true None (make_change_arg t) (* Pour usage interne (le niveau User est pris en compte par reduce) *) @@ -934,7 +934,7 @@ let is_local_unfold env flags = let reduce redexp cl = let trace env sigma = let open Printer in - let pr = (pr_econstr_env, pr_leconstr_env, pr_evaluable_reference, pr_constr_pattern_env) in + let pr = ((fun e -> pr_econstr_env e), (fun e -> pr_leconstr_env e), pr_evaluable_reference, pr_constr_pattern_env) in Pp.(hov 2 (Ppred.pr_red_expr_env env sigma pr str redexp)) in Proofview.Trace.name_tactic trace begin @@ -999,7 +999,7 @@ let find_intro_names ctxt gl = let build_intro_tac id dest tac = match dest with | MoveLast -> Tacticals.New.tclTHEN (introduction id) (tac id) - | dest -> Tacticals.New.tclTHENLIST + | dest -> Tacticals.New.tclTHENLIST [introduction id; move_hyp id dest; tac id] let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = @@ -1011,10 +1011,10 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = match EConstr.kind sigma concl with | Prod (name,t,u) when not dep_flag || not (noccurn sigma 1 u) -> let name = find_name false (LocalAssum (name,t)) name_flag gl in - build_intro_tac name move_flag tac + build_intro_tac name move_flag tac | LetIn (name,b,t,u) when not dep_flag || not (noccurn sigma 1 u) -> let name = find_name false (LocalDef (name,b,t)) name_flag gl in - build_intro_tac name move_flag tac + build_intro_tac name move_flag tac | Evar ev when force_flag -> let sigma, t = Evardefine.define_evar_as_product env sigma ev in Tacticals.New.tclTHEN @@ -1028,9 +1028,9 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = (* probably also a pity that intro does zeta *) else Proofview.tclUNIT () end <*> - Proofview.tclORELSE - (Tacticals.New.tclTHEN hnf_in_concl - (intro_then_gen name_flag move_flag false dep_flag tac)) + Proofview.tclORELSE + (Tacticals.New.tclTHEN hnf_in_concl + (intro_then_gen name_flag move_flag false dep_flag tac)) begin function (e, info) -> match e with | RefinerError (env, sigma, IntroNeedsProduct) -> Tacticals.New.tclZEROMSG (str "No product even after head-reduction.") @@ -1107,9 +1107,9 @@ let intros_possibly_replacing ids = let hyps = Proofview.Goal.hyps gl in let posl = List.map (fun id -> (id, get_next_hyp_position env sigma id hyps)) ids in Tacticals.New.tclTHEN - (Tacticals.New.tclMAP (fun id -> - Tacticals.New.tclTRY (clear_for_replacing [id])) - (if suboptimal then ids else List.rev ids)) + (Tacticals.New.tclMAP (fun id -> + Tacticals.New.tclTRY (clear_for_replacing [id])) + (if suboptimal then ids else List.rev ids)) (Tacticals.New.tclMAP (fun (id,pos) -> Tacticals.New.tclORELSE (intro_move (Some id) pos) (intro_using id)) posl) @@ -1182,9 +1182,9 @@ let depth_of_quantified_hypothesis red h gl = | None -> user_err ~hdr:"lookup_quantified_hypothesis" (str "No " ++ msg_quantified_hypothesis h ++ - strbrk " in current goal" ++ - (if red then strbrk " even after head-reduction" else mt ()) ++ - str".") + strbrk " in current goal" ++ + (if red then strbrk " even after head-reduction" else mt ()) ++ + str".") let intros_until_gen red h = Proofview.Goal.enter begin fun gl -> @@ -1215,7 +1215,7 @@ let rec intros_move = function | [] -> Proofview.tclUNIT () | (hyp,destopt) :: rest -> Tacticals.New.tclTHEN (intro_gen (NamingMustBe (CAst.make hyp)) destopt false false) - (intros_move rest) + (intros_move rest) (* Apply a tactic on a quantified hypothesis, an hypothesis in context or a term with bindings *) @@ -1365,8 +1365,8 @@ let do_replace id = function let clenv_refine_in with_evars targetid id sigma0 clenv tac = let clenv = Clenvtac.clenv_pose_dependent_evars ~with_evars clenv in let clenv = - { clenv with evd = Typeclasses.resolve_typeclasses - ~fail:(not with_evars) clenv.env clenv.evd } + { clenv with evd = Typeclasses.resolve_typeclasses + ~fail:(not with_evars) clenv.env clenv.evd } in let new_hyp_typ = clenv_type clenv in if not with_evars then check_unresolved_evars_of_metas sigma0 clenv; @@ -1518,8 +1518,8 @@ let general_case_analysis with_evars clear_flag (c,lbindc as cx) = Proofview.tclEVARMAP >>= fun sigma -> match EConstr.kind sigma c with | Var id when lbindc == NoBindings -> - Tacticals.New.tclTHEN (try_intros_until_id_check id) - (general_case_analysis_in_context with_evars clear_flag cx) + Tacticals.New.tclTHEN (try_intros_until_id_check id) + (general_case_analysis_in_context with_evars clear_flag cx) | _ -> general_case_analysis_in_context with_evars clear_flag cx @@ -1569,10 +1569,10 @@ let elim with_evars clear_flag (c,lbindc as cx) elim = Proofview.tclEVARMAP >>= fun sigma -> match EConstr.kind sigma c with | Var id when lbindc == NoBindings -> - Tacticals.New.tclTHEN (try_intros_until_id_check id) - (elim_in_context with_evars clear_flag cx elim) + Tacticals.New.tclTHEN (try_intros_until_id_check id) + (elim_in_context with_evars clear_flag cx elim) | _ -> - elim_in_context with_evars clear_flag cx elim + elim_in_context with_evars clear_flag cx elim (* The simplest elimination tactic, with no substitutions at all. *) @@ -1605,36 +1605,36 @@ let make_projection env sigma params cstr sign elim i n c u = let b = match decl with LocalAssum _ -> mkRel (i+1) | LocalDef (_,b,_) -> b in let branch = it_mkLambda_or_LetIn b cs_args in if - (* excludes dependent projection types *) - noccur_between sigma 1 (n-i-1) t - (* to avoid surprising unifications, excludes flexible - projection types or lambda which will be instantiated by Meta/Evar *) - && not (isEvar sigma (fst (whd_betaiota_stack sigma t))) - && (accept_universal_lemma_under_conjunctions () || not (isRel sigma t)) + (* excludes dependent projection types *) + noccur_between sigma 1 (n-i-1) t + (* to avoid surprising unifications, excludes flexible + projection types or lambda which will be instantiated by Meta/Evar *) + && not (isEvar sigma (fst (whd_betaiota_stack sigma t))) + && (accept_universal_lemma_under_conjunctions () || not (isRel sigma t)) then let t = lift (i+1-n) t in - let abselim = beta_applist sigma (elim, params@[t;branch]) in - let args = Context.Rel.to_extended_vect mkRel 0 sign in - let c = beta_applist sigma (abselim, [mkApp (c, args)]) in - Some (it_mkLambda_or_LetIn c sign, it_mkProd_or_LetIn t sign) + let abselim = beta_applist sigma (elim, params@[t;branch]) in + let args = Context.Rel.to_extended_vect mkRel 0 sign in + let c = beta_applist sigma (abselim, [mkApp (c, args)]) in + Some (it_mkLambda_or_LetIn c sign, it_mkProd_or_LetIn t sign) else - None + None | DefinedRecord l -> (* goes from left to right when i increases! *) match List.nth l i with | Some proj -> - let args = Context.Rel.to_extended_vect mkRel 0 sign in - let proj = + let args = Context.Rel.to_extended_vect mkRel 0 sign in + let proj = match Recordops.find_primitive_projection proj with | Some proj -> - mkProj (Projection.make proj false, mkApp (c, args)) + mkProj (Projection.make proj false, mkApp (c, args)) | None -> - mkApp (mkConstU (proj,u), Array.append (Array.of_list params) - [|mkApp (c, args)|]) - in - let app = it_mkLambda_or_LetIn proj sign in - let t = Retyping.get_type_of env sigma app in - Some (app, t) + mkApp (mkConstU (proj,u), Array.append (Array.of_list params) + [|mkApp (c, args)|]) + in + let app = it_mkLambda_or_LetIn proj sign in + let t = Retyping.get_type_of env sigma app in + Some (app, t) | None -> None in elim @@ -1649,32 +1649,32 @@ let descend_in_conjunctions avoid tac (err, info) c = match match_with_tuple env sigma ccl with | Some (_,_,isrec) -> let n = (constructors_nrealargs env ind).(0) in - let sort = Tacticals.New.elimination_sort_of_goal gl in - let IndType (indf,_) = find_rectype env sigma ccl in - let (_,inst), params = dest_ind_family indf in - let params = List.map EConstr.of_constr params in - let cstr = (get_constructors env indf).(0) in - let elim = - try DefinedRecord (Recordops.lookup_projections ind) - with Not_found -> + let sort = Tacticals.New.elimination_sort_of_goal gl in + let IndType (indf,_) = find_rectype env sigma ccl in + let (_,inst), params = dest_ind_family indf in + let params = List.map EConstr.of_constr params in + let cstr = (get_constructors env indf).(0) in + let elim = + try DefinedRecord (Recordops.lookup_projections ind) + with Not_found -> let u = EInstance.kind sigma u in - let (_, elim) = build_case_analysis_scheme env sigma (ind,u) false sort in - let elim = EConstr.of_constr elim in - NotADefinedRecordUseScheme elim in - Tacticals.New.tclORELSE0 - (Tacticals.New.tclFIRST - (List.init n (fun i -> + let (_, elim) = build_case_analysis_scheme env sigma (ind,u) false sort in + let elim = EConstr.of_constr elim in + NotADefinedRecordUseScheme elim in + Tacticals.New.tclORELSE0 + (Tacticals.New.tclFIRST + (List.init n (fun i -> Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - match make_projection env sigma params cstr sign elim i n c u with - | None -> Tacticals.New.tclFAIL 0 (mt()) - | Some (p,pt) -> - Tacticals.New.tclTHENS - (assert_before_gen false (NamingAvoid avoid) pt) + match make_projection env sigma params cstr sign elim i n c u with + | None -> Tacticals.New.tclFAIL 0 (mt()) + | Some (p,pt) -> + Tacticals.New.tclTHENS + (assert_before_gen false (NamingAvoid avoid) pt) [Proofview.V82.tactic (refiner ~check:true EConstr.Unsafe.(to_constr p)); - (* Might be ill-typed due to forbidden elimination. *) - Tacticals.New.onLastHypId (tac (not isrec))] + (* Might be ill-typed due to forbidden elimination. *) + Tacticals.New.onLastHypId (tac (not isrec))] end))) (Proofview.tclZERO ~info err) | None -> Proofview.tclZERO ~info err @@ -1783,7 +1783,7 @@ let apply_with_delayed_bindings_gen b e l = let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let (sigma, cb) = f env sigma in - Tacticals.New.tclWITHHOLES e + Tacticals.New.tclWITHHOLES e (general_apply ~respect_opaque:(not b) b b e k CAst.(make ?loc cb)) sigma end in @@ -1903,7 +1903,7 @@ let apply_in_delayed_once ?(respect_opaque = false) with_delta let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let (sigma, c) = f env sigma in - Tacticals.New.tclWITHHOLES with_evars + Tacticals.New.tclWITHHOLES with_evars (apply_in_once ~respect_opaque with_delta with_destruct with_evars naming id (clear_flag,CAst.(make ?loc c)) tac) sigma @@ -2007,7 +2007,7 @@ let assumption = match ans with | Some sigma -> (Proofview.Unsafe.tclEVARS sigma) <*> - exact_no_check (mkVar (NamedDecl.get_id decl)) + exact_no_check (mkVar (NamedDecl.get_id decl)) | None -> arec gl only_eq rest in let assumption_tac gl = @@ -2127,7 +2127,7 @@ let keep hyps = let hyp = NamedDecl.get_id decl in if Id.List.mem hyp hyps || List.exists (occur_var_in_decl env sigma hyp) keep - || occur_var env sigma hyp ccl + || occur_var env sigma hyp ccl then (clear,decl::keep) else (hyp::clear,keep)) ~init:([],[]) (Proofview.Goal.env gl) @@ -2173,7 +2173,7 @@ let bring_hyps hyps = end end -let revert hyps = +let revert hyps = Proofview.Goal.enter begin fun gl -> let ctx = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) hyps in (bring_hyps ctx) <*> (clear hyps) @@ -2187,7 +2187,7 @@ let check_number_of_constructors expctdnumopt i nconstr = if Int.equal i 0 then error "The constructors are numbered starting from 1."; begin match expctdnumopt with | Some n when not (Int.equal n nconstr) -> - user_err ~hdr:"Tactics.check_number_of_constructors" + user_err ~hdr:"Tactics.check_number_of_constructors" (str "Not an inductive goal with " ++ int n ++ str (String.plural n " constructor") ++ str ".") | _ -> () end; @@ -2351,8 +2351,8 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac = let l2r = not l2r in (* equality of the form eq_true *) if isVar sigma c then let id' = destVar sigma c in - Tacticals.New.tclTHEN (rew_on l2r allHypsAndConcl) - (clear_var_and_eq id'), + Tacticals.New.tclTHEN (rew_on l2r allHypsAndConcl) + (clear_var_and_eq id'), early_clear id' thin else Tacticals.New.tclTHEN (rew_on l2r onConcl) (clear [id]), @@ -2362,7 +2362,7 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac = thin in (* Skip the side conditions of the rewriting step *) Tacticals.New.tclTHENFIRST eqtac (tac thin) - end + end let prepare_naming ?loc = function | IntroIdentifier id -> NamingMustBe (CAst.make ?loc id) @@ -2473,12 +2473,12 @@ let rec intro_patterns_core with_evars b avoid ids thin destopt bound n tac = match pat with | IntroForthcoming onlydeps -> intro_forthcoming_then_gen (NamingAvoid (Id.Set.union avoid (explicit_intro_names l))) - destopt onlydeps n bound + destopt onlydeps n bound (fun ids -> intro_patterns_core with_evars b avoid ids thin destopt bound (n+List.length ids) tac l) | IntroAction pat -> intro_then_gen (make_tmp_naming avoid l pat) - destopt true false + destopt true false (intro_pattern_action ?loc with_evars (b || not (List.is_empty l)) false pat thin destopt (fun thin bound' -> intro_patterns_core with_evars b avoid ids thin destopt bound' 0 @@ -2496,12 +2496,12 @@ and intro_pattern_naming loc with_evars b avoid ids pat thin destopt bound n tac (fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l)) | IntroAnonymous -> intro_then_gen (NamingAvoid (Id.Set.union avoid (explicit_intro_names l))) - destopt true false + destopt true false (fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l) | IntroFresh id -> (* todo: avoid thinned names to interfere with generation of fresh name *) intro_then_gen (NamingBasedOn (id, Id.Set.union avoid (explicit_intro_names l))) - destopt true false + destopt true false (fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l) and intro_pattern_action ?loc with_evars b style pat thin destopt tac id = @@ -2538,7 +2538,7 @@ and prepare_intros ?loc with_evars dft destopt = function (fun _ l -> clear_wildcards l) in fun id -> intro_pattern_action ?loc with_evars true true ipat [] destopt tac id) - | IntroForthcoming _ -> user_err ?loc + | IntroForthcoming _ -> user_err ?loc (str "Introduction pattern for one hypothesis expected.") let intro_patterns_head_core with_evars b destopt bound pat = @@ -2670,12 +2670,12 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty = let refl = applist (refl, [t;mkVar id]) in let term = mkNamedLetIn (make_annot id Sorts.Relevant) c t (mkLetIn (make_annot (Name heq) Sorts.Relevant, refl, eq, ccl)) in - let sigma, _ = Typing.type_of env sigma term in + let sigma, _ = Typing.type_of env sigma term in let ans = term, Tacticals.New.tclTHENLIST - [ + [ intro_gen (NamingMustBe CAst.(make ?loc heq)) (decode_hyp lastlhyp) true false; - clear_body [heq;id]] + clear_body [heq;id]] in (sigma, ans) | None -> @@ -2830,19 +2830,19 @@ let enough_by na t tac = forward false (Some (Some tac)) (ipat_of_name na) t let generalized_name env sigma c t ids cl = function | Name id as na -> if Id.List.mem id ids then - user_err (Id.print id ++ str " is already used."); + user_err (Id.print id ++ str " is already used."); na | Anonymous -> match EConstr.kind sigma c with | Var id -> - (* Keep the name even if not occurring: may be used by intros later *) - Name id + (* Keep the name even if not occurring: may be used by intros later *) + Name id | _ -> - if noccurn sigma 1 cl then Anonymous else - (* On ne s'etait pas casse la tete : on avait pris pour nom de + if noccurn sigma 1 cl then Anonymous else + (* On ne s'etait pas casse la tete : on avait pris pour nom de variable la premiere lettre du type, meme si "c" avait ete une constante dont on aurait pu prendre directement le nom *) - named_hd env sigma t Anonymous + named_hd env sigma t Anonymous (* Abstract over [c] in [forall x1:A1(c)..xi:Ai(c).T(c)] producing [forall x, x1:A1(x1), .., xi:Ai(x). T(x)] with all [c] abtracted in [Ai] @@ -2890,7 +2890,7 @@ let generalize_dep ?(with_let=false) c = let tothin' = match EConstr.kind sigma c with | Var id when mem_named_context_val id (val_of_named_context sign) && not (Id.List.mem id init_ids) - -> id::tothin + -> id::tothin | _ -> tothin in let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in @@ -2936,19 +2936,19 @@ let new_generalize_gen_let lconstr = let env = Proofview.Goal.env gl in let ids = Tacmach.New.pf_ids_of_hyps gl in let newcl, sigma, args = - List.fold_right_i - (fun i ((_,c,b),_ as o) (cl, sigma, args) -> - let sigma, t = Typing.type_of env sigma c in - let args = if Option.is_empty b then c :: args else args in + List.fold_right_i + (fun i ((_,c,b),_ as o) (cl, sigma, args) -> + let sigma, t = Typing.type_of env sigma c in + let args = if Option.is_empty b then c :: args else args in let cl, sigma = generalize_goal_gen env sigma ids i o t cl in (cl, sigma, args)) - 0 lconstr (concl, sigma, []) + 0 lconstr (concl, sigma, []) in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) - (Refine.refine ~typecheck:false begin fun sigma -> + (Refine.refine ~typecheck:false begin fun sigma -> let (sigma, ev) = Evarutil.new_evar env sigma ~principal:true newcl in (sigma, applist (ev, args)) - end) + end) end let generalize_gen lconstr = @@ -2982,14 +2982,17 @@ let quantify lconstr = hypothesis of the goal, the new hypothesis replaces it. (c,lbind) are supposed to be of the form - ((t t1 t2 ... tm) , someBindings) + ((H t1 t2 ... tm) , someBindings) + whete t1..tn are user given args, to which someBinding must be combined. + + The goal is to pose a proof with body - in which case we pose a proof with body + (fun y1...yp => H t1 t2 ... tm u1 ... uq) - (fun y1...yp => H t1 t2 ... tm u1 ... uq) where yi are the - remaining arguments of H that lbind could not resolve, ui are a mix - of inferred args and yi. The overall effect is to remove from H as - much quantification as possible given lbind. *) + where yi are the remaining arguments of H that lbind could not + solve, ui are a mix of inferred args and yi. The overall effect + is to remove from H as much quantification as possible given + lbind. *) let specialize (c,lbind) ipat = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in @@ -2998,6 +3001,7 @@ let specialize (c,lbind) ipat = if lbind == NoBindings then sigma, c else + (* ***** SOLVING ARGS ******* *) let typ_of_c = Retyping.get_type_of env sigma c in (* If the term is lambda then we put a letin to put avoid interaction between the term and the bindings. *) @@ -3010,16 +3014,24 @@ let specialize (c,lbind) ipat = let clause = clenv_unify_meta_types ~flags clause in let sigma = clause.evd in let (thd,tstack) = whd_nored_stack sigma (clenv_value clause) in - let c_hd , c_args = decompose_app sigma c in + (* The completely applied term is (thd tstack), but tstack may + contain unsolved metas, so now we must reabstract them + args with there name to have + fun unsolv1 unsolv2 ... => (thd tstack_with _rels) + Note: letins have been reudced, they are not present in tstack *) + (* ****** REBUILDING UNSOLVED FORALLs ****** *) + (* thd is the thing to which we reapply everything, solved or + unsolved, unsolved things are requantified too *) let liftrel x = match kind sigma x with | Rel n -> mkRel (n+1) | _ -> x in (* We grab names used in product to remember them at re-abstracting phase *) - let typ_of_c_hd = pf_get_type_of gl c_hd in + let typ_of_c_hd = pf_get_type_of gl thd in let lprod, concl = decompose_prod_assum sigma typ_of_c_hd in - (* accumulator args: arguments to apply to c_hd: all inferred - args + re-abstracted rels *) + (* lprd = initial products (including letins). + l(tstack initially) = the same products after unification vs lbind (some metas remain) + args: accumulator : args to apply to hd: inferred args + metas reabstracted *) let rec rebuild_lambdas sigma lprd args hd l = match lprd , l with | _, [] -> sigma,applist (hd, (List.map (nf_evar sigma) args)) @@ -3038,8 +3050,13 @@ let specialize (c,lbind) ipat = | Context.Rel.Declaration.LocalAssum _::lp' , t::l' -> let sigma,hd' = rebuild_lambdas sigma lp' (args@[t]) hd l' in sigma,hd' + | Context.Rel.Declaration.LocalDef _::lp' , _ -> + (* letins have been reduced in l and should anyway not + correspond to an arg, we ignore them. *) + let sigma,hd' = rebuild_lambdas sigma lp' args hd l in + sigma,hd' | _ ,_ -> assert false in - let sigma,hd = rebuild_lambdas sigma (List.rev lprod) [] c_hd tstack in + let sigma,hd = rebuild_lambdas sigma (List.rev lprod) [] thd tstack in Evd.clear_metas sigma, hd in let typ = Retyping.get_type_of env sigma term in @@ -3052,7 +3069,7 @@ let specialize (c,lbind) ipat = let repl = do_replace (Some id) naming in Tacticals.New.tclTHENFIRST (assert_before_then_gen repl naming typ tac) - (exact_no_check term) + (exact_no_check term) | _ -> match ipat with | None -> @@ -3067,7 +3084,7 @@ let specialize (c,lbind) ipat = let naming,tac = prepare_intros ?loc false IntroAnonymous MoveLast ipat in Tacticals.New.tclTHENFIRST (assert_before_then_gen false naming typ tac) - (exact_no_check term) + (exact_no_check term) in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) tac end @@ -3253,16 +3270,16 @@ let induct_discharge with_evars dests avoid' tac (avoid,ra) names = let (hyprec,names) = consume_pattern avoid (Name hyprecname) depind gl names in - dest_intro_patterns with_evars avoid thin MoveLast [hyprec] (fun ids' thin -> - peel_tac ra' (update_dest dests ids') names thin) + dest_intro_patterns with_evars avoid thin MoveLast [hyprec] (fun ids' thin -> + peel_tac ra' (update_dest dests ids') names thin) end) end | (IndArg,_,dep,hyprecname) :: ra' -> Proofview.Goal.enter begin fun gl -> - (* Rem: does not happen in Coq schemes, only in user-defined schemes *) + (* Rem: does not happen in Coq schemes, only in user-defined schemes *) let pat,names = consume_pattern avoid (Name hyprecname) dep gl names in - dest_intro_patterns with_evars avoid thin MoveLast [pat] (fun ids thin -> + dest_intro_patterns with_evars avoid thin MoveLast [pat] (fun ids thin -> peel_tac ra' (update_dest dests ids) names thin) end | (RecArg,_,dep,recvarname) :: ra' -> @@ -3270,14 +3287,14 @@ let induct_discharge with_evars dests avoid' tac (avoid,ra) names = let (pat,names) = consume_pattern avoid (Name recvarname) dep gl names in let dest = get_recarg_dest dests in - dest_intro_patterns with_evars avoid thin dest [pat] (fun ids thin -> + dest_intro_patterns with_evars avoid thin dest [pat] (fun ids thin -> peel_tac ra' dests names thin) end | (OtherArg,_,dep,_) :: ra' -> Proofview.Goal.enter begin fun gl -> let (pat,names) = consume_pattern avoid Anonymous dep gl names in let dest = get_recarg_dest dests in - safe_dest_intro_patterns with_evars avoid thin dest [pat] (fun ids thin -> + safe_dest_intro_patterns with_evars avoid thin dest [pat] (fun ids thin -> peel_tac ra' dests names thin) end | [] -> @@ -3301,8 +3318,8 @@ let expand_projections env sigma c = | _ -> map_constr_with_full_binders sigma push_rel aux env c in aux env c - - + + (* Marche pas... faut prendre en compte l'occurrence précise... *) let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = @@ -3327,14 +3344,14 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = else let c = List.nth argl (i-1) in match EConstr.kind sigma c with - | Var id when not (List.exists (fun c -> occur_var env sigma id c) args') && + | Var id when not (List.exists (fun c -> occur_var env sigma id c) args') && not (List.exists (fun c -> occur_var env sigma id c) params') -> (* Based on the knowledge given by the user, all constraints on the variable are generalizable in the current environment so that it is clearable after destruction *) - atomize_one (i-1) (c::args) (c::args') (Id.Set.add id avoid) - | _ -> - let c' = expand_projections env' sigma c in + atomize_one (i-1) (c::args) (c::args') (Id.Set.add id avoid) + | _ -> + let c' = expand_projections env' sigma c in let dependent t = dependent sigma c t in if List.exists dependent params' || List.exists dependent args' @@ -3344,7 +3361,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = follow the (old) discipline of not generalizing over this term, since we don't try to invert the constraint anyway. *) - atomize_one (i-1) (c::args) (c'::args') avoid + atomize_one (i-1) (c::args) (c'::args') avoid else (* We reason blindly on the term and do as if it were generalizable, ignoring the constraints coming from @@ -3355,9 +3372,9 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = let type_of = Tacmach.New.pf_unsafe_type_of gl in id_of_name_using_hdchar env sigma (type_of c) Anonymous in let x = fresh_id_in_env avoid id env in - Tacticals.New.tclTHEN - (letin_tac None (Name x) c None allHypsAndConcl) - (atomize_one (i-1) (mkVar x::args) (mkVar x::args') (Id.Set.add x avoid)) + Tacticals.New.tclTHEN + (letin_tac None (Name x) c None allHypsAndConcl) + (atomize_one (i-1) (mkVar x::args) (mkVar x::args') (Id.Set.add x avoid)) in atomize_one (List.length argl) [] [] Id.Set.empty end @@ -3454,30 +3471,30 @@ let cook_sign hyp0_opt inhyps indvars env sigma = toclear := hyp::!toclear; rhyp end else - let dephyp0 = List.is_empty inhyps && - (Option.cata (fun id -> occur_var_in_decl env sigma id decl) false hyp0_opt) + let dephyp0 = List.is_empty inhyps && + (Option.cata (fun id -> occur_var_in_decl env sigma id decl) false hyp0_opt) in let depother = List.is_empty inhyps && - (Id.Set.exists (fun id -> occur_var_in_decl env sigma id decl) indvars || + (Id.Set.exists (fun id -> occur_var_in_decl env sigma id decl) indvars || List.exists (fun decl' -> occur_var_in_decl env sigma (NamedDecl.get_id decl') decl) !decldeps) in if not (List.is_empty inhyps) && Id.List.mem hyp inhyps || dephyp0 || depother then begin - decldeps := decl::!decldeps; - avoid := Id.Set.add hyp !avoid; + decldeps := decl::!decldeps; + avoid := Id.Set.add hyp !avoid; maindep := dephyp0 || !maindep; - if !before then begin + if !before then begin toclear := hyp::!toclear; - rstatus := (hyp,rhyp)::!rstatus + rstatus := (hyp,rhyp)::!rstatus end - else begin - toclear := hyp::!toclear; - ldeps := hyp::!ldeps (* status computed in 2nd phase *) + else begin + toclear := hyp::!toclear; + ldeps := hyp::!ldeps (* status computed in 2nd phase *) end; - MoveBefore hyp end + MoveBefore hyp end else - MoveBefore hyp + MoveBefore hyp in let _ = fold_named_context seek_deps env ~init:MoveFirst in (* 2nd phase from R to L: get left hyp of [hyp0] and [lhyps] *) @@ -3543,7 +3560,7 @@ type elim_scheme = { indarg: rel_declaration option; (* Some (H,I prm1..prmp x1...xni) if HI is in premisses, None otherwise *) concl: types; (* Qi x1...xni HI (f...), HI and (f...) - are optional and mutually exclusive *) + are optional and mutually exclusive *) indarg_in_concl: bool; (* true if HI appears at the end of conclusion *) farg_in_concl: bool; (* true if (f...) appears at the end of conclusion *) } @@ -3584,8 +3601,8 @@ let make_up_names n ind_opt cname = let base_ind = if is_hyp then match ind_opt with - | None -> Id.of_string ind_prefix - | Some ind_id -> add_prefix ind_prefix (Nametab.basename_of_global ind_id) + | None -> Id.of_string ind_prefix + | Some ind_id -> add_prefix ind_prefix (Nametab.basename_of_global ind_id) else add_prefix ind_prefix cname in let hyprecname = make_base n base_ind in let avoid = @@ -3633,7 +3650,7 @@ let lift_togethern n l = let l', _ = List.fold_right (fun x (acc, n) -> - (lift n x :: acc, succ n)) + (lift n x :: acc, succ n)) l ([], n) in l' @@ -3644,14 +3661,14 @@ let ids_of_constr sigma ?(all=false) vars c = match EConstr.kind sigma c with | Var id -> Id.Set.add id vars | App (f, args) -> - (match EConstr.kind sigma f with - | Construct ((ind,_),_) - | Ind (ind,_) -> + (match EConstr.kind sigma f with + | Construct ((ind,_),_) + | Ind (ind,_) -> let (mib,mip) = Global.lookup_inductive ind in - Array.fold_left_from - (if all then 0 else mib.Declarations.mind_nparams) - aux vars args - | _ -> EConstr.fold sigma aux vars c) + Array.fold_left_from + (if all then 0 else mib.Declarations.mind_nparams) + aux vars args + | _ -> EConstr.fold sigma aux vars c) | _ -> EConstr.fold sigma aux vars c in aux vars c @@ -3662,7 +3679,7 @@ let decompose_indapp sigma f args = let (mib,mip) = Global.lookup_inductive ind in let first = mib.Declarations.mind_nparams_rec in let pars, args = Array.chop first args in - mkApp (f, pars), args + mkApp (f, pars), args | _ -> f, args let mk_term_eq homogeneous env sigma ty t ty' t' = @@ -3722,13 +3739,13 @@ let hyps_of_vars env sigma sign nogen hyps = Context.Named.fold_inside (fun (hs,hl) d -> let x = NamedDecl.get_id d in - if Id.Set.mem x nogen then (hs,hl) - else if Id.Set.mem x hs then (hs,x::hl) - else - let xvars = global_vars_set_of_decl env sigma d in - if not (Id.Set.is_empty (Id.Set.diff xvars hs)) then - (Id.Set.add x hs, x :: hl) - else (hs, hl)) + if Id.Set.mem x nogen then (hs,hl) + else if Id.Set.mem x hs then (hs,x::hl) + else + let xvars = global_vars_set_of_decl env sigma d in + if not (Id.Set.is_empty (Id.Set.diff xvars hs)) then + (Id.Set.add x hs, x :: hl) + else (hs, hl)) ~init:(hyps,[]) sign in lh @@ -3739,14 +3756,14 @@ let linear sigma vars args = let seen = ref vars in try Array.iter (fun i -> - let rels = ids_of_constr sigma ~all:true Id.Set.empty i in - let seen' = - Id.Set.fold (fun id acc -> - if Id.Set.mem id acc then raise Seen - else Id.Set.add id acc) - rels !seen - in seen := seen') - args; + let rels = ids_of_constr sigma ~all:true Id.Set.empty i in + let seen' = + Id.Set.fold (fun id acc -> + if Id.Set.mem id acc then raise Seen + else Id.Set.add id acc) + rels !seen + in seen := seen') + args; true with Seen -> false @@ -3785,62 +3802,62 @@ let abstract_args gl generalize_vars dep id defined f args = let leq = constr_cmp !sigma Reduction.CUMUL liftargty ty in match EConstr.kind !sigma arg with | Var id when not (is_defined_variable env id) && leq && not (Id.Set.mem id nongenvars) -> - (subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, - Id.Set.add id nongenvars, Id.Set.remove id vars, env) + (subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, + Id.Set.add id nongenvars, Id.Set.remove id vars, env) | _ -> - let name = get_id name in + let name = get_id name in let decl = LocalAssum (make_annot (Name name) ty_relevance, ty) in - let ctx = decl :: ctx in - let c' = mkApp (lift 1 c, [|mkRel 1|]) in - let args = arg :: args in - let liftarg = lift (List.length ctx) arg in - let eq, refl = - if leq then - let sigma', eq = mkEq !sigma (lift 1 ty) (mkRel 1) liftarg in + let ctx = decl :: ctx in + let c' = mkApp (lift 1 c, [|mkRel 1|]) in + let args = arg :: args in + let liftarg = lift (List.length ctx) arg in + let eq, refl = + if leq then + let sigma', eq = mkEq !sigma (lift 1 ty) (mkRel 1) liftarg in let sigma', refl = mkRefl sigma' (lift (-lenctx) ty) arg in sigma := sigma'; eq, refl - else - let sigma', eq = mkHEq !sigma (lift 1 ty) (mkRel 1) liftargty liftarg in + else + let sigma', eq = mkHEq !sigma (lift 1 ty) (mkRel 1) liftargty liftarg in let sigma', refl = mkHRefl sigma' argty arg in sigma := sigma'; eq, refl - in - let eqs = eq :: lift_list eqs in - let refls = refl :: refls in - let argvars = ids_of_constr !sigma vars arg in - (arity, ctx, push_rel decl ctxenv, c', args, eqs, refls, - nongenvars, Id.Set.union argvars vars, env) + in + let eqs = eq :: lift_list eqs in + let refls = refl :: refls in + let argvars = ids_of_constr !sigma vars arg in + (arity, ctx, push_rel decl ctxenv, c', args, eqs, refls, + nongenvars, Id.Set.union argvars vars, env) in let f', args' = decompose_indapp !sigma f args in let dogen, f', args' = let parvars = ids_of_constr !sigma ~all:true Id.Set.empty f' in if not (linear !sigma parvars args') then true, f, args else - match Array.findi (fun i x -> not (isVar !sigma x) || is_defined_variable env (destVar !sigma x)) args' with - | None -> false, f', args' - | Some nonvar -> - let before, after = Array.chop nonvar args' in - true, mkApp (f', before), after + match Array.findi (fun i x -> not (isVar !sigma x) || is_defined_variable env (destVar !sigma x)) args' with + | None -> false, f', args' + | Some nonvar -> + let before, after = Array.chop nonvar args' in + true, mkApp (f', before), after in if dogen then let tyf' = Tacmach.New.pf_unsafe_type_of gl f' in let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env = - Array.fold_left aux (tyf',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args' + Array.fold_left aux (tyf',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args' in let args, refls = List.rev args, List.rev refls in let vars = - if generalize_vars then - let nogen = Id.Set.add id nogen in - hyps_of_vars (pf_env gl) (project gl) (Proofview.Goal.hyps gl) nogen vars - else [] + if generalize_vars then + let nogen = Id.Set.add id nogen in + hyps_of_vars (pf_env gl) (project gl) (Proofview.Goal.hyps gl) nogen vars + else [] in let body, c' = - if defined then Some c', Retyping.get_type_of ctxenv !sigma c' - else None, c' + if defined then Some c', Retyping.get_type_of ctxenv !sigma c' + else None, c' in let typ = Tacmach.New.pf_get_hyp_typ id gl in let tac = make_abstract_generalize (pf_env gl) id typ concl dep ctx body c' eqs args refls in let tac = Proofview.Unsafe.tclEVARS !sigma <*> tac in - Some (tac, dep, succ (List.length ctx), vars) + Some (tac, dep, succ (List.length ctx), vars) else None let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id = @@ -3852,10 +3869,10 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id = let oldid = Tacmach.New.pf_get_new_id id gl in match Tacmach.New.pf_get_hyp id gl with | LocalAssum (_,t) -> let f, args = decompose_app sigma t in - (f, args, false, id, oldid) + (f, args, false, id, oldid) | LocalDef (_,t,_) -> - let f, args = decompose_app sigma t in - (f, args, true, id, oldid) + let f, args = decompose_app sigma t in + (f, args, true, id, oldid) in if List.is_empty args then Proofview.tclUNIT () else @@ -3864,23 +3881,23 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id = match newc with | None -> Proofview.tclUNIT () | Some (tac, dep, n, vars) -> - let tac = - if dep then + let tac = + if dep then Tacticals.New.tclTHENLIST [ tac; - rename_hyp [(id, oldid)]; Tacticals.New.tclDO n intro; - generalize_dep ~with_let:true (mkVar oldid)] + rename_hyp [(id, oldid)]; Tacticals.New.tclDO n intro; + generalize_dep ~with_let:true (mkVar oldid)] else Tacticals.New.tclTHENLIST [ tac; - clear [id]; - Tacticals.New.tclDO n intro] - in - if List.is_empty vars then tac - else Tacticals.New.tclTHEN tac + clear [id]; + Tacticals.New.tclDO n intro] + in + if List.is_empty vars then tac + else Tacticals.New.tclTHEN tac (Tacticals.New.tclFIRST [revert vars ; - Tacticals.New.tclMAP (fun id -> - Tacticals.New.tclTRY (generalize_dep ~with_let:true (mkVar id))) vars]) + Tacticals.New.tclMAP (fun id -> + Tacticals.New.tclTRY (generalize_dep ~with_let:true (mkVar id))) vars]) end let compare_upto_variables sigma x y = @@ -3905,26 +3922,26 @@ let specialize_eqs id = let rec aux in_eqs ctx acc ty = match EConstr.kind !evars ty with | Prod (na, t, b) -> - (match EConstr.kind !evars t with + (match EConstr.kind !evars t with | App (eq, [| eqty; x; y |]) when EConstr.is_global !evars Coqlib.(lib_ref "core.eq.type") eq -> - let c = if noccur_between !evars 1 (List.length ctx) x then y else x in - let pt = mkApp (eq, [| eqty; c; c |]) in + let c = if noccur_between !evars 1 (List.length ctx) x then y else x in + let pt = mkApp (eq, [| eqty; c; c |]) in let ind = destInd !evars eq in - let p = mkApp (mkConstructUi (ind,0), [| eqty; c |]) in - if unif (push_rel_context ctx env) evars pt t then - aux true ctx (mkApp (acc, [| p |])) (subst1 p b) - else acc, in_eqs, ctx, ty - | App (heq, [| eqty; x; eqty'; y |]) when EConstr.is_global !evars (Lazy.force coq_heq_ref) heq -> - let eqt, c = if noccur_between !evars 1 (List.length ctx) x then eqty', y else eqty, x in - let pt = mkApp (heq, [| eqt; c; eqt; c |]) in + let p = mkApp (mkConstructUi (ind,0), [| eqty; c |]) in + if unif (push_rel_context ctx env) evars pt t then + aux true ctx (mkApp (acc, [| p |])) (subst1 p b) + else acc, in_eqs, ctx, ty + | App (heq, [| eqty; x; eqty'; y |]) when EConstr.is_global !evars (Lazy.force coq_heq_ref) heq -> + let eqt, c = if noccur_between !evars 1 (List.length ctx) x then eqty', y else eqty, x in + let pt = mkApp (heq, [| eqt; c; eqt; c |]) in let ind = destInd !evars heq in - let p = mkApp (mkConstructUi (ind,0), [| eqt; c |]) in - if unif (push_rel_context ctx env) evars pt t then - aux true ctx (mkApp (acc, [| p |])) (subst1 p b) - else acc, in_eqs, ctx, ty - | _ -> - if in_eqs then acc, in_eqs, ctx, ty - else + let p = mkApp (mkConstructUi (ind,0), [| eqt; c |]) in + if unif (push_rel_context ctx env) evars pt t then + aux true ctx (mkApp (acc, [| p |])) (subst1 p b) + else acc, in_eqs, ctx, ty + | _ -> + if in_eqs then acc, in_eqs, ctx, ty + else let sigma, e = Evarutil.new_evar (push_rel_context ctx env) !evars t in evars := sigma; aux false (LocalDef (na,e,t) :: ctx) (mkApp (lift 1 acc, [| mkRel 1 |])) b) @@ -3944,7 +3961,7 @@ let specialize_eqs id = if worked then Tacticals.New.tclTHENFIRST (internal_cut true id ty') - (exact_no_check ((* refresh_universes_strict *) acc')) + (exact_no_check ((* refresh_universes_strict *) acc')) else Tacticals.New.tclFAIL 0 (str "Nothing to do in hypothesis " ++ Id.print id) end @@ -3973,10 +3990,10 @@ let decompose_paramspred_branch_args sigma elimt = let rec cut_noccur elimt acc2 = match EConstr.kind sigma elimt with | Prod(nme,tpe,elimt') -> - let hd_tpe,_ = decompose_app sigma (snd (decompose_prod_assum sigma tpe)) in - if not (occur_rel sigma 1 elimt') && isRel sigma hd_tpe + let hd_tpe,_ = decompose_app sigma (snd (decompose_prod_assum sigma tpe)) in + if not (occur_rel sigma 1 elimt') && isRel sigma hd_tpe then cut_noccur elimt' (LocalAssum (nme,tpe)::acc2) - else let acc3,ccl = decompose_prod_assum sigma elimt in acc2 , acc3 , ccl + else let acc3,ccl = decompose_prod_assum sigma elimt in acc2 , acc3 , ccl | App(_, _) | Rel _ -> acc2 , [] , elimt | _ -> error_ind_scheme "" in let rec cut_occur elimt acc1 = @@ -4048,8 +4065,8 @@ let compute_elim_sig sigma ?elimc elimt = if !res.farg_in_concl then begin res := { !res with - indarg = None; - indarg_in_concl = false; farg_in_concl = true }; + indarg = None; + indarg_in_concl = false; farg_in_concl = true }; raise Exit end; (* 2- If no args_indargs (=!res.nargs at this point) then no indarg *) @@ -4059,34 +4076,34 @@ let compute_elim_sig sigma ?elimc elimt = match List.hd args_indargs with | LocalDef (hiname,_,hi) -> error_ind_scheme "" | LocalAssum (hiname,hi) -> - let hi_ind, hi_args = decompose_app sigma hi in - let hi_is_ind = (* hi est d'un type globalisable *) - match EConstr.kind sigma hi_ind with - | Ind (mind,_) -> true - | Var _ -> true - | Const _ -> true - | Construct _ -> true - | _ -> false in - let hi_args_enough = (* hi a le bon nbre d'arguments *) - Int.equal (List.length hi_args) (List.length params + !res.nargs -1) in - (* FIXME: Ces deux tests ne sont pas suffisants. *) - if not (hi_is_ind && hi_args_enough) then raise Exit (* No indarg *) - else (* Last arg is the indarg *) - res := {!res with - indarg = Some (List.hd !res.args); - indarg_in_concl = occur_rel sigma 1 ccl; - args = List.tl !res.args; nargs = !res.nargs - 1; - }; - raise Exit); + let hi_ind, hi_args = decompose_app sigma hi in + let hi_is_ind = (* hi est d'un type globalisable *) + match EConstr.kind sigma hi_ind with + | Ind (mind,_) -> true + | Var _ -> true + | Const _ -> true + | Construct _ -> true + | _ -> false in + let hi_args_enough = (* hi a le bon nbre d'arguments *) + Int.equal (List.length hi_args) (List.length params + !res.nargs -1) in + (* FIXME: Ces deux tests ne sont pas suffisants. *) + if not (hi_is_ind && hi_args_enough) then raise Exit (* No indarg *) + else (* Last arg is the indarg *) + res := {!res with + indarg = Some (List.hd !res.args); + indarg_in_concl = occur_rel sigma 1 ccl; + args = List.tl !res.args; nargs = !res.nargs - 1; + }; + raise Exit); raise Exit(* exit anyway *) with Exit -> (* Ending by computing indref: *) match !res.indarg with | None -> !res (* No indref *) | Some (LocalDef _) -> error_ind_scheme "" | Some (LocalAssum (_,ind)) -> - let indhd,indargs = decompose_app sigma ind in - try {!res with indref = Some (fst (Termops.global_of_constr sigma indhd)) } - with e when CErrors.noncritical e -> + let indhd,indargs = decompose_app sigma ind in + try {!res with indref = Some (fst (Termops.global_of_constr sigma indhd)) } + with e when CErrors.noncritical e -> error "Cannot find the inductive type of the inductive scheme." let compute_scheme_signature evd scheme names_info ind_type_guess = @@ -4096,23 +4113,23 @@ let compute_scheme_signature evd scheme names_info ind_type_guess = let cond, check_concl = match scheme.indarg with | Some (LocalDef _) -> - error "Strange letin, cannot recognize an induction scheme." + error "Strange letin, cannot recognize an induction scheme." | None -> (* Non standard scheme *) - let cond hd = EConstr.eq_constr evd hd ind_type_guess && not scheme.farg_in_concl - in (cond, fun _ _ -> ()) + let cond hd = EConstr.eq_constr evd hd ind_type_guess && not scheme.farg_in_concl + in (cond, fun _ _ -> ()) | Some (LocalAssum (_,ind)) -> (* Standard scheme from an inductive type *) - let indhd,indargs = decompose_app evd ind in - let cond hd = EConstr.eq_constr evd hd indhd in - let check_concl is_pred p = - (* Check again conclusion *) - let ccl_arg_ok = is_pred (p + scheme.nargs + 1) f == IndArg in - let ind_is_ok = - List.equal (fun c1 c2 -> EConstr.eq_constr evd c1 c2) - (List.lastn scheme.nargs indargs) - (Context.Rel.to_extended_list mkRel 0 scheme.args) in - if not (ccl_arg_ok && ind_is_ok) then - error_ind_scheme "the conclusion of" - in (cond, check_concl) + let indhd,indargs = decompose_app evd ind in + let cond hd = EConstr.eq_constr evd hd indhd in + let check_concl is_pred p = + (* Check again conclusion *) + let ccl_arg_ok = is_pred (p + scheme.nargs + 1) f == IndArg in + let ind_is_ok = + List.equal (fun c1 c2 -> EConstr.eq_constr evd c1 c2) + (List.lastn scheme.nargs indargs) + (Context.Rel.to_extended_list mkRel 0 scheme.args) in + if not (ccl_arg_ok && ind_is_ok) then + error_ind_scheme "the conclusion of" + in (cond, check_concl) in let is_pred n c = let hd = fst (decompose_app evd c) in @@ -4124,27 +4141,27 @@ let compute_scheme_signature evd scheme names_info ind_type_guess = let rec check_branch p c = match EConstr.kind evd c with | Prod (_,t,c) -> - (is_pred p t, true, not (Vars.noccurn evd 1 c)) :: check_branch (p+1) c + (is_pred p t, true, not (Vars.noccurn evd 1 c)) :: check_branch (p+1) c | LetIn (_,_,_,c) -> - (OtherArg, false, not (Vars.noccurn evd 1 c)) :: check_branch (p+1) c + (OtherArg, false, not (Vars.noccurn evd 1 c)) :: check_branch (p+1) c | _ when is_pred p c == IndArg -> [] | _ -> raise Exit in let rec find_branches p lbrch = match lbrch with | LocalAssum (_,t) :: brs -> - (try - let lchck_brch = check_branch p t in - let n = List.fold_left - (fun n (b,_,_) -> if b == RecArg then n+1 else n) 0 lchck_brch in - let recvarname, hyprecname, avoid = - make_up_names n scheme.indref names_info in - let namesign = - List.map (fun (b,is_assum,dep) -> - (b,is_assum,dep,if b == IndArg then hyprecname else recvarname)) - lchck_brch in - (avoid,namesign) :: find_branches (p+1) brs - with Exit-> error_ind_scheme "the branches of") + (try + let lchck_brch = check_branch p t in + let n = List.fold_left + (fun n (b,_,_) -> if b == RecArg then n+1 else n) 0 lchck_brch in + let recvarname, hyprecname, avoid = + make_up_names n scheme.indref names_info in + let namesign = + List.map (fun (b,is_assum,dep) -> + (b,is_assum,dep,if b == IndArg then hyprecname else recvarname)) + lchck_brch in + (avoid,namesign) :: find_branches (p+1) brs + with Exit-> error_ind_scheme "the branches of") | LocalDef _ :: _ -> error_ind_scheme "the branches of" | [] -> check_concl is_pred p; [] in @@ -4210,12 +4227,12 @@ let find_induction_type isrec elim hyp0 gl = (* We drop the scheme waiting to know if it is dependent *) scheme, ElimOver (isrec,hyp0) | Some e -> - let evd, (elimc,elimt),ind_guess = given_elim hyp0 e gl in - let scheme = compute_elim_sig sigma ~elimc elimt in - if Option.is_empty scheme.indarg then error "Cannot find induction type"; - let indsign = compute_scheme_signature evd scheme hyp0 ind_guess in + let evd, (elimc,elimt),ind_guess = given_elim hyp0 e gl in + let scheme = compute_elim_sig sigma ~elimc elimt in + if Option.is_empty scheme.indarg then error "Cannot find induction type"; + let indsign = compute_scheme_signature evd scheme hyp0 ind_guess in let elim = ({ elimindex = Some(-1); elimbody = elimc },elimt) in - scheme, ElimUsing (elim,indsign) + scheme, ElimUsing (elim,indsign) in match scheme.indref with | None -> error_ind_scheme "" @@ -4251,9 +4268,9 @@ let recolle_clenv i params args elimclause gl = let lindmv = Array.map (fun x -> - match EConstr.kind elimclause.evd x with - | Meta mv -> mv - | _ -> user_err ~hdr:"elimination_clause" + match EConstr.kind elimclause.evd x with + | Meta mv -> mv + | _ -> user_err ~hdr:"elimination_clause" (str "The type of the elimination clause is not well-formed.")) arr in let k = match i with -1 -> Array.length lindmv - List.length args | _ -> i in @@ -4399,18 +4416,18 @@ let clear_unselected_context id inhyps cls = Proofview.Goal.enter begin fun gl -> if occur_var (Tacmach.New.pf_env gl) (Tacmach.New.project gl) id (Tacmach.New.pf_concl gl) && cls.concl_occs == NoOccurrences - then user_err + then user_err (str "Conclusion must be mentioned: it depends on " ++ Id.print id ++ str "."); match cls.onhyps with | Some hyps -> let to_erase d = let id' = NamedDecl.get_id d in - if Id.List.mem id' inhyps then (* if selected, do not erase *) None - else - (* erase if not selected and dependent on id or selected hyps *) - let test id = occur_var_in_decl (Tacmach.New.pf_env gl) (Tacmach.New.project gl) id d in - if List.exists test (id::inhyps) then Some id' else None in + if Id.List.mem id' inhyps then (* if selected, do not erase *) None + else + (* erase if not selected and dependent on id or selected hyps *) + let test id = occur_var_in_decl (Tacmach.New.pf_env gl) (Tacmach.New.project gl) id d in + if List.exists test (id::inhyps) then Some id' else None in let ids = List.map_filter to_erase (Proofview.Goal.hyps gl) in clear ids | None -> Proofview.tclUNIT () @@ -4591,7 +4608,7 @@ let induction_gen clear_flag isrec with_evars elim isrec with_evars info_arg elim id arg t inhyps cls (induction_with_atomization_of_ind_arg isrec with_evars elim names id) - end + end (* Induction on a list of arguments. First make induction arguments atomic (using letins), then do induction. The specificity here is @@ -4610,32 +4627,32 @@ let induction_gen_l isrec with_evars elim names lc = | [] -> Proofview.tclUNIT () | c::l' -> Proofview.tclEVARMAP >>= fun sigma -> - match EConstr.kind sigma c with - | Var id when not (mem_named_context_val id (Global.named_context_val ())) - && not with_evars -> + match EConstr.kind sigma c with + | Var id when not (mem_named_context_val id (Global.named_context_val ())) + && not with_evars -> let () = newlc:= id::!newlc in - atomize_list l' + atomize_list l' - | _ -> + | _ -> Proofview.Goal.enter begin fun gl -> let type_of = Tacmach.New.pf_unsafe_type_of gl in let sigma = Tacmach.New.project gl in Proofview.tclENV >>= fun env -> let x = - id_of_name_using_hdchar env sigma (type_of c) Anonymous in + id_of_name_using_hdchar env sigma (type_of c) Anonymous in let id = new_fresh_id Id.Set.empty x gl in - let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in + let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in let () = newlc:=id::!newlc in - Tacticals.New.tclTHEN - (letin_tac None (Name id) c None allHypsAndConcl) - (atomize_list newl') + Tacticals.New.tclTHEN + (letin_tac None (Name id) c None allHypsAndConcl) + (atomize_list newl') end in Tacticals.New.tclTHENLIST [ (atomize_list lc); (Proofview.tclUNIT () >>= fun () -> (* ensure newlc has been computed *) - induction_without_atomization isrec with_evars elim names !newlc) + induction_without_atomization isrec with_evars elim names !newlc) ] (* Induction either over a term, over a quantified premisse, or over @@ -4657,8 +4674,8 @@ let induction_destruct isrec with_evars (lc,elim) = if not (Option.is_empty cls) then error "'in' clause not supported here."; let _,c = force_destruction_arg false env sigma c in onInductionArg - (fun _clear_flag c -> - induction_gen_l isrec with_evars elim names + (fun _clear_flag c -> + induction_gen_l isrec with_evars elim names [with_no_bindings c,eqname]) c | _ -> (* standard induction *) @@ -4694,12 +4711,12 @@ let induction_destruct isrec with_evars (lc,elim) = let newlc = List.map (fun (x,(eqn,names),cls) -> if cls != None then error "'in' clause not yet supported here."; - match x with (* FIXME: should we deal with ElimOnIdent? *) + match x with (* FIXME: should we deal with ElimOnIdent? *) | _clear_flag,ElimOnConstr x -> if eqn <> None then error "'eqn' clause not supported here."; (with_no_bindings x,names) - | _ -> error "Don't know where to find some argument.") - lc in + | _ -> error "Don't know where to find some argument.") + lc in (* Check that "as", if any, is given only on the last argument *) let names,rest = List.sep_last (List.map snd newlc) in if List.exists (fun n -> not (Option.is_empty n)) rest then @@ -4729,10 +4746,10 @@ let elim_scheme_type elim t = match EConstr.kind clause.evd (last_arg clause.evd clause.templval.rebus) with | Meta mv -> let clause' = - (* t is inductive, then CUMUL or CONV is irrelevant *) - clenv_unify ~flags:(elim_flags ()) Reduction.CUMUL t + (* t is inductive, then CUMUL or CONV is irrelevant *) + clenv_unify ~flags:(elim_flags ()) Reduction.CUMUL t (clenv_meta_type clause mv) clause in - Clenvtac.res_pf clause' ~flags:(elim_flags ()) ~with_evars:false + Clenvtac.res_pf clause' ~flags:(elim_flags ()) ~with_evars:false | _ -> anomaly (Pp.str "elim_scheme_type.") end @@ -4815,7 +4832,7 @@ let prove_symmetry hdcncl eq_kind = (Tacticals.New.tclTHENLIST [ intro; Tacticals.New.onLastHyp simplest_case; - one_constructor 1 NoBindings ]) + one_constructor 1 NoBindings ]) let match_with_equation sigma c = Proofview.tclENV >>= fun env -> @@ -4915,9 +4932,9 @@ let prove_transitivity hdcncl eq_kind t = Tacticals.New.tclTHENFIRST (cut eq2) (Tacticals.New.tclTHENFIRST (cut eq1) (Tacticals.New.tclTHENLIST - [ Tacticals.New.tclDO 2 intro; - Tacticals.New.onLastHyp simplest_case; - assumption ])) + [ Tacticals.New.tclDO 2 intro; + Tacticals.New.onLastHyp simplest_case; + assumption ])) end let transitivity_red allowred t = @@ -4933,8 +4950,8 @@ let transitivity_red allowred t = Tacticals.New.tclTHEN (convert_concl ~check:false concl DEFAULTcast) (match t with - | None -> Tacticals.New.pf_constr_of_global eq_data.trans >>= eapply - | Some t -> Tacticals.New.pf_constr_of_global eq_data.trans >>= fun trans -> apply_list [trans; t]) + | None -> Tacticals.New.pf_constr_of_global eq_data.trans >>= eapply + | Some t -> Tacticals.New.pf_constr_of_global eq_data.trans >>= fun trans -> apply_list [trans; t]) | None,eq,eq_kind -> match t with | None -> Tacticals.New.tclZEROMSG (str"etransitivity not supported for this relation.") @@ -4981,8 +4998,8 @@ let unify ?(state=TransparentState.full) x y = try let core_flags = { (default_unify_flags ()).core_unify_flags with - modulo_delta = state; - modulo_conv_on_closed_terms = Some state} in + modulo_delta = state; + modulo_conv_on_closed_terms = Some state} in (* What to do on merge and subterm flags?? *) let flags = { (default_unify_flags ()) with core_unify_flags = core_flags; @@ -5021,7 +5038,7 @@ module New = struct let reduce_after_refine = reduce (Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true; - rZeta=false;rDelta=false;rConst=[]}) + rZeta=false;rDelta=false;rConst=[]}) {onhyps = Some []; concl_occs = AllOccurrences } let refine ~typecheck c = diff --git a/tactics/tactics.mli b/tactics/tactics.mli index d3c800df20..308399c5db 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -221,12 +221,12 @@ val eapply_with_bindings : constr with_bindings -> unit Proofview.tactic val cut_and_apply : constr -> unit Proofview.tactic val apply_in : - advanced_flag -> evars_flag -> Id.t -> + advanced_flag -> evars_flag -> Id.t -> (clear_flag * constr with_bindings CAst.t) list -> intro_pattern option -> unit Proofview.tactic val apply_delayed_in : - advanced_flag -> evars_flag -> Id.t -> + advanced_flag -> evars_flag -> Id.t -> (clear_flag * delayed_open_constr_with_bindings CAst.t) list -> intro_pattern option -> unit Proofview.tactic @@ -270,9 +270,9 @@ type elim_scheme = { args: rel_context; (** (xni, Ti_ni) ... (x1, Ti_1) *) nargs: int; (** number of arguments *) indarg: rel_declaration option; (** Some (H,I prm1..prmp x1...xni) - if HI is in premisses, None otherwise *) + if HI is in premisses, None otherwise *) concl: types; (** Qi x1...xni HI (f...), HI and (f...) - are optional and mutually exclusive *) + are optional and mutually exclusive *) indarg_in_concl: bool; (** true if HI appears at the end of conclusion *) farg_in_concl: bool; (** true if (f...) appears at the end of conclusion *) } diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index c5c7969a09..0c4e496650 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -1,3 +1,4 @@ +DeclareScheme Declare Proof_global Pfedit diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index ccd7a818b9..7f2a6f94b5 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -45,6 +45,7 @@ struct | DFix of int array * int * 't array * 't array | DCoFix of int * 't array * 't array | DInt of Uint63.t + | DFloat of Float64.t (* special constructors only inside the left-hand side of DCtx or DApp. Used to encode lists of foralls/letins/apps as contexts *) @@ -63,9 +64,10 @@ struct | DFix _ -> str "fix" | DCoFix _ -> str "cofix" | DInt _ -> str "INT" + | DFloat _ -> str "FLOAT" | DCons ((t,dopt),tl) -> f t ++ (match dopt with - Some t' -> str ":=" ++ f t' - | None -> str "") ++ spc() ++ str "::" ++ spc() ++ f tl + Some t' -> str ":=" ++ f t' + | None -> str "") ++ spc() ++ str "::" ++ spc() ++ f tl | DNil -> str "[]" (* @@ -74,15 +76,15 @@ struct *) let map f = function - | (DRel | DSort | DNil | DRef _ | DInt _) as c -> c + | (DRel | DSort | DNil | DRef _ | DInt _ | DFloat _) as c -> c | DCtx (ctx,c) -> DCtx (f ctx, f c) | DLambda (t,c) -> DLambda (f t, f c) | DApp (t,u) -> DApp (f t,f u) | DCase (ci,p,c,bl) -> DCase (ci, f p, f c, Array.map f bl) | DFix (ia,i,ta,ca) -> - DFix (ia,i,Array.map f ta,Array.map f ca) + DFix (ia,i,Array.map f ta,Array.map f ca) | DCoFix(i,ta,ca) -> - DCoFix (i,Array.map f ta,Array.map f ca) + DCoFix (i,Array.map f ta,Array.map f ca) | DCons ((t,topt),u) -> DCons ((f t,Option.map f topt), f u) let compare_ci ci1 ci2 = @@ -151,6 +153,10 @@ struct | DInt _, _ -> -1 | _, DInt _ -> 1 + | DFloat f1, DFloat f2 -> Float64.total_compare f1 f2 + + | DFloat _, _ -> -1 | _, DFloat _ -> 1 + | DCons ((t1, ot1), u1), DCons ((t2, ot2), u2) -> let c = cmp t1 t2 in if Int.equal c 0 then @@ -163,19 +169,19 @@ struct | DNil, DNil -> 0 let fold f acc = function - | (DRel | DNil | DSort | DRef _ | DInt _) -> acc + | (DRel | DNil | DSort | DRef _ | DInt _ | DFloat _) -> acc | DCtx (ctx,c) -> f (f acc ctx) c | DLambda (t,c) -> f (f acc t) c | DApp (t,u) -> f (f acc t) u | DCase (ci,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl | DFix (ia,i,ta,ca) -> - Array.fold_left f (Array.fold_left f acc ta) ca + Array.fold_left f (Array.fold_left f acc ta) ca | DCoFix(i,ta,ca) -> - Array.fold_left f (Array.fold_left f acc ta) ca + Array.fold_left f (Array.fold_left f acc ta) ca | DCons ((t,topt),u) -> f (Option.fold_left f (f acc t) topt) u let choose f = function - | (DRel | DSort | DNil | DRef _ | DInt _) -> invalid_arg "choose" + | (DRel | DSort | DNil | DRef _ | DInt _ | DFloat _) -> invalid_arg "choose" | DCtx (ctx,c) -> f ctx | DLambda (t,c) -> f t | DApp (t,u) -> f u @@ -192,20 +198,20 @@ struct then invalid_arg "fold2:compare" else match c1,c2 with | (DRel, DRel | DNil, DNil | DSort, DSort | DRef _, DRef _ - | DInt _, DInt _) -> acc - | (DCtx (c1,t1), DCtx (c2,t2) - | DApp (c1,t1), DApp (c2,t2) - | DLambda (c1,t1), DLambda (c2,t2)) -> f (f acc c1 c2) t1 t2 - | DCase (ci,p1,c1,bl1),DCase (_,p2,c2,bl2) -> - Array.fold_left2 f (f (f acc p1 p2) c1 c2) bl1 bl2 - | DFix (ia,i,ta1,ca1), DFix (_,_,ta2,ca2) -> - Array.fold_left2 f (Array.fold_left2 f acc ta1 ta2) ca1 ca2 - | DCoFix(i,ta1,ca1), DCoFix(_,ta2,ca2) -> - Array.fold_left2 f (Array.fold_left2 f acc ta1 ta2) ca1 ca2 - | DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) -> - f (Option.fold_left2 f (f acc t1 t2) topt1 topt2) u1 u2 + | DInt _, DInt _ | DFloat _, DFloat _) -> acc + | (DCtx (c1,t1), DCtx (c2,t2) + | DApp (c1,t1), DApp (c2,t2) + | DLambda (c1,t1), DLambda (c2,t2)) -> f (f acc c1 c2) t1 t2 + | DCase (ci,p1,c1,bl1),DCase (_,p2,c2,bl2) -> + Array.fold_left2 f (f (f acc p1 p2) c1 c2) bl1 bl2 + | DFix (ia,i,ta1,ca1), DFix (_,_,ta2,ca2) -> + Array.fold_left2 f (Array.fold_left2 f acc ta1 ta2) ca1 ca2 + | DCoFix(i,ta1,ca1), DCoFix(_,ta2,ca2) -> + Array.fold_left2 f (Array.fold_left2 f acc ta1 ta2) ca1 ca2 + | DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) -> + f (Option.fold_left2 f (f acc t1 t2) topt1 topt2) u1 u2 | (DRel | DNil | DSort | DRef _ | DCtx _ | DApp _ | DLambda _ | DCase _ - | DFix _ | DCoFix _ | DCons _ | DInt _), _ -> assert false + | DFix _ | DCoFix _ | DCons _ | DInt _ | DFloat _), _ -> assert false let map2 (f:'a -> 'b -> 'c) (c1:'a t) (c2:'b t) : 'c t = let head w = map (fun _ -> ()) w in @@ -213,24 +219,24 @@ struct then invalid_arg "map2_t:compare" else match c1,c2 with | (DRel, DRel | DSort, DSort | DNil, DNil | DRef _, DRef _ - | DInt _, DInt _) as cc -> - let (c,_) = cc in c - | DCtx (c1,t1), DCtx (c2,t2) -> DCtx (f c1 c2, f t1 t2) - | DLambda (t1,c1), DLambda (t2,c2) -> DLambda (f t1 t2, f c1 c2) - | DApp (t1,u1), DApp (t2,u2) -> DApp (f t1 t2,f u1 u2) - | DCase (ci,p1,c1,bl1), DCase (_,p2,c2,bl2) -> - DCase (ci, f p1 p2, f c1 c2, Array.map2 f bl1 bl2) - | DFix (ia,i,ta1,ca1), DFix (_,_,ta2,ca2) -> - DFix (ia,i,Array.map2 f ta1 ta2,Array.map2 f ca1 ca2) - | DCoFix (i,ta1,ca1), DCoFix (_,ta2,ca2) -> - DCoFix (i,Array.map2 f ta1 ta2,Array.map2 f ca1 ca2) - | DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) -> - DCons ((f t1 t2,Option.lift2 f topt1 topt2), f u1 u2) + | DInt _, DInt _ | DFloat _, DFloat _) as cc -> + let (c,_) = cc in c + | DCtx (c1,t1), DCtx (c2,t2) -> DCtx (f c1 c2, f t1 t2) + | DLambda (t1,c1), DLambda (t2,c2) -> DLambda (f t1 t2, f c1 c2) + | DApp (t1,u1), DApp (t2,u2) -> DApp (f t1 t2,f u1 u2) + | DCase (ci,p1,c1,bl1), DCase (_,p2,c2,bl2) -> + DCase (ci, f p1 p2, f c1 c2, Array.map2 f bl1 bl2) + | DFix (ia,i,ta1,ca1), DFix (_,_,ta2,ca2) -> + DFix (ia,i,Array.map2 f ta1 ta2,Array.map2 f ca1 ca2) + | DCoFix (i,ta1,ca1), DCoFix (_,ta2,ca2) -> + DCoFix (i,Array.map2 f ta1 ta2,Array.map2 f ca1 ca2) + | DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) -> + DCons ((f t1 t2,Option.lift2 f topt1 topt2), f u1 u2) | (DRel | DNil | DSort | DRef _ | DCtx _ | DApp _ | DLambda _ | DCase _ - | DFix _ | DCoFix _ | DCons _ | DInt _), _ -> assert false + | DFix _ | DCoFix _ | DCons _ | DInt _ | DFloat _), _ -> assert false let terminal = function - | (DRel | DSort | DNil | DRef _ | DInt _) -> true + | (DRel | DSort | DNil | DRef _ | DInt _ | DFloat _) -> true | DLambda _ | DApp _ | DCase _ | DFix _ | DCoFix _ | DCtx _ | DCons _ -> false @@ -268,8 +274,8 @@ module Make = struct module TDnet : Dnet.S with type ident=Ident.t - and type 'a structure = 'a DTerm.t - and type meta = int + and type 'a structure = 'a DTerm.t + and type meta = int = Dnet.Make(DTerm)(Ident)(Int) type t = TDnet.t @@ -322,9 +328,10 @@ struct | App (f,ca) -> Array.fold_left (fun c a -> Term (DApp (c,a))) (pat_of_constr f) (Array.map pat_of_constr ca) - | Proj (p,c) -> + | Proj (p,c) -> Term (DApp (Term (DRef (ConstRef (Projection.constant p))), pat_of_constr c)) | Int i -> Term (DInt i) + | Float f -> Term (DFloat f) and ctx_of_constr ctx c = match Constr.kind c with | Prod (_,t,c) -> ctx_of_constr (Term(DCons((pat_of_constr t,None),ctx))) c @@ -385,16 +392,16 @@ struct let dpat = under_prod (empty_ctx dpat) in TDnet.Idset.fold (fun id acc -> - let c_id = Opt.reduce (Ident.constr_of id) in - let c_id = EConstr.of_constr c_id in - let (ctx,wc) = + let c_id = Opt.reduce (Ident.constr_of id) in + let c_id = EConstr.of_constr c_id in + let (ctx,wc) = try Termops.align_prod_letin Evd.empty whole_c c_id (* FIXME *) - with Invalid_argument _ -> [],c_id in - let wc,whole_c = if Opt.direction then whole_c,wc else wc,whole_c in - try + with Invalid_argument _ -> [],c_id in + let wc,whole_c = if Opt.direction then whole_c,wc else wc,whole_c in + try let _ = Termops.filtering Evd.empty ctx Reduction.CUMUL wc whole_c in id :: acc - with Termops.CannotFilter -> (* msgnl(str"recon "++Termops.print_constr_env (Global.env()) wc); *) acc + with Termops.CannotFilter -> (* msgnl(str"recon "++Termops.print_constr_env (Global.env()) wc); *) acc ) (TDnet.find_match dpat dn) [] (* |