Make readme_gen deal with subdirs and lem files

Author: myreen

Holmakefile

@@ -1,7 +1,7 @@
 INCLUDES = developers $(HOLDIR)/examples/formal-languages/context-free $(HOLDIR)/examples/fun-op-sem/lprefix_lub lem_lib_stub $(HOLDIR)/examples/machine-code/hoare-triple
 OPTIONS = QUIT_ON_FAILURE
 
-README_SOURCES = mlstringScript.sml miscScript.sml COPYING developers build-instructions.sh
+README_SOURCES = mlstringScript.sml miscScript.sml COPYING developers build-instructions.sh lib.lem libScript.sml
 
 THYFILES = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml))
 TARGETS = README.md $(patsubst %.sml,%.uo,$(THYFILES))

README.md

@@ -21,17 +21,76 @@ Directory structure
 [COPYING](COPYING):
 CakeML Copyright Notice, License, and Disclaimer.
 
+[basis](basis):
+Contains the beginnings of a standard basis library for CakeML,
+similar to the standard basis library of SML.
+
 [build-instructions.sh](build-instructions.sh):
 This script installs Poly/ML, HOL and CakeML.
 
+[candle](candle):
+Verification of a HOL theorem prover, based on HOL Light
+(http://www.cl.cam.ac.uk/~jrh13/hol-light/), implemented in CakeML.
+
+[characteristic](characteristic):
+A verified CakeML adaption of Arthur Charguéraud's "Characteristic
+Formulae for the Verification of Imperative Programs"
+
+[compiler](compiler):
+A verified compiler for CakeML, including:
+ - parsing: lexer and PEG parser
+ - inference: type inferencer
+ - backend: compilation to ASM assembly language
+ - targets: code generation to x86, ARM, and more
+
+[developers](developers):
+This directory contains scripts for automating routine tasks, e.g. for
+running regression tests.
+
 [developers](developers):
 This directory contains scripts for automating routine tasks, e.g. for
 running regression tests.
 
+[documentation](documentation):
+Work-in-progress documentation regarding the CakeML language.
+
+[explorer](explorer):
+Tools for stepping through execution of the compiler from one
+intermediate language to the next, and pretty-printing the
+intermediate results. An instance is available on the CakeML website.
+
+[flame](flame):
+The start of a set theory formalisation that has net yet been used.
+
+[lem_lib_stub](lem_lib_stub):
+Empty versions of the Lem libraries (which we don't use, but building
+with Lem requires)
+
+[lib.lem](lib.lem):
+Extensions to Lem's built-in library to target things we need in HOL.
+
 [miscScript.sml](miscScript.sml):
 Miscellaneous definitions and minor lemmas used throughout the
 development.
 
 [mlstringScript.sml](mlstringScript.sml):
 Small theory of wrapped strings, so the translator can distinguish
 them from char lists and can target CakeML strings directly.
+
+[semantics](semantics):
+The definition of the CakeML language. The definition is (mostly)
+expressed in Lem (http://www.cs.kent.ac.uk/~sao/lem), but the
+generated HOL is also included. The directory includes definitions of:
+ - the concrete syntax
+ - the abstract syntax
+ - small step semantics
+ - big step semantics (both functional and relational)
+ - semantics of FFI calls
+ - a type system
+
+[translator](translator):
+A proof-producing translator from HOL functions to CakeML.
+
+[unverified](unverified):
+Various unverified tools, e.g. tools for converting OCaml to CakeML
+and an SML version of the CakeML register allocator.

basis/readmePrefix

@@ -0,0 +1,2 @@
+Contains the beginnings of a standard basis library for CakeML,
+similar to the standard basis library of SML.

candle/readmePrefix

@@ -0,0 +1,2 @@
+Verification of a HOL theorem prover, based on HOL Light
+(http://www.cl.cam.ac.uk/~jrh13/hol-light/), implemented in CakeML.

characteristic/readmePrefix

@@ -0,0 +1,2 @@
+A verified CakeML adaption of Arthur Charguéraud's "Characteristic
+Formulae for the Verification of Imperative Programs"

compiler/readmePrefix

@@ -0,0 +1,5 @@
+A verified compiler for CakeML, including:
+ - parsing: lexer and PEG parser
+ - inference: type inferencer
+ - backend: compilation to ASM assembly language
+ - targets: code generation to x86, ARM, and more

developers/readme_gen.sml

@@ -211,8 +211,17 @@ datatype res = TitleAndContent of string * (string list)
 
 fun isError (Error _) = true | isError _ = false;
 
-fun create_summary filenames = let
-  val filenames = sort (fn s1 => fn s2 => s1 <= s2) filenames
+fun create_summary filenames_and_paths = let
+  val filenames = sort (fn s1 => fn s2 => s1 <= s2) filenames_and_paths
+  (* remove lem generated scrit files *)
+  fun mem x [] = false
+    | mem x (y::ys) = (x = y) orelse mem x ys
+  fun is_lem_generated filename =
+    if String.isSuffix "Script.sml" filename then let
+      val str = String.substring(filename,0,String.size(filename)-10)
+      in mem (str ^ ".lem") filenames end
+    else false
+  val filenames = List.filter (not o is_lem_generated) filenames
   (* read what needs to come first in the output *)
   val filename = PREFIX_FILENAME
   val header = Prefix (read_readme_prefix filename)
@@ -221,7 +230,8 @@ fun create_summary filenames = let
   fun do_filename filename =
     (if (OS.FileSys.isDir filename handle OS.SysErr _ => false) then
        TitleAndContent (filename,read_comment_from_dir filename)
-     else if String.isSuffix ".sml" filename then
+     else if String.isSuffix ".sml" filename orelse
+             String.isSuffix ".lem" filename then
        TitleAndContent (filename,read_comment_from_sml filename)
      else if String.isSuffix ".sh" filename then
        TitleAndContent (filename,read_comment_from_script filename)
@@ -254,4 +264,22 @@ fun create_summary filenames = let
   val _ = TextIO.closeOut(f)
   in () end;
 
-fun main () = (create_summary (CommandLine.arguments ()); ());
+fun all_nondot_subdirs () = let
+  val d = OS.FileSys.openDir(OS.FileSys.getDir())
+  fun all () =
+    case OS.FileSys.readDir(d) of
+      NONE => [] | SOME name => name :: all ()
+  val names = all ()
+  val _ = OS.FileSys.closeDir(d)
+  val names = List.filter (fn n => OS.FileSys.isDir(n)
+                                   handle OS.SysErr _ => false) names
+  val names = List.filter (not o String.isPrefix ".") names
+  in names end
+
+fun main () = let
+  val args = CommandLine.arguments ()
+  val dirs = all_nondot_subdirs ()
+  val _ = create_summary (args @ dirs)
+  in () end;
+
+val filenames_and_paths = ["../lib.lem", "../libScript.sml"]

documentation/readmePrefix

@@ -0,0 +1 @@
+Work-in-progress documentation regarding the CakeML language.

explorer/readmePrefix

@@ -0,0 +1,3 @@
+Tools for stepping through execution of the compiler from one
+intermediate language to the next, and pretty-printing the
+intermediate results. An instance is available on the CakeML website.

flame/readmePrefix

@@ -0,0 +1 @@
+The start of a set theory formalisation that has net yet been used.

lem_lib_stub/readmePrefix

@@ -0,0 +1,2 @@
+Empty versions of the Lem libraries (which we don't use, but building
+with Lem requires)

lib.lem

@@ -1,3 +1,6 @@
+(*
+   Extensions to Lem's built-in library to target things we need in HOL.
+*)
 open import Pervasives
 import List_extra
 import String

libScript.sml

@@ -8,6 +8,9 @@ val _ = numLib.prefer_num();
 
 val _ = new_theory "lib"
 
+(*
+   Extensions to Lem's built-in library to target things we need in HOL.
+*)
 (*open import Pervasives*)
 (*import List_extra*)
 (*import String*)

semantics/readmePrefix

@@ -0,0 +1,9 @@
+The definition of the CakeML language. The definition is (mostly)
+expressed in Lem (http://www.cs.kent.ac.uk/~sao/lem), but the
+generated HOL is also included. The directory includes definitions of:
+ - the concrete syntax
+ - the abstract syntax
+ - small step semantics
+ - big step semantics (both functional and relational)
+ - semantics of FFI calls
+ - a type system

translator/readmePrefix

@@ -0,0 +1 @@
+A proof-producing translator from HOL functions to CakeML.

unverified/readmePrefix

@@ -0,0 +1,2 @@
+Various unverified tools, e.g. tools for converting OCaml to CakeML
+and an SML version of the CakeML register allocator.