Modification mkAppL; abstraction via kind_of_term; changement dans Reduction

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

3 files changed, 40 insertions, 42 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 1a2cc53aef..af2f73b130 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -112,8 +112,8 @@ let ids_of_ctxt ctxt =
 
 let maybe_constructor env s =
   try 
-    match Declare.global_reference CCI (id_of_string s) with 
-      | DOPN(MutConstruct (spi,j),cl) -> Some ((spi,j),ids_of_ctxt cl)
+    match kind_of_term (Declare.global_reference CCI (id_of_string s)) with 
+      | IsMutConstruct ((spi,j),cl) -> Some ((spi,j),ids_of_ctxt cl)
       | _ -> warning ("Defined identifier "
 		      ^s^" is here considered as a matching variable"); None
   with Not_found -> 
@@ -156,13 +156,12 @@ let dbize_global loc = function
   | _ -> anomaly_loc (loc,"dbize_global",
 		      [< 'sTR "Bad ast for this global a reference">])
 
-let ref_from_constr = function
-  | DOPN (Const sp,ctxt) -> RConst (sp, dbize_constr_ctxt ctxt)
-  | DOPN (Evar ev,ctxt) -> REVar (ev, dbize_constr_ctxt ctxt) 
-  | DOPN (MutConstruct (spi,j),ctxt) -> 
-      RConstruct ((spi,j), dbize_constr_ctxt ctxt)
-  | DOPN (MutInd (sp,i),ctxt) -> RInd ((sp,i), dbize_constr_ctxt ctxt)
-  | VAR id -> RVar id  (* utilisé pour coe_value (tmp) *)
+let ref_from_constr c = match kind_of_term c with
+  | IsConst (sp,ctxt) -> RConst (sp, dbize_constr_ctxt ctxt)
+  | IsEvar (ev,ctxt) -> REVar (ev, dbize_constr_ctxt ctxt) 
+  | IsMutConstruct (csp,ctxt) -> RConstruct (csp, dbize_constr_ctxt ctxt)
+  | IsMutInd (isp,ctxt) -> RInd (isp, dbize_constr_ctxt ctxt)
+  | IsVar id -> RVar id  (* utilisé pour coe_value (tmp) *)
   | _ -> anomaly "Not a reference"
 
 (* [vars1] is a set of name to avoid (used for the tactic language);
@@ -469,14 +468,14 @@ let ast_adjust_consts sigma = (* locations are kept *)
 	   ast
 	 else 
 	   try 
-	     match Declare.global_reference CCI id with
-	       | DOPN (Const sp,_) -> 
+	     match kind_of_term (Declare.global_reference CCI id) with
+	       | IsConst (sp,_) -> 
 		   Node(loc,"CONST",[path_section loc sp])
-	       | DOPN (Evar ev,_) ->
+	       | IsEvar (ev,_) ->
 		   Node(loc,"EVAR",[Num(loc,ev)])
-	       | DOPN (MutConstruct ((sp,i),j),_) ->
+	       | IsMutConstruct (((sp,i),j),_) ->
 		   Node (loc,"MUTCONSTRUCT",[path_section loc sp;num i;num j])
-	       | DOPN (MutInd (sp,i),_) ->
+	       | IsMutInd ((sp,i),_) ->
 		   Node (loc,"MUTIND",[path_section loc sp;num i])
 	       | _ -> anomaly "Not a reference"
 	   with UserError _ | Not_found ->
diff --git a/parsing/pattern.ml b/parsing/pattern.ml
index f84a2d929c..47c1d5716d 100644
--- a/parsing/pattern.ml
+++ b/parsing/pattern.ml
@@ -64,11 +64,11 @@ let rec head_pattern_bound t =
     | PRel _ | PMeta _ | PSoApp _  | PSort _ -> raise BoundPattern
     | PBinder(BLambda,_,_,_) -> anomaly "head_pattern_bound: not a type"
 
-let head_of_constr_reference = function
-  | DOPN (Const sp,_) -> ConstNode sp
-  | DOPN (MutConstruct sp,_) -> CstrNode sp
-  | DOPN (MutInd sp,_) -> IndNode sp
-  | VAR id -> VarNode id
+let head_of_constr_reference c = match kind_of_term c with
+  | IsConst (sp,_) -> ConstNode sp
+  | IsMutConstruct (sp,_) -> CstrNode sp
+  | IsMutInd (sp,_) -> IndNode sp
+  | IsVar id -> VarNode id
   | _ -> anomaly "Not a rigid reference"
 
 
@@ -166,8 +166,7 @@ let matches_core convert pat c =
       | PSort RType, IsSort (Type _) -> sigma
 
       | PApp (c1,arg1), IsAppL (c2,arg2) ->
-	  array_fold_left2 (sorec stk) (sorec stk sigma c1 c2)
-	    arg1 (Array.of_list arg2)
+	  array_fold_left2 (sorec stk) (sorec stk sigma c1 c2) arg1 arg2
 
       | PBinder(BProd,na1,c1,d1), IsProd(na2,c2,d2) ->
 	  sorec ((na2,c2)::stk) (sorec stk sigma c1 c2) d1 d2
@@ -221,7 +220,7 @@ let rec try_matches nocc pat = function
 let rec sub_match nocc pat c =
   match kind_of_term c with
   | IsCast (c1,c2) ->
-    (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with
+    (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
     | PatternMatchingFailure ->
       let (lm,lc) = try_sub_match nocc pat [c1] in
       (lm,mkCast (List.hd lc, c2))
@@ -229,7 +228,7 @@ let rec sub_match nocc pat c =
       let (lm,lc) = try_sub_match (nocc - 1) pat [c1] in
       (lm,mkCast (List.hd lc, c2)))
   | IsLambda (x,c1,c2) ->
-    (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with
+    (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
     | PatternMatchingFailure ->
       let (lm,lc) = try_sub_match nocc pat [c1;c2] in
       (lm,mkLambda (x,List.hd lc,List.nth lc 1))
@@ -237,7 +236,7 @@ let rec sub_match nocc pat c =
       let (lm,lc) = try_sub_match (nocc - 1) pat [c1;c2] in
       (lm,mkLambda (x,List.hd lc,List.nth lc 1)))
   | IsProd (x,c1,c2) ->
-    (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with
+    (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
     | PatternMatchingFailure ->
       let (lm,lc) = try_sub_match nocc pat [c1;c2] in
       (lm,mkProd (x,List.hd lc,List.nth lc 1))
@@ -245,7 +244,7 @@ let rec sub_match nocc pat c =
       let (lm,lc) = try_sub_match (nocc - 1) pat [c1;c2] in
       (lm,mkProd (x,List.hd lc,List.nth lc 1)))
   | IsLetIn (x,c1,t2,c2) ->
-    (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with
+    (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
     | PatternMatchingFailure ->
       let (lm,lc) = try_sub_match nocc pat [c1;t2;c2] in
       (lm,mkLetIn (x,List.hd lc,List.nth lc 1,List.nth lc 2))
@@ -253,15 +252,15 @@ let rec sub_match nocc pat c =
       let (lm,lc) = try_sub_match (nocc - 1) pat [c1;t2;c2] in
       (lm,mkLetIn (x,List.hd lc,List.nth lc 1,List.nth lc 2)))
   | IsAppL (c1,lc) ->
-    (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with
+    (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
     | PatternMatchingFailure ->
-      let (lm,le) = try_sub_match nocc pat (c1::lc) in
-      (lm,mkAppL (Array.of_list le))
+      let (lm,le) = try_sub_match nocc pat (c1::(Array.to_list lc)) in
+      (lm,mkAppList le)
     | NextOccurrence nocc ->
-      let (lm,le) = try_sub_match (nocc - 1) pat (c1::lc) in
-      (lm,mkAppL (Array.of_list le)))
+      let (lm,le) = try_sub_match (nocc - 1) pat (c1::(Array.to_list lc)) in
+      (lm,mkAppList le))
   | IsMutCase (ci,hd,c1,lc) ->
-    (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with
+    (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
     | PatternMatchingFailure ->
       let (lm,le) = try_sub_match nocc pat (c1::Array.to_list lc) in
       (lm,mkMutCaseL (ci,hd,List.hd le,List.tl le))
@@ -270,7 +269,7 @@ let rec sub_match nocc pat c =
       (lm,mkMutCaseL (ci,hd,List.hd le,List.tl le)))
   | IsMutConstruct _ | IsFix _ | IsMutInd _|IsCoFix _ |IsEvar _|IsConst _
   | IsRel _|IsMeta _|IsVar _|IsXtra _|IsSort _ ->
-    (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with
+    (try authorized_occ nocc ((matches pat c),mkMeta (-1)) with
     | PatternMatchingFailure -> raise (NextOccurrence nocc)
     | NextOccurrence nocc -> raise (NextOccurrence (nocc - 1)))
 
@@ -311,8 +310,7 @@ let rec pattern_of_constr t =
     | IsLambda (na,c,b) ->
 	PBinder (BLambda,na,pattern_of_constr c,pattern_of_constr b)
     | IsAppL (f,args)   ->
-	PApp (pattern_of_constr f,
-	      Array.of_list (List.map pattern_of_constr args))
+	PApp (pattern_of_constr f, Array.map pattern_of_constr args)
     | IsConst (cst_sp,ctxt)         ->
 	PRef (RConst (cst_sp, ctxt))
     | IsMutInd (ind_sp,ctxt)        ->
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index d9e22af376..a6f4bdb0e6 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -349,8 +349,8 @@ let crible (fn : string -> env -> constr -> unit) name =
                let mib = Global.lookup_mind sp in 
 	       let arities = array_map_to_list (fun mip -> (Name mip.mind_typename, None, mip.mind_nf_arity)) mib.mind_packets in
 	       let env_ar = push_rels arities env in
-               (match const with 
-		  | (DOPN(MutInd(sp',tyi),_)) -> 
+               (match kind_of_term const with 
+		  | IsMutInd ((sp',tyi),_) -> 
 		      if sp = objsp_of sp' then
 			print_constructors fn env_ar
 			  (mind_nth_type_packet mib tyi)
@@ -493,7 +493,7 @@ let unfold_head_fconst =
   let rec unfrec k = match kind_of_term k with
     | IsConst _ -> constant_value (Global.env ()) k 
     | IsLambda (na,t,b) -> mkLambda (na,t,unfrec b)
-    | IsAppL (f,v) -> applist (unfrec f,v)
+    | IsAppL (f,v) -> appvect (unfrec f,v)
     | _ -> k
   in 
   unfrec
@@ -502,8 +502,9 @@ let unfold_head_fconst =
 let print_extracted_name name =
   let (sigma,(sign,fsign)) = initial_sigma_assumptions() in
   try
-    match (Machops.global (gLOB sign) name) with
-      | DOPN(Const _,_) as x ->
+    let x = (Machops.global (gLOB sign) name) in
+    match kind_of_term x with
+      | IsConst _ ->
           let cont = snd(infexecute sigma (sign,fsign) x) in 
           (match cont with
              | Inf {_VAL=trm; _TYPE=typ} ->
@@ -519,7 +520,7 @@ let print_extracted_name name =
 			 [< >]; 
 		       'sTR " :  "; fprterm typ; 'fNL >])
              | _ -> error "Non informative term")
-      | VAR id ->
+      | IsVar id ->
 	  (* Pourquoi on n'utilise pas fsign ? *)
           let a = snd(lookup_sign id sign) in
           let cont = snd(infexecute sigma (sign,fsign) a.body) in 
@@ -530,14 +531,14 @@ let print_extracted_name name =
 			fprint_var (string_of_id name) {body=t;typ=s})
              | _  -> error "Non informative term")
 	  
-      | DOPN(MutInd (sp,_),_) as x ->
+      | IsMutInd ((sp,_),_) ->
           let cont = snd(infexecute sigma (sign,fsign) x) in 
 	  (match cont with
              | Inf _ ->
                  (hOV 0 [< 'sTR (string_of_id name); 'sTR " ==>"; 'bRK(1,4);
                            print_extracted_mutual sp >])
              | _ -> error "Non informative term")
-      | DOPN(MutConstruct _ ,_) as x ->
+      | IsMutConstruct _  ->
           let cont = snd(infexecute sigma (sign,fsign) x) in 
 	  (match cont with
              | Inf d ->