Changeset 34637 in project


Ignore:
Timestamp:
09/22/17 18:49:34 (4 weeks ago)
Author:
juergen
Message:

simple-contracts 1.4 with syntax additions

Location:
release/4/simple-contracts
Files:
6 edited
1 copied

Legend:

Unmodified
Added
Removed
  • release/4/simple-contracts/tags/1.4/simple-contracts.scm

    r33853 r34637  
    4343duties and the supplier is not even forced to do anything at all. In
    4444other words, the supplier can safely assume a procedure is called
    45 with correct arguments, he or she need not and should not check tehem
     45with correct arguments, he or she need not and should not check them
    4646again.
    4747
     
    5252changes.
    5353
    54 (xdefine ((r r? ...) ... name (a a? ...) ... [as as? ...]) xpr ....)
    55 
    56 where name is the name of the procedure, r ... are retrurn values with
     54(xdefine ((r r? ...) .. name (a a? ...) ...) xpr ....)
     55or -- with variable arguments --
     56(xdefine ((r r? ...) .. name (a a? ...) ... as as? ...) xpr ....)
     57
     58where name is the name of the procedure, r .. are return values with
    5759corresponding postconditions r? ..., a ... are fixed variables with
    5860preconditions a? ... and as is an optional variable argument with
    5961preconditions as? ...
    6062
    61 For state-changing routines, so called commands, xlambda must
    62 be used. The syntax is
    63 
    64 (xlambda k ((r r? ...) ... (a a? ...) ... [as as? ...]) xpr ....)
    65 
    66 where k is the number of return values. xlambda can be defined on top of
    67 a let, thus supplying state. But even those routines must return values,
    68 namely the values of state variables before a state change has taken
    69 place. So one can check, if the state change did what it should have
    70 done.
     63If you want to export the documentation of pre- and postcoditions, you
     64can use (here without varible arguments)
     65
     66(xdefine ((r r? ...) .. #(name-post name name-pre) (a a? ...) ...) xpr ....)
     67
     68Note, that post- and precondition documentation is placed next to
     69the corresponding conditions.
     70
     71xdefine is implemented with xlambda, whose syntax --for variable
     72argument lists -- is
     73
     74(xlambda ((r r? ...) .. <- (a a? ...) ... as as? ...) xpr ....)
     75
     76where <- separates the return values from the arguments. These
     77expressions can be bound via define or define-values to export the
     78documentation as well. But note that in the latter case the routine must
     79be named first, of course, so that we have
     80
     81(define-values (proc proc-pre proc-post) (xlambda ...))
     82
     83For state-changing routines, so called commands, xlambda can be defined
     84on top of a let, thus supplying state.
     85
     86To make postcondition-checking easy and command-chaining possible,
     87commands should return values as well, namely the changed state
     88variables after and before the change, for example
     89
     90(let ((state ...))
     91  (xlambda ((new new? ...) (old old? ...)
     92            <-
     93            (a a? ...) ...) | (a a? ...) ... as as? ...)
     94            xpr ....)
     95
     96So one can check, if the state change did what it should have done.
    7197
    7298Note, that a parameter, contract-check-level, is supplied, so that one
     
    152178                          (list (car args)))))))
    153179
    154 ;;; TODO: replace prec and cons by contracts
     180;;; TODO: replace proc and cons by contracts
    155181;;;(preconditions proc pre post)
    156182;;;(postconditions proc pre post)
     
    162188;;; dbc for procedures
    163189;;; ==================
     190;;; old version, used in new version below
    164191;;; (xlambda [k] ((r1 r1? ...) ...(rk rk? ...)
    165192;;;               (x x? ...) ... xs xs? ...)
     
    172199;;; x ... are the fixed arguments, xs the optional variable arguments,
    173200;;; the following predicates naming the corresponding preconditions.
    174 (define-ir-macro (xlambda form inject compare?)
     201(define-ir-macro (xlambda% form inject compare?)
     202;(define-ir-macro (xlambda form inject compare?)
    175203  (let ((multi? (integer? (cadr form))))
    176204    (let ((k (if multi? (cadr form) 1))
     
    202230                         '()
    203231                         (car xrest)))
    204                 (loc (inject 'xlambda)))
     232                (loc (inject 'xlambda%)))
     233                ;(loc (inject 'xlambda)))
    205234            (let* (
    206235              ;; no checks
     
    303332                 ))))))))
    304333
    305 ;;; (xdefine ((r1 r1? ...) ... (rk rk? ...)
    306 ;;;           name
    307 ;;;           (x x? ...) ... xs xs? ...)
    308 ;;;            xpr . xprs)
    309 ;;; ----------------------------------------------
     334;;; new version:
     335;;; (xlambda ((r r? ...) .. <- (x x? ...) ...) xpr ....)
     336;;; or
     337;;; (xlambda ((r r? ...) .. <- (x x? ...) ... xs xs? ...) xpr ....)
     338;;; or old versions (deprecated):
     339;;; (xlambda k ((r1 r1? ...) ...(rk rk? ...)
     340;;;             (x x? ...) ... ) xpr ....)
     341;;; (xlambda k ((r1 r1? ...) ... (rk rk? ...)
     342;;;             (x x? ...) ... xs xs? ...) xpr ....)
     343;;; (xlambda ((r r? ...) (x x? ...) ... ) xpr ....)
     344;;; (xlambda ((r r? ...) (x x? ...) ... xs xs? ...) xpr ....)
     345;;; --------------------------------------------------------
     346(define-er-macro (xlambda form rename compare?)
     347  (let* ((k (cadr form)) (iform (if (integer? k)
     348                                  (cddr form)
     349                                  (cdr form))))
     350    (let ((header (car iform)) (body (cdr iform))
     351          (%xlambda% (rename 'xlambda%)) (%<- (rename '<-)))
     352      (if (integer? k)
     353        `(,%xlambda% ,k ,header ,@body)
     354        (receive (results args)
     355          (let loop ((header header) (results '()))
     356            (cond
     357              ((null? header) ; no <- symbol
     358               (let ((header (reverse results)))
     359                 (values (list (car header)) (cdr header))))
     360              ((compare? (car header) %<-)
     361               (values (reverse results) (cdr header)))
     362              (else
     363                (loop (cdr header) (cons (car header) results)))))
     364          `(,%xlambda% ,(length results) (,@results ,@args) ,@body))))))
     365
     366;;; (xdefine ((r r? ...) .. name (x x? ...) ...) xpr ....)
     367;;; or
     368;;; (xdefine ((r r? ...) .. #(post name pre) (x x? ...) ...) xpr ....)
     369;;; or
     370;;; (xdefine ((r r? ...) .. name (x x? ...) ... xs xs? ...) xpr ....)
     371;;; or
     372;;; (xdefine ((r r? ...) .. #(post name pre) (x x? ...) ... xs xs? ...) xpr ....)
     373;;; -----------------------------------------------------------------------------
     374;;; defines name -- and possibly post- and precondition documentation -- as a
     375;;; contract-checked procedure with postconditions named r checked by
     376;;; predicates r? ... and preconditions x ... xs .. checked by x? ...
     377;;; and xs? ...
    310378(define-er-macro (xdefine form rename compare?)
    311379  (let ((header (cadr form))
    312380        (xpr (caddr form))
    313381        (xprs (cdddr form))
     382        (%<- (rename '<-))
    314383        (%define (rename 'define))
    315         (%xlambda (rename 'xlambda)))
    316     (receive (k main returns)
    317       (let loop ((n 0) (tail header) (head '()))
    318         (if (symbol? (car tail))
    319           (values n tail (reverse head))
    320           (loop (+ n 1) (cdr tail) (cons (car tail) head))))
    321       `(,%define ,(car main)
    322                  (,%xlambda ,k ,(append returns (cdr main)) ,xpr ,@xprs)))))
     384        (%xlambda (rename 'xlambda))
     385        (%define-values (rename 'define-values)))
     386    (receive (posts names pres)
     387      (let loop ((tail header) (head '()))
     388        (if (or (symbol? (car tail)) (vector? (car tail)))
     389          (values (reverse head) (car tail) (cdr tail))
     390          (loop (cdr tail) (cons (car tail) head))))
     391      (if (symbol? names)
     392        `(,%define ,names
     393                   (,%xlambda (,@posts ,%<- ,@pres) ,xpr ,@xprs))
     394        `(,%define-values ,(list (vector-ref names 1) ; name
     395                                 (vector-ref names 2) ; pres
     396                                 (vector-ref names 0)); posts
     397                   (,%xlambda (,@posts ,%<- ,@pres) ,xpr ,@xprs))
     398        ))))
    323399
    324400;;; (simple-contracts sym ..)
     
    339415    (xdefine
    340416      macro:
    341       (xdefine ((r r? ...) ... name (a a? ...) ... [as as? ...]) . body)
     417      (xdefine ((r r? ...) .. name (a a? ...) ...) xpr ....)
     418      (xdefine ((r r? ...) .. #(post name pre) (a a? ...) ...) xpr ....)
     419      (xdefine ((r r? ...) .. name (a a? ...) ... as as? ...) xpr ....)
     420      (xdefine ((r r? ...) .. #(post name pre) (a a? ...) ... as as? ...) xpr ....)
    342421      "contract guarded version of define for procedures, where"
    343       "name is the name of the procedure"
     422      "name is the name of the procedure, post and pre"
     423      "the documentations of the pre- and postconditions respectively"
    344424      "r ... are return values with corresponding postcondition r?"
    345425      "a ... are fixed arguments with preconditions a? ..."
    346       "as is an optional variable argument with preconditions as? ...")
     426      "as is an optional variable argument with preconditions as? ..."
     427      "xpr starts the body")
    347428    (xlambda
    348429      macro:
    349       (xlambda k ((r r? ...) ... (a a? ...) ... [as as? ...]) . body)
     430      (xlambda ((r r? ...) .. <- (a a? ...) ...) xpr ...)
     431      (xlambda ((r r? ...) .. <- (a a? ...) ... as as? ...) xpr ...)
    350432      "contract guarded version of lambda, where"
    351       "k is the number of returned values r ..."
    352       "r? ... their corresponding postconditions"
     433      "<- separates returned values r .. from arguments"
     434      "r? ... are their corresponding postconditions"
    353435      "a ... are fixed arguments with preconditions a? ..."
    354436      "as is an optional variable argument with preconditions as? ..."
    355       "procedures with state change should return old versions"
     437      "xpr starts the body"
     438      "procedures with state change should return new and old versions"
    356439      "of state variables before the state change")
    357440    (%%
     
    362445      macro:
    363446      (pipe combination ...)
    364       "sequencing curried combinations")
     447      "sequencing curried combinations from left to right")
    365448    )))
    366449    (case-lambda
  • release/4/simple-contracts/tags/1.4/simple-contracts.setup

    r33861 r34637  
    77 'simple-contracts
    88 '("simple-contracts.so" "simple-contracts.import.so")
    9  '((version "1.3.1")))
     9 '((version "1.4")))
  • release/4/simple-contracts/tags/1.4/tests/run.scm

    r33853 r34637  
    1 (use simple-tests simple-contracts)
     1(use simple-tests simple-exceptions simple-contracts)
    22(contract-check-level 1)
    33
     
    3030(define-test (contracts?)
    3131  (check
    32     "STATE"
     32    "COMMANDS"
    3333    (define-values (counter! counter)
    3434      (let ((state 0))
    3535        (values
    36           (xlambda 1 ((old (pipe (+ 1) (= state))))
    37             (let ((o state))
     36          (xlambda ((new (pipe (= (add1 old))))
     37                         ;integer? (pipe (= (add1 old))))
     38                         ;integer? (lambda (x) (= x (add1 old))))
     39                    (old integer?)
     40                    <-)
     41            (let ((old state))
    3842              (set! state (add1 state))
    39               o))
    40           (xlambda 1 ((result (pipe (= state))))
     43              (values state old)))
     44          (xlambda ((result (pipe (= state))) <-)
    4145            state))))
    4246    (zero? (counter))
     
    4650    (= (counter) 2)
    4751 
     52    (define-values (push pop top)
     53      (let ((stk '()))
     54        (let (
     55          (push
     56            (xlambda ((new list? (pipe (equal? (cons arg old))))
     57                      (old list?)
     58                      <-
     59                      (arg))
     60              (let ((old stk))
     61                (set! stk (cons arg stk))
     62                (values stk old))))
     63          (pop
     64            (xlambda ((new list? (pipe (equal? (cdr old))))
     65                      (old list?)
     66                      <-)
     67              (let ((old (<< stk 'pop (pipe (null?) (not)))))
     68                (set! stk (cdr stk))
     69                (values stk old))))
     70          (top
     71            (xlambda ((result) <-)
     72              (car (<< stk 'top (pipe (null?) (not))))))
     73          )
     74          (values push pop top)
     75          )))
     76    ;(top) ; precondition violated
     77    ;(pop) ; precondition violated
     78    (push 0)
     79    (push 1)
     80    (= 1 (top))
     81    (equal? (call-with-values (lambda () (push 2)) list)
     82            '((2 1 0) (1 0)))
     83    (= 2 (top))
     84    (equal? (call-with-values (lambda () (pop)) list)
     85            '((1 0) (2 1 0)))
     86
     87    "QUERIES"
    4888    (define-values (add add-pre add-post)
    49       ;(xlambda 1 ((result integer? odd? (pipe (= (apply + x y ys))))
    5089      (xlambda ((result integer? odd? (pipe (= (apply + x y ys))))
     90                <-
    5191                (x integer? odd?) (y integer? even?) ys integer? even?)
    5292        (apply + x y ys)))
     
    61101
    62102    (define wrong-add
    63       ;(xlambda 1 ((result integer? even?)
    64103      (xlambda ((result integer? even?)
     104                <-
    65105                (x integer? odd?) xs integer?  even?)
    66106        (apply + x xs)))
     
    68108 
    69109    (define-values (divide divide-pre divide-post)
    70       (xlambda 2 ((q integer?)
    71                   (r (pipe (+ (* n q))
    72                            (= m)))
    73                   (m integer? (pipe (>= 0)))
    74                   (n integer? positive?))
     110      (xlambda ((q integer?)
     111                (r (pipe (+ (* n q))
     112                         (= m)))
     113                <-
     114                (m integer? (pipe (>= 0)))
     115                (n integer? positive?))
    75116        (let loop ((q 0) (r m))
    76117          (if (< r n)
     
    90131 
    91132    "XDEFINE"
    92     (xdefine ((result integer?) sum (a integer?) as integer?)
     133    ;(xdefine ((result integer?) sum (a integer?) as integer?)
     134    (xdefine ((result integer?) #(sum-post sum sum-pre) (a integer?) as integer?)
    93135      (apply + a as))
     136    ;(print sum-post)
     137    ;(print sum-pre)
    94138    (= (sum 1 2 3) 6)
    95139    (not (condition-case (sum 1 2 #f) ((exn argument) #f)))
  • release/4/simple-contracts/trunk/simple-contracts.scm

    r33853 r34637  
    4343duties and the supplier is not even forced to do anything at all. In
    4444other words, the supplier can safely assume a procedure is called
    45 with correct arguments, he or she need not and should not check tehem
     45with correct arguments, he or she need not and should not check them
    4646again.
    4747
     
    5252changes.
    5353
    54 (xdefine ((r r? ...) ... name (a a? ...) ... [as as? ...]) xpr ....)
    55 
    56 where name is the name of the procedure, r ... are retrurn values with
     54(xdefine ((r r? ...) .. name (a a? ...) ...) xpr ....)
     55or -- with variable arguments --
     56(xdefine ((r r? ...) .. name (a a? ...) ... as as? ...) xpr ....)
     57
     58where name is the name of the procedure, r .. are return values with
    5759corresponding postconditions r? ..., a ... are fixed variables with
    5860preconditions a? ... and as is an optional variable argument with
    5961preconditions as? ...
    6062
    61 For state-changing routines, so called commands, xlambda must
    62 be used. The syntax is
    63 
    64 (xlambda k ((r r? ...) ... (a a? ...) ... [as as? ...]) xpr ....)
    65 
    66 where k is the number of return values. xlambda can be defined on top of
    67 a let, thus supplying state. But even those routines must return values,
    68 namely the values of state variables before a state change has taken
    69 place. So one can check, if the state change did what it should have
    70 done.
     63If you want to export the documentation of pre- and postcoditions, you
     64can use (here without varible arguments)
     65
     66(xdefine ((r r? ...) .. #(name-post name name-pre) (a a? ...) ...) xpr ....)
     67
     68Note, that post- and precondition documentation is placed next to
     69the corresponding conditions.
     70
     71xdefine is implemented with xlambda, whose syntax --for variable
     72argument lists -- is
     73
     74(xlambda ((r r? ...) .. <- (a a? ...) ... as as? ...) xpr ....)
     75
     76where <- separates the return values from the arguments. These
     77expressions can be bound via define or define-values to export the
     78documentation as well. But note that in the latter case the routine must
     79be named first, of course, so that we have
     80
     81(define-values (proc proc-pre proc-post) (xlambda ...))
     82
     83For state-changing routines, so called commands, xlambda can be defined
     84on top of a let, thus supplying state.
     85
     86To make postcondition-checking easy and command-chaining possible,
     87commands should return values as well, namely the changed state
     88variables after and before the change, for example
     89
     90(let ((state ...))
     91  (xlambda ((new new? ...) (old old? ...)
     92            <-
     93            (a a? ...) ...) | (a a? ...) ... as as? ...)
     94            xpr ....)
     95
     96So one can check, if the state change did what it should have done.
    7197
    7298Note, that a parameter, contract-check-level, is supplied, so that one
     
    152178                          (list (car args)))))))
    153179
    154 ;;; TODO: replace prec and cons by contracts
     180;;; TODO: replace proc and cons by contracts
    155181;;;(preconditions proc pre post)
    156182;;;(postconditions proc pre post)
     
    162188;;; dbc for procedures
    163189;;; ==================
     190;;; old version, used in new version below
    164191;;; (xlambda [k] ((r1 r1? ...) ...(rk rk? ...)
    165192;;;               (x x? ...) ... xs xs? ...)
     
    172199;;; x ... are the fixed arguments, xs the optional variable arguments,
    173200;;; the following predicates naming the corresponding preconditions.
    174 (define-ir-macro (xlambda form inject compare?)
     201(define-ir-macro (xlambda% form inject compare?)
     202;(define-ir-macro (xlambda form inject compare?)
    175203  (let ((multi? (integer? (cadr form))))
    176204    (let ((k (if multi? (cadr form) 1))
     
    202230                         '()
    203231                         (car xrest)))
    204                 (loc (inject 'xlambda)))
     232                (loc (inject 'xlambda%)))
     233                ;(loc (inject 'xlambda)))
    205234            (let* (
    206235              ;; no checks
     
    303332                 ))))))))
    304333
    305 ;;; (xdefine ((r1 r1? ...) ... (rk rk? ...)
    306 ;;;           name
    307 ;;;           (x x? ...) ... xs xs? ...)
    308 ;;;            xpr . xprs)
    309 ;;; ----------------------------------------------
     334;;; new version:
     335;;; (xlambda ((r r? ...) .. <- (x x? ...) ...) xpr ....)
     336;;; or
     337;;; (xlambda ((r r? ...) .. <- (x x? ...) ... xs xs? ...) xpr ....)
     338;;; or old versions (deprecated):
     339;;; (xlambda k ((r1 r1? ...) ...(rk rk? ...)
     340;;;             (x x? ...) ... ) xpr ....)
     341;;; (xlambda k ((r1 r1? ...) ... (rk rk? ...)
     342;;;             (x x? ...) ... xs xs? ...) xpr ....)
     343;;; (xlambda ((r r? ...) (x x? ...) ... ) xpr ....)
     344;;; (xlambda ((r r? ...) (x x? ...) ... xs xs? ...) xpr ....)
     345;;; --------------------------------------------------------
     346(define-er-macro (xlambda form rename compare?)
     347  (let* ((k (cadr form)) (iform (if (integer? k)
     348                                  (cddr form)
     349                                  (cdr form))))
     350    (let ((header (car iform)) (body (cdr iform))
     351          (%xlambda% (rename 'xlambda%)) (%<- (rename '<-)))
     352      (if (integer? k)
     353        `(,%xlambda% ,k ,header ,@body)
     354        (receive (results args)
     355          (let loop ((header header) (results '()))
     356            (cond
     357              ((null? header) ; no <- symbol
     358               (let ((header (reverse results)))
     359                 (values (list (car header)) (cdr header))))
     360              ((compare? (car header) %<-)
     361               (values (reverse results) (cdr header)))
     362              (else
     363                (loop (cdr header) (cons (car header) results)))))
     364          `(,%xlambda% ,(length results) (,@results ,@args) ,@body))))))
     365
     366;;; (xdefine ((r r? ...) .. name (x x? ...) ...) xpr ....)
     367;;; or
     368;;; (xdefine ((r r? ...) .. #(post name pre) (x x? ...) ...) xpr ....)
     369;;; or
     370;;; (xdefine ((r r? ...) .. name (x x? ...) ... xs xs? ...) xpr ....)
     371;;; or
     372;;; (xdefine ((r r? ...) .. #(post name pre) (x x? ...) ... xs xs? ...) xpr ....)
     373;;; -----------------------------------------------------------------------------
     374;;; defines name -- and possibly post- and precondition documentation -- as a
     375;;; contract-checked procedure with postconditions named r checked by
     376;;; predicates r? ... and preconditions x ... xs .. checked by x? ...
     377;;; and xs? ...
    310378(define-er-macro (xdefine form rename compare?)
    311379  (let ((header (cadr form))
    312380        (xpr (caddr form))
    313381        (xprs (cdddr form))
     382        (%<- (rename '<-))
    314383        (%define (rename 'define))
    315         (%xlambda (rename 'xlambda)))
    316     (receive (k main returns)
    317       (let loop ((n 0) (tail header) (head '()))
    318         (if (symbol? (car tail))
    319           (values n tail (reverse head))
    320           (loop (+ n 1) (cdr tail) (cons (car tail) head))))
    321       `(,%define ,(car main)
    322                  (,%xlambda ,k ,(append returns (cdr main)) ,xpr ,@xprs)))))
     384        (%xlambda (rename 'xlambda))
     385        (%define-values (rename 'define-values)))
     386    (receive (posts names pres)
     387      (let loop ((tail header) (head '()))
     388        (if (or (symbol? (car tail)) (vector? (car tail)))
     389          (values (reverse head) (car tail) (cdr tail))
     390          (loop (cdr tail) (cons (car tail) head))))
     391      (if (symbol? names)
     392        `(,%define ,names
     393                   (,%xlambda (,@posts ,%<- ,@pres) ,xpr ,@xprs))
     394        `(,%define-values ,(list (vector-ref names 1) ; name
     395                                 (vector-ref names 2) ; pres
     396                                 (vector-ref names 0)); posts
     397                   (,%xlambda (,@posts ,%<- ,@pres) ,xpr ,@xprs))
     398        ))))
    323399
    324400;;; (simple-contracts sym ..)
     
    339415    (xdefine
    340416      macro:
    341       (xdefine ((r r? ...) ... name (a a? ...) ... [as as? ...]) . body)
     417      (xdefine ((r r? ...) .. name (a a? ...) ...) xpr ....)
     418      (xdefine ((r r? ...) .. #(post name pre) (a a? ...) ...) xpr ....)
     419      (xdefine ((r r? ...) .. name (a a? ...) ... as as? ...) xpr ....)
     420      (xdefine ((r r? ...) .. #(post name pre) (a a? ...) ... as as? ...) xpr ....)
    342421      "contract guarded version of define for procedures, where"
    343       "name is the name of the procedure"
     422      "name is the name of the procedure, post and pre"
     423      "the documentations of the pre- and postconditions respectively"
    344424      "r ... are return values with corresponding postcondition r?"
    345425      "a ... are fixed arguments with preconditions a? ..."
    346       "as is an optional variable argument with preconditions as? ...")
     426      "as is an optional variable argument with preconditions as? ..."
     427      "xpr starts the body")
    347428    (xlambda
    348429      macro:
    349       (xlambda k ((r r? ...) ... (a a? ...) ... [as as? ...]) . body)
     430      (xlambda ((r r? ...) .. <- (a a? ...) ...) xpr ...)
     431      (xlambda ((r r? ...) .. <- (a a? ...) ... as as? ...) xpr ...)
    350432      "contract guarded version of lambda, where"
    351       "k is the number of returned values r ..."
    352       "r? ... their corresponding postconditions"
     433      "<- separates returned values r .. from arguments"
     434      "r? ... are their corresponding postconditions"
    353435      "a ... are fixed arguments with preconditions a? ..."
    354436      "as is an optional variable argument with preconditions as? ..."
    355       "procedures with state change should return old versions"
     437      "xpr starts the body"
     438      "procedures with state change should return new and old versions"
    356439      "of state variables before the state change")
    357440    (%%
     
    362445      macro:
    363446      (pipe combination ...)
    364       "sequencing curried combinations")
     447      "sequencing curried combinations from left to right")
    365448    )))
    366449    (case-lambda
  • release/4/simple-contracts/trunk/simple-contracts.setup

    r33861 r34637  
    77 'simple-contracts
    88 '("simple-contracts.so" "simple-contracts.import.so")
    9  '((version "1.3.1")))
     9 '((version "1.4")))
  • release/4/simple-contracts/trunk/tests/run.scm

    r33853 r34637  
    1 (use simple-tests simple-contracts)
     1(use simple-tests simple-exceptions simple-contracts)
    22(contract-check-level 1)
    33
     
    3030(define-test (contracts?)
    3131  (check
    32     "STATE"
     32    "COMMANDS"
    3333    (define-values (counter! counter)
    3434      (let ((state 0))
    3535        (values
    36           (xlambda 1 ((old (pipe (+ 1) (= state))))
    37             (let ((o state))
     36          (xlambda ((new (pipe (= (add1 old))))
     37                         ;integer? (pipe (= (add1 old))))
     38                         ;integer? (lambda (x) (= x (add1 old))))
     39                    (old integer?)
     40                    <-)
     41            (let ((old state))
    3842              (set! state (add1 state))
    39               o))
    40           (xlambda 1 ((result (pipe (= state))))
     43              (values state old)))
     44          (xlambda ((result (pipe (= state))) <-)
    4145            state))))
    4246    (zero? (counter))
     
    4650    (= (counter) 2)
    4751 
     52    (define-values (push pop top)
     53      (let ((stk '()))
     54        (let (
     55          (push
     56            (xlambda ((new list? (pipe (equal? (cons arg old))))
     57                      (old list?)
     58                      <-
     59                      (arg))
     60              (let ((old stk))
     61                (set! stk (cons arg stk))
     62                (values stk old))))
     63          (pop
     64            (xlambda ((new list? (pipe (equal? (cdr old))))
     65                      (old list?)
     66                      <-)
     67              (let ((old (<< stk 'pop (pipe (null?) (not)))))
     68                (set! stk (cdr stk))
     69                (values stk old))))
     70          (top
     71            (xlambda ((result) <-)
     72              (car (<< stk 'top (pipe (null?) (not))))))
     73          )
     74          (values push pop top)
     75          )))
     76    ;(top) ; precondition violated
     77    ;(pop) ; precondition violated
     78    (push 0)
     79    (push 1)
     80    (= 1 (top))
     81    (equal? (call-with-values (lambda () (push 2)) list)
     82            '((2 1 0) (1 0)))
     83    (= 2 (top))
     84    (equal? (call-with-values (lambda () (pop)) list)
     85            '((1 0) (2 1 0)))
     86
     87    "QUERIES"
    4888    (define-values (add add-pre add-post)
    49       ;(xlambda 1 ((result integer? odd? (pipe (= (apply + x y ys))))
    5089      (xlambda ((result integer? odd? (pipe (= (apply + x y ys))))
     90                <-
    5191                (x integer? odd?) (y integer? even?) ys integer? even?)
    5292        (apply + x y ys)))
     
    61101
    62102    (define wrong-add
    63       ;(xlambda 1 ((result integer? even?)
    64103      (xlambda ((result integer? even?)
     104                <-
    65105                (x integer? odd?) xs integer?  even?)
    66106        (apply + x xs)))
     
    68108 
    69109    (define-values (divide divide-pre divide-post)
    70       (xlambda 2 ((q integer?)
    71                   (r (pipe (+ (* n q))
    72                            (= m)))
    73                   (m integer? (pipe (>= 0)))
    74                   (n integer? positive?))
     110      (xlambda ((q integer?)
     111                (r (pipe (+ (* n q))
     112                         (= m)))
     113                <-
     114                (m integer? (pipe (>= 0)))
     115                (n integer? positive?))
    75116        (let loop ((q 0) (r m))
    76117          (if (< r n)
     
    90131 
    91132    "XDEFINE"
    92     (xdefine ((result integer?) sum (a integer?) as integer?)
     133    ;(xdefine ((result integer?) sum (a integer?) as integer?)
     134    (xdefine ((result integer?) #(sum-post sum sum-pre) (a integer?) as integer?)
    93135      (apply + a as))
     136    ;(print sum-post)
     137    ;(print sum-pre)
    94138    (= (sum 1 2 3) 6)
    95139    (not (condition-case (sum 1 2 #f) ((exn argument) #f)))
Note: See TracChangeset for help on using the changeset viewer.