From 6e1f26a075a48fb32bce32e07d6b58e2f38b97a5 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 12 Aug 2017 14:23:11 +0200 Subject: More precise explanation when a notation is not reversible for printing. --- interp/notation_ops.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp/notation_ops.mli') diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 0904a4ea3e..80348c78ee 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -29,7 +29,7 @@ val ldots_var : Id.t bound by the notation; also interpret recursive patterns *) val notation_constr_of_glob_constr : notation_interp_env -> - glob_constr -> notation_constr * reversibility_flag + glob_constr -> notation_constr * reversibility_status (** Re-interpret a notation as a [glob_constr], taking care of binders *) -- cgit v1.2.3 From 398358618bb3eabfe822b79c669703c1c33b67e6 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 15 Aug 2017 18:32:02 +0200 Subject: Adding patterns in the category of binders for notations. For instance, the following is now possible: Check {(x,y)|x+y=0}. Some questions remains. Maybe, by consistency, the notation should be "{'(x,y)|x+y=0}"... --- interp/notation_ops.mli | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'interp/notation_ops.mli') diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 80348c78ee..74be6f5120 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -33,8 +33,11 @@ val notation_constr_of_glob_constr : notation_interp_env -> (** Re-interpret a notation as a [glob_constr], taking care of binders *) +val apply_cases_pattern : ?loc:Loc.t -> + (Id.t list * cases_pattern) * Id.t -> glob_constr -> glob_constr + val glob_constr_of_notation_constr_with_binders : ?loc:Loc.t -> - ('a -> Name.t -> 'a * Name.t) -> + ('a -> Name.t -> 'a * ((Id.t list * cases_pattern) * Id.t) option * Name.t) -> ('a -> notation_constr -> glob_constr) -> 'a -> notation_constr -> glob_constr -- cgit v1.2.3 From edd0d22429354a5f2c703a8c7bd1f775e2f97d9e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 12 Aug 2017 09:15:40 +0200 Subject: Adding support for parsing subterms of a notation as "pattern". This allows in particular to define notations with 'pat style binders. E.g.: A non-trivial change in this commit is storing binders and patterns separately from terms. This is not strictly necessary but has some advantages. However, it is relatively common to have binders also used as terms, or binders parsed as terms. Thus, it is already relatively common to embed binders into terms (see e.g. notation for ETA in output test Notations3.v) or to coerce terms to idents (see e.g. the notation for {x|P} where x is parsed as a constr). So, it is as simple to always store idents (and eventually patterns) as terms. --- interp/notation_ops.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'interp/notation_ops.mli') diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 74be6f5120..1a2dfc9cac 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -52,6 +52,7 @@ exception No_match val match_notation_constr : bool -> 'a glob_constr_g -> interpretation -> ('a glob_constr_g * subscopes) list * ('a glob_constr_g list * subscopes) list * + ('a cases_pattern_g * subscopes) list * ('a extended_glob_local_binder_g list * subscopes) list val match_notation_constr_cases_pattern : -- cgit v1.2.3 From e4d93d1cef27d3a8c1e36139fc1e118730406f67 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 17 Aug 2017 20:12:55 +0200 Subject: Adding general support for irrefutable disjunctive patterns. This now works not only for parsing of fun/forall (as in 8.6), but also for arbitraty notations with binders and for printing. --- interp/notation_ops.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'interp/notation_ops.mli') diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 1a2dfc9cac..746f52e485 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -34,10 +34,10 @@ val notation_constr_of_glob_constr : notation_interp_env -> (** Re-interpret a notation as a [glob_constr], taking care of binders *) val apply_cases_pattern : ?loc:Loc.t -> - (Id.t list * cases_pattern) * Id.t -> glob_constr -> glob_constr + (Id.t list * cases_pattern_disjunction) * Id.t -> glob_constr -> glob_constr val glob_constr_of_notation_constr_with_binders : ?loc:Loc.t -> - ('a -> Name.t -> 'a * ((Id.t list * cases_pattern) * Id.t) option * Name.t) -> + ('a -> Name.t -> 'a * ((Id.t list * cases_pattern_disjunction) * Id.t) option * Name.t) -> ('a -> notation_constr -> glob_constr) -> 'a -> notation_constr -> glob_constr @@ -52,7 +52,7 @@ exception No_match val match_notation_constr : bool -> 'a glob_constr_g -> interpretation -> ('a glob_constr_g * subscopes) list * ('a glob_constr_g list * subscopes) list * - ('a cases_pattern_g * subscopes) list * + ('a cases_pattern_disjunction_g * subscopes) list * ('a extended_glob_local_binder_g list * subscopes) list val match_notation_constr_cases_pattern : -- cgit v1.2.3