diff options
| -rw-r--r-- | proofs/goal.ml | 205 | ||||
| -rw-r--r-- | proofs/goal.mli | 127 | ||||
| -rw-r--r-- | proofs/proofview.ml | 18 | ||||
| -rw-r--r-- | proofs/proofview.mli | 4 | ||||
| -rw-r--r-- | tactics/tactics.ml | 8 | ||||
| -rw-r--r-- | tactics/tactics.mli | 3 |
6 files changed, 28 insertions, 337 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index 031e1d34c..5bbc502bd 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -152,16 +152,6 @@ let bind e f = (); fun env rdefs goal info -> let r = f a in r env rdefs goal info -(* monadic return on sensitive expressions *) -let return v = () ; fun _ _ _ _ -> v - -(* interpretation of "open" constr *) -(* spiwack: it is a wrapper around [Constrintern.interp_open_constr]. - In an ideal world, this could/should be the other way round. - As of now, though, it seems at least quite useful to build tactics. *) -let interp_constr cexpr = (); fun env rdefs _ _ -> - Constrintern.interp_constr_evars rdefs env cexpr - (* Type of constr with holes used by refine. *) (* The list of evars doesn't necessarily contain all the evars in the constr, only those the constr has introduced. *) @@ -174,26 +164,12 @@ type refinable = { } module Refinable = struct - type t = refinable - - type handle = Evd.evar list ref let make t = (); fun env rdefs gl info -> let r = ref [] in let me = t r in let me = me env rdefs gl info in { me = me; my_evars = !r } - let make_with t = (); fun env rdefs gl info -> - let r = ref [] in - let t = t r in - let (me,side) = t env rdefs gl info in - ({ me = me ; my_evars = !r }, side) - - let mkEvar handle env typ = (); fun _ rdefs _ _ -> - let ev = Evarutil.e_new_evar rdefs env typ in - let (e,_) = destEvar ev in - handle := e::!handle; - ev (* [with_type c typ] constrains term [c] to have type [typ]. *) let with_type t typ = (); fun env rdefs _ _ -> @@ -209,14 +185,6 @@ module Refinable = struct rdefs := new_defs; j'.Environ.uj_val - (* spiwack: it is not very fine grain since it solves all typeclasses holes, - not only those containing the current goal, or a given term. But it - seems to fit our needs so far. *) - let resolve_typeclasses ?filter ?split ?(fail=false) () = (); fun env rdefs _ _ -> - rdefs:=Typeclasses.resolve_typeclasses ?filter ?split ~fail env !rdefs - - - (* a pessimistic (i.e : there won't be many positive answers) filter over evar_maps, acting only on undefined evars *) let evar_map_filter_undefined f evm = @@ -270,177 +238,14 @@ let refine step = (); fun env rdefs gl info -> in { subgoals = subgoals } - -(*** Cleaning goals ***) - -let clear ids = (); fun env rdefs gl info -> - let hyps = Evd.evar_hyps info in - let concl = Evd.evar_concl info in - let (hyps,concl) = Evarutil.clear_hyps_in_evi rdefs hyps concl ids in - let cleared_env = Environ.reset_with_named_context hyps env in - let cleared_concl = Evarutil.e_new_evar rdefs cleared_env concl in - let (cleared_evar,_) = destEvar cleared_concl in - let cleared_goal = descendent gl cleared_evar in - rdefs := Evd.define gl.content cleared_concl !rdefs; - { subgoals = [cleared_goal] } - -let wrap_apply_to_hyp_and_dependent_on sign id f g = - try Environ.apply_to_hyp_and_dependent_on sign id f g - with Environ.Hyp_not_found -> - Errors.error "No such assumption" - -let check_typability env sigma c = - let _ = Typing.type_of env sigma c in () - -let recheck_typability (what,id) env sigma t = - try check_typability env sigma t - with e when Errors.noncritical e -> - let s = match what with - | None -> "the conclusion" - | Some id -> "hypothesis "^(Names.Id.to_string id) in - Errors.error - ("The correctness of "^s^" relies on the body of "^(Names.Id.to_string id)) - -let remove_hyp_body env sigma id = - let sign = - wrap_apply_to_hyp_and_dependent_on (Environ.named_context_val env) id - (fun (_,c,t) _ -> - match c with - | None -> Errors.error ((Names.Id.to_string id)^" is not a local definition") - | Some c ->(id,None,t)) - (fun (id',c,t as d) sign -> - ( - begin - let env = Environ.reset_with_named_context sign env in - match c with - | None -> recheck_typability (Some id',id) env sigma t - | Some b -> - let b' = mkCast (b,DEFAULTcast, t) in - recheck_typability (Some id',id) env sigma b' - end;d)) - in - Environ.reset_with_named_context sign env - - -let clear_body idents = (); fun env rdefs gl info -> - let info = content !rdefs gl in - let full_env = Environ.reset_with_named_context (Evd.evar_hyps info) env in - let aux env id = - let env' = remove_hyp_body env !rdefs id in - recheck_typability (None,id) env' !rdefs (Evd.evar_concl info); - env' - in - let new_env = - List.fold_left aux full_env idents - in - let concl = Evd.evar_concl info in - let (defs',new_constr) = Evarutil.new_evar !rdefs new_env concl in - let (new_evar,_) = destEvar new_constr in - let new_goal = descendent gl new_evar in - rdefs := Evd.define gl.content new_constr defs'; - { subgoals = [new_goal] } - - -(*** Sensitive primitives ***) - -(* representation of the goal in form of an {!Evd.evar_info} *) -let info _ _ _ info = info - -(* [concl] is the conclusion of the current goal *) -let concl _ _ _ info = - Evd.evar_concl info - -(* [hyps] is the [named_context_val] representing the hypotheses - of the current goal *) -let hyps _ _ _ info = - Evd.evar_hyps info - -(* [env] is the current [Environ.env] containing both the - environment in which the proof is ran, and the goal hypotheses *) -let env env _ _ _ = env - -(* [defs] is the [Evd.evar_map] at the current evaluation point *) -let defs _ rdefs _ _ = - !rdefs +let refine_open_constr c = + let pf h = Refinable.constr_of_open_constr h true c in + bind (Refinable.make pf) refine let enter f = (); fun env rdefs gl info -> let sigma = !rdefs in f env sigma (Evd.evar_hyps info) (Evd.evar_concl info) gl -(*** Conversion in goals ***) - -let convert_hyp check (id,b,bt as d) = (); fun env rdefs gl info -> - let sigma = !rdefs in - (* This function substitutes the new type and body definitions - in the appropriate variable when used with {!Environ.apply_hyps}. *) - let replace_function = - (fun _ (_,c,ct) _ -> - if check && not (Reductionops.is_conv env sigma bt ct) then - Errors.error ("Incorrect change of the type of "^(Names.Id.to_string id)); - if check && not (Option.equal (Reductionops.is_conv env sigma) b c) then - Errors.error ("Incorrect change of the body of "^(Names.Id.to_string id)); - d) - in - (* Modified named context. *) - let new_hyps = - let hyps = hyps env rdefs gl info in - Environ.apply_to_hyp hyps id replace_function - in - let new_env = Environ.reset_with_named_context new_hyps env in - let new_constr = - let concl = concl env rdefs gl info in - Evarutil.e_new_evar rdefs new_env concl - in - let (new_evar,_) = destEvar new_constr in - let new_goal = descendent gl new_evar in - rdefs := Evd.define gl.content new_constr !rdefs; - { subgoals = [new_goal] } - -let convert_concl check cl' = (); fun env rdefs gl info -> - let sigma = !rdefs in - let cl = concl env rdefs gl info in - check_typability env sigma cl'; - if (not check) || Reductionops.is_conv_leq env sigma cl' cl then - let new_constr = - Evarutil.e_new_evar rdefs env cl' - in - let (new_evar,_) = destEvar new_constr in - let new_goal = descendent gl new_evar in - rdefs := Evd.define gl.content new_constr !rdefs; - { subgoals = [new_goal] } - else - Errors.error "convert-concl rule passed non-converting term" - - -(*** Bureaucracy in hypotheses ***) - -(* Renames a hypothesis. *) -let rename_hyp_sign id1 id2 sign = - let subst = [id1,mkVar id2] in - let replace_vars c = replace_vars subst c in - Environ.apply_to_hyp_and_dependent_on sign id1 - (fun (_,b,t) _ -> (id2,b,t)) - (fun d _ -> map_named_declaration replace_vars d) - -let rename_hyp id1 id2 = (); fun env rdefs gl info -> - let hyps = hyps env rdefs gl info in - if not (Names.Id.equal id1 id2) && - Names.Id.List.mem id2 - (Termops.ids_of_named_context (Environ.named_context_of_val hyps)) - then - Errors.error ((Names.Id.to_string id2)^" is already used."); - let new_hyps = rename_hyp_sign id1 id2 hyps in - let new_env = Environ.reset_with_named_context new_hyps env in - let old_concl = concl env rdefs gl info in - let new_concl = Vars.replace_vars [id1,mkVar id2] old_concl in - let new_subproof = Evarutil.e_new_evar rdefs new_env new_concl in - let new_subproof = Vars.replace_vars [id2,mkVar id1] new_subproof in - let (new_evar,_) = destEvar new_subproof in - let new_goal = descendent gl new_evar in - rdefs := Evd.define gl.content new_subproof !rdefs; - { subgoals = [new_goal] } - - (* Layer to implement v8.2 tactic engine ontop of the new architecture. Types are different from what they used to be due to a change of the internal types. *) @@ -579,8 +384,4 @@ module V82 = struct t ) ~init:(concl sigma gl) env - let to_sensitive f = (); fun _ rsigma g _ -> - f { Evd.it = g ; sigma = !rsigma } - let change_evar_map sigma = (); fun _ rsigma _ _ -> - (rsigma := sigma) end diff --git a/proofs/goal.mli b/proofs/goal.mli index 988853382..535a2f2b1 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -42,112 +42,6 @@ val equal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool non-unifiable goals. *) val partition_unifiable : Evd.evar_map -> goal list -> goal list * goal list -(*** Goal tactics ***) - - -(* Goal tactics are [subgoal sensitive]-s *) -type subgoals = private { subgoals: goal list } - -(* Goal sensitive values *) -type +'a sensitive - -(* evaluates a goal sensitive value in a given goal (knowing the current evar_map). *) -val eval : - 'a sensitive -> Environ.env -> Evd.evar_map -> goal -> - 'a * Evd.evar_map - -(* monadic bind on sensitive expressions *) -val bind : 'a sensitive -> ('a -> 'b sensitive) -> 'b sensitive - -(* monadic return on sensitive expressions *) -val return : 'a -> 'a sensitive - - -(* interpretation of "open" constr *) -(* spiwack: it is a wrapper around [Constrintern.interp_open_constr]. - In an ideal world, this could/should be the other way round. - As of now, though, it seems at least quite useful to build tactics. *) -val interp_constr : Constrexpr.constr_expr -> Term.constr sensitive - -(* Type of constr with holes used by refine. *) -type refinable - -module Refinable : sig - type t = refinable - type handle - - val make : (handle -> Term.constr sensitive) -> refinable sensitive - val make_with : (handle -> (Term.constr*'a) sensitive) -> (refinable*'a) sensitive - - val mkEvar : handle -> Environ.env -> Term.types -> Term.constr sensitive - - (* [with_type c typ] constrains term [c] to have type [typ]. *) - val with_type : Term.constr -> Term.types -> Term.constr sensitive - - val resolve_typeclasses : ?filter:Typeclasses.evar_filter -> ?split:bool -> ?fail:bool -> unit -> unit sensitive - - - (* [constr_of_open_constr h check_type] transforms an open constr into a - goal-sensitive constr, adding the undefined variables to the set of subgoals. - If [check_type] is true, the term is coerced to the conclusion of the goal. - It allows to do refinement with already-built terms with holes. - *) - val constr_of_open_constr : handle -> bool -> Evd.open_constr -> Term.constr sensitive - -end - -(* [refine t] takes a refinable term and use it as a partial proof for current - goal. *) -val refine : refinable -> subgoals sensitive - - -(*** Cleaning goals ***) - -(* Implements the [clear] tactic *) -val clear : Names.Id.Set.t -> subgoals sensitive - -(* Implements the [clearbody] tactic *) -val clear_body : Names.Id.t list -> subgoals sensitive - - -(*** Conversion in goals ***) - -(* Changes an hypothesis of the goal with a convertible type and body. - Checks convertibility if the boolean argument is true. *) -val convert_hyp : bool -> Context.named_declaration -> subgoals sensitive - -(* Changes the conclusion of the goal with a convertible type and body. - Checks convertibility if the boolean argument is true. *) -val convert_concl : bool -> Term.constr -> subgoals sensitive - -(*** Bureaucracy in hypotheses ***) - -(* Renames a hypothesis. *) -val rename_hyp : Names.Id.t -> Names.Id.t -> subgoals sensitive - -(*** Sensitive primitives ***) - -(* representation of the goal in form of an {!Evd.evar_info} *) -val info : Evd.evar_info sensitive - -(* [concl] is the conclusion of the current goal *) -val concl : Term.constr sensitive - -(* [hyps] is the [named_context_val] representing the hypotheses - of the current goal *) -val hyps : Environ.named_context_val sensitive - -(* [env] is the current [Environ.env] containing both the - environment in which the proof is ran, and the goal hypotheses *) -val env : Environ.env sensitive - -(* [defs] is the [Evd.evar_map] at the current evaluation point *) -val defs : Evd.evar_map sensitive - -(* [enter] combines [env], [defs], [hyps] and [concl] in a single - primitive. *) -val enter : (Environ.env -> Evd.evar_map -> Environ.named_context_val -> Term.constr -> goal -> 'a) -> 'a sensitive - (* Layer to implement v8.2 tactic engine ontop of the new architecture. Types are different from what they used to be due to a change of the internal types. *) @@ -220,6 +114,23 @@ module V82 : sig (* Goal represented as a type, doesn't take into account section variables *) val abstract_type : Evd.evar_map -> goal -> Term.types - val to_sensitive : (goal Evd.sigma -> 'a) -> 'a sensitive - val change_evar_map : Evd.evar_map -> unit sensitive end + +(*** Goal tactics. DEPRECATED. ***) + +(* Goal tactics are [subgoal sensitive]-s *) +type subgoals = private { subgoals: goal list } + +(* Goal sensitive values *) +type +'a sensitive + +(* evaluates a goal sensitive value in a given goal (knowing the current evar_map). *) +val eval : + 'a sensitive -> Environ.env -> Evd.evar_map -> goal -> + 'a * Evd.evar_map + +val refine_open_constr : Evd.open_constr -> subgoals sensitive + +(* [enter] combines [env], [defs], [hyps] and [concl] in a single + primitive. *) +val enter : (Environ.env -> Evd.evar_map -> Environ.named_context_val -> Term.constr -> goal -> 'a) -> 'a sensitive diff --git a/proofs/proofview.ml b/proofs/proofview.ml index f1759548e..a75059891 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -851,24 +851,6 @@ module Goal = struct let hyps { hyps=hyps } = Environ.named_context_of_val hyps let concl { concl=concl } = concl - let lift s k = - (* spiwack: convenience notations, waiting for ocaml 3.12 *) - let (>>=) = Proof.bind in - let (>>) = Proof.seq in - Proof.current >>= fun env -> - Proof.get >>= fun step -> - try - let (ks,sigma) = - Evd.Monad.List.map begin fun g sigma -> - Util.on_fst k (Goal.eval s env sigma g) - end step.comb step.solution - in - Proof.set { step with solution=sigma } >> - tclDISPATCH ks - with e when catchable_exception e -> - let e = Errors.push e in - tclZERO e - let enter_t f = Goal.enter begin fun env sigma hyps concl self -> let concl = Reductionops.nf_evar sigma concl in let map_nf c = Reductionops.nf_evar sigma c in diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 288a46cb7..4472bbcb7 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -394,10 +394,6 @@ module Goal : sig val env : 'a t -> Environ.env val sigma : 'a t -> Evd.evar_map - (* [lift_sensitive s k] applies [s] in each goal independently - raising result [a] then continues with [k a]. *) - val lift : 'a Goal.sensitive -> ('a->unit tactic) -> unit tactic - (* [enter t] execute the goal-dependent tactic [t] in each goal independently. In particular [t] need not backtrack the same way in each goal. *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 62c3a8fc1..7a8bb36b9 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4050,11 +4050,9 @@ module New = struct open Locus let refine c = - let c = Goal.Refinable.make begin fun h -> - Goal.Refinable.constr_of_open_constr h true c - end in - Proofview.Goal.lift c begin fun c -> - Proofview.tclSENSITIVE (Goal.refine c) <*> + Proofview.Goal.enter begin fun gl -> + let pf = Goal.refine_open_constr c in + Proofview.tclSENSITIVE pf <*> Proofview.V82.tactic (reduce (Lazy {rBeta=true;rIota=true;rZeta=false;rDelta=false;rConst=[]}) {onhyps=None; concl_occs=AllOccurrences } diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 238b95a46..e5ba7f14c 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -429,6 +429,9 @@ end module New : sig val refine : Evd.open_constr -> unit Proofview.tactic + (** DEPRECATED. Legacy refine tactic. You should not be using this code, as + it may be unsound to manipulate evar maps without care. Use the + [Proofview.Refine] module instead. *) open Proofview val exact_proof : Constrexpr.constr_expr -> unit tactic |