Adding phantom types to discriminate normalized goals, and adding a way to

observe non-normalized goals.

5 files changed, 55 insertions, 24 deletions

diff --git a/proofs/goal.ml b/proofs/goal.ml
index b0fded2890..64eeb69d90 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -375,10 +375,7 @@ let defs _ rdefs _ _ =
 
 let enter f = (); fun env rdefs gl info ->
   let sigma = !rdefs in
-  let concl = Reductionops.nf_evar sigma (Evd.evar_concl info) in
-  let map_nf c = Reductionops.nf_evar sigma c in
-  let hyps = Environ.map_named_val map_nf (Evd.evar_hyps info) in
-  f env sigma hyps concl gl
+  f env sigma (Evd.evar_hyps info) (Evd.evar_concl info) gl
 
 (*** Conversion in goals ***)
 
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 1365fe86e7..67893e3b78 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -768,7 +768,7 @@ end
 
 module Goal = struct
 
-  type t = {
+  type 'a t = {
     env : Environ.env;
     sigma : Evd.evar_map;
     hyps : Environ.named_context_val;
@@ -776,6 +776,8 @@ module Goal = struct
     self : Goal.goal ; (* for compatibility with old-style definitions *)
   }
 
+  let assume (gl : 'a t) = (gl :> [ `NF ] t)
+
   let env { env=env } = env
   let sigma { sigma=sigma } = sigma
   let hyps { hyps=hyps } = Environ.named_context_of_val hyps
@@ -800,8 +802,12 @@ module Goal = struct
       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
+    let hyps = Environ.map_named_val map_nf hyps in
     f {env=env;sigma=sigma;hyps=hyps;concl=concl;self=self}
   end
+
   let enter f =
     list_iter_goal () begin fun goal () ->
       Proof.current >>= fun env ->
@@ -815,6 +821,22 @@ module Goal = struct
         tclZERO e
     end
 
+  let raw_enter_t f = Goal.enter begin fun env sigma hyps concl self ->
+    f {env=env;sigma=sigma;hyps=hyps;concl=concl;self=self}
+  end
+
+  let raw_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 (raw_enter_t f) env sigma goal in
+        t
+      with e when catchable_exception e ->
+        let e = Errors.push e in
+        tclZERO e
+    end
 
   (* compatibility *)
   let goal { self=self } = self
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 7e2d374d5b..7be8f6003b 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -335,17 +335,24 @@ end
    Eventually I'll try to remove it in favour of [Proofview.Goal] *)
 module Goal : sig
 
-  (* The type of goals *)
-  type t
+  (** The type of goals. The parameter type is a phantom argument indicating
+      whether the data contained in the goal has been normalized w.r.t. the
+      current sigma. If it is the case, it is flagged [ `NF ]. You may still
+      access the un-normalized data using {!assume} if you known you do not rely
+      on the assumption of being normalized, at your own risk. *)
+  type 'a t
+
+  (** Assume that you do not need the goal to be normalized. *)
+  val assume : 'a t -> [ `NF ] t
 
   (* [concl], [hyps], [env] and [sigma] given a goal [gl] return
      respectively the conclusion of [gl], the hypotheses of [gl], the
      environment of [gl] (i.e. the global environment and the hypotheses)
      and the current evar map. *)
-  val concl : t -> Term.constr
-  val hyps : t -> Context.named_context
-  val env : t -> Environ.env
-  val sigma : t -> Evd.evar_map
+  val concl : [ `NF ] t -> Term.constr
+  val hyps : [ `NF ] t -> Context.named_context
+  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]. *)
@@ -354,15 +361,16 @@ module Goal : sig
   (* [enter t] execute the goal-dependent tactic [t] in each goal
      independently. In particular [t] need not backtrack the same way in
      each goal. *)
-  val enter : (t -> unit tactic) -> unit tactic
+  val enter : ([ `NF ] t -> unit tactic) -> unit tactic
 
+  val raw_enter : ([ `LZ ] t -> unit tactic) -> unit tactic
 
   (* compatibility: avoid if possible *)
-  val goal : t -> Goal.goal
+  val goal : [ `NF ] t -> Goal.goal
 
   (** [refresh g] updates the [sigma g] to the current value, may be
       useful with compatibility functions like [Tacmach.New.of_old] *)
-  val refresh_sigma : t -> t tactic
+  val refresh_sigma : 'a t -> 'a t tactic
 end
 
 (* The [NonLogical] module allows to execute side effects in tactics
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 9a03df0417..adeb507416 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -212,6 +212,8 @@ module New = struct
     f { Evd.it = Proofview.Goal.goal gl ; sigma = Proofview.Goal.sigma gl }
 
   let pf_global id gl =
+    (** We only check for the existence of an [id] in [hyps] *)
+    let gl = Proofview.Goal.assume gl in
     let hyps = Proofview.Goal.hyps gl in
     Constrintern.construct_reference hyps id
 
@@ -221,6 +223,8 @@ module New = struct
 
 
   let pf_ids_of_hyps gl =
+    (** We only get the identifiers in [hyps] *)
+    let gl = Proofview.Goal.assume gl in
     let hyps = Proofview.Goal.hyps gl in
     ids_of_named_context hyps
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 10f6be1d5d..07639f475d 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -130,17 +130,17 @@ val pr_glls   : goal list sigma -> Pp.std_ppcmds
 
 (* Variants of [Tacmach] functions built with the new proof engine *)
 module New : sig
-  val pf_apply : (env -> evar_map -> 'a) -> Proofview.Goal.t -> 'a
-  val pf_global : identifier -> Proofview.Goal.t -> constr
-  val of_old : (Proof_type.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a
+  val pf_apply : (env -> evar_map -> 'a) -> 'b Proofview.Goal.t -> 'a
+  val pf_global : identifier -> 'a Proofview.Goal.t -> constr
+  val of_old : (Proof_type.goal Evd.sigma -> 'a) -> [ `NF ] Proofview.Goal.t -> 'a
 
-  val pf_type_of : Proofview.Goal.t -> Term.constr -> Term.types
+  val pf_type_of : 'b Proofview.Goal.t -> Term.constr -> Term.types
 
-  val pf_get_new_id  : identifier -> Proofview.Goal.t -> identifier
-  val pf_ids_of_hyps : Proofview.Goal.t -> identifier list
-  val pf_hyps_types : Proofview.Goal.t -> (identifier * types) list
+  val pf_get_new_id  : identifier -> [ `NF ] Proofview.Goal.t -> identifier
+  val pf_ids_of_hyps : 'b Proofview.Goal.t -> identifier list
+  val pf_hyps_types : 'b Proofview.Goal.t -> (identifier * types) list
 
-  val pf_get_hyp : identifier -> Proofview.Goal.t -> named_declaration
-  val pf_get_hyp_typ        : identifier -> Proofview.Goal.t -> types
-  val pf_last_hyp           : Proofview.Goal.t -> named_declaration
+  val pf_get_hyp : identifier -> [ `NF ] Proofview.Goal.t -> named_declaration
+  val pf_get_hyp_typ        : identifier -> [ `NF ] Proofview.Goal.t -> types
+  val pf_last_hyp           : [ `NF ] Proofview.Goal.t -> named_declaration
 end