details

Makefile

@@ -14,7 +14,10 @@ sti:
 
 .PHONY: clean-sti
 clean-sti:
-	find . -maxdepth 1 -name '*.sti' -exec rm -f {} `basename {}`.nbp `basename {}`.pos `basename {}`.use \;
+	find . -maxdepth 1 -name '*.sti' -delete
+	find . -maxdepth 1 -name '*.nbp' -delete
+	find . -maxdepth 1 -name '*.pos' -a ! -name $(BASE).pos -delete
+	find . -maxdepth 1 -name '*.use' -a ! -name $(BASE).use -delete
 	rm -f $(BASE).thp
 
 BASE_FILES := $(BASE)_types $(BASE)_terms $(BASE)_axioms

TODO.md

@@ -1,9 +1,11 @@
 TODO
 ----
 
-- get rid of use file? in pos files, set pos to -1 for unused theorems
+- use hashconsing for building map_term
 
-- proofs can be simplified in parallel by working on the proof of each named theorem separately
+- get rid of use file? in pos files, set pos to -1 for unused theorems?
+
+- simplify/purge proofs in parallel?
 
 - add commands for patch/unpatch/add-links ?
 

add-links

@@ -19,7 +19,7 @@ then
     exit 1
 fi
 
-for ext in prf sig thm pos use
+for ext in prf nbp sig thm pos use
 do
    ln -f -s $HOLLIGHT_DIR/$1.$ext
 done

dune

@@ -1,7 +1,7 @@
 (executable
  (public_name hol2dk)
  (name main)
- (libraries str unix)
+ (libraries str unix memtrace)
 )
 
 (install

main.ml

@@ -152,11 +152,6 @@ let read_sig b =
   update_map_const_typ_vars_pos();
   update_reserved()
 
-let read_thm b =
-  let map = read_val (b ^ ".thm") in
-  log "%d named theorems\n%!" (MapInt.cardinal map);
-  map
-
 let integer s = try int_of_string s with Failure _ -> wrong_arg()
 
 (* [make nb_proofs dg b] generates a makefile for translating the
@@ -456,7 +451,7 @@ and command = function
      read_pos b;
      init_proof_reading b;
      read_use b;
-     let map_thid_name = read_thm b in
+     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
@@ -561,7 +556,7 @@ and command = function
      (* compute useful theorems *)
      read_pos b;
      init_proof_reading b;
-     let map_thid_name = read_thm b in
+     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
@@ -604,7 +599,7 @@ and command = function
      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_thm b);
+     MapInt.iter (fun k _ -> Array.set last_use k 0) (read_val (b ^ ".thm"));
      let dump_file = b ^ ".use" in
      log "generate %s ...\n" dump_file;
      let oc = open_out_bin dump_file in
@@ -695,7 +690,7 @@ and command = function
      let dk = is_dk f in
      let b = Filename.chop_extension f in
      read_sig b;
-     let map_thid_name = read_thm b in
+     let map_thid_name = read_val (b ^ ".thm") in
      read_pos b;
      init_proof_reading b;
      begin
@@ -710,7 +705,7 @@ and command = function
      let dk = is_dk f in
      let b = Filename.chop_extension f in
      read_sig b;
-     let map_thid_name = read_thm b in
+     let map_thid_name = read_val (b ^ ".thm") in
      read_pos b;
      init_proof_reading b;
      begin
@@ -757,7 +752,8 @@ and command = function
   | ["split";b] ->
      read_pos b;
      read_use b;
-     let map_thid_name = read_thm b in
+     init_proof_reading b;
+     let map_thid_name = read_val (b ^ ".thm") in
      let map = ref MapInt.empty in
      let create_segment start_index end_index =
        let n = try MapInt.find end_index map_thid_name
@@ -769,6 +765,15 @@ and command = function
        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;
+       (*let dump_file = n ^ ".prf" in
+       log "write %s ...\n%!" dump_file;
+       let oc = open_out_bin dump_file in
+       seek_in !ic_prf (get_pos start_index);
+       for _k = 1 to len do
+         let p : proof = input_value !ic_prf in
+         output_value oc p
+       done;
+       close_out oc*)
      in
      let end_idx = ref (Array.length !prf_pos - 1) in
      while Array.get !last_use !end_idx < 0 do decr end_idx done;
@@ -873,7 +878,7 @@ and command = function
      if dk then
        begin
          Xdk.export_proofs b r;
-         if r = All then Xdk.export_theorems b (read_thm b);
+         if r = All then Xdk.export_theorems b (read_val (b ^ ".thm"));
          Xdk.export_term_abbrevs b "";
          Xdk.export_type_abbrevs b "";
          log "generate %s.dk ...\n%!" b;
@@ -890,11 +895,13 @@ and command = function
      else
        begin
          Xlp.export_proofs b b r;
-         if r = All then Xlp.export_theorems b (read_thm b);
+         if r = All then Xlp.export_theorems b (read_val (b ^ ".thm"));
          Xlp.export_term_abbrevs b b "";
          Xlp.export_type_abbrevs b b ""
        end;
      close_in !Xproof.ic_prf;
      0
 
-let _ = exit (command (List.tl (Array.to_list Sys.argv)))
+let _ =
+  Memtrace.trace_if_requested ();
+  exit (command (List.tl (Array.to_list Sys.argv)))

xlib.ml

@@ -369,7 +369,7 @@ let add_var rmap v =
 (* [renaming_map tvs vs] returns an association list giving names to
    the term variables in [vs] that are distinct to one another and
    distinct from the type variables in [tvs]. This is needed to
-   include type variables because HOL-Light may ave type variables and
+   include type variables because HOL-Light may have type variables and
    term variables with the same name. *)
 let renaming_map =
   let tyvar = function Tyvar n -> mk_var(n,bool_ty),n | _ -> assert false in
@@ -380,7 +380,6 @@ let el b =
   mk_comb(mk_const("@",[b,aty]),mk_abs(mk_var("_",b),mk_const("T",[])))
 *)
 (*if not(!el_added) then (new_constant("el",aty); el_added := true);;*)
-
 let mk_el b = mk_const("el",[b,aty]);;
 
 (* [canonical_term t] returns the type variables and term variables of

xlp.ml

@@ -209,6 +209,7 @@ let unabbrev_term =
 ;;
 
 let abbrev_term =
+  (*let oc_abbrevs = open_out "term_abbrevs" in*)
   let idx = ref (-1) in
   let abbrev oc t =
     (* check whether the term is already abbreviated; add a new
@@ -219,6 +220,8 @@ let abbrev_term =
       | Some (k,_,_) -> k
       | None ->
          let k = !idx + 1 in
+         (*if k mod 1000 = 0 then log "term abbrev %d\n%!" k;*)
+         (*out oc_abbrevs "%a\n\n" raw_term t;*)
          idx := k;
          let x = (k, List.length tvs, bs) in
          map_term := MapTrm.add t x !map_term;
@@ -532,8 +535,8 @@ let theorem_as_axiom oc k p = decl_theorem oc k p Axiom;;
    [x] .. [y]. *)
 let proofs_in_interval oc x y =
   for k = x to y do
-    (*log "proof %d\n%!" k;*)
-    if get_use k >= 0 then theorem oc k (proof_at k)
+    if get_use k >= 0 then
+      begin (*log "proof %d ...\n%!" k;*) theorem oc k (proof_at k) end
   done
 
 (* [proofs_in_range oc r] outputs on [oc] the proofs in range [r]. *)