;; demo.scm
;;
;; Demonstration of how to use FoolProofScheme with PLT Scheme V200
;;
;; @author Morgan McGuire, morgan@cs.brown.edu
;;
;; @created 2002-02-24
;; @edited 2002-02-24
;;
;; The individual entrypoints in foolproofscheme.ss, typedproc.ss, and
;; basescheme.ss are well documented; look through those files for
;; detailed docs.
;;
;; FoolProofScheme is:
;;
;; List & table (alist) functions
;; (e.g. first, rest, filter, fold, map)
;; table-get, table-set-with-mutation
;; list-copy
;;
;; Typed data structures and procedures
;; typed-tuple, typed-struct, typed-set,
;; proc, define-proc, type-check
;;
;; Type constructors and predicates
;; alist1?, table-of1, proc?, list-of1
;;
;; Convenience functions & macros
;; inc, dec, pow, mem?, not-equal?, ->boolean,
;; symbol-append, assert, neq?, define-macro,
;; symbol-remove-first, string-index
;;
;; HTML pretty printer
;; register-html-conmverter, ->html
;;
;; Use the foolproofscheme unit
(require (file "foolproofscheme.ss"))
;; Only need the second require if you are making macros
(require-for-syntax (file "foolproofscheme.ss"))
;; A typed procedure. Optional type predicates follow arguments and
;; procedures. Types are pre- and post- conditions, not static types
;; for the variables.
(define-proc (factorial x:integer?):integer?
(cond [(<= x 2) x]
[else (* (factorial (- x 1) x))]))
;; A procedure with more complicated types Note that list-of1 checks
;; that at least the first element actually has type integer but
;; assumes the other elements match. This makes the run-time check
;; constant and catches most bugs.
(define-proc (sum L:(list-of1 integer?)):integer?
(cond [(empty? L) 0]
[else (+ (sum (rest L)) (first L))]))
;; Can also define procedures with types using PROC, a typed version
;; of LAMBDA. This procedure uses a typed procedure as a type
;; predicate.
(define div2
(proc (x:(proc (x):boolean?
(and (integer? x)
(even? x)
(> 3 x)))):integer?
(/ x 2)))
;; integer-tuple := integer+
(define-typed-tuple integer-tuple integer?)
;; A set (in the sense that each element appears at most once
;; of integers)
(define-typed-set integer-set integer? equal?)