From 905f2ccf16ff104769f33f1672ef404bc8424413 Mon Sep 17 00:00:00 2001 From: Basile Pesin Date: Mon, 3 Jun 2019 10:09:31 +0200 Subject: [PATCH 1/8] Creating an empty rst file --- src/auxl.ml | 2 ++ src/defns.ml | 10 +++++++--- src/embed_pp.ml | 5 +++-- src/grammar_pp.ml | 14 +++++++++----- src/main.ml | 19 ++++++++++++++++--- src/system_pp.ml | 4 ++++ src/types.ml | 3 +++ 7 files changed, 44 insertions(+), 13 deletions(-) diff --git a/src/auxl.ml b/src/auxl.ml index 5c64e04..4cb367c 100644 --- a/src/auxl.ml +++ b/src/auxl.ml @@ -51,6 +51,7 @@ let mode_name m = match m with | Rdx _ -> "Redex" | Lex _ -> "Lex" | Menhir _ -> "Menhir" + | Rst _ -> "ReStructuredText" let debug_on = false @@ -599,6 +600,7 @@ let hom_name_for_pp_mode m | Caml _ -> "ocaml" | Lex _ -> "lex" | Menhir _ -> "menhir" + | Rst _ -> "rst" (* select dependencies *) diff --git a/src/defns.ml b/src/defns.ml index 39d83d4..781260a 100644 --- a/src/defns.ml +++ b/src/defns.ml @@ -693,6 +693,7 @@ let pp_defnclass fd (m:pp_mode) (xd:syntaxdefn) lookup (dc:defnclass) = List.iter (fun d -> output_string fd (Grammar_pp.tex_defn_name m dc.dc_wrapper d.d_name); output_string fd "{}") dc.dc_defns; output_string fd "}\n\n" + | Rst _ -> () (* TODO *) (**********************************************) (* pp of fundefns *) @@ -708,6 +709,7 @@ let pp_funclause (m:pp_mode) (xd:syntaxdefn) (fc:funclause) : string = ppd_lhs ^ " === " ^ ppd_rhs ^ "\n" | Tex _ -> Grammar_pp.pp_tex_FUNCLAUSE_NAME m^"{"^ppd_lhs^"}"^"{"^ppd_rhs^"}%\n" + | Rst _ -> "" (* TODO *) | Isa _ | Hol _ | Lem _ | Coq _ | Caml _ | Twf _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_funclause" @@ -735,7 +737,7 @@ let pp_symterm_node_lhs m xd sie de st = match m with | Coq _ | Caml _ | Lem _ (* LemTODO4: really? *) -> (insert_commas hom) | Hol _ | Isa _ -> hom - | Twf _ | Ascii _ | Tex _ | Lex _ | Menhir _ -> raise Auxl.ThisCannotHappen + | Twf _ | Ascii _ | Tex _ | Rst _ | Lex _ | Menhir _ -> raise Auxl.ThisCannotHappen in String.concat " " (Grammar_pp.apply_hom_spec m xd hom pes) | _ -> Auxl.int_error "pp_symterm_node_lhs" @@ -839,7 +841,7 @@ let fundefn_to_int_func (m:pp_mode) (xd:syntaxdefn) (deps:string list) (fd:funde (v,ms) in Some ( fd.fd_name ^ " " ^ type_defn ^ ": " ^ result_type_name ^ "=\n", "", match_string) - | Tex _ | Ascii _ | Twf _ | Lex _ | Menhir _ -> raise Auxl.ThisCannotHappen + | Tex _ | Rst _ | Ascii _ | Twf _ | Lex _ | Menhir _ -> raise Auxl.ThisCannotHappen in match header with None -> None | Some header -> @@ -888,7 +890,7 @@ let pp_fundefn (m:pp_mode) (xd:syntaxdefn) lookup (fd:fundefn) : string = (List.map (pp_funclause m xd) fd.fd_clauses) ^ "\\end{"^Grammar_pp.pp_tex_FUNDEFN_BLOCK_NAME m ^"}" ^ "}\n\n" - + | Rst ro -> "" (* TODO *) | Isa _ | Hol _ | Lem _ | Coq _ | Twf _ | Caml _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_fundefn" @@ -911,6 +913,7 @@ let pp_fundefnclass (m:pp_mode) (xd:syntaxdefn) lookup (fdc:fundefnclass) : stri "\n" (List.map (function fd -> Grammar_pp.tex_fundefn_name m fd.fd_name^"{}") fdc.fdc_fundefns)) ^ "}\n\n" + | Rst _ -> "" (* TODO *) | Isa _ | Coq _ | Hol _ | Lem _ | Caml _ -> let proof = @@ -1005,6 +1008,7 @@ let pp_fun_or_reln_defnclass_list | FDC fdc -> Printf.fprintf fd "%s\n" (Grammar_pp.tex_fundefnclass_name m fdc.fdc_name) | RDC dc -> Printf.fprintf fd "%s\n" (Grammar_pp.tex_defnclass_name m dc.dc_name)) frdcs; output_string fd "}\n\n" + | Rst _ -> () (* TODO *) | Lex _ | Menhir _ -> () diff --git a/src/embed_pp.ml b/src/embed_pp.ml index da006ac..f77b799 100644 --- a/src/embed_pp.ml +++ b/src/embed_pp.ml @@ -61,6 +61,7 @@ and pp_embedmorphism fd m xd lookup (l,hn,es) = | (Lem _, "lem") | (Twf _, "twf") | (Tex _, "tex") + | (Rst _, "rst") | (Caml _, "ocaml") | (Rdx _, "rdx") | (Menhir _, "menhir") @@ -73,7 +74,7 @@ and pp_embedmorphism fd m xd lookup (l,hn,es) = | (Isa io, "isa-lib") -> let x = io.isa_library in x := (fst !x, embed_strings (snd !x) es) - | (Coq _, _) | (Isa _, _) | (Hol _,_) | (Lem _,_) | (Twf _,_) | (Tex _,_) | (Caml _,_) | (Lex _, _) | (Menhir _, _) -> () + | (Coq _, _) | (Isa _, _) | (Hol _,_) | (Lem _,_) | (Twf _,_) | (Tex _,_) | (Caml _,_) | (Lex _, _) | (Menhir _, _) | (Rst _, _) -> () and pp_embed_spec fd m xd lookup es = List.iter (pp_embed_spec_el fd m xd lookup) es @@ -89,7 +90,7 @@ and pp_embed_spec_el fd m xd lookup ese = output_string fd Grammar_pp.pp_DOUBLERIGHTBRACKET ) | Tex xo when (match ese with Embed_inner (_,"TEX_NAME_PREFIX")->true | _->false) -> output_string fd xo.ppt_name_prefix - | Tex _ | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Rdx _ | Caml _ | Lex _ | Menhir _ -> + | Tex _ | Rst _ | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Rdx _ | Caml _ | Lex _ | Menhir _ -> ( match ese with | Embed_string (l,s) -> output_string fd s diff --git a/src/grammar_pp.ml b/src/grammar_pp.ml index befd1ef..3423c1f 100644 --- a/src/grammar_pp.ml +++ b/src/grammar_pp.ml @@ -1027,6 +1027,7 @@ and pp_nonterm_with_sie_internal as_type m xd sie (ntr,suff) = String.concat "" (apply_hom_spec m xd hs [Auxl.pp_tex_escape ntr^(pp_suffix_with_sie m xd sie suff)])) + | Rst ro -> "" (* TODO *) | Coq _ | Isa _ | Hol _ | Lem _ | Rdx _ | Twf _ | Caml _ | Lex _ | Menhir _ -> let s0 = pp_ntr ^ (pp_suffix_with_sie m xd sie suff) in let s1 = @@ -1075,7 +1076,7 @@ and pp_metavar_with_sie_internal as_type m xd sie (mvr,suff) = String.concat "" (apply_hom_spec m xd hs [Auxl.pp_tex_escape mvr^(pp_suffix_with_sie m xd sie suff)])) - + | Rst _ -> "" (* TODO *) | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Rdx _ | Caml _ | Lex _ | Menhir _ -> let s = pp_mvr ^ (pp_suffix_with_sie m xd sie suff) in if as_type then s @@ -1312,9 +1313,10 @@ and pp_metavardefn m xd mvd = "%abbrev " ^ pp_metavarroot_ty m xd mvd.mvd_name ^ " : type = nat.\n" - | Lex _ -> "" - | Menhir _ -> "" - | Ascii _ | Tex _ -> raise Auxl.ThisCannotHappen )) + | Lex _ -> "" + | Menhir _ -> "" + | Rst _ -> "" + | Ascii _ | Tex _ -> raise Auxl.ThisCannotHappen )) and pp_metavarrep m xd mvd_rep type_name = match m with @@ -2810,7 +2812,7 @@ and pp_rule_list m xd rs = ^ strip_surrounding_parens (pp_nontermroot_ty m xd ntr) ^ " = " ^ pp_hom_spec m xd hs ^ "\n\n" - | Ascii _ | Tex _ | Lex _ | Menhir _ -> Auxl.errorm m "int_rule_list_dep" ) + | Ascii _ | Tex _ | Rst _ | Lex _ | Menhir _ -> Auxl.errorm m "int_rule_list_dep" ) (* or not, in which case we generate an inductive type definition *) | b -> let b = List.rev b in (* FZ this ensures that the output follows the source order *) @@ -2878,6 +2880,7 @@ and pp_rule_list m xd rs = rs) ^ (match rs with []-> "" | _ -> pp_tex_AFTERLASTRULE_NAME m) ^ "\n"^pp_tex_END_RULES ^ "}\n\n" + | Rst ro -> "" (* TODO *) | Lex _ | Menhir _ -> String.concat "\n" (Auxl.option_map (pp_rule m xd) rs) @@ -4366,4 +4369,5 @@ let pp_pp_mode m = match m with | Caml _ -> "Caml" | Lex _ -> "Lex" | Menhir _ -> "Menhir" + | Rst _ -> "ReStructuredText" diff --git a/src/main.ml b/src/main.ml index 99f2cf7..d992df8 100644 --- a/src/main.ml +++ b/src/main.ml @@ -64,6 +64,9 @@ let twf_filter_filename_dsts = ref ([] : string list) let caml_filter_filenames = ref ([] : (string * string) list) let caml_filter_filename_srcs = ref ([] : string list) let caml_filter_filename_dsts = ref ([] : string list) +let rst_filter_filenames = ref ([] : (string * string) list) +let rst_filter_filename_srcs = ref ([] : string list) +let rst_filter_filename_dsts = ref ([] : string list) let lift_cons_prefixes = ref false let test_parse_list = ref ([] : string list) let sort = ref true @@ -146,6 +149,10 @@ let options = Arg.align [ Arg.Tuple[Arg.String (fun s -> caml_filter_filename_srcs := s :: !caml_filter_filename_srcs); Arg.String (fun s -> caml_filter_filename_dsts := s :: !caml_filter_filename_dsts)], " Files to OCaml filter" ); + ( "-rst_filter", + Arg.Tuple[Arg.String (fun s -> rst_filter_filename_srcs := s :: !rst_filter_filename_srcs); + Arg.String (fun s -> rst_filter_filename_dsts := s :: !rst_filter_filename_dsts)], + " Files to ReStructuredText filter" ); ( "-merge", Arg.Bool (fun b -> merge_fragments := b), "<"^string_of_bool !merge_fragments ^"> merge grammar and definition rules" ); @@ -307,6 +314,7 @@ let _ = isa_filter_filenames := List.combine (!isa_filter_filename_srcs) (!isa_f let _ = coq_filter_filenames := List.combine (!coq_filter_filename_srcs) (!coq_filter_filename_dsts) let _ = twf_filter_filenames := List.combine (!twf_filter_filename_srcs) (!twf_filter_filename_dsts) let _ = caml_filter_filenames := List.combine (!caml_filter_filename_srcs) (!caml_filter_filename_dsts) +let _ = rst_filter_filenames := List.combine (!rst_filter_filename_srcs) (!rst_filter_filename_dsts) let types_of_extensions = [ "ott","ott"; @@ -319,7 +327,8 @@ let types_of_extensions = "ml", "ocaml"; "mll", "lex"; "mly", "menhir"; - "rkt", "rdx"] + "rkt", "rdx"; + "rst", "rst"] let extension_of_type t = List.assoc t (List.map (function (a,b)->(b,a)) types_of_extensions) @@ -334,7 +343,7 @@ let file_type name = _ -> None let non_tex_output_types = ["coq"; "isa"; "hol"; "lem"; "twf"; "ocaml"; "rdx"] -let output_types = "tex" :: "lex" :: "menhir" :: non_tex_output_types +let output_types = "tex" :: "lex" :: "menhir" :: "rst" :: non_tex_output_types let input_types = "ott" :: output_types let classify_file_argument arg = @@ -405,6 +414,7 @@ let m_tex = Tex {ppt_colour= !tex_colour; ppt_suppressed_ntrs= !tex_suppressed_ntrs; ppt_wrap= !tex_wrap; ppt_name_prefix= !tex_name_prefix } +let m_rst = Rst () let m_isa = Isa { ppi_isa_primrec = !isa_primrec; ppi_isa_inductive = !isa_inductive; isa_library = ref ("",[]); @@ -515,7 +525,8 @@ let m_rdx = Rdx pp_rdx_opts_default "twf",m_twf; "coq",m_coq; "tex",m_tex; - "rdx",m_rdx]) + "rdx",m_rdx; + "rst",m_rst]) targets_for_non_picky) (* process *) @@ -773,6 +784,8 @@ let output_stage (sd,lookup,sd_unquotiented,sd_quotiented_unaux) = let xd_quotiented_unaux = sd_quotiented_unaux.syntax in (Lex_menhir_pp.pp_menhir_syntaxdefn m_menhir sd.sources xd_quotiented xd_unquotiented lookup !generate_aux_rules fi; Lex_menhir_pp.pp_pp_syntaxdefn m_menhir sd.sources xd_quotiented xd_unquotiented xd_quotiented_unaux !generate_aux_rules fi ) + | "rst" -> + System_pp.pp_systemdefn_core_io m_rst sd lookup fi !merge_fragments | _ -> Auxl.int_error("unknown target "^t)) diff --git a/src/system_pp.ml b/src/system_pp.ml index 9813e85..b872e17 100644 --- a/src/system_pp.ml +++ b/src/system_pp.ml @@ -190,6 +190,7 @@ let pp_library fd m = | Twf wo -> pp_lib wo.twf_library | Caml oo-> pp_lib oo.caml_library | Rdx ro -> () + | Rst _ -> () (* TODO *) | Ascii _ | Tex _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_library" let pp_struct_entry fd m sd xd_expanded lookup stre : unit = @@ -507,6 +508,9 @@ let pp_systemdefn_core_io m sd lookup oi merge_fragments = [ Embed_string (dummy_loc, ";;; generated by Ott "^Version.n^" from: "^file_sources^"\n\n" ^ "#lang racket\n(require redex)\n")] + | Rst _ -> + [ Embed_string (dummy_loc, + ".. generated by Ott "^Version.n^" from: "^file_sources^"\n")] | _ -> Auxl.errorm m "std_preamble_embed" )) diff --git a/src/types.ml b/src/types.ml index f08788a..d27780d 100644 --- a/src/types.ml +++ b/src/types.ml @@ -860,6 +860,8 @@ type pp_menhir_opts = ppm_caml_ast_module : string; ppm_caml_parser_module : string; } (* yo *) + +type pp_rst_opts = unit (* TODO *) type pp_mode = (* m *) | Coq of pp_coq_opts @@ -873,6 +875,7 @@ type pp_mode = (* m *) | Caml of pp_caml_opts | Lex of pp_menhir_opts (* NB: same as pp_menhir_opts *) | Menhir of pp_menhir_opts + | Rst of pp_rst_opts let pp_ascii_opts_default = Ascii { ppa_colour = true; From 64c6cb7f74b57ceb2c63b67bd68ca63ff8fd04df Mon Sep 17 00:00:00 2001 From: Basile Pesin Date: Mon, 3 Jun 2019 15:29:28 +0200 Subject: [PATCH 2/8] Displaying relations OK for non-merge source --- src/auxl.ml | 1 + src/defns.ml | 31 +++++++++++++++++++++++++++++-- src/grammar_pp.ml | 33 ++++++++++++++++++++++----------- src/system_pp.ml | 5 ++++- 4 files changed, 56 insertions(+), 14 deletions(-) diff --git a/src/auxl.ml b/src/auxl.ml index 4cb367c..219a318 100644 --- a/src/auxl.ml +++ b/src/auxl.ml @@ -794,6 +794,7 @@ let big_line_comment m s = | Coq _ | Hol _ | Lem _ | Isa _ | Caml _ -> "(** "^s^" *)\n" | Twf _ -> "%%% "^s^" %%%\n\n" | Tex _ -> "% "^s^"\n" + | Rst _ -> ".. "^s^"\n" | Menhir _ | Lex _ | Ascii _ -> errorm m "big_line_comment" (* print only if not empty *) diff --git a/src/defns.ml b/src/defns.ml index 781260a..3bbf3a3 100644 --- a/src/defns.ml +++ b/src/defns.ml @@ -243,6 +243,7 @@ let pp_drule fd (m:pp_mode) (xd:syntaxdefn) (dr:drule) : unit = (Grammar_pp.pp_tex_DRULE_NAME_NAME m) (Auxl.pp_tex_escape dr.drule_name) pp_com + | Rst _ -> print_endline "rule" (* TODO *) | Isa _ | Hol _ | Lem _ | Coq _ | Twf _ | Rdx _ -> let non_free_ntrs = Subrules_pp.non_free_ntrs m xd xd.xd_srs in @@ -561,6 +562,26 @@ let pp_defn fd (m:pp_mode) (xd:syntaxdefn) lookup (defnclass_wrapper:string) (un | PSR_Defncom es -> Embed_pp.pp_embed_spec fd m xd lookup es) d.d_rules; Printf.fprintf fd "\\end{%s}}\n\n" (Grammar_pp.pp_tex_DEFN_BLOCK_NAME m) + | Rst _ -> + Printf.fprintf fd ".. defn %s\n" d.d_name; + List.iter (function + | PSR_Rule dr -> + let ascii_mode = (Ascii {ppa_colour = false; + ppa_ugly = false; + ppa_lift_cons_prefixes = false; + ppa_show_deps = false; + ppa_show_defns = false; }) in + Printf.fprintf fd "%s::\n\n" dr.drule_name; + let premises_str = List.map (fun (_, p) -> Grammar_pp.pp_symterm ascii_mode xd [] de_empty p) dr.drule_premises + and conclusion_str = (Grammar_pp.pp_symterm ascii_mode xd [] de_empty dr.drule_conclusion) in + let len = List.fold_left (fun m s -> max m (String.length s)) 0 premises_str in + let len = max len (String.length conclusion_str) in + List.iter (Printf.fprintf fd "\t%s\n") premises_str; + Printf.fprintf fd "\t%s\n" (String.make len '-'); + Printf.fprintf fd "\t%s\n\n" conclusion_str + | PSR_Defncom es -> Embed_pp.pp_embed_spec fd m xd lookup es) + d.d_rules; + Printf.fprintf fd "\n" | Caml _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_defn" @@ -693,7 +714,10 @@ let pp_defnclass fd (m:pp_mode) (xd:syntaxdefn) lookup (dc:defnclass) = List.iter (fun d -> output_string fd (Grammar_pp.tex_defn_name m dc.dc_wrapper d.d_name); output_string fd "{}") dc.dc_defns; output_string fd "}\n\n" - | Rst _ -> () (* TODO *) + | Rst _ -> + Printf.fprintf fd ".. defns %s\n" dc.dc_name; + List.iter (fun d -> pp_defn fd m xd lookup dc.dc_wrapper universe d) dc.dc_defns + (* TODO *) (**********************************************) (* pp of fundefns *) @@ -1008,7 +1032,10 @@ let pp_fun_or_reln_defnclass_list | FDC fdc -> Printf.fprintf fd "%s\n" (Grammar_pp.tex_fundefnclass_name m fdc.fdc_name) | RDC dc -> Printf.fprintf fd "%s\n" (Grammar_pp.tex_defnclass_name m dc.dc_name)) frdcs; output_string fd "}\n\n" - | Rst _ -> () (* TODO *) + | Rst _ -> + (* output_string fd ".. defnss\n"; *) + List.iter (fun frdc -> pp_fun_or_reln_defnclass fd m xd lookup frdc) frdcs; + output_string fd "\n\n" | Lex _ | Menhir _ -> () diff --git a/src/grammar_pp.ml b/src/grammar_pp.ml index 3423c1f..a092de3 100644 --- a/src/grammar_pp.ml +++ b/src/grammar_pp.ml @@ -838,6 +838,9 @@ and pp_tex_terminal m xd tm = if (*(String.length es > 1) ||*) (Auxl.is_alpha tm) then pp_tex_KW_NAME m ^ "{"^es^"}" else pp_tex_SYM_NAME m ^"{"^es ^"}" +(* rst stuff *) +and rst_rule_name m ntr = ntr + and pp_isa_terminal m xd tm = try (* firstcheck if this terminal is defined in the terminalsproduction *) let term_rule = Auxl.rule_of_ntr xd "terminals" in @@ -914,6 +917,7 @@ and pp_terminal m xd tm = match m with | Ascii ao -> col_green ao (quote_ident tm) | Tex _ -> pp_tex_terminal m xd tm + | Rst _ -> tm | Coq _ -> tm | Isa _ -> pp_isa_terminal m xd tm | Hol _ -> tm @@ -927,6 +931,7 @@ and pp_terminal_unquoted m xd tm = match m with | Ascii ao -> col_green ao tm | Tex _ -> pp_tex_terminal m xd tm + | Rst _ -> tm | Coq _ -> tm | Isa _ -> pp_isa_terminal m xd tm | Hol _ -> tm @@ -1090,7 +1095,7 @@ and pp_nt_or_mv_with_sie_internal as_type m xd sie (ntmv,suff) = and pp_nt_or_mv_with_de_with_sie_internal as_type m xd sie (de :dotenv) ((ntmvr,suff0) as ntmv) = match m with - | Ascii _ | Tex _ -> pp_nt_or_mv_with_sie_internal as_type m xd sie ntmv + | Ascii _ | Tex _ | Rst _ -> pp_nt_or_mv_with_sie_internal as_type m xd sie ntmv | Isa _ | Coq _ | Hol _ | Lem _ | Twf _ | Caml _ | Rdx _ | Lex _ | Menhir _ -> let (de1,de2) = de in match try Some(List.assoc ntmv de2) with Not_found -> None with @@ -1267,6 +1272,7 @@ and pp_metavardefn m xd mvd = (function (mvr,homs)->pp_metavarroot m xd mvr) mvd.mvd_names)) ^ " $ & " ^ pp_com ^ " \\\\" + | Rst _ -> "" (* TODO do we need to show metavariables ? *) | _ -> ( match mvd.mvd_phantom with | true -> "" @@ -1315,8 +1321,7 @@ and pp_metavardefn m xd mvd = ^ " : type = nat.\n" | Lex _ -> "" | Menhir _ -> "" - | Rst _ -> "" - | Ascii _ | Tex _ -> raise Auxl.ThisCannotHappen )) + | Ascii _ | Tex _ | Rst _ -> raise Auxl.ThisCannotHappen )) and pp_metavarrep m xd mvd_rep type_name = match m with @@ -2736,6 +2741,9 @@ and pp_rule m xd r = (* returns a string option *) r.rule_ps))) (* ^"[5.0mm]" *) ^ "}\n" )) + | Rst ro -> Some ("::\n\n"^ + "\t"^(rst_rule_name m r.rule_ntr_name)^" ::= "^ + "\n") (* TODO *) in match result with | Some s -> Some (if !Global_option.output_source_locations >= 2 then "\n"^pp_source_location m r.rule_loc ^ s else s) @@ -2880,7 +2888,7 @@ and pp_rule_list m xd rs = rs) ^ (match rs with []-> "" | _ -> pp_tex_AFTERLASTRULE_NAME m) ^ "\n"^pp_tex_END_RULES ^ "}\n\n" - | Rst ro -> "" (* TODO *) + | Rst ro -> "" (* String.concat "\n" (Auxl.option_map (pp_rule m xd) rs) *) (* TODO do we want to display all these pesky rules ? *) | Lex _ | Menhir _ -> String.concat "\n" (Auxl.option_map (pp_rule m xd) rs) @@ -3011,6 +3019,7 @@ and pp_syntaxdefn m xd = ^ String.concat "\n" (List.map (pp_metavardefn m xd) xd.xd_mds) ^ "\n"^pp_tex_END_METAVARS ^"}\n\n" (* ^ "\\end{array}\\]\n" *) ^ pp_rule_list m xd xd.xd_rs + | Rst _ -> "" (* TODO *) | Lex _ | Menhir _ -> "<>" @@ -3211,7 +3220,7 @@ and pp_symterm_node_body m xd sie de stnb : string = | None -> let include_terminals = match m with - | Ascii _ | Tex _ | Lex _ | Menhir _ -> true + | Ascii _ | Tex _ | Lex _ | Rst _ | Menhir _ -> true | Coq _ | Isa _ | Hol _ | Lem _ | Rdx _ | Twf _ -> false | Caml oo -> oo.ppo_include_terminals in let pp_es' () = pp_symterm_elements' m xd sie de include_terminals prod_es stnb.st_es in @@ -3223,6 +3232,7 @@ and pp_symterm_node_body m xd sie de stnb : string = ( match stnb.st_prod_name with | "formula_dots" -> String.concat " \\quad " (pp_es()) | _ -> pp_tex_insert_spacing (pp_es'())) + | Rst _ -> String.concat " " (pp_es ()) (* TODO *) | Isa _ | Hol _ | Lem _ | Coq _ | Twf _ | Rdx _ | Caml _ -> ( match stnb.st_prod_name with @@ -3250,7 +3260,7 @@ and pp_symterm_node_body m xd sie de stnb : string = pp_symterm_element_judge_hol_plain m xd sie de p'' stnb'' | Lem lo -> pp_symterm_element_judge_lem_plain m xd sie de p'' stnb'' - | Ascii _ | Tex _ | Lex _ | Menhir _ -> raise ThisCannotHappen + | Ascii _ | Tex _ | Lex _ | Rst _ | Menhir _ -> raise ThisCannotHappen | Caml _ -> Auxl.error "internal: Caml pp_symterm for proper symterms not supported" ) | _ -> raise (Invalid_argument ("pp_symterm_node_body2: strange production in formula_judgement"))) @@ -3270,7 +3280,7 @@ and pp_symterm_node_body m xd sie de stnb : string = | "formula_dots" -> (match m with - | Ascii _ | Tex _ | Lex _ | Menhir _ -> Auxl.errorm m "formula_dots" + | Ascii _ | Tex _ | Rst _ | Lex _ | Menhir _ -> Auxl.errorm m "formula_dots" | Caml _ -> Auxl.error "internal: Caml pp_symterm for proper symterms not supported" | Isa io -> (match isa_fancy_syntax_hom_for_prod m xd io p with @@ -3705,7 +3715,7 @@ and pp_symterm_list_items m xd sie (de :dotenv) tmopt prod_es stlis : (string * let include_terminals = match m with - | Ascii _ | Tex _ | Lex _ | Menhir _ -> true + | Ascii _ | Tex _ | Rst _ | Lex _ | Menhir _ -> true | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Rdx _ -> false | Caml oo -> oo.ppo_include_terminals in let tmopt' = @@ -3716,6 +3726,7 @@ and pp_symterm_list_items m xd sie (de :dotenv) tmopt prod_es stlis : (string * | [] -> (match m with | Ascii ao -> if ao.ppa_ugly then [col_magenta ao "[empty stlis]",TTC_dummy] else ["",TTC_dummy] | Tex _ -> ["\\,",TTC_space] + | Rst _ -> ["\\,",TTC_space] | Isa _ -> ["[]",TTC_dummy] | Caml _ -> ["[]",TTC_dummy] | Lem _ -> ["[]",TTC_dummy] @@ -3730,7 +3741,7 @@ and pp_symterm_list_items m xd sie (de :dotenv) tmopt prod_es stlis : (string * | _ -> match m with | Lex _ | Menhir _ -> assert false - | Ascii _ | Tex _ -> + | Ascii _ | Tex _ | Rst _ -> let ss = Auxl.list_concat tmopt' (List.map (pp_symterm_list_item m xd sie de tmopt include_terminals prod_es) stlis) in @@ -3788,7 +3799,7 @@ and pp_symterm_list_items m xd sie (de :dotenv) tmopt prod_es stlis : (string * ^ ")" ] else [ List.hd l ] | Twf _ -> raise TwelfNotImplemented - | Lex _ | Menhir _ | Tex _ | Ascii _ -> raise ThisCannotHappen) + | Lex _ | Menhir _ | Tex _ | Rst _ | Ascii _ -> raise ThisCannotHappen) ) and pp_symterm_list_item m xd sie (de :dotenv) tmopt include_terminals prod_es stli : (string * tex_token_category) list = @@ -3810,7 +3821,7 @@ and pp_symterm_list_item m xd sie (de :dotenv) tmopt include_terminals prod_es s let pp_es = List.map fst pp_es' in (match m with | Ascii ao -> if ao.ppa_ugly then [col_magenta ao "[stli_single",TTC_dummy] @ pp_es' @ [col_magenta ao "stli_single]",TTC_dummy] else pp_es' - | Tex _ -> pp_es' + | Rst _ | Tex _ -> pp_es' | Caml _ | Isa _ | Hol _ | Lem _ -> ["[(" ^ String.concat "," pp_es ^ ")]",TTC_dummy] | Coq co -> diff --git a/src/system_pp.ml b/src/system_pp.ml index b872e17..4587911 100644 --- a/src/system_pp.ml +++ b/src/system_pp.ml @@ -219,7 +219,7 @@ let pp_struct_entry fd m sd xd_expanded lookup stre : unit = (List.map (fun mvs -> " (" ^mvs^" variable-not-otherwise-mentioned)\n") !(ro.ppr_metavars))); output_string fd (")\n"); - | _ -> () ); + | _ -> () ); (* induction_principles_rules *) ( match m with | Coq co when not co.coq_expand_lists -> @@ -418,6 +418,9 @@ let pp_systemdefn fd m sd lookup fn = | Lem lo -> Printf.fprintf fd "(* generated by Ott %s from: %s *)\n" Version.n sd.sources; pp_systemdefn_core fd m sd lookup + | Rst ro -> + Printf.fprintf fd ".. generated by Ott %s from: %s\n" Version.n sd.sources; + pp_systemdefn_core fd m sd lookup | Ascii _ | Lex _ | Menhir _ | Tex _ -> Auxl.errorm m "pp_systemdefn" From f62d6652fadc87d76c6b474f34e6c7d4f7ea76e3 Mon Sep 17 00:00:00 2001 From: Basile Pesin Date: Mon, 3 Jun 2019 16:12:11 +0200 Subject: [PATCH 3/8] Support for -merge true --- src/main.ml | 2 +- src/system_pp.ml | 6 +----- 2 files changed, 2 insertions(+), 6 deletions(-) diff --git a/src/main.ml b/src/main.ml index d992df8..0dfa5c1 100644 --- a/src/main.ml +++ b/src/main.ml @@ -785,7 +785,7 @@ let output_stage (sd,lookup,sd_unquotiented,sd_quotiented_unaux) = (Lex_menhir_pp.pp_menhir_syntaxdefn m_menhir sd.sources xd_quotiented xd_unquotiented lookup !generate_aux_rules fi; Lex_menhir_pp.pp_pp_syntaxdefn m_menhir sd.sources xd_quotiented xd_unquotiented xd_quotiented_unaux !generate_aux_rules fi ) | "rst" -> - System_pp.pp_systemdefn_core_io m_rst sd lookup fi !merge_fragments + System_pp.pp_systemdefn_core_io m_rst sd lookup fi false | _ -> Auxl.int_error("unknown target "^t)) diff --git a/src/system_pp.ml b/src/system_pp.ml index 4587911..ec93247 100644 --- a/src/system_pp.ml +++ b/src/system_pp.ml @@ -418,10 +418,7 @@ let pp_systemdefn fd m sd lookup fn = | Lem lo -> Printf.fprintf fd "(* generated by Ott %s from: %s *)\n" Version.n sd.sources; pp_systemdefn_core fd m sd lookup - | Rst ro -> - Printf.fprintf fd ".. generated by Ott %s from: %s\n" Version.n sd.sources; - pp_systemdefn_core fd m sd lookup - | Ascii _ | Lex _ | Menhir _ | Tex _ -> Auxl.errorm m "pp_systemdefn" + | Ascii _ | Lex _ | Menhir _ | Tex _ | Rst _ -> Auxl.errorm m "pp_systemdefn" (* multi-file stuff *) @@ -632,4 +629,3 @@ let pp_systemdefn_core_tex m sd lookup oi = close_out fd; | _ -> Auxl.error "must specify only one output file in the TeX backend.\n" - From bdc43955b44c232b69fa0d08a5ab820cd2cfbff2 Mon Sep 17 00:00:00 2001 From: Basile Pesin Date: Mon, 3 Jun 2019 17:52:51 +0200 Subject: [PATCH 4/8] Displaying grammar rules --- src/defns.ml | 17 ++++++++--------- src/grammar_pp.ml | 37 ++++++++++++++++++++++++++++--------- src/system_pp.ml | 2 +- 3 files changed, 37 insertions(+), 19 deletions(-) diff --git a/src/defns.ml b/src/defns.ml index 3bbf3a3..6a3861a 100644 --- a/src/defns.ml +++ b/src/defns.ml @@ -243,7 +243,7 @@ let pp_drule fd (m:pp_mode) (xd:syntaxdefn) (dr:drule) : unit = (Grammar_pp.pp_tex_DRULE_NAME_NAME m) (Auxl.pp_tex_escape dr.drule_name) pp_com - | Rst _ -> print_endline "rule" (* TODO *) + | Rst _ -> () (* TODO *) | Isa _ | Hol _ | Lem _ | Coq _ | Twf _ | Rdx _ -> let non_free_ntrs = Subrules_pp.non_free_ntrs m xd xd.xd_srs in @@ -563,14 +563,14 @@ let pp_defn fd (m:pp_mode) (xd:syntaxdefn) lookup (defnclass_wrapper:string) (un d.d_rules; Printf.fprintf fd "\\end{%s}}\n\n" (Grammar_pp.pp_tex_DEFN_BLOCK_NAME m) | Rst _ -> - Printf.fprintf fd ".. defn %s\n" d.d_name; + let ascii_mode = (Ascii {ppa_colour = false; + ppa_ugly = false; + ppa_lift_cons_prefixes = false; + ppa_show_deps = false; + ppa_show_defns = false; }) in + Printf.fprintf fd "**defn %s :** ``%s``\n\n" d.d_name (Grammar_pp.pp_symterm ascii_mode xd [] de_empty d.d_form); List.iter (function | PSR_Rule dr -> - let ascii_mode = (Ascii {ppa_colour = false; - ppa_ugly = false; - ppa_lift_cons_prefixes = false; - ppa_show_deps = false; - ppa_show_defns = false; }) in Printf.fprintf fd "%s::\n\n" dr.drule_name; let premises_str = List.map (fun (_, p) -> Grammar_pp.pp_symterm ascii_mode xd [] de_empty p) dr.drule_premises and conclusion_str = (Grammar_pp.pp_symterm ascii_mode xd [] de_empty dr.drule_conclusion) in @@ -715,9 +715,8 @@ let pp_defnclass fd (m:pp_mode) (xd:syntaxdefn) lookup (dc:defnclass) = output_string fd "{}") dc.dc_defns; output_string fd "}\n\n" | Rst _ -> - Printf.fprintf fd ".. defns %s\n" dc.dc_name; + Printf.fprintf fd "defns %s:\n%s\n\n" dc.dc_name (String.make (String.length dc.dc_name + 10) '^'); List.iter (fun d -> pp_defn fd m xd lookup dc.dc_wrapper universe d) dc.dc_defns - (* TODO *) (**********************************************) (* pp of fundefns *) diff --git a/src/grammar_pp.ml b/src/grammar_pp.ml index a092de3..078a213 100644 --- a/src/grammar_pp.ml +++ b/src/grammar_pp.ml @@ -838,9 +838,6 @@ and pp_tex_terminal m xd tm = if (*(String.length es > 1) ||*) (Auxl.is_alpha tm) then pp_tex_KW_NAME m ^ "{"^es^"}" else pp_tex_SYM_NAME m ^"{"^es ^"}" -(* rst stuff *) -and rst_rule_name m ntr = ntr - and pp_isa_terminal m xd tm = try (* firstcheck if this terminal is defined in the terminalsproduction *) let term_rule = Auxl.rule_of_ntr xd "terminals" in @@ -902,12 +899,12 @@ and pp_uninterpreted m xd s = and pp_maybe_quote_ident m xd s = match m with - | Ascii ao -> quote_ident s + | Ascii _ | Rst _ -> quote_ident s | Tex _ | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> s and pp_prod_flavour m xd pf = match m with - | Ascii _ -> pp_BAR + | Ascii _ | Rst _ -> pp_BAR | Tex _ -> pp_tex_BAR | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen @@ -2492,6 +2489,24 @@ and pp_prod m xd rnn rpw p = (* returns a string option *) (* ^ pp_categories_and_name m xd pcs pn *) ^ pn ^ " " ^String.concat " " (List.map (pp_homomorphism m xd) p.prod_homs)) + | Rst ro -> + let pn = p.prod_name in + let pp_prod m'= + let stnb = canonical_symterm_node_body_of_prod rnn p in + let st = St_node(dummy_loc,stnb) in + pp_symterm m' xd [] de_empty st + in + let ascii_mode = (Ascii {ppa_colour = false; + ppa_ugly = false; + ppa_lift_cons_prefixes = false; + ppa_show_deps = false; + ppa_show_defns = false; }) in + Some + ((pad2 60 + (pp_prod_flavour ascii_mode xd p.prod_flavour ^ " " + ^ (pp_prod (ascii_mode))) + (pp_prod_flavour ascii_mode xd p.prod_flavour ^ " " + ^ (pp_prod ascii_mode )))) | Isa io -> if p.prod_meta then None @@ -2741,9 +2756,12 @@ and pp_rule m xd r = (* returns a string option *) r.rule_ps))) (* ^"[5.0mm]" *) ^ "}\n" )) - | Rst ro -> Some ("::\n\n"^ - "\t"^(rst_rule_name m r.rule_ntr_name)^" ::= "^ - "\n") (* TODO *) + | Rst ro -> + let names = (String.concat ", " (List.map fst r.rule_ntr_names)) in + let name = ("::\n\n\t"^names^" ::= ") in + let prods = (List.fold_left (fun a so -> match so with | Some s -> a^"\n\t"^(String.make (String.length names + 1) ' ')^s | None -> a) "" + (List.map (pp_prod m xd r.rule_ntr_name r.rule_pn_wrapper) r.rule_ps)) in + Some (name^prods^"\n\n") in match result with | Some s -> Some (if !Global_option.output_source_locations >= 2 then "\n"^pp_source_location m r.rule_loc ^ s else s) @@ -2888,7 +2906,8 @@ and pp_rule_list m xd rs = rs) ^ (match rs with []-> "" | _ -> pp_tex_AFTERLASTRULE_NAME m) ^ "\n"^pp_tex_END_RULES ^ "}\n\n" - | Rst ro -> "" (* String.concat "\n" (Auxl.option_map (pp_rule m xd) rs) *) (* TODO do we want to display all these pesky rules ? *) + | Rst ro -> + (String.concat "\n" (Auxl.option_map (pp_rule m xd) rs)) | Lex _ | Menhir _ -> String.concat "\n" (Auxl.option_map (pp_rule m xd) rs) diff --git a/src/system_pp.ml b/src/system_pp.ml index ec93247..642de95 100644 --- a/src/system_pp.ml +++ b/src/system_pp.ml @@ -190,7 +190,7 @@ let pp_library fd m = | Twf wo -> pp_lib wo.twf_library | Caml oo-> pp_lib oo.caml_library | Rdx ro -> () - | Rst _ -> () (* TODO *) + | Rst _ -> () | Ascii _ | Tex _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_library" let pp_struct_entry fd m sd xd_expanded lookup stre : unit = From bd01a33fda19604360d841c6765b7c263b7bbb35 Mon Sep 17 00:00:00 2001 From: Basile Pesin Date: Mon, 3 Jun 2019 18:18:18 +0200 Subject: [PATCH 5/8] Added sort to take the grammar rules to the top --- src/system_pp.ml | 26 +++++++++++++++++++++++++- 1 file changed, 25 insertions(+), 1 deletion(-) diff --git a/src/system_pp.ml b/src/system_pp.ml index 642de95..3a12a48 100644 --- a/src/system_pp.ml +++ b/src/system_pp.ml @@ -334,8 +334,32 @@ let pp_struct_entry fd m sd xd_expanded lookup stre : unit = Embed_pp.pp_embeds fd m sd.syntax lookup [embed] (* FIXME should be a list *) ) +(* Pull the grammar rules at the top of the list *) +let rec select_struct l = match l with + | [] -> (None, []) + | (Struct_rs e)::l -> (Some (Struct_rs e), l) + | (Struct_srs e)::l -> (Some (Struct_srs e), l) + | (Struct_crs e)::l -> (Some (Struct_crs e), l) + | t::l -> let (res, l) = select_struct l in (res, t::l) + +let rec select_sort_struct l = match l with + | [] -> [] + (* Keep grammar rules ar the beginning *) + | (Struct_rs e)::l -> (Struct_rs e)::(select_sort_struct l) + | (Struct_srs e)::l -> (Struct_srs e)::(select_sort_struct l) + | (Struct_crs e)::l -> (Struct_crs e)::(select_sort_struct l) + | t::l -> let (e, l) = select_struct l in match e with + | Some e -> e::(select_sort_struct (t::l)) + | None -> t::l +(* *) + let pp_systemdefn_structure fd m sd xd_expanded structure_expanded lookup = - List.iter (fun (_,x) -> pp_struct_entry fd m sd xd_expanded lookup x) structure_expanded + let structure_expanded = match m with + | Rst _ -> ( + select_sort_struct (List.map (fun (_, x) -> x) structure_expanded) + ) + | _ -> List.map (fun (_, x) -> x) structure_expanded + in List.iter (pp_struct_entry fd m sd xd_expanded lookup) structure_expanded (* old algorithm that ignores the structure informations: core for isa/hol/coq/twf output *) let pp_systemdefn_core fd m sd lookup = From 362f2ae6b4f5f5f2753e095244c4da7d8a1d54da Mon Sep 17 00:00:00 2001 From: Basile Pesin Date: Tue, 4 Jun 2019 09:36:52 +0200 Subject: [PATCH 6/8] Changed the indent for grammar rules --- src/grammar_pp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/grammar_pp.ml b/src/grammar_pp.ml index 078a213..7e2d3c0 100644 --- a/src/grammar_pp.ml +++ b/src/grammar_pp.ml @@ -2759,7 +2759,7 @@ and pp_rule m xd r = (* returns a string option *) | Rst ro -> let names = (String.concat ", " (List.map fst r.rule_ntr_names)) in let name = ("::\n\n\t"^names^" ::= ") in - let prods = (List.fold_left (fun a so -> match so with | Some s -> a^"\n\t"^(String.make (String.length names + 1) ' ')^s | None -> a) "" + let prods = (List.fold_left (fun a so -> match so with | Some s -> a^"\n\t "^s | None -> a) "" (List.map (pp_prod m xd r.rule_ntr_name r.rule_pn_wrapper) r.rule_ps)) in Some (name^prods^"\n\n") in From 6e907e1103a0893380e958a5d10200000ec4d7a5 Mon Sep 17 00:00:00 2001 From: Basile Pesin Date: Tue, 4 Jun 2019 13:03:53 +0200 Subject: [PATCH 7/8] First version of split output --- src/main.ml | 10 ++++- src/system_pp.ml | 97 +++++++++++++++++++++++++++++++++++++++++++++-- src/system_pp.mli | 3 +- src/types.ml | 5 ++- 4 files changed, 107 insertions(+), 8 deletions(-) diff --git a/src/main.ml b/src/main.ml index 0dfa5c1..ad5d537 100644 --- a/src/main.ml +++ b/src/main.ml @@ -94,6 +94,7 @@ let coq_expand_lists = ref true let coq_lngen = ref false let coq_names_in_rules = ref true let coq_use_filter_fn = ref false +let rst_split_output = ref false let merge_fragments = ref false let picky_multiple_parses = ref false let caml_include_terminals = ref false @@ -257,6 +258,11 @@ let options = Arg.align [ Arg.Bool (fun b -> caml_include_terminals := b), "<"^string_of_bool !caml_include_terminals^"> Include terminals in OCaml output (experimental!)" ); + (* options for rst output *) + ( "-rst_split_output", + Arg.Bool (fun b -> rst_split_output := b), + ("<"^string_of_bool !rst_split_output^"> Split ReStructuredText output (one file per rule)" )); + (* options for debugging *) ( "-pp_grammar", Arg.Set Global_option.do_pp_grammar, @@ -414,7 +420,7 @@ let m_tex = Tex {ppt_colour= !tex_colour; ppt_suppressed_ntrs= !tex_suppressed_ntrs; ppt_wrap= !tex_wrap; ppt_name_prefix= !tex_name_prefix } -let m_rst = Rst () +let m_rst = Rst { split_output = !rst_split_output; } let m_isa = Isa { ppi_isa_primrec = !isa_primrec; ppi_isa_inductive = !isa_inductive; isa_library = ref ("",[]); @@ -785,7 +791,7 @@ let output_stage (sd,lookup,sd_unquotiented,sd_quotiented_unaux) = (Lex_menhir_pp.pp_menhir_syntaxdefn m_menhir sd.sources xd_quotiented xd_unquotiented lookup !generate_aux_rules fi; Lex_menhir_pp.pp_pp_syntaxdefn m_menhir sd.sources xd_quotiented xd_unquotiented xd_quotiented_unaux !generate_aux_rules fi ) | "rst" -> - System_pp.pp_systemdefn_core_io m_rst sd lookup fi false + System_pp.pp_systemdefn_core_rst m_rst sd lookup fi | _ -> Auxl.int_error("unknown target "^t)) diff --git a/src/system_pp.ml b/src/system_pp.ml index 3a12a48..b0c2c55 100644 --- a/src/system_pp.ml +++ b/src/system_pp.ml @@ -532,9 +532,6 @@ let pp_systemdefn_core_io m sd lookup oi merge_fragments = [ Embed_string (dummy_loc, ";;; generated by Ott "^Version.n^" from: "^file_sources^"\n\n" ^ "#lang racket\n(require redex)\n")] - | Rst _ -> - [ Embed_string (dummy_loc, - ".. generated by Ott "^Version.n^" from: "^file_sources^"\n")] | _ -> Auxl.errorm m "std_preamble_embed" )) @@ -653,3 +650,97 @@ let pp_systemdefn_core_tex m sd lookup oi = close_out fd; | _ -> Auxl.error "must specify only one output file in the TeX backend.\n" + +let pp_systemdefn_core_rst m sd lookup oi = + (* if -merge true, ignore the new algorithm *) + let is = snd(List.hd oi) in + (* synthesize an embed for the standard preamble *) + let std_preamble_embed fn = + let file_sources = + if is = [] then "no input files" else String.concat " " is in + (fn, Struct_embed + (dummy_loc, Auxl.hom_name_for_pp_mode m, + match m with + | Rst _ -> + [ Embed_string (dummy_loc, + ".. generated by Ott "^Version.n^" from: "^file_sources^"\n")] + | _ -> Auxl.errorm m "std_preamble_embed" + )) + in + + let xd_expanded, structure_expanded = + Transform.expand_lists_in_syntaxdefn m sd.syntax sd.structure in (* identity if m <> Coq *) + + (* special case if there is only one i file *) + match oi with + | (o,_)::[] -> + (match m with + | Rst ro -> + if ro.split_output then ( + let fn = let fn = (String.concat "/" (List.rev (List.tl (List.rev (String.split_on_char '/' o))))) in + if fn = "" then "." else fn in + List.iter (fun (_, entry) -> + match entry with + | Struct_rs ntrs -> + let rs = List.map (fun ntr -> Auxl.rule_of_ntr xd_expanded ntr) ntrs in + + List.iter (fun rule -> + let s = Grammar_pp.pp_rule m xd_expanded rule in + match s with + | Some s -> ( + let fd = open_out (fn^"/"^rule.rule_ntr_name^".rst") in + output_string fd s; + close_out fd + ) + | None -> () + ) rs; + + | Struct_fun_or_defnclass s -> + let frdc = + List.find + (fun frdc -> match frdc with + | FDC fdc -> if String.compare fdc.fdc_name s = 0 then true else false + | RDC dc -> if String.compare dc.dc_name s = 0 then true else false ) + sd.relations in + + (match frdc with + | FDC _ -> Auxl.warning "FDC not yet supported in rst output-splitting" + | RDC dc -> ( + print_endline dc.dc_name; + let universe = try Grammar_pp.pp_hom_spec m xd_expanded (List.assoc "coq-universe" dc.dc_homs) with Not_found -> "Prop" in + List.iter (fun d -> + let ascii_mode = (Ascii {ppa_colour = false; + ppa_ugly = false; + ppa_lift_cons_prefixes = false; + ppa_show_deps = false; + ppa_show_defns = false; }) in + List.iter (function + | PSR_Rule dr -> + let fd = open_out (fn^"/"^dr.drule_name^".rst") in + Printf.fprintf fd "%s::\n\n" dr.drule_name; + let premises_str = List.map (fun (_, p) -> Grammar_pp.pp_symterm ascii_mode xd_expanded [] de_empty p) dr.drule_premises + and conclusion_str = (Grammar_pp.pp_symterm ascii_mode xd_expanded [] de_empty dr.drule_conclusion) in + let len = List.fold_left (fun m s -> max m (String.length s)) 0 premises_str in + let len = max len (String.length conclusion_str) in + List.iter (Printf.fprintf fd "\t%s\n") premises_str; + Printf.fprintf fd "\t%s\n" (String.make len '-'); + Printf.fprintf fd "\t%s\n\n" conclusion_str; + close_out fd + | PSR_Defncom es -> Auxl.warning "PSR_Defncom not supported in rst output-splitting") + d.d_rules; + ) dc.dc_defns + )) + + | _ -> Auxl.warning "Struct not supported in rst output-splitting\n" + ) structure_expanded + ) else ( (* Default case *) + let fd = open_out o in + let fn = Auxl.filename_check m o in + pp_systemdefn_structure fd m sd xd_expanded ([std_preamble_embed fn]) lookup; + pp_auxiliary_lemmas m xd_expanded; + pp_systemdefn_structure fd m sd xd_expanded structure_expanded lookup; + output_string fd "\n\n"; + close_out fd +) + | _ -> Auxl.errorm m "pp_systemdefn_core_rst") +| _ -> Auxl.error "must specify only one output file in the Rst backend.\n" diff --git a/src/system_pp.mli b/src/system_pp.mli index 1ff974d..a3b6fe8 100644 --- a/src/system_pp.mli +++ b/src/system_pp.mli @@ -37,4 +37,5 @@ val pp_systemdefn_core_io : Types.pp_mode -> Types.systemdefn -> Types.made_parser -> (string * (string list)) list -> bool -> unit val pp_systemdefn_core_tex : Types.pp_mode -> Types.systemdefn -> Types.made_parser -> (string * (string list)) list -> unit - +val pp_systemdefn_core_rst : + Types.pp_mode -> Types.systemdefn -> Types.made_parser -> (string * (string list)) list -> unit diff --git a/src/types.ml b/src/types.ml index d27780d..9198334 100644 --- a/src/types.ml +++ b/src/types.ml @@ -861,8 +861,9 @@ type pp_menhir_opts = ppm_caml_parser_module : string; } (* yo *) -type pp_rst_opts = unit (* TODO *) - +type pp_rst_opts = + { split_output : bool; } + type pp_mode = (* m *) | Coq of pp_coq_opts | Isa of pp_isa_opts From 10d5a1ecf28f0366da5ce481caacffddee5515b9 Mon Sep 17 00:00:00 2001 From: Basile Pesin Date: Tue, 4 Jun 2019 13:56:08 +0200 Subject: [PATCH 8/8] Some aesthetic changes --- src/defns.ml | 23 +++++++++++++---------- src/defns.mli | 1 + src/system_pp.ml | 9 +-------- 3 files changed, 15 insertions(+), 18 deletions(-) diff --git a/src/defns.ml b/src/defns.ml index 6a3861a..6019b9a 100644 --- a/src/defns.ml +++ b/src/defns.ml @@ -478,6 +478,17 @@ let pp_processed_semiraw_rule fd (m:pp_mode) (xd:syntaxdefn) (s: string) (psr:pr | PSR_Rule dr -> output_string fd s; pp_drule fd m xd dr; true | PSR_Defncom _ -> false +let pp_drule_rst fd m dr xd = + Printf.fprintf fd "::\n\n"; + let premises_str = List.map (fun (_, p) -> Grammar_pp.pp_symterm m xd [] de_empty p) dr.drule_premises + and conclusion_str = (Grammar_pp.pp_symterm m xd [] de_empty dr.drule_conclusion) in + let len = List.fold_left (fun m s -> max m (String.length s)) 0 premises_str in + let len = max len (String.length conclusion_str) in + List.iter (Printf.fprintf fd "\t%s\n") premises_str; + Printf.fprintf fd "\t%s" (String.make len '-'); + Printf.fprintf fd " (%s)\n" dr.drule_name; + Printf.fprintf fd "\t%s\n\n" conclusion_str + let pp_defn fd (m:pp_mode) (xd:syntaxdefn) lookup (defnclass_wrapper:string) (universe:string) (d:defn) = match m with | Ascii _ -> @@ -571,20 +582,12 @@ let pp_defn fd (m:pp_mode) (xd:syntaxdefn) lookup (defnclass_wrapper:string) (un Printf.fprintf fd "**defn %s :** ``%s``\n\n" d.d_name (Grammar_pp.pp_symterm ascii_mode xd [] de_empty d.d_form); List.iter (function | PSR_Rule dr -> - Printf.fprintf fd "%s::\n\n" dr.drule_name; - let premises_str = List.map (fun (_, p) -> Grammar_pp.pp_symterm ascii_mode xd [] de_empty p) dr.drule_premises - and conclusion_str = (Grammar_pp.pp_symterm ascii_mode xd [] de_empty dr.drule_conclusion) in - let len = List.fold_left (fun m s -> max m (String.length s)) 0 premises_str in - let len = max len (String.length conclusion_str) in - List.iter (Printf.fprintf fd "\t%s\n") premises_str; - Printf.fprintf fd "\t%s\n" (String.make len '-'); - Printf.fprintf fd "\t%s\n\n" conclusion_str + pp_drule_rst fd ascii_mode dr xd; | PSR_Defncom es -> Embed_pp.pp_embed_spec fd m xd lookup es) d.d_rules; Printf.fprintf fd "\n" | Caml _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_defn" - let pp_defnclass fd (m:pp_mode) (xd:syntaxdefn) lookup (dc:defnclass) = let universe = try Grammar_pp.pp_hom_spec m xd (List.assoc "coq-universe" dc.dc_homs) with Not_found -> "Prop" in let isa_type_of_defn (m: pp_mode) (xd: syntaxdefn) (d: defn) : string = @@ -715,7 +718,7 @@ let pp_defnclass fd (m:pp_mode) (xd:syntaxdefn) lookup (dc:defnclass) = output_string fd "{}") dc.dc_defns; output_string fd "}\n\n" | Rst _ -> - Printf.fprintf fd "defns %s:\n%s\n\n" dc.dc_name (String.make (String.length dc.dc_name + 10) '^'); + Printf.fprintf fd "%s\n%s\n\n" dc.dc_name (String.make (String.length dc.dc_name + 5) '^'); List.iter (fun d -> pp_defn fd m xd lookup dc.dc_wrapper universe d) dc.dc_defns (**********************************************) diff --git a/src/defns.mli b/src/defns.mli index b1e928d..d145878 100644 --- a/src/defns.mli +++ b/src/defns.mli @@ -45,3 +45,4 @@ val process_raw_defnclasss : Types.syntaxdefn -> Types.made_parser -> Types.raw_fun_or_reln_defnclass list -> Types.fun_or_reln_defnclass list val pp_counts : Types.systemdefn -> bool * string +val pp_drule_rst : out_channel -> Types.pp_mode -> Types.drule -> Types.syntaxdefn -> unit diff --git a/src/system_pp.ml b/src/system_pp.ml index b0c2c55..3d823f8 100644 --- a/src/system_pp.ml +++ b/src/system_pp.ml @@ -717,14 +717,7 @@ let pp_systemdefn_core_rst m sd lookup oi = List.iter (function | PSR_Rule dr -> let fd = open_out (fn^"/"^dr.drule_name^".rst") in - Printf.fprintf fd "%s::\n\n" dr.drule_name; - let premises_str = List.map (fun (_, p) -> Grammar_pp.pp_symterm ascii_mode xd_expanded [] de_empty p) dr.drule_premises - and conclusion_str = (Grammar_pp.pp_symterm ascii_mode xd_expanded [] de_empty dr.drule_conclusion) in - let len = List.fold_left (fun m s -> max m (String.length s)) 0 premises_str in - let len = max len (String.length conclusion_str) in - List.iter (Printf.fprintf fd "\t%s\n") premises_str; - Printf.fprintf fd "\t%s\n" (String.make len '-'); - Printf.fprintf fd "\t%s\n\n" conclusion_str; + Defns.pp_drule_rst fd ascii_mode dr xd_expanded; close_out fd | PSR_Defncom es -> Auxl.warning "PSR_Defncom not supported in rst output-splitting") d.d_rules;