uniformisation avec constr des lieurs dans rawterm/pattern

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

7 files changed, 69 insertions, 88 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index da66f63a4..2909ff125 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -338,7 +338,9 @@ let occur_rawconstr id =
   let rec occur = function
     | RVar (loc,id') -> id = id'
     | RApp (loc,f,args) -> (occur f) or (List.exists occur args)
-    | RBinder (loc,bk,na,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
+    | RLambda (loc,na,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
+    | RProd (loc,na,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
+    | RLetIn (loc,na,b,c) -> (occur b) or ((na <> Name id) & (occur c))
     | RCases (loc,prinfo,tyopt,tml,pl) ->
 	(occur_option tyopt) or (List.exists occur tml)
 	or (List.exists occur_pattern pl)
@@ -543,8 +545,8 @@ let prepare_unif_pb typ cs =
     if noccur_between_without_evar 1 n p then lift (-n) p
     else (* TODO4-1 *)
       error "Inference of annotation not yet implemented in this case" in
-  let ci = applist
-	     (mkMutConstruct cs.cs_cstr, cs.cs_params@(rel_list (-n) n)) in
+  let args = extended_rel_list (-n) cs.cs_args in
+  let ci = applist (mkMutConstruct cs.cs_cstr, cs.cs_params@args) in
 
   (* This is the problem: finding P s.t. cs_args |- (P realargs ci) = p' *)
   (Array.map (lift (-n)) cs.cs_concl_realargs, ci, p')
@@ -821,7 +823,7 @@ let build_branch pb defaults eqns const_info =
     applist
       (mkMutConstruct const_info.cs_cstr, 
        (List.map (lift const_info.cs_nargs) const_info.cs_params)
-       @(rel_list 0 const_info.cs_nargs)) in
+       @(extended_rel_list 0 const_info.cs_args)) in
 
   (* We replace [(mkRel 1)] by its expansion [ci] *)
   let updated_old_tomatch =
@@ -913,8 +915,7 @@ let prepare_initial_alias lpat tomatchl rhs =
        match alias_of_pat pat with
 	 | Anonymous -> (pat::stripped_pats, rhs)
 	 | Name _ as na ->
-	     (unalias_pat pat::stripped_pats,
-	      RBinder (dummy_loc, BLetIn, na, tm, rhs)))
+	     (unalias_pat pat::stripped_pats, RLetIn (dummy_loc, na, tm, rhs)))
     lpat tomatchl ([], rhs)
 
 (* builds the matrix of equations testing that each eqn has n patterns
@@ -961,9 +962,8 @@ exception NotCoercible
 
 let inh_coerce_to_ind isevars env ty tyi =
   let (ntys,_) =
-    splay_prod env !isevars
-      (body_of_type (mis_nf_arity (Global.lookup_mind_specif tyi))) in
-  let (_,evarl) =
+    splay_prod env !isevars (mis_arity (Global.lookup_mind_specif tyi)) in
+   let (_,evarl) =
     List.fold_right
       (fun (na,ty) (env,evl) ->
 	 (push_rel_assum (na,ty) env,
@@ -1066,20 +1066,6 @@ let build_initial_predicate env sigma isdep pred tomatchl =
 	      PrLetIn ((realargs,cur),buildrec (n+nrealargs+1) predccl ltm)
   in buildrec 0 pred tomatchl
 
-let rec eta_expand0 env sigma n c t =
-  match kind_of_term (whd_betadeltaiota env sigma t) with
-    | IsProd (na,a,b) -> mkLambda (na,a,eta_expand0 env sigma (n+1) c b)
-    | _ -> applist (lift n c, rel_list 0 n)
-
-
-let rec eta_expand env sigma c t =
-  let c' = whd_betadeltaiota env sigma c in 
-  let t' = whd_betadeltaiota env sigma t in
-  match kind_of_term c', kind_of_term t' with
-   | IsLambda (na,ta,cb), IsProd (_,_,tb) ->
-       mkLambda (na,ta,eta_expand env sigma cb tb)
-   | _, _ -> eta_expand0 env sigma 0 c' t'
-
 (* determines wether the multiple case is dependent or not. For that
  * the predicate given by the user is eta-expanded. If the result
  * of expansion is pred, then :
@@ -1090,26 +1076,7 @@ let rec eta_expand env sigma c t =
  *        then case_dependent=true
  *        else error! (can not treat mixed dependent and non dependent case
  *)
-(*
-let case_dependent env sigma loc predj tomatchs =
-  let nb_dep_ity = function
-      (_,IsInd (_,IndType(_,realargs))) -> List.length realargs
-    | (c,NotInd t) ->
-	errorlabstrm "case_dependent" (error_case_not_inductive CCI env c t)
-  in
-  let etapred = eta_expand env sigma predj.uj_val (body_of_type predj.uj_type) in
-  let n = nb_lam etapred in
-  let _,sort = splay_prod env sigma (body_of_type predj.uj_type) in
-  let ndepv = List.map nb_dep_ity tomatchs in
-  let sum = List.fold_right (fun i j -> i+j)  ndepv 0 in
-  let depsum = sum + List.length tomatchs in
-  if n = sum then
-    (etapred,false)
-  else if n = depsum then
-    (etapred,true)
-  else
-    error_wrong_predicate_arity_loc loc CCI env etapred sum depsum
-*)
+
 let prepare_predicate typing_fun isevars env tomatchs = function
   | None -> None
   | Some pred ->
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 2e7e804aa..dc4330b5e 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -394,6 +394,8 @@ and detype_binder bk avoid env na ty c =
       match concrete_name avoid env na c with
 	| (Some id,l') -> (Name id), l'
 	| (None,l')    -> Anonymous, l' in
-  RBinder (dummy_loc,bk,
-	   na',detype [] env ty,
-	   detype avoid' (add_name na' env) c)
+  let r =  detype avoid' (add_name na' env) c in
+  match bk with
+    | BProd -> RProd (dummy_loc, na',detype [] env ty, r)
+    | BLambda -> RLambda (dummy_loc, na',detype [] env ty, r)
+    | BLetIn -> RLetIn (dummy_loc, na',detype [] env ty, r)
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 513e47ea0..625e28d56 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -15,7 +15,9 @@ type constr_pattern =
   | PRel of int
   | PApp of constr_pattern * constr_pattern array
   | PSoApp of int * constr_pattern list
-  | PBinder of binder_kind * name * constr_pattern * constr_pattern
+  | PLambda of name * constr_pattern * constr_pattern
+  | PProd of name * constr_pattern * constr_pattern
+  | PLetIn of name * constr_pattern * constr_pattern
   | PSort of rawsort
   | PMeta of int option
   | PCase of constr_pattern option * constr_pattern * constr_pattern array
@@ -25,7 +27,9 @@ type constr_pattern =
 let rec occur_meta_pattern = function
   | PApp (f,args) ->
       (occur_meta_pattern f) or (array_exists occur_meta_pattern args)
-  | PBinder(_,na,t,c)  -> (occur_meta_pattern t) or (occur_meta_pattern c)
+  | PLambda (na,t,c)  -> (occur_meta_pattern t) or (occur_meta_pattern c)
+  | PProd (na,t,c)  -> (occur_meta_pattern t) or (occur_meta_pattern c)
+  | PLetIn (na,t,c)  -> (occur_meta_pattern t) or (occur_meta_pattern c)
   | PCase(None,c,br)   ->
       (occur_meta_pattern c) or (array_exists occur_meta_pattern br)
   | PCase(Some p,c,br) ->
@@ -54,15 +58,16 @@ let label_of_ref = function
 
 let rec head_pattern_bound t =
   match t with
-    | PBinder ((BProd|BLetIn),_,_,b) -> head_pattern_bound b 
-    | PApp (c,args)         -> head_pattern_bound c
-    | PCase (p,c,br)        -> head_pattern_bound c
-    | PRef r                -> label_of_ref r
-    | PVar id               -> VarNode id
+    | PProd (_,_,b)  -> head_pattern_bound b 
+    | PLetIn (_,_,b) -> head_pattern_bound b 
+    | PApp (c,args)  -> head_pattern_bound c
+    | PCase (p,c,br) -> head_pattern_bound c
+    | PRef r         -> label_of_ref r
+    | PVar id        -> VarNode id
     | PEvar _ | PRel _ | PMeta _ | PSoApp _  | PSort _ | PFix _
 	-> raise BoundPattern
     (* Perhaps they were arguments, but we don't beta-reduce *)
-    | PBinder(BLambda,_,_,_) -> raise BoundPattern
+    | PLambda _ -> raise BoundPattern
     | PCoFix _ -> anomaly "head_pattern_bound: not a type"
 
 let head_of_constr_reference c = match kind_of_term c with
@@ -165,13 +170,13 @@ let matches_core convert pat c =
         (try array_fold_left2 (sorec stk) (sorec stk sigma c1 c2) arg1 arg2
          with Invalid_argument _ -> raise PatternMatchingFailure)
 
-      | PBinder(BProd,na1,c1,d1), IsProd(na2,c2,d2) ->
+      | PProd (na1,c1,d1), IsProd(na2,c2,d2) ->
 	  sorec ((na2,c2)::stk) (sorec stk sigma c1 c2) d1 d2
 
-      | PBinder(BLambda,na1,c1,d1), IsLambda(na2,c2,d2) ->
+      | PLambda (na1,c1,d1), IsLambda(na2,c2,d2) ->
 	  sorec ((na2,c2)::stk) (sorec stk sigma c1 c2) d1 d2
 
-      | PBinder(BLetIn,na1,c1,d1), IsLetIn(na2,c2,t2,d2) ->
+      | PLetIn (na1,c1,d1), IsLetIn(na2,c2,t2,d2) ->
 	  sorec ((na2,t2)::stk) (sorec stk sigma c1 c2) d1 d2
 
       | PRef (ConstRef _ as ref), _ when convert <> None ->
@@ -299,20 +304,13 @@ let rec pattern_of_constr t =
     | IsSort (Prop c) -> PSort (RProp c)
     | IsSort (Type _) -> PSort RType
     | IsCast (c,_)      -> pattern_of_constr c
-    | IsLetIn (na,c,_,b)   ->
-	PBinder (BLetIn,na,pattern_of_constr c,pattern_of_constr b)
-    | IsProd (na,c,b)   ->
-	PBinder (BProd,na,pattern_of_constr c,pattern_of_constr b)
-    | IsLambda (na,c,b) ->
-	PBinder (BLambda,na,pattern_of_constr c,pattern_of_constr b)
-    | IsApp (f,args)   ->
-	PApp (pattern_of_constr f, Array.map pattern_of_constr args)
-    | IsConst (sp,ctxt)         ->
-	pattern_of_ref (ConstRef sp) ctxt
-    | IsMutInd (sp,ctxt)        ->
-	pattern_of_ref (IndRef sp) ctxt
-    | IsMutConstruct (sp,ctxt) ->
-	pattern_of_ref (ConstructRef sp) ctxt
+    | IsLetIn (na,c,_,b) -> PLetIn (na,pattern_of_constr c,pattern_of_constr b)
+    | IsProd (na,c,b)   -> PProd (na,pattern_of_constr c,pattern_of_constr b)
+    | IsLambda (na,c,b) -> PLambda (na,pattern_of_constr c,pattern_of_constr b)
+    | IsApp (f,a) -> PApp (pattern_of_constr f,Array.map pattern_of_constr a)
+    | IsConst (sp,ctxt)         -> pattern_of_ref (ConstRef sp) ctxt
+    | IsMutInd (sp,ctxt)        -> pattern_of_ref (IndRef sp) ctxt
+    | IsMutConstruct (sp,ctxt) -> pattern_of_ref (ConstructRef sp) ctxt
     | IsEvar (n,ctxt) ->
 	if ctxt = [||] then PEvar n
 	else PApp (PEvar n, Array.map pattern_of_constr ctxt)
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 115e86d61..0bce54e74 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -15,7 +15,9 @@ type constr_pattern =
   | PRel of int
   | PApp of constr_pattern * constr_pattern array
   | PSoApp of int * constr_pattern list
-  | PBinder of Rawterm.binder_kind * name * constr_pattern * constr_pattern
+  | PLambda of name * constr_pattern * constr_pattern
+  | PProd of name * constr_pattern * constr_pattern
+  | PLetIn of name * constr_pattern * constr_pattern
   | PSort of Rawterm.rawsort
   | PMeta of int option
   | PCase of constr_pattern option * constr_pattern * constr_pattern array
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 6ef3ad8e5..ba3e56aea 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -62,23 +62,27 @@ let transform_rec loc env sigma (p,c,lf) (indt,pt) =
       it_mkLambda_or_LetIn_name env
 	(lambda_create env
 	   (applist (mI,List.append (List.map (lift (nar+1)) params)
-                       (rel_list 0 nar)),
+                       (extended_rel_list 0 lnames)),
             mkMutCase (ci, lift (nar+2) p, mkRel 1, branches)))
         (lift_rel_context 1 lnames) 
     in
     if noccurn 1 deffix then 
       whd_beta (applist (pop deffix,realargs@[c]))
     else
+      let ind = applist (mI,(List.append 
+			     (List.map (lift nar) params)
+			     (extended_rel_list 0 lnames))) in
       let typPfix = 
 	it_mkProd_or_LetIn_name env
-	  (prod_create env
-	     (applist (mI,(List.append 
-			     (List.map (lift nar) params)
-			     (rel_list 0 nar))),
-	      (if dep then 
-		 whd_beta (applist (lift (nar+1) p, rel_list 0 (nar+1)))
-	       else 
-		 whd_beta (applist (lift (nar+1) p, rel_list 1 nar)))))
+	  (prod_create env 
+	     (ind,
+	      (if dep then
+		 let ext_lnames = (Anonymous,None,ind)::lnames in
+		 let args = extended_rel_list 0 ext_lnames in
+		 whd_beta (applist (lift (nar+1) p, args))
+	       else
+		 let args = extended_rel_list 1 lnames in
+		 whd_beta (applist (lift (nar+1) p, args)))))
           lnames 
       in
       let fix = mkFix (([|nar|],0),
@@ -318,7 +322,7 @@ let rec pretype tycon env isevars lvar lmeta = function
       *)
       inh_conv_coerce_to_tycon loc env isevars resj tycon
 
-  | RBinder(loc,BLambda,name,c1,c2)      ->
+  | RLambda(loc,name,c1,c2)      ->
       let (dom,rng) = split_tycon loc env isevars tycon in
       let dom_valcon = valcon_of_tycon dom in
       let j = pretype_type dom_valcon env isevars lvar lmeta c1 in
@@ -327,7 +331,7 @@ let rec pretype tycon env isevars lvar lmeta = function
       in 
       fst (abs_rel env !isevars name j.utj_val j')
 
-  | RBinder(loc,BProd,name,c1,c2)        ->
+  | RProd(loc,name,c1,c2)        ->
       let j = pretype_type empty_valcon env isevars lvar lmeta c1 in
       let var = (name,j.utj_val) in
       let env' = push_rel_assum var env in
@@ -337,7 +341,7 @@ let rec pretype tycon env isevars lvar lmeta = function
 	with TypeError _ as e -> Stdpp.raise_with_loc loc e in
       inh_conv_coerce_to_tycon loc env isevars resj tycon
 	
-  | RBinder(loc,BLetIn,name,c1,c2)      ->
+  | RLetIn(loc,name,c1,c2)      ->
       let j = pretype empty_tycon env isevars lvar lmeta c1 in
       let var = (name,j.uj_val,j.uj_type) in
       let j' = pretype tycon (push_rel_def var env) isevars lvar lmeta c2 in
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 99e32c76d..e410bd77f 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -37,7 +37,9 @@ type rawconstr =
   | REvar of loc * existential_key
   | RMeta of loc * int
   | RApp of loc * rawconstr * rawconstr list
-  | RBinder of loc * binder_kind * name * rawconstr * rawconstr
+  | RLambda of loc * name * rawconstr * rawconstr
+  | RProd of loc * name * rawconstr * rawconstr
+  | RLetIn of loc * name * rawconstr * rawconstr
   | RCases of loc * Term.case_style * rawconstr option * rawconstr list * 
       (identifier list * cases_pattern list * rawconstr) list
   | ROldCase of loc * bool * rawconstr option * rawconstr * 
@@ -68,7 +70,9 @@ let loc_of_rawconstr = function
   | REvar (loc,_) -> loc
   | RMeta (loc,_) -> loc
   | RApp (loc,_,_) -> loc
-  | RBinder (loc,_,_,_,_) -> loc
+  | RLambda (loc,_,_,_) -> loc
+  | RProd (loc,_,_,_) -> loc
+  | RLetIn (loc,_,_,_) -> loc
   | RCases (loc,_,_,_,_) -> loc
   | ROldCase (loc,_,_,_,_) -> loc
   | RRec (loc,_,_,_,_) -> loc
@@ -83,7 +87,9 @@ let set_loc_of_rawconstr loc = function
   | REvar (_,a)      -> REvar (loc,a)
   | RMeta (_,a)     -> RMeta (loc,a) 
   | RApp (_,a,b)    -> RApp (loc,a,b)
-  | RBinder (_,a,b,c,d) -> RBinder (loc,a,b,c,d)
+  | RLambda (_,a,b,c) -> RLambda (loc,a,b,c)
+  | RProd (_,a,b,c)   -> RProd (loc,a,b,c)
+  | RLetIn (_,a,b,c)  -> RLetIn (loc,a,b,c)
   | RCases (_,a,b,c,d) -> RCases (loc,a,b,c,d) 
   | ROldCase (_,a,b,c,d) -> ROldCase (loc,a,b,c,d) 
   | RRec (_,a,b,c,d) -> RRec (loc,a,b,c,d) 
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 1bb4c13a9..67049b927 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -35,7 +35,9 @@ type rawconstr =
   | REvar of loc * existential_key
   | RMeta of loc * int
   | RApp of loc * rawconstr * rawconstr list
-  | RBinder of loc * binder_kind * name * rawconstr * rawconstr
+  | RLambda of loc * name * rawconstr * rawconstr
+  | RProd of loc * name * rawconstr * rawconstr
+  | RLetIn of loc * name * rawconstr * rawconstr
   | RCases of loc * Term.case_style * rawconstr option * rawconstr list * 
       (identifier list * cases_pattern list * rawconstr) list
   | ROldCase of loc * bool * rawconstr option * rawconstr *