Goal: remove most of the API (make [Goal.goal] concrete).

We are left with the compatibility layer and a handful of primitives which require some thought to move.

3 files changed, 90 insertions, 181 deletions

diff --git a/proofs/goal.ml b/proofs/goal.ml
index 395f82753..544282c4d 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -21,24 +21,6 @@ type goal = Evd.evar
 
 let pr_goal e = str "GOAL:" ++ Pp.int (Evar.repr e)
 
-let goal_ident sigma e = Evd.evar_ident e sigma
-
-let dependent_goal_ident sigma e = Evd.dependent_evar_ident e sigma
-
-(* access primitive *)
-(* invariant : [e] must exist in [em] *)
-let content evars e = Evd.find evars e
-
-
-(* Builds a new (empty) goal with evar [e] *)
-let build e = e
-
-let mark_as_goal evd content =
-  let info = Evd.find evd content in
-  let info = { info with Evd.evar_source = (fst (info.Evd.evar_source),Evar_kinds.GoalEvar) } in
-  let info = Typeclasses.mark_unresolvable info in
-  Evd.add evd content info
-
 let uid e = string_of_int (Evar.repr e)
 let get_by_uid u = Evar.unsafe_of_int (int_of_string u)
 
@@ -63,79 +45,6 @@ let rec advance sigma g =
       else
         None
 
