diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/_static/coqnotations.sty | 5 | ||||
| -rw-r--r-- | doc/sphinx/_static/notations.css | 14 | ||||
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 34 | ||||
| -rw-r--r-- | doc/tools/docgram/README.md | 19 | ||||
| -rw-r--r-- | doc/tools/docgram/doc_grammar.ml | 532 |
5 files changed, 338 insertions, 266 deletions
diff --git a/doc/sphinx/_static/coqnotations.sty b/doc/sphinx/_static/coqnotations.sty index 3dfe4db439..2b1678e7ef 100644 --- a/doc/sphinx/_static/coqnotations.sty +++ b/doc/sphinx/_static/coqnotations.sty @@ -79,7 +79,7 @@ \newcssclass{prodn-table}{% \begin{savenotes} \sphinxattablestart - \begin{tabulary}{\linewidth}[t]{lLL} + \begin{tabulary}{\linewidth}[t]{lLLL} #1 \end{tabulary} \par @@ -89,4 +89,5 @@ \newcssclass{prodn-target}{\raisebox{\dimexpr \nscriptsize \relax}{#1}} \newcssclass{prodn-cell-nonterminal}{#1 &} \newcssclass{prodn-cell-op}{#1 &} -\newcssclass{prodn-cell-production}{#1\\} +\newcssclass{prodn-cell-production}{#1 &} +\newcssclass{prodn-cell-tag}{#1\\} diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css index 9546f7107e..8c3f7ac3c1 100644 --- a/doc/sphinx/_static/notations.css +++ b/doc/sphinx/_static/notations.css @@ -192,7 +192,8 @@ .prodn-cell-nonterminal, .prodn-cell-op, -.prodn-cell-production +.prodn-cell-production, +.prodn-cell-tag { display: table-cell; } @@ -206,6 +207,17 @@ font-weight: normal; } +.prodn-cell-production { + width: 99%; +} + +.prodn-cell-tag { + text-align: right; + font-weight: normal; + font-size: 75%; + font-family: "Lato","proxima-nova","Helvetica Neue",Arial,sans-serif; +} + .prodn-table .notation > .repeat-wrapper { margin-top: 0.28em; } diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 284c5d585a..d8caf4efe2 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -494,7 +494,11 @@ class ProductionObject(CoqObject): loc = os.path.basename(get_node_location(signode)) raise ExtensionError(ProductionObject.SIG_ERROR.format(loc, signature)) - self.signatures.append((lhs, op, rhs)) + parts = rhs.split(" ", maxsplit=1) + rhs = parts[0].strip() + tag = parts[1].strip() if len(parts) == 2 else "" + + self.signatures.append((lhs, op, rhs, tag)) return [('token', lhs)] if op == '::=' else None def _add_index_entry(self, name, target): @@ -513,21 +517,21 @@ class ProductionObject(CoqObject): self.signatures = [] indexnode = super().run()[0] # makes calls to handle_signature - table = nodes.inline(classes=['prodn-table']) - tgroup = nodes.inline(classes=['prodn-column-group']) - for _ in range(3): - tgroup += nodes.inline(classes=['prodn-column']) + table = nodes.container(classes=['prodn-table']) + tgroup = nodes.container(classes=['prodn-column-group']) + for _ in range(4): + tgroup += nodes.container(classes=['prodn-column']) table += tgroup - tbody = nodes.inline(classes=['prodn-row-group']) + tbody = nodes.container(classes=['prodn-row-group']) table += tbody # create rows for signature in self.signatures: - lhs, op, rhs = signature + lhs, op, rhs, tag = signature position = self.state_machine.get_source_and_line(self.lineno) - row = nodes.inline(classes=['prodn-row']) - entry = nodes.inline(classes=['prodn-cell-nonterminal']) + row = nodes.container(classes=['prodn-row']) + entry = nodes.container(classes=['prodn-cell-nonterminal']) if lhs != "": target_name = 'grammar-token-' + nodes.make_id(lhs) target = nodes.target('', '', ids=[target_name], names=[target_name]) @@ -537,17 +541,21 @@ class ProductionObject(CoqObject): entry += inline entry += notation_to_sphinx('@'+lhs, *position) else: - entry += nodes.literal('', '') + entry += nodes.Text('') row += entry - entry = nodes.inline(classes=['prodn-cell-op']) - entry += nodes.literal(op, op) + entry = nodes.container(classes=['prodn-cell-op']) + entry += nodes.Text(op) row += entry - entry = nodes.inline(classes=['prodn-cell-production']) + entry = nodes.container(classes=['prodn-cell-production']) entry += notation_to_sphinx(rhs, *position) row += entry + entry = nodes.container(classes=['prodn-cell-tag']) + entry += nodes.Text(tag) + row += entry + tbody += row return [indexnode, table] # only this node goes into the doc diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md index 910f400f99..14f87e5885 100644 --- a/doc/tools/docgram/README.md +++ b/doc/tools/docgram/README.md @@ -241,9 +241,22 @@ to the grammar. The end of the existing `prodn` is recognized by a blank line. -### Other details +### Tagging productions + +`doc_grammar` tags the origin of productions from plugins that aren't automatically +loaded. In grammar files, they appear as `(* XXX plugin *)`. In rsts, productions +generated by `.. insertprodn` will include where relevant three spaces as (a delimiter) +and a tag name after each production, which Sphinx will show on the far right-hand side +of the production. + +The origin of a production can be specified explicitly in `common.edit_mlg` with the +`TAG name` appearing at the end of a production. `name` must be in quotes if it +contains whitespace characters. Some edit operations preserve the +tags, but others, such as `REPLACE ... WITH ...` do not. + +A mapping from filenames to tags (e.g. "g_ltac2.mlg" is "Ltac2") is hard-coded as is +filtering to avoid showing tags for, say, Ltac2 productions from appearing on every +production in that chapter. -The output identifies productions from plugins that aren't automatically loaded with -`(* XXX plugin *)` in grammar files and with `(XXX plugin)` in productionlists. If desired, this mechanism could be extended to tag certain productions as deprecated, perhaps in conjunction with a coqpp change. diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml index 9851b1c788..0f8144cbcf 100644 --- a/doc/tools/docgram/doc_grammar.ml +++ b/doc/tools/docgram/doc_grammar.ml @@ -82,6 +82,138 @@ type gram = { order: string list; } + +(*** Print routines ***) + +let sprintf = Printf.sprintf + +let map_and_concat f ?(delim="") l = + String.concat delim (List.map f l) + +let rec db_output_prodn = function + | Sterm s -> sprintf "(Sterm %s) " s + | Snterm s -> sprintf "(Snterm %s) " s + | Slist1 sym -> sprintf "(Slist1 %s) " (db_output_prodn sym) + | Slist1sep (sym, sep) -> sprintf "(Slist1sep %s %s) " (db_output_prodn sep) (db_output_prodn sym) + | Slist0 sym -> sprintf "(Slist0 %s) " (db_output_prodn sym) + | Slist0sep (sym, sep) -> sprintf "(Slist0sep %s %s) " (db_output_prodn sep) (db_output_prodn sym) + | Sopt sym -> sprintf "(Sopt %s) " (db_output_prodn sym) + | Sparen prod -> sprintf "(Sparen %s) " (db_out_list prod) + | Sprod prods -> sprintf "(Sprod %s) " (db_out_prods prods) + | Sedit s -> sprintf "(Sedit %s) " s + | Sedit2 (s, s2) -> sprintf "(Sedit2 %s %s) " s s2 +and db_out_list prod = sprintf "(%s)" (map_and_concat db_output_prodn prod) +and db_out_prods prods = sprintf "( %s )" (map_and_concat ~delim:" | " db_out_list prods) + +(* identify special chars that don't get a trailing space in output *) +let omit_space s = List.mem s ["?"; "."; "#"] + +let rec output_prod plist need_semi = function + | Sterm s -> if plist then sprintf "%s" s else sprintf "\"%s\"" s + | Snterm s -> + if plist then sprintf "`%s`" s else + sprintf "%s%s" s (if s = "IDENT" && need_semi then ";" else "") + | Slist1 sym -> sprintf "LIST1 %s" (prod_to_str ~plist [sym]) + | Slist1sep (sym, sep) -> sprintf "LIST1 %s SEP %s" (prod_to_str ~plist [sym]) (prod_to_str ~plist [sep]) + | Slist0 sym -> sprintf "LIST0 %s" (prod_to_str ~plist [sym]) + | Slist0sep (sym, sep) -> sprintf "LIST0 %s SEP %s" (prod_to_str ~plist [sym]) (prod_to_str ~plist [sep]) + | Sopt sym -> sprintf "OPT %s" (prod_to_str ~plist [sym]) + | Sparen sym_list -> sprintf "( %s )" (prod_to_str sym_list) + | Sprod sym_list_list -> + sprintf "[ %s ]" (String.concat " " (List.mapi (fun i r -> + let prod = (prod_to_str r) in + let sep = if i = 0 then "" else + if prod <> "" then "| " else "|" in + sprintf "%s%s" sep prod) + sym_list_list)) + | Sedit s -> sprintf "%s" s + (* todo: make TAG info output conditional on the set of prods? *) + | Sedit2 ("TAG", plugin) -> + if plist then + sprintf " (%s plugin)" plugin + else + sprintf " (* %s plugin *)" plugin + | Sedit2 ("FILE", file) -> + let file_suffix_regex = Str.regexp ".*/\\([a-zA-Z0-9_\\.]+\\)" in + let suffix = if Str.string_match file_suffix_regex file 0 then Str.matched_group 1 file else file in + if plist then + sprintf " (%s)" suffix + else + sprintf " (* %s *)" suffix + | Sedit2 (s, s2) -> sprintf "%s \"%s\"" s s2 + +and prod_to_str_r plist prod = + match prod with + | Sterm s :: Snterm "ident" :: tl when omit_space s && plist -> + (sprintf "%s`ident`" s) :: (prod_to_str_r plist tl) + | p :: tl -> + let need_semi = + match prod with + | Snterm "IDENT" :: Sterm _ :: _ + | Snterm "IDENT" :: Sprod _ :: _ -> true + | _ -> false in + (output_prod plist need_semi p) :: (prod_to_str_r plist tl) + | [] -> [] + +and prod_to_str ?(plist=false) prod = + String.concat " " (prod_to_str_r plist prod) + +(* Determine if 2 productions are equal ignoring Sedit and Sedit2 *) +let ematch prod edit = + let rec ematchr prod edit = + (*Printf.printf "%s and\n %s\n\n" (prod_to_str prod) (prod_to_str edit);*) + match (prod, edit) with + | (_, Sedit _ :: tl) + | (_, Sedit2 _ :: tl) + -> ematchr prod tl + | (Sedit _ :: tl, _) + | (Sedit2 _ :: tl, _) + -> ematchr tl edit + | (phd :: ptl, hd :: tl) -> + let m = match (phd, hd) with + | (Slist1 psym, Slist1 sym) + | (Slist0 psym, Slist0 sym) + | (Sopt psym, Sopt sym) + -> ematchr [psym] [sym] + | (Slist1sep (psym, psep), Slist1sep (sym, sep)) + | (Slist0sep (psym, psep), Slist0sep (sym, sep)) + -> ematchr [psym] [sym] && ematchr [psep] [sep] + | (Sparen psyml, Sparen syml) + -> ematchr psyml syml + | (Sprod psymll, Sprod symll) -> + if List.compare_lengths psymll symll != 0 then false + else + List.fold_left (&&) true (List.map2 ematchr psymll symll) + | _, _ -> phd = hd + in + m && ematchr ptl tl + | ([], hd :: tl) -> false + | (phd :: ptl, []) -> false + | ([], []) -> true +in + (*Printf.printf "\n";*) + let rv = ematchr prod edit in + (*Printf.printf "%b\n" rv;*) + rv + +let get_first m_prod prods = + let rec find_first_r prods i = + match prods with + | [] -> + raise Not_found + | prod :: tl -> + if ematch prod m_prod then i + else find_first_r tl (i+1) + in + find_first_r prods 0 + +let find_first edit prods nt = + try + get_first edit prods + with Not_found -> + error "Can't find '%s' in edit for '%s'\n" (prod_to_str edit) nt; + raise Not_found + module DocGram = struct (* these guarantee that order and map have a 1-1 relationship on the nt name. They don't guarantee that nts on rhs of a production @@ -169,81 +301,6 @@ module DocGram = struct end open DocGram -(*** Print routines ***) - -let sprintf = Printf.sprintf - -let map_and_concat f ?(delim="") l = - String.concat delim (List.map f l) - -let rec db_output_prodn = function - | Sterm s -> sprintf "(Sterm %s) " s - | Snterm s -> sprintf "(Snterm %s) " s - | Slist1 sym -> sprintf "(Slist1 %s) " (db_output_prodn sym) - | Slist1sep (sym, sep) -> sprintf "(Slist1sep %s %s) " (db_output_prodn sep) (db_output_prodn sym) - | Slist0 sym -> sprintf "(Slist0 %s) " (db_output_prodn sym) - | Slist0sep (sym, sep) -> sprintf "(Slist0sep %s %s) " (db_output_prodn sep) (db_output_prodn sym) - | Sopt sym -> sprintf "(Sopt %s) " (db_output_prodn sym) - | Sparen prod -> sprintf "(Sparen %s) " (db_out_list prod) - | Sprod prods -> sprintf "(Sprod %s) " (db_out_prods prods) - | Sedit s -> sprintf "(Sedit %s) " s - | Sedit2 (s, s2) -> sprintf "(Sedit2 %s %s) " s s2 -and db_out_list prod = sprintf "(%s)" (map_and_concat db_output_prodn prod) -and db_out_prods prods = sprintf "( %s )" (map_and_concat ~delim:" | " db_out_list prods) - -(* identify special chars that don't get a trailing space in output *) -let omit_space s = List.mem s ["?"; "."; "#"] - -let rec output_prod plist need_semi = function - | Sterm s -> if plist then sprintf "%s" s else sprintf "\"%s\"" s - | Snterm s -> - if plist then sprintf "`%s`" s else - sprintf "%s%s" s (if s = "IDENT" && need_semi then ";" else "") - | Slist1 sym -> sprintf "LIST1 %s" (prod_to_str ~plist [sym]) - | Slist1sep (sym, sep) -> sprintf "LIST1 %s SEP %s" (prod_to_str ~plist [sym]) (prod_to_str ~plist [sep]) - | Slist0 sym -> sprintf "LIST0 %s" (prod_to_str ~plist [sym]) - | Slist0sep (sym, sep) -> sprintf "LIST0 %s SEP %s" (prod_to_str ~plist [sym]) (prod_to_str ~plist [sep]) - | Sopt sym -> sprintf "OPT %s" (prod_to_str ~plist [sym]) - | Sparen sym_list -> sprintf "( %s )" (prod_to_str sym_list) - | Sprod sym_list_list -> - sprintf "[ %s ]" (String.concat " " (List.mapi (fun i r -> - let prod = (prod_to_str r) in - let sep = if i = 0 then "" else - if prod <> "" then "| " else "|" in - sprintf "%s%s" sep prod) - sym_list_list)) - | Sedit s -> sprintf "%s" s - (* todo: make TAG info output conditional on the set of prods? *) - | Sedit2 ("TAG", plugin) -> - if plist then - sprintf " (%s plugin)" plugin - else - sprintf " (* %s plugin *)" plugin - | Sedit2 ("FILE", file) -> - let file_suffix_regex = Str.regexp ".*/\\([a-zA-Z0-9_\\.]+\\)" in - let suffix = if Str.string_match file_suffix_regex file 0 then Str.matched_group 1 file else file in - if plist then - sprintf " (%s)" suffix - else - sprintf " (* %s *)" suffix - | Sedit2 (s, s2) -> sprintf "%s \"%s\"" s s2 - -and prod_to_str_r plist prod = - match prod with - | Sterm s :: Snterm "ident" :: tl when omit_space s && plist -> - (sprintf "%s`ident`" s) :: (prod_to_str_r plist tl) - | p :: tl -> - let need_semi = - match prod with - | Snterm "IDENT" :: Sterm _ :: _ - | Snterm "IDENT" :: Sprod _ :: _ -> true - | _ -> false in - (output_prod plist need_semi p) :: (prod_to_str_r plist tl) - | [] -> [] - -and prod_to_str ?(plist=false) prod = - String.concat " " (prod_to_str_r plist prod) - let rec output_prodn = function | Sterm s -> @@ -294,10 +351,13 @@ and prod_to_prodn_r prod = and prod_to_prodn prod = String.concat " " (prod_to_prodn_r prod) -let get_tag prod = +let get_tag file prod = List.fold_left (fun rv sym -> match sym with - | Sedit2 ("TAG", s2) -> " " ^ s2 + (* todo: temporarily limited to Ltac2 tags in prodn when not in ltac2.rst *) + | Sedit2 ("TAG", s2) + when (s2 = "Ltac2" || s2 = "not Ltac2") && + file <> "doc/sphinx/proof-engine/ltac2.rst" -> " " ^ s2 | _ -> rv ) "" prod @@ -408,6 +468,8 @@ and cvt_gram_sym_list l = (Sedit2 ("USE_NT", s2)) :: cvt_gram_sym_list tl | GSymbQualid ("TAG", _) :: GSymbQualid (s2, l) :: tl -> (Sedit2 ("TAG", s2)) :: cvt_gram_sym_list tl + | GSymbQualid ("TAG", _) :: GSymbString (s2) :: tl -> + (Sedit2 ("TAG", s2)) :: cvt_gram_sym_list tl | GSymbString s :: tl -> (* todo: not seeing "(bfs)" here for some reason *) keywords := StringSet.add s !keywords; @@ -485,43 +547,6 @@ let autoloaded_mlgs = [ (* in the order they are loaded by Coq *) ] -let ematch prod edit = - let rec ematchr prod edit = - (*Printf.printf "%s and\n %s\n\n" (prod_to_str prod) (prod_to_str edit);*) - match (prod, edit) with - | (_, Sedit _ :: tl) - | (_, Sedit2 _ :: tl) - -> ematchr prod tl - | (Sedit _ :: tl, _) - | (Sedit2 _ :: tl, _) - -> ematchr tl edit - | (phd :: ptl, hd :: tl) -> - let m = match (phd, hd) with - | (Slist1 psym, Slist1 sym) - | (Slist0 psym, Slist0 sym) - | (Sopt psym, Sopt sym) - -> ematchr [psym] [sym] - | (Slist1sep (psym, psep), Slist1sep (sym, sep)) - | (Slist0sep (psym, psep), Slist0sep (sym, sep)) - -> ematchr [psym] [sym] && ematchr [psep] [sep] - | (Sparen psyml, Sparen syml) - -> ematchr psyml syml - | (Sprod psymll, Sprod symll) -> - if List.compare_lengths psymll symll != 0 then false - else - List.fold_left (&&) true (List.map2 ematchr psymll symll) - | _, _ -> phd = hd - in - m && ematchr ptl tl - | ([], hd :: tl) -> false - | (phd :: ptl, []) -> false - | ([], []) -> true -in - (*Printf.printf "\n";*) - let rv = ematchr prod edit in - (*Printf.printf "%b\n" rv;*) - rv - let has_match p prods = List.exists (fun p2 -> ematch p p2) prods let plugin_regex = Str.regexp "^plugins/\\([a-zA-Z0-9_]+\\)/" @@ -649,6 +674,110 @@ let add_rule g nt prods file = g_maybe_add_begin g nt (ent @ nodups) +let remove_Sedit2 p = + List.filter (fun sym -> match sym with | Sedit2 _ -> false | _ -> true) p + +(* edit a production: rename nonterminals, drop nonterminals, substitute nonterminals *) +let rec edit_prod g top edit_map prod = + let edit_nt edit_map sym0 nt = + try + let binding = StringMap.find nt edit_map in + match binding with + | "DELETE" -> [] + | "SPLICE" -> + begin + try let splice_prods = NTMap.find nt !g.map in + match splice_prods with + | [] -> error "Empty splice for '%s'\n" nt; [] + | [p] -> List.rev (remove_Sedit2 p) + | _ -> [Sprod (List.map remove_Sedit2 splice_prods)] (* todo? check if we create a dup *) + with Not_found -> error "Missing nt '%s' for splice\n" nt; [Snterm nt] + end + | _ -> [Snterm binding] + with Not_found -> [sym0] + in + let maybe_wrap syms = + match syms with + | s :: [] -> List.hd syms + | s -> Sparen (List.rev syms) + in + + let rec edit_symbol sym0 = + match sym0 with + | Sterm s -> [sym0] + | Snterm s -> edit_nt edit_map sym0 s + | Slist1 sym -> [Slist1 (maybe_wrap (edit_symbol sym))] + (* you'll get a run-time failure deleting a SEP symbol *) + | Slist1sep (sym, sep) -> [Slist1sep (maybe_wrap (edit_symbol sym), (List.hd (edit_symbol sep)))] + | Slist0 sym -> [Slist0 (maybe_wrap (edit_symbol sym))] + | Slist0sep (sym, sep) -> [Slist0sep (maybe_wrap (edit_symbol sym), (List.hd (edit_symbol sep)))] + | Sopt sym -> [Sopt (maybe_wrap (edit_symbol sym))] + | Sparen slist -> [Sparen (List.hd (edit_prod g false edit_map slist))] + | Sprod slistlist -> let (_, prods) = edit_rule g edit_map "" slistlist in + [Sprod prods] + | Sedit _ + | Sedit2 _ -> [sym0] (* these constructors not used here *) + in + let is_splice nt = + try + StringMap.find nt edit_map = "SPLICE" + with Not_found -> false + in + let get_splice_prods nt = + try NTMap.find nt !g.map + with Not_found -> (error "Missing nt '%s' for splice\n" nt; []) + in + + (* special case splice creating multiple new productions *) + let splice_prods = match prod with + | Snterm nt :: [] when is_splice nt -> + get_splice_prods nt + | _ -> [] + in + if top && splice_prods <> [] then + splice_prods + else + [List.rev (List.concat (List.rev (List.map (fun sym -> edit_symbol sym) prod)))] + +and edit_rule g edit_map nt rule = + let nt = + try let new_name = StringMap.find nt edit_map in + match new_name with + | "SPLICE" -> nt + | "DELETE" -> "" + | _ -> new_name + with Not_found -> nt + in + (nt, (List.concat (List.map (edit_prod g true edit_map) rule))) + +let read_mlg_files g args symdef_map = + let level_renames = ref StringMap.empty in + let last_autoloaded = List.hd (List.rev autoloaded_mlgs) in + List.iter (fun file -> + (* todo: ??? does nt renaming, deletion and splicing *) + let rules, locals, dup_renames = read_mlg g false (parse_file file) file level_renames symdef_map in + let numprods = List.fold_left (fun num rule -> + let nt, prods = rule in + (* rename local duplicates *) + let prods = List.map (fun prod -> List.hd (edit_prod g true dup_renames prod)) prods in + let nt = try StringMap.find nt dup_renames with Not_found -> nt in +(* if NTMap.mem nt !g.map && (StringSet.mem nt locals) &&*) +(* StringSet.cardinal (StringSet.of_list (StringMap.find nt !symdef_map)) > 1 then*) +(* warn "%s: local nonterminal '%s' already defined\n" file nt; (* todo: goes away *)*) + add_rule g nt prods file; + num + List.length prods) + 0 rules + in + if args.verbose then begin + Printf.eprintf "%s: %d nts, %d prods\n" file (List.length rules) numprods; + if file = last_autoloaded then + Printf.eprintf " Optionally loaded plugins:\n" + end + ) args.mlg_files; + g_reverse g; + !level_renames + + (* get the nt's in the production, preserving order, don't worry about dups *) let nts_in_prod prod = let rec traverse = function @@ -702,6 +831,11 @@ let create_edit_map g op edits = | "RENAME" -> if not (StringSet.mem key all_nts_ref || (StringSet.mem key all_nts_def)) then error "Unused/undefined nt `%s` in RENAME\n" key; + | "MERGE" -> + if not (StringSet.mem key all_nts_ref || (StringSet.mem key all_nts_def)) then + error "Unused/undefined nt `%s` in MERGE\n" key; + if not (StringSet.mem binding all_nts_ref || (StringSet.mem binding all_nts_def)) then + error "Unused/undefined nt `%s` in MERGE\n" key; (* todo: could not get the following code to type check (match binding with | _ :: Snterm new_nt :: _ -> @@ -714,9 +848,6 @@ let create_edit_map g op edits = in aux edits StringMap.empty -let remove_Sedit2 p = - List.filter (fun sym -> match sym with | Sedit2 _ -> false | _ -> true) p - (* don't deal with Sedit, Sedit2 yet (ever?) *) let rec pmatch fullprod fullpat repl = let map_prod prod = List.concat (List.map (fun s -> pmatch [s] fullpat repl) prod) in @@ -769,88 +900,15 @@ let global_repl g pat repl = g_update_prods g nt (List.map (fun prod -> pmatch prod pat repl) (NTMap.find nt !g.map)) ) !g.order -(* edit a production: rename nonterminals, drop nonterminals, substitute nonterminals *) -let rec edit_prod g top edit_map prod = - let edit_nt edit_map sym0 nt = - try - let binding = StringMap.find nt edit_map in - match binding with - | "DELETE" -> [] - | "SPLICE" -> - begin - try let splice_prods = NTMap.find nt !g.map in - match splice_prods with - | [] -> error "Empty splice for '%s'\n" nt; [] - | [p] -> List.rev (remove_Sedit2 p) - | _ -> [Sprod (List.map remove_Sedit2 splice_prods)] (* todo? check if we create a dup *) - with Not_found -> error "Missing nt '%s' for splice\n" nt; [Snterm nt] - end - | _ -> [Snterm binding] - with Not_found -> [sym0] - in - let maybe_wrap syms = - match syms with - | s :: [] -> List.hd syms - | s -> Sparen (List.rev syms) - in - - let rec edit_symbol sym0 = - match sym0 with - | Sterm s -> [sym0] - | Snterm s -> edit_nt edit_map sym0 s - | Slist1 sym -> [Slist1 (maybe_wrap (edit_symbol sym))] - (* you'll get a run-time failure deleting a SEP symbol *) - | Slist1sep (sym, sep) -> [Slist1sep (maybe_wrap (edit_symbol sym), (List.hd (edit_symbol sep)))] - | Slist0 sym -> [Slist0 (maybe_wrap (edit_symbol sym))] - | Slist0sep (sym, sep) -> [Slist0sep (maybe_wrap (edit_symbol sym), (List.hd (edit_symbol sep)))] - | Sopt sym -> [Sopt (maybe_wrap (edit_symbol sym))] - | Sparen slist -> [Sparen (List.hd (edit_prod g false edit_map slist))] - | Sprod slistlist -> let (_, prods) = edit_rule g edit_map "" slistlist in - [Sprod prods] - | Sedit _ - | Sedit2 _ -> [sym0] (* these constructors not used here *) - in - let is_splice nt = - try - StringMap.find nt edit_map = "SPLICE" - with Not_found -> false - in - let get_splice_prods nt = - try NTMap.find nt !g.map - with Not_found -> (error "Missing nt '%s' for splice\n" nt; []) - in - - (* special case splice creating multiple new productions *) - let splice_prods = match prod with - | Snterm nt :: [] when is_splice nt -> - get_splice_prods nt - | _ -> [] - in - if top && splice_prods <> [] then - splice_prods - else - [List.rev (List.concat (List.rev (List.map (fun sym -> edit_symbol sym) prod)))] - -and edit_rule g edit_map nt rule = - let nt = - try let new_name = StringMap.find nt edit_map in - match new_name with - | "SPLICE" -> nt - | "DELETE" -> "" - | _ -> new_name - with Not_found -> nt - in - (nt, (List.concat (List.map (edit_prod g true edit_map) rule))) - (*** splice: replace a reference to a nonterminal with its definition ***) (* todo: create a better splice routine *) -let apply_splice g splice_map = +let apply_splice g edit_map = List.iter (fun b -> let (nt0, prods0) = b in let rec splice_loop nt prods cnt = let max_cnt = 10 in - let (nt', prods') = edit_rule g splice_map nt prods in + let (nt', prods') = edit_rule g edit_map nt prods in if cnt > max_cnt then error "Splice for '%s' not done after %d iterations\n" nt0 max_cnt; if nt' = nt && prods' = prods then @@ -868,19 +926,8 @@ let apply_splice g splice_map = | "SPLICE" -> g_remove g nt; | _ -> ()) - (StringMap.bindings splice_map) + (StringMap.bindings edit_map) -let find_first edit prods nt = - let rec find_first_r edit prods nt i = - match prods with - | [] -> - error "Can't find '%s' in edit for '%s'\n" (prod_to_str edit) nt; - raise Not_found - | prod :: tl -> - if ematch prod edit then i - else find_first_r edit tl nt (i+1) - in - find_first_r edit prods nt 0 let remove_prod edit prods nt = let res, got_first = List.fold_left (fun args prod -> @@ -899,34 +946,6 @@ let insert_after posn insert prods = if i = posn then prod :: insert else [prod]) prods) - -let read_mlg_files g args symdef_map = - let level_renames = ref StringMap.empty in - let last_autoloaded = List.hd (List.rev autoloaded_mlgs) in - List.iter (fun file -> - (* todo: ??? does nt renaming, deletion and splicing *) - let rules, locals, dup_renames = read_mlg g false (parse_file file) file level_renames symdef_map in - let numprods = List.fold_left (fun num rule -> - let nt, prods = rule in - (* rename local duplicates *) - let prods = List.map (fun prod -> List.hd (edit_prod g true dup_renames prod)) prods in - let nt = try StringMap.find nt dup_renames with Not_found -> nt in -(* if NTMap.mem nt !g.map && (StringSet.mem nt locals) &&*) -(* StringSet.cardinal (StringSet.of_list (StringMap.find nt !symdef_map)) > 1 then*) -(* warn "%s: local nonterminal '%s' already defined\n" file nt; (* todo: goes away *)*) - add_rule g nt prods file; - num + List.length prods) - 0 rules - in - if args.verbose then begin - Printf.eprintf "%s: %d nts, %d prods\n" file (List.length rules) numprods; - if file = last_autoloaded then - Printf.eprintf " Optionally loaded plugins:\n" - end - ) args.mlg_files; - g_reverse g; - !level_renames - (*** replace LIST*, OPT with new nonterminals ***) (* generate a non-terminal name for a replacement *) @@ -1116,6 +1135,29 @@ let expand_lists g = with | Queue.Empty -> () +let apply_merge g edit_map = + List.iter (fun b -> + let (from_nt, to_nt) = b in + let from_prods = NTMap.find from_nt !g.map in + List.iter (fun prod -> + try + ignore( get_first prod (NTMap.find to_nt !g.map)); + with Not_found -> g_add_prod_after g None to_nt prod) + from_prods) + (NTMap.bindings edit_map) + +let apply_rename_delete g edit_map = + List.iter (fun b -> let (nt, _) = b in + let prods = try NTMap.find nt !g.map with Not_found -> [] in + let (nt', prods') = edit_rule g edit_map nt prods in + if nt' = "" then + g_remove g nt + else if nt <> nt' then + g_rename_merge g nt nt' prods' + else + g_update_prods g nt prods') + (NTMap.bindings !g.map) + let edit_all_prods g op eprods = let do_it op eprods num = let rec aux eprods res = @@ -1130,25 +1172,20 @@ let edit_all_prods g op eprods = op (prod_to_str eprod) num; aux tl res in - let map = create_edit_map g op (aux eprods []) in - if op = "SPLICE" then - apply_splice g map - else (* RENAME/DELETE *) - List.iter (fun b -> let (nt, _) = b in - let prods = try NTMap.find nt !g.map with Not_found -> [] in - let (nt', prods') = edit_rule g map nt prods in - if nt' = "" then - g_remove g nt - else if nt <> nt' then - g_rename_merge g nt nt' prods' - else - g_update_prods g nt prods') - (NTMap.bindings !g.map); + let edit_map = create_edit_map g op (aux eprods []) in + match op with + | "SPLICE" -> apply_splice g edit_map + | "MERGE" -> apply_merge g edit_map; apply_rename_delete g edit_map + | "RENAME" + | "DELETE" -> apply_rename_delete g edit_map + | _ -> () + in match op with | "RENAME" -> do_it op eprods 2; true | "DELETE" -> do_it op eprods 1; true | "SPLICE" -> do_it op eprods 1; true + | "MERGE" -> do_it op eprods 2; true | "EXPAND" -> if List.length eprods > 1 || List.length (List.hd eprods) <> 0 then error "'EXPAND:' expects a single empty production\n"; @@ -1790,11 +1827,12 @@ let process_rst g file args seen tac_prods cmd_prods = let prods = NTMap.find nt !g.map in List.iteri (fun i prod -> let rhs = String.trim (prod_to_prodn prod) in + let tag = get_tag file prod in let sep = if i = 0 then " ::=" else "|" in if has_empty_prod prod then error "%s line %d: Empty (sub-)production for %s, edit to remove: '%s %s'\n" file !linenum nt sep rhs; - fprintf new_rst "%s %s%s %s\n" indent (if i = 0 then nt else "") sep rhs) + fprintf new_rst "%s %s%s %s%s\n" indent (if i = 0 then nt else "") sep rhs tag) prods; if nt <> end_ then copy_prods tl in |