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

10 files changed, 95 insertions, 142 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 1e48d3443c..0745081760 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -74,13 +74,6 @@ let count_rec_arg j =
   in 
   crec 0
 
-(* Used in Program only *)      
-let make_case_ml isrec pred c ci lf = 
-  if isrec then 
-    DOPN(XTRA("REC"),Array.append [|pred;c|] lf)
-  else 
-    mkMutCase (ci, pred, c, lf)
-
 (* if arity of mispec is (p_bar:P_bar)(a_bar:A_bar)s where p_bar are the
  * K parameters. Then then build_notdep builds the predicate
  * [a_bar:A'_bar](lift k pred) 
@@ -160,11 +153,11 @@ let insert_lifted a = (0,a);;
 
 (* INVARIANT:
 
-   The pattern variables of it are the disjoint union of [user_ids]
-   and the domain of [subst]. Non global VAR in the codomain of [subst] are
-   in private_ids.
-   The non pattern variables of it + the global VAR in the codomain of
-   [subst] are in others_ids
+   The pattern variables for [it] are the disjoint union of [user_ids]
+   and the domain of [subst]. Non global Var in the codomain of [subst] are
+   in [private_ids].
+   The non pattern variables of [it] + the global Var in the codomain of
+   [subst] are in [other_ids]
 
 *)
 
@@ -496,7 +489,14 @@ let push_rels_eqn sign eqn =
   {eqn with
      rhs = {eqn.rhs with
 	      rhs_env = push_rels sign' eqn.rhs.rhs_env} }
-
+(*
+let push_decls_eqn sign eqn =
+  let pats = List.rev (fst (list_chop (List.length sign) eqn.patterns)) in
+  let sign' = recover_pat_names (sign, pats) in
+  {eqn with
+     rhs = {eqn.rhs with
+	      rhs_env = push_decls sign' eqn.rhs.rhs_env} }
+*)
 let prepend_pattern tms eqn = {eqn with patterns = tms@eqn.patterns }
 
 (*
@@ -510,19 +510,10 @@ let pop_pattern eqn = { eqn with patterns = List.tl eqn.patterns }
 
 exception Occur
 let noccur_between_without_evar n m term = 
-  let rec occur_rec n = function
-    | Rel(p)        -> if n<=p && p<n+m then raise Occur
-    | VAR _         -> ()
-    | DOPN(Evar _,cl) -> ()
-    | DOPN(_,cl)    -> Array.iter (occur_rec n) cl
-    | DOP1(_,c)     -> occur_rec n c
-    | DOP2(_,c1,c2) -> occur_rec n c1; occur_rec n c2
-    | DLAM(_,c)     -> occur_rec (n+1) c
-    | DLAMV(_,v)    -> Array.iter (occur_rec (n+1)) v
-    | CLam (_,t,c)   -> occur_rec n (body_of_type t); occur_rec (n+1) c
-    | CPrd (_,t,c)   -> occur_rec n (body_of_type t); occur_rec (n+1) c
-    | CLet (_,b,t,c) -> occur_rec n b; occur_rec n (body_of_type t); occur_rec (n+1) c
-    | _             -> ()
+  let rec occur_rec n c = match kind_of_term c with
+    | IsRel p       -> if n<=p && p<n+m then raise Occur
+    | IsEvar (_,cl) -> ()
+    | _             -> iter_constr_with_binders succ occur_rec n c
   in 
   try occur_rec n term; true with Occur -> false
 
@@ -1075,15 +1066,20 @@ let compile_cases loc (typing_fun,isevars) tycon env (predopt, tomatchl, eqns)=
   (* with the type of arguments to match *)
   let pred = prepare_predicate typing_fun isevars env tomatchs predopt in
 
+  (* We push the initial terms to match and push their alias to rhs' envs *)
+  (* names of aliases will be recovered from patterns (hence Anonymous here) *)
   let initial_pushed =
     List.map (fun tm -> Pushed (insert_lifted (tm,NotDepInRhs))) tomatchs in
+  let initial_sign =
+    List.map (fun (_,t) -> (Anonymous, type_of_tomatch_type t)) tomatchs in
+  let matx_with_initial_aliases = (*List.map (push_rels_eqn initial_sign) *)matx in
 
   let pb =
     { env      = env;
       isevars  = isevars;
       pred     = pred;
       tomatch  = initial_pushed;
-      mat      = matx;
+      mat      = matx_with_initial_aliases;
       typing_function = typing_fun } in
   
   let j = compile pb in
diff --git a/pretyping/class.ml b/pretyping/class.ml
index 6c0da8c204..ee759ad96d 100644
--- a/pretyping/class.ml
+++ b/pretyping/class.ml
@@ -127,7 +127,7 @@ let constructor_at_head1 t =
       | IsVar id -> t',[],[],CL_Var id,0
       | IsCast (c,_) -> aux c
       | IsAppL(f,args) -> 
-	  let t',_,l,c,_ = aux f in t',args,l,c,List.length args
+	  let t',_,l,c,_ = aux f in t',Array.to_list args,l,c,Array.length args
       | IsProd (_,_,_) -> t',[],[],CL_FUN,0
       | IsLetIn (_,_,_,c) -> aux c
       | IsSort _ -> t',[],[],CL_SORT,0
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index f5af725b26..d8475e50e3 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -20,11 +20,11 @@ type cte_typ =
   | NAM_Inductive of inductive_path
   | NAM_Constructor of constructor_path
 
-let cte_of_constr = function  
-  | DOPN(Const sp,_) -> NAM_Constant sp
-  | DOPN(MutInd ind_sp,_) -> NAM_Inductive ind_sp
-  | DOPN(MutConstruct cstr_cp,_) -> NAM_Constructor cstr_cp
-  | VAR id -> NAM_Var id
+let cte_of_constr c = match kind_of_term c with
+  | IsConst (sp,_) -> NAM_Constant sp
+  | IsMutInd (ind_sp,_) -> NAM_Inductive ind_sp
+  | IsMutConstruct (cstr_cp,_) -> NAM_Constructor cstr_cp
+  | IsVar id -> NAM_Var id
   |  _ -> raise Not_found
 
 type cl_typ = 
@@ -196,7 +196,7 @@ let constructor_at_head t =
     | IsLetIn (_,_,_,c) -> aux c
     | IsSort _ -> CL_SORT,0
     | IsCast (c,_) -> aux (collapse_appl c)
-    | IsAppL (f,args) -> let c,_ = aux f in c, List.length args
+    | IsAppL (f,args) -> let c,_ = aux f in c, Array.length args
     |  _ -> raise Not_found
   in 
   aux (collapse_appl t)
@@ -217,13 +217,7 @@ let class_of env sigma t =
   in
   if n = n1 then t,i else raise Not_found
 
-let rec class_args_of c = 
-  let aux = function 
-    | (DOP2(Cast,c,_)) -> class_args_of c
-    | (DOPN(AppL,cl)) -> Array.to_list(array_tl cl)
-    | _ -> []
-  in 
-  aux (collapse_appl c)
+let class_args_of c = snd (decomp_app c)
 
 (* verfications pour l'ajout d'une classe *)
 
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 7197110bf3..c298852f40 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -80,14 +80,14 @@ let inh_tosort_force env isevars j =
 
 let inh_tosort env isevars j = 
   let typ = whd_betadeltaiota env !isevars (body_of_type j.uj_type) in
-  match typ with
-    | DOP0(Sort _) -> j  (* idem inh_app_fun *)
+  match kind_of_term typ with
+    | IsSort _ -> j  (* idem inh_app_fun *)
     | _ -> inh_tosort_force env isevars j
 
 let inh_ass_of_j env isevars j =
   let typ = whd_betadeltaiota env !isevars (body_of_type j.uj_type) in
-  match typ with
-    | DOP0(Sort s) -> { utj_val = j.uj_val; utj_type = s }
+  match kind_of_term typ with
+    | IsSort s -> { utj_val = j.uj_val; utj_type = s }
     | _ ->
         let j1 = inh_tosort_force env isevars j in 
 	type_judgment env !isevars j1 
@@ -147,7 +147,7 @@ let rec inh_conv_coerce_to_fail env isevars c1 hj =
 		   {uj_val = Rel 1; 
 		    uj_type = typed_app (fun _ -> u1) assu1 } in
                let h2 = inh_conv_coerce_to_fail env isevars u2  
-			 { uj_val = DOPN(AppL,[|(lift 1 v);h1.uj_val|]);
+			 { uj_val = mkAppL (lift 1 v, [|h1.uj_val|]);
                            uj_type = get_assumption_of env1 !isevars
 				       (subst1 h1.uj_val t2) }
 	       in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index ce72f7e011..0801d8f2c3 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -49,33 +49,7 @@ let occur_id env id0 c =
   in 
   try occur 1 c; false
   with Occur -> true
-(*
-let occur_id env_names id0 c =
-  let rec occur n = function
-    | VAR id             -> id=id0
-    | DOPN (Const sp,cl) -> (basename sp = id0) or (array_exists (occur n) cl)
-    | DOPN (MutInd ind_sp, cl) as t -> 
-  	(basename (path_of_inductive_path ind_sp) = id0)
-	or (array_exists (occur n) cl)
-    | DOPN (MutConstruct cstr_sp, cl) as t -> 
-    	(basename (path_of_constructor_path cstr_sp) = id0)
-	or (array_exists (occur n) cl)
-    | DOPN(_,cl)         -> array_exists (occur n) cl
-    | DOP1(_,c)          -> occur n c
-    | DOP2(_,c1,c2)      -> (occur n c1) or (occur n c2)
-    | DLAM(_,c)          -> occur (n+1) c
-    | DLAMV(_,v)         -> array_exists (occur (n+1)) v
-    | CLam (_,t,c)   -> occur n (body_of_type t) or occur (n+1) c
-    | CPrd (_,t,c)   -> occur n (body_of_type t) or occur (n+1) c
-    | CLet (_,b,t,c) -> occur n b or occur n (body_of_type t) or occur (n+1) c
-    | Rel p              ->
-    	p>n &
-    	(try lookup_name_of_rel (p-n) env_names = Name id0
-	 with Not_found -> false) (* Unbound indice: may happen in debug *)
-    | DOP0 _             -> false
-  in 
-  occur 1 c
-*)
+
 let next_name_not_occuring name l env_names t =
   let rec next id =
     if List.mem id l or occur_id env_names id t then next (lift_ident id)
@@ -314,7 +288,7 @@ let rec detype avoid env t =
     | IsLambda (na,ty,c) -> detype_binder BLambda avoid env na ty c
     | IsLetIn (na,b,_,c) -> detype_binder BLetIn avoid env na b c
     | IsAppL (f,args) ->
-	RApp (dummy_loc,detype avoid env f,List.map (detype avoid env) args)
+	RApp (dummy_loc,detype avoid env f,array_map_to_list (detype avoid env) args)
     | IsConst (sp,cl) ->
 	RRef(dummy_loc,RConst(sp,Array.map (detype avoid env) cl))
     | IsEvar (ev,cl) ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 4f551f31dd..0a400a3a6d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -44,12 +44,15 @@ open Evarutil
  * ass.
  *)
 
-let rec evar_apprec env isevars stack c =
-  let (t,stack) = Reduction.apprec env !isevars c stack in 
-  if ise_defined isevars t then 
-    evar_apprec env isevars stack (existential_value !isevars (destEvar t))
-  else 
-    (t,stack)
+let evar_apprec env isevars stack c =
+  let rec aux s =
+    let (t,stack as s') = Reduction.apprec env !isevars s in
+    match kind_of_term t with
+      | IsEvar (n,_ as ev) when Evd.is_defined !isevars n ->
+	  aux (existential_value !isevars ev, stack)
+      | _ -> (t, list_of_stack stack)
+  in aux (c, append_stack (Array.of_list stack) empty_stack)
+
 
 let conversion_problems = ref ([] : (conv_pb * constr * constr) list)
 
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index e94ac55d39..c360df8695 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -153,12 +153,12 @@ let ise_map isevars sp = Evd.map !isevars sp
 let ise_define isevars sp body = isevars := Evd.define !isevars sp body
 
 (* Does k corresponds to an (un)defined existential ? *)
-let ise_undefined isevars = function
-  | DOPN(Evar n,_) -> not (Evd.is_defined !isevars n)
+let ise_undefined isevars c = match kind_of_term c with
+  | IsEvar (n,_) -> not (Evd.is_defined !isevars n)
   | _ -> false
 
-let ise_defined isevars = function
-  | DOPN(Evar n,_) -> Evd.is_defined !isevars n
+let ise_defined isevars c = match kind_of_term c with
+  | IsEvar (n,_) -> Evd.is_defined !isevars n
   | _ -> false
 
 let restrict_hyps isevars c =
@@ -180,6 +180,22 @@ let has_ise sigma t =
  * conversion test that lead to the faulty call to [real_clean] should return
  * false. The problem is that we won't get the right error message.
  *)
+
+let real_clean isevars sp args rhs =
+  let subst = List.map (fun (x,y) -> (y,VAR x)) (filter_unique args) in
+  let rec subs k t =
+    match kind_of_term t with
+      |IsRel i ->
+ 	 if i<=k then t
+ 	 else (try List.assoc (Rel (i-k)) subst with Not_found -> t)
+      | IsVar _ -> (try List.assoc t subst with Not_found -> t)
+      | _ -> map_constr_with_binders (fun na k -> k+1) subs k t
+  in
+  let body = subs 0 rhs in
+  (* if not (closed0 body) then error_not_clean CCI empty_env sp body; *)
+  body
+
+(*
 let real_clean isevars sp args rhs =
   let subst = List.map (fun (x,y) -> (y,VAR x)) (filter_unique args) in
   let rec subs k t =
@@ -201,6 +217,7 @@ let real_clean isevars sp args rhs =
   let body = subs 0 rhs in
   (* if not (closed0 body) then error_not_clean CCI empty_env sp body; *)
   body
+*)
 
 let make_instance_with_rel env =
   let n = rel_context_length (rel_context env) in
@@ -233,7 +250,7 @@ let new_isevar isevars env typ k =
   evar
 
 (* [evar_define] solves the problem lhs = rhs when lhs is an uninstantiated
- * evar, i.e. tries to find the body ?sp for lhs=DOPN(Const sp,args)
+ * evar, i.e. tries to find the body ?sp for lhs=mkConst (sp,args)
  * ?sp [ sp.hyps \ args ]  unifies to rhs
  * ?sp must be a closed term, not referring to itself.
  * Not so trivial because some terms of args may be terms that are not
@@ -340,29 +357,28 @@ let has_undefined_isevars isevars c =
 let head_is_exist isevars = 
   let rec hrec k = match kind_of_term k with
     | IsEvar _     -> ise_undefined isevars k
-    | IsAppL (f,l) -> hrec f
+    | IsAppL (f,_) -> hrec f
     | IsCast (c,_) -> hrec c
     | _ -> false
   in 
   hrec 
 
-let rec is_eliminator = function
-  | DOPN (AppL,_)      -> true
-  | DOPN (MutCase _,_) -> true
-  | DOP2 (Cast,c,_)    -> is_eliminator c
+let rec is_eliminator c = match kind_of_term c with
+  | IsAppL _    -> true
+  | IsMutCase _ -> true
+  | IsCast (c,_) -> is_eliminator c
   | _ -> false
 
 let head_is_embedded_exist isevars c =
   (head_is_exist isevars c) & (is_eliminator c)
 
 let head_evar = 
-  let rec hrec = function
-    | DOPN(Evar ev,_)       -> ev
-    | DOPN(MutCase _,_) as mc -> 
-	let (_,_,c,_) = destCase mc in hrec c
-    | DOPN(AppL,cl)          -> hrec (array_hd cl)
-    | DOP2(Cast,c,_)         -> hrec c
-    | _                      -> failwith "headconstant"
+  let rec hrec c = match kind_of_term c with
+    | IsEvar (ev,_)       -> ev
+    | IsMutCase (_,_,c,_) -> hrec c
+    | IsAppL (c,_)        -> hrec c
+    | IsCast (c,_)        -> hrec c
+    | _                   -> failwith "headconstant"
   in 
   hrec 
     
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 41f1878d6b..5743d7d063 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -27,38 +27,6 @@ open Coercion
 open Inductive
 open Instantiate
 
-(*
-(* Pour le vieux "match" que Program utilise encore, vieille histoire ... *)
-
-(* Awful special reduction function which skips abstraction on Xtra in
-   order to be safe for Program ... *)
-
-let stacklamxtra recfun = 
-  let rec lamrec sigma s t = match s,kind_of_term t with 
-    | (stack, IsLambda (_,DOP1(XTRA "COMMENT",_),_)) ->
-        recfun stack (substl sigma t)
-    | ((h::t), IsLambda (_,_,c)) -> lamrec (h::sigma) t c
-    | (stack, _) -> recfun stack (substl sigma t)
-  in 
-  lamrec 
-
-let rec whrec x stack =
-  match kind_of_term x with   
-    | IsLambda (name, DOP1(XTRA "COMMENT",c),t) ->
-    	let t' = applist (whrec t (List.map (lift 1) stack)) in 
-	mkLambda (name,DOP1(XTRA "COMMENT",c),t'),[]
-    | IsLambda (name,c1,c2) ->
-    	(match stack with
-	   | [] -> mkLambda (name,c1,whd_betaxtra c2),[]
-	   | a1::rest -> stacklamxtra (fun l x -> whrec x l) [a1] rest c2)
-    | IsAppL (f,args) -> whrec f (args@stack)
-    | IsCast (c,_) ->  whrec c stack
-    | _ -> x,stack
-
-and whd_betaxtra x = applist(whrec x [])
-*)
-let whd_betaxtra = whd_beta
-
 let lift_context n l = 
   let k = List.length l in 
   list_map_i (fun i (name,c) -> (name,liftn n (k-i) c)) 0 l
@@ -85,7 +53,7 @@ let transform_rec loc env sigma (p,c,lf) (indt,pt) =
     let branches = 
       array_map3
 	(fun f t reca -> 
-	   whd_betaxtra
+	   whd_beta
              (Indrec.make_rec_branch_arg env sigma
                 (nparams,depFvec,nar+1)
                 f t reca))
@@ -109,9 +77,9 @@ let transform_rec loc env sigma (p,c,lf) (indt,pt) =
 			     (List.map (lift nar) params)
 			     (rel_list 0 nar))),
 	      (if dep then 
-		 applist (whd_beta_stack (lift (nar+1) p) (rel_list 0 (nar+1)))
+		 whd_beta (applist (lift (nar+1) p, rel_list 0 (nar+1)))
 	       else 
-		 applist (whd_beta_stack (lift (nar+1) p) (rel_list 1 nar)))))
+		 whd_beta (applist (lift (nar+1) p, rel_list 1 nar)))))
           lnames 
       in
       let fix = mkFix (([|nar|],0),
@@ -258,7 +226,7 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 	      user_err_loc (loc,"pretype",
 	        [< 'sTR "Metavariable "; 'iNT n; 'sTR" is unbound" >])
 	  in
-          { uj_val=DOP0 (Meta n); uj_type = outcast_type metaty })
+          { uj_val= mkMeta n; uj_type = outcast_type metaty })
 
 | RHole loc ->
   if !compter then nbimpl:=!nbimpl+1;
@@ -464,12 +432,13 @@ let process_evars fail_evar env sigma =
             [< 'sTR"There is an unknown subterm I cannot solve" >]
    else whd_ise1_metas env sigma)
 
-
+(*
 let j_apply f env sigma j =
-  let under_outer_cast f env sigma = function
-    | DOP2 (Cast,b,t) -> DOP2 (Cast,f env sigma b,f env sigma t)
-    | c -> f env sigma c in
-  { uj_val=strong (under_outer_cast f) env sigma j.uj_val;
+  { uj_val= local_strong (under_outer_cast (f env sigma)) j.uj_val;
+    uj_type= typed_app (strong f env sigma) j.uj_type }
+*)
+let j_apply f env sigma j =
+  { uj_val= strong f env sigma j.uj_val;
     uj_type= typed_app (strong f env sigma) j.uj_type }
 
 let utj_apply f env sigma j =
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index d6d3395e53..0bae65053c 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -34,7 +34,7 @@ let sort_of_atomic_type env sigma ft args =
     match kind_of_term (whd_betadeltaiota env sigma ar) with
       | IsProd (_, _, b) -> concl_of_arity b
       | IsSort s -> s
-      | _ -> outsort env sigma (subst_type env sigma ft args)
+      | _ -> outsort env sigma (subst_type env sigma ft (Array.to_list args))
   in concl_of_arity ft
 
 let typeur sigma metamap =
@@ -71,14 +71,15 @@ let rec type_of env cstr=
     | IsFix ((vn,i),(lar,lfi,vdef)) -> lar.(i)
     | IsCoFix (i,(lar,lfi,vdef)) -> lar.(i)
     | IsAppL(f,args)->
-      strip_outer_cast (subst_type env sigma (type_of env f) args)
+      strip_outer_cast (subst_type env sigma (type_of env f) 
+			  (Array.to_list args))
     | IsCast (c,t) -> t
     | IsSort _ | IsProd (_,_,_) | IsMutInd _ -> mkSort (sort_of env cstr)
     | IsXtra _ -> error "type_of: Unexpected constr"
 
 and sort_of env t = 
   match kind_of_term t with
-    | IsCast (c,DOP0(Sort s)) -> s
+    | IsCast (c,s) when isSort s -> destSort s
     | IsSort (Prop c) -> type_0
     | IsSort (Type u) -> Type Univ.dummy_univ
     | IsProd (name,t,c2) ->
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 99f2f09a8f..b946911e06 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -79,7 +79,7 @@ let rec execute mf env sigma cstr =
 	  
     | IsAppL (f,args) ->
 	let j = execute mf env sigma f in
-        let jl = execute_list mf env sigma args in
+        let jl = execute_list mf env sigma (Array.to_list args) in
 	let (j,_) = apply_rel_list env sigma mf.nocheck jl j in
 	j