(index ("make-ral" 0) ("ral->list" 259) ("ral->list" 259) ("ral-add!" 583) ("ral-add-left!" 907) ("ral-clear!" 1241) ("ral-count" 1464) ("ral-cursor-jump" 1628) ("ral-cursor-next" 1917) ("ral-eq?" 2163) ("ral-eql?" 2325) ("ral-equal?" 2550) ("ral-eqv?" 2718) ("ral-filter" 2882) ("ral-for-each" 3127) ("ral-from-upto" 3325) ("ral-height" 3668) ("ral-insert!" 3833) ("ral-item?" 4259) ("ral-join" 4404) ("ral-level" 4729) ("ral-map" 4936) ("ral-map" 4936) ("ral-max-height" 5344) ("ral-node?" 5517) ("ral-null?" 5654) ("ral-place" 5797) ("ral-place-next" 6075) ("ral-print" 6363) ("ral-ref" 6510) ("ral-remove!" 6740) ("ral-restructure" 6960) ("ral-restructure" 6960) ("ral-set!" 7486) ("ral-split" 7800) ("ral-start" 8152) ("ral-width" 8296) ("ral?" 8459))
(def (sig (procedure "(make-ral item? . args)" (id make-ral))) (highlight scheme "function (result)\nrequires (and ((list-of? (lambda (arg) (and (fixnum? arg) (fx> arg 1)))) args)\n              (procedure? item?) \"(item? item)\")\nensures  (ral? result)"))
(def (sig (procedure "(ral->list ls)" (id ral->list)) (procedure "(ral->list ls level)" (id ral->list))) (highlight scheme "function (result)\nrequires (and (ral? ls) (fixnum? level)\n              (fx<= 0 level) (fx< level (ral-height ls)))\n         ; default (fx= level 0)\nensures  ((list-of? (ral-item? ls)) result)"))
(def (sig (procedure "(ral-add! ls item . items)" (id ral-add!))) (highlight scheme "command ((oldcount newcount (lambda (ls item . items) (ral-count ls))))\nrequires (and (ral? ls) ((ral-item? ls) item)\n              ((list-of? (ral-item? ls)) items))\nensures  (fx= newcount (fx+ (length (cons item items)) oldcount))"))
(def (sig (procedure "(ral-add-left! ls item . items)" (id ral-add-left!))) (highlight scheme "command ((oldcount newcount (lambda (ls item . items) (ral-count ls))))\nrequires (and (ral? ls) ((ral-item? ls) item)\n              ((list-of? (ral-item? ls)) items))\nensures  (fx= newcount (fx+ (length (cons item items)) oldcount))"))
(def (sig (procedure "(ral-clear! ls)" (id ral-clear!))) (highlight scheme "command ((oldcount newcount ral-count) (oldheight newheight ral-height))\nrequires (ral? ls)\nensures  (and (fx= 0 newcount) (fx= 1 newheight))"))
(def (sig (procedure "(ral-count ls)" (id ral-count))) (highlight scheme "function (result)\nrequires (ral? ls)\nensures  (and (fixnum? result) (fx>= result 0))"))
(def (sig (procedure "(ral-cursor-jump ls k)" (id ral-cursor-jump))) (highlight scheme "function (result)\nrequires (and (ral? ls) (fixnum? k)\n              (fx>= k 0) (fx< k (ral-height ls)))\nensures  (and (fixnum? result)\n              (fx> result 0) (fx<= result (ral-count ls)))"))
(def (sig (procedure "(ral-cursor-next ls k)" (id ral-cursor-next))) (highlight scheme "function (result)\nrequires (and (ral? ls) (fixnum? k)\n              (fx>= k 0) (fx< k (ral-height ls)))\nensures  (or (null? result) (ral-node? result))"))
(def (sig (procedure "(ral-eq? ls0 ls1)" (id ral-eq?))) (highlight scheme "function (result)\nrequires (and (ral? ls0) (ral? ls1))\nensures  (boolean? result)"))
(def (sig (procedure "(ral-eql? eql? ls0 ls1)" (id ral-eql?))) (highlight scheme "function (result)\nrequires (and (procedure? eql?) \"(eql? item0 item1)\"\n              (ral? ls0) (ral? ls1))\nensures  (boolean? result)"))
(def (sig (procedure "(ral-equal? ls0 ls1)" (id ral-equal?))) (highlight scheme "function (result)\nrequires (and (ral? ls0) (ral? ls1))\nensures  (boolean? result)"))
(def (sig (procedure "(ral-eqv? ls0 ls1)" (id ral-eqv?))) (highlight scheme "function (result)\nrequires (and (ral? ls0) (ral? ls1))\nensures  (boolean? result)"))
(def (sig (procedure "(ral-filter ls ok?)" (id ral-filter))) (highlight scheme "function (result)\nrequires (and (ral? ls) (procedure? ok?) \"(ok? item)\")\nensures  (and (ral? result)\n              (fx<= (ral-count result) (ral-count ls)))"))
(def (sig (procedure "(ral-for-each ls proc)" (id ral-for-each))) (highlight scheme "command ((old new (constantly #t)))\nrequires (and (ral? ls) (procedure? proc) \"(proc item)\")\nensures  new"))
(def (sig (procedure "(ral-from-upto ls from upto)" (id ral-from-upto))) (highlight scheme "function (result)\nrequires (and (ral? ls) (fixnum? from) (fixnum? upto)\n              (fx>= from 0) (fx>= upto from)\n              (fx<= upto (ral-count ls)))\nensures  (and (ral? result)\n              (fx= (ral-count result) (fx- upto from)))"))
(def (sig (procedure "(ral-height ls)" (id ral-height))) (highlight scheme "function (result)\nrequires (ral? ls)\nensures  (and (fixnum? result) (fx> result 0))"))
(def (sig (procedure "(ral-insert! ls place item)" (id ral-insert!))) (highlight scheme "command ((oldcount newcount (lambda (ls place item) (ral-count ls)))\n         (olditem newitem (lambda (ls place item) (ral-ref ls place))))\nrequires (and (ral? ls) ((ral-item? ls) item)\n              (fixnum? place) (fx>= place 0) (fx<= place (ral-count ls)))\nensures  (and (fx= newcount (fx+ 1 oldcount)) (equal? newitem item))"))
(def (sig (procedure "(ral-item? ls)" (id ral-item?))) (highlight scheme "function (result)\nrequires (ral? ls)\nensures  (procedure? result)"))
(def (sig (procedure "(ral-join head tail)" (id ral-join))) (highlight scheme "function (result)\nrequires (and (ral? head) (ral? tail)\n              (eq? (ral-item? head) (ral-item? tail)))\nensures  (and (ral? result)\n              (fx= (ral-count result)\n                   (fx+ (ral-count head) (ral-count tail))))"))
(def (sig (procedure "(ral-level ls)" (id ral-level))) (highlight scheme "function (result)\nrequires (ral? ls)\nensures  (and (fixnum? result) (fx> result 0)\n              (fx< result (ral-height ls)))"))
(def (sig (procedure "(ral-map ls fn)" (id ral-map)) (procedure "(ral-map ls fn item?)" (id ral-map))) (highlight scheme "function (result)\nrequires (and (ral? ls) (procedure? fn) \"(fn item)\"\n              (procedure? item?) \"(item? item)\")\n         ; default (eq? item? ral-item?)\nensures  (and (ral? result) (fx= (ral-count result) (ral-count ls))\n              (eq? item? (ral-item? result)))"))
(def (sig (procedure "(ral-max-height ls)" (id ral-max-height))) (highlight scheme "function (result)\nrequires (ral? ls)\nensures  (and (fixnum? result) (fx> result 0))"))
(def (sig (procedure "(ral-node? xpr)" (id ral-node?))) (highlight scheme "function (result)\nrequires #t\nensures  (boolean? result)"))
(def (sig (procedure "(ral-null? ls)" (id ral-null?))) (highlight scheme "function (result)\nrequires (ral? ls)\nensures  (boolean? result)"))
(def (sig (procedure "(ral-place ls k)" (id ral-place))) (highlight scheme "function (result)\nrequires (and (ral? ls) (fixnum? k)\n              (fx>= k 0) (fx< k (ral-height ls)))\nensures  (and (fixnum? result) (fx>= result -1)\n              (fx< result (ral-count ls)))"))
(def (sig (procedure "(ral-place-next ls k)" (id ral-place-next))) (highlight scheme "function (result)\nrequires (and (ral? ls) (fixnum? k)\n              (fx>= k 0) (fx< k (ral-height ls)))\nensures  (and (fixnum? result) (fx>= result 0)\n              (fx<= result (ral-count ls)))"))
(def (sig (procedure "(ral-print ls)" (id ral-print))) (highlight scheme "command ((old new (constantly #t)))\nrequires (ral? ls)\nensures  new"))
(def (sig (procedure "(ral-ref ls place)" (id ral-ref))) (highlight scheme "function (result)\nrequires (and (ral? ls) (fixnum? place)\n              (fx>= place 0) (fx< place (ral-count ls)))\nensures  ((ral-item? ls) result)"))
(def (sig (procedure "(ral-remove! ls place)" (id ral-remove!))) (highlight scheme "command ((oldcount newcount (lambda (ls place) (ral-count ls))))\nrequires (ral? ls)\nensures  (and (fx= newcount (fx- oldcount 1)))"))
(def (sig (procedure "(ral-restructure ls width)" (id ral-restructure)) (procedure "(ral-restructure ls width max-height)" (id ral-restructure))) (highlight scheme "function (result)\nrequires (and (ral? ls) (fixnum? width)\n              (fx> width 1) (fixnum? max-height) (fx> max-height 1))\n         ; default (fx= max-height (ral-max-height ls))\nensures  (and (ral? result) (fx= (ral-count ls) (ral-count result))\n              (fx= (ral-width result) width)\n              (fx= (ral-max-height result) max-height))"))
(def (sig (procedure "(ral-set! ls place item)" (id ral-set!))) (highlight scheme "command ((old new (lambda (ls place item) (ral-ref ls place))))\nrequires (and (ral? ls) ((ral-item? ls) item)\n              (fixnum? place) (fx>= place 0)\n              (fx< place (ral-count ls)))\nensures  (equal? new item)"))
(def (sig (procedure "(ral-split ls place)" (id ral-split))) (highlight scheme "function (head tail)\nrequires (and (ral? ls) (fixnum? place)\n              (fx>= place 0) (fx< place (ral-count ls)))\nensures  (and (ral? head) (ral? tail)\n              (fx= (ral-count head) place)\n              (fx= (ral-count tail) (fx- (ral-count ls) place)))"))
(def (sig (procedure "(ral-start ls)" (id ral-start))) (highlight scheme "function (result)\nrequires (ral? ls)\nensures  (ral-node? result)"))
(def (sig (procedure "(ral-width ls)" (id ral-width))) (highlight scheme "function (result)\nrequires (ral? ls)\nensures  (and (fixnum? result) (fx> result 1))"))
(def (sig (procedure "(ral? xpr)" (id ral?))) (highlight scheme "function (result)\nrequires #t\nensures  (boolean? result)"))
