main.ml

(* Main program for translating HOL-Light proofs to Dedukti or Lambdapi. *)

open Fusion
open Xlib
open Xprelude
open Xproof
open Xfiles
open Xnames

let usage() =
  print_string
"hol2dk uses
------------

hol2dk [-h|--help]
  print this help

hol2dk options command arguments

Options
-------

--root-path MODNAME: set lambdapi and coq's root_path (default to HOLLight)

--max-dup INT: maximum number of theorem duplications

--max-proof-size INT: maximum size of proof files (default to 500_000)

--max-abbrev-size INT: maximum size of term abbreviation files (default to 2_000_000)

--use-sharing: define term abbreviations using let's

--print-stats: print statistics on hash tables at exit

Patching commands
-----------------

hol2dk patch
  patch the $HOLLIGHT_DIR sources

hol2dk unpatch
  unpatch the $HOLLIGHT_DIR sources

Dumping commands
----------------

hol2dk dump-simp $base.(ml|hl)
  compose the commands dump, pos, use, rewrite and purge
  for a file $base.(ml|hl) depending on hol.ml

hol2dk dump-simp-before-hol $base.(ml|hl)
  same as hol2dk dump-simp except that hol.ml is not loaded first

hol2dk dump $base.(ml|hl)
  run OCaml toplevel to check $base.(ml|hl) and generate
  $base.sig (type and term constants), $base.prf (proof steps)
  and $base.thm (named theorems)

hol2dk dump-before-hol $base.(ml|hl)
  same as hol2dk dump except that hol.ml is not loaded first

hol2dk pos $base
  generate $base.pos, the positions of proof steps in $base.prf

hol2dk use $base
  generate $base.use, some data to know whether a proof step is used or not

hol2dk rewrite $base
  simplify $base.prf and update $base.pos and $base.use

hol2dk purge $base
  set as unused the proof steps that do not contribute to a named theorem

Single-threaded dk/lp file generation
-------------------------------------

hol2dk $base.(dk|lp)
  generate $base.(dk|lp)

hol2dk $base.(dk|lp) $thm_id
  generate $base.(dk|lp) but with theorem index $thm_id only (for debug)

Multi-threaded lp file generation with a file for each named theorem
--------------------------------------------------------------------

hol2dk config hollight_file.ml root_path [coq_module_or_file ...] [mappings.lp] [mappings.mk]
  create files and links to the files generated by hol2dk dump
  in $HOLLIGHT_DIR and to the $HOL2DK_DIR files needed to translate
  hollight_file.prf to Dedukti, Lambdapi and Coq, and check the obtained files
  (do hol2dk config without arguments to get more details)
 
hol2dk split $base
  generate $base.thp and the files $thm.sti, $thm.pos, $thm.use and $thm.nbp
  for each theorem $thm in $base

hol2dk unsplit $base $module ...
  for each file $module, generate the files $module.sti, $module.pos,
  $module.use, $module.nbp and, for each theorem $thm proved in
  $HOLLIGHT_DIR/$module.ml, remove the files $thm.sti, $thm.pos, $thm.use and
  $thm.nbp, and update $base.thp

hol2dk theorem $base $thm.lp
  generate the lp proof of the theorem $thm

hol2dk thmsplit $base $thm.lp
  split the proof of $thm in various pieces according to --max-proof-size

hol2dk thmpart $base ${thm}_part_$k.lp
  generate ${thm}_part_$k.lp and record its term abbreviations
  according to --max-abbrev-size

hol2dk abbrev $base ${thm}_term_abbrevs_part_$k.lp
  generate ${thm}_term_abbrevs_part_$k.lp

hol2dk type_abbrevs $base
  generate ${file}_type_abbrevs.lp

hol2dk tvs $base
  generate $base.tvs

Multi-threaded dk/lp file generation by splitting proofs in $n parts
--------------------------------------------------------------------

hol2dk mk $n $base
  generate $base.dg, the dependency graph between parts when $base.prf is
  split in $n parts, and the Makefile $base.mk for translating and checking
  those parts in parallel

hol2dk part $k $x $y $base.(dk|lp)
  generate dk/lp proof files of part $k from proof index $x to proof index $y

hol2dk sig $base
  generate dk/lp signature files from $base.sig

hol2dk thm $base.(dk|lp)
  generate $base.(dk|lp)

Other commands
--------------

hol2dk axm $base.(dk|lp)
  generate ${base}_opam.(dk|lp) with all the statements of all the theorems
  but without proofs

hol2dk files [$path/]$base.(dk|lp)
  for each HOL-Light file required by $HOLLIGHT_DIR/$path/$base.ml, generate
  a (dk|lp) file with the statements of the theorems proved in that file

hol2dk env
  print the values of $HOL2DK_DIR and $HOLLIGHT_DIR

hol2dk nbp $base
  print the number of useful proof steps in $base.prf

hol2dk proof $base $x [$y]
  print proof steps between theorem indexes $x and $y

hol2dk print use $base $x
  print the contents of $base.use for theorem index $x

hol2dk print $file.tvs
  print the contents of $file.tvs (number of type parameters of each symbol)

hol2dk print $file.thm
  print the contents of $file.thm (named theorems with their indexes)

hol2dk thms $base [$path/]$file.(ml|hl)
  print the list of theorems (named or not) proved in [$path/]$file.(ml|hl)

hol2dk stat $base [$thm]
  print statistics on proof steps

hol2dk size $base [$lower_bound]
  print statistics on the size of terms
  and the number of terms of size greater than $lower_bound

hol2dk dep
  print on stdout a Makefile giving the dependencies of all HOL-Light files
  in the working directory and all its subdirectories recursively

hol2dk dep [$path/]$base.(ml|hl)
  print the HOL-Light files required to check [$path/]$base.(ml|hl)

hol2dk name [$path/]$base.(ml|hl)
  print the named theorems proved in [$path/]$base.(ml|hl)

