Start on READMEs for basis for #71

Author: xrchz

basis/Holmakefile

@@ -3,8 +3,15 @@ OPTIONS = QUIT_ON_FAILURE
 THYFILES = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml))
 TARGETS0 = $(patsubst %Theory.sml,,$(THYFILES))
 TARGETS = $(patsubst %.sml,%.uo,$(TARGETS0))
-all: $(TARGETS) basis_ffi.o
+
+README_SOURCES = basis.sml basis_ffi.c dependency-order
+
+README.md: $(README_SOURCES) readmePrefix ../developers/readme_gen
+	../developers/readme_gen $(README_SOURCES)
+
+all: $(TARGETS) basis_ffi.o README.md
 .PHONY: all
+
 ifndef CC
 CC=gcc
 endif

basis/README.md

@@ -0,0 +1,17 @@
+Contains the beginnings of a standard basis library for CakeML,
+similar to the standard basis library of SML.
+
+[basis.sml](basis.sml):
+Convenience structure that re-exports all the libraries and theories of the
+CakeML basis library.
+
+[basis_ffi.c](basis_ffi.c):
+Implements the foreign function interface (FFI) used in the CakeML basis
+library, as a thin wrapper around the relevant system calls.
+
+[dependency-order](dependency-order):
+This file records the current, linear dependency order between the
+translation/CF theories making up the basis library verification.
+
+[pure](pure):
+HOL definitions of the pure functions used in the CakeML basis.

basis/basis_ffi.c

@@ -1,3 +1,7 @@
+/*
+  Implements the foreign function interface (FFI) used in the CakeML basis
+  library, as a thin wrapper around the relevant system calls.
+*/
 #include <stdio.h>
 #include <string.h>
 #include <stdlib.h>

basis/dependency-order

@@ -1,4 +1,3 @@
-(*
 This file records the current, linear dependency order between the
 translation/CF theories making up the basis library verification.
 
@@ -7,7 +6,6 @@ translator (which provides only translation_extends as a method for joining two
 translations). Eventually, when we have an abstract mode translator, the
 different modules can be made more independent and different combinations can
 be selected than simple prefixes of the current ordering.
-*)
 
 std_prelude
 Runtime

basis/pure/Holmakefile

@@ -1,2 +1,8 @@
 INCLUDES = ../../misc $(HOLDIR)/examples/formal-languages/regular
 OPTIONS = QUIT_ON_FAILURE
+
+README_SOURCES =
+
+README.md: $(README_SOURCES) readmePrefix ../../developers/readme_gen
+	../../developers/readme_gen $(README_SOURCES)
+

basis/pure/README.md

@@ -0,0 +1,4 @@
+HOL definitions of the pure functions used in the CakeML basis.
+
+The CakeML code for the pure parts of the basis is produced
+from these by the translator.

basis/pure/readmePrefix

@@ -0,0 +1,4 @@
+HOL definitions of the pure functions used in the CakeML basis.
+
+The CakeML code for the pure parts of the basis is produced
+from these by the translator.