diff options
| -rw-r--r-- | interp/constrextern.ml | 16 | ||||
| -rw-r--r-- | interp/notation.ml | 18 | ||||
| -rw-r--r-- | interp/notation.mli | 7 | ||||
| -rw-r--r-- | test-suite/output/Notations.out | 6 | ||||
| -rw-r--r-- | test-suite/output/Notations.v | 25 |
5 files changed, 58 insertions, 14 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/notation.ml b/interp/notation.ml index e282d62396..c4e9496b95 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 *) 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 diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 53ad8a9612..90a6a2ad96 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -80,6 +80,12 @@ NIL : list nat : Z * Z * (Z * Z) * (Z * Z) * (Z * bool * (Z * bool) * (Z * bool)) fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|} : Z : (Z -> Z -> Z -> Z) -> Z +{|fun x : Z => x + x; 0|} + : Z +{|op; 0; 1|} + : Z +false = 0 + : Prop Init.Nat.add : nat -> nat -> nat S diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index 7d2f1e9ba8..d0b2f40f9c 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -216,13 +216,32 @@ Check [|0*(1,2,3);(4,5,6)*false|]. (**********************************************************************) (* Test recursive notations involving applications *) -(* Caveat: does not work for applied constant because constants are *) -(* classified as notations for the particular constant while this *) -(* generic application notation is classified as generic *) + +Module Application. Notation "{| f ; x ; .. ; y |}" := ( .. (f x) .. y). + +(* Application to a variable *) + Check fun f => {| f; 0; 1; 2 |} : Z. +(* Application to a fun *) + +Check {| (fun x => x+x); 0 |}. + +(* Application to a reference *) + +Axiom op : Z -> Z -> Z. +Check {| op; 0; 1 |}. + +(* Interaction with coercion *) + +Axiom c : Z -> bool. +Coercion c : Z >-> bool. +Check false = {| c; 0 |}. + +End Application. + (**********************************************************************) (* Check printing of notations from other modules *) |