Finish let| implementation and document it

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

6 files changed, 55 insertions, 9 deletions

diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index 986825f25c..9669acc230 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -493,7 +493,13 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	let j = 
 	  pretype tycon env isevars lvar 
 	    (RCases (loc, None, [c], [p]))
-	in j
+	(* 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
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 31a1eabb2b..da39b1d3dd 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -285,17 +285,18 @@ Check (fun x (H:{x=0}+{x<>0}) =>
 Notice that the printing uses the {\tt if} syntax because {\tt sumbool} is
 declared as such (see Section~\ref{printing-options}).
 
-\subsection{Irrefutable patterns: the destructuring {\tt let}
+\subsection{Irrefutable patterns: the destructuring {\tt let} variants 
 \index{let in@{\tt let ... in}}
 \label{Letin}}
 
-
-
 Closed terms (that is not relying on any axiom or variable) in an
 inductive type having only one constructor, say {\tt foo}, have
 necessarily the form \texttt{(foo ...)}. In this case, the {\tt match}
 construction can be written with a syntax close to the {\tt let ... in
-...}  construction. Expression {\tt let
+...}  construction. 
+
+\subsubsection{Destructuring {\tt let}}
+Expression {\tt let
 (}~{\ident$_1$},\ldots,{\ident$_n$}~{\tt ) :=}~{\term$_0$}~{\tt
 in}~{\term$_1$} performs case analysis on {\term$_0$} which must be in
 an inductive type with one constructor with $n$ arguments. Variables
@@ -331,6 +332,35 @@ The general equivalence for an inductive type with one constructors {\tt C} is
 $\equiv$~
 {\tt match {\term} \zeroone{\ifitem} with C {\ident}$_1$ {\ldots} {\ident}$_n$ \verb!=>! {\term}' end}
 
+
+\subsubsection{{\tt let} pattern}
+
+Another destructuring {\tt let} syntax is available for inductives with
+one constructor by giving an arbitrary pattern instead of just a tuple
+for all the arguments. For example, the preceding example can be written:
+\begin{coq_eval}
+Reset fst.
+\end{coq_eval}
+\begin{coq_example}
+Definition fst (A B:Set) (p:A * B) := let| pair x _ := p in x.
+\end{coq_example}
+
+This is useful to match deeper inside tuples and also to use notations
+for the pattern, as the syntax {\tt let| p := t in b} allows arbitrary
+patterns to do the deconstruction. For example:
+
+\begin{coq_example}
+Definition deep_tuple (A : Set) (x : (A * A) * (A * A)) : A * A * A * A :=
+  let| ((a,b), (c, d)) := x in (a,b,c,d).
+Notation " x 'with' p " := (exist _ x p) (at level 20).
+Definition proj1_sig' (A :Set) (P : A -> Prop) (t:{ x : A | P x }) : A :=
+  let| x with p := t in x.
+\end{coq_example}
+
+When printing definitions which are written using this construct it
+takes precedence over {\tt let} printing directives for the datatype
+under consideration (see Section~\ref{printing-options}).
+
 \subsection{Controlling pretty-printing of {\tt match} expressions
 \label{printing-options}}
 
@@ -1433,5 +1463,4 @@ The constraints on the internal level of the occurrences of {\Type}
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
-%%% TeX-master: "Reference-Manual"
 %%% End: 
diff --git a/kernel/term.ml b/kernel/term.ml
index ad4bd2bda2..45cd2fb0e0 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -24,7 +24,7 @@ type metavariable = int
 (* This defines the strategy to use for verifiying a Cast *)
 
 (* This defines Cases annotations *)
-type case_style = LetStyle | IfStyle | MatchStyle | RegularStyle
+type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
 type case_printing =
   { ind_nargs : int; (* number of real args of the inductive type *)
     style     : case_style }
diff --git a/kernel/term.mli b/kernel/term.mli
index f71207c5e1..2c6e7f0b48 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -40,7 +40,7 @@ type existential_key = int
 type metavariable = int
 
 (*s Case annotation *)
-type case_style = LetStyle | IfStyle | MatchStyle | RegularStyle
+type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
 type case_printing =
   { ind_nargs : int; (* number of real args of the inductive type *)
     style     : case_style }
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index f0203fa2c4..b6ec169254 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -321,6 +321,8 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
     try 
       if !Flags.raw_print then
         RegularStyle
+      else if st = LetPatternStyle then 
+	st
       else if PrintingLet.active (indsp,consnargsl) then
 	LetStyle
       else if PrintingIf.active (indsp,consnargsl) then 
@@ -334,6 +336,8 @@ 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 =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index db492c026b..e30f553fe0 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -588,7 +588,14 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	let j = 
 	  pretype tycon env evdref lvar 
 	    (RCases (loc, None, [c], [p]))
-	in j
+	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