Export de fonctions d'interprétation acceptant des evars non résolues

en entrée et en sortie


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

2 files changed, 49 insertions, 1 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index aa9a379db..76d0a1bf6 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1100,6 +1100,21 @@ let interp_open_constr sigma env c =
 let interp_constr_judgment sigma env c =
   Default.understand_judgment sigma env (intern_constr sigma env c)
 
+
+let interp_constr_evars_gen isevars env ?(impls=([],[])) kind c =
+  Default.understand_tcc_evars isevars env kind
+    (intern_gen (kind=IsType) ~impls (Evd.evars_of !isevars) env c)
+
+let interp_casted_constr_evars isevars env ?(impls=([],[])) c typ =
+  interp_constr_evars_gen isevars env ~impls (OfType (Some typ)) c
+
+let interp_type_evars isevars env ?(impls=([],[])) c =
+  interp_constr_evars_gen isevars env IsType ~impls c
+
+let interp_constr_judgment_evars isevars env c =
+  Default.understand_judgment_tcc isevars env
+    (intern_constr (Evd.evars_of !isevars) env c)
+
 type ltac_sign = identifier list * unbound_ltac_var_map
 
 let interp_constrpattern sigma env c =
@@ -1123,7 +1138,13 @@ let interp_aconstr impls vars a =
 
 let interp_binder sigma env na t =
   let t = intern_gen true sigma env t in
-  Default.understand_type sigma env (locate_if_isevar (loc_of_rawconstr t) na t)
+  let t' = locate_if_isevar (loc_of_rawconstr t) na t in
+  Default.understand_type sigma env t'
+
+let interp_binder_evars isevars env na t =
+  let t = intern_gen true (Evd.evars_of !isevars) env t in
+  let t' = locate_if_isevar (loc_of_rawconstr t) na t in
+  Default.understand_tcc_evars isevars env IsType t'
 
 open Environ
 open Term
@@ -1146,6 +1167,24 @@ let interp_context sigma env params =
 	  (push_rel d env,d::params))
     (env,[]) params
 
+let interp_context_evars isevars env params =
+  List.fold_left
+    (fun (env,params) d -> match d with
+      | LocalRawAssum ([_,na],(CHole _ as t)) ->
+	  let t = interp_binder_evars isevars env na t in
+	  let d = (na,None,t) in
+	  (push_rel d env, d::params)
+      | LocalRawAssum (nal,t) ->
+	  let t = interp_type_evars isevars env t in
+	  let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in
+	  let ctx = List.rev ctx in
+	  (push_rel_context ctx env, ctx@params)
+      | LocalRawDef ((_,na),c) ->
+	  let c = interp_constr_judgment_evars isevars env c in
+	  let d = (na, Some c.uj_val, c.uj_type) in
+	  (push_rel d env,d::params))
+    (env,[]) params
+
 (**********************************************************************)
 (* Locating reference, possibly via an abbreviation *)
 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 70af93885..4603565e3 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -76,6 +76,12 @@ val interp_type : evar_map -> env -> ?impls:full_implicits_env ->
 
 val interp_open_constr   : evar_map -> env -> constr_expr -> evar_map * constr
 
+val interp_casted_constr_evars : evar_defs ref -> env -> 
+  ?impls:full_implicits_env -> constr_expr -> types -> constr
+
+val interp_type_evars : evar_defs ref -> env -> ?impls:full_implicits_env ->
+  constr_expr -> types
+
 (*s Build a judgment  *)
 
 val interp_constr_judgment : evar_map -> env -> constr_expr -> unsafe_judgment
@@ -95,6 +101,9 @@ val interp_binder  : evar_map -> env -> name -> constr_expr -> types
 
 val interp_context : evar_map -> env -> local_binder list -> env * rel_context
 
+val interp_context_evars : 
+  evar_defs ref -> env -> local_binder list -> env * rel_context
+
 (* Locating references of constructions, possibly via a syntactic definition *)
 
 val locate_reference : qualid -> global_reference