Generate the proofs of all the theorems of an HOL-Light file in a single Lambdapi file (#183)

other changes:
- Xlib: concat and remove takes a list of filenames in argument

Author: fblanqui

CHANGES.md

@@ -9,6 +9,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 
 - command nbp to print the number of (useful) proofs
 - command files to print theorem statements following the file structuration in HOL-Light
+- command thms to print theorems (named or not) proved in a file
+- command merge to generate a single lp file for the proofs of all the theorems (named or not) proved in a file
 - renamings to handle the Multivariate library
 - test/Sig_mappings_N.v and test/Sig_With_N.v: axiomatizations of mappings_N.v and With_N.v respectively
 

README.md

@@ -309,7 +309,7 @@ b.sig: signature (types, constants, axioms, definitions)
 
 b.thm: map from theorem indexes having a name to their name
 
-b.thp: map every useful theorem index to its name and position (similar to f.thm but with position)
+b.thp: map every useful theorem index to its position in b.prf and the lp filename where its proof is translated
 
 f.nbp: number of proof steps
 

TODO.md

@@ -1,6 +1,8 @@
 TODO
 ----
 
+- xnames.ml: define string_of_file as an iterator
+
 - replace variables like _1718 by better names
 
 - always share closed subterms

main.ml

@@ -78,8 +78,8 @@ hol2dk $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 by having a file for each named theorem
--------------------------------------------------------------------------
+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
@@ -91,6 +91,10 @@ hol2dk split $base
   generate $base.thp and the files $thm.sti, $thm.pos and $thm.use
   for each theorem $thm
 
+hol2dk merge $base [$path/]$file.(dk|lp)
+  generate a single lp file for the proofs of all the theorems (named or not)
+  proved in [$path/]$file.(dk|lp)
+ 
 hol2dk theorem $base $thm.lp
   generate the lp proof of the theorem $thm
 
@@ -148,7 +152,10 @@ hol2dk print use $base $x
   print the contents of $base.use for theorem index $x
 
 hol2dk print $base.thm
-  print the contents of $base.thm
+  print the contents of $base.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
@@ -308,6 +315,24 @@ let print_env_var n =
 
 let wrong_nb_args() = err "wrong number of arguments\n"; 1;;
 
+(* compute the minimum and maximum theorem indexes in f *)
+let thid_range_of_file b f =
+  let min_id = ref max_int and max_id = ref min_int in
+  let map_thid_name = read_val (b^".thm") in
+  let map_name_thid = (* inverse of map_thid_name *)
+    MapInt.fold (fun k n map -> MapStr.add n k map) map_thid_name MapStr.empty
+  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);
+  !min_id, !max_id, map_thid_name
+;;
+
 let rec log_command l =
   print_string "\nhol2dk";
   List.iter (fun s -> print_char ' '; print_string s) l;
@@ -337,12 +362,16 @@ and command = function
   | "--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()
+
   | "--root-path"::arg::args -> Xlp.root_path := arg; command args
 
-  | ["--root-path"] -> err "missing root path\n"; 1
+  | ["--root-path"] -> wrong_nb_args()
 
   | s::_ when String.starts_with ~prefix:"--" s ->
      err "unknown option \"%s\"\n" s; 1
@@ -887,8 +916,9 @@ and command = function
 
   | "axm"::_ -> wrong_nb_args()
 
