aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-08-21 14:59:06 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-08-21 15:20:52 +0200
commit1fbcea38dc9d995f7c6786b543675ba27970642e (patch)
treec1d574f081038b403313daaed905521a5964603c /proofs
parent9a24bc736d5782b7b9c23ebd4cfcf5f5f99836eb (diff)
Removing unused parts of the Goal.sensitive monad.
Some legacy code remains to keep the newish refine tactic working, but ultimately it should be removed. I did not manage to do it properly though, i.e. without breaking the test-suite furthermore.
Diffstat (limited to 'proofs')
-rw-r--r--proofs/goal.ml205
-rw-r--r--proofs/goal.mli127
-rw-r--r--proofs/proofview.ml18
-rw-r--r--proofs/proofview.mli4
4 files changed, 22 insertions, 332 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. *)