update README

Author: ordinarymath

candle/standard/README.md

@@ -9,9 +9,6 @@ generated by the translator (proof-producing synthesis).
 Implementation of the Candle kernel as monadic functions in HOL (i.e. a
 shallow embedding), and proof that they refine the HOL inference system.
 
-[opentheory](opentheory):
-Implementation of an OpenTheory reader based on the Candle kernel.
-
 [semantics](semantics):
 Semantics, soundness, and consistency for the HOL inference system.
 

compiler/README.md

@@ -14,10 +14,6 @@ Two benchmark suites for the CakeML compiler.
 Theories that perform proof-grounded bootstrapping of
 the CakeML compiler in HOL.
 
-[compilationLib.sml](compilationLib.sml):
-Library for in-logic compilation of CakeML abstract syntax producing machine
-code (for a variety of targets) using the CakeML compiler backend.
-
 [compilerScript.sml](compilerScript.sml):
 Definition of the CakeML compiler as a function that takes a list of command
 line arguments and a string corresponding to standard input, and produces a

examples/compilation/README.md

@@ -3,8 +3,5 @@ Compilation of the CakeML examples to different architectures.
 [ag32](ag32):
 Compile the examples via in-logic evaluation to Silver machine code.
 
-[to_word](to_word):
-Example compilation
-
 [x64](x64):
 Compile the examples via in-logic evaluation to x86 machine code.

icing/flover/Infra/README.md

@@ -0,0 +1,16 @@
+Infrastructural lemmas and formalizations for FloVer
+
+[FloverCompLib.sml](FloverCompLib.sml):
+Small changes to computeLib for FloVer
+
+[MachineTypeScript.sml](MachineTypeScript.sml):
+f machine-precision as a datatype for mixed-precision computations
+
+[RealSimpsScript.sml](RealSimpsScript.sml):
+Real-number simplification theorems
+
+[ResultsLib.sml](ResultsLib.sml):
+A monad for results used by FlOVer
+
+[ResultsScript.sml](ResultsScript.sml):
+A simple Result datatype to ease some implementations

icing/flover/semantics/README.md

@@ -0,0 +1,26 @@
+Formalization of idealized semantics of FloVer that handle both real-numbered
+semantics and finite-precision semantics.
+
+Supported types are defined in `Infra/MachineTypesScript.sml`.
+
+[AbbrevsScript.sml](AbbrevsScript.sml):
+This file contains some type abbreviations, to ease writing.
+
+[CommandsScript.sml](CommandsScript.sml):
+Formalization of the Abstract Syntax Tree of a subset used in the Flover
+framework
+
+[ExpressionAbbrevsScript.sml](ExpressionAbbrevsScript.sml):
+Some abbreviations that require having defined expressions beforehand
+If we would put them in the Abbrevs file, this would create a circular
+dependency
+
+[ExpressionSemanticsScript.sml](ExpressionSemanticsScript.sml):
+Formalization of the base expression language for the flover framework
+
+[ExpressionsScript.sml](ExpressionsScript.sml):
+Formalization of the base expression language for the flover framework
+
+[FloverMapScript.sml](FloverMapScript.sml):
+A simple Map datatype for FloVer, implement a version based on lists and one
+based on trees

pancake/README.md

@@ -17,9 +17,6 @@ Simplification of arithmetic in crepLang.
 [crep_to_loopScript.sml](crep_to_loopScript.sml):
 Compilation from crepLang to panLang.
 
-[ffi](ffi):
-FFI for Pancake
-
 [loopLangScript.sml](loopLangScript.sml):
 loopLang intermediate language
 

pancake/static_checker/README.md

@@ -0,0 +1,4 @@
+Support files for Pancake static checker
+
+[panStaticExamplesScript.sml](panStaticExamplesScript.sml):
+* Some simple static checking examples/unit tests/sanity checks for Pancake

pancake/ta_progs/README.md

@@ -1 +1 @@
-Same TA programs
+Some sample timed automata (TA) programs.