aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml16
-rw-r--r--interp/constrintern.ml9
-rw-r--r--interp/impargs.ml30
-rw-r--r--interp/notation.ml20
-rw-r--r--interp/notation.mli7
5 files changed, 45 insertions, 37 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 95df626d4c..3667757a2f 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -858,10 +858,17 @@ let extern_possible_prim_token (custom,scopes) r =
insert_entry_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
let filter_enough_applied nargs l =
+ (* This is to ensure that notations for coercions are used only when
+ the coercion is fully applied; not explicitly done yet, but we
+ could also expect that the notation is exactly talking about the
+ coercion *)
match nargs with
| None -> l
| Some nargs ->
- List.filter (fun (keyrule,pat,n as _rule) -> match n with Some n -> n > nargs | None -> false) l
+ List.filter (fun (keyrule,pat,n as _rule) ->
+ match n with
+ | AppBoundedNotation n -> n > nargs
+ | AppUnboundedNotation | NotAppNotation -> false) l
(* Helper function for safe and optimal printing of primitive tokens *)
(* such as those for Int63 *)
@@ -1247,7 +1254,7 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
[], [] in
(* Adjust to the number of arguments expected by the notation *)
let (t,args,argsscopes,argsimpls) = match n with
- | Some n when nallargs >= n ->
+ | AppBoundedNotation n when nallargs >= n ->
let args1, args2 = List.chop n args in
let args2scopes = try List.skipn n argsscopes with Failure _ -> [] in
let args2impls =
@@ -1257,12 +1264,13 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
[]
else try List.skipn n argsimpls with Failure _ -> [] in
DAst.make @@ GApp (f,args1), args2, args2scopes, args2impls
- | None ->
+ | AppUnboundedNotation -> t, [], [], []
+ | NotAppNotation ->
begin match DAst.get f with
| GRef (ref,us) -> f, args, argsscopes, argsimpls
| _ -> t, [], [], []
end
- | _ -> raise No_match in
+ | AppBoundedNotation _ -> raise No_match in
(* Try matching ... *)
let terms,termlists,binders,binderlists =
match_notation_constr !print_universes t pat in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 987aa63392..1d3b1bbb24 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1659,12 +1659,12 @@ let drop_notations_pattern looked_for genv =
| None -> DAst.make ?loc @@ RCPatAtom None
| Some (n, head, pl) ->
let pl =
- if get_asymmetric_patterns () then pl else
let pars = List.make n (CAst.make ?loc @@ CPatAtom None) in
- List.rev_append pars pl in
+ List.rev_append pars pl
+ in
let (_,argscs) = find_remaining_scopes [] pl head in
let pats = List.map2 (in_pat_sc scopes) argscs pl in
- DAst.make ?loc @@ RCPatCstr(head, [], pats)
+ DAst.make ?loc @@ RCPatCstr(head, pats, [])
end
| CPatCstr (head, None, pl) ->
begin
@@ -1724,8 +1724,7 @@ let drop_notations_pattern looked_for genv =
the domains of lambdas in the encoding of match in constr.
This check is here and not in the parser because it would require
duplicating the levels of the [pattern] rule. *)
- CErrors.user_err ?loc ~hdr:"drop_notations_pattern"
- (Pp.strbrk "Casts are not supported in this pattern.")
+ CErrors.user_err ?loc (Pp.strbrk "Casts are not supported in this pattern.")
and in_pat_sc scopes x = in_pat false (x,snd scopes)
and in_not top loc scopes (subst,substlist as fullsubst) args = function
| NVar id ->
diff --git a/interp/impargs.ml b/interp/impargs.ml
index db102470b0..48961c6c8a 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -20,7 +20,6 @@ open Lib
open Libobject
open EConstr
open Reductionops
-open Namegen
open Constrexpr
module NamedDecl = Context.Named.Declaration
@@ -247,24 +246,15 @@ let is_rigid env sigma t =
is_rigid_head sigma t
| _ -> true
-let find_displayed_name_in sigma all avoid na (env, b) =
- let envnames_b = (env, b) in
- let flag = RenamingElsewhereFor envnames_b in
- if all then compute_and_force_displayed_name_in sigma flag avoid na b
- else compute_displayed_name_in sigma flag avoid na b
-
-let compute_implicits_names_gen all env sigma t =
+let compute_implicits_names env sigma t =
let open Context.Rel.Declaration in
- let rec aux env avoid names t =
+ let rec aux env names t =
let t = whd_all env sigma t in
match kind sigma t with
| Prod (na,a,b) ->
- let na',avoid' = find_displayed_name_in sigma all avoid na.Context.binder_name (names,b) in
- aux (push_rel (LocalAssum (na,a)) env) avoid' (na'::names) b
+ aux (push_rel (LocalAssum (na,a)) env) (na.Context.binder_name::names) b
| _ -> List.rev names
- in aux env Id.Set.empty [] t
-
-let compute_implicits_names = compute_implicits_names_gen true
+ in aux env [] t
let compute_implicits_explanation_gen strict strongly_strict revpat contextual env sigma t =
let open Context.Rel.Declaration in
@@ -291,9 +281,9 @@ let compute_implicits_explanation_flags env sigma f t =
(f.strict || f.strongly_strict) f.strongly_strict
f.reversible_pattern f.contextual env sigma t
-let compute_implicits_flags env sigma f all t =
+let compute_implicits_flags env sigma f t =
List.combine
- (compute_implicits_names_gen all env sigma t)
+ (compute_implicits_names env sigma t)
(compute_implicits_explanation_flags env sigma f t)
let compute_auto_implicits env sigma flags enriching t =
@@ -361,10 +351,10 @@ let positions_of_implicits (_,impls) =
let rec prepare_implicits i f = function
| [] -> []
- | (Anonymous, Some _)::_ -> anomaly (Pp.str "Unnamed implicit.")
- | (Name id, Some imp)::imps ->
+ | (na, Some imp)::imps ->
let imps' = prepare_implicits (i+1) f imps in
- Some (ExplByName id,imp,(set_maximality Silent (Name id) i imps' f.maximal,true)) :: imps'
+ let expl = match na with Name id -> ExplByName id | Anonymous -> ExplByPos (i,None) in
+ Some (expl,imp,(set_maximality Silent na i imps' f.maximal,true)) :: imps'
| _::imps -> None :: prepare_implicits (i+1) f imps
let set_manual_implicits silent flags enriching autoimps l =
@@ -393,7 +383,7 @@ let set_manual_implicits silent flags enriching autoimps l =
let compute_semi_auto_implicits env sigma f t =
if not f.auto then [DefaultImpArgs, []]
- else let l = compute_implicits_flags env sigma f false t in
+ else let l = compute_implicits_flags env sigma f t in
[DefaultImpArgs, prepare_implicits 1 f l]
(*s Constants. *)
diff --git a/interp/notation.ml b/interp/notation.ml
index e282d62396..0bd5da5729 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -293,7 +293,12 @@ let key_compare k1 k2 = match k1, k2 with
module KeyOrd = struct type t = key let compare = key_compare end
module KeyMap = Map.Make(KeyOrd)
-type notation_rule = interp_rule * interpretation * int option
+type notation_applicative_status =
+ | AppBoundedNotation of int
+ | AppUnboundedNotation
+ | NotAppNotation
+
+type notation_rule = interp_rule * interpretation * notation_applicative_status
let keymap_add key interp map =
let old = try KeyMap.find key map with Not_found -> [] in
@@ -329,13 +334,14 @@ let cases_pattern_key c = match DAst.get c with
| _ -> Oth
let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
- | NApp (NRef ref,args) -> RefKey(canonical_gr ref), Some (List.length args)
+ | NApp (NRef ref,args) -> RefKey(canonical_gr ref), AppBoundedNotation (List.length args)
| NList (_,_,NApp (NRef ref,args),_,_)
| NBinderList (_,_,NApp (NRef ref,args),_,_) ->
- RefKey (canonical_gr ref), Some (List.length args)
- | NRef ref -> RefKey(canonical_gr ref), None
- | NApp (_,args) -> Oth, Some (List.length args)
- | _ -> Oth, None
+ RefKey (canonical_gr ref), AppBoundedNotation (List.length args)
+ | NRef ref -> RefKey(canonical_gr ref), NotAppNotation
+ | NApp (_,args) -> Oth, AppBoundedNotation (List.length args)
+ | NList (_,_,NApp (NVar x,_),_,_) when x = Notation_ops.ldots_var -> Oth, AppUnboundedNotation
+ | _ -> Oth, NotAppNotation
(** Dealing with precedences *)
@@ -1423,7 +1429,7 @@ let declare_entry_coercion (scope,(entry,key)) lev entry' =
let toaddright =
EntryCoercionMap.fold (fun (entry'',entry''') paths l ->
List.fold_right (fun ((lev'',lev'''),path) l ->
- if entry' = entry'' && level_ord lev' lev'' && entry <> entry'''
+ if entry' = entry'' && level_ord lev'' lev' && entry <> entry'''
then ((entry,entry'''),((lev,lev'''),path@[(scope,(entry,key))]))::l else l) paths l)
!entry_coercion_map [] in
entry_coercion_map :=
diff --git a/interp/notation.mli b/interp/notation.mli
index c39bfa6e28..05ddd25a62 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -239,7 +239,12 @@ val declare_uninterpretation : interp_rule -> interpretation -> unit
val interp_notation : ?loc:Loc.t -> notation -> subscopes ->
interpretation * (notation_location * scope_name option)
-type notation_rule = interp_rule * interpretation * int option
+type notation_applicative_status =
+ | AppBoundedNotation of int
+ | AppUnboundedNotation
+ | NotAppNotation
+
+type notation_rule = interp_rule * interpretation * notation_applicative_status
(** Return the possible notations for a given term *)
val uninterp_notations : 'a glob_constr_g -> notation_rule list
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 14:14:05 +0000