diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-15 14:51:08 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-12-12 13:30:57 +0100 |
commit | 5c9d569cee804c099c44286777ab084e0370399f (patch) | |
tree | 11bd5f12337af5fa823db5c6283b317f391def67 /interp | |
parent | c1cab3ba606f7034f2785f06c0d3892bca3976cf (diff) |
In printing, factorizing "match" clauses with same right-hand side.
Moreover, when there are at least two clauses and the last most
factorizable one is a disjunction with no variables, turn it into a
catch-all clause.
Adding options
Unset Printing Allow Default Clause.
to deactivate the second behavior, and
Unset Printing Factorizable Match Patterns.
to deactivate the first behavior (deactivating the first one
deactivates also the second one).
E.g. printing
match x with Eq => 1 | _ => 0 end
gives
match x with
| Eq => 1
| _ => 0
end
or (with default clause deactivates):
match x with
| Eq => 1
| Lt | Gt => 0
end
More to be done, e.g. reconstructing multiple patterns in Nat.eqb...
Diffstat (limited to 'interp')
-rw-r--r-- | interp/constrextern.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 6704ed4b7..1330b3741 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -852,7 +852,7 @@ let rec extern inctx scopes vars r = ) x)) tml in - let eqns = List.map (extern_eqn inctx scopes vars) eqns in + let eqns = List.map (extern_eqn inctx scopes vars) (factorize_eqns eqns) in CCases (sty,rtntypopt',tml,eqns) | GLetTuple (nal,(na,typopt),tm,b) -> @@ -966,9 +966,9 @@ and extern_local_binder scopes vars = function let (assums,ids,l) = extern_local_binder scopes vars l in (assums,ids, CLocalPattern(Loc.tag @@ (p,ty)) :: l) -and extern_eqn inctx scopes vars (loc,(ids,pl,c)) = - Loc.tag ?loc ([List.map (extern_cases_pattern_in_scope scopes vars) pl], - extern inctx scopes vars c) +and extern_eqn inctx scopes vars (loc,(ids,pll,c)) = + let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in + Loc.tag ?loc (pll,extern inctx scopes vars c) and extern_notation (tmp_scope,scopes as allscopes) vars t = function | [] -> raise No_match |