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, 105 insertions, 139 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 06d11e6653..6eacde19ad 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -247,7 +247,7 @@ let set_var_scope loc id (_,scopt,scopes) varscopes =
    [vars2] is the set of global variables, env is the set of variables
    abstracted until this point *)
 
-let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,_,impls) loc id =
+let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) loc id =
   let (vars1,unbndltacvars) = ltacvars in
   (* Is [id] an inductive type potentially with implicit *)
   try
@@ -285,7 +285,7 @@ let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,_,impls) loc id =
     (* [id] a goal variable *)
     RVar (loc,id), [], [], []
 
-let find_appl_head_data (_,_,_,_,impls) = function
+let find_appl_head_data (_,_,_,(_,impls)) = function
   | RRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[]
   | x -> x,[],[],[]
 
@@ -334,7 +334,7 @@ let intern_reference env lvar = function
 	else raise e
 
 let interp_reference vars r =
-  let (r,_,_,_) = intern_reference (Idset.empty,None,[]) (vars,[],[],[],[]) r 
+  let r,_,_,_ = intern_reference (Idset.empty,None,[]) (vars,[],[],([],[])) r 
   in r
 
 let apply_scope_env (ids,_,scopes) = function
@@ -628,7 +628,7 @@ let locate_if_isevar loc na = function
       with Not_found -> RHole (loc, Evd.BinderType na))
   | x -> x
 
-let check_hidden_implicit_parameters id (_,_,_,indnames,_) =
+let check_hidden_implicit_parameters id (_,_,_,(indnames,_)) =
   if List.mem id indnames then
     errorlabstrm "" (str "A parameter or name of an inductive type " ++
     pr_id id ++ str " must not be used as a bound variable in the type \
@@ -919,7 +919,7 @@ let internalise sigma env allow_soapp lvar c =
     | CPatVar (loc, (false,n)) when Options.do_translate () ->
 	RVar (loc, n)
     | CPatVar (loc, (false,n)) ->
-        if List.mem n (fst (let (a,_,_,_,_) = lvar in a)) & !Options.v7 then
+        if List.mem n (fst (let (a,_,_,_) = lvar in a)) & !Options.v7 then
 	  RVar (loc, n)
 	else
           error_unbound_patvar loc n
@@ -1063,113 +1063,53 @@ let extract_ids env =
     (Termops.ids_of_rel_context (Environ.rel_context env))
     Idset.empty
 
-let interp_rawconstr_gen_with_implicits isarity sigma env (indpars,impls) allow_soapp ltacvar c =
+let intern_gen isarity sigma env
+               ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[]))
+               c =
   let tmp_scope = if isarity then Some Notation.type_scope else None in
   internalise sigma (extract_ids env, tmp_scope,[])
-    allow_soapp (ltacvar,Environ.named_context env, [], indpars, impls) c
+    allow_soapp (ltacvars,Environ.named_context env, [], impls) c
 
-let interp_rawconstr_gen isarity sigma env allow_soapp ltacvar c =
-  interp_rawconstr_gen_with_implicits isarity sigma env ([],[]) allow_soapp ltacvar c
+let intern_constr sigma env c = intern_gen true sigma env c 
 
-let interp_rawconstr sigma env c =
-  interp_rawconstr_gen false sigma env false ([],[]) c
-
-let interp_rawtype sigma env c =
-  interp_rawconstr_gen true sigma env false ([],[]) c
-
-let interp_rawtype_with_implicits sigma env impls c =
-  interp_rawconstr_gen_with_implicits true sigma env impls false ([],[]) c
-
-let interp_rawconstr_with_implicits sigma env vars impls c =
-  interp_rawconstr_gen_with_implicits false sigma env ([],impls) false
-    (vars,[]) c
-
-(*
-(* The same as interp_rawconstr but with a list of variables which must not be
-   globalized *)
-
-let interp_rawconstr_wo_glob sigma env lvar c =
-  interp_rawconstr_gen sigma env [] (Some []) lvar c
-*)
+let intern_ltac isarity ltacvars sigma env c =
+  intern_gen isarity sigma env ~ltacvars:ltacvars c
 
 (*********************************************************************)
 (* Functions to parse and interpret constructions *)
 
-let interp_constr sigma env c =
-  understand sigma env (interp_rawconstr sigma env c)
-
-let interp_openconstr sigma env c =
-  understand_gen_tcc sigma env [] None (interp_rawconstr sigma env c)
-
-(*
-let interp_casted_openconstr sigma env c typ =
-  understand_gen_tcc sigma env [] (Some typ) (interp_rawconstr sigma env c)
-*)
-
-let interp_type sigma env c =
-  understand_type sigma env (interp_rawtype sigma env c)
+let interp_gen kind sigma env 
+               ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[]))
+               c =
+  understand_gen kind sigma env 
+    (intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars sigma env c)
 
