- Prise en compte de la clause 'in I' pour coercer le type du terme à filtrer;

- Prise en compte coercions autour des sous-termes filtrés (si non dépendants)
- Renommage v7 -> v8 dans commentaires


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

1 files changed, 92 insertions, 55 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index d9f7324cf..3a4a904f1 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -388,64 +388,67 @@ type pattern_matching_problem =
  * A few functions to infer the inductive type from the patterns instead of *
  * checking that the patterns correspond to the ind. type of the            *
  * destructurated object. Allows type inference of examples like            *
- *  [n]Cases n of O => true | _ => false end                                *
+ *  match n with O => true | _ => false end                                 *
+ *  match x in I with C => true | _ => false end                            *
  *--------------------------------------------------------------------------*)
 
 (* Computing the inductive type from the matrix of patterns *)
 
+(* We use the "in I" clause to coerce the terms to match and otherwise
+   use the constructor to know in which type is the matching problem
+
+   Note that insertion of coercions inside nested patterns is done
+   each time the matrix is expanded *)
+
 let rec find_row_ind = function
     [] -> None
   | PatVar _ :: l -> find_row_ind l
   | PatCstr(loc,c,_,_) :: _ -> Some (loc,c)
 
-exception NotCoercible
-
-let inh_coerce_to_ind isevars env tmloc ty tyi =
-  let (mib,mip) = Inductive.lookup_mind_specif env tyi in
+let inductive_template isevars env tmloc ind =
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
   let (ntys,_) = splay_prod env (Evd.evars_of !isevars) mip.mind_nf_arity in
   let hole_source = match tmloc with 
-    | Some loc -> fun i -> (loc, Evd.TomatchTypeParameter (tyi,i))
+    | Some loc -> fun i -> (loc, Evd.TomatchTypeParameter (ind,i))
     | None -> fun _ -> (dummy_loc, Evd.InternalHole) in
    let (evarl,_) =
     List.fold_right
       (fun (na,ty) (evl,n) ->
 	(e_new_evar isevars env ~src:(hole_source n) (substl evl ty))::evl,n+1)
       ntys ([],1) in
-  let expected_typ = applist (mkInd tyi,List.rev evarl) in
+   applist (mkInd ind,List.rev evarl)
+
+let inh_coerce_to_ind isevars env ty tyi =
+  let expected_typ = inductive_template isevars env None tyi in
      (* devrait être indifférent d'exiger leq ou pas puisque pour 
         un inductif cela doit être égal *)
-  if e_cumul env isevars expected_typ ty then ty
-  else raise NotCoercible
-
-(* We do the unification for all the rows that contain
- * constructor patterns. This is what we do at the higher level of patterns.
- * For nested patterns, we do this unif when we ``expand'' the matrix, and we
- * use the function above.
- *)
-
-let unify_tomatch_with_patterns isevars env tmloc typ = function
-  | Some (cloc,(cstr,_ as c)) ->
-      (let tyi = inductive_of_constructor c in
-       try 
-	 let _indtyp = inh_coerce_to_ind isevars env tmloc typ tyi in
-	 IsInd (typ,find_rectype env (Evd.evars_of !isevars) typ)
-       with NotCoercible ->
-	 (* 2 cases : Not the right inductive or not an inductive at all *)
-	 try
-	   IsInd (typ,find_rectype env (Evd.evars_of !isevars) typ)
-             (* will try to coerce later in check_and_adjust_constructor.. *)
-	 with Not_found ->
-	   NotInd (None,typ))
-	     (* error will be detected in check_all_variables *)
-  | None -> 
-      try IsInd (typ,find_rectype env (Evd.evars_of !isevars) typ)
-      with Not_found -> NotInd (None,typ)
-
-let coerce_row typing_fun isevars env cstropt tomatch =
-  let j = typing_fun empty_tycon env tomatch in
-  let typ = body_of_type j.uj_type in
-  let loc = loc_of_rawconstr tomatch in
-  let t = unify_tomatch_with_patterns isevars env (Some loc) typ cstropt in
+  let _ = e_cumul env isevars expected_typ ty in ()
+
+let unify_tomatch_with_patterns isevars env typ tm =
+  match find_row_ind tm with
+    | None -> NotInd (None,typ)
+    | Some (_,(ind,_)) ->
+	inh_coerce_to_ind isevars env typ ind;
+	try IsInd (typ,find_rectype env (Evd.evars_of !isevars) typ)
+	with Not_found -> NotInd (None,typ)
+
+let find_tomatch_tycon isevars env loc = function
+  (* Try first if some 'in I ...' is present and can be used as a constraint *)
+  | Some (_,ind,_),_ 
+  (* Otherwise try to get constraints from (the 1st) constructor in clauses *)
+  | None, Some (_,(ind,_)) ->
+      Some (inductive_template isevars env loc ind)
+  | None, None -> 
+      empty_tycon
+
+let coerce_row typing_fun isevars env cstropt (tomatch,(_,indopt)) =
+  let loc = Some (loc_of_rawconstr tomatch) in
+  let tycon = find_tomatch_tycon isevars env loc (indopt,cstropt) in
+  let j = typing_fun tycon env tomatch in
+  let typ = nf_evar (Evd.evars_of !isevars) j.uj_type in
+  let t = 
+    try IsInd (typ,find_rectype env (Evd.evars_of !isevars) typ)
+    with Not_found -> NotInd (None,typ) in
   (j.uj_val,t)
 
 let coerce_to_indtype typing_fun isevars env matx tomatchl =
