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.

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. *)