- 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

4 files changed, 34 insertions, 38 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 423ade8b6d..0e7c92a6ce 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -125,6 +125,8 @@ let ident_eq =
               | _ -> raise Stream.Failure)
         | _ -> raise Stream.Failure)
 
+let aliasvar = function CPatAlias (_, _, id) -> Some (Name id) | _ -> None
+
 GEXTEND Gram
   GLOBAL: binder_constr lconstr constr operconstr sort global
   constr_pattern lconstr_pattern Constr.ident
@@ -228,15 +230,16 @@ GEXTEND Gram
 	  ":="; c1 = operconstr LEVEL "200"; "in";
           c2 = operconstr LEVEL "200" ->
           CLetTuple (loc,List.map snd lb,po,c1,c2)
-      | "let"; "|"; p=pattern; ":="; c1 = operconstr LEVEL "200";
+      | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
           "in"; c2 = operconstr LEVEL "200" ->
-	    CLetPattern (loc, p, c1, c2)
-      | "dest"; c1 = operconstr LEVEL "200";
-	  "as"; p=pattern; 
+	    CCases (loc, LetPatternStyle, None, [(c1,(None,None))], [(loc, [(loc,[p])], c2)])
+      | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; 
+	  rt = case_type; "in"; c2 = operconstr LEVEL "200" ->
+	    CCases (loc, LetPatternStyle, Some rt, [(c1, (aliasvar p, None))], [(loc, [(loc, [p])], c2)])
+      | "let"; "'"; p=pattern; "in"; t = operconstr LEVEL "200"; 
+	  ":="; c1 = operconstr LEVEL "200"; rt = case_type;
           "in"; c2 = operconstr LEVEL "200" ->
-	    let loc' = cases_pattern_expr_loc p in
-              CCases (loc, None, [(c1, (None, None))],
-                     [loc, [loc',[p]], c2])
+	    CCases (loc, LetPatternStyle, Some rt, [(c1, (aliasvar p, Some t))], [(loc, [(loc, [p])], c2)])
       | "if"; c=operconstr LEVEL "200"; po = return_type;
 	"then"; b1=operconstr LEVEL "200";
         "else"; b2=operconstr LEVEL "200" ->
@@ -283,7 +286,7 @@ GEXTEND Gram
 (*   ; *)
   match_constr:
     [ [ "match"; ci=LIST1 case_item SEP ","; ty=OPT case_type; "with";
-        br=branches; "end" -> CCases(loc,ty,ci,br) ] ]
+        br=branches; "end" -> CCases(loc,RegularStyle,ty,ci,br) ] ]
   ;
   case_item:
     [ [ c=operconstr LEVEL "100"; p=pred_pattern -> (c,p) ] ]
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 47725cbd65..a9f3fd487c 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -171,7 +171,7 @@ let rec interp_xml_constr = function
       let mat = simple_cases_matrix_of_branches ind brns brs in
       let nparams,n = compute_inductive_nargs ind in
       let nal,rtn = return_type_of_predicate ind nparams n p in
-      RCases (loc,rtn,[tm,nal],mat)
+      RCases (loc,RegularStyle,rtn,[tm,nal],mat)
   | XmlTag (loc,"MUTIND",al,[]) ->
       RRef (loc, IndRef (get_xml_inductive al))
   | XmlTag (loc,"MUTCONSTRUCT",al,[]) ->
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 7d0d085938..21c5a343b4 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -434,27 +434,16 @@ let tm_clash = function
       -> Some id
   | _ -> None
 
-let pr_case_item pr (tm,(na,indnalopt)) =
-  hov 0 (pr (lcast,E) tm ++
-(*
-  (match na with
-    | Name id when not (is_var id tm) -> spc () ++ str "as " ++  pr_id id
-    | Anonymous when tm_clash (tm,indnalopt) <> None ->
-	(* hide [tm] name to avoid conflicts *)
-	spc () ++ str "as _" (* ++ pr_id (Option.get (tm_clash (tm,indnalopt)))*)
-    | _ -> mt ()) ++
-*)
+let pr_asin pr (na,indnalopt) =
   (match na with (* Decision of printing "_" or not moved to constrextern.ml *)
     | Some na -> spc () ++ str "as " ++  pr_name na
     | None -> mt ()) ++
   (match indnalopt with
     | None -> mt ()
-(*
-    | Some (_,ind,nal) ->
-        spc () ++ str "in " ++ 
-        hov 0 (pr_reference ind ++ prlist (pr_arg pr_name) nal))
-*)
-    | Some t -> spc () ++ str "in " ++ pr lsimple t))
+    | Some t -> spc () ++ str "in " ++ pr lsimple t)
+    
+let pr_case_item pr (tm,asin) =
+  hov 0 (pr (lcast,E) tm ++ pr_asin pr asin)
 
 let pr_case_type pr po =
   match po with
