Bugs prise en compte du prédicat dans le Cases; le prédicat du Cases devient systématiquement dépendent; blindage de certaines erreurs

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

3 files changed, 163 insertions, 107 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 4e4ee9fbe..fc7442aef 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -190,6 +190,7 @@ type tomatch_stack = tomatch_status list
 type predicate_signature =
   | PrLetIn of (constr list * constr option) * predicate_signature
   | PrProd of (bool * name * tomatch_type) * predicate_signature
+  | PrNotInd of constr option * predicate_signature
   | PrCcl of constr
 
 (* A pattern-matching problem has the following form:
@@ -581,7 +582,8 @@ let abstract_conclusion typ cs =
   let (sign,p) = decompose_prod_n n typ in
   lam_it p sign
 
-let infer_predicate env isevars typs cstrs (IndFamily (mis,_) as indf) =
+let infer_predicate env isevars typs cstrs (IndType (indf,_) as indt) =
+  let IndFamily (mis,_) = indf in
   (* Il faudra substituer les isevars a un certain moment *)
   if Array.length cstrs = 0 then (* "TODO4-3" *)
     error "Inference of annotation for empty inductive types not implemented"
@@ -592,8 +594,10 @@ let infer_predicate env isevars typs cstrs (IndFamily (mis,_) as indf) =
     let (sign,_) = get_arity indf in
     if array_for_all (fun (_,_,typ) -> the_conv_x env isevars typn typ) eqns
     then
+      (* Non dependent case -> turn it into a (dummy) dependent one *)
+      let sign = (Anonymous,None,mkAppliedInd indt)::sign in
       let pred = it_mkLambda_or_LetIn (lift (List.length sign) typn) sign in
-      (false,pred) (* true = dependent -- par défaut *)
+      (true,pred) (* true = dependent -- par défaut *)
     else
       let s = get_sort_of env !isevars typs.(0) in
       let predpred = it_mkLambda_or_LetIn (mkSort s) sign in
@@ -602,22 +606,25 @@ let infer_predicate env isevars typs cstrs (IndFamily (mis,_) as indf) =
       let predbody = mkMutCase (caseinfo, predpred, mkRel 1, brs) in
       let pred = it_mkLambda_or_LetIn (lift (List.length sign) typn) sign in
       (* "TODO4-2" *)
-      error "General inference of annotation not yet implemented;\
+      error "General inference of annotation not yet implemented; \
              you need to give the predicate";
       (true,pred)
 
 (* Propagation of user-provided predicate through compilation steps *)
 
-let lift_predicate n pred =
+let liftn_predicate n k pred =
   let rec liftrec k = function
   | PrCcl ccl -> PrCcl (liftn n k ccl)
+  | PrNotInd (copt,ccl) -> PrNotInd (option_app (liftn n k) copt,liftrec k ccl)
   | PrProd ((dep,na,t),pred) ->
 	PrProd ((dep,na,liftn_tomatch_type n k t), liftrec (k+1) pred)
-    | PrLetIn ((args,copt),pred) ->
-	let args' = List.map (liftn n k) args in
-	let copt' = option_app (liftn n k) copt in
-	PrLetIn ((args',copt'), liftrec (k+1) pred) in
-  liftrec 1 pred
+  | PrLetIn ((args,copt),pred) ->
+      let args' = List.map (liftn n k) args in
+      let copt' = option_app (liftn n k) copt in
+      PrLetIn ((args',copt'), liftrec (k+1) pred) in
+  liftrec k pred
+
+let lift_predicate n = liftn_predicate n 1
 
 let subst_predicate (args,copt) pred =
   let sigma = match copt with
@@ -625,6 +632,8 @@ let subst_predicate (args,copt) pred =
     | Some c -> c::(List.rev args) in
   let rec substrec k = function
     | PrCcl ccl -> PrCcl (substnl sigma k ccl)
+    | PrNotInd (copt,pred) ->
+	PrNotInd (option_app (substnl sigma k) copt, substrec (k+1) pred)
     | PrProd ((dep,na,t),pred) ->
 	PrProd ((dep,na,substnl_tomatch sigma k t), substrec (k+1) pred)
     | PrLetIn ((args,copt),pred) ->
@@ -636,30 +645,21 @@ let subst_predicate (args,copt) pred =
 let specialize_predicate_var = function
   | PrProd _ | PrCcl _ ->
      anomaly "specialize_predicate_var: a pattern-variable must be pushed"
+  | PrNotInd (copt,pred) -> subst_predicate ([],copt) pred
   | PrLetIn (tm,pred) -> subst_predicate tm pred
 
-let rec weaken_predicate n pred =
-  if n=0 then pred else match pred with
-    | PrLetIn _ | PrCcl _ ->
-		    anomaly "weaken_predicate: only product can be weakened"
-    | PrProd ((dep,_,IsInd (_,IndType(indf,realargs))),pred) ->
-	(* To make it more uniform, we apply realargs but they not occur! *)
-	let copt = if dep then Some (mkRel n) else None in
-	PrLetIn ((realargs,copt), weaken_predicate (n-1)
-		   (lift_predicate (List.length realargs) pred))
-    | PrProd ((dep,_,NotInd t),pred) ->
-	let copt = if dep then Some (mkRel n) else None in
-	PrLetIn (([],copt), weaken_predicate (n-1) pred)
-
 let rec extract_predicate = function
   | PrProd ((_,na,t),pred) ->
       mkProd (na, type_of_tomatch_type t, extract_predicate pred)
+  | PrNotInd (Some c,pred) -> substl [c] (extract_predicate pred)
+  | PrNotInd (None,pred) -> extract_predicate pred
   | PrLetIn ((args,Some c),pred) -> substl (c::(List.rev args)) (extract_predicate pred)
   | PrLetIn ((args,None),pred) -> substl (List.rev args) (extract_predicate pred)
   | PrCcl ccl -> ccl
 
 let abstract_predicate env sigma indf = function
-  | PrProd _ | PrCcl _ -> anomaly "abstract_predicate: must be some LetIn"
+  | (PrProd _ | PrCcl _ | PrNotInd _) ->
+      anomaly "abstract_predicate: must be some LetIn"
   | PrLetIn ((_,copt),pred) ->
       let sign,_ = get_arity indf in
       let dep = copt <> None in
@@ -669,27 +669,73 @@ let abstract_predicate env sigma indf = function
 	else sign in
       (dep, it_mkLambda_or_LetIn_name env (extract_predicate pred) sign')
 
+(*****************************************************************************)
+(* pred = (x1:I1(args1))...(xn:In(argsn))P types the following problem:      *)
+(*                                                                           *)
+(*  Gamma |- Cases ToPush (x1:T1) ... ToPush (xn:Tn) rest of ... end : pred  *)
+(*                                                                           *)
+(* We replace it by pred' = [X1:=rargs1,x1:=x1]...[Xn:=rargsn,xn:=xn]P s.t.  *)
+(*                                                                           *)
+(*  Gamma,x1:T1...xn:Tn |- Cases Pushed(x1)...Pushd(xn) rest of...end: pred' *)
+(*                                                                           *)
+(* The realargs are not necessary; it would be simpler not to take then into *)
+(* account; especially, no lift would be necessary (but                      *)
+(* [specialize_predicate_match] assumes realargs are given, then ...)        *)
+(*****************************************************************************)
+let weaken_predicate q pred =
+  let rec weakrec n k pred =
+    if n=0 then lift_predicate k pred else match pred with
+      | (PrLetIn _ | PrCcl _ | PrNotInd _) ->
+	  anomaly "weaken_predicate: only product can be weakened"
+      | PrProd ((dep,_,IsInd (_,IndType(indf,realargs))),pred) ->
+	  (* To make it more uniform, we apply realargs but they not occur! *)
+	  let copt, p = if dep then Some (mkRel (q+k)), 1 else None, 0 in
+  let realargs = List.map (lift k) realargs in
+	  (* We replace 1 product by |realargs| arguments + possibly copt *)
+	  (* Then we need to add this to the global lift *)
+	  let lift = k+(List.length realargs)+p in
+	  PrLetIn ((realargs, copt), weakrec (n-1) lift pred)
+    | PrProd ((dep,_,NotInd t),pred) ->
+	(* Does copt occur in pred ? Does it need to be remembered ? *)
+	let copt, p = if dep then Some (mkRel (q+k)), 1 else None, 0 in
+	PrNotInd (copt, weakrec (n-1) (k+p) pred)
+  in weakrec q 0 pred
+
+(*****************************************************************************)
+(* pred = [X:=realargs;x:=e]P types the following problem:                   *)
+(*                                                                           *)
+(*  Gamma |- Cases Pushed(e:I) rest of...end: pred                           *)
+(*                                                                           *)
+(* where the case of constructor C:(x1:T1)...(xn:Tn)->I is considered.       *)
+(* We replace pred by pred' = (x1:T1)...(xn:Tn)P[X:=realargs;x:=e] s.t.      *)
+(*                                                                           *)
+(*  Gamma |- Cases ToPush(x1)...ToPush(xn) rest of...end: pred'              *)
+(*****************************************************************************)
 let specialize_predicate_match tomatchs cs = function
-  | PrProd _ | PrCcl _ ->
-     anomaly "specialize_predicate_match: a matched pattern must be pushed"
+  | (PrProd _ | PrCcl _ | PrNotInd _) ->
+      anomaly "specialize_predicate_match: a matched pattern must be pushed"
   | PrLetIn ((args,copt),pred) ->
+      let k = List.length args + (if copt = None then 0 else 1) in
+      let pred' = liftn_predicate cs.cs_nargs (k+1) pred in
       let argsi = Array.to_list cs.cs_concl_realargs in
       let copti = option_app (fun _ -> build_dependent_constructor cs) copt in
-      let pred' = subst_predicate (argsi, copti) pred in
-      let pred'' = (*lift_predicate cs.cs_nargs *) pred' in
+      let pred'' = subst_predicate (argsi, copti) pred' in
       let dep = (copt <> None) in
       List.fold_right
 	(* Ne perd-on pas des cas en ne posant pas true à la place de dep ? *)
 	(fun ((na,t),_) p -> PrProd ((dep,na,t),p)) tomatchs pred''
 
-let find_predicate env isevars p typs cstrs current (IndType (indf,realargs)) =
+let find_predicate env isevars p typs cstrs current 
+  (IndType (indf,realargs) as indt) =
   let (dep,pred) =
     match p with
       | Some p -> abstract_predicate env !isevars indf p
-      | None -> infer_predicate env isevars typs cstrs indf in
-  let typ = applist (pred, realargs) in
-  if dep then (pred, applist (typ, [current]), Type Univ.dummy_univ)
-  else (pred, typ, Type Univ.dummy_univ)
+      | None -> infer_predicate env isevars typs cstrs indt in
+  let typ = whd_beta (applist (pred, realargs)) in
+  if dep then
+    (pred, whd_beta (applist (typ, [current])), Type Univ.dummy_univ)
+  else
+    (pred, typ, Type Univ.dummy_univ)
 
 (************************************************************************)
 (* Sorting equation by constructor *)
@@ -964,37 +1010,51 @@ let build_expected_arity env isevars isdep tomatchl =
   let cook n = function
     | _,IsInd (_,IndType(indf,_)) ->
 	let indf' = lift_inductive_family n indf in
-	(build_dependent_inductive indf', fst (get_arity indf'))
-    | _,NotInd _ -> anomaly "Should have been catched in case_dependent"
+	Some (build_dependent_inductive indf', fst (get_arity indf'))
+    | _,NotInd _ -> None
   in
   let rec buildrec n = function
     | [] -> dummy_sort
     | tm::ltm ->
-	let (ty1,aritysign) = cook n tm in
-	let rec follow n = function
-	  | d::sign -> mkProd_or_LetIn d (follow (n+1) sign)
-	  | [] ->
-	      if isdep then mkProd (Anonymous, ty1, buildrec (n+1) ltm)
-	      else buildrec n ltm
-	in follow n (List.rev aritysign)
+	match cook n tm with
+	  | None -> buildrec n ltm
+	  | Some (ty1,aritysign) ->
+	      let rec follow n = function
+		| d::sign -> mkProd_or_LetIn d (follow (n+1) sign)
+		| [] ->
+		    if isdep then mkProd (Anonymous, ty1, buildrec (n+1) ltm)
+		    else buildrec n ltm
+	      in follow n (List.rev aritysign)
   in buildrec 0 tomatchl
 
-let build_initial_predicate isdep pred tomatchl =
+let build_initial_predicate env sigma isdep pred tomatchl =
   let cook n = function
-    | _,IsInd (_,IndType(ind_data,realargs)) ->
-	let args = List.map (lift n) realargs in
-	if isdep then
-	  let ty = lift n (build_dependent_inductive ind_data) in
-	  (List.length realargs + 1, (args,Some ty))
-	else
-	  (List.length realargs, (args,None))
-    | _,NotInd _ -> anomaly "Should have been catched in case_dependent"
-  in
+    | c,IsInd (_,IndType(ind_data,realargs)) ->
+	Some (List.map (lift n) realargs), Some (lift n c)
+    | c,NotInd _ -> None, Some (lift n c) in
+  let decomp_lam_force p =
+    match kind_of_term (whd_betadeltaiota env sigma p) with
+      | IsLambda (_,_,c) -> c
+      | _ -> (* eta-expansion *) applist (lift 1 pred, [mkRel 1]) in
+  let rec strip_and_adjust nargs pred =
+    if nargs = 0 then
+      if isdep then
+	(* We remove an existing lambda (up to eta-expansion) *)
+	decomp_lam_force pred
+      else 
+	(* Turn pred into a dependent predicate --> [_:?](lift 1 pred) and *)
+	(* immediately remove the (virtually) inserted lambda *)
+	lift 1 pred
+    else strip_and_adjust (nargs-1) (decomp_lam_force pred) in
   let rec buildrec n pred = function
     | [] -> PrCcl pred
     | tm::ltm ->
-	let (nargs,args) = cook n tm in
-	PrLetIn (args,buildrec (n+nargs) (snd(decompose_lam_n nargs pred)) ltm)
+	match cook n tm with
+	  | None, cur -> PrNotInd (cur, buildrec (n+1) pred ltm)
+	  | Some realargs, cur ->
+	      let nrealargs = List.length realargs in
+	      let predccl = strip_and_adjust nrealargs pred in
+	      PrLetIn ((realargs,cur),buildrec (n+nrealargs+1) predccl ltm)
   in buildrec 0 pred tomatchl
 
 let rec eta_expand0 env sigma n c t =
@@ -1021,6 +1081,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
@@ -1039,31 +1100,36 @@ let case_dependent env sigma loc predj tomatchs =
     (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 ->
       let loc = loc_of_rawconstr pred in
-      let predj =
+      let dep, predj =
 	let isevars_copy = ref !isevars in
         (* We first assume the predicate is non dependent *)
+	let ndep_arity = build_expected_arity env isevars false tomatchs in
         try
-	  let ndep_arity = build_expected_arity env isevars false tomatchs in
-	  typing_fun (mk_tycon ndep_arity) env pred
+	  false, typing_fun (mk_tycon ndep_arity) env pred
 	with TypeError _ | Stdpp.Exc_located (_,TypeError _) ->
         isevars := !isevars_copy;
         (* We then assume the predicate is dependent *)
+	let dep_arity = build_expected_arity env isevars true tomatchs in
 	try
-	  let dep_arity = build_expected_arity env isevars true tomatchs in
-	  typing_fun (mk_tycon dep_arity) env pred
+	  true, typing_fun (mk_tycon dep_arity) env pred
 	with TypeError _ | Stdpp.Exc_located (_,TypeError _) ->
         isevars := !isevars_copy;
         (* Otherwise we attempt to type it without constraints, possibly *)
         (* failing with an error message; it may also be well-typed *)
 	(* but fails to satisfy arity constraints in case_dependent *)
-        typing_fun empty_tycon env pred in
+        let predj = typing_fun empty_tycon env pred in
+	error_wrong_predicate_arity_loc
+	  loc env predj.uj_val ndep_arity dep_arity
+      in
+(*
       let etapred,cdep = case_dependent env !isevars loc predj tomatchs in
-      Some (build_initial_predicate cdep etapred tomatchs)
+*)
+      Some (build_initial_predicate env !isevars dep predj.uj_val tomatchs)
 
 
 (**************************************************************************)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 26122a540..978532c07 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -235,13 +235,10 @@ let computable p k =
        sinon on perd la réciprocité de la synthèse (qui, lui,
        engendrera un prédicat non dépendant) *)
 
-  let rec striprec (n,c) = match n, kind_of_term c with
-    | (0,IsLambda (_,_,d)) -> false
-    | (0,_)                -> noccur_between 1 k c
-    | (n,IsLambda (_,_,d)) -> striprec (n-1,d)
-    |  _                           -> false
-  in 
-  striprec (k,p)
+  let _,ccl = decompose_lam p in 
+  noccur_between 1 (k+1) ccl
+
+
 
 let lookup_name_as_renamed ctxt t s =
   let rec lookup avoid env_names n c = match kind_of_term c with
@@ -300,35 +297,27 @@ let rec detype avoid env t =
     | IsMutCase (annot,p,c,bl) ->
 	let synth_type = synthetize_type () in
 	let tomatch = detype avoid env c in
-	begin 
-	  match annot with
-(*	  | None -> (* Pas d'annotation --> affichage avec vieux Case *)
-	      warning "Printing in old Case syntax";
-	      ROldCase (dummy_loc,false,Some (detype avoid env p),
-			tomatch,Array.map (detype avoid env) bl)
-	  | Some *) (consnargsl,(indsp,considl,k,style,tags)) ->
-	    let pred = 
-	      if synth_type & computable p k & considl <> [||] then
-		None
-	      else 
-		Some (detype avoid env p) 
-	    in
-	    let constructs = 
-	      Array.init (Array.length considl)
-		(fun i -> ((indsp,i+1),[] (* on triche *))) in
-	    let eqnv =
-	      array_map3 (detype_eqn avoid env) constructs consnargsl bl in
-	    let eqnl = Array.to_list eqnv in
-	    let tag =
-	      if PrintingLet.active (indsp,consnargsl) then 
-		PrintLet 
-	      else if PrintingIf.active (indsp,consnargsl) then 
-		PrintIf 
-	      else 
-		PrintCases
-	    in 
-	    RCases (dummy_loc,tag,pred,[tomatch],eqnl)
-	end
+	let (consnargsl,(indsp,considl,k,style,tags)) = annot in
+	let pred = 
+	  if synth_type & computable p k & considl <> [||] then
+	    None
+	  else 
+	    Some (detype avoid env p) in
+	let constructs = 
+	  Array.init (Array.length considl)
+	    (fun i -> ((indsp,i+1),[] (* on triche *))) in
+	let eqnv =
+	  array_map3 (detype_eqn avoid env) constructs consnargsl bl in
+	let eqnl = Array.to_list eqnv in
+	let tag =
+	  if PrintingLet.active (indsp,consnargsl) then 
+	    PrintLet 
+	  else if PrintingIf.active (indsp,consnargsl) then 
+	    PrintIf 
+	  else 
+	    PrintCases
+	in 
+	RCases (dummy_loc,tag,pred,[tomatch],eqnl)
 	
     | IsFix (nvn,(cl,lfn,vt)) -> detype_fix (RFix nvn) avoid env cl lfn vt
     | IsCoFix (n,(cl,lfn,vt))  -> detype_fix (RCoFix n) avoid env cl lfn vt
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b25af668c..bd7e61342 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -346,11 +346,7 @@ let rec pretype tycon env isevars lvar lmeta cstr =
 	  | Some p -> pretype empty_tycon env isevars lvar lmeta p
 	  | None -> 
 	      try match tycon with
-		  Some pred -> 
-		    let predj = Retyping.get_judgment_of env !isevars pred in
-		    let tj = inh_coerce_to_sort env isevars predj in (* Utile ?? *)
-		    let { utj_val = v; utj_type = s } = tj in
-		    { uj_val = v; uj_type = mkSort s }
+		  Some pred -> Retyping.get_judgment_of env !isevars pred
 		| None -> error "notype"
 	      with UserError _ -> (* get type information from type of branches *)
 		let expbr = Cases.branch_scheme env isevars isrec indf in
@@ -374,11 +370,16 @@ let rec pretype tycon env isevars lvar lmeta cstr =
 		    with UserError _ -> findtype (i+1) in
 		findtype 0 in
 
-	let evalct = find_rectype env !isevars cj.uj_type (*Pour normaliser evars*)
-	and evalPt = nf_ise1 !isevars pj.uj_type in
+	let evalPt = nf_ise1 !isevars pj.uj_type in
 
+	let dep = find_case_dep_nparams env !isevars (cj.uj_val,pj.uj_val) indf evalPt in
+
+	let (p,pt) =
+	  if dep then (pj.uj_val, evalPt) else
+	    (mkLambda (Anonymous, mkAppliedInd indt, lift 1 pj.uj_val),
+	     mkProd (Anonymous, mkAppliedInd indt, lift 1 evalPt)) in
 	let (bty,rsty) =
-	  Indrec.type_rec_branches isrec env !isevars evalct evalPt pj.uj_val cj.uj_val in
+	  Indrec.type_rec_branches isrec env !isevars indt pt p cj.uj_val in
 	if Array.length bty <> Array.length lf then
 	  wrong_number_of_cases_message loc env isevars 
 	    (cj.uj_val,nf_ise1 !isevars cj.uj_type)
@@ -394,11 +395,11 @@ let rec pretype tycon env isevars lvar lmeta cstr =
 	  let v =
 	    if isrec
 	    then 
-	      transform_rec loc env !isevars(pj.uj_val,cj.uj_val,lfv) (evalct,evalPt)
+	      transform_rec loc env !isevars(p,cj.uj_val,lfv) (indt,pt)
 	    else
 	      let mis,_ = dest_ind_family indf in
 	      let ci = make_default_case_info mis in
-	      mkMutCase (ci, pj.uj_val, cj.uj_val, Array.map (fun j-> j.uj_val) lfj)
+	      mkMutCase (ci, p, cj.uj_val, Array.map (fun j-> j.uj_val) lfj)
 	  in
 	  {uj_val = v;
 	   uj_type = rsty }