Make fpXXSyntax modules load successfully and test for same

Prompted by discussion in github issue #1053
HOL-Theorem-Prover · Jul 18, 2022 · ec6a32a · ec6a32a
1 parent ba57e71
commit ec6a32a
Show file tree

Hide file tree

Showing 3 changed files with 27 additions and 5 deletions.
diff --git a/src/floating-point/Holmakefile b/src/floating-point/Holmakefile
@@ -1,5 +1,7 @@
 INCLUDES = ../real ../integer ../n-bit
 
+WORDS_SYNTAX = $(HOLDIR)/src/n-bit/wordsSyntax.uo
+
 all: $(DEFAULT_TARGETS)
 .PHONY: all
 
@@ -18,15 +20,26 @@ fp-sig.uo: fp-sig.sml
 fp-functor.uo: fp-functor.sml fp-sig.uo machine_ieeeTheory.uo
 	$(HOLMOSMLC) -c -toplevel Overlay.ui fp-sig.ui machine_ieeeTheory.ui fp-functor.sml
 
-fp16Syntax.uo: fp-functor.uo fp16Syntax.sml
+fp16Syntax.uo: fp-functor.uo fp16Syntax.sml $(WORDS_SYNTAX)
 	$(HOLMOSMLC) -c -toplevel Overlay.ui fp-sig.ui fp-functor.ui fp16Syntax.sml
 
-fp32Syntax.uo: fp-functor.uo fp32Syntax.sml
+fp32Syntax.uo: fp-functor.uo fp32Syntax.sml $(WORDS_SYNTAX)
 	$(HOLMOSMLC) -c -toplevel Overlay.ui fp-sig.ui fp-functor.ui fp32Syntax.sml
 
-fp64Syntax.uo: fp-functor.uo fp64Syntax.sml
+fp64Syntax.uo: fp-functor.uo fp64Syntax.sml $(WORDS_SYNTAX)
 	$(HOLMOSMLC) -c -toplevel Overlay.ui fp-sig.ui fp-functor.ui fp64Syntax.sml
 
+selftest.exe: selftest.uo
+	$(HOLMOSMLC) -o $@ $<
+
+ifdef HOLSELFTESTLEVEL
+all: floating-point-selftest.log
+
+floating-point-selftest.log: selftest.exe
+	$(tee ./selftest.exe 2>&1,$@)
+
+endif
+
 ifeq ($(KERNELID),otknl)
 ARTFILES = $(patsubst %Script.sml,%.ot.art,$(wildcard *Script.sml))
 

diff --git a/src/floating-point/native/Holmakefile b/src/floating-point/native/Holmakefile
@@ -9,9 +9,9 @@ selftest.exe: selftest.uo
 EXTRA_CLEANS = selftest.exe floating-point-selftest.log
 
 ifdef HOLSELFTESTLEVEL
-all: floating-point-selftest.log
+all: native-floating-point-selftest.log
 
-floating-point-selftest.log: selftest.exe
+native-floating-point-selftest.log: selftest.exe
 	$(tee ./selftest.exe 2>&1,$@)
 
 endif

diff --git a/src/floating-point/selftest.sml b/src/floating-point/selftest.sml
@@ -0,0 +1,9 @@
+open HolKernel boolLib testutils
+
+local open fp64Syntax in end
+open fp16Syntax
+
+val _ = tprint "mk_fp_isZero(16) has correct rator"
+val _ = require_msg (check_result (same_const “machine_ieee$fp16_isZero”))
+                    term_to_string
+                    (rator o mk_fp_isZero) (mk_var("x", “:word16”))