Work on READMEs in examples for #71

Author: xrchz

examples/Holmakefile

@@ -7,8 +7,10 @@ TARGETS = $(patsubst %.sml,%.uo,$(TARGETS0))
 all: $(TARGETS)
 .PHONY: all
 
-README.md: readmePrefix ../developers/readme_gen
-	../developers/readme_gen
+README_SOURCES = $(wildcard *Script.sml)
+DIRS = $(wildcard */)
+README.md: ../developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
+	../developers/readme_gen $(README_SOURCES)
 all: README.md
 
 ifdef POLY

examples/README.md

@@ -3,5 +3,58 @@ Examples of verified programs built using CakeML infrastructure.
 Larger examples (like the CakeML compiler and Candle theorem prover) can be
 found in their own top-level directories.
 
+[catProgScript.sml](catProgScript.sml):
+cat program example: concatenate and print lines from files.
+
 [compilation](compilation):
 Theories for compiling the examples in the logic
+
+[diffProgScript.sml](diffProgScript.sml):
+diff example: find a patch representing the difference between two files.
+
+[diffScript.sml](diffScript.sml):
+Implementation and verification of diff and patch algorithms
+
+[echoProgScript.sml](echoProgScript.sml):
+echo program example: print the command line arguments.
+
+[grepProgScript.sml](grepProgScript.sml):
+grep example: search for file lines matching a regular expression.
+
+[helloErrProgScript.sml](helloErrProgScript.sml):
+Hello World on standard error.
+
+[helloProgScript.sml](helloProgScript.sml):
+Hello World example, printing to standard output.
+
+[insertSortProgScript.sml](insertSortProgScript.sml):
+In-place insertion sort on a polymorphic array.
+
+[iocatProgScript.sml](iocatProgScript.sml):
+Faster cat: process 2048 chars at a time.
+
+[lcsScript.sml](lcsScript.sml):
+Verification of longest common subsequence algorithms.
+
+[patchProgScript.sml](patchProgScript.sml):
+patch example: apply a patch to a file.
+
+[queueProgScript.sml](queueProgScript.sml):
+An example of a queue data structure implemented using CakeML arrays, verified
+using CF.
+
+[quicksortProgScript.sml](quicksortProgScript.sml):
+In-place quick sort on a polymorphic array.
+
+[sortProgScript.sml](sortProgScript.sml):
+Program to sort the lines in a file, built on top of the quick sort example.
+
+[splitwordsScript.sml](splitwordsScript.sml):
+A high-level specification of words and frequencies
+
+[stackProgScript.sml](stackProgScript.sml):
+An example of a stack data structure implemented using CakeML arrays, verified
+using CF.
+
+[wordcountProgScript.sml](wordcountProgScript.sml):
+Simple wordcount program, to demonstrate use of CF.

examples/catProgScript.sml

@@ -1,3 +1,8 @@
+(*
+  cat program example: concatenate and print lines from files.
+
+  Simple version that operates one character at a time.
+*)
 open preamble basis
 
 val _ = new_theory "catProg"

examples/diffProgScript.sml

@@ -1,3 +1,6 @@
+(*
+  diff example: find a patch representing the difference between two files.
+*)
 open preamble basis
      charsetTheory lcsTheory diffTheory
 

examples/echoProgScript.sml

@@ -1,3 +1,6 @@
+(*
+  echo program example: print the command line arguments.
+*)
 open preamble basis
 
 val _ = new_theory "echoProg";

examples/grepProgScript.sml

@@ -1,3 +1,6 @@
+(*
+  grep example: search for file lines matching a regular expression.
+*)
 open preamble basis
      charsetTheory regexpTheory regexp_parserTheory regexp_compilerTheory
 

examples/helloErrProgScript.sml

@@ -1,3 +1,6 @@
+(*
+  Hello World on standard error.
+*)
 open preamble basis
 
 val _ = new_theory "helloErrProg"

examples/helloProgScript.sml

@@ -1,3 +1,6 @@
+(*
+  Hello World example, printing to standard output.
+*)
 open preamble basis
 
 val _ = new_theory "helloProg"

examples/insertSortProgScript.sml

@@ -1,3 +1,6 @@
+(*
+  In-place insertion sort on a polymorphic array.
+*)
 open preamble semanticPrimitivesTheory
      ml_translatorTheory ml_translatorLib ml_progLib cfLib
      basisFunctionsLib ArrayProofTheory

examples/iocatProgScript.sml

@@ -1,3 +1,6 @@
+(*
+  Faster cat: process 2048 chars at a time.
+*)
 open preamble basis
 
 val _ = new_theory "iocatProg"

examples/patchProgScript.sml

@@ -1,3 +1,6 @@
+(*
+  patch example: apply a patch to a file.
+*)
 open preamble basis
      charsetTheory diffTheory
 

examples/quicksortProgScript.sml

@@ -1,3 +1,6 @@
+(*
+  In-place quick sort on a polymorphic array.
+*)
 open preamble semanticPrimitivesTheory
 open ml_translatorTheory ml_translatorLib ml_progLib cfLib basisFunctionsLib
 open basisProgTheory ArrayProofTheory
@@ -6,6 +9,8 @@ val _ = new_theory "quicksortProg";
 
 val _ = translation_extends"basisProg";
 
+(* TODO: move *)
+
 val list_rel_perm_help = Q.prove (
   `!l1 l2.
     PERM l1 l2
@@ -143,6 +148,8 @@ val length_gt1 = Q.store_thm ("length_gt1",
   Cases_on `t` >>
   fs []);
 
+(* -- *)
+
 fun basis_st () = get_ml_prog_state ()
 
 val partition = process_topdecs `

examples/sortProgScript.sml

@@ -1,3 +1,6 @@
+(*
+  Program to sort the lines in a file, built on top of the quick sort example.
+*)
 open preamble basis quicksortProgTheory
 
 val _ = new_theory "sortProg";