From 38c47ac0626fed51d17bc7513d7dbbd63053016e Mon Sep 17 00:00:00 2001 From: Abhishek Anand (optiplex7010@home) Date: Thu, 20 Feb 2020 19:52:39 -0800 Subject: added the new option --- interp/constrextern.ml | 4 ++++ interp/constrextern.mli | 1 + 2 files changed, 5 insertions(+) (limited to 'interp') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 38dc10a9b3..a5e7b89ded 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -57,6 +57,10 @@ let print_implicits_defensive = ref true (* This forces printing of coercions *) let print_coercions = ref false +(* This forces printing of parentheses even when + it is implied by associativity/precedence *) +let print_parens = ref false + (* This forces printing universe names of Type{.} *) let print_universes = Detyping.print_universes diff --git a/interp/constrextern.mli b/interp/constrextern.mli index fa263cbeb7..2691d27f69 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -53,6 +53,7 @@ val print_implicits_defensive : bool ref val print_arguments : bool ref val print_evar_arguments : bool ref val print_coercions : bool ref +val print_parens : bool ref val print_universes : bool ref val print_no_symbol : bool ref val print_projections : bool ref -- cgit v1.2.3 From 5820b274acda8be0372471758842b0ea2b950d41 Mon Sep 17 00:00:00 2001 From: Abhishek Anand (optiplex7010@home) Date: Sat, 22 Feb 2020 13:22:27 -0800 Subject: parens --> parentheses --- interp/constrextern.ml | 2 +- interp/constrextern.mli | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'interp') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index a5e7b89ded..bdfb63add3 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -59,7 +59,7 @@ let print_coercions = ref false (* This forces printing of parentheses even when it is implied by associativity/precedence *) -let print_parens = ref false +let print_parentheses = ref false (* This forces printing universe names of Type{.} *) let print_universes = Detyping.print_universes diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 2691d27f69..0eca287c1d 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -53,7 +53,7 @@ val print_implicits_defensive : bool ref val print_arguments : bool ref val print_evar_arguments : bool ref val print_coercions : bool ref -val print_parens : bool ref +val print_parentheses : bool ref val print_universes : bool ref val print_no_symbol : bool ref val print_projections : bool ref -- cgit v1.2.3 From 61f2f55a08dcef612c538ec7e6d0864d86fe3e0a Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 23 Feb 2020 17:09:21 +0100 Subject: Not iterating recursive notations more than once. --- interp/constrextern.ml | 2 +- interp/notation_ops.ml | 3 +++ interp/notation_ops.mli | 2 ++ 3 files changed, 6 insertions(+), 1 deletion(-) (limited to 'interp') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index bdfb63add3..3a0c6648cf 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -59,7 +59,7 @@ let print_coercions = ref false (* This forces printing of parentheses even when it is implied by associativity/precedence *) -let print_parentheses = ref false +let print_parentheses = Notation_ops.print_parentheses (* This forces printing universe names of Type{.} *) let print_universes = Detyping.print_universes diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index d1eb50d370..9f052278ad 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -258,6 +258,8 @@ let glob_constr_of_notation_constr ?loc x = (******************************************************************************) (* Translating a glob_constr into a notation, interpreting recursive patterns *) +let print_parentheses = ref false + type found_variables = { vars : Id.t list; recursive_term_vars : (Id.t * Id.t) list; @@ -1092,6 +1094,7 @@ let match_termlist match_fun alp metas sigma rest x y iter termin revert = let rest = Id.List.assoc ldots_var terms in let t = Id.List.assoc y terms in let sigma = remove_sigma y (remove_sigma ldots_var sigma) in + if !print_parentheses && not (List.is_empty acc) then raise No_match; aux sigma (t::acc) rest with No_match when not (List.is_empty acc) -> acc, match_fun metas sigma rest termin in diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index c62dac013b..d235f87580 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -61,6 +61,8 @@ val glob_constr_of_notation_constr : ?loc:Loc.t -> notation_constr -> glob_const exception No_match +val print_parentheses : bool ref + val match_notation_constr : bool -> 'a glob_constr_g -> interpretation -> ('a glob_constr_g * extended_subscopes) list * ('a glob_constr_g list * extended_subscopes) list * ('a cases_pattern_disjunction_g * extended_subscopes) list * -- cgit v1.2.3