-let interp_binder sigma env na t =
-  let t = interp_rawtype sigma env t in
-  understand_type sigma env (locate_if_isevar (loc_of_rawconstr t) na t)
-
-let interp_type_with_implicits sigma env impls c =
-  understand_type sigma env (interp_rawtype_with_implicits sigma env impls c)
+let interp_constr sigma env c =
+  interp_gen (OfType None) sigma env c 
 
-let judgment_of_rawconstr sigma env c =
-  understand_judgment sigma env (interp_rawconstr sigma env c)
+let interp_type sigma env ?(impls=([],[])) c =
+  interp_gen IsType sigma env ~impls c
 
-let type_judgment_of_rawconstr sigma env c =
-  understand_type_judgment sigma env (interp_rawconstr sigma env c)
+let interp_casted_constr sigma env ?(impls=([],[])) c typ =
+  interp_gen (OfType (Some typ)) sigma env ~impls c 
 
-(* To retype a list of key*constr with undefined key *)
-let retype_list sigma env lst =
-  List.fold_right (fun (x,csr) a ->
-    try (x,Retyping.get_judgment_of env sigma csr)::a with
-    | Anomaly _ -> a) lst []
+let interp_open_constr sigma env c =
+  understand_tcc sigma env (intern_constr sigma env c)
 
-(*  List.map (fun (x,csr) -> (x,Retyping.get_judgment_of env sigma csr)) lst*)
+let interp_constr_judgment sigma env c =
+  understand_judgment sigma env (intern_constr sigma env c)
 
 type ltac_sign = identifier list * unbound_ltac_var_map
-type ltac_env = (identifier * Term.constr) list * unbound_ltac_var_map
-
-(* Interprets a constr according to two lists *)
-(* of instantiations (variables and metas)    *)
-(* Note: typ is retyped *)
-let interp_constr_gen sigma env (ltacvars,unbndltacvars) c exptyp =
-  let c = interp_rawconstr_gen false sigma env false
-    (List.map fst ltacvars,unbndltacvars) c in
-  let typs = retype_list sigma env ltacvars in
-  understand_gen_ltac sigma env (typs,[]) exptyp c
-
-(*Interprets a casted constr according to two lists of instantiations
-  (variables and metas)*)
-let interp_openconstr_gen sigma env (ltacvars,unbndltacvars) c exptyp =
-  let c = interp_rawconstr_gen false sigma env false
-    (List.map fst ltacvars,unbndltacvars) c in
-  let typs = retype_list sigma env ltacvars in
-  understand_gen_tcc sigma env typs exptyp c
-
-let interp_casted_constr sigma env c typ = 
-  understand_gen sigma env [] (Some typ) (interp_rawconstr sigma env c)
-
-let interp_casted_constr_with_implicits sigma env impls c typ =
-  understand_gen sigma env [] (Some typ) 
-    (interp_rawconstr_with_implicits sigma env [] impls c)
-
-let interp_constrpattern_gen sigma env ltacvar c =
-  let c = interp_rawconstr_gen false sigma env true (ltacvar,[]) c in
-  pattern_of_rawconstr c
 
 let interp_constrpattern sigma env c =
-  interp_constrpattern_gen sigma env [] c
+  pattern_of_rawconstr (intern_constr sigma env c)
 
 let interp_aconstr impls vars a =
   let env = Global.env () in
   (* [vl] is intended to remember the scope of the free variables of [a] *)
   let vl = List.map (fun id -> (id,ref None)) vars in
   let c = internalise Evd.empty (extract_ids env, None, [])
-    false (([],[]),Environ.named_context env,vl,[],impls) a in
+    false (([],[]),Environ.named_context env,vl,([],impls)) a in
   (* Translate and check that [c] has all its free variables bound in [vars] *)
   let a = aconstr_of_rawconstr vars c in
   (* Returns [a] and the ordered list of variables with their scopes *)
@@ -1178,6 +1118,33 @@ let interp_aconstr impls vars a =
     (fun (id,r) -> (id,match !r with None -> None,[] | Some (a,l) -> a,l)) vl,
   a
 
+(* Interpret binders and contexts  *)
+
+let interp_binder sigma env na t =
+  let t = intern_gen true sigma env t in
+  understand_type sigma env (locate_if_isevar (loc_of_rawconstr t) na t)
+
+open Environ
+open Term
+
+let interp_context sigma env params = 
+  List.fold_left
+    (fun (env,params) d -> match d with
+      | LocalRawAssum ([_,na],(CHole _ as t)) ->
+	  let t = interp_binder sigma env na t in
+	  let d = (na,None,t) in
+	  (push_rel d env, d::params)
+      | LocalRawAssum (nal,t) ->
+	  let t = interp_type sigma 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 sigma 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 757f02a466..08de85d87b 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -35,7 +35,11 @@ open Pretyping
 *)
 
 (* To interpret implicits and arg scopes of recursive variables in
-   inductive types and recursive definitions *)
+   inductive types and recursive definitions; mention of a list of
+   implicits arguments in the ``rel'' part of [env]; the second
+   argument associates a list of implicit positions and scopes to
+   identifiers declared in the [rel_context] of [env] *)
+
 type var_internalisation_data =
     identifier list * Impargs.implicits_list * scope_name option list
 
