Introduction d'un type constr_pattern pour les différents filtrages

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

6 files changed, 114 insertions, 66 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index cf68a472b4..fd32cda392 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -90,7 +90,22 @@ let ident_of_nvar loc s =
     user_err_loc (loc,"ident_of_nvar", [< 'sTR "Unexpected wildcard" >])
   else (id_of_string s)
 
-let ids_of_ctxt = array_map_to_list (function VAR id -> id | _ -> assert false)
+let rctxt_of_ctxt =
+  Array.map
+    (function
+       | VAR id -> RRef (dummy_loc,RVar id)
+       | _ ->
+     error "Astterm: arbitrary substitution of references not yet implemented")
+
+let ids_of_ctxt ctxt =
+  Array.to_list
+    (Array.map
+       (function
+	  | VAR id -> id
+	  | _ ->
+      error
+	"Astterm: arbitrary substitution of references not yet implemented")
+    ctxt)
 
 let maybe_constructor env s =
   try 
@@ -100,11 +115,14 @@ let maybe_constructor env s =
   with Not_found -> 
     None
 
-let dbize_ctxt = 
-  List.map 
-    (function
-       | Nvar (loc,s) -> ident_of_nvar loc s
-       | _ -> anomaly "Bad ast for local ctxt of a global reference")
+let dbize_ctxt ctxt =
+  let l =
+    List.map
+      (function
+	 | Nvar (loc,s) -> RRef (dummy_loc,RVar (ident_of_nvar loc s))
+	 | _ -> anomaly "Bad ast for local ctxt of a global reference") ctxt
+  in
+  Array.of_list l
 
 let dbize_global loc = function
   | ("CONST", sp::ctxt) -> 
@@ -121,10 +139,10 @@ let dbize_global loc = function
 		      [< 'sTR "Bad ast for this global a reference">])
 
 let ref_from_constr = function
-  | DOPN (Const sp,ctxt) -> RConst (sp,ids_of_ctxt ctxt)
-  | DOPN (Evar ev,ctxt) -> REVar (ev,ids_of_ctxt ctxt) 
-  | DOPN (MutConstruct (spi,j),ctxt) -> RConstruct ((spi,j),ids_of_ctxt ctxt)
-  | DOPN (MutInd (sp,i),ctxt) -> RInd ((sp,i),ids_of_ctxt ctxt)
+  | DOPN (Const sp,ctxt) -> RConst (sp,rctxt_of_ctxt ctxt)
+  | DOPN (Evar ev,ctxt) -> REVar (ev,rctxt_of_ctxt ctxt) 
+  | DOPN (MutConstruct (spi,j),ctxt) -> RConstruct ((spi,j),rctxt_of_ctxt ctxt)
+  | DOPN (MutInd (sp,i),ctxt) -> RInd ((sp,i),rctxt_of_ctxt ctxt)
   | VAR id -> RVar id  (* utilisé dans trad pour coe_value (tmp) *)
   | _ -> anomaly "Not a reference"
 
@@ -373,18 +391,10 @@ let dbize k sigma =
   in 
   dbrec
 
-let dbize_cci sigma env com = dbize CCI sigma env com
-let dbize_fw  sigma env com = dbize FW sigma env com
-
 (* constr_of_com takes an environment of typing assumptions,
  * and translates a command to a constr. *)
 
-let interp_rawconstr sigma env com = dbize_cci sigma (unitize_env (context env)) com
-
-let raw_fconstr_of_com sigma env com = dbize_fw sigma (unitize_env (context env)) com
-let raw_constr_of_compattern sigma env com = 
-  dbize_cci sigma (unitize_env env) com
-
+let interp_rawconstr sigma env com = dbize CCI sigma (unitize_env (context env)) com
 
 (* Globalization of AST quotations (mainly used in command quotations
    to get statically bound idents in grammar or pretty-printing rules) *)
@@ -496,6 +506,12 @@ let typed_type_of_com sigma env com =
 let interp_casted_constr sigma env com typ = 
   ise_resolve_casted sigma env typ (interp_rawconstr sigma env com)
 
+(*
+let dbize_fw  sigma env com = dbize FW sigma env com
+
+let raw_fconstr_of_com sigma env com = dbize_fw sigma (unitize_env (context env)) com
+let raw_constr_of_compattern sigma env com = 
+  dbize_cci sigma (unitize_env env) com
 
 let fconstr_of_com1 is_ass sigma env com = 
   let c = raw_fconstr_of_com sigma env com in
@@ -507,7 +523,7 @@ let fconstr_of_com1 is_ass sigma env com =
 let fconstr_of_com sigma hyps com =
   fconstr_of_com1 false sigma hyps com 
 
-
+*)
 (* Typing with Trad, and re-checking with Mach *)
 (* Should be done in two passes by library commands ...
 let fconstruct_type sigma sign com =
@@ -544,48 +560,52 @@ let fconstruct_with_univ sigma sign com =
 let ctxt_of_ids ids =
   Array.of_list (List.map (function id -> VAR id) ids)
 
-let constr_of_ref vars = function
-  | RConst (sp,ids) -> DOPN (Const sp, ctxt_of_ids ids)
-  | RInd (ip,ids) -> DOPN (MutInd ip, ctxt_of_ids ids)
-  | RConstruct (cp,ids) -> DOPN (MutConstruct cp, ctxt_of_ids ids)
-  | RAbst sp -> DOPN (Abst sp, [||])
-  | RVar id -> 
-      (try Rel (list_index (Name id) vars) with Not_found -> VAR id)
-  | REVar (n,ids) -> DOPN (Evar n, ctxt_of_ids ids)
-  | RMeta n -> DOP0 (Meta n)
-
-let constr_of_rawconstr c = 
-  let rec glob vars = function
-    | RRef (_,r) -> 
-	constr_of_ref vars r
-    | RApp (_,c,cl) -> 
-	let l = List.map (glob vars) (c::cl) in
-	DOPN (AppL, Array.of_list l)
-    | RBinder (_,BProd,na,c1,c2) ->
-	DOP2 (Prod, glob vars c1, DLAM (na, glob (na::vars) c2))
-    | RBinder (_,BLambda,na,c1,c2) ->
-	DOP2 (Lambda, glob vars c1, DLAM (na, glob (na::vars) c2))
-    | RSort (_,RProp c) ->
-	DOP0 (Sort (Prop c))
-    | RSort (_,RType) ->
-	DOP0 (Sort (Type (Univ.dummy_univ)))
-    | RHole _ -> 
-	DOP0 (Meta (new_meta()))
-    | RCast (_,c1,c2) ->
-	DOP2 (Cast, glob vars c1, glob vars c2)
-    | _ ->
-	error "constr_of_rawconstr: not implemented"
-  in
-  glob [] c
-
-let constr_of_com_pattern sigma env com = 
+let rec pat_of_ref metas vars = function
+  | RConst (sp,ctxt) -> RConst (sp, Array.map (pat_of_raw metas vars) ctxt)
+  | RInd (ip,ctxt) -> RInd (ip, Array.map (pat_of_raw metas vars) ctxt)
+  | RConstruct(cp,ctxt) ->RConstruct(cp,Array.map (pat_of_raw metas vars) ctxt)
+  | REVar (n,ctxt) -> REVar (n,Array.map (pat_of_raw metas vars) ctxt)
+  | RMeta n -> RMeta n
+  | RAbst _ -> error "pattern_of_rawconstr: not implemented"
+  | RVar _ -> assert false (* Capturé dans pattern_of_raw *)
+
+and pat_of_raw metas vars = function
+  | RRef (_,RVar id) -> 
+      (try PRel (list_index (Name id) vars)
+       with Not_found -> PRef (RVar id))
+  | RRef (_,r) ->
+      PRef (pat_of_ref metas vars r)
+  | RApp (_,c,cl) -> 
+      PApp (pat_of_raw metas vars c,
+	    Array.of_list (List.map (pat_of_raw metas vars) cl))
+  | RBinder (_,bk,na,c1,c2) ->
+      PBinder (bk, na, pat_of_raw metas vars c1,
+	       pat_of_raw metas (na::vars) c2)
+  | RSort (_,s) ->
+      PSort s
+  | RHole _ -> error "Place-holders must be numbered in patterns"
+(*
+      let n = new_meta () in
+      metas := n::!metas;
+      PMeta n *)
+  | RCast (_,c,t) ->
+      warning "Cast not taken into account in constr pattern";
+      pat_of_raw metas vars c
+  | _ ->
+      error "pattern_of_rawconstr: not implemented"
+
+let pattern_of_rawconstr c =
+  let metas = ref [] in
+  let p = pat_of_raw metas [] c in
+  (!metas,p)
+
+let interp_constrpattern sigma env com = 
   let c = interp_rawconstr sigma env com in
   try 
-    constr_of_rawconstr c
+    pattern_of_rawconstr c
   with e -> 
     Stdpp.raise_with_loc (Ast.loc com) e
 
-
 (* Translation of reduction expression: we need trad because of Fold
  * Moreover, reduction expressions are used both in tactics and in
  * vernac. *)
diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index b33c4b825f..70e7ab7a30 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -19,7 +19,9 @@ val interp_type          : 'a evar_map -> env -> Coqast.t -> constr
 val typed_type_of_com    : 'a evar_map -> env -> Coqast.t -> typed_type
 val judgment_of_com      : 'a evar_map -> env -> Coqast.t -> unsafe_judgment
 
-val constr_of_com_pattern : 'a evar_map -> env -> Coqast.t -> constr
+val interp_constrpattern : 
+  'a evar_map -> env -> Coqast.t -> int list * constr_pattern
+
 val redexp_of_ast : 
   'a evar_map -> env -> string * Coqast.t list -> Tacred.red_expr
 
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 99db762e02..36f8d11a36 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -97,6 +97,13 @@ let pr_existential ev = gencompr CCI (ast_of_existential ev)
 let pr_inductive ind = gencompr CCI (ast_of_inductive ind)
 let pr_constructor cstr = gencompr CCI (ast_of_constructor cstr)
 
+open Rawterm
+let pr_ref_label = function (* On triche sur le contexte *)
+  | ConstNode sp -> pr_constant (sp,[||])
+  | IndNode sp -> pr_inductive (sp,[||])
+  | CstrNode sp -> pr_constructor (sp,[||])
+  | VarNode id -> print_id id
+
 (* For compatibility *)
 let term0 = prterm_env
 let fterm0 = fprterm_env
diff --git a/parsing/printer.mli b/parsing/printer.mli
index b9c7f7182f..40a1bdad3b 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -25,12 +25,13 @@ val fprtype_env     : 'a assumptions -> typed_type -> std_ppcmds
 val fprtype         : typed_type -> std_ppcmds
 
 val prrawterm       : Rawterm.rawconstr -> std_ppcmds
-val prpattern       : Rawterm.pattern -> std_ppcmds
+val prpattern       : Rawterm.cases_pattern -> std_ppcmds
 
 val pr_constant     : constant -> std_ppcmds
 val pr_existential  : existential -> std_ppcmds
 val pr_constructor  : constructor -> std_ppcmds
 val pr_inductive    : inductive -> std_ppcmds
+val pr_ref_label    : Rawterm.constr_label -> std_ppcmds
 
 val pr_ne_env       : std_ppcmds -> path_kind -> context -> std_ppcmds
 
diff --git a/parsing/termast.ml b/parsing/termast.ml
index bd7a22cbd4..bcdc21f054 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -50,7 +50,25 @@ let with_coercions f = with_option print_coercions f
 (**********************************************************************)
 (* conversion of references                                           *)
 
-let ids_of_ctxt = array_map_to_list (function VAR id -> id | _ -> assert false)
+let ids_of_rctxt ctxt =
+  Array.to_list
+    (Array.map
+       (function
+	  | RRef (_,RVar id) -> id
+	  | _ ->
+       error
+       "Termast: arbitrary substitution of references not yet implemented")
+     ctxt)
+
+let ids_of_ctxt ctxt =
+  Array.to_list
+    (Array.map
+       (function
+	  | VAR id -> id
+	  | _ ->
+       error
+       "Termast: arbitrary substitution of references not yet implemented")
+     ctxt)
 
 let ast_of_ident id = nvar (string_of_id id)
 
@@ -101,17 +119,17 @@ let ast_of_inductive_ref ((sp,tyi) as ind_sp,ids) =
     try ast_of_qualified sp (Global.id_of_global (MutInd ind_sp))
     with Not_found -> nvar (string_of_path sp) (* May happen while debugging *)
 
-let ast_of_inductive (ev,ids) = ast_of_inductive_ref (ev,ids_of_ctxt ids)
+let ast_of_inductive (ev,ctxt) = ast_of_inductive_ref (ev,ids_of_ctxt ctxt)
 
 let ast_of_ref = function
-  | RConst (sp,ids) -> ast_of_constant_ref (sp,ids)
+  | RConst (sp,ctxt) -> ast_of_constant_ref (sp,ids_of_rctxt ctxt)
   | RAbst (sp) ->
       ope("ABST", (path_section dummy_loc sp)
 	    ::(List.map ast_of_ident (* on triche *) []))
-  | RInd (ind,ids) -> ast_of_inductive_ref (ind,ids)
-  | RConstruct (cstr,ids) -> ast_of_constructor_ref (cstr,ids)
+  | RInd (ind,ctxt) -> ast_of_inductive_ref (ind,ids_of_rctxt ctxt)
+  | RConstruct (cstr,ctxt) -> ast_of_constructor_ref (cstr,ids_of_rctxt ctxt)
   | RVar id -> nvar (string_of_id id)
-  | REVar (ev,ids) -> ast_of_existential_ref (ev,ids)
+  | REVar (ev,ctxt) -> ast_of_existential_ref (ev,ids_of_rctxt ctxt)
   | RMeta n -> ope("META",[num n])
 
 (**********************************************************************)
diff --git a/parsing/termast.mli b/parsing/termast.mli
index 29ff2d19c8..516856bcd9 100644
--- a/parsing/termast.mli
+++ b/parsing/termast.mli
@@ -10,7 +10,7 @@ open Rawterm
 
 (* Translation of pattern, rawterm and term into syntax trees for printing *)
 
-val ast_of_pattern : pattern -> Coqast.t
+val ast_of_pattern : cases_pattern -> Coqast.t
 val ast_of_rawconstr : rawconstr -> Coqast.t
 val bdize : bool -> unit assumptions -> constr -> Coqast.t