<commit_before>open Syntax
open Format

type mode = ML | TeX

let mode = ref ML
let filename = ref ""

let spec = [("-TeX", Arg.Unit (fun () -> mode := TeX), "display rules in TeX")]

let parse_file s =
  Parser.toplevel Lexer.main (Lexing.from_channel (open_in s))

let emit_game g = 
  let env = Env.of_game g in
    printf "(* @["; 
    Syntax.Env.print_env env;
    printf "@] *)"; print_newline(); print_newline();
  print_string "open MySupport.Error"; print_newline ();
  print_string "open Derivation"; print_newline ();
  Emit.typedef env g.syndefs; print_newline ();
  Emit.jdgdef env g.jdgdecls; print_newline ();
  print_newline();
  Emit.rules env g.ruledefs;
  print_newline ()

let _ = 
  Arg.parse spec (fun s -> filename := s) "Usage: gmc [-TeX] filename";
  let g = parse_file !filename in
    match !mode with
	ML -> emit_game g
      | TeX -> Emit.tex_rules g.ruledefs


  
  
<commit_msg>prover generation.<commit_after>open Syntax
open Format

type mode = ML | TeX

let mode = ref ML
let filename = ref ""

let spec = [("-TeX", Arg.Unit (fun () -> mode := TeX), "display rules in TeX")]

let parse_file s =
  Parser.toplevel Lexer.main (Lexing.from_channel (open_in s))

let emit_game g = 
  let env = Env.of_game g in
    printf "(* @["; 
    Syntax.Env.print_env env;
    printf "@] *)"; print_newline(); print_newline();
  print_string "open MySupport.Error"; print_newline ();
  print_string "open Derivation"; print_newline ();
  Emit.typedef env g.syndefs; print_newline ();
  Emit.jdgdef env g.jdgdecls; print_newline ();
  print_newline();
  Emit.rules env g.ruledefs;
  print_newline ();  print_newline ();
  (* experimental prover generation *)
  Emit.Prover.emit_jdgdef env g.jdgdecls; print_newline();
  print_string "let dummy = Lexing.dummy_pos"; print_newline();
  Emit.Prover.emit env g.ruledefs

let _ = 
  Arg.parse spec (fun s -> filename := s) "Usage: gmc [-TeX] filename";
  let g = parse_file !filename in
    match !mode with
	ML -> emit_game g
      | TeX -> Emit.tex_rules g.ruledefs

{'fraction_non_alphanumeric': 0.13343180699162974, 'fraction_numerical': 0.0, 'mean_word_length': 3.5458612975391497, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 11, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '703267', 'n_tokens_mistral': 761, 'n_tokens_neox': 728, 'n_words': 205}