Commits

Thomas Tuerk committed a895c36

work on HOL 4 libs, now a heap is used

some steps towards getting the HOL 4 libs tested on a more regular basis.
Now a heap called "lemheap" is generated. For a template how to use this
hol heap see "library/Holmakefile". This heap is used for automatically
running the HOL-auxiliary files of the libs through HOL. However, eval
still fails often and we need to provide computeLib with some rewrite
rules for these executable functions. This especially affects maps.

Comments (0)

Files changed (13)

+ifdef POLY
+HOLHEAP_NAME = lemheap
+EXTRA_CLEANS = $(HOLHEAP_NAME) $(HOLHEAP_NAME).o 
+
+BARE_DEPS = lemTheory lem_pervasivesTheory lem_pervasives_extraTheory
+DEPS = $(patsubst %,%.uo,$(BARE_DEPS))
+
+.PHONY: all
+all: $(HOLHEAP_NAME) 
+
+$(HOLHEAP_NAME): $(DEPS)
+	$(protect $(HOLDIR)/bin/buildheap) -o $@ $(BARE_DEPS)
+endif
+OPTIONS = QUIT_ON_FAILURE
+HOLHEAP = ../../hol-lib/lemheap
 
 NOW=$(shell date +%Y-%m-%d---%H-%M-%S)
 OCAML_BUILD_DIR=ocaml-build-dir---${NOW}
+HOL_BUILD_DIR=hol-build-dir---${NOW}
 
 markdown_targets := $(patsubst %.markdown,%.html,$(wildcard *.markdown))
 
 
 ocaml-lib-tests:
 	mkdir -p ${OCAML_BUILD_DIR}
-	../lem -ocaml -outdir ${OCAML_BUILD_DIR} -wl ign -wl_auto_import err -wl_rename err ${LIBS} -only_changed_output
+	../lem -ocaml -outdir ${OCAML_BUILD_DIR} -wl ign -wl_auto_import err -wl_rename err ${LIBS} -only_auxiliary -only_changed_output
 	./run-ocaml-tests.sh ${OCAML_BUILD_DIR}
 
+hol-lib-tests:
+	mkdir -p ${HOL_BUILD_DIR}
+	../lem -hol -outdir ${HOL_BUILD_DIR} -wl ign -wl_auto_import err -wl_rename err ${LIBS} -only_auxiliary -auxiliary_level auto -only_changed_output
+	cp Holmakefile ${HOL_BUILD_DIR}
 markdown: $(markdown_targets)
 
 %.html : %.markdown
 (* Header                                                                     *)
 (* ========================================================================== *)
 
-declare {isabelle} rename module = Lem_either []
-
-declare {ocaml} rename module = Lem_either [`Either`]
-declare {hol} rename module = Lem_either [`sumTheory`; `lem_eitherTheory`]
+declare {isabelle; hol} rename module = Lem_either 
+declare {ocaml} rename module = Lem_either [`Either`; `Lem_either`]
 
 open import Bool Basic_classes List Tuple
 open import {hol} `sumTheory`
+open import {ocaml} `Either`
 
 type either 'a 'b
   = Left  of 'a

library/map_extra.lem

 
 declare ocaml    target_rep function find = `Pmap.find`
 declare isabelle target_rep function find = `map_find`
-declare hol      target_rep function find = `FAPPLY`
+declare hol      target_rep function find k m = `FAPPLY` m k
 
 declare compile_message find = "find is only defined if the key is found. Use lookup instead and handle the not-found case explicitly."
 
 (* It mainly follows the Haskell Maybe-library                                *)
 (******************************************************************************)
 
-declare ~{hol;ocaml;coq} rename module = lem_maybe 
-declare {hol} rename module = lem_maybe [`optionTheory`]
-declare {ocaml} rename module = lem_maybe []
+declare {hol;isabelle;ocaml} rename module = lem_maybe 
 
 open import Bool Basic_classes 
 

library/maybe_extra.lem

 (*                                                                            *)
 (******************************************************************************)
 
