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, 30 insertions, 29 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index efc5190511..5fce6b5956 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -35,7 +35,7 @@ type wc = walking_constraints
 let new_evar_in_sign env =
   let ids = ids_of_var_context (Environ.var_context env) in
   let ev = new_evar () in
-  mkEvar (ev, Array.of_list (List.map (fun id -> VAR id) ids))
+  mkEvar (ev, Array.of_list (List.map mkVar ids))
 
 let rec whd_evar sigma t = match kind_of_term t with
   | IsEvar (ev,_ as evc) when is_defined sigma ev ->
@@ -92,19 +92,19 @@ let unify_0 mc wc m n =
 	    unirec_rec (unirec_rec substn t1 t2) c1 c2
 
 	| IsAppL (f1,l1), IsAppL (f2,l2) ->
-	    let len1 = List.length l1
-	    and len2 = List.length l2 in
+	    let len1 = Array.length l1
+	    and len2 = Array.length l2 in
 	    if len1 = len2 then
-              List.fold_left2 unirec_rec (unirec_rec substn f1 f2) l1 l2
+              array_fold_left2 unirec_rec (unirec_rec substn f1 f2) l1 l2
 	    else if len1 < len2 then
-              let extras,restl2 = list_chop (len2-len1) l2 in 
-	      List.fold_left2 unirec_rec 
-		(unirec_rec substn f1 (applist (f2,extras)))
+              let extras,restl2 = array_chop (len2-len1) l2 in 
+	      array_fold_left2 unirec_rec 
+		(unirec_rec substn f1 (appvect (f2,extras)))
                 l1 restl2
 	    else 
-	      let extras,restl1 = list_chop (len1-len2) l1 in 
-	      List.fold_left2 unirec_rec 
-		(unirec_rec substn (applist (f1,extras)) f2)
+	      let extras,restl1 = array_chop (len1-len2) l1 in 
+	      array_fold_left2 unirec_rec 
+		(unirec_rec substn (appvect (f1,extras)) f2)
                 restl1 l2
 		
 	| IsMutCase (_,p1,c1,cl1), IsMutCase (_,p2,c2,cl2) ->
@@ -155,18 +155,18 @@ let unify_0 mc wc m n =
       unirec_rec (mc,[]) m n
 
 	
-let whd_castappevar_stack sigma c l = 
+let whd_castappevar_stack sigma c = 
   let rec whrec (c, l as s) =
     match kind_of_term c with
       | IsEvar (ev,args) when is_defined sigma ev -> 
 	  whrec (existential_value sigma (ev,args), l)
       | IsCast (c,_) -> whrec (c, l)
-      | IsAppL (f,args) -> whrec (f, args@l)
+      | IsAppL (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l)
       | _ -> s
   in 
-  whrec (c,l)
+  whrec (c, [])
 
-let whd_castappevar sigma c = applist(whd_castappevar_stack sigma c [])
+let whd_castappevar sigma c = applist (whd_castappevar_stack sigma c)
 
 let w_whd wc c = whd_castappevar (w_Underlying wc) c
 
@@ -245,7 +245,7 @@ and w_resrec metas evars wc =
                with ex when catchable_exception ex ->
 		 (match krhs with
              	    | IsAppL (f,cl) when isConst f ->
-			let wc' = mimick_evar f (List.length cl) evn wc in
+			let wc' = mimick_evar f (Array.length cl) evn wc in
 			w_resrec metas evars wc'
 		    | _ -> error "w_Unify"))
 	| _ -> anomaly "w_resrec"
@@ -445,7 +445,7 @@ let clenv_cast_meta clenv =
 	       | Clval(_) -> u
 	   with Not_found -> 
 	     u)
-      | IsAppL(f,args) -> mkAppList (crec_hd f) (List.map crec args)
+      | IsAppL(f,args) -> mkAppL (crec_hd f, Array.map crec args)
       | IsMutCase(ci,p,c,br) ->
 	  mkMutCase (ci, crec_hd p, crec_hd c, Array.map crec br)
       | _ -> u
@@ -553,7 +553,8 @@ let clenv_merge with_types =
 		   (match krhs with
 		      | IsAppL (f,cl) when isConst f or isMutConstruct f ->
 			  clenv_resrec metas evars 
-			    (clenv_wtactic (mimick_evar f (List.length cl) evn)
+			    (clenv_wtactic
+			       (mimick_evar f (Array.length cl) evn)
 			       clenv)
            	      | _ -> error "w_Unify"))
 
