aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst1
-rw-r--r--interp/constrextern.ml82
-rw-r--r--interp/constrextern.mli2
-rw-r--r--interp/notation_ops.ml2
-rw-r--r--pretyping/glob_ops.ml6
-rw-r--r--pretyping/glob_ops.mli4
-rw-r--r--pretyping/patternops.mli1
-rw-r--r--test-suite/output/Notations4.out2
-rw-r--r--test-suite/output/Notations4.v4
9 files changed, 49 insertions, 55 deletions
diff --git a/doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst b/doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst
new file mode 100644
index 0000000000..5f279fc9ba
--- /dev/null
+++ b/doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst
@@ -0,0 +1 @@
+- In printing, now interleave search for notations and removal of coercions (`#11172 <https://github.com/coq/coq/pull/11172>`_, by Hugo Herbelin).
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index c85f4f2cf7..a31dddbbd5 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -674,17 +674,15 @@ let match_coercion_app c = match DAst.get c with
end
| _ -> None
-let rec remove_coercions inctx c =
- match match_coercion_app c with
+let remove_one_coercion inctx c =
+ try match match_coercion_app c with
| Some (loc,r,pars,args) when not (!Flags.raw_print || !print_coercions) ->
let nargs = List.length args in
- (try match Classops.hide_coercion r with
+ (match Classops.hide_coercion r with
| Some n when (n - pars) < nargs && (inctx || (n - pars)+1 < nargs) ->
- (* We skip a coercion *)
+ (* We skip the coercion *)
let l = List.skipn (n - pars) args in
let (a,l) = match l with a::l -> (a,l) | [] -> assert false in
- (* Recursively remove the head coercions *)
- let a' = remove_coercions true a in
(* Don't flatten App's in case of funclass so that
(atomic) notations on [a] work; should be compatible
since printer does not care whether App's are
@@ -693,10 +691,13 @@ let rec remove_coercions inctx c =
been confused with ordinary application or would have need
a surrounding context and the coercion to funclass would
have been made explicit to match *)
- if List.is_empty l then a' else DAst.make ?loc @@ GApp (a',l)
- | _ -> c
- with Not_found -> c)
- | _ -> c
+ let a' = if List.is_empty l then a else DAst.make ?loc @@ GApp (a,l) in
+ let inctx = inctx || not (List.is_empty l) in
+ Some (n-pars+1, inctx, a')
+ | _ -> None)
+ | _ -> None
+ with Not_found ->
+ None
let rec flatten_application c = match DAst.get c with
| GApp (f, l) ->
@@ -721,27 +722,11 @@ let extern_possible_prim_token (custom,scopes) r =
| None -> raise No_match
| Some key -> insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
-let filter_fully_applied r l =
- let nargs = match DAst.get r with
- | GApp (f,args) -> List.length args
- | _ -> assert false in
- List.filter (fun (keyrule,pat,n as _rule) -> n = Some nargs) l
-
-let extern_optimal extern extern_fully_applied r r' =
- if r==r' then
- (* No coercion: we look for a notation for r or a partial application of it *)
- extern r
- else
- (* A coercion is removed: we prefer in order:
- - a notation w/o a delimiter for the expression w/o coercions (or a partial application of it), if any
- - a notation for the fully-applied expression with coercions, if any
- - a notation with a delimiter for the expression w/o coercions (or a partial applied of it), if any *)
- try
- let c' = extern r' in
- match c' with
- | { CAst.v = CDelimiters _} -> (try extern_fully_applied r with No_match -> c')
- | _ -> c'
- with No_match -> extern_fully_applied r
+let filter_enough_applied nargs l =
+ 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
(* Helper function for safe and optimal printing of primitive tokens *)
(* such as those for Int63 *)
@@ -807,22 +792,17 @@ let extern_ref vars ref us =
let extern_var ?loc id = CRef (qualid_of_ident ?loc id,None)
let rec extern inctx scopes vars r =
- let r' = remove_coercions inctx r in
- try
- if !Flags.raw_print || !print_no_symbol then raise No_match;
- let extern_fun = extern_possible_prim_token scopes in
- extern_optimal extern_fun extern_fun r r'
- with No_match ->
- try
- let r'' = flatten_application r' in
- if !Flags.raw_print || !print_no_symbol then raise No_match;
- extern_optimal
- (fun r -> extern_notation scopes vars r (uninterp_notations r))
- (fun r -> extern_notation scopes vars r (filter_fully_applied r (uninterp_notations r)))
- r r''
+ match remove_one_coercion inctx (flatten_application r) with
+ | Some (nargs,inctx,r') ->
+ (try extern_notations scopes vars (Some nargs) r
+ with No_match -> extern inctx scopes vars r')
+ | None ->
+
+ try extern_notations scopes vars None r
with No_match ->
- let loc = r'.CAst.loc in
- match DAst.get r' with
+
+ let loc = r.CAst.loc in
+ 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)
@@ -1110,7 +1090,15 @@ and extern_eqn inctx scopes vars {CAst.loc;v=(ids,pll,c)} =
let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in
make ?loc (pll,extern inctx scopes vars c)
-and extern_notation (custom,scopes as allscopes) vars t = function
+and extern_notations scopes vars nargs t =
+ if !Flags.raw_print || !print_no_symbol then raise No_match;
+ try extern_possible_prim_token scopes t
+ with No_match ->
+ let t = flatten_application t in
+ extern_notation scopes vars t (filter_enough_applied nargs (uninterp_notations t))
+
+and extern_notation (custom,scopes as allscopes) vars t rules =
+ match rules with
| [] -> raise No_match
| (keyrule,pat,n as _rule)::rules ->
let loc = Glob_ops.loc_of_glob_constr t in
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index e22dd2be86..aa6aa5f5f9 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -92,5 +92,3 @@ val toggle_scope_printing :
val toggle_notation_printing :
?scope:Notation_term.scope_name -> notation:Constrexpr.notation -> activate:bool -> unit
-
-
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index ff2498386d..265ca58ed9 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1225,7 +1225,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
bind_bindinglist_env alp sigma id [DAst.make @@ GLocalAssum (Name id',Explicit,t1)]
else
match_names metas (alp,sigma) (Name id') na in
- match_in u alp metas sigma (mkGApp a1 (DAst.make @@ GVar id')) b2
+ match_in u alp metas sigma (mkGApp a1 [DAst.make @@ GVar id']) b2
| (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _
| GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 1264b0b33c..02c2fc4a13 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -34,10 +34,10 @@ let cases_predicate_names tml =
| (tm,(na,None)) -> [na]
| (tm,(na,Some {v=(_,nal)})) -> na::nal) tml)
-let mkGApp ?loc p t = DAst.make ?loc @@
+let mkGApp ?loc p l = DAst.make ?loc @@
match DAst.get p with
- | GApp (f,l) -> GApp (f,l@[t])
- | _ -> GApp (p,[t])
+ | GApp (f,l') -> GApp (f,l'@l)
+ | _ -> GApp (p,l)
let map_glob_decl_left_to_right f (na,k,obd,ty) =
let comp1 = Option.map f obd in
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 37aa31d094..20ac35888e 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -42,8 +42,8 @@ val cases_pattern_loc : 'a cases_pattern_g -> Loc.t option
val cases_predicate_names : 'a tomatch_tuples_g -> Name.t list
-(** Apply one argument to a glob_constr *)
-val mkGApp : ?loc:Loc.t -> 'a glob_constr_g -> 'a glob_constr_g -> 'a glob_constr_g
+(** Apply a list of arguments to a glob_constr *)
+val mkGApp : ?loc:Loc.t -> 'a glob_constr_g -> 'a glob_constr_g list -> 'a glob_constr_g
val map_glob_constr :
(glob_constr -> glob_constr) -> glob_constr -> glob_constr
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index 304e06818e..342891d65f 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -37,6 +37,7 @@ val head_pattern_bound : constr_pattern -> GlobRef.t
returns its label; raises an anomaly otherwise *)
val head_of_constr_reference : Evd.evar_map -> constr -> GlobRef.t
+[@@ocaml.deprecated "use [EConstr.destRef]"]
(** [pattern_of_constr c] translates a term [c] with metavariables into
a pattern; currently, no destructor (Cases, Fix, Cofix) and no
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 32120a9674..799d310fa7 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -31,6 +31,8 @@ Let "x" e1 e2
: expr
Let "x" e1 e2
: expr
+Let "x" e1 e2 : list string
+ : list string
myAnd1 True True
: Prop
r 2 3
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index d3433949d1..26c7840a16 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -94,6 +94,10 @@ Coercion App : expr >-> Funclass.
Check (Let "x" e1 e2).
+Axiom free_vars :> expr -> list string.
+
+Check (Let "x" e1 e2) : list string.
+
End D.
(* Fixing bugs reported by G. Gonthier in #9207 *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:25:37 +0000