-declare {isabelle} rename module = lem_maybe_extra []
-declare {hol} rename module = lem_maybe_extra [`optionTheory`]
-declare {ocaml} rename module = lem_maybe_extra [`Lem_maybe`]
+declare {isabelle; hol; ocaml} rename module = lem_maybe_extra 
 
 open import Basic_classes Maybe
 

library/set_extra.lem

 
 open import Bool Basic_classes Maybe Function Num List Sorting Set
 
-declare ~{lem;coq} rename module = lem_set_extra[]
+declare {hol;isabelle;ocaml} rename module = lem_set_extra
 
 
 (* ----------------------------*)

library/set_helpers.lem

 (* ========================================================================== *)
 
 open import Bool Basic_classes Maybe Function Num 
-declare {isabelle;hol;ocaml} rename module = lem_set_helpers []
+declare {isabelle;hol;ocaml} rename module = lem_set_helpers 
 
 open import {coq} `Coq.Lists.TheoryList`
 
 
 (* The type for tuples (pairs) is hard-coded, so here only a few functions are used *)
 
-declare {isabelle;hol;ocaml} rename module = lem_tuple []
+declare {isabelle;hol;ocaml} rename module = lem_tuple 
 
 open import Bool Basic_classes
 
   ( "-only_changed_output",
     Arg.Unit (fun b -> Process_file.always_replace_files := false),
     " generate only output files, whose content really changed compared to the existing file");
+  ( "-only_auxiliary",
+    Arg.Unit (fun b -> Process_file.only_auxiliary := true),
+    " generate only auxiliary output files");
   ( "-auxiliary_level", 
     Arg.Symbol (["none"; "auto"; "all"], (fun s ->
      Backend.gen_extra_level := (match s with
   (o, (o, temp_file_name, Filename.concat dir file_name)) 
 
 let always_replace_files = ref true 
+let only_auxiliary = ref false
 
 let close_output_with_check (o, temp_file_name, file_name) =
   let _ = close_out o in
               Printf.fprintf o "val _ = numLib.prefer_num();\n\n";
               Printf.fprintf o "\n\n";
             end in
-            let _ = begin
+            let _ = if (!only_auxiliary) then () else begin
               let (o, ext_o) = open_output_with_check dir (module_name_lower ^ "Script.sml") in
               hol_header imported_modules o;
               Printf.fprintf o "val _ = new_theory \"%s\"\n\n" module_name_lower;
       | Target.Target_no_ident(Target.Target_ocaml) -> 
           begin
             let (r_main, r_extra_opt) = B.ocaml_defs m.typed_ast in
-            let _ = begin
+            let _ = if (!only_auxiliary) then () else begin
               let (o, ext_o) = open_output_with_check dir (module_name_lower ^ ".ml") in
               Printf.fprintf o "(*%s*)\n" (generated_line m.filename);
               Printf.fprintf o "%s" (Ulib.Text.to_string r_main);
           begin
           try begin
             let (r_main, r_extra_opt) = B.isa_defs m.typed_ast in
-            let r1 = B.isa_header_defs m.typed_ast in
-            let _ = 
-            begin
+            let _ = if (!only_auxiliary) then () else 
+              begin
                 let (o, ext_o) = open_output_with_check dir (module_name ^ ".thy") in 
+                let r1 = B.isa_header_defs m.typed_ast in
                 Printf.fprintf o "header{*%s*}\n\n" (generated_line m.filename);
                 Printf.fprintf o "theory \"%s\" \n\n" module_name;
                 Printf.fprintf o "imports \n \t Main\n";
       | Target.Target_no_ident(Target.Target_coq) -> 
           try begin
             let (r, r_extra) = B.coq_defs m.typed_ast in
-            let _ =
+            let _ = if (!only_auxiliary) then () else 
               begin
                 let (o, ext_o) = open_output_with_check dir (module_name_lower ^ ".v") in
                   Printf.fprintf o "(* %s *)\n\n" (generated_line m.filename);
     from reprocessing these unchanged files. *)
 val always_replace_files : bool ref
 
+(** [only_auxiliary] determines whether Lem generates only auxiliary files *)
+val only_auxiliary : bool ref
+
 val output_sig : Format.formatter -> Typed_ast.env -> unit