@@ -681,7 +682,7 @@ let constrain_clenv_to_subterm clause (op,cl) =
        else error "Bound 1"
      with ex when catchable_exception ex ->
        (match kind_of_term (telescope_appl cl) with 
-	  | IsAppL (c1,[c2]) ->
+	  | IsAppL (c1,[|c2|]) ->
 	      (try 
 		 matchrec c1 
 	       with ex when catchable_exception ex -> 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index e06949be3f..fdece93e21 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -70,7 +70,8 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 
     | IsAppL (f,l) ->
 	let (acc',hdty) = mk_hdgoals sigma goal goalacc f in
-	let (acc'',conclty') = mk_arggoals sigma goal acc' hdty l in
+	let (acc'',conclty') =
+	  mk_arggoals sigma goal acc' hdty (Array.to_list l) in
 	let _ = conv_leq_goal env sigma trm conclty' conclty in
         (acc'',conclty')
 
@@ -103,7 +104,7 @@ and mk_hdgoals sigma goal goalacc trm =
 
     | IsAppL (f,l) ->
 	let (acc',hdty) = mk_hdgoals sigma goal goalacc f in
-	mk_arggoals sigma goal acc' hdty l
+	mk_arggoals sigma goal acc' hdty (Array.to_list l)
 
     | IsMutCase (_,p,c,lf) ->
 	let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in
@@ -155,7 +156,7 @@ let new_meta_variables =
   let rec newrec x = match kind_of_term x with
     | IsMeta _ -> mkMeta (new_meta())
     | IsCast (c,t) -> mkCast (newrec c, t)
-    | IsAppL (f,cl) -> applist (newrec f, List.map newrec cl)
+    | IsAppL (f,cl) -> appvect (newrec f, Array.map newrec cl)
     | IsMutCase (ci,p,c,lf) ->
 	mkMutCase (ci, newrec p, newrec c, Array.map newrec lf)
     | _ -> x
@@ -298,13 +299,13 @@ let prim_refiner r sigma goal =
 	   | IsProd (_,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
 	       let a = get_assumption_of env sigma c1
-	       and v = VAR id in
+	       and v = mkVar id in
 	       let sg = mk_goal info (push_var_decl (id,a) env) (subst1 v b) in
 	       [sg]
 	   | IsLetIn (_,c1,t1,b) ->
 	       if occur_meta c1 or occur_meta t1 then error_use_instantiate();
 	       let a = get_assumption_of env sigma t1
-	       and v = VAR id in
+	       and v = mkVar id in
 	       let sg =
 		 mk_goal info (push_var_def (id,c1,a) env) (subst1 v b) in
 	       [sg]
@@ -319,14 +320,14 @@ let prim_refiner r sigma goal =
 	   | IsProd (_,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
 	       let a = get_assumption_of env sigma c1
-	       and v = VAR id in
+	       and v = mkVar id in
 	       let env' = insert_after_hyp env whereid (id,None,a) in
 	       let sg = mk_goal info env' (subst1 v b) in 
 	       [sg]
 	   | IsLetIn (_,c1,t1,b) ->
 	       if occur_meta c1 or occur_meta t1 then error_use_instantiate();
 	       let a = get_assumption_of env sigma t1
-	       and v = VAR id in
+	       and v = mkVar id in
 	       let env' = insert_after_hyp env whereid (id,Some c1,a) in
 	       let sg = mk_goal info env' (subst1 v b) in 
 	       [sg]
@@ -339,14 +340,14 @@ let prim_refiner r sigma goal =
            | IsProd (_,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
 	       let a = get_assumption_of env sigma c1
-	       and v = VAR id in
+	       and v = mkVar id in
 	       let env' = replace_hyp env id (id,None,a) in
 	       let sg = mk_goal info env' (subst1 v b) in
 	       [sg]
            | IsLetIn (_,c1,t1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
 	       let a = get_assumption_of env sigma t1
-	       and v = VAR id in
+	       and v = mkVar id in
 	       let env' = replace_hyp env id (id,Some c1,a) in
 	       let sg = mk_goal info env' (subst1 v b) in
 	       [sg]
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index e6130c3f60..ae2ebc9eec 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -61,8 +61,7 @@ val pf_reduce :
     goal sigma -> constr -> constr
 
 val pf_whd_betadeltaiota       : goal sigma -> constr -> constr
-val pf_whd_betadeltaiota_stack : 
-  goal sigma -> constr -> constr list -> constr * constr list 
+val pf_whd_betadeltaiota_stack : goal sigma -> constr -> constr * constr list 
 val pf_hnf_constr              : goal sigma -> constr -> constr
 val pf_red_product             : goal sigma -> constr -> constr
 val pf_nf                      : goal sigma -> constr -> constr