@@ -458,11 +461,47 @@ let coerce_to_indtype typing_fun isevars env matx tomatchl =
 (************************************************************************)
 (* Utils *)
 
+let evd_comb2 f isevars x y =
+  let (evd',y) = f !isevars x y in
+  isevars := evd';
+  y
+
+let adjust_tomatch_to_pattern pb ((current,typ),deps) =
+  (* Ideally, we could find a common inductive type to which both the
+     term to match and the patterns coerce *)
+  (* In practice, we coerce the term to match if it is not already an
+     inductive type and it is not dependent; moreover, we use only 
+     the first pattern type and forget about the others *)
+  let typ = match typ with IsInd (t,_) -> t | NotInd (_,t) -> t in
+  let typ =
+    try IsInd (typ,find_rectype pb.env (Evd.evars_of !(pb.isevars)) typ)
+    with Not_found -> NotInd (None,typ) in
+  let tomatch = ((current,typ),deps) in
+  match typ with
+  | NotInd (None,typ) ->
+      let tm1 = List.map (fun eqn -> List.hd eqn.patterns) pb.mat in
+      (match find_row_ind tm1 with
+	| None -> tomatch
+	| Some (_,(ind,_)) ->
+	    let indt = inductive_template pb.isevars pb.env None ind in
+	    let current =
+	      if deps = [] & isEvar typ then
+	      (* Don't insert coercions if dependent; only solve evars *)
+		let _ = e_cumul pb.env pb.isevars indt typ in
+		current
+	      else
+		(evd_comb2 (Coercion.inh_conv_coerce_to dummy_loc pb.env)
+		  pb.isevars (make_judge current typ) indt).uj_val in
+	    let sigma = Evd.evars_of !(pb.isevars) in
+	    let typ = IsInd (indt,find_rectype pb.env sigma indt) in
+	    ((current,typ),deps))
+  | _ -> tomatch
+
    (* extract some ind from [t], possibly coercing from constructors in [tm] *)
 let to_mutind env isevars tm c t =
   match c with
     | Some body -> NotInd (c,t)
-    | None -> unify_tomatch_with_patterns isevars env None t (find_row_ind tm)
+    | None -> unify_tomatch_with_patterns isevars env t tm
 
 let type_of_tomatch = function
   | IsInd (t,_) -> t
@@ -715,11 +754,11 @@ let lift_tomatch_stack n = liftn_tomatch_stack n 1
 (* Some heuristics to get names for variables pushed in pb environment *)
 (* Typical requirement:
 
-   [Cases y of (S (S x)) => x | x => x end] should be compiled into
-   [Cases y of O => y | (S n) => Cases n of O => y | (S x) => x end end]
+   [match y with (S (S x)) => x | x => x end] should be compiled into
+   [match y with O => y | (S n) => match n with O => y | (S x) => x end end]
 
-   and [Cases y of (S (S n)) => n | n => n end] into 
-   [Cases y of O => y | (S n0) => Cases n0 of O => y | (S n) => n end end]
+   and [match y with (S (S n)) => n | n => n end] into 
+   [match y with O => y | (S n0) => match n0 with O => y | (S n) => n end end]
 
   i.e. user names should be preserved and created names should not
   interfere with user names *)
@@ -868,10 +907,10 @@ the following n+1 equations:
 
 Some hints:
 
-- Clearly, if xij occurs in Ti, then, a "Cases z of (Ci xi1..xipi) => ..."
+- Clearly, if xij occurs in Ti, then, a "match z with (Ci xi1..xipi) => ..."
   should be inserted somewhere in Ti.
 
-- If T is undefined, an easy solution is to insert a "Cases z of (Ci
+- If T is undefined, an easy solution is to insert a "match z with (Ci
   xi1..xipi) => ..." in front of each Ti
 
 - Otherwise, T1..Tn and T must be step by step unified, if some of them
@@ -922,7 +961,7 @@ let infer_predicate loc env isevars typs cstrs indf =
     error "Inference of annotation for empty inductive types not implemented"
   else
     (* Empiric normalization: p may depend in a irrelevant way on args of the*)
-    (* cstr as in [c:{_:Alpha & Beta}] Cases c of (existS a b)=>(a,b) end *)
+    (* cstr as in [c:{_:Alpha & Beta}] match c with (existS a b)=>(a,b) end *)
     let typs =
       Array.map (local_strong (whd_betaevar empty_env (Evd.evars_of !isevars))) typs
     in
@@ -1107,7 +1146,7 @@ let expand_arg n alreadydep (na,t) deps (k,pred) =
 (*****************************************************************************)
 (* pred = [X:=realargs;x:=c]P types the following problem:                   *)
 (*                                                                           *)
-(*  Gamma |- Cases Pushed(c:I(realargs)) rest of...end: pred                 *)
+(*  Gamma |- match Pushed(c:I(realargs)) rest with...end: pred               *)
 (*                                                                           *)
 (* where the branch with constructor Ci:(x1:T1)...(xn:Tn)->I(realargsi)      *)
 (* is considered. Assume each Ti is some Ii(argsi).                          *)
@@ -1115,7 +1154,7 @@ let expand_arg n alreadydep (na,t) deps (k,pred) =
 (*                                                                           *)
 (* pred' = [X1:=rargs1,x1:=x1']...[Xn:=rargsn,xn:=xn'](P[X:=realargsi;x:=e]) *)
 (*                                                                           *)
-(* s.t Gamma,x1'..xn' |- Cases Pushed(x1')..Pushed(xn') rest of...end: pred' *)
+(* s.t Gamma,x1'..xn' |- match Pushed(x1')..Pushed(xn') rest with..end :pred'*)
 (*                                                                           *)
 (*****************************************************************************)
 let specialize_predicate tomatchs deps cs = function
@@ -1323,10 +1362,8 @@ let rec compile pb =
     | (Abstract d)::rest -> compile_generalization pb d rest
     | [] -> build_leaf pb
 
-and match_current pb ((current,typ as ct),deps) =
-  let tm1 = List.map (fun eqn -> List.hd eqn.patterns) pb.mat in
-  let (_,c,t) = mkDeclTomatch Anonymous typ in
-  let typ = to_mutind pb.env pb.isevars tm1 c t in
+and match_current pb tomatch =
+  let ((current,typ as ct),deps) = adjust_tomatch_to_pattern pb tomatch in
   match typ with
     | NotInd (_,typ) ->
 	check_all_variables typ pb.mat;
@@ -1718,11 +1755,11 @@ let compile_cases loc (typing_fun,isevars) tycon env (predopt, tomatchl, eqns)=
 
   (* We build the vector of terms to match consistently with the *)
   (* constructors found in patterns *)
-  let rawtms, tmsign = List.split tomatchl in
-  let tomatchs = coerce_to_indtype typing_fun isevars env matx rawtms in
+  let tomatchs = coerce_to_indtype typing_fun isevars env matx tomatchl in
 
   (* We build the elimination predicate if any and check its consistency *)
   (* with the type of arguments to match *)
+  let tmsign = List.map snd tomatchl in
   let pred = prepare_predicate loc typing_fun isevars env tomatchs tmsign tycon predopt in
 
   (* We deal with initial aliases *)