- Second pass on implementation of let pattern. Parse "let ' par [as x]?

  [in I] := t [return pred] in b", just as SSReflect does with let:. 
  Change implementation: no longer a separate AST node, just add a case_style
  annotation on Cases to indicate it (if ML was dependently typed we
  could ensure that LetPatternStyle Cases have only one term to be
  matched and one branch, alas...). This factors out most code and we lose
  no functionality (win ! win !). Add LetPat.v test suite.

- Slight improvement of inference of return clauses for dependent
  pattern matching. If matching a variable of non-dependent type
  under a tycon that mentions it while giving no return clause, the
  dependency will be automatically infered. Examples at the end of
  DepPat. Should get rid of most explicit returns under tycons.


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

7 files changed, 91 insertions, 83 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index b7317b5be0..e1c5beeea2 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -65,7 +65,7 @@ let error_needs_inversion env x t =
 
 module type S = sig
   val compile_cases :
-    loc ->
+    loc -> case_style ->
     (type_constraint -> env -> rawconstr -> unsafe_judgment) *
       Evd.evar_defs ref ->
     type_constraint -> 
@@ -275,13 +275,14 @@ let push_history_pattern n current cont =
 
 *)
 type pattern_matching_problem =
-    { env      : env;
-      evdref   : Evd.evar_defs ref;
-      pred     : predicate_signature option;
-      tomatch  : tomatch_stack;
-      history  : pattern_continuation;
-      mat      : matrix;
-      caseloc  : loc;
+    { env       : env;
+      evdref    : Evd.evar_defs ref;
+      pred      : predicate_signature option;
+      tomatch   : tomatch_stack;
+      history   : pattern_continuation;
+      mat       : matrix;
+      caseloc   : loc;
+      casestyle : case_style;
       typing_function: type_constraint -> env -> rawconstr -> unsafe_judgment }
 
 (*--------------------------------------------------------------------------*
@@ -1275,7 +1276,7 @@ and match_current pb tomatch =
 	  let (pred,typ,s) =
 	    find_predicate pb.caseloc pb.env pb.evdref 
 	      pb.pred brtyps cstrs current indt pb.tomatch in
-	  let ci = make_case_info pb.env mind RegularStyle in
+	  let ci = make_case_info pb.env mind pb.casestyle in
 	  let case = mkCase (ci,nf_betaiota pred,current,brvals) in
 	  let inst = List.map mkRel deps in
 	  { uj_val = applist (case, inst);
@@ -1504,7 +1505,7 @@ let extract_arity_signature env0 tomatchl tmsign =
 	    | Some (loc,_,_,_) -> 
  	    user_err_loc (loc,"",
 	    str "Unexpected type annotation for a term of non inductive type"))
-      | IsInd (_,IndType(indf,realargs)) ->
+      | IsInd (term,IndType(indf,realargs)) ->
           let indf' = lift_inductive_family n indf in
 	  let (ind,params) = dest_ind_family indf' in
 	  let nrealargs = List.length realargs in
@@ -1519,6 +1520,14 @@ let extract_arity_signature env0 tomatchl tmsign =
 		  List.rev realnal
 	      | None -> list_tabulate (fun _ -> Anonymous) nrealargs in
 	  let arsign = fst (get_arity env0 indf') in
+(* 	  let na =  *)
+(* 	    match na with  *)
+(* 	      | Name _ -> na *)
+(* 	      | Anonymous -> *)
+(* 		  match kind_of_term term with *)
+(* 		    | Rel n -> pi1 (lookup_rel n (Environ.rel_context env0)) *)
+(* 		    | _ -> Anonymous *)
+(* 	  in *)
 	  (na,None,build_dependent_inductive env0 indf')
 	  ::(List.map2 (fun x (_,c,t) ->(x,c,t)) realnal arsign) in
   let rec buildrec n = function
@@ -1537,6 +1546,34 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon =
           j
     | None -> j
 
+(* We put the tycon inside the arity signature, possibly discovering dependencies. *)
+
+let prepare_predicate_from_arsign_tycon loc env evdref tomatchs sign arsign c =
+  let nar = List.fold_left (fun n sign -> List.length sign + n) 0 arsign in
+  let subst, len = 
+    List.fold_left2 (fun (subst, len) (tm, tmtype) sign ->
+      let signlen = List.length sign in
+	match kind_of_term tm with
+	  | Rel n when dependent tm c 
+		&& signlen = 1 (* The term to match is not of a dependent type itself *) ->
+	      ((n, len) :: subst, len - signlen)
+	  | _ -> (subst, len - signlen))
+      ([], nar) tomatchs arsign
+  in
+  let rec predicate lift c =
+    match kind_of_term c with
+      | Rel n when n > lift -> 
+	  (try 
+	      (* Make the predicate dependent on the matched variable *)
+	      let idx = List.assoc (n - lift) subst in
+		mkRel (idx + lift)
+	    with Not_found -> 
+	      (* A variable that is not matched, lift over the arsign. *)
+	      mkRel (n + nar))
+      | _ ->
+	  map_constr_with_binders succ predicate lift c 
+  in predicate 0 c
+
 
 (* Builds the predicate. If the predicate is dependent, its context is
  * made of 1+nrealargs assumptions for each matched term in an inductive
@@ -1545,7 +1582,8 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon =
 
  * Each matched terms are independently considered dependent or not.
 
- * A type constraint but no annotation case: it is assumed non dependent.
+ * A type constraint but no annotation case: we try to specialize the
+ * tycon to make the predicate if it is not closed.
  *)
 
 let prepare_predicate loc typing_fun evdref env tomatchs sign tycon = function
@@ -1553,9 +1591,23 @@ let prepare_predicate loc typing_fun evdref env tomatchs sign tycon = function
   | None ->
       (match tycon with
        | Some (None, t) ->
-	   let names,pred = 
-	     prepare_predicate_from_tycon loc false env evdref tomatchs sign t 
-	   in Some (build_initial_predicate false names pred)
+	   if noccur_with_meta 0 max_int t then
+	     let names,pred =
+	       prepare_predicate_from_tycon loc false env evdref tomatchs sign t
+	     in
+	       Some (build_initial_predicate false names pred)
+	   else
+	     let arsign = extract_arity_signature env tomatchs sign in
+	     let env' = List.fold_right push_rels arsign env in
+	     let names = List.rev (List.map (List.map pi1) arsign) in
+	     let pred = prepare_predicate_from_arsign_tycon loc env' evdref tomatchs sign arsign t in
+	       if eq_constr pred t then
+		 let names,pred =
+		   prepare_predicate_from_tycon loc false env evdref tomatchs sign t
+		 in
+		   Some (build_initial_predicate false names pred)
+	       else
+		 Some (build_initial_predicate true names pred)
        | _ -> None)
 
   (* Some type annotation *)
@@ -1577,7 +1629,7 @@ let prepare_predicate loc typing_fun evdref env tomatchs sign tycon = function
 (**************************************************************************)
 (* Main entry of the matching compilation                                 *)
   
-let compile_cases loc (typing_fun, evdref) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns)=
+let compile_cases loc style (typing_fun, evdref) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns)=
   
   (* We build the matrix of patterns and right-hand-side *)
   let matx = matx_of_eqns env tomatchl eqns in
@@ -1596,13 +1648,14 @@ let compile_cases loc (typing_fun, evdref) (tycon : Evarutil.type_constraint) en
   let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
     
   let pb =
-    { env      = env;
-      evdref   = evdref;
-      pred     = pred;
-      tomatch  = initial_pushed;
-      history  = start_history (List.length initial_pushed);
-      mat      = matx;
-      caseloc  = loc;
+    { env       = env;
+      evdref    = evdref;
+      pred      = pred;
+      tomatch   = initial_pushed;
+      history   = start_history (List.length initial_pushed);
+      mat       = matx;
+      caseloc   = loc;
+      casestyle = style;
       typing_function = typing_fun } in
     
   let j = compile pb in
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index d105ca2d0f..a2015c2b17 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -50,7 +50,7 @@ val error_needs_inversion : env -> constr -> types -> 'a
 
 module type S = sig
   val compile_cases :
-    loc ->
+    loc -> case_style ->
     (type_constraint -> env -> rawconstr -> unsafe_judgment) * evar_defs ref ->
     type_constraint -> 
     env -> rawconstr option * tomatch_tuples * cases_clauses ->
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 34e6945584..164043cf7c 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -349,8 +349,6 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
       let bl' = Array.map detype bl in
       let (nal,d) = it_destRLambda_or_LetIn_names consnargsl.(0) bl'.(0) in
       RLetTuple (dl,nal,(alias,pred),tomatch,d)
-  | LetPatternStyle when List.length eqnl = 1 -> (* If irrefutable due to some inversion, print as match *) 
-      RLetPattern (dl,(tomatch,(alias,aliastyp)),List.hd eqnl)
   | IfStyle when aliastyp = None ->
       let bl' = Array.map detype bl in
       let nondepbrs =
@@ -359,9 +357,9 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
 	RIf (dl,tomatch,(alias,pred),
              Option.get nondepbrs.(0),Option.get nondepbrs.(1))
       else
-	RCases (dl,pred,[tomatch,(alias,aliastyp)],eqnl)
+	RCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl)
   | _ ->
-      RCases (dl,pred,[tomatch,(alias,aliastyp)],eqnl)
+      RCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl)
 
 let detype_sort = function
   | Prop c -> RProp c
@@ -605,7 +603,7 @@ let rec subst_rawconstr subst raw =
 	if r1' == r1 && r2' == r2 then raw else
 	  RLetIn (loc,n,r1',r2')
 
-  | RCases (loc,rtno,rl,branches) -> 
+  | RCases (loc,sty,rtno,rl,branches) -> 
       let rtno' = Option.smartmap (subst_rawconstr subst) rtno
       and rl' = list_smartmap (fun (a,x as y) ->
         let a' = subst_rawconstr subst a in
@@ -625,7 +623,7 @@ let rec subst_rawconstr subst raw =
 			branches
       in
 	if rtno' == rtno && rl' == rl && branches' == branches then raw else
-	  RCases (loc,rtno',rl',branches')
+	  RCases (loc,sty,rtno',rl',branches')
 
   | RLetTuple (loc,nal,(na,po),b,c) ->
       let po' = Option.smartmap (subst_rawconstr subst) po
@@ -633,28 +631,6 @@ let rec subst_rawconstr subst raw =
       and c' = subst_rawconstr subst c in
 	if po' == po && b' == b && c' == c then raw else
           RLetTuple (loc,nal,(na,po'),b',c')
-
-  | RLetPattern (loc, (a,x as c), (loc',idl,cpl,r as branch)) ->
-      let c' = 
-	let a' = subst_rawconstr subst a in
-        let (n,topt) = x in 
-        let topt' = Option.smartmap
-          (fun (loc,(sp,i),x,y as t) ->
-            let sp' = subst_kn subst sp in
-              if sp == sp' then t else (loc,(sp',i),x,y))
-	  topt 
-	in
-          if a == a' && topt == topt' then c else (a',(n,topt'))
-      in
-      let p' = 
-	let cpl' =
-	  list_smartmap (subst_cases_pattern subst) cpl
-	and r' = subst_rawconstr subst r in
-	  if cpl' == cpl && r' == r then branch else
-	    (loc',idl,cpl',r')
-      in 
-	if c' == c && p' == branch then raw else
-	  RLetPattern (loc, c', p')
 	        
   | RIf (loc,c,(na,po),b1,b2) ->
       let po' = Option.smartmap (subst_rawconstr subst) po
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 845f9fae1f..90a3728ebb 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -245,7 +245,7 @@ let rec pat_of_raw metas vars = function
       let c = List.fold_left mkRLambda c nal in
       PCase ((LetStyle,[|1|],None,None),PMeta None,pat_of_raw metas vars b,
              [|pat_of_raw metas vars c|])
-  | RCases (loc,p,[c,(na,indnames)],brs) ->
+  | RCases (loc,sty,p,[c,(na,indnames)],brs) ->
       let pred,ind_nargs, ind = match p,indnames with
 	| Some p, Some (_,ind,n,nal) ->
 	    rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas vars p)),
@@ -259,7 +259,7 @@ let rec pat_of_raw metas vars = function
 	Array.init (List.length brs) (pat_of_raw_branch loc metas vars ind brs)
       in
       let cstr_nargs,brs = (Array.map fst cbrs, Array.map snd cbrs) in
-      PCase ((RegularStyle,cstr_nargs,ind,ind_nargs), pred,
+      PCase ((sty,cstr_nargs,ind,ind_nargs), pred,
              pat_of_raw metas vars c, brs)
              
   | r ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f9fcdb7b63..83381710d3 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -582,23 +582,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	      mkCase (ci, pred, cj.uj_val, [|b1;b2|])
 	  in
 	    { uj_val = v; uj_type = p }
-
-    | RLetPattern (loc, c, p) ->
-	(* Just use cases typing *)
-	let j = 
-	  pretype tycon env evdref lvar 
-	    (RCases (loc, None, [c], [p]))
-	in 
-	(* Change case info *)
-	let j' = match kind_of_term j.uj_val with
-	    Case (ci, po, c, br) ->
-	      let pp_info = { ci.ci_pp_info with style = LetPatternStyle } in
-		{ j with uj_val = mkCase ({ ci with ci_pp_info = pp_info }, po, c, br) }
-	  | _ -> j
-	in j'
 	
-    | RCases (loc,po,tml,eqns) ->
-	Cases.compile_cases loc
+    | RCases (loc,sty,po,tml,eqns) ->
+	Cases.compile_cases loc sty
 	  ((fun vtyc env -> pretype vtyc env evdref lvar),evdref)
 	  tycon env (* loc *) (po,tml,eqns)
 
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index e7f5de028f..fe48cd4fa7 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -62,10 +62,9 @@ type rawconstr =
   | RLambda of loc * name * binding_kind * rawconstr * rawconstr
   | RProd of loc * name * binding_kind * rawconstr * rawconstr
   | RLetIn of loc * name * rawconstr * rawconstr
-  | RCases of loc * rawconstr option * tomatch_tuples * cases_clauses
+  | RCases of loc * case_style * rawconstr option * tomatch_tuples * cases_clauses
   | RLetTuple of loc * name list * (name * rawconstr option) * 
       rawconstr * rawconstr
-  | RLetPattern of loc * tomatch_tuple * cases_clause
   | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
   | RRec of loc * fix_kind * identifier array * rawdecl list array *
       rawconstr array * rawconstr array
@@ -115,14 +114,12 @@ let map_rawconstr f = function
   | RLambda (loc,na,bk,ty,c) -> RLambda (loc,na,bk,f ty,f c)
   | RProd (loc,na,bk,ty,c) -> RProd (loc,na,bk,f ty,f c)
   | RLetIn (loc,na,b,c) -> RLetIn (loc,na,f b,f c)
-  | RCases (loc,rtntypopt,tml,pl) ->
-      RCases (loc,Option.map f rtntypopt,
+  | RCases (loc,sty,rtntypopt,tml,pl) ->
+      RCases (loc,sty,Option.map f rtntypopt,
         List.map (fun (tm,x) -> (f tm,x)) tml,
         List.map (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl)
   | RLetTuple (loc,nal,(na,po),b,c) ->
       RLetTuple (loc,nal,(na,Option.map f po),f b,f c)
-  | RLetPattern (loc,(b,x),(loc',idl,p,c)) ->
-      RLetPattern (loc,(f b,x),(loc',idl,p,f c))
   | RIf (loc,c,(na,po),b1,b2) ->
       RIf (loc,f c,(na,Option.map f po),f b1,f b2)
   | RRec (loc,fk,idl,bl,tyl,bv) ->
@@ -177,14 +174,13 @@ let occur_rawconstr id =
     | RLambda (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
     | RProd (loc,na,bk,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,rtntypopt,tml,pl) ->
+    | RCases (loc,sty,rtntypopt,tml,pl) ->
 	(occur_option rtntypopt)
         or (List.exists (fun (tm,_) -> occur tm) tml)
 	or (List.exists occur_pattern pl)
     | RLetTuple (loc,nal,rtntyp,b,c) -> 
 	occur_return_type rtntyp id
         or (occur b) or (not (List.mem (Name id) nal) & (occur c))
-    | RLetPattern (loc, (b, _), p) -> (occur b) or (occur_pattern p)
     | RIf (loc,c,rtntyp,b1,b2) -> 
 	occur_return_type rtntyp id or (occur c) or (occur b1) or (occur b2)
     | RRec (loc,fk,idl,bl,tyl,bv) ->
@@ -224,7 +220,7 @@ let free_rawvars  =
 	let vs' = vars bounded vs ty in 
 	let bounded' = add_name_to_ids bounded na in 
 	vars bounded' vs' c
-    | RCases (loc,rtntypopt,tml,pl) ->
+    | RCases (loc,sty,rtntypopt,tml,pl) ->
 	let vs1 = vars_option bounded vs rtntypopt in 
 	let vs2 = List.fold_left (fun vs (tm,_) -> vars bounded vs tm) vs1 tml in 
 	List.fold_left (vars_pattern bounded) vs2 pl
@@ -233,7 +229,6 @@ let free_rawvars  =
 	let vs2 = vars bounded vs1 b in 
 	let bounded' = List.fold_left add_name_to_ids bounded nal in
 	vars bounded' vs2 c
-    | RLetPattern (loc, (c, _), p) -> vars_pattern bounded (vars bounded vs c) p
     | RIf (loc,c,rtntyp,b1,b2) -> 
 	let vs1 = vars_return_type bounded vs rtntyp in 
 	let vs2 = vars bounded vs1 c in 
@@ -285,8 +280,7 @@ let loc_of_rawconstr = function
   | RLambda (loc,_,_,_,_) -> loc
   | RProd (loc,_,_,_,_) -> loc
   | RLetIn (loc,_,_,_) -> loc
-  | RLetPattern (loc,_,_) -> loc
-  | RCases (loc,_,_,_) -> loc
+  | RCases (loc,_,_,_,_) -> loc
   | RLetTuple (loc,_,_,_,_) -> loc
   | RIf (loc,_,_,_,_) -> loc
   | RRec (loc,_,_,_,_,_) -> loc
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 7b342c4115..ab67a0922b 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -66,10 +66,9 @@ type rawconstr =
   | RLambda of loc * name * binding_kind *  rawconstr * rawconstr
   | RProd of loc * name * binding_kind * rawconstr * rawconstr
   | RLetIn of loc * name * rawconstr * rawconstr
-  | RCases of loc * rawconstr option * tomatch_tuples * cases_clauses
+  | RCases of loc * case_style * rawconstr option * tomatch_tuples * cases_clauses
   | RLetTuple of loc * name list * (name * rawconstr option) * 
       rawconstr * rawconstr
-  | RLetPattern of loc * tomatch_tuple * cases_clause
   | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
   | RRec of loc * fix_kind * identifier array * rawdecl list array *
       rawconstr array * rawconstr array