From 97aac6a7cf1bab3226f979b55e37d61f22c2f358 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 25 Dec 2019 11:35:14 +0100 Subject: Renaming confusingly-named insert_coercion into insert_entry_coercion. This is to avoid confusion with typing coercions. No change of semantics. --- interp/constrextern.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'interp') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 7a14ca3e48..0c29806774 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -282,9 +282,9 @@ let insert_pat_alias ?loc p = function | Anonymous -> p | Name _ as na -> CAst.make ?loc @@ CPatAlias (p,(CAst.make ?loc na)) -let rec insert_coercion ?loc l c = match l with +let rec insert_entry_coercion ?loc l c = match l with | [] -> c - | (inscope,ntn)::l -> CAst.make ?loc @@ CNotation (Some inscope,ntn,([insert_coercion ?loc l c],[],[],[])) + | (inscope,ntn)::l -> CAst.make ?loc @@ CNotation (Some inscope,ntn,([insert_entry_coercion ?loc l c],[],[],[])) let rec insert_pat_coercion ?loc l c = match l with | [] -> c @@ -849,7 +849,7 @@ let extern_possible_prim_token (custom,scopes) r = | Some coercion -> match availability_of_prim_token n sc scopes with | None -> raise No_match - | Some key -> insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key) + | Some key -> insert_entry_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key) let filter_enough_applied nargs l = match nargs with @@ -1081,7 +1081,7 @@ let rec extern inctx ?impargs scopes vars r = | GFloat f -> extern_float f (snd scopes) - in insert_coercion coercion (CAst.make ?loc c) + in insert_entry_coercion coercion (CAst.make ?loc c) and extern_typ ?impargs (subentry,(_,scopes)) = extern true ?impargs (subentry,(Notation.current_type_scope_name (),scopes)) @@ -1279,7 +1279,7 @@ and extern_notation (custom,scopes as allscopes) vars t rules = pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) vars bl)) binderlists in let c = make_notation loc specific_ntn (l,ll,bl,bll) in - let c = insert_coercion coercion (insert_delimiters c key) in + let c = insert_entry_coercion coercion (insert_delimiters c key) in let args = fill_arg_scopes args argsscopes allscopes in let args = extern_args (extern true) vars args in CAst.make ?loc @@ extern_applied_notation nallargs argsimpls c args) @@ -1296,7 +1296,7 @@ and extern_notation (custom,scopes as allscopes) vars t rules = let args = fill_arg_scopes args argsscopes allscopes in let args = extern_args (extern true) vars args in let c = CAst.make ?loc @@ extern_applied_syntactic_definition nallargs argsimpls (a,cf) l args in - insert_coercion coercion c + insert_entry_coercion coercion c with No_match -> extern_notation allscopes vars t rules -- cgit v1.2.3 From 9aefd708109658a8a17412e1fd7cc95bff454050 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 30 Dec 2019 17:18:33 +0100 Subject: If a custom entry has global, an argument-free abbreviation is valid in this entry. Parsing was automatically supporting this. This commit adds support for printing. Note: It would be more delicate to recognize that some given entry support applicative nodes hence abbreviations with arguments. --- interp/constrextern.ml | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) (limited to 'interp') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 0c29806774..0396e556cf 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -615,6 +615,10 @@ let is_projection nargs r = let is_hole = function CHole _ | CEvar _ -> true | _ -> false +let isCRef_no_univ = function + | CRef (_,None) -> true + | _ -> false + let is_significant_implicit a = not (is_hole (a.CAst.v)) @@ -1284,9 +1288,6 @@ and extern_notation (custom,scopes as allscopes) vars t rules = let args = extern_args (extern true) vars args in CAst.make ?loc @@ extern_applied_notation nallargs argsimpls c args) | SynDefRule kn -> - match availability_of_entry_coercion custom InConstrEntrySomeLevel with - | None -> raise No_match - | Some coercion -> let l = List.map (fun (c,(subentry,(scopt,scl))) -> extern true (subentry,(scopt,scl@snd scopes)) vars c) @@ -1296,7 +1297,10 @@ and extern_notation (custom,scopes as allscopes) vars t rules = let args = fill_arg_scopes args argsscopes allscopes in let args = extern_args (extern true) vars args in let c = CAst.make ?loc @@ extern_applied_syntactic_definition nallargs argsimpls (a,cf) l args in - insert_entry_coercion coercion c + if isCRef_no_univ c.CAst.v && entry_has_global custom then c + else match availability_of_entry_coercion custom InConstrEntrySomeLevel with + | None -> raise No_match + | Some coercion -> insert_entry_coercion coercion c with No_match -> extern_notation allscopes vars t rules -- cgit v1.2.3 From 33aaa5d64771c3644de4771338c371ce6b865647 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 8 Apr 2020 17:23:44 +0200 Subject: If a custom entry has global, a bound variable is valid in this entry. This is due to "global" being a syntactic notation, thus including ident. Parsing was automatically supporting this. This commit adds support for printing. --- interp/constrextern.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'interp') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 0396e556cf..a37bac3275 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -453,7 +453,8 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = with No_match -> let loc = pat.CAst.loc in match DAst.get pat with - | PatVar (Name id) when entry_has_ident custom -> CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id))) + | PatVar (Name id) when entry_has_global custom || entry_has_ident custom -> + CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id))) | pat -> match availability_of_entry_coercion custom InConstrEntrySomeLevel with | None -> raise No_match @@ -935,7 +936,8 @@ let rec extern inctx ?impargs scopes vars r = match DAst.get r with | GRef (ref,us) when entry_has_global (fst scopes) -> CAst.make ?loc (extern_ref vars ref us) - | GVar id when entry_has_ident (fst scopes) -> CAst.make ?loc (extern_var ?loc id) + | GVar id when entry_has_global (fst scopes) || entry_has_ident (fst scopes) -> + CAst.make ?loc (extern_var ?loc id) | c -> -- cgit v1.2.3