Safer typing primitives.

Some functions from pretyping/typing.ml and their derivatives were potential
source of evarmap leaks, as they dropped their resulting evarmap. This commit
clarifies the situation by renaming them according to a unsafe_* scheme. Their
sound variant is likewise renamed to their old name. The following renamings
were made.

- Typing.type_of -> unsafe_type_of
- Typing.e_type_of -> type_of
- A new e_type_of function that matches the e_ prefix policy
- Tacmach.pf_type_of -> pf_unsafe_type_of
- A new safe pf_type_of function.

All uses of unsafe_* functions should be eventually eliminated.

7 files changed, 28 insertions, 16 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index fcbe90b6a..ef196e0a7 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1668,7 +1668,7 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t =
 	(lift (n'-n) impossible_case_type, mkSort u)
     | Some t ->
         let t = abstract_tycon loc tycon_env evdref subst tycon extenv t in
-        let evd,tt = Typing.e_type_of extenv !evdref t in
+        let evd,tt = Typing.type_of extenv !evdref t in
         evdref := evd;
         (t,tt) in
   let b = e_cumul env evdref tt (mkSort s) (* side effect *) in
@@ -2014,7 +2014,7 @@ let constr_of_pat env evdref arsign pat avoid =
 	let IndType (indf, _) = 
 	  try find_rectype env ( !evdref) (lift (-(List.length realargs)) ty)
 	  with Not_found -> error_case_not_inductive env 
-	    {uj_val = ty; uj_type = Typing.type_of env !evdref ty}
+	    {uj_val = ty; uj_type = Typing.unsafe_type_of env !evdref ty}
 	in
 	let (ind,u), params = dest_ind_family indf in
 	if not (eq_ind ind cind) then error_bad_constructor_loc l env cstr ind;
@@ -2214,7 +2214,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
 	 let j = typing_fun (mk_tycon tycon) rhs_env eqn.rhs.it in
 	 let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels'
 	 and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in
-	 let _btype = evd_comb1 (Typing.e_type_of env) evdref bbody in
+	 let _btype = evd_comb1 (Typing.type_of env) evdref bbody in
 	 let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in
 	 let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in
 	 let branch =
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 8ebb8cd27..f5135f5c6 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -295,8 +295,8 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
 		   let evm = !evdref in
 		     (try subco ()
 		      with NoSubtacCoercion ->
-			let typ = Typing.type_of env evm c in
-			let typ' = Typing.type_of env evm c' in
+			let typ = Typing.unsafe_type_of env evm c in
+			let typ' = Typing.unsafe_type_of env evm c' in
 			  (* 			     if not (is_arity env evm typ) then *)
 			  coerce_application typ typ' c c' l l')
 		       (* 			     else subco () *)
@@ -305,8 +305,8 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
 	   | x, y when Constr.equal c c' ->
 	       if Int.equal (Array.length l) (Array.length l') then
 		 let evm =  !evdref in
-		 let lam_type = Typing.type_of env evm c in
-		 let lam_type' = Typing.type_of env evm c' in
+		 let lam_type = Typing.unsafe_type_of env evm c in
+		 let lam_type' = Typing.unsafe_type_of env evm c' in
 		   (* 			 if not (is_arity env evm lam_type) then ( *)
 		   coerce_application lam_type lam_type' c c' l l'
 		     (* 			 ) else subco () *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 0cadffa4f..03fe2122c 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -374,7 +374,7 @@ let pretype_ref loc evdref env ref us =
   | ref ->
     let evd, c = pretype_global loc univ_flexible env !evdref ref us in
     let () = evdref := evd in
-    let ty = Typing.type_of env evd c in
+    let ty = Typing.unsafe_type_of env evd c in
       make_judge c ty
 
 let judge_of_Type evd s =
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 372b26aa2..8a5db9059 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1134,7 +1134,7 @@ let abstract_scheme env (locc,a) (c, sigma) =
 let pattern_occs loccs_trm env sigma c =
   let abstr_trm, sigma = List.fold_right (abstract_scheme env) loccs_trm (c,sigma) in
   try
-    let _ = Typing.type_of env sigma abstr_trm in
+    let _ = Typing.unsafe_type_of env sigma abstr_trm in
       sigma, applist(abstr_trm, List.map snd loccs_trm)
   with Type_errors.TypeError (env',t) ->
     raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t))))
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index c6209cc33..fb5927dbf 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -270,7 +270,7 @@ let check env evdref c t =
 
 (* Type of a constr *)
 
-let type_of env evd c =
+let unsafe_type_of env evd c =
   let j = execute env (ref evd) c in
     j.uj_type
 
@@ -283,7 +283,7 @@ let sort_of env evdref c =
 
 (* Try to solve the existential variables by typing *)
 
-let e_type_of ?(refresh=false) env evd c =
+let type_of ?(refresh=false) env evd c =
   let evdref = ref evd in
   let j = execute env evdref c in
   (* side-effect on evdref *)
@@ -291,6 +291,15 @@ let e_type_of ?(refresh=false) env evd c =
       Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type
     else !evdref, j.uj_type
 
+let e_type_of ?(refresh=false) env evdref c =
+  let j = execute env evdref c in
+  (* side-effect on evdref *)
+    if refresh then
+      let evd, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type in
+      let () = evdref := evd in
+      c
+    else j.uj_type
+
 let solve_evars env evdref c =
   let c = (execute env evdref c).uj_val in
   (* side-effect on evdref *)
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 1f822f1a5..bfae46ff8 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -13,12 +13,15 @@ open Evd
 (** This module provides the typing machine with existential variables
     and universes. *)
 
-(** Typecheck a term and return its type *)
-val type_of : env -> evar_map -> constr -> types
+(** Typecheck a term and return its type. May trigger an evarmap leak. *)
+val unsafe_type_of : env -> evar_map -> constr -> types
 
 (** Typecheck a term and return its type + updated evars, optionally refreshing
     universes *)
-val e_type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types
+val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types
+
+(** Variant of [type_of] using references instead of state-passing. *)
+val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types
 
 (** Typecheck a type and return its sort *)
 val sort_of : env -> evar_map ref -> types -> sorts
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index c2281e13a..b5fe5d0b6 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -93,7 +93,7 @@ let abstract_list_all env evd typ c l =
   let l_with_all_occs = List.map (function a -> (LikeFirst,a)) l in
   let p,evd = abstract_scheme env evd c l_with_all_occs ctxt in
   let evd,typp =
-    try Typing.e_type_of env evd p
+    try Typing.type_of env evd p
     with
     | UserError _ ->
         error_cannot_find_well_typed_abstraction env evd p l None
@@ -1150,7 +1150,7 @@ let applyHead env evd n c  =
 	  apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd'
       | _ -> error "Apply_Head_Then"
   in
-    apprec n c (Typing.type_of env evd c) evd
+    apprec n c (Typing.unsafe_type_of env evd c) evd
     
 let is_mimick_head ts f =
   match kind_of_term f with