diff options
| -rw-r--r-- | doc/changelog/03-notations/11090-master+refactoring-application-printing.rst | 1 | ||||
| -rw-r--r-- | interp/constrextern.ml | 34 | ||||
| -rw-r--r-- | test-suite/output/Notations4.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations4.v | 14 |
4 files changed, 41 insertions, 10 deletions
diff --git a/doc/changelog/03-notations/11090-master+refactoring-application-printing.rst b/doc/changelog/03-notations/11090-master+refactoring-application-printing.rst new file mode 100644 index 0000000000..5c3936073a --- /dev/null +++ b/doc/changelog/03-notations/11090-master+refactoring-application-printing.rst @@ -0,0 +1 @@ +- Fixed #11033: regression in not printing coercions to which is also associated a notation (`#11090 <https://github.com/coq/coq/pull/11090>`_, by Hugo Herbelin). diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 0a1371413a..343bcbc059 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -721,15 +721,27 @@ 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 extern_possible extern r = - try Some (extern r) with No_match -> None - -let extern_optimal extern r r' = - let c = extern_possible extern r in - let c' = if r==r' then None else extern_possible extern r' in - match c,c' with - | Some n, (Some ({ CAst.v = CDelimiters _}) | None) | _, Some n -> n - | _ -> raise No_match +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 (* Helper function for safe and optimal printing of primitive tokens *) (* such as those for Int63 *) @@ -798,13 +810,15 @@ 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; - extern_optimal (extern_possible_prim_token scopes) r r' + 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'' with No_match -> let loc = r'.CAst.loc in diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index ba4ac5a8f9..32120a9674 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -59,3 +59,5 @@ where |- Type] (pat, p0, p cannot be used) fun '{| |} => true : R -> bool +b = a + : Prop diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 4b9d0abd95..d3433949d1 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -140,3 +140,17 @@ Record R := { n : nat }. Check fun '{|n:=x|} => true. End EmptyRecordSyntax. + +Module L. + +(* Testing regression #11053 *) + +Section Test. +Variables (A B : Type) (a : A) (b : B). +Variable c : A -> B. +Coercion c : A >-> B. +Notation COERCION := (c). +Check b = a. +End Test. + +End L. |