hol2dk name upto [$path/]$base.(ml|hl)
  print the named theorems proved in [$path/]$base.(ml|hl)
  and all its dependencies

hol2dk name
  print on stdout the named theorems proved in all HOL-Light files
  in the working directory and all its subdirectories recursively
"

let is_dk f =
  match Filename.extension f with
  | ".dk"  -> true
  | ".lp" -> false
  | _ -> err "\"%s\" does not end with \".dk\" or \".lp\"\n" f; exit 1
;;

let read_sig b =
  let dump_file = b^".sig" in
  let ic = open_in_bin dump_file in
  log_read dump_file;
  the_type_constants := List.rev (input_value ic);
  (* we add "el" to use mk_const without failing *)
  the_term_constants := ("el",aty)::List.rev (input_value ic);
  the_axioms := List.rev (input_value ic);
  the_definitions := List.rev (input_value ic);
  close_in ic;
  update_map_const_typ_vars_pos();
  update_reserved()
;;

let integer s =
  try int_of_string s
  with Failure _ ->
    Printf.eprintf "\"%s\" is not a valid integer\n" s; exit 1
;;

(* [make nb_proofs dg b] generates a makefile for translating the
   proofs of [b] in parallel, according to the dependency graph
   between parts [dg]. *)
let make nb_proofs dg b =
  let nb_parts = Array.length dg in
  let dump_file = b^".mk" in
  log_gen dump_file;
  let oc = open_out dump_file in
  out oc "# file generated with: hol2dk mkfile %s\n" b;
  out oc "\nNB_PARTS := %d\n" nb_parts;
  out oc "\ninclude part.mk\n\n";
  let cmd i x y =
    out oc "$(BASE)_part_%d.dk $(BASE)_part_%d_type_abbrevs.dk \
            $(BASE)_part_%d_term_abbrevs.dk &:\n\
            \thol2dk part %d %d %d $(BASE).dk\n" i i i i x y;
    out oc "$(BASE)_part_%d.lp $(BASE)_part_%d_term_abbrevs.lp &:\n\
            \thol2dk part %d %d %d $(BASE).lp\n" i i i x y
  in
  Xlib.iter_parts nb_proofs nb_parts cmd;
  close_out oc
;;

let range args =
  match args with
  | [] -> All
  | [x] ->
     let x = integer x in
     if x < 0 then (err "%d is negative\n" x; exit 1);
     Only x
  | [x;y] ->
     let x = integer x in
     if x < 0 then (err "%d is negative\n" x; exit 1);
     let y = integer y in
     if y < x then (err "%d is smaller than %d\n" y x; exit 1);
     if x=0 then Upto y else Inter(x,y)
  | _ -> (err "too many arguments\n"; exit 1)
;;

let dump after_hol f b =
  let ml_file = "dump.ml" in
  log_gen ml_file;
  let oc = open_out ml_file in
  let use oc after_hol =
    if after_hol then out oc "#use \"hol.ml\";;\nneeds \"%s\";;" f
    else out oc "#use \"%s\";;" f
  in
  let dg = dep_graph "" (files ".") in
  let deps = trans_file_deps dg (if after_hol then ["hol.ml";f] else [f]) in
  let cmd oc after_hol =
    if after_hol then out oc " dump" else out oc " dump-before-hol" in
  out oc
{|(* file generated with: hol2dk%a %s *)
#use "topfind";;
#require "str";;
#require "zarith";;
#require "unix";;
#load "bignum.cmo";;
let dump_filename = "%s.prf";;
%a
close_out oc_dump;;
dump_nb_proofs "%s.nbp";;
dump_signature "%s.sig";;
#use "xnames.ml";;
dump_map_thid_name "%s.thm" %a;;
|} cmd after_hol f b use after_hol b b b (olist ostring) deps;
  close_out oc;
  Xlib.command ("ocaml -w -A -I . "^ml_file)
;;

let basename_ml f =
  match Filename.extension f with
  | ".ml" | ".hl" -> Filename.chop_extension f
  | _ -> err "\"%s\" does not end with \".ml\" or \".hl\"\n" f; exit 1
;;

let print_hstats() =
  log "\nstring: %a\ntype: %a\nterm: %a\ntype_abbrev: %a\nterm_abbrev: %a\
       \nsubterms: %a\nabbrev_part: %a\npart_abbrev_max: %a"
    hstats (StrHashtbl.stats htbl_string)
    hstats (TypHashtbl.stats htbl_type)
    hstats (TrmHashtbl.stats htbl_term)
    hstats (TypHashtbl.stats htbl_type_abbrev)
    hstats (TrmHashtbl.stats htbl_term_abbrev)
    hstats (TrmHashtbl.stats htbl_subterms)
    hstats (Hashtbl.stats Xlp.htbl_abbrev_part)
    hstats (Hashtbl.stats Xlp.htbl_abbrev_part_max)
;;

let call_script s args =
  match Sys.getenv_opt "HOL2DK_DIR" with
  | None -> err "set $HOL2DK_DIR first\n"; exit 1
  | Some d -> exit (Sys.command ("sh "^d^"/"^s^" "^String.concat " " args))
;;

let print_env_var n =
  match Sys.getenv_opt n with
  | None -> log "%s is undefined\n" n
  | Some v -> log "%s = \"%s\"\n" n v
;;

let wrong_nb_args() = err "wrong number of arguments\n"; exit 1;;

(* compute the minimum and maximum theorem indexes in f *)
let thid_range map_name_thid f =
  let min_id = ref max_int and max_id = ref min_int in
  List.iter
    (fun n ->
      try
        let k = MapStr.find n map_name_thid in
        min_id := min !min_id k;
        max_id := max !max_id k
      with Not_found -> ())
    (thms_of_file f);
  if !min_id > !max_id then
    (err "\"%s\" has no recorded named theorem.\n" f; exit 1);
  !min_id, !max_id
;;

let inverse map_thid_name =
  MapInt.fold (fun k n map -> MapStr.add n k map) map_thid_name MapStr.empty