-  (* Called in Makefile to generate a file f.lp with, for each named
-     theorem in f.ml, a declaration "symbol thm_name : type". *)
+  (* 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
@@ -1047,6 +1077,98 @@ and command = function
 
   | "theorem"::_ -> wrong_nb_args()
 
+  (* List theorems proved in file f. *)
+  | ["thms";b;f] ->
+     let min_id, max_id, map_thid_name = thid_range_of_file b 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 _ ->
+         try log "%s\n" (MapInt.find k map_thid_name)
+         with Not_found -> log "thm%d\n" k)
+       map;
+     0
+
+  | "thms"::_ -> wrong_nb_args()
+
+  (* Generate p.lp and its associated files, where
+     p=chop_extension(basename f), with all the theorems (named or
+     not) proved in f. *)
+  | ["merge";b;f] ->
+     let p = Filename.chop_extension (Filename.basename f) in
+     if Sys.file_exists (p^".lp") then
+       begin
+         err "\"%s.lp\" already exists. If you generated it using \"hol2dk merge\", you cannot regenerate it again unless you remove it and do \"hol2dk split\" again.\n" p;
+         exit 1
+       end;
+     (* update b.thp and set Xproof.map_thid_pos for export *)
+     let min_id, max_id, _ = thid_range_of_file b f
+     and thm_names = ref SetStr.empty
+     and map_thid_name = ref MapInt.empty in
+     Xproof.map_thid_pos :=
+       MapInt.mapi (fun k ((name,pos) as v) ->
+           if min_id <= k && k <= max_id && name <> p then
+             begin
+               thm_names := SetStr.add name !thm_names;
+               map_thid_name := MapInt.add k name !map_thid_name;
+               (p,pos)
+             end
+           else v)
+         (read_val (b^".thp"));
+     write_val (b^".thp") !Xproof.map_thid_pos;
+     (* generate proof steps *)
+     read_sig b;
+     init_proof_reading b;
+     let deps = ref SetStr.empty in
+     let gen oc_spec n =
+       read_pos n;
+       read_use n;
+       the_start_idx := read_val (n^".sti");
+       Xlib.remove [n^".pos";n^".use";n^".sti";n^".nbp"];
+       (* part of Xlp.export_theorem_proof b n; *)
+       let thid = !the_start_idx + Array.length !prf_pos - 1 in
+       Xlp.export_proofs_in_interval n !the_start_idx thid;
+       Xlib.rename (n^part !Xlp.proof_part^"_proofs.lp") (n^"_proofs.lp");
+       (* record external dependencies *)
+       for i = 1 to !Xlp.proof_part do
+         deps := SetStr.fold
+                   (fun n acc ->
+                     if SetStr.mem n !thm_names then acc else SetStr.add n acc)
+                   (Hashtbl.find Xlp.htbl_thm_deps i)
+                   !deps
+       done;
+       (* generate corresponding spec *)
+       Xlp.theorem_as_axiom false oc_spec thid (proof_at thid)
+     in
+     Xlp.export (p^"_spec") [b^"_types";b^"_terms"]
+       (fun oc_spec -> SetStr.iter (gen oc_spec) !thm_names);
+     close_in !Xproof.ic_prf;
+     (* merge all proof files into [n_proofs.lp]. The order of proof
+        files is important. *)
+     let proof_files =
+       List.map (fun (_,n) -> n^"_proofs.lp")
+         (MapInt.bindings !map_thid_name) in
+     Xlib.concat proof_files (p^"_proofs.lp");
+     Xlib.remove proof_files;
+     Xlp.export_term_abbrevs_in_one_file b p;
+     write_val (p^".typ") !Xlp.map_typ_abbrev;
+     (* export deps *)
+     let iter_deps f =
+       f (b^"_types");
+       f (b^"_terms");
+       f (b^"_axioms");
+       f (b^"_type_abbrevs");
+       if !use_sharing then f (p^"_subterm_abbrevs");
+       f (p^"_term_abbrevs");
+       SetStr.iter (Xlp.spec f) !deps
+     in
+     Xlp.create_file_with_deps (p^"_deps") p iter_deps (fun _ -> ());
+     Xlib.concat [p^"_deps.lp";p^"_proofs.lp"] (p^".lp");
+     Xlib.remove [p^"_deps.lp";p^"_proofs.lp"];
+     0
+
+  | "merge"::_ -> 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. *)
@@ -1152,9 +1274,7 @@ and command = function
            List.map (fun s -> b^"_"^s^".dk")
              (if r = All then deps @ ["theorems"] else deps)
          in
-         exit
-           (Sys.command
-              ("cat theory_hol.dk "^String.concat " " infiles^" > "^b^".dk"))
+         Xlib.concat ("theory_hol.dk"::infiles) (b^".dk")
        end
      else
        begin

test.mk

@@ -3,6 +3,10 @@
 .PHONY: default
 default: test1 test2 test3 test4 test5
 
+test%:
+	mkdir -p output$*
+	$(MAKE) -C output$* -f ../test.mk do-test$*
+
 clean:
 	-rm -rf output1 output2 output3 output4 output5
 
@@ -12,49 +16,29 @@ config:
 
 # single dk
 
-.PHONY: test1
-test%:
-	mkdir -p output$*
-	$(MAKE) -C output$* -f ../test.mk do-test$*
-
-.PHONY: do-test1
+.PHONY: test1 do-test1
 do-test1: config
 	hol2dk hol_upto_arith.dk
 	dk check hol_upto_arith.dk
 
 # single lp
 
-.PHONY: test2
-test2:
-	mkdir -p output2
-	$(MAKE) -C output2 -f ../test.mk do-test2
-
-.PHONY: do-test2
+.PHONY: test2 do-test2
 do-test2: config
 	hol2dk hol_upto_arith.lp
 	lambdapi check -v0 -w -c hol_upto_arith.lp
 
 # multi dk
 
-.PHONY: test3
-test3:
-	mkdir -p output3
-	$(MAKE) -C output3 -f ../test.mk do-test3
-
-.PHONY: do-test3
+.PHONY: test3 do-test3
 do-test3: config
 	hol2dk mk 3 hol_upto_arith
 	$(MAKE) -f hol_upto_arith.mk dk
 	dk check hol_upto_arith.dk
 
 # multi lp with mk
 
-.PHONY: test4
-test4:
-	mkdir -p output4
-	$(MAKE) -C output1 -f ../test.mk do-test4
-
-.PHONY: do-test4
+.PHONY: test4 do-test4
 do-test4: config
 	hol2dk mk 3 hol_upto_arith
 	$(MAKE) -f hol_upto_arith.mk lp
@@ -64,12 +48,7 @@ do-test4: config
 
 # multi lp with split
 
