From f7ae4e6433e44a0b3a838847c58ab72ffffa3d48 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 19 Jul 2016 13:19:34 +0200
Subject: Some extra fixes in printing patterns in binders.

- typo in notation_ops.ml
- factorization of patterns in ppconstr.ml
- update of test-suite
- printing of cast of a binding pattern if in mode "printing all"

The question of whether or not to print the type of a binding pattern
by default seems open to me.
---
 printing/ppconstr.ml | 43 ++++++++++++-------------------------------
 1 file changed, 12 insertions(+), 31 deletions(-)

(limited to 'printing/ppconstr.ml')

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 7aa6d4858c..dab97d603b 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -350,7 +350,12 @@ end) = struct
       surround (pr_lname na ++ pr_opt_type pr_c topt ++
                   str":=" ++ cut() ++ pr_c c)
     | LocalPattern (loc,p,tyo) ->
-        str "'" ++ pr_patt lsimplepatt p
+      let p = pr_patt lsimplepatt p in
+      match tyo with
+        | None ->
+          str "'" ++ p
+        | Some ty ->
+          str "'" ++ surround (p ++ spc () ++ str ":" ++ ws 1 ++ pr_c ty)
 
   let pr_undelimited_binders sep pr_c =
     prlist_with_sep sep (pr_binder_among_many pr_c)
@@ -374,6 +379,9 @@ end) = struct
       if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*)
     | CProdN (loc,[],c) ->
       extract_prod_binders c
+    | CProdN (loc,[[_,Name id],bk,t],CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)])) ->
+      let bl,c = extract_prod_binders b in
+      LocalPattern (loc,p,None) :: bl, c
     | CProdN (loc,(nal,bk,t)::bl,c) ->
       let bl,c = extract_prod_binders (CProdN(loc,bl,c)) in
       LocalRawAssum (nal,bk,t) :: bl, c
@@ -385,6 +393,9 @@ end) = struct
       if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*)
     | CLambdaN (loc,[],c) ->
       extract_lam_binders c
+    | CLambdaN (loc,[[_,Name id],bk,t],CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)])) ->
+      let bl,c = extract_lam_binders b in
+      LocalPattern (loc,p,None) :: bl, c
     | CLambdaN (loc,(nal,bk,t)::bl,c) ->
       let bl,c = extract_lam_binders (CLambdaN(loc,bl,c)) in
       LocalRawAssum (nal,bk,t) :: bl, c
@@ -536,21 +547,6 @@ end) = struct
                    (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) cofix),
           lfix
         )
-      | CProdN
-          (_,
-           [([(_,Name n)],_,_)],
-           CCases
-             (_,LetPatternStyle,None,[(CRef(Ident(_,m),None),None,None)],
-              [(_,[(_,[p])],a)]))
-          when
-            Id.equal m n &&
-            not (Id.Set.mem n (Topconstr.free_vars_of_constr_expr a)) ->
-        return (
-          hov 0 (
-            keyword "forall" ++ spc () ++ str "'" ++ pr_patt lsimplepatt p ++
-            str "," ++ pr spc ltop a),
-          llambda
-        )
       | CProdN _ ->
         let (bl,a) = extract_prod_binders a in
         return (
@@ -560,21 +556,6 @@ end) = struct
               str "," ++ pr spc ltop a),
           lprod
         )
-      | CLambdaN
-          (_,
-           [([(_,Name n)],_,_)],
-           CCases
-             (_,LetPatternStyle,None,[(CRef(Ident(_,m),None),None,None)],
-              [(_,[(_,[p])],a)]))
-          when
-            Id.equal m n &&
-            not (Id.Set.mem n (Topconstr.free_vars_of_constr_expr a)) ->
-        return (
-          hov 0 (
-            keyword "fun" ++ spc () ++ str "'" ++ pr_patt lsimplepatt p ++
-            pr_fun_sep ++ pr spc ltop a),
-          llambda
-        )
       | CLambdaN _ ->
         let (bl,a) = extract_lam_binders a in
         return (
-- 
cgit v1.2.3