Quelques fonctions sur les locations des rawconstr

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

2 files changed, 80 insertions, 3 deletions

diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
new file mode 100644
index 000000000..c3f7d8822
--- /dev/null
+++ b/pretyping/rawterm.ml
@@ -0,0 +1,73 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+open Sign
+open Type_errors
+(*i*)
+
+(* Untyped intermediate terms, after ASTs and before constr. *)
+
+type loc = int * int
+
+(* locs here refers to the ident's location, not whole pat *)
+(* the last argument of PatCstr is a possible alias ident for the pattern *)
+type pattern =
+  | PatVar of loc * name
+  | PatCstr of loc * (constructor_path * identifier list) * pattern list * name
+
+type binder_kind = BProd | BLambda
+type fix_kind = RFix of int array * int | RCofix of int
+type rawsort = RProp of Term.contents | RType
+
+type reference =
+  | RConst of section_path * identifier list
+  | RInd of inductive_path * identifier list
+  | RConstruct of constructor_path * identifier list
+  | RAbst of section_path
+  | RVar of identifier
+  | REVar of int * identifier list
+  | RMeta of int
+
+type cases_style = PrintLet | PrintIf | PrintCases
+
+type rawconstr = 
+  | RRef of loc * reference
+  | RApp of loc * rawconstr * rawconstr list
+  | RBinder of loc * binder_kind * name * rawconstr * rawconstr
+  | RCases of loc * cases_style * rawconstr option * rawconstr list * 
+      (identifier list * pattern list * rawconstr) list
+  | ROldCase of loc * bool * rawconstr option * rawconstr * 
+      rawconstr array
+  | RRec of loc * fix_kind * identifier array * 
+      rawconstr array * rawconstr array
+  | RSort of loc * rawsort
+  | RHole of loc option
+  | RCast of loc * rawconstr * rawconstr
+
+
+(*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 
+
+  [On pourrait plutot mettre les arités aves le type qu'elles auront
+   dans le contexte servant à typer les body ???]
+
+   - boolean in POldCase means it is recursive
+   - option in PHole tell if the "?" was apparent or has been implicitely added
+i*)
+
+let dummy_loc = (0,0)
+
+let loc_of_rawconstr = function
+  | RRef (loc,_) -> loc
+  | RApp (loc,_,_) -> loc
+  | RBinder (loc,_,_,_,_) -> loc
+  | RCases (loc,_,_,_,_) -> loc
+  | ROldCase (loc,_,_,_,_) -> loc
+  | RRec (loc,_,_,_,_) -> loc
+  | RSort (loc,_) -> loc
+  | RHole (Some loc) -> loc
+  | RHole (None) -> dummy_loc
+  | RCast (loc,_,_) -> loc
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 440d9ed44..8c93eecd9 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -11,10 +11,11 @@ open Type_errors
 
 type loc = int * int
 
-type pattern =  (* locs here refers to the ident's location, not whole pat *)
+(* locs here refers to the ident's location, not whole pat *)
+(* the last argument of PatCstr is a possible alias ident for the pattern *)
+type pattern =
   | PatVar of loc * name
-  | PatCstr of loc * (constructor_path * identifier list) * pattern list
-  | PatAs of loc * identifier * pattern
+  | PatCstr of loc * (constructor_path * identifier list) * pattern list * name
 
 type binder_kind = BProd | BLambda
 type fix_kind = RFix of int array * int | RCofix of int
@@ -56,3 +57,6 @@ type rawconstr =
    - boolean in POldCase means it is recursive
    - option in PHole tell if the "?" was apparent or has been implicitely added
 i*)
+
+val dummy_loc : loc
+val loc_of_rawconstr : rawconstr -> loc