diff --git a/src/auxl.ml b/src/auxl.ml index 5c64e04..219a318 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 *) @@ -792,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 39d83d4..6019b9a 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 _ -> () (* TODO *) | Isa _ | Hol _ | Lem _ | Coq _ | Twf _ | Rdx _ -> let non_free_ntrs = Subrules_pp.non_free_ntrs m xd xd.xd_srs in @@ -477,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 _ -> @@ -561,9 +573,21 @@ 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 _ -> + 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 -> + 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 = @@ -693,6 +717,9 @@ 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 _ -> + 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 (**********************************************) (* pp of fundefns *) @@ -708,6 +735,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 +763,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 +867,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 +916,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 +939,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 +1034,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 _ -> + (* 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/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/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..7e2d3c0 100644 --- a/src/grammar_pp.ml +++ b/src/grammar_pp.ml @@ -899,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 @@ -914,6 +914,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 +928,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 @@ -1027,6 +1029,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 +1078,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 @@ -1089,7 +1092,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 @@ -1266,6 +1269,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 -> "" @@ -1312,9 +1316,9 @@ 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 _ -> "" + | Ascii _ | Tex _ | Rst _ -> raise Auxl.ThisCannotHappen )) and pp_metavarrep m xd mvd_rep type_name = match m with @@ -2485,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 @@ -2734,6 +2756,12 @@ and pp_rule m xd r = (* returns a string option *) r.rule_ps))) (* ^"[5.0mm]" *) ^ "}\n" )) + | 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 "^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) @@ -2810,7 +2838,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 +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)) | Lex _ | Menhir _ -> String.concat "\n" (Auxl.option_map (pp_rule m xd) rs) @@ -3008,6 +3038,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 _ -> "<>" @@ -3208,7 +3239,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 @@ -3220,6 +3251,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 @@ -3247,7 +3279,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"))) @@ -3267,7 +3299,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 @@ -3702,7 +3734,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' = @@ -3713,6 +3745,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] @@ -3727,7 +3760,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 @@ -3785,7 +3818,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 = @@ -3807,7 +3840,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 -> @@ -4366,4 +4399,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..ad5d537 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 @@ -91,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 @@ -146,6 +150,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" ); @@ -250,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, @@ -307,6 +320,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 +333,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 +349,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 +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 { split_output = !rst_split_output; } let m_isa = Isa { ppi_isa_primrec = !isa_primrec; ppi_isa_inductive = !isa_inductive; isa_library = ref ("",[]); @@ -515,7 +531,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 +790,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_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 9813e85..3d823f8 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 _ -> () | Ascii _ | Tex _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_library" let pp_struct_entry fd m sd xd_expanded lookup stre : unit = @@ -218,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 -> @@ -333,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 = @@ -417,7 +442,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 - | Ascii _ | Lex _ | Menhir _ | Tex _ -> Auxl.errorm m "pp_systemdefn" + | Ascii _ | Lex _ | Menhir _ | Tex _ | Rst _ -> Auxl.errorm m "pp_systemdefn" (* multi-file stuff *) @@ -626,3 +651,89 @@ let pp_systemdefn_core_tex m sd lookup oi = | _ -> 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 + 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; + ) 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 f08788a..9198334 100644 --- a/src/types.ml +++ b/src/types.ml @@ -860,7 +860,10 @@ type pp_menhir_opts = ppm_caml_ast_module : string; ppm_caml_parser_module : string; } (* yo *) - + +type pp_rst_opts = + { split_output : bool; } + type pp_mode = (* m *) | Coq of pp_coq_opts | Isa of pp_isa_opts @@ -873,6 +876,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;