Add libmGen, a simple generator for mathematical functions

.gitignore

@@ -77,6 +77,10 @@ compiler/benchmarks/*.dat
 compiler/benchmarks/*.eps
 
 #sexp files generated by Icing
-icing/examples/output/*/*.sexp.cml
-icing/examples/*_data_prog.txt
+floatingPoint/icing/examples/output/*/*.sexp.cml
+floatingPoint/icing/examples/*_data_prog.txt
 .DS_Store
+
+#Sollya build files for floating-point tools
+floatingPoint/tools/dandelion/sollya-8.0/*
+

candle/prover/candle_prover_evaluateScript.sml

@@ -649,6 +649,11 @@ Proof
     \\ first_assum (irule_at Any)
     \\ simp [v_ok_def])
   \\ Cases_on ‘op = RealFromFP’ \\ gs[]
+  >- (
+    rw[do_app_cases] \\ gs [SF SFY_ss]
+    \\ first_assum (irule_at Any)
+    \\ simp [v_ok_def])
+  \\ Cases_on ‘op = RealFromIntProd’ \\ gs[]
   >- (
     rw[do_app_cases] \\ gs [SF SFY_ss]
     \\ first_assum (irule_at Any)

candle/prover/permsScript.sml

@@ -578,6 +578,10 @@ Proof
     rw [do_app_cases] \\ gs[]
     \\ rw [perms_ok_def])
   \\ Cases_on ‘op = RealFromFP’ \\ gs[]
+  >- (
+    rw [do_app_cases] \\ gs[]
+    \\ rw [perms_ok_def])
+  \\ Cases_on ‘op = RealFromIntProd’ \\ gs[]
   >- (
     rw [do_app_cases] \\ gs[]
     \\ rw [perms_ok_def])

compiler/inference/inferScript.sml

@@ -378,6 +378,7 @@ val op_to_string_def = Define `
 (op_to_string (Real_uop _) = (implode "Real_uop", 1)) ∧
 (op_to_string (Real_cmp _) = (implode "Real_cmp", 2)) ∧
 (op_to_string (RealFromFP) = (implode "RealFromFP", 1)) ∧
+(op_to_string (RealFromIntProd) = (implode "RealFromIntProd", 1)) ∧
 (op_to_string (Shift _ _ _) = (implode "Shift", 1)) ∧
 (op_to_string Equality = (implode "Equality", 2)) ∧
 (op_to_string Opapp = (implode "Opapp", 2)) ∧
@@ -556,6 +557,7 @@ constrain_op l op ts =
    | (Real_bop _, _) => failwith l (implode "Reals do not have a type")
    | (Real_cmp _, _) => failwith l (implode "Reals do not have a type")
    | (RealFromFP, _) => failwith l (implode "Reals do not have a type")
+   | (RealFromIntProd, _) => failwith l (implode "Reals do not have a type")
    | (AallocFixed, _) => failwith l (implode "Unsafe ops do not have a type") (* not actually unsafe *)
    | (Eval, _) => failwith l (implode "Unsafe ops do not have a type")
    | (Env_id, _) => failwith l (implode "Unsafe ops do not have a type")

compiler/parsing/fromSexpScript.sml

@@ -688,6 +688,7 @@ val sexpop_def = Define`
   if s = "RealbopRealMul" then SOME (Real_bop realOps$Real_Mul) else
   if s = "RealbopRealDiv" then SOME (Real_bop realOps$Real_Div) else
   if s = "RealFromFP" then SOME (RealFromFP) else
+  if s = "RealFromIntProd" then SOME (RealFromIntProd) else
   if s = "Opapp" then SOME Opapp else
   if s = "Opassign" then SOME Opassign else
   if s = "Opref" then SOME Opref else
@@ -1335,6 +1336,7 @@ val opsexp_def = Define`
   (opsexp (Real_bop realOps$Real_Mul) = SX_SYM "RealbopRealMul") ∧
   (opsexp (Real_bop realOps$Real_Div) = SX_SYM "RealbopRealDiv") ∧
   (opsexp (RealFromFP) = SX_SYM "RealFromFP") ∧
+  (opsexp (RealFromIntProd) = SX_SYM "RealFromIntProd") ∧
   (opsexp Opapp = SX_SYM "Opapp") ∧
   (opsexp Opassign = SX_SYM "Opassign") ∧
   (opsexp Opref = SX_SYM "Opref") ∧

compiler/repl/evaluate_initScript.sml

@@ -675,6 +675,11 @@ Proof
     \\ ‘s with <| refs := s.refs; ffi := s.ffi |> = s’ suffices_by gs[]
     \\ gs[state_component_equality])
   \\ Cases_on ‘op = RealFromFP’ \\ gs[]
+  >- (
+    gvs[do_app_cases, v_ok_thm]
+    \\ ‘s with <| refs := s.refs; ffi := s.ffi |> = s’ suffices_by gs[]
+    \\ gs[state_component_equality])
+  \\ Cases_on ‘op = RealFromIntProd’ \\ gs[]
   >- (
     gvs[do_app_cases, v_ok_thm]
     \\ ‘s with <| refs := s.refs; ffi := s.ffi |> = s’ suffices_by gs[]

compiler/repl/evaluate_skipScript.sml

@@ -1790,6 +1790,13 @@ Proof
     \\ rpt (irule_at Any SUBMAP_REFL) \\ gs []
     \\ first_assum (irule_at Any) \\ gs [])
   \\ Cases_on ‘op = RealFromFP’ \\ gs[]
+  >- (
+    Cases_on ‘res’ \\ gvs [do_app_def, v_rel_def, OPTREL_def,
+                           CaseEqs ["list", "v", "option", "prod", "lit",
+                                    "store_v", "v"]]
+    \\ rpt (irule_at Any SUBMAP_REFL) \\ gs []
+    \\ first_assum (irule_at Any) \\ gs [])
+  \\ Cases_on ‘op = RealFromIntProd’ \\ gs[]
   >- (
     Cases_on ‘res’ \\ gvs [do_app_def, v_rel_def, OPTREL_def,
                            CaseEqs ["list", "v", "option", "prod", "lit",

developers/build-sequence

@@ -4,6 +4,14 @@
 developers
 developers/bin
 
+# Floating-Point optimizer & codegen
+floatingPoint/tools/dandelion
+floatingPoint/icing/
+floatingPoint/icing/examples
+
+# Floating-Point codegen
+floatingPoint/libmGen/
+
 # build many things in parallel at the start
 compiler/proofs
 compiler/bootstrap/translation
@@ -127,11 +135,6 @@ compiler/parsing/tests
 compiler/inference/tests
 compiler/printing/test
 
-# Floating-Point optimizer
-icing/flover
-icing/
-icing/examples
-
 # compiler translation
 compiler/repl
 

floatingPoint/README.md

@@ -0,0 +1,5 @@
+# Floating-point related tooling for CakeML
+
+This directory contains tools for implementation of elementary functions (`libmGen`),
+and to optimize floating-point arithmetic (`icing`).
+The `tools` directory contains dependencies used in both implementations.

icing/Holmakefile → floatingPoint/icing/Holmakefile

@@ -4,7 +4,7 @@ INCLUDES = $(HOLDIR)/examples/formal-languages/context-free\
 	   $(CAKEMLDIR)/semantics $(CAKEMLDIR)/characteristic\
 	   $(CAKEMLDIR)/compiler $(CAKEMLDIR)/compiler/inference\
 	   $(CAKEMLDIR)/compiler/backend/proofs\
-	   $(CAKEMLDIR)/icing/flover
+	   $(CAKEMLDIR)/floatingPoint/tools/flover
 
 all: $(DEFAULT_TARGETS) README.md
 .PHONY: all

icing/README.md → floatingPoint/icing/README.md

@@ -34,9 +34,6 @@ theorems.
 Translation from CakeML floating-point computations to
 CakeML real-number computations.
 
-[flover](flover):
-# FloVer - A Certificate Checker for Roundoff Error Bounds
-
 [icingTacticsLib.sml](icingTacticsLib.sml):
 Tactic library for PrincessCake development
 

icing/examples/Holmakefile → floatingPoint/icing/examples/Holmakefile

@@ -4,7 +4,7 @@ INCLUDES = $(HOLDIR)/examples/formal-languages/context-free\
 	   $(CAKEMLDIR)/semantics $(CAKEMLDIR)/characteristic\
 	   $(CAKEMLDIR)/compiler $(CAKEMLDIR)/compiler/inference\
 	   $(CAKEMLDIR)/compiler/backend/semantics\
-           $(CAKEMLDIR)/icing $(CAKEMLDIR)/icing/flover
+           $(CAKEMLDIR)/floatingPoint/icing $(CAKEMLDIR)/floatingPoint/tools/flover
 
 #Explicitly without $(DEFAULT_TARGETS) to reduce compilation time
 DEFAULT_TARGETS = dopplerProgCompTheory.uo

icing/pull_wordsScript.sml → floatingPoint/icing/pull_wordsScript.sml

@@ -1316,6 +1316,7 @@ Proof
   >- trivial_tac
   >- trivial_tac
   >- trivial_tac
+  >- trivial_tac
   >- (
     rpt strip_tac
     >> ‘LENGTH a1 = LENGTH a2’ by (irule LIST_REL_LENGTH >> asm_exists_tac >> gs[])