-let solution sigma g =
-  let evi = Evd.find sigma g in
-  match evi.Evd.evar_body with
-  | Evd.Evar_empty -> None
-  | Evd.Evar_defined v -> Some v
-
-(* Equality function on goals *)
-let equal evars1 gl1 evars2 gl2 =
-  let evi1 = content evars1 gl1 in
-  let evi2 = content evars2 gl2 in
-  Evd.eq_evar_info evars2 evi1 evi2
-
-(* [contained_in_info e evi] checks whether the evar [e] appears in
-   the hypotheses, the conclusion or the body of the evar_info
-   [evi]. Note: since we want to use it on goals, the body is actually
-   supposed to be empty. *)
-let contained_in_info sigma e evi =
-  Evar.Set.mem e (Evd.evars_of_filtered_evar_info (Evarutil.nf_evar_info sigma evi))
-
-(* [depends_on sigma src tgt] checks whether the goal [src] appears as an
-   existential variable in the definition of the goal [tgt] in [sigma]. *)
-let depends_on sigma src tgt =
-  let evi = Evd.find sigma tgt in
-  contained_in_info sigma src evi
-
-(* [unifiable sigma g l] checks whether [g] appears in another subgoal
-   of [l]. The list [l] may contain [g], but it does not affect the
-   result. *)
-let unifiable sigma g l =
-  List.exists (fun tgt -> g != tgt && depends_on sigma g tgt) l
-
-(* [partition_unifiable sigma l] partitions [l] into a pair [(u,n)]
-   where [u] is composed of the unifiable goals, i.e. the goals on
-   whose definition other goals of [l] depend, and [n] are the
-   non-unifiable goals. *)
-let partition_unifiable sigma l =
-  List.partition (fun g -> unifiable sigma g l) l
-
-(*** Goal tactics ***)
-
-
-(* type of the base elements of the goal API.*)
-(* it has an extra evar_info with respect to what would be expected,
-   it is supposed to be the evar_info of the goal in the evar_map.
-   The idea is that it is computed by the [run] function as an
-   optimisation, since it will generaly not change during the
-   evaluation. *)
-type 'a sensitive =
-    Environ.env -> Evd.evar_map ref -> goal -> Evd.evar_info -> 'a
-
-(* evaluates a goal sensitive value in a given goal (knowing the current evar_map). *)
-(* the evar_info corresponding to the goal is computed at once
-   as an optimisation (it shouldn't change during the evaluation). *)
-let eval t env defs gl =
-  let info = content defs gl in
-  let env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env in
-  let rdefs = ref defs in
-  let r = t env rdefs gl info in
-  ( r , !rdefs )
-
-let enter f = (); fun env rdefs gl info ->
-  let sigma = !rdefs in
-  f env sigma (Evd.evar_concl info) gl
-
-let nf_enter f = (); fun env rdefs gl info ->
-  let sigma = !rdefs in
-  let info = Evarutil.nf_evar_info sigma info in
-  let sigma = Evd.add sigma gl info in
-  let () = rdefs := sigma in
-  let hyps = Evd.evar_filtered_hyps info in
-  let env = Environ.reset_with_named_context hyps env in
-  f env sigma (Evd.evar_concl info) gl
-
 (* 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. *)
@@ -143,7 +52,7 @@ module V82 = struct
 
   (* Old style env primitive *)
   let env evars gl =
-    let evi = content evars gl in
+    let evi = Evd.find evars gl in
     Evd.evar_filtered_env evi
 
   (* same as [env], but ensures that existential variables are
@@ -153,7 +62,7 @@ module V82 = struct
 
   (* Old style hyps primitive *)
   let hyps evars gl =
-    let evi = content evars gl in
+    let evi = Evd.find evars gl in
     Evd.evar_filtered_hyps evi
 
   (* same as [hyps], but ensures that existential variables are
@@ -164,7 +73,7 @@ module V82 = struct
 
   (* Access to ".evar_concl" *)
   let concl evars gl =
-    let evi = content evars gl in
+    let evi = Evd.find evars gl in
     evi.Evd.evar_concl
 
   (* same as [concl] but ensures that existential variables are
@@ -174,12 +83,12 @@ module V82 = struct
 
   (* Access to ".evar_extra" *)
   let extra evars gl =
-    let evi = content evars gl in
+    let evi = Evd.find evars gl in
     evi.Evd.evar_extra
 
   (* Old style filtered_context primitive *)
   let filtered_context evars gl =
-    let evi = content evars gl in
+    let evi = Evd.find evars gl in
     Evd.evar_filtered_context evi
 
   (* Old style mk_goal primitive *)
@@ -197,7 +106,7 @@ module V82 = struct
     let ctxt = Environ.named_context_of_val hyps in
     let inst = Array.map_of_list (fun (id, _, _) -> mkVar id) ctxt in
     let ev = Term.mkEvar (evk,inst) in
-    (build evk, ev, evars)
+    (evk, ev, evars)
 
   (* Creates a dummy [goal sigma] for use in auto *)
   let dummy_goal =
@@ -206,10 +115,10 @@ module V82 = struct
        to have functional content. *)
     let evi = Evd.make_evar Environ.empty_named_context_val Term.mkProp in
     let (sigma, evk) = Evarutil.new_pure_evar_full Evd.empty evi in
-    { Evd.it = build evk ; Evd.sigma = sigma; }
+    { Evd.it = evk ; Evd.sigma = sigma; }
 
   (* Makes a goal out of an evar *)
-  let build = build
+  let build e = e
 
   (* Instantiates a goal with an open term *)
   let partial_solution sigma evk c =
@@ -222,8 +131,8 @@ module V82 = struct
 
   (* Parts of the progress tactical *)
   let same_goal evars1 gl1 evars2 gl2 =
-    let evi1 = content evars1 gl1 in
-    let evi2 = content evars2 gl2 in
+    let evi1 = Evd.find evars1 gl1 in
+    let evi2 = Evd.find evars2 gl2 in
     Term.eq_constr evi1.Evd.evar_concl evi2.Evd.evar_concl &&
     Environ.eq_named_context_val evi1.Evd.evar_hyps evi2.Evd.evar_hyps
 
@@ -243,7 +152,7 @@ module V82 = struct
 
   (* Used for congruence closure and change *)
   let new_goal_with sigma gl extra_hyps =
-    let evi = content sigma gl in
+    let evi = Evd.find sigma gl in
     let hyps = evi.Evd.evar_hyps in
     let new_hyps =
       List.fold_right Environ.push_named_context_val extra_hyps hyps in
@@ -257,7 +166,7 @@ module V82 = struct
 
   (* Used by the compatibility layer and typeclasses *)
   let nf_evar sigma gl =
-    let evi = content sigma gl in
+    let evi = Evd.find sigma gl in
     let evi = Evarutil.nf_evar_info sigma evi in
     let sigma = Evd.add sigma gl evi in
     (gl, sigma)
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 1be315c54..7c8fdef29 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -8,14 +8,7 @@
 
 (* This module implements the abstract interface to goals *)
 
-type goal
-
-(* spiwack: this primitive is not extremely brilliant. It may be a good
-    idea to define goals and proof views in the same file to avoid this
-    sort of communication pipes. But I find it heavy. *)
-val build : Evd.evar -> goal 
-
-val mark_as_goal : Evd.evar_map -> goal -> Evd.evar_map
+type goal = Evar.t
 
 (* Gives a unique identifier to each goal. The identifier is
    guaranteed to contain no space. *)
@@ -27,26 +20,11 @@ val get_by_uid : string -> goal
 (* Debugging help *)
 val pr_goal : goal -> Pp.std_ppcmds
 
-val goal_ident : Evd.evar_map -> goal -> Names.Id.t
-
-val dependent_goal_ident : Evd.evar_map -> goal -> Names.Id.t
-
 (* [advance sigma g] returns [Some g'] if [g'] is undefined and 
     is the current avatar of [g] (for instance [g] was changed by [clear]
     into [g']). It returns [None] if [g] has been (partially) solved. *)
 val advance : Evd.evar_map -> goal -> goal option
 
-val solution : Evd.evar_map -> goal -> Term.constr option
-
-(* Equality function on goals. Return [true] if all of its hypotheses
-   and conclusion are equal. *)
-val equal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool
-
-(* [partition_unifiable sigma l] partitions [l] into a pair [(u,n)]
-   where [u] is composed of the unifiable goals, i.e. the goals on
-   whose definition other goals of [l] depend, and [n] are the
-   non-unifiable goals. *)
-val partition_unifiable : Evd.evar_map -> goal list -> goal list * goal list
 
 (* 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
@@ -124,19 +102,3 @@ module V82 : sig
   val abstract_type : Evd.evar_map -> goal -> Term.types 
 
 end
-
-(*** Goal tactics. DEPRECATED. ***)
-
-(* 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
-
-(* [enter] combines [env], [defs], [hyps] and [concl] in a single
-   primitive. *)
-val enter : (Environ.env -> Evd.evar_map -> Term.constr -> goal -> 'a) -> 'a sensitive
-
-val nf_enter : (Environ.env -> Evd.evar_map -> Term.constr -> goal -> 'a) -> 'a sensitive
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 9110cb4f1..e6c8032bf 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -42,8 +42,7 @@ let init sigma =
     let src = (Loc.ghost,Evar_kinds.GoalEvar) in
     let naming = Misctypes.IntroIdentifier (Names.Id.of_string "Main") in
     let (new_defs , econstr) = Evarutil.new_evar env sol ~src ~naming typ in
-    let (e, _) = Term.destEvar econstr in
-    let gl = Goal.build e in
+    let (gl, _) = Term.destEvar econstr in
     let entry = (econstr, typ) :: ret in
     entry, { solution = new_defs; comb = gl::comb; }
   in
@@ -62,8 +61,7 @@ let dependent_init =
   | TCons (env, sigma, typ, t) ->
     let (sigma, econstr ) = Evarutil.new_evar env sigma typ in
     let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in
-    let (e, _) = Term.destEvar econstr in
-    let gl = Goal.build e in
+    let (gl, _) = Term.destEvar econstr in
     let entry = (econstr, typ) :: ret in
     entry, { solution = sol; comb = gl :: comb; }
   in
@@ -337,7 +335,7 @@ let tclFOCUSID id t =
   let rec aux n = function
     | [] -> tclZERO (NoSuchGoals 1)
     | g::l ->
-        if Names.Id.equal (Goal.goal_ident initial.solution g) id then
+        if Names.Id.equal (Evd.evar_ident g initial.solution) id then
           let (focused,context) = focus n n initial in
           Proof.set focused >>
             t >>= fun result ->
@@ -545,6 +543,12 @@ let tclNEWGOALS gls =
   { step with comb = step.comb @ gls }
   end
 
+(* Equality function on goals *)
+let goal_equal evars1 gl1 evars2 gl2 =
+  let evi1 = Evd.find evars1 gl1 in
+  let evi2 = Evd.find evars2 gl2 in
+  Evd.eq_evar_info evars2 evi1 evi2
+
 let tclPROGRESS t =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
@@ -553,7 +557,7 @@ let tclPROGRESS t =
   Proof.get >>= fun final ->
   let test =
     Evd.progress_evar_map initial.solution final.solution &&
-    not (Util.List.for_all2eq (fun i f -> Goal.equal initial.solution i final.solution f) initial.comb final.comb)
+    not (Util.List.for_all2eq (fun i f -> goal_equal initial.solution i final.solution f) initial.comb final.comb)
   in
   if test then
     tclUNIT res
@@ -650,6 +654,33 @@ let shelve =
   Proof.set {initial with comb=[]} >>
   Proof.put (true,(initial.comb,[]))
 
+
+(* [contained_in_info e evi] checks whether the evar [e] appears in
+   the hypotheses, the conclusion or the body of the evar_info
+   [evi]. Note: since we want to use it on goals, the body is actually
+   supposed to be empty. *)
+let contained_in_info sigma e evi =
+  Evar.Set.mem e (Evd.evars_of_filtered_evar_info (Evarutil.nf_evar_info sigma evi))
+
+(* [depends_on sigma src tgt] checks whether the goal [src] appears as an
+   existential variable in the definition of the goal [tgt] in [sigma]. *)
+let depends_on sigma src tgt =
+  let evi = Evd.find sigma tgt in
+  contained_in_info sigma src evi
+
+(* [unifiable sigma g l] checks whether [g] appears in another subgoal
+   of [l]. The list [l] may contain [g], but it does not affect the
+   result. *)
+let unifiable sigma g l =
+  List.exists (fun tgt -> g != tgt && depends_on sigma g tgt) l
+
+(* [partition_unifiable sigma l] partitions [l] into a pair [(u,n)]
+   where [u] is composed of the unifiable goals, i.e. the goals on
+   whose definition other goals of [l] depend, and [n] are the
+   non-unifiable goals. *)
+let partition_unifiable sigma l =
+  List.partition (fun g -> unifiable sigma g l) l
+
 (* Shelves the unifiable goals under focus, i.e. the goals which
    appear in other goals under focus (the unfocused goals are not
    considered). *)
@@ -658,18 +689,18 @@ let shelve_unifiable =
   let (>>=) = Proof.bind in
   let (>>) = Proof.seq in
   Proof.get >>= fun initial ->
-  let (u,n) = Goal.partition_unifiable initial.solution initial.comb in
+  let (u,n) = partition_unifiable initial.solution initial.comb in
   Proof.set {initial with comb=n} >>
   Proof.put (true,(u,[]))
 
 let check_no_dependencies =
   let (>>=) = Proof.bind in
   Proof.get >>= fun initial ->
-  let (u,n) = Goal.partition_unifiable initial.solution initial.comb in
+  let (u,n) = partition_unifiable initial.solution initial.comb in
   match u with
   | [] -> tclUNIT ()
   | gls ->
-      let l = List.map (Goal.dependent_goal_ident initial.solution) gls in
+      let l = List.map (fun g -> Evd.dependent_evar_ident g initial.solution) gls in
       let l = List.map (fun id -> Names.Name id) l in
       tclZERO (Logic.RefinerError (Logic.UnresolvedBindings l))
 
@@ -809,11 +840,7 @@ module V82 = struct
   (* Main function in the implementation of Grab Existential Variables.*)
   let grab pv =
     let undef = Evd.undefined_map pv.solution in
-    let goals =
-      List.map begin fun (e,_) ->
-	Goal.build e
-      end (Evar.Map.bindings undef)
-    in
+    let goals = List.map fst (Evar.Map.bindings undef) in
     { pv with comb = goals }
       
     
@@ -869,8 +896,6 @@ module V82 = struct
 end
 
 type goal = Goal.goal
-let build_goal = Goal.build
-let mark_as_goal = Goal.mark_as_goal
 let partial_solution = Goal.V82.partial_solution
 let partial_solution_to = Goal.V82.partial_solution_to
 
@@ -892,16 +917,24 @@ module Goal = struct
 
   let raw_concl { concl=concl } = concl
 
-  let nf_enter_t = Goal.nf_enter begin fun env sigma concl self ->
-    {env=env;sigma=sigma;concl=concl;self=self}
-  end
+
+  let gmake_with info env sigma goal = 
+    { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ;
+      sigma = sigma ;
+      concl = Evd.evar_concl info ;
+      self = goal }
+
+  let nf_gmake env sigma goal =
+    let info = Evarutil.nf_evar_info sigma (Evd.find sigma goal) in
+    let sigma = Evd.add sigma goal info in
+    gmake_with info env sigma goal , sigma
 
   let nf_enter f =
     list_iter_goal () begin fun goal () ->
       Proof.current >>= fun env ->
       tclEVARMAP >>= fun sigma ->
       try
-        let (gl, sigma) = Goal.eval nf_enter_t env sigma goal in
+        let (gl, sigma) = nf_gmake env sigma goal in
         tclTHEN (V82.tclEVARS sigma) (f gl)
       with e when catchable_exception e ->
         let e = Errors.push e in
@@ -911,21 +944,18 @@ module Goal = struct
   let normalize { self } =
     Proof.current >>= fun env ->
     tclEVARMAP >>= fun sigma ->
-    let (gl,sigma) = Goal.eval nf_enter_t env sigma self in
+    let (gl,sigma) = nf_gmake env sigma self in
     tclTHEN (V82.tclEVARS sigma) (tclUNIT gl)
 
-  let enter_t f = Goal.enter begin fun env sigma concl self ->
-    f {env=env;sigma=sigma;concl=concl;self=self}
-  end
+  let gmake env sigma goal =
+    let info = Evd.find sigma goal in
+    gmake_with info env sigma goal
 
   let enter f =
     list_iter_goal () begin fun goal () ->
       Proof.current >>= fun env ->
       tclEVARMAP >>= fun sigma ->
-      try
-        (* raw_enter_t cannot modify the sigma. *)
-        let (t,_) = Goal.eval (enter_t f) env sigma goal in
-        t
+      try f (gmake env sigma goal)
       with e when catchable_exception e ->
         let e = Errors.push e in
         tclZERO e
@@ -941,9 +971,7 @@ module Goal = struct
       | Some goal ->
         let gl =
           tclEVARMAP >>= fun sigma ->
-          (** The sigma is unchanged. *)
-          let (gl, _) = Goal.eval (enter_t (fun gl -> gl)) env sigma goal in
-          tclUNIT gl
+          tclUNIT (gmake env sigma goal)
         in
         Some gl
     in
@@ -960,13 +988,13 @@ end
 module Refine =
 struct
 
-  let with_type env evd c t =
-    let my_type = Retyping.get_type_of env evd c in
-    let j = Environ.make_judge c my_type in
-    let (evd,j') =
-      Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t
+  let mark_as_goal evd content =
+    let info = Evd.find evd content in
+    let info =
+      { info with Evd.evar_source = (fst (info.Evd.evar_source),Evar_kinds.GoalEvar) }
     in
-    evd , j'.Environ.uj_val
+    let info = Typeclasses.mark_unresolvable info in
+    Evd.add evd content info
 
   let typecheck_evar ev env sigma =
     let info = Evd.find sigma ev in
@@ -995,13 +1023,23 @@ struct
     (** Proceed to the refinement *)
     let sigma = match evkmain with
       | None -> partial_solution sigma gl.Goal.self c 
-      | Some evk -> partial_solution_to sigma gl.Goal.self (build_goal evk) c in
+      | Some evk -> partial_solution_to sigma gl.Goal.self evk c in
     (** Select the goals *)
-    let comb = undefined sigma (List.rev_map build_goal evs) in
+    let comb = undefined sigma (List.rev evs) in
     let sigma = List.fold_left mark_as_goal sigma comb in
     Proof.set { solution = Evd.reset_future_goals sigma; comb; }
   end
 
+  (** Useful definitions *)
+
+  let with_type env evd c t =
+    let my_type = Retyping.get_type_of env evd c in
+    let j = Environ.make_judge c my_type in
+    let (evd,j') =
+      Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t
+    in
+    evd , j'.Environ.uj_val
+
   let refine_casted ?(unsafe = false) f = Goal.enter begin fun gl ->
     let concl = Goal.concl gl in
     let env = Goal.env gl in