diff options
| -rw-r--r-- | interp/notation.ml | 55 | ||||
| -rw-r--r-- | interp/notation.mli | 6 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 74 |
3 files changed, 68 insertions, 67 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 2b54bba2c8..45ab9c75e1 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -2202,7 +2202,60 @@ 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) +(* 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 possible_notations ntn = (* We collect the possible interpretations of a notation string depending on whether it is 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/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" |