diff options
Diffstat (limited to 'kernel/constr.ml')
-rw-r--r-- | kernel/constr.ml | 17 |
1 files changed, 11 insertions, 6 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 |