From 7efeff178470ab204e531cd07176091bf5022da6 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 20 Oct 2014 12:56:43 +0200 Subject: 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. --- kernel/constr.ml | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) (limited to 'kernel/constr.ml') 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 -- cgit v1.2.3