MAJ pour fusion avec pretyping

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

2 files changed, 92 insertions, 3 deletions

diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index cab7a15d2f..7b95e2dcc6 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -1,2 +1,80 @@
 
 (* $Id$ *)
+
+(*i*)
+open Names
+open Sign
+open Term
+open Environ
+open Evd
+open Rawterm
+(*i*)
+
+val type_of_com : context -> Coqast.t -> typed_type
+
+val constr_of_com_casted : 'c evar_map -> context -> Coqast.t -> constr ->
+  constr
+
+val constr_of_com1 : bool -> 'c evar_map -> context -> Coqast.t -> constr
+val constr_of_com : 'c evar_map -> context -> Coqast.t -> constr
+val constr_of_com_sort : 'c evar_map -> context -> Coqast.t -> constr
+
+val fconstr_of_com1 : bool -> 'c evar_map -> context -> Coqast.t -> constr
+val fconstr_of_com : 'c evar_map -> context -> Coqast.t -> constr
+val fconstr_of_com_sort : 'c evar_map -> context -> Coqast.t -> constr
+
+
+(* Typing with Trad, and re-checking with Mach *)
+(*i
+val fconstruct :'c evar_map -> context -> Coqast.t -> judgement
+val fconstruct_type :
+  'c evar_map -> context -> Coqast.t -> type_judgement
+
+val infconstruct_type :
+  'c evar_map -> (context * context) ->
+    Coqast.t -> type_judgement * information
+val infconstruct :
+  'c evar_map -> (context * context) ->
+    Coqast.t -> judgement * information
+
+(* Typing, re-checking with universes constraints *)
+val fconstruct_with_univ :
+  'c evar_map -> context -> Coqast.t -> judgement
+val fconstruct_with_univ_sp : 'c evar_map -> context
+  -> section_path -> constr -> Impuniv.universes * judgement
+val fconstruct_type_with_univ_sp : 'c evar_map -> context
+  -> section_path -> constr -> Impuniv.universes * type_judgement
+val infconstruct_with_univ_sp :
+  'c evar_map -> (context * context)
+  -> section_path -> constr -> Impuniv.universes * (judgement * information)
+val infconstruct_type_with_univ_sp :
+  'c evar_map -> (context * context)
+  -> section_path -> constr 
+  -> Impuniv.universes * (type_judgement * information)
+i*)
+
+(* Low level typing functions, for terms with de Bruijn indices and Metas *)
+
+(* Raw calls to the inference machine of Trad: boolean says if we must fail
+ * on unresolved evars, or replace them by Metas *)
+val ise_resolve : bool -> 'c evar_map -> (int * constr) list ->
+  context -> rawconstr -> unsafe_judgment
+val ise_resolve_type : bool -> 'c evar_map -> (int * constr) list ->
+  context -> rawconstr -> typed_type
+
+(* Call ise_resolve with empty metamap and fail_evar=true. The boolean says
+ * if we must coerce to a type *)
+val ise_resolve1 : bool -> 'c evar_map -> context -> rawconstr -> constr
+
+(* progmach.ml tries to type ill-typed terms: does not perform the conversion
+ * test in application.
+ *)
+val ise_resolve_nocheck : 'c evar_map -> (int * constr) list ->
+  context -> rawconstr -> unsafe_judgment
+
+
+(* Internal of Trad...
+ * Unused outside Trad, but useful for debugging
+ *)
+val pretype : bool * (constr option * constr option) -> 'c evar_map ref
+  -> context -> rawconstr -> unsafe_judgment
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index d30de0647b..0ee1e04349 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -1,5 +1,15 @@
+
+(* $Id$ *)
+
+(*i*)
 open Names
-open CoqAst
+open Sign
+open Type_errors
+(*i*)
+
+(* Untyped intermediate terms, after ASTs and before constr. *)
+
+type loc = int * int
 
 type indtype_id = section_path * int
 type constructor_id = indtype_id * int
@@ -39,7 +49,8 @@ type rawconstr =
   | RHole of loc option
   | RCast of loc * rawconstr * rawconstr
 
-(* - if PRec (_, names, arities, bodies) is in env then arities are
+
+(*i - if PRec (_, names, arities, bodies) is in env then arities are
    typed in env too and bodies are typed in env enriched by the
    arities incrementally lifted 
 
@@ -48,4 +59,4 @@ type rawconstr =
 
    - boolean in POldCase means it is recursive
    - option in PHole tell if the "?" was apparent or has been implicitely added
-*)
+i*)