@@ -551,15 +540,24 @@ let rec pr sep inherited a =
       else
 	p, lproj
   | CApp (_,(None,a),l) -> pr_app (pr mt) a l, lapp
-  | CCases (_,rtntypopt,c,eqns) ->
+  | CCases (_,LetPatternStyle,rtntypopt,[c,asin],[(_,[(loc,[p])],b)]) ->
+      hv 0 (
+	str "let '" ++ 
+	  hov 0 (pr_patt ltop p ++ 
+		 pr_asin (pr_dangling_with_for mt) asin ++
+		 str " :=" ++ pr spc ltop c ++ 
+		 pr_case_type (pr_dangling_with_for mt) rtntypopt ++
+		 str " in" ++ pr spc ltop b)),
+	lletpattern
+  | CCases(_,_,rtntypopt,c,eqns) ->
       v 0
         (hv 0 (str "match" ++ brk (1,2) ++
-	  hov 0 (
-	    prlist_with_sep sep_v
-              (pr_case_item (pr_dangling_with_for mt)) c
-            ++ pr_case_type (pr_dangling_with_for mt) rtntypopt) ++
-	spc () ++ str "with") ++
-        prlist (pr_eqn (pr mt)) eqns ++ spc() ++ str "end"),
+		  hov 0 (
+		    prlist_with_sep sep_v
+		      (pr_case_item (pr_dangling_with_for mt)) c
+		    ++ pr_case_type (pr_dangling_with_for mt) rtntypopt) ++
+		  spc () ++ str "with") ++
+		  prlist (pr_eqn (pr mt)) eqns ++ spc() ++ str "end"),
       latom
   | CLetTuple (_,nal,(na,po),c,b) ->
       hv 0 (
@@ -571,11 +569,6 @@ let rec pr sep inherited a =
                pr spc ltop c ++ str " in") ++
         pr spc ltop b),
       lletin
-  | CLetPattern (_, p, c, b) ->
-      hv 0 (
-	str "let| " ++ 
-	hov 0 (pr_patt ltop p ++ str " :=" ++ pr spc ltop c ++ str " in") ++
-	pr spc ltop b), lletpattern
   | CIf (_,c,(na,po),b1,b2) ->
       (* On force les parenthèses autour d'un "if" sous-terme (même si le
 	 parsing est lui plus tolérant) *)
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index b5ad753afc..922c7af163 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -153,7 +153,7 @@ let rec mlexpr_of_constr = function
   | Topconstr.CLetIn (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO"
   | Topconstr.CAppExpl (loc,a,l) -> <:expr< Topconstr.CAppExpl $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >>
   | Topconstr.CApp (loc,a,l) -> <:expr< Topconstr.CApp $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option (mlexpr_of_located mlexpr_of_explicitation))) l$ >>
-  | Topconstr.CCases (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO"
+  | Topconstr.CCases (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO"
   | Topconstr.CHole (loc, None) -> <:expr< Topconstr.CHole $dloc$ None >>
   | Topconstr.CHole (loc, Some _) -> failwith "mlexpr_of_constr: TODO CHole (Some _)"
   | Topconstr.CNotation(_,ntn,l) ->