diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-20 12:56:43 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-20 23:29:19 +0200 |
| commit | 7efeff178470ab204e531cd07176091bf5022da6 (patch) | |
| tree | afdc79d6eb2a371fa2cec235aabea3c5425d46b9 /kernel/constr.ml | |
| parent | f00f8482e1d21ef8b03044ed2162cb29d9e4537d (diff) | |
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.
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 |