Brings the Redex examples documentation up to date (for 5.0 release)

collects/redex/examples/README

@@ -0,0 +1,52 @@
+The examples subcollection contains several small languages 
+to demonstrate various different uses of PLT Redex:
+
+  arithmetic.rkt: an arithmetic language with every
+  possible order of evaluation
+
+  beginner.rkt: a PLT Redex implementation of (much of) the
+  beginning student teaching language.
+
+  church.rkt: Church numerals with call by name
+  normal order evaluation
+
+  combinators.rkt: fills in the gaps in a proof in
+  Barendregt that i and j (defined in the file) are
+  a combinator basis
+
+  compatible-closure.rkt: an example use of compatible
+  closure. Also, one of the first examples from Matthias
+  Felleisen and Matthew Flatt's monograph
+
+  contracts.rkt: A core contract calculus, including blame, 
+  with function contracts, (eager) pair contracts, 
+  and a few numeric predicates
+
+  letrec.rkt: shows how to model letrec with a store and
+  some infinite looping terms
+
+  omega.rkt: the call by value lambda calculus with call/cc.
+  Includes omega and two call/cc-based infinite loops, one of
+  which has an ever-expanding term size and one of which has
+  a bounded term size.
+
+  pi-calculus.rkt: a formulation of the pi calculus, following
+  Milner's 1990 paper, "Functions as Processes"
+
+  racket-machine: an operational semantics for (much of) Racket 
+  bytecode
+
+  r6rs: an implementation of the R6RS Scheme formal semantics
+
+  semaphores.rkt: a simple threaded language with semaphores
+
+  subject-reduction.rkt: demos traces/pred that type checks
+  the term.
+
+  threads.rkt: shows how non-deterministic choice can be
+  modeled in a reduction semantics. Contains an example use
+  of a simple alternative pretty printer.
+
+  types.rkt: shows how the simply-typed lambda calculus's
+  type system can be written as a rewritten system (see
+  Kuan, MacQueen, Findler in ESOP 2007 for more).

collects/redex/examples/r6rs/README

@@ -1,4 +1,4 @@
-This directory contains the PLT Redex implementation of the
+This directory a the PLT Redex implementation of the
 R6RS operational semantics and a test suite for the
 semantics.
 
@@ -6,20 +6,20 @@ semantics.
 
 == r6rs-tests.ss: the test suite for the semantics. Use:
 
-   mzscheme -t r6rs-tests.ss -m
+   racket -t r6rs-tests.ss -m
 
    to run the tests and see a single period shown per test
    run (each test that explores more than 100 states shows a
    colon for each 100 states it explores). To see a more
    verbose output (that shows each test), use:
 
-   mzscheme -t r6rs-tests.ss -m #t
+   racket -t r6rs-tests.ss -m #t
 
 == show-examples.ss: use this file to explore particular
    examples in a GUI. Its content shows how to use it and
    gives a few examples. Either run it in DrRacket's module
    language, or like this from the commandline:
 
-   mred show-examples.ss
+   gracket show-examples.ss
 
 == test.ss: test suite infrastructure

collects/redex/examples/r6rs/show-examples.rkt

@@ -36,26 +36,21 @@
 ;; example uses of the above functions
 ;; if any of the terms in the graph don't 
 ;;    match p*, they will be colored red
-;; #; comments out an entire sexpression.
 ;; 
 
-#;
 (show '(store () (((lambda (x y) (set! x (+ x y)) x) 2 3))))
 
 ;; an infinite, tail-recursive loop
-#;
 (show-expression '((lambda (x) ((call/cc call/cc) x)) (call/cc call/cc)))
 
 ;; two infinite loops, one in left-to-right and one in right-to-left evaluation order
 ;; one goes into a non-tail infinite loop, the other's reduction graph has a cycle
-#;
 (step '(store () 
               ((call/cc call/cc) 
                (call/cc call/cc))))
 
 
 ;; demonstrates sharing
-#;
 (show-expression
  '((lambda (c)
      ((lambda (x y)