@@ -43,61 +47,55 @@ type implicits_env = (identifier * var_internalisation_data) list
 type full_implicits_env = identifier list * implicits_env
 
 type ltac_sign = identifier list * unbound_ltac_var_map
-type ltac_env = (identifier * constr) list * unbound_ltac_var_map
-
-(* Interprets global names, including syntactic defs and section variables *)
-val interp_rawconstr     : evar_map -> env -> constr_expr -> rawconstr
-val interp_rawconstr_gen : bool -> evar_map -> env -> 
-    bool -> ltac_sign -> constr_expr -> rawconstr
-
-(*s Composing the translation with typing *)
-val interp_constr        : evar_map -> env -> constr_expr -> constr
-val interp_casted_constr : evar_map -> env -> constr_expr -> types -> constr
-val interp_type          : evar_map -> env -> constr_expr -> types
-val interp_binder        : evar_map -> env -> name -> constr_expr -> types
-val interp_openconstr    : evar_map -> env -> constr_expr -> evar_map * constr
-
-(* [interp_type_with_implicits] extends [interp_type] by allowing
-   implicits arguments in the ``rel'' part of [env]; the extra
-   argument associates a list of implicit positions to identifiers
-   declared in the [rel_context] of [env] *)
-val interp_type_with_implicits : 
-  evar_map -> env -> full_implicits_env -> constr_expr -> types
-
-val interp_casted_constr_with_implicits :
-  evar_map -> env -> implicits_env -> constr_expr -> types -> constr
-
-val interp_rawconstr_with_implicits :
-  evar_map -> env -> identifier list -> implicits_env -> constr_expr -> 
-    rawconstr
-
-(*s Build a judgement from *)
-val judgment_of_rawconstr : evar_map -> env -> constr_expr -> unsafe_judgment
-val type_judgment_of_rawconstr :
-  evar_map -> env -> constr_expr -> unsafe_type_judgment
-
-(* Interprets a constr according to two lists of instantiations (variables and
-  metas), possibly casting it*)
-val interp_constr_gen     :
-  evar_map -> env -> ltac_env -> constr_expr -> constr option ->
-    evar_defs * constr
-
-(* Interprets a constr according to two lists of instantiations (variables and
-  metas), possibly casting it, and turning unresolved evar into metas*)
-val interp_openconstr_gen     :
-  evar_map -> env -> ltac_env ->
-    constr_expr -> constr option -> evar_map * constr
-
-(* Interprets constr patterns according to a list of instantiations
-  (variables)*)
-val interp_constrpattern_gen : evar_map -> env -> identifier list ->
-  constr_expr -> patvar list * constr_pattern
+
+(*s Internalisation performs interpretation of global names and notations *)
+
+val intern_constr : evar_map -> env -> constr_expr -> rawconstr
+
+val intern_gen : bool -> evar_map -> env ->
+  ?impls:full_implicits_env -> ?allow_soapp:bool -> ?ltacvars:ltac_sign ->
+  constr_expr -> rawconstr
+
+(*s Composing internalisation with pretyping *)
+
+(* Main interpretation function *)
+
+val interp_gen : typing_constraint -> evar_map -> env ->
+  ?impls:full_implicits_env -> ?allow_soapp:bool -> ?ltacvars:ltac_sign ->
+  constr_expr -> constr
+
+(* Particular instances *)
+
+val interp_constr : evar_map -> env -> 
+  constr_expr -> constr
+
+val interp_casted_constr : evar_map -> env -> ?impls:full_implicits_env -> 
+  constr_expr -> types -> constr
+
+val interp_type : evar_map -> env -> ?impls:full_implicits_env -> 
+  constr_expr -> types
+
+val interp_open_constr   : evar_map -> env -> constr_expr -> evar_map * constr
+
+(*s Build a judgment  *)
+
+val interp_constr_judgment : evar_map -> env -> constr_expr -> unsafe_judgment
+
+(* Interprets constr patterns *)
 
 val interp_constrpattern : 
   evar_map -> env -> constr_expr -> patvar list * constr_pattern
 
 val interp_reference : ltac_sign -> reference -> rawconstr
 
+(* Interpret binders *)
+
+val interp_binder  : evar_map -> env -> name -> constr_expr -> types
+
+(* Interpret contexts: returns extended env and context *)
+
+val interp_context : evar_map -> env -> local_binder list -> env * rel_context
+
 (* Locating references of constructions, possibly via a syntactic definition *)
 
 val locate_reference : qualid -> global_reference
@@ -107,6 +105,7 @@ val global_reference : identifier -> constr
 val global_reference_in_absolute_module : dir_path -> identifier -> constr
 
 (* Interprets into a abbreviatable constr *)
+
 val interp_aconstr : implicits_env -> identifier list -> constr_expr ->
   interpretation