diff options
| -rw-r--r-- | interp/notation.ml | 129 | ||||
| -rw-r--r-- | interp/notation.mli | 6 | ||||
| -rw-r--r-- | test-suite/output/locate.out | 6 | ||||
| -rw-r--r-- | test-suite/output/locate.v | 23 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 74 |
5 files changed, 153 insertions, 85 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 8d05fab63c..948ebe9640 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -2035,12 +2035,12 @@ type symbol = | Break of int let rec symbol_eq s1 s2 = match s1, s2 with -| Terminal s1, Terminal s2 -> String.equal s1 s2 -| NonTerminal id1, NonTerminal id2 -> Id.equal id1 id2 -| SProdList (id1, l1), SProdList (id2, l2) -> - Id.equal id1 id2 && List.equal symbol_eq l1 l2 -| Break i1, Break i2 -> Int.equal i1 i2 -| _ -> false + | Terminal s1, Terminal s2 -> String.equal s1 s2 + | NonTerminal id1, NonTerminal id2 -> Id.equal id1 id2 + | SProdList (id1, l1), SProdList (id2, l2) -> + Id.equal id1 id2 && List.equal symbol_eq l1 l2 + | Break i1, Break i2 -> Int.equal i1 i2 + | _ -> false let rec string_of_symbol = function | NonTerminal _ -> ["_"] @@ -2202,23 +2202,114 @@ let rec raw_analyze_notation_tokens = function | WhiteSpace n :: sl -> Break n :: raw_analyze_notation_tokens sl -let decompose_raw_notation ntn = raw_analyze_notation_tokens (split_notation_string ntn) - -let possible_notations ntn = +let rec raw_analyze_anonymous_notation_tokens = function + | [] -> [] + | String ".." :: sl -> NonTerminal Notation_ops.ldots_var :: raw_analyze_anonymous_notation_tokens sl + | String "_" :: sl -> NonTerminal (Id.of_string "dummy") :: raw_analyze_anonymous_notation_tokens sl + | String s :: sl -> + Terminal (String.drop_simple_quotes s) :: raw_analyze_anonymous_notation_tokens sl + | WhiteSpace n :: sl -> raw_analyze_anonymous_notation_tokens sl + +(* Interpret notations with a recursive component *) + +let out_nt = function NonTerminal x -> x | _ -> assert false + +let msg_expected_form_of_recursive_notation = + "In the notation, the special symbol \"..\" must occur in\na configuration of the form \"x symbs .. symbs y\"." + +let rec find_pattern nt xl = function + | Break n as x :: l, Break n' :: l' when Int.equal n n' -> + find_pattern nt (x::xl) (l,l') + | Terminal s as x :: l, Terminal s' :: l' when String.equal s s' -> + find_pattern nt (x::xl) (l,l') + | [], NonTerminal x' :: l' -> + (out_nt nt,x',List.rev xl),l' + | _, Break s :: _ | Break s :: _, _ -> + user_err Pp.(str ("A break occurs on one side of \"..\" but not on the other side.")) + | _, Terminal s :: _ | Terminal s :: _, _ -> + user_err ~hdr:"Metasyntax.find_pattern" + (str "The token \"" ++ str s ++ str "\" occurs on one side of \"..\" but not on the other side.") + | _, [] -> + user_err Pp.(str msg_expected_form_of_recursive_notation) + | ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) -> + anomaly (Pp.str "Only Terminal or Break expected on left, non-SProdList on right.") + +let rec interp_list_parser hd = function + | [] -> [], List.rev hd + | NonTerminal id :: tl when Id.equal id Notation_ops.ldots_var -> + if List.is_empty hd then user_err Pp.(str msg_expected_form_of_recursive_notation); + let hd = List.rev hd in + let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in + let xyl,tl'' = interp_list_parser [] tl' in + (* We remember each pair of variable denoting a recursive part to *) + (* remove the second copy of it afterwards *) + (x,y)::xyl, SProdList (x,sl) :: tl'' + | (Terminal _ | Break _) as s :: tl -> + if List.is_empty hd then + let yl,tl' = interp_list_parser [] tl in + yl, s :: tl' + else + interp_list_parser (s::hd) tl + | NonTerminal _ as x :: tl -> + let xyl,tl' = interp_list_parser [x] tl in + xyl, List.rev_append hd tl' + | SProdList _ :: _ -> anomaly (Pp.str "Unexpected SProdList in interp_list_parser.") + +let get_notation_vars l = + List.map_filter (function NonTerminal id | SProdList (id,_) -> Some id | _ -> None) l + +let decompose_raw_notation ntn = + let l = split_notation_string ntn in + let l = raw_analyze_notation_tokens l in + let recvars,l = interp_list_parser [] l in + let vars = get_notation_vars l in + recvars, vars, l + +let interpret_notation_string ntn = (* We collect the possible interpretations of a notation string depending on whether it is in "x 'U' y" or "_ U _" format *) let toks = split_notation_string ntn in - if List.exists (function String "_" -> true | _ -> false) toks then - (* Only "_ U _" format *) - [ntn] - else - let _,ntn' = make_notation_key None (raw_analyze_notation_tokens toks) in - if String.equal ntn ntn' then (* Only symbols *) [ntn] else [ntn;ntn'] + let toks = + if + List.exists (function String "_" -> true | _ -> false) toks || + List.for_all (function String id -> Id.is_valid id | _ -> false) toks + then + (* Only "_ U _" format *) + raw_analyze_anonymous_notation_tokens toks + else + (* Includes the case of only a subset of tokens or an "x 'U' y"-style format *) + raw_analyze_notation_tokens toks + in + let _,toks = interp_list_parser [] toks in + let _,ntn' = make_notation_key None toks in + ntn' + +(* Tell if a non-recursive notation is an instance of a recursive one *) +let is_approximation ntn ntn' = + let rec aux toks1 toks2 = match (toks1, toks2) with + | Terminal s1 :: toks1, Terminal s2 :: toks2 -> String.equal s1 s2 && aux toks1 toks2 + | NonTerminal _ :: toks1, NonTerminal _ :: toks2 -> aux toks1 toks2 + | SProdList (_,l1) :: toks1, SProdList (_, l2) :: toks2 -> aux l1 l2 && aux toks1 toks2 + | NonTerminal _ :: toks1, SProdList (_,l2) :: toks2 -> aux' toks1 l2 l2 toks2 || aux toks1 toks2 + | [], [] -> true + | (Break _ :: _, _) | (_, Break _ :: _) -> assert false + | (Terminal _ | NonTerminal _ | SProdList _) :: _, _ -> false + | [], _ -> false + and aux' toks1 l2 l2full toks2 = match (toks1, l2) with + | Terminal s1 :: toks1, Terminal s2 :: l2 when String.equal s1 s2 -> aux' toks1 l2 l2full toks2 + | NonTerminal _ :: toks1, [] -> aux' toks1 l2full l2full toks2 || aux toks1 toks2 + | _ -> false + in + let _,toks = interp_list_parser [] (raw_analyze_anonymous_notation_tokens (split_notation_string ntn)) in + let _,toks' = interp_list_parser [] (raw_analyze_anonymous_notation_tokens (split_notation_string ntn')) in + aux toks toks' let browse_notation strict ntn map = - let ntns = possible_notations ntn in - let find (from,ntn' as fullntn') ntn = - if String.contains ntn ' ' then String.equal ntn ntn' + let ntn = interpret_notation_string ntn in + let find (from,ntn' as fullntn') = + if String.contains ntn ' ' then + if String.string_contains ~where:ntn' ~what:".." then is_approximation ntn ntn' + else String.equal ntn ntn' else let _,toks = decompose_notation_key fullntn' in let get_terminals = function Terminal ntn -> Some ntn | _ -> None in @@ -2230,7 +2321,7 @@ let browse_notation strict ntn map = String.Map.fold (fun scope_name sc -> NotationMap.fold (fun ntn data l -> - if List.exists (find ntn) ntns + if find ntn then List.map (fun d -> (ntn,scope_name,d)) (extract_notation_data data) @ l else l) sc.notations) map [] in diff --git a/interp/notation.mli b/interp/notation.mli index b8939ff87b..97955bf92e 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -334,8 +334,10 @@ val symbol_eq : symbol -> symbol -> bool val make_notation_key : notation_entry -> symbol list -> notation val decompose_notation_key : notation -> notation_entry * symbol list -(** Decompose a notation of the form "a 'U' b" *) -val decompose_raw_notation : string -> symbol list +(** Decompose a notation of the form "a 'U' b" together with the lists + of pairs of recursive variables and the list of all variables + binding in the notation *) +val decompose_raw_notation : string -> (Id.t * Id.t) list * Id.t list * symbol list (** Prints scopes (expects a pure aconstr printer) *) val pr_scope_class : scope_class -> Pp.t diff --git a/test-suite/output/locate.out b/test-suite/output/locate.out index 93d9d6cf7b..0196ead5e4 100644 --- a/test-suite/output/locate.out +++ b/test-suite/output/locate.out @@ -1,2 +1,8 @@ Notation "b1 && b2" := (if b1 then b2 else false) (default interpretation) Notation "x && y" := (andb x y) : bool_scope +Notation "'U' t" := (S t) (default interpretation) +Notation "'_' t" := (S t) (default interpretation) +Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope (default interpretation) +Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope (default interpretation) +Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope (default interpretation) +Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope (default interpretation) diff --git a/test-suite/output/locate.v b/test-suite/output/locate.v index af8b0ee193..6995743531 100644 --- a/test-suite/output/locate.v +++ b/test-suite/output/locate.v @@ -1,3 +1,26 @@ Set Printing Width 400. Notation "b1 && b2" := (if b1 then b2 else false). Locate "&&". + +Module M. + +Notation "'U' t" := (S t) (at level 0). +Notation "'_' t" := (S t) (at level 0). +Locate "U". (* was wrongly returning also "'_' t" *) +Locate "_". + +End M. + +Module N. + +(* Was not working at some time *) +Locate "( t , u , .. , v )". + +(* Was working though *) +Locate "( _ , _ , .. , _ )". + +(* We also support this *) +Locate "( t , u )". +Locate "( t , u , v )". + +End N. diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 8477870cb4..dc2b2e889e 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -194,52 +194,6 @@ let parse_format ({CAst.loc;v=str} : lstring) = (***********************) (* Analyzing notations *) -(* Interpret notations with a recursive component *) - -let out_nt = function NonTerminal x -> x | _ -> assert false - -let msg_expected_form_of_recursive_notation = - "In the notation, the special symbol \"..\" must occur in\na configuration of the form \"x symbs .. symbs y\"." - -let rec find_pattern nt xl = function - | Break n as x :: l, Break n' :: l' when Int.equal n n' -> - find_pattern nt (x::xl) (l,l') - | Terminal s as x :: l, Terminal s' :: l' when String.equal s s' -> - find_pattern nt (x::xl) (l,l') - | [], NonTerminal x' :: l' -> - (out_nt nt,x',List.rev xl),l' - | _, Break s :: _ | Break s :: _, _ -> - user_err Pp.(str ("A break occurs on one side of \"..\" but not on the other side.")) - | _, Terminal s :: _ | Terminal s :: _, _ -> - user_err ~hdr:"Metasyntax.find_pattern" - (str "The token \"" ++ str s ++ str "\" occurs on one side of \"..\" but not on the other side.") - | _, [] -> - user_err Pp.(str msg_expected_form_of_recursive_notation) - | ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) -> - anomaly (Pp.str "Only Terminal or Break expected on left, non-SProdList on right.") - -let rec interp_list_parser hd = function - | [] -> [], List.rev hd - | NonTerminal id :: tl when Id.equal id ldots_var -> - if List.is_empty hd then user_err Pp.(str msg_expected_form_of_recursive_notation); - let hd = List.rev hd in - let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in - let xyl,tl'' = interp_list_parser [] tl' in - (* We remember each pair of variable denoting a recursive part to *) - (* remove the second copy of it afterwards *) - (x,y)::xyl, SProdList (x,sl) :: tl'' - | (Terminal _ | Break _) as s :: tl -> - if List.is_empty hd then - let yl,tl' = interp_list_parser [] tl in - yl, s :: tl' - else - interp_list_parser (s::hd) tl - | NonTerminal _ as x :: tl -> - let xyl,tl' = interp_list_parser [x] tl in - xyl, List.rev_append hd tl' - | SProdList _ :: _ -> anomaly (Pp.str "Unexpected SProdList in interp_list_parser.") - - (* Find non-terminal tokens of notation *) (* To protect alphabetic tokens and quotes from being seen as variables *) @@ -256,24 +210,16 @@ let is_numeral_in_constr entry symbs = | _ -> false -let rec get_notation_vars onlyprint = function - | [] -> [] - | NonTerminal id :: sl -> - let vars = get_notation_vars onlyprint sl in - if Id.equal id ldots_var then vars else - (* don't check for nonlinearity if printing only, see Bug 5526 *) - if not onlyprint && Id.List.mem id vars then - user_err ~hdr:"Metasyntax.get_notation_vars" - (str "Variable " ++ Id.print id ++ str " occurs more than once.") - else id::vars - | (Terminal _ | Break _) :: sl -> get_notation_vars onlyprint sl - | SProdList _ :: _ -> assert false - -let analyze_notation_tokens ~onlyprint ntn = - let l = decompose_raw_notation ntn in - let vars = get_notation_vars onlyprint l in - let recvars,l = interp_list_parser [] l in - recvars, List.subtract Id.equal vars (List.map snd recvars), l +let analyze_notation_tokens ~onlyprint df = + let (recvars,mainvars,symbols as res) = decompose_raw_notation df in + (* don't check for nonlinearity if printing only, see Bug 5526 *) + (if not onlyprint then + match List.duplicates Id.equal (mainvars @ List.map snd recvars) with + | id :: _ -> + user_err ~hdr:"Metasyntax.get_notation_vars" + (str "Variable " ++ Id.print id ++ str " occurs more than once.") + | _ -> ()); + res let error_not_same_scope x y = user_err ~hdr:"Metasyntax.error_not_name_scope" |