;; 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?)