;;

let valid_coq_filename s = match s with "at" -> "_"^s | _ -> s;;

let thm_name map_thid_name k =
  try valid_coq_filename (MapInt.find k map_thid_name)
  with Not_found -> "thm"^string_of_int k
;;

let create_segment n start_index end_index =
  let len = end_index - start_index + 1 in
  write_val (n^".nbp") len;
  write_val (n^".sti") start_index;
  write_val (n^".pos") (Array.sub !prf_pos start_index len);
  write_val (n^".use") (Array.sub !last_use start_index len)
;;

(* maximum number of proof duplications before creating a new theorem *)
let max_dup = ref max_int;;

let rec log_command l =
  print_string "\nhol2dk";
  List.iter (fun s -> print_char ' '; print_string s) l;
  print_string " ...\n";
  flush stdout;
  command l

and dump_and_simp after_hol f =
  let b = basename_ml f in
  dump after_hol f b;
  log_command ["pos";b];
  log_command ["use";b];
  command ["simp";b]

and command = function
  | [] | ["-h"|"--help"|"help"] -> usage()

  | "--print-stats"::args -> at_exit print_hstats; command args

  | "--use-sharing"::args -> use_sharing := true; command args

  | "--max-abbrev-size"::k::args ->
     Xlp.max_abbrev_part_size := integer k; command args

  | ["--max-abbrev-size"] -> wrong_nb_args()

  | "--max-proof-size"::k::args ->
     Xlp.max_proof_part_size := integer k; command args

  | ["--max-proof-size"] -> wrong_nb_args()

  | "--max-dup"::k::args -> max_dup := integer k; command args
  | ["--max-dup"] -> wrong_nb_args()

  | "--root-path"::arg::args -> Xlp.root_path := arg; command args

  | ["--root-path"] -> wrong_nb_args()

  | s::_ when String.starts_with ~prefix:"--" s ->
     err "unknown option \"%s\"\n" s; exit 1

  (* Print dependencies of the ml file f. *)
  | ["dep";f] ->
     let dg = dep_graph "" (files ".") in
     log "%a\n" (list_sep " " string) (trans_file_deps dg [f])

  (* Print dependencies of all ml files in the current directory and
     its subdirectories recursively. *)
  | ["dep"] ->
     out_dep_graph stdout (dep_graph "" (files "."))

  | "dep"::_ -> wrong_nb_args()

  (* Print the names of theorems proved in f. *)
  | ["name";f] ->
     log "%a\n" (list_sep "\n" string) (thms_of_file f)

  (* Print the names of theorems proved in f and all its dependencies. *)
  | ["name";"upto";f] ->
     let dg = dep_graph "" (files ".") in
     List.iter
       (fun d -> List.iter (log "%s %s\n" d) (thms_of_file d))
       (trans_file_deps dg [f])

  (* Print the names of theorems proved in all files in the current
     directory and its subdirectories recursively. *)
  | ["name"] ->
     List.iter
       (fun f -> List.iter (log "%s %s\n" f) (thms_of_file f))
       (files ".")

  | "name"::_ -> wrong_nb_args()

  | ["env"] -> print_env_var "HOL2DK_DIR"; print_env_var "HOLLIGHT_DIR"
  | "env"::_ -> wrong_nb_args()

  | ["patch" as s] -> call_script s []
  | "patch"::_ -> wrong_nb_args()

  | ["unpatch" as s] -> call_script s []
  | "unpatch"::_ -> wrong_nb_args()

  | "config"::args -> call_script "config" args

  | ["dump";f] -> dump true f (basename_ml f)
  | "dump"::_ -> wrong_nb_args()

  | ["dump-before-hol";f] -> dump false f (basename_ml f)
  | "dump-before-hol"::_ -> wrong_nb_args()

  | ["dump-simp";f] -> dump_and_simp true f
  | "dump-simp"::_ -> wrong_nb_args()

  | ["dump-simp-before-hol";f] -> dump_and_simp false f
  | "dump-simp-before-hol"::_ -> wrong_nb_args()

  (* Create the file b.pos. *)
  | ["pos";b] ->
     let nb_proofs = read_val (b^".nbp") in
     let pos = Array.make nb_proofs 0 in
     let dump_file = b^".prf" in
     log_read dump_file;
     let ic = open_in_bin dump_file in
     let idx = ref 0 in
     begin
       try
         while !idx < nb_proofs do
           Array.set pos (!idx) (pos_in ic);
           ignore (input_value ic);
           incr idx;
         done
       with End_of_file -> assert false
     end;
     close_in ic;
     let dump_file = b^".pos" in
     log_gen dump_file;
     let oc = open_out_bin dump_file in
     output_value oc pos;
     close_out oc

  | "pos"::_ -> wrong_nb_args()

  (* Print statistics on all proof steps. *)
  | ["stat";b] ->
     let nb_proofs = read_val (b^".nbp") in
     let thm_uses = Array.make nb_proofs 0 in
     let rule_uses = Array.make nb_rules 0 in
     let unused = ref 0 in
     read_use b;
     let handle_proof k p =
       if Array.get !Xproof.last_use k >= 0 then
         (count_thm_uses thm_uses p; count_rule_uses rule_uses p)
       else incr unused
     in
     read_prf b handle_proof;
     print_string "compute statistics ...\n";
     print_histogram thm_uses;
     print_rule_uses rule_uses (nb_proofs - !unused)

  (* Print statistics on the proof steps for theorem s. *)
  | ["stat";b;s] ->
     let nb_proofs = read_val (s^".nbp") in
     let thm_uses = Array.make nb_proofs 0 in
     let rule_uses = Array.make nb_rules 0 in
     let unused = ref 0 in
     read_use s;
     let dump_file = b^".prf" in
     log_read dump_file;
     let ic = open_in_bin dump_file in
     the_start_idx := read_val (s^".sti");
     read_pos b;
     seek_in ic (get_pos !the_start_idx);
     let f k p =
       if Array.get !Xproof.last_use k >= 0 then
         (count_thm_uses thm_uses p; count_rule_uses rule_uses p)
       else incr unused
     in
     for k = 0 to nb_proofs - 1 do f k (input_value ic) done;
     close_in ic;
     print_string "compute statistics ...\n";
     print_histogram thm_uses;
     print_rule_uses rule_uses (nb_proofs - !unused)

  | "stat"::_ -> wrong_nb_args()

  | ["nbp";b] ->
     read_use b;
     let n =
       Array.fold_left (fun n k -> if k >= 0 then n+1 else n) 0 !last_use in
     let nb_proofs = Array.length !last_use in
     log "%#d / %#d = %2d%% useful proof steps\n"
       n nb_proofs (percent n nb_proofs)

  | "nbp"::_ -> wrong_nb_args()

  (* Print statistics on the size of terms. *)
  | ["size";b] -> command ["size";b;"0"]

  | ["size";b;l] ->
     let l = integer l in
     read_use b;
     init_proof_reading b;
     let max_size = ref 0 and sum_size = ref 0 and nb_terms = ref 0
     and nb_terms_gt_l = ref 0 in
     let handle_term t =
       incr nb_terms;
       let s = nb_cons t in
       if s > !max_size then max_size := s;
       if s > l then incr nb_terms_gt_l;
       sum_size := s + !sum_size
     in
     let handle_proof k p =
       if Array.get !Xproof.last_use k >= 0 then
         begin
           let Proof(th,_) = p in
           let hs,c = dest_thm th in
           handle_term c; List.iter handle_term hs
         end
     in
     read_prf b handle_proof;
     log "%#d terms, average size = %#d, max size = %#d, \
          %#d terms of size >%#d (%d%%)\n"
       !nb_terms (!sum_size / !nb_terms) !max_size
       !nb_terms_gt_l l (percent !nb_terms_gt_l !nb_terms)

  | "size"::_ -> wrong_nb_args()

  (* Print proof steps between x and y. *)
  | ["proof";b;x;y] ->
     let x = integer x and y = integer y in
     let nb_proofs = read_val (b^".nbp") in
     if x < 0 || y < x || y >= nb_proofs then
       (err "[%d,%d] is not a valid interval\n" x y; exit 1);
     read_pos b;
     init_proof_reading b;
     read_use b;
     let map_thid_name = read_val (b^".thm") in
     for k = x to y do
       log "%8d: %a" k proof (proof_at k);
       begin match Array.get !Xproof.last_use k with
       | 0 -> (try log " (named %s)" (MapInt.find k map_thid_name)
               with Not_found -> assert false)
       | n -> if n < 0 then log " (unused)"
       end;
       log "\n"
     done;
     close_in !Xproof.ic_prf

  | ["proof";b;x] -> command ["proof";b;x;x]

  | "proof"::_ -> wrong_nb_args()

  (* Print statements between x and y. *)
  | ["concl";b;x;y] ->
     let x = integer x and y = integer y in
     let nb_proofs = read_val (b^".nbp") in
     if x < 0 || y < x || y >= nb_proofs then
       (err "[%d,%d] is not a valid interval\n" x y; exit 1);
     read_pos b;
     init_proof_reading b;
     read_use b;
     read_sig b;
     for k = x to y do
       if Array.get !Xproof.last_use k >= 0 then
         match proof_at k with
         | Proof(th,_) ->
            log "%a |- %a\n"
              (Xlib.list_sep ", " Xlp.raw_term) (hyp th)
              Xlp.raw_term (concl th)
     done;
     close_in !Xproof.ic_prf

  | ["concl";b;x] -> command ["concl";b;x;x]

  | "concl"::_ -> wrong_nb_args()

  (* Simplify some proof steps in b.prf. *)
  | ["rewrite";b] ->
     read_pos b;
     init_proof_reading b;
     read_use b;
     let dump_file = b^"-simp.prf" in
     log_gen dump_file;
     let oc = open_out_bin dump_file in
     (* count the number of simplications and duplications *)
     let n = ref 0 and d = ref 0 in
     (* map from theorem indexes to their new proofs *)
     let map_thid_pc = ref MapInt.empty in
     let add i c = map_thid_pc := MapInt.add i c !map_thid_pc in
     let pc_at j =
       match MapInt.find_opt j !map_thid_pc with
       | Some c -> c
       | None -> content_of (proof_at j)
     in
     (* map from theorem statements to theorem indexes *)
     let map_stmt_thid = Hashtbl.create
                           (if !max_dup < max_int then 10_000_000 else 0) in
     let rmap = ref MapInt.empty in
     (* simplification of proof p at index k *)
     let default k p th c =
       let v = hyp th, concl th in
       if !max_dup < max_int then
         begin
           begin match Hashtbl.find_opt map_stmt_thid v with
           | Some (k',l) ->
              if l >= !max_dup then (incr d; rmap := MapInt.add k k' !rmap)
              else Hashtbl.replace map_stmt_thid v (k',l+1)
           | None -> Hashtbl.add map_stmt_thid v (k,1)
           end;
           output_value oc (change_content p (rename_pc !rmap c))
         end
       else output_value oc p
     in
     let out k p c =
       incr n; add k c; output_value oc (change_content p c)
     in
     let p0 = proof_at 0 in
     let simp k p =
       let l = Array.get !last_use k in
       if l < 0 then output_value oc p0 (* unused proof step *)
       else
         begin
           let Proof(th,c) = p in
           begin match c with
           | Prefl _ | Pbeta _ | Passume _ | Paxiom _ | Pdef _ | Ptruth ->
              (* proof steps with no dependency do not need to be shared *)
              output_value oc p
           | Pabs _ | Pdeduct _ | Pinst _ | Pinstt _ | Pdeft _ | Pconj _
           | Pmp _ | Pdisch _ | Pspec _ | Pgen _ | Pexists _ | Pchoose _
           | Pdisj1 _ | Pdisj2 _ | Pdisj_cases _ ->
              default k p th c
           | Ptrans(i,j) ->
              let ci = pc_at i and cj = pc_at j in
              begin match ci, cj with
              | Prefl _, _ -> (* i:t=t j:t=u ==> k:t=u *) out k p cj
              | _, Prefl _ -> (* i:t=u j:u=u ==> k:t=u *) out k p ci
              | _ -> default k p th c
              end
           | Psym i ->
              let ci = pc_at i in
              begin match ci with
              | Prefl _ -> (* i:t=t ==> k:t=t *) out k p ci
              | Psym j -> (* j:t=u ==> i:u=t ==> k:t=u *) out k p (pc_at j)
              | _ -> default k p th c
              end
           | Pconjunct1 i ->
              begin match pc_at i with
              | Pconj(j,_) -> (* j:p ==> i:p/\q ==> k:p *) out k p (pc_at j)
              | _ -> default k p th c
              end
           | Pconjunct2 i ->
              begin match pc_at i with
              | Pconj(_,j) -> (* j:q ==> i:p/\q ==> k:q *) out k p (pc_at j)
              | _ -> default k p th c
              end
           | Pmkcomb(i,j) ->
              begin match pc_at i with
              | Prefl t ->
                 begin match pc_at j with
                 | Prefl u -> (* i:t=t j:u=u ==> k:tu=tu *)
                    out k p (Prefl(mk_comb(t,u)))
                 | _ -> default k p th c
                 end
              | _ -> default k p th c
              end
           | Peqmp(i,j) ->
              begin match pc_at i with
              | Prefl _ -> (* i:p=p j:p ==> k:p *) out k p (pc_at j)
              | _ -> default k p th c
              end
           end;
           (* we can empty the map since the proofs coming after a named
              theorem cannot refer to proofs coming before it *)
           if l = 0 then map_thid_pc := MapInt.empty
         end
     in
     let nb_proofs = Array.length !prf_pos in
     for k = 0 to nb_proofs - 1 do simp k (proof_at k) done;
     close_in !Xproof.ic_prf;
     close_out oc;
     log "%#d simplifications (%#d%%)\n" !n (percent !n nb_proofs);
     log "%#d duplications removed (%#d%%)\n" !d (percent !d nb_proofs);
     Xlib.command ("mv "^b^"-simp.prf "^b^".prf");
     log_command ["pos";b];
     log_command ["use";b]

  | "rewrite"::_ -> wrong_nb_args()

  (* Update b.use which indicates which proof steps are useful. *)
  | ["purge";b] ->
     (* compute useful theorems *)
     read_pos b;
     init_proof_reading b;
     let map_thid_name = read_val (b^".thm") in
     let nb_proofs = Array.length !prf_pos in
     let useful = Array.make nb_proofs false in
     let rec mark_as_useful = function
       | [] -> ()
       | k::ks ->
          if useful.(k) then mark_as_useful ks
          else begin
              useful.(k) <- true;
              mark_as_useful (List.rev_append (deps (proof_at k)) ks)
            end
     in
     MapInt.iter (fun k _ -> mark_as_useful [k]) map_thid_name;
     close_in !Xproof.ic_prf;
     (* update file.use *)
     read_use b;
     let nb_useless = ref nb_proofs in
     Array.iteri
       (fun k b ->
         if b then decr nb_useless else Array.set !Xproof.last_use k (-1))
       useful;
     let dump_file = b^".use" in
     log_gen dump_file;
     let oc = open_out_bin dump_file in
     output_value oc !Xproof.last_use;
     log "%#d useless proof steps (%d%%)\n"
       !nb_useless (percent !nb_useless nb_proofs)

  | "purge"::_ -> wrong_nb_args()

  | ["simp";b] ->
     log_command ["rewrite";b];
     log_command ["purge";b]

  | "simp"::_ -> wrong_nb_args()

  (* Create b.use. *)
  | ["use";b] ->
     (* The .use file records an array [last_use] such that
        [last_use.(i) = 0] if [i] is a named theorem, the highest
        theorem index using [i] if there is one, and -1 otherwise. *)
     let nb_proofs = read_val (b^".nbp") in
     let last_use = Array.make nb_proofs (-1) in
     read_prf b
       (fun i p -> List.iter (fun k -> Array.set last_use k i) (deps p));
     MapInt.iter (fun k _ -> Array.set last_use k 0) (read_val (b^".thm"));
     let dump_file = b^".use" in
     log_gen dump_file;
     let oc = open_out_bin dump_file in
     output_value oc last_use;
     let unused = ref 0 in
     Array.iter (fun n -> if n < 0 then incr unused) last_use;
     log "%#d unused proof steps (%d%%)\n" !unused (percent !unused nb_proofs);
     close_out oc

  | "use"::_ -> wrong_nb_args()

  (* Print the value of b.use.(k). *)
  | ["print";"use";b;k] ->
     let k = integer k in
     let nb_proofs = read_val (b^".nbp") in
     if k < 0 || k >= nb_proofs then
       (err "%d is not a valid proof index\n" k; exit 1);
     read_use b;
     log "%d\n" (Array.get !Xproof.last_use k)

  | ["print";f] ->
     begin
       match Filename.extension f with
       | ".thm" -> MapInt.iter (log "%d %s\n") (read_val f)
       | ".tvs" -> MapStr.iter (log "%s %d\n") (read_val f)
       | _ -> err "\"%s\" does not end with \".thm\" or \".tvs\"\n" f; exit 1
     end

  | "print"::_ -> wrong_nb_args()

  (* Create b.mk. *)
  | ["mkfile";b] ->
     let dump_file = b^".dg" in
     log_read dump_file;
     let ic = open_in_bin dump_file in
     let _nb_parts = input_value ic in
     let dg = input_value ic in
     close_in ic;
     let nb_proofs = read_val (b^".nbp") in
     make nb_proofs dg b

  (* Create b.dg and b.mk. *)
  | ["mk";nb_parts;b] ->
     let nb_parts = integer nb_parts in
     if nb_parts < 2 then (err "the number of parts must be > 1\n"; exit 1);
     let nb_proofs = read_val (b^".nbp") in
     let part_size = nb_proofs / nb_parts in
     let part idx =
       let k = idx / part_size in
       if k >= nb_parts - 1 then nb_parts - 1 else k in
     let dg = Array.init nb_parts (fun i -> Array.make i false) in
     let add_dep x =
       let px = part x in
       fun y ->
       let py = part y in
       if px <> py then
         begin
           (*try*) dg.(px).(py) <- true (*dg.(px).(py) + 1*)
           (*with (Invalid_argument _) as e ->
             log "x = %d, px = %d, y = %d, py = %d\n%!" x px y py;
             raise e*)
         end
     in
     read_use b;
     let handle_proof k p =
       if Array.get !Xproof.last_use k >= 0 then
         List.iter (add_dep k) (deps p)
     in
     read_prf b handle_proof;
     for i = 1 to nb_parts - 1 do
       log "%d:" (i+1);
       for j = 0 to i - 1 do
         (*if dg.(i).(j) > 0 then log " %d (%d)" (j+1) dg.(i).(j)*)
         if dg.(i).(j) then log " %d" (j+1)
       done;
       log "\n"
     done;
     let dump_file = b^".dg" in
     log_gen dump_file;
     let oc = open_out_bin dump_file in
     output_value oc nb_parts;
     output_value oc dg;
     close_out oc;
     make nb_proofs dg b

  | "mk"::_ -> wrong_nb_args()

  (* Create the files b_types, b_terms, b_axioms. *)
  | ["sig";f] ->
     let dk = is_dk f in
     let b = Filename.chop_extension f in
     read_sig b;
     if dk then
       begin
         Xdk.export_types b;
         Xdk.export_terms b;
         Xdk.export_axioms b
       end
     else
       begin
         Xlp.export_types b;
         Xlp.export_terms b;
         Xlp.export_axioms b;
         write_val (b^"_terms.tvs") !Xlp.tvs_map
       end

  | "sig"::_ -> wrong_nb_args()

  (* Called in b.mk to create b_theorems.dk or b.lp with, for each
     named theorem, a definition "name := lemXXX" in b.lp, and "name :
     type := lemXXX" in b_theorems.dk, where XXX is the index of
     name. *)
  | ["thm";f] ->
     let dk = is_dk f in
     let b = Filename.chop_extension f in
     read_sig b;
     let map_thid_name = read_val (b^".thm") in
     read_pos b;
     init_proof_reading b;
     begin
       if dk then Xdk.export_theorems (b^"_theorems")
                    map_thid_name (fun _ _ -> true) true
       else let nb_parts = read_val (b^".dg") in
            Xlp.export_theorems_part nb_parts b map_thid_name
     end;
     close_in !Xproof.ic_prf

  | "thm"::_ -> wrong_nb_args()

  (* Called in b.mk to create b_part_k and the associated type and
     term abbreviation files. *)
  | ["part";k;x;y;f] ->
     let b = Filename.chop_extension f in

     let dump_file = b^".dg" in
     log_read dump_file;
     let ic = open_in_bin dump_file in
     let nb_parts = input_value ic in

     let k = integer k and x = integer x and y = integer y in
     if k < 1 || k > nb_parts || x < 0 || y < x then
       (err "wrong part number or invalid interval\n"; exit 1);
     read_sig b;
     read_pos b;
     init_proof_reading b;
     read_use b;
     if is_dk f then
       begin
         Xdk.export_proofs_part b k x y;
         Xdk.export_term_abbrevs (b^part k);
         Xdk.export_type_abbrevs (b^part k)
       end
     else
       begin
         let dg = input_value ic in
         Xlp.export_proofs_part b dg k x y;
         Xlp.export_term_abbrevs_in_one_file b (b^part k)
       end;
     close_in ic;
     close_in !Xproof.ic_prf

  | "part"::_ -> wrong_nb_args()

  (* Called in Makefile to generate b_opam.lp with, for each named
     theorem, a declaration "symbol thm_name : type". *)
  | ["axm";f] ->
     let dk = is_dk f in
     let b = Filename.chop_extension f in
     read_sig b;
     let map_thid_name = read_val (b^".thm") in
     read_pos b;
     init_proof_reading b;
     let cond _ _ = true in
     begin
       if dk then Xdk.export_theorems (b^"_opam") map_thid_name cond false
       else Xlp.export_theorems (b^"_opam") b map_thid_name cond
     end;
     close_in !Xproof.ic_prf

  | "axm"::_ -> wrong_nb_args()

  (* Called in Makefile to generate, for each file n required by f, a
     file n.lp with a declaration "symbol thm_name : type" for each
     named theorem in n.ml. *)
  | ["files";f] ->
     let dk = is_dk f in
     let f = Filename.chop_extension f in
     let b = Filename.basename f in
     read_sig b;
     let map_thid_name = read_val (b^".thm") in
     read_pos b;
     init_proof_reading b;
     begin
       try
         let d = Sys.getenv "HOLLIGHT_DIR" in
         let dg = dep_graph d (files d) in
         let files = trans_file_deps dg [f^".ml"] in
         let gen file =
           let thm_names = thms_of_file (Filename.concat d file) in
           let cond _ n = List.mem n thm_names in
           let f = Filename.chop_extension file in
           if dk then Xdk.export_theorems f map_thid_name cond false
           else Xlp.export_theorems f b map_thid_name cond
         in
         List.iter gen files;
         close_in !Xproof.ic_prf
       with Not_found ->
         close_in !Xproof.ic_prf;
         err "set $HOLLIGHT_DIR first\n";
         exit 1
     end

  | "files"::_ -> wrong_nb_args()

  (* Called in Makefile when n is in BIG_FILES to create the file
     n.siz which contains an array mapping every proof step index used
     in the proof of n to an estimation of the size of its Dedukti
     tree representation. *)
  | ["thmsize";b;n] ->
     init_proof_reading b;
     read_use n;
     read_pos n;
     the_start_idx := read_val (n^".sti");
     let size = Array.make (Array.length !Xproof.prf_pos) 0 in
     (*let total = ref 0 in*)
     Array.iteri (fun k pos ->
         if Array.get !last_use k >= 0 then
           begin
             seek_in !ic_prf pos;
             let s = size_proof (input_value !ic_prf) in
             Array.set size k s;
             (*total := !total + s*)
           end)
       !Xproof.prf_pos;
     write_val (n^".siz") size;
     (*log "size: %#d\n" !total;*)

  | "thmsize"::_ -> wrong_nb_args()

  (* Create b.thp, which contains a map from the index of each theorem
     to its name and position in b.prf and, for each theorem n, create
     the files n.nbp, n.sti, n.pos and n.use. *)
  | ["split";b] ->
     read_pos b;
     read_use b;
     let map_thid_name = read_val (b^".thm") in
     let map = ref MapInt.empty in (* to build b.thp *)
     let s = ref 0 in
     let create_segment start_index end_index =
       incr s;
       let n = thm_name map_thid_name end_index in
       let len = end_index - start_index + 1 in
       write_val (n^".nbp") len;
       write_val (n^".sti") start_index;
       write_val (n^".pos") (Array.sub !prf_pos start_index len);
       write_val (n^".use") (Array.sub !last_use start_index len);
       let p = Array.get !prf_pos end_index in
       map := MapInt.add end_index (n,p) !map
     in
     (* read proof steps from the end *)
     let end_idx = ref (Array.length !prf_pos - 1) in
     (* ignore last unused proof steps *)
     while Array.get !last_use !end_idx < 0 do decr end_idx done;
     for k = !end_idx - 1 downto 0 do
       let l = Array.get !last_use k in
       if l = 0 || l > !end_idx then
         begin
           create_segment (k+1) !end_idx;
           end_idx := k
         end
     done;
     create_segment 0 !end_idx;
     (*MapInt.iter (fun i (n,_) -> log "%d %s\n" i n) !map;*)
     write_val (b^".thp") !map;
     log "%d proof files\n" !s

  | "split"::_ -> wrong_nb_args()

  (* For each f in files such that $HOLLIGHT_DIR/f.ml exists, generate
     the files f.sti, f.pos, f.use and f.nbp, and remove all the files
     t.sti, t.pos, t.use and t.nbp such that t is proved in f. Update
     b.thp accordingly. *)
  | "unsplit"::_::[] -> ()
  | "unsplit"::b::files ->
     let d =
       try Sys.getenv "HOLLIGHT_DIR"
       with Not_found -> err "HOLLIGHT_DIR needs to be set first"; exit 1
     in
     read_pos b;
     read_use b;
     let map_thid_name = read_val (b^".thm") in
     let map_name_thid = inverse map_thid_name in
     let ranges =
       List.map
         (fun f ->
           let min,max =
             thid_range map_name_thid (Filename.concat d (f^".ml")) in
           let k = ref (min - 1) in
           let cond() = let l = Array.get !last_use !k in l <> 0 && l <= max in
           while cond() do decr k done;
           let min = !k + 1 in
           let f = Filename.basename f in
           create_segment f min max;
           (min,max),f)
         files
     in
     let map =
       MapInt.mapi (fun k ((_,p) as v) ->
           let in_range k ((min,max),_) = min <= k && k <= max in
           match List.find_opt (in_range k) ranges with
           | Some(_,f) ->
              (*FIXME: these files should not be generated in the
                first place. unsplit and split should be merged somehow. *)
              let n = thm_name map_thid_name k in
              if not(List.exists (fun (_,f) -> f=n) ranges) then
                Xlib.remove [n^".pos";n^".use";n^".sti";n^".nbp"];
              f,p
           | None -> v)
         (read_val (b^".thp"))
     in
     write_val (b^".thp") map

  | "unsplit"::_ -> wrong_nb_args()

  (* Called in Makefile when f is in BIG_FILES to create the files
     n.lp, n_spec.lp, n_part_k.idx, which contains the first and last
     proof step index of part_k, and n.max, which contains an array
     with the last proof index of each part. *)
  | ["thmsplit";b;f] ->
     let n = Filename.chop_extension f in
     read_use n;
     the_start_idx := read_val (n^".sti");
     Xproof.thm_size := read_val (n^".siz");
     (* to generate [n^".lp"] *)
     read_sig b;
     map_thid_pos := read_val (b^".thp");
     read_pos n;
     init_proof_reading b;
     if is_dk f then (err "dk output not available for this command\n"; exit 1)
     else Xlp.split_theorem_proof b n

  | "thmsplit"::_ -> wrong_nb_args()

  (* Called in Makefile with f=n_part_k when n is in BIG_FILES to
     create the files f.lp, f_spec.lp, f.typ, f.brv, f.brp,
     f_term_abbrevs_part_i.min and f_term_abbrevs_part_i.max. *)
  | ["thmpart";b;f] ->
     begin
       let dk = is_dk f in
       let f = Filename.chop_extension f in
       match get_part f "" with
       | None -> err "\"%s\" does not end with \"_part_\" \
                      followed by an integer\n" f; exit 1
       | Some(n,k) ->
          read_sig b;
          map_thid_pos := read_val (b^".thp");
          read_pos n;
          read_use n;
          the_start_idx := read_val (n^".sti");
          init_proof_reading b;
          if dk then (err "dk output not available for this command\n"; exit 1);
          Xlp.export_theorem_proof_part b n k;
          write_val (n^part(k)^".tvs") !Xlp.tvs_map
     end

  | "thmpart"::_ -> wrong_nb_args()

  (* Called in Makefile to create n.lp when n is NOT in BIG_FILES. *)
  | ["theorem";b;f] ->
     read_sig b;
     map_thid_pos := read_val (b^".thp");
     let n = Filename.chop_extension f in
     read_pos n;
     read_use n;
     the_start_idx := read_val (n^".sti");
     init_proof_reading b;
     if is_dk f then (err "dk output not available for this command\n"; exit 1)
     else
       begin
         Xlp.export_theorem_proof b n;
         close_in !Xproof.ic_prf;
         Xlp.export_term_abbrevs_in_one_file b n;
         Xlp.export_theorem_deps b n;
         write_val (n^".tvs") !Xlp.tvs_map
       end

  | "theorem"::_ -> wrong_nb_args()

  (* List theorems proved in file f. *)
  | ["thms";b;f] ->
     let map_thid_name = read_val (b^".thm") in
     let min_id, max_id = thid_range (inverse map_thid_name) f in
     let map,_,_ = MapInt.split (max_id + 1) (read_val (b^".thp")) in
     let _,_,map = MapInt.split (min_id - 1) map in
     MapInt.iter (fun k _ -> log "%s\n" (thm_name map_thid_name k)) map

  | "thms"::_ -> wrong_nb_args()

  (* Merge all tvs files in a single one. *)
  | ["tvs";b] ->
    let map = ref MapStr.empty and n = b^".tvs" in
    let read_tvs_file f =
      if String.ends_with ~suffix:".tvs" f && f <> n then
        MapStr.iter (fun s x -> map := MapStr.add s x !map) (read_val f);
    in
    Array.iter read_tvs_file (Sys.readdir ".");
    write_val n !map

  | "tvs"::_ -> wrong_nb_args()

  (* Merge all maps in typ files into a single map, give a unique
     index to every entry in the obtained map, generate
     b^"_type_abbrevs.lp" and a sed file for every typ file. *)
  | ["type_abbrevs";b] ->
    let files = Sys.readdir "." and map = ref MapStr.empty in
    (* merge all type abbrev maps into [!map] *)
    let read_typ_file f =
      if String.ends_with ~suffix:".typ" f then
        MapStr.iter (fun s x -> map := MapStr.add s x !map) (read_val f);
    in
    Array.iter read_typ_file files;
    (* give a unique id to each entry *)
    let map =
      let idx = ref (-1) in MapStr.map (fun x -> incr idx; (!idx,x)) !map in
    (* generate sed files *)
    let gen_sed_file f =
      if String.ends_with ~suffix:".typ" f then
        begin
          let m = read_val f in
          let oc = log_open_out (Filename.chop_extension f^".sed") in
          let add_cmd s (d,_n) =
            let idx =
              match MapStr.find_opt s map with
              | Some(idx,_) -> idx
              | None -> assert false
            in
            string oc "s/"; digest oc d; char oc '/'; int oc idx;
            string oc "/g\n";
          in
          MapStr.iter add_cmd m;
          close_out oc
        end
    in
    Array.iter gen_sed_file files;
    (* generate [b^"_type_abbrevs.lp"] *)
    let decl_type_abbrevs oc =
      let abbrev s (idx,(_d,n)) =
        string oc "symbol type"; int oc idx;
        if n > 0 then begin
          string oc " (a0";
          for i=1 to n-1 do string oc " a"; int oc i done;
          string oc " : Set)"
        end;
        string oc " ≔ "; string oc s; string oc ";\n"
      in
      MapStr.iter abbrev map
    in
    Xlp.export (b^"_type_abbrevs") [b^"_types"] decl_type_abbrevs

  | "type_abbrevs"::_ -> wrong_nb_args()

  (* Generate Lambdapi term abbreviation files. *)
  | ["abbrev";b;f] ->
     begin
       let dk = is_dk f in
       let f = Filename.chop_extension f in
       match get_part f "_term_abbrevs" with
       | None -> err "\"%s\" does not end with \"_term_abbrevs_part_\"\
                      followed by an integer\n" f; exit 1
       | Some(n,k) ->
         if dk then (err "dk output not available for this command\n"; exit 1);
         read_sig b;
         map_thid_pos := read_val (b^".thp");
         Xlp.export_theorem_term_abbrevs_part b n k;
         write_val (n^"_term_abbrevs"^part(k)^".tvs") !Xlp.tvs_map
     end

  | "abbrev"::_ -> wrong_nb_args()

  (* Single file generation (used neither in b.mk nor in Makefile). *)
  | f::args ->
     let r = range args in
     let dk = is_dk f in
     let b = Filename.chop_extension f in
     read_sig b;
     if dk then
       begin
         Xdk.export_types b;
         Xdk.export_terms b;
         Xdk.export_axioms b;
       end
     else
       begin
         Xlp.export_types b;
         Xlp.export_terms b;
         Xlp.export_axioms b
       end;
     read_pos b;
     init_proof_reading b;
     read_use b;
     if dk then
       begin
         Xdk.export_proofs b r;
         if r = All then
           Xdk.export_theorems (b^"_theorems")
             (read_val (b^".thm")) (fun _ _ -> true) true;
         Xdk.export_term_abbrevs b;
         Xdk.export_type_abbrevs b;
         log_gen f;
         let deps = ["types";"type_abbrevs";"terms";"term_abbrevs";"axioms"
                     ;"proofs"] in
         let infiles =
           List.map (fun s -> b^"_"^s^".dk")
             (if r = All then deps @ ["theorems"] else deps)
         in
         Xlib.concat ("theory_hol.dk"::infiles) (b^".dk")
       end
     else
       begin
         Xlp.export_proofs b r;
         if r = All then Xlp.single_export_theorems b b (read_val (b^".thm"));
         Xlp.export_term_abbrevs_in_one_file b b;
         Xlp.export_type_abbrevs b b
       end;
     close_in !Xproof.ic_prf

let _ =
  (*Memtrace.trace_if_requested ();*)
  command (List.tl (Array.to_list Sys.argv))