A patch for printing "match" when constructors are defined with let-in

but the internal representation dropped let-in.

Ideally, the internal representation of the "match" should use
contexts for the predicate and the branches. This would however be a
rather significant change. In the meantime, just a hack.

To do, there is still an extra @ in the constructor name that does not
need to be there.

8 files changed, 27 insertions, 11 deletions

diff --git a/kernel/constr.ml b/kernel/constr.ml
index 912067629..f688cca45 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -38,7 +38,8 @@ type cast_kind = VMcast | NATIVEcast | DEFAULTcast | REVERTcast
 (* This defines Cases annotations *)
 type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
 type case_printing =
-  { ind_nargs : int; (* length of the arity of the inductive type *)
+  { ind_tags : bool list; (** tell whether letin or lambda in the arity of the inductive type *)
+    cstr_tags : bool list array; (* whether each pattern var of each constructor is a let-in (true) or not (false) *)
     style     : case_style }
 type case_info =
   { ci_ind        : inductive;
@@ -933,7 +934,8 @@ struct
   type u = inductive -> inductive
   let hashcons hind ci = { ci with ci_ind = hind ci.ci_ind }
   let pp_info_equal info1 info2 =
-    Int.equal info1.ind_nargs info2.ind_nargs &&
+    List.equal (==) info1.ind_tags info2.ind_tags &&
+    Array.equal (List.equal (==)) info1.cstr_tags info2.cstr_tags &&
     info1.style == info2.style
   let equal ci ci' =
     ci.ci_ind == ci'.ci_ind &&
@@ -942,15 +944,18 @@ struct
     Array.equal Int.equal ci.ci_cstr_nargs ci'.ci_cstr_nargs && (* we use [Array.equal] on purpose *)
     pp_info_equal ci.ci_pp_info ci'.ci_pp_info  (* we use (=) on purpose *)
   open Hashset.Combine
+  let hash_bool b = if b then 0 else 1
+  let hash_bool_list = List.fold_left (fun n b -> combine n (hash_bool b))
   let hash_pp_info info =
-    let h = match info.style with
+    let h1 = match info.style with
     | LetStyle -> 0
     | IfStyle -> 1
     | LetPatternStyle -> 2
     | MatchStyle -> 3
-    | RegularStyle -> 4
-    in
-    combine info.ind_nargs h
+    | RegularStyle -> 4 in
+    let h2 = hash_bool_list 0 info.ind_tags in
+    let h3 = Array.fold_left hash_bool_list 0 info.cstr_tags in
+    combine3 h1 h2 h3
   let hash ci =
     let h1 = ind_hash ci.ci_ind in
     let h2 = Int.hash ci.ci_npar in
diff --git a/kernel/constr.mli b/kernel/constr.mli
index da7ac6a0d..1e23911dd 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -26,7 +26,8 @@ type metavariable = int
 type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle 
   | RegularStyle (** infer printing form from number of constructor *)
 type case_printing =
-  { ind_nargs : int; (** length of the arity of the inductive type *)
+  { ind_tags : bool list; (** tell whether letin or lambda in the arity of the inductive type *)
+    cstr_tags : bool list array; (** tell whether letin or lambda in the signature of each constructor *)
     style     : case_style }
 
 (** the integer is the number of real args, needed for reduction *)
diff --git a/kernel/context.ml b/kernel/context.ml
index 5256ee417..5cb964b9c 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -76,6 +76,13 @@ let rel_context_nhyps hyps =
     | (_,Some _,_)::hyps -> nhyps acc hyps in
   nhyps 0 hyps
 
+let rel_context_tags ctx =
+  let rec aux l = function
+  | [] -> l
+  | (_,Some _,_)::ctx -> aux (true::l) ctx
+  | (_,None _,_)::ctx -> aux (false::l) ctx
+  in aux [] ctx
+
 (*s Signatures of named hypotheses. Used for section variables and
     goal assumptions. *)
 
diff --git a/kernel/context.mli b/kernel/context.mli
index 1d732d273..b7eb7a76a 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -115,3 +115,5 @@ val lookup_rel : int -> rel_context -> rel_declaration
 val rel_context_length : rel_context -> int
 (** Size of the [rel_context] without LetIns *)
 val rel_context_nhyps : rel_context -> int
+(** Indicates whether a LetIn or a Lambda, starting from oldest declaration *)
+val rel_context_tags : rel_context -> bool list
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 39455a7d2..45e0261d3 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -666,7 +666,8 @@ let compute_projections ((kn, _ as ind), u as indsp) n x nparamargs params
   let mp, dp, l = repr_mind kn in
   let rp = mkApp (mkIndU indsp, rel_vect 0 nparamargs) in
   let ci = 
-    let print_info = { ind_nargs = 0; style = LetStyle } in
+    let print_info =
+      { ind_tags = []; cstr_tags = [|rel_context_tags ctx|]; style = LetStyle } in
       { ci_ind     = ind;
 	ci_npar    = nparamargs;
 	ci_cstr_ndecls = mind_consnrealdecls;
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 041751ecf..c8a4fa897 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1807,7 +1807,7 @@ let compile_constant env sigma prefix ~interactive con cb =
       let ci = { ci_ind = ind; ci_npar = mib.mind_nparams; 
 		 ci_cstr_nargs = [|0|];
 		 ci_cstr_ndecls = [||] (*FIXME*);
-		 ci_pp_info = { ind_nargs = 0; style = RegularStyle } } in
+		 ci_pp_info = { ind_tags = []; cstr_tags = [||] (*FIXME*); style = RegularStyle } } in
       let asw = { asw_ind = ind; asw_prefix = prefix; asw_ci = ci;
 		  asw_reloc = tbl; asw_finite = true } in
       let c_uid = fresh_lname Anonymous in
diff --git a/kernel/term.ml b/kernel/term.ml
index 734b7853f..3adfa5e37 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -40,7 +40,7 @@ type case_style = Constr.case_style =
   LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
 
 type case_printing = Constr.case_printing =
-  { ind_nargs : int; style     : case_style }
+  { ind_tags : bool list; cstr_tags : bool list array; style : case_style }
 
 type case_info = Constr.case_info =
   { ci_ind        : inductive;
diff --git a/kernel/term.mli b/kernel/term.mli
index 50cd433e9..c5e85b1e5 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -47,7 +47,7 @@ type case_style = Constr.case_style =
   LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
 
 type case_printing = Constr.case_printing =
-  { ind_nargs : int; style     : case_style }
+  { ind_tags : bool list; cstr_tags : bool list array; style : case_style }
 
 type case_info = Constr.case_info =
   { ci_ind        : inductive;