Restructuration des points d'entrée de Pretyping et Constrintern

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7682 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 58 insertions, 59 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index c0e20c399e..0baaa98198 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -956,13 +956,16 @@ and pretype_type valcon env isevars lvar = function
                 (loc_of_rawconstr c) env (evars_of !isevars) tj.utj_val v
 
 
-let unsafe_infer tycon isevars env lvar constr =
-  let j = pretype tycon env isevars lvar constr in
-  j_nf_evar (evars_of !isevars) j
+type typing_constraint = OfType of types option | IsType
 
-let unsafe_infer_type valcon isevars env lvar constr =
-  let tj = pretype_type valcon env isevars lvar constr in
-  tj_nf_evar (evars_of !isevars) tj
+let pretype_gen isevars env lvar kind c =
+  let c' = match kind with
+  | OfType exptyp ->
+    let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
+    (pretype tycon env isevars lvar c).uj_val
+  | IsType ->
+    (pretype_type empty_valcon env isevars lvar c).utj_val in
+  nf_evar (evars_of !isevars) c'
 
 (* [check_evars] fails if some unresolved evar remains *)
 (* it assumes that the defined existentials have already been substituted
@@ -998,52 +1001,43 @@ let check_evars env initial_sigma isevars c =
        retourne aussi le nouveau sigma...
 *)
 
+let understand_judgment sigma env c =
+  let isevars = ref (create_evar_defs sigma) in
+  let j = pretype empty_tycon env isevars ([],[]) c in
+  let j = j_nf_evar (evars_of !isevars) j in
+  check_evars env sigma isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
+  j
+
 (* Raw calls to the unsafe inference machine: boolean says if we must
    fail on unresolved evars; the unsafe_judgment list allows us to
    extend env with some bindings *)
 
-let ise_infer_gen fail_evar sigma env lvar exptyp c =
-  let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
-  let isevars = ref (create_evar_defs sigma) in
-  let j = unsafe_infer tycon isevars env lvar c in
-  if fail_evar then 
-    check_evars env sigma isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
-  (!isevars, j)
-
-let ise_infer_type_gen fail_evar sigma env lvar c =
+let ise_pretype_gen fail_evar sigma env lvar kind c =
   let isevars = ref (create_evar_defs sigma) in
-  let tj = unsafe_infer_type empty_valcon isevars env lvar c in
-  if fail_evar then check_evars env sigma isevars tj.utj_val;
-  (!isevars, tj)
+  let c = pretype_gen isevars env lvar kind c in
+  if fail_evar then check_evars env sigma isevars c;
+  (!isevars, c)
 
 (** Entry points of the high-level type synthesis algorithm *)
 
 type var_map = (identifier * unsafe_judgment) list
 type unbound_ltac_var_map = (identifier * identifier option) list
 
-let understand_judgment sigma env c =
-  snd (ise_infer_gen true sigma env ([],[]) None c)
-
-let understand_type_judgment sigma env c =
-  snd (ise_infer_type_gen true sigma env ([],[]) c)
+let understand_gen kind sigma env c =
+  snd (ise_pretype_gen true sigma env ([],[]) kind c)
 
-let understand sigma env c =
-  (understand_judgment sigma env c).uj_val
+let understand sigma env ?expected_type:exptyp c =
+  snd (ise_pretype_gen true sigma env ([],[]) (OfType exptyp) c)
 
 let understand_type sigma env c =
-  (understand_type_judgment sigma env c).utj_val
-
-let understand_gen_ltac sigma env lvar ~expected_type:exptyp c =
-  let evars,j = ise_infer_gen false sigma env lvar exptyp c in
-  (evars, j.uj_val)
+  snd (ise_pretype_gen true sigma env ([],[]) IsType c)
 
-let understand_gen sigma env lvar ~expected_type:exptyp c =
-  let _, c = ise_infer_gen true sigma env (lvar,[]) exptyp c in
-  c.uj_val
+let understand_ltac sigma env lvar kind c =
+  ise_pretype_gen false sigma env lvar kind c
 
-let understand_gen_tcc sigma env lvar ~expected_type:exptyp c =
-  let evars,j = ise_infer_gen false sigma env (lvar,[]) exptyp c in
-  evars_of evars, j.uj_val
+let understand_tcc sigma env ?expected_type:exptyp c =
+  let evars,c = ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c in
+  evars_of evars,c
 
 (** Miscellaneous interpretation functions *)
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 80a9529c8a..d07b83ebac 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -18,49 +18,54 @@ open Rawterm
 open Evarutil
 (*i*)
 
+type typing_constraint = OfType of types option | IsType
+
+(* Generic call to the interpreter from rawconstr to open_constr, leaving
+   unresolved holes as evars and returning the typing contexts of
+   these evars. Work as [understand_gen] for the rest. *)
+
+val understand_tcc :
+  evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr
+
+(* More general entry point with evars from ltac *)
+
 type var_map = (identifier * unsafe_judgment) list
 type unbound_ltac_var_map = (identifier * identifier option) list
 
 (* Generic call to the interpreter from rawconstr to constr, failing
    unresolved holes in the rawterm cannot be instantiated.
 
-   In [understand_gen sigma env varmap typopt raw],
+   In [understand_ltac sigma env ltac_env constraint c],
 
    sigma : initial set of existential variables (typically dependent subgoals)
-   varmap : partial subtitution of variables (used for the tactic language)
-   metamap : partial subtitution of meta (used for the tactic language)
-   typopt : is not None, this is the expected type for raw (used to define evars)
+   ltac_env : partial substitution of variables (used for the tactic language)
+   constraint : tell if interpreted as a possibly constrained term or a type 
 *)
-val understand_gen :
-  evar_map -> env -> var_map
-    -> expected_type:(constr option) -> rawconstr -> constr
-
-(* Generic call to the interpreter from rawconstr to constr, leaving
-   unresolved holes as evars and returning the typing contexts of
-   these evars. Work as [understand_gen] for the rest. *)
-val understand_gen_tcc :
-  evar_map -> env -> var_map
-    -> expected_type:(constr option) -> rawconstr -> open_constr
 
-(* More general entry point with evars from ltac *)
-val understand_gen_ltac :
-  evar_map -> env -> var_map * unbound_ltac_var_map
-    -> expected_type:(constr option) -> rawconstr -> evar_defs * constr
+val understand_ltac :
+  evar_map -> env -> var_map * unbound_ltac_var_map ->
+    typing_constraint -> rawconstr -> evar_defs * constr
 
 (* Standard call to get a constr from a rawconstr, resolving implicit args *)
-val understand : evar_map -> env -> rawconstr -> constr
+
+val understand : evar_map -> env -> ?expected_type:Term.types ->
+  rawconstr -> constr
 
 (* Idem but the rawconstr is intended to be a type *)
+
 val understand_type : evar_map -> env -> rawconstr -> constr
 
+(* A generalization of the two previous case *)
+
+val understand_gen : typing_constraint -> evar_map -> env -> 
+  rawconstr -> constr
+
 (* Idem but returns the judgment of the understood term *)
-val understand_judgment : evar_map -> env -> rawconstr -> unsafe_judgment
 
-(* Idem but returns the judgment of the understood type *)
-val understand_type_judgment : evar_map -> env -> rawconstr 
-  -> unsafe_type_judgment
+val understand_judgment : evar_map -> env -> rawconstr -> unsafe_judgment
 
 (* To embed constr in rawconstr *)
+
 val constr_in : constr -> Dyn.t
 val constr_out : Dyn.t -> constr