Extend the computation of dependencies in pattern-matching compilation

to the dependencies in the real arguments (a.k.a. indices) of the
terms to match.

This allows in particular to make the example from bug report #2404
work.

TODO: move the computation of dependencies in compile_branch at the time
of splitting a branch (where the computation is done now, it does not allow
to support dependent matching on the second argument of a constructor of
type  "forall b, (if b then Vector.t n else nat) -> Vector.t n -> foo").

TODO: take dependencies in Var's into account and take dependencies within
non-Rel arguments also into account (as in "match v (f t) with ... end"
where v is a Var and the type of (f t) depends on it).

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

1 files changed, 70 insertions, 38 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 46dabb266..3060d4bd9 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -301,13 +301,24 @@ let try_find_ind env sigma typ realnames =
       | None -> list_make (List.length realargs) Anonymous in
   IsInd (typ,ind,names)
 
-
 let inh_coerce_to_ind evdref env ty tyi =
   let expected_typ = inductive_template evdref env None tyi in
      (* devrait être indifférent d'exiger leq ou pas puisque pour
         un inductif cela doit être égal *)
   let _ = e_cumul env evdref expected_typ ty in ()
 
+let binding_vars_of_inductive = function
+  | NotInd _ -> []
+  | IsInd (_,IndType(_,realargs),_) -> List.filter isRel realargs
+
+let extract_inductive_data env sigma (_,b,t) =
+  if b<>None then (NotInd (None,t),[]) else
+  let tmtyp =
+    try try_find_ind env sigma t None
+    with Not_found -> NotInd (None,t) in
+  let tmtypvars = binding_vars_of_inductive tmtyp in
+  (tmtyp,tmtypvars)
+
 let unify_tomatch_with_patterns evdref env loc typ pats realnames =
   match find_row_ind pats with
     | None -> NotInd (None,typ)
@@ -538,16 +549,16 @@ let dependencies_in_rhs nargs current tms eqns =
    [n-2;1], [1] points to [dn] and [n-2] to [d3]
 *)
 
-let rec find_dependency_list tm = function
+let rec find_dependency_list tmblock = function
   | [] -> []
   | (used,tdeps,d)::rest ->
-      let deps = find_dependency_list tm rest in
-      if used && dependent_decl tm d
+      let deps = find_dependency_list tmblock rest in
+      if used && List.exists (fun x -> dependent_decl x d) tmblock
       then list_add_set (List.length rest + 1) (list_union deps tdeps)
       else deps
 
-let find_dependencies is_dep_or_cstr_in_rhs (tm,d) nextlist =
-  let deps = find_dependency_list tm nextlist in
+let find_dependencies is_dep_or_cstr_in_rhs (tm,(_,tmtypleaves),d) nextlist =
+  let deps = find_dependency_list (tm::tmtypleaves) nextlist in
   if is_dep_or_cstr_in_rhs || deps <> []
   then ((true ,deps,d)::nextlist)
   else ((false,[]  ,d)::nextlist)
@@ -699,7 +710,7 @@ let get_names env sign eqns =
       ([],allvars) (List.rev sign) names2 in
   names3,aliasname
 
-(************************************************************************)
+(*****************************************************************)
 (* Recovering names for variables pushed to the rhs' environment *)
 (* We just factorized a match over a matrix of equations         *)
 (* "C xi1 .. xin as xi" as a single match over "C y1 .. yn as y" *)
@@ -865,18 +876,25 @@ let rec extract_predicate ccl = function
   | [] ->
       ccl
 
-let abstract_predicate env sigma indf cur (names,na) tms ccl =
+let abstract_predicate env sigma indf cur realargs (names,na) tms ccl =
   let sign = make_arity_signature env true indf in
-  (* n is the number of real args + 1 *)
+  (* n is the number of real args + 1 (+ possible let-ins in sign) *)
   let n = List.length sign in
-  let tms = lift_tomatch_stack n tms in
-  let tms =
-    match kind_of_term cur with
-      | Rel i -> relocate_index_tomatch (i+n) 1 tms
-      | _ -> (* Initial case *) tms in
-  let sign = List.map2 (fun na (_,c,t) -> (na,c,t)) (na::names) sign in
+  (* Before abstracting we generalize over cur and on those realargs *)
+  (* that are rels, consistently with the specialization made in     *)
+  (* build_branch                                                    *)
+  let tms = List.fold_right2 (fun par arg tomatch ->
+    match kind_of_term par with
+    | Rel i -> relocate_index_tomatch (i+n) (destRel arg) tomatch
+    | _ -> tomatch) (realargs@[cur]) (extended_rel_list 0 sign)
+       (lift_tomatch_stack n tms) in
+  (* Pred is already dependent in the current term to match (if      *)
+  (* (na<>Anonymous) and its realargs; we just need to adjust it to  *)
+  (* full sign if dep in cur is not taken into account               *)
   let ccl = if na <> Anonymous then ccl else lift_predicate 1 ccl tms in
   let pred = extract_predicate ccl tms in
+  (* Build the predicate properly speaking *)
+  let sign = List.map2 set_declaration_name (na::names) sign in
   it_mkLambda_or_LetIn_name env pred sign
 
 (* [expand_arg] is used by [specialize_predicate]
@@ -965,7 +983,7 @@ let specialize_predicate newtomatchs (names,depna) arsign cs tms ccl =
   snd (List.fold_left (expand_arg tms) (1,ccl''') newtomatchs)
 
 let find_predicate loc env evdref p current (IndType (indf,realargs)) dep tms =
-  let pred = abstract_predicate env !evdref indf current dep tms p in
+  let pred = abstract_predicate env !evdref indf current realargs dep tms p in
   (pred, whd_betaiota !evdref
            (applist (pred, realargs@[current])))
 
@@ -1121,7 +1139,7 @@ let build_leaf pb =
   j_nf_evar !(pb.evdref) j
 
 (* Build the sub-pattern-matching problem for a given branch "C x1..xn as x" *)
-let build_branch current deps (realnames,curname) pb arsign eqns const_info =
+let build_branch current realargs deps (realnames,curname) pb arsign eqns const_info =
   (* We remember that we descend through constructor C *)
   let history =
     push_history_pattern const_info.cs_nargs const_info.cs_cstr pb.history in
@@ -1143,6 +1161,12 @@ let build_branch current deps (realnames,curname) pb arsign eqns const_info =
   let typs' =
     list_map_i (fun i d -> (mkRel i,map_rel_declaration (lift i) d)) 1 typs in
 
+  let extenv = push_rels typs pb.env in
+
+  let typs' =
+    List.map (fun (c,d) ->
+      (c,extract_inductive_data extenv !(pb.evdref) d,d)) typs' in
+
   (* We compute over which of x(i+1)..xn and x matching on xi will need a *)
   (* generalization *)
   let dep_sign =
@@ -1154,29 +1178,34 @@ let build_branch current deps (realnames,curname) pb arsign eqns const_info =
      terms is relative to the current context enriched by topushs *)
   let ci = build_dependent_constructor const_info in
 
-  (* We replace [(mkRel 1)] by its expansion [ci] *)
-  (* and context "Gamma = Gamma1, current, Gamma2" by "Gamma;typs;curalias" *)
-  (* This is done in two steps : first from "Gamma |- tms" *)
-  (* into  "Gamma; typs; curalias |- tms" *)
-  let tomatch = lift_tomatch_stack const_info.cs_nargs pb.tomatch in
+  (* Current context Gamma has the form Gamma1;cur:I(realargs);Gamma2 *)
+  (* We go from Gamma |- PI tms. pred to                              *)
+  (* Gamma;x1..xn;curalias:I(x1..xn) |- PI tms'. pred'                *)
+  (* where, in tms and pred, those realargs that are vars are         *)
+  (* replaced by the corresponding xi and cur replaced by curalias    *)
+  let cirealargs = Array.to_list const_info.cs_concl_realargs in
 
-  let tomatch = match kind_of_term current with
-    | Rel i -> replace_tomatch (i+const_info.cs_nargs) ci tomatch
-    | _ -> (* non-rel initial term *) tomatch in
+  (* Do the specialization for terms to match *)
+  let tomatch = List.fold_right2 (fun par arg tomatch ->
+    match kind_of_term par with
+    | Rel i -> replace_tomatch (i+const_info.cs_nargs) arg tomatch
+    | _ -> tomatch) (current::realargs) (ci::cirealargs)
+      (lift_tomatch_stack const_info.cs_nargs pb.tomatch) in
 
   let pred_is_not_dep =
     noccur_predicate_between 1 (List.length realnames + 1) pb.pred tomatch in
 
   let typs' =
     List.map2
-      (fun (tm,(na,c,t)) deps ->
+      (fun (tm,(tmtyp,_),(na,_,_)) deps ->
 	let na = match curname with
 	| Name _ -> (if na <> Anonymous then na else curname)
 	| Anonymous ->
 	    if deps = [] && pred_is_not_dep then Anonymous else force_name na in
-	((tm,NotInd(c,t)),deps,na))
+	((tm,tmtyp),deps,na))
       typs' (List.rev dep_sign) in
 
+  (* Do the specialization for the predicate *)
   let pred =
     specialize_predicate typs' (realnames,curname) arsign const_info tomatch pb.pred in
 
@@ -1205,7 +1234,7 @@ let build_branch current deps (realnames,curname) pb arsign eqns const_info =
 
   typs,
   { pb with
-      env = push_rels typs pb.env;
+      env = extenv;
       tomatch = tomatch;
       pred = pred;
       history = history;
@@ -1253,7 +1282,7 @@ and match_current pb tomatch =
 	  let pb,deps = generalize_problem (names,dep) pb deps in
 
 	  (* We compile branches *)
-	  let brvals = array_map2 (compile_branch current (names,dep) deps pb arsign) eqns cstrs in
+	  let brvals = array_map2 (compile_branch current realargs (names,dep) deps pb arsign) eqns cstrs in
 	  (* We build the (elementary) case analysis *)
           let brvals,tomatch,pred,inst =
             postprocess_dependencies !(pb.evdref) current
@@ -1287,8 +1316,8 @@ and shift_problem ((current,t),_,na) pb =
     uj_type = subst1 current j.uj_type }
 
 (* Building the sub-problem when all patterns are variables *)
-and compile_branch current names deps pb arsign eqns cstr =
-  let sign, pb = build_branch current deps names pb arsign eqns cstr in
+and compile_branch current realargs names deps pb arsign eqns cstr =
+  let sign, pb = build_branch current realargs deps names pb arsign eqns cstr in
   sign, (compile pb).uj_val
 
 (* Abstract over a declaration before continuing splitting *)
@@ -1547,18 +1576,18 @@ let build_inversion_problem loc env sigma tms t =
 
   let decls =
     list_map_i (fun i d -> (mkRel i,map_rel_declaration (lift i) d)) 1 sign in
+
+  let pb_env = push_rels sign env in
+  let decls =
+    List.map (fun (c,d) -> (c,extract_inductive_data pb_env sigma d,d)) decls in
+
   let decls = List.rev decls in
   let dep_sign = find_dependencies_signature (list_make n true) decls in
 
-  let pb_env = push_rels sign env in
   let sub_tms =
-    List.map2 (fun deps (tm,(na,b,t)) ->
-      let typ =
-	if b<>None then NotInd (None,t) else
-	  try try_find_ind pb_env sigma t None
-	  with Not_found -> NotInd (None,t) in
+    List.map2 (fun deps (tm,(tmtyp,_),(na,b,t)) ->
       let na = if deps = [] then Anonymous else force_name na in
-      Pushed ((tm,typ),deps,na))
+      Pushed ((tm,tmtyp),deps,na))
       dep_sign decls in
   let subst = List.map (fun (na,t) -> (na,lift n t)) subst in
   (* [eqn1] is the first clause of the auxiliary pattern-matching that
@@ -1787,6 +1816,9 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e
     let out_tmt na = function NotInd (c,t) -> (na,c,t) | IsInd (typ,_,_) -> (na,None,typ) in
     let typs = List.map2 (fun na (tm,tmt) -> (tm,out_tmt na tmt)) nal tomatchs in
 
+    let typs =
+      List.map (fun (c,d) -> (c,extract_inductive_data env sigma d,d)) typs in
+
     let dep_sign =
       find_dependencies_signature
         (list_make (List.length typs) true)