diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/elimschemes.ml | 38 | ||||
| -rw-r--r-- | tactics/elimschemes.mli | 8 | ||||
| -rw-r--r-- | tactics/equality.ml | 9 | ||||
| -rw-r--r-- | tactics/ind_tables.ml | 26 | ||||
| -rw-r--r-- | tactics/ind_tables.mli | 6 | ||||
| -rw-r--r-- | tactics/tactics.ml | 41 |
6 files changed, 79 insertions, 49 deletions
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 51f01888aa..d6fda00ad8 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -24,14 +24,14 @@ 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 @@ -47,11 +47,11 @@ let optimize_non_type_induction_scheme kind dep sort _ ind = 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 093a4c456b..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/equality.ml b/tactics/equality.ml index fc37d5a254..96b61b6994 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -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 diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 9c94f3c319..517ccfaf53 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -82,10 +82,9 @@ let is_visible_name id = 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 @@ -94,10 +93,7 @@ let define internal role id c poly univs = let univs = UState.univ_entry ~poly ctx 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) = @@ -107,7 +103,8 @@ 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 + 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 @@ -125,7 +122,8 @@ 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 @@ -153,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 7e544b09dc..d886fb67d3 100644 --- a/tactics/ind_tables.mli +++ b/tactics/ind_tables.mli @@ -45,15 +45,17 @@ val declare_individual_scheme_object : string -> ?aux:string -> 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/tactics.ml b/tactics/tactics.ml index 33c9c11350..9258a75461 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -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 @@ -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. - in which case we pose a proof with body + The goal is to pose a proof with body - (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. *) + (fun y1...yp => H t1 t2 ... tm u1 ... uq) + + 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 |