-.PHONY: test5
-test5:
-	mkdir -p output5
-	$(MAKE) -C output5 -f ../test.mk do-test5
-
-.PHONY: do-test5
+.PHONY: test5 do-test5
 do-test5: config
 	$(MAKE) split
 	$(MAKE) lp

xlib.ml

@@ -45,7 +45,10 @@ let percent k n = (100 * k) / n;;
 (****************************************************************************)
 
 let command s =
-  if Sys.command s <> 0 then (log "Error: \"%s\" failed.\n" s; exit 1);;
+  match Sys.command s with
+  | 0 -> ()
+  | n -> log "Error: \"%s\" failed.\n" s; exit n
+;;
 
 (****************************************************************************)
 (* Functions on files. *)
@@ -61,11 +64,14 @@ let create_file_bin n f = let oc = log_open_out_bin n in f oc; close_out oc;;
 
 let read_file_bin n f = let ic = log_open_in_bin n in f ic; close_in ic;;
 
-let concat f1 f2 f3 =
-  log "generate %s ...\n%!" f3; command ("cat "^f1^" "^f2^" > "^f3)
+let concat fs out =
+  log "generate %s ...\n%!" out;
+  match fs with
+  | [] -> command ("touch "^out)
+  | _ -> command ("cat "^String.concat " " fs^" > "^out)
 ;;
 
-let remove f = command ("rm -f "^f);;
+let remove fs = command ("rm -f "^String.concat " " fs);;
 
 let copy f1 f2 = log "generate %s ...\n%!" f2; command ("cp -f "^f1^" "^f2);;
 

xlp.ml

@@ -752,11 +752,16 @@ let export_subterm_abbrevs b n =
    [export_term_abbrevs_in_one_file b n] generates
    [n^"_term_abbrevs.lp"] and [n^"_term_abbrevs.typ"]. *)
 let export_term_abbrevs_in_one_file b n =
-  let deps = [b^"_types";b^"_type_abbrevs";b^"_terms"] in
-  export (n^"_term_abbrevs")
-    (if !use_sharing then deps @ [n^"_subterm_abbrevs"] else deps)
-    decl_term_abbrevs;
-  if !use_sharing then export_subterm_abbrevs b n;
+  begin
+    if !use_sharing then
+      let deps =
+        [b^"_types";b^"_type_abbrevs";b^"_terms";n^"_subterm_abbrevs"] in
+      export (n^"_term_abbrevs") deps decl_term_abbrevs;
+      export_subterm_abbrevs b n
+    else
+      let deps = [b^"_types";b^"_type_abbrevs";b^"_terms"] in
+      export (n^"_term_abbrevs") deps decl_term_abbrevs
+  end;
   write_val (n^"_term_abbrevs.typ") !map_typ_abbrev
 ;;
 
@@ -790,8 +795,8 @@ let export_theorem_term_abbrevs_part b n k =
   in
   create_file_with_deps (p^"_head") p iter_deps (fun _ -> ());
   (* generate [p^".lp"] *)
-  concat (p^"_head.lp") (p^"_tail.lp") (p^".lp");
-  remove (p^"_head.lp "^p^"_tail.lp")
+  Xlib.concat [p^"_head.lp";p^"_tail.lp"] (p^".lp");
+  Xlib.remove [p^"_head.lp";p^"_tail.lp"]
 ;;
 
 (****************************************************************************)
@@ -908,8 +913,8 @@ let export_theorem_deps b n =
       SetStr.iter (spec f) (Hashtbl.find htbl_thm_deps i);
     in
     create_file_with_deps (p^"_deps") p iter_deps (fun _ -> ());
-    concat (p^"_deps.lp") (p^"_proofs.lp") (p^".lp");
-    remove (p^"_deps.lp "^p^"_proofs.lp")
+    Xlib.concat [p^"_deps.lp";p^"_proofs.lp"] (p^".lp");
+    Xlib.remove [p^"_deps.lp";p^"_proofs.lp"]
   done
 ;;
 
@@ -1070,9 +1075,9 @@ let export_theorem_proof_part b n k =
   in
   create_file_with_deps (p^"_spec_deps") (p^"_spec") iter_deps (fun _ -> ());
   (* generate [n^part(k)^".lp"] and [n^part(k)^"_spec.lp"] *)
-  concat (p^"_deps.lp") (p^"_body.lp") (p^".lp");
-  concat (p^"_spec_deps.lp") (p^"_spec_body.lp") (p^"_spec.lp");
-  remove (p^"_deps.lp "^p^"_body.lp "^p^"_spec_deps.lp "^p^"_spec_body.lp")
+  Xlib.concat [p^"_deps.lp";p^"_body.lp"] (p^".lp");
+  Xlib.concat [p^"_spec_deps.lp";p^"_spec_body.lp"] (p^"_spec.lp");
+  Xlib.remove [p^"_deps.lp";p^"_body.lp";p^"_spec_deps.lp";p^"_spec_body.lp"]
 ;;
 
 (****************************************************************************)