diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/abstract.ml | 5 | ||||
| -rw-r--r-- | tactics/ind_tables.ml | 13 | ||||
| -rw-r--r-- | tactics/tactics.ml | 101 |
3 files changed, 88 insertions, 31 deletions
diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 499152f39a..6dd9a976f9 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -158,9 +158,9 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = (* 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_constant ~internal:Declare.InternalTacticRequest ~local:true id decl + Declare.declare_private_constant ~role:Entries.Subproof ~internal:Declare.InternalTacticRequest ~local:true id decl in - let cst = Impargs.with_implicit_protection cst () in + let cst, eff = Impargs.with_implicit_protection cst () in let inst = match const.Entries.const_entry_universes with | Entries.Monomorphic_entry _ -> EInstance.empty | Entries.Polymorphic_entry (_, ctx) -> @@ -174,7 +174,6 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = let lem = mkConstU (cst, inst) in let evd = Evd.set_universe_context evd ectx in let open Safe_typing in - let eff = private_constant (Global.safe_env ()) Entries.Subproof cst in let effs = concat_private eff Entries.(snd (Future.force const.const_entry_body)) in let solve = diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index e95778a90d..b9485b8823 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -116,8 +116,7 @@ let compute_name internal id = | InternalTacticRequest -> Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name -let define internal id c poly univs = - let fd = declare_constant ~internal in +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 @@ -133,12 +132,12 @@ let define internal id c poly univs = const_entry_inline_code = false; const_entry_feedback = None; } in - let kn = fd id (DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in + let kn, eff = declare_private_constant ~role ~internal id (DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in let () = match internal with | InternalTacticRequest -> () | _-> definition_message id in - kn + kn, eff let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = let (c, ctx), eff = f mode ind in @@ -146,9 +145,8 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = let id = match idopt with | Some id -> id | None -> add_suffix mib.mind_packets.(i).mind_typename suff in - let const = define mode id c (Declareops.inductive_is_polymorphic mib) ctx in let role = Entries.Schema (ind, kind) in - let neff = Safe_typing.private_constant (Global.safe_env ()) role const in + let const, neff = define mode role id c (Declareops.inductive_is_polymorphic mib) ctx in declare_scheme kind [|ind,const|]; const, Safe_typing.concat_private neff eff @@ -165,9 +163,8 @@ let define_mutual_scheme_base kind suff f mode names mind = try Int.List.assoc i names with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in let fold i effs id cl = - let cst = define mode id cl (Declareops.inductive_is_polymorphic mib) ctx in let role = Entries.Schema ((mind, i), kind)in - let neff = Safe_typing.private_constant (Global.safe_env ()) role cst in + let cst, neff = define mode role id cl (Declareops.inductive_is_polymorphic mib) ctx in (Safe_typing.concat_private neff effs, cst) in let (eff, consts) = Array.fold_left2_map_i fold eff ids cl in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2bdfc85d6d..9dafa8bad9 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -614,7 +614,7 @@ let cofix id = mutual_cofix id [] 0 type tactic_reduction = Reductionops.reduction_function type e_tactic_reduction = Reductionops.e_reduction_function -let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigma = +let e_pf_change_decl (redfun : bool -> e_reduction_function) where env sigma decl = let open Context.Named.Declaration in match decl with | LocalAssum (id,ty) -> @@ -713,28 +713,61 @@ let e_change_in_hyp ~check ~reorder redfun (id,where) = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let hyp = Tacmach.New.pf_get_hyp id gl in - let (sigma, c) = e_pf_change_decl redfun where hyp (Proofview.Goal.env gl) sigma in + let (sigma, c) = e_pf_change_decl redfun where (Proofview.Goal.env gl) sigma hyp in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (convert_hyp ~check ~reorder c) end +type hyp_conversion = +| AnyHypConv (** Arbitrary conversion *) +| StableHypConv (** Does not introduce new dependencies on variables *) +| LocalHypConv (** Same as above plus no dependence on the named environment *) + let e_change_in_hyps ~check ~reorder f args = Proofview.Goal.enter begin fun gl -> - let fold (env, sigma) arg = - let (redfun, id, where) = f arg in - let hyp = - try lookup_named id env - with Not_found -> - raise (RefinerError (env, sigma, NoSuchHyp id)) + let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in + let (env, sigma) = match reorder with + | LocalHypConv -> + (* If the reduction function is known not to depend on the named + context, then we can perform it in parallel. *) + let fold accu arg = + let (id, redfun) = f arg in + let old = try Id.Map.find id accu with Not_found -> [] in + Id.Map.add id (redfun :: old) accu + in + let reds = List.fold_left fold Id.Map.empty args in + let evdref = ref sigma in + let map d = + let id = NamedDecl.get_id d in + match Id.Map.find id reds with + | reds -> + let d = EConstr.of_named_decl d in + let fold redfun (sigma, d) = redfun env sigma d in + let (sigma, d) = List.fold_right fold reds (sigma, d) in + let () = evdref := sigma in + EConstr.Unsafe.to_named_decl d + | exception Not_found -> d in - let (sigma, d) = e_pf_change_decl redfun where hyp env sigma in - let sign = Logic.convert_hyp ~check ~reorder env sigma d in + let sign = Environ.map_named_val map (Environ.named_context_val env) in let env = reset_with_named_context sign env in - (env, sigma) + (env, !evdref) + | StableHypConv | AnyHypConv -> + let reorder = reorder == AnyHypConv in + let fold (env, sigma) arg = + let (id, redfun) = f arg in + let hyp = + try lookup_named id env + with Not_found -> + raise (RefinerError (env, sigma, NoSuchHyp id)) + in + let (sigma, d) = redfun env sigma hyp in + let sign = Logic.convert_hyp ~check ~reorder env sigma d in + let env = reset_with_named_context sign env in + (env, sigma) + in + List.fold_left fold (env, sigma) args in - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let (env, sigma) = List.fold_left fold (env, sigma) args in let ty = Proofview.Goal.concl gl in Proofview.Unsafe.tclEVARS sigma <*> @@ -851,10 +884,12 @@ let change ~check chg c cls = let f (id, occs, where) = let occl = bind_change_occurrences occs chg in let redfun deep env sigma t = change_on_subterm ~check Reduction.CONV deep c occl env sigma t in - (redfun, id, where) + let redfun env sigma d = e_pf_change_decl redfun where env sigma d in + (id, redfun) in + let reorder = if check then AnyHypConv else StableHypConv in (* Don't check, we do it already in [change_on_subterm] *) - e_change_in_hyps ~check:false ~reorder:check f hyps + e_change_in_hyps ~check:false ~reorder f hyps end let change_concl t = @@ -881,6 +916,22 @@ let pattern_option l = e_reduct_option ~check:false (pattern_occs l,DEFAULTcast) (* The main reduction function *) +let is_local_flag env flags = + if flags.rDelta then false + else + let check = function + | EvalVarRef _ -> false + | EvalConstRef c -> Id.Set.is_empty (Environ.vars_of_global env (ConstRef c)) + in + List.for_all check flags.rConst + +let is_local_unfold env flags = + let check (_, c) = match c with + | EvalVarRef _ -> false + | EvalConstRef c -> Id.Set.is_empty (Environ.vars_of_global env (ConstRef c)) + in + List.for_all check flags + let reduce redexp cl = let trace env sigma = let open Printer in @@ -889,23 +940,33 @@ let reduce redexp cl = in Proofview.Trace.name_tactic trace begin Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in let hyps = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in let nbcl = (if cl.concl_occs = NoOccurrences then 0 else 1) + List.length hyps in let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in - let reorder = match redexp with Fold _ | Pattern _ -> true | _ -> false in + let reorder = match redexp with + | Fold _ | Pattern _ -> AnyHypConv + | Simpl (flags, _) | Cbv flags | Cbn flags | Lazy flags -> + if is_local_flag env flags then LocalHypConv else StableHypConv + | Unfold flags -> + if is_local_unfold env flags then LocalHypConv else StableHypConv + | Red _ | Hnf | CbvVm _ | CbvNative _ -> StableHypConv + | ExtraRedExpr _ -> StableHypConv (* Should we be that lenient ?*) + in begin match cl.concl_occs with | NoOccurrences -> Proofview.tclUNIT () | occs -> let redexp = bind_red_expr_occurrences occs nbcl redexp in - let redfun = Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp in + let redfun = Redexpr.reduction_of_red_expr env redexp in e_change_in_concl ~check (revert_cast redfun) end <*> let f (id, occs, where) = let redexp = bind_red_expr_occurrences occs nbcl redexp in - let (redfun, _) = Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp in + let (redfun, _) = Redexpr.reduction_of_red_expr env redexp in let redfun _ env sigma c = redfun env sigma c in - (redfun, id, where) + let redfun env sigma d = e_pf_change_decl redfun where env sigma d in + (id, redfun) in e_change_in_hyps ~check ~reorder f hyps end |