;
; std.scm - standard environment of known-total procedures.
; Total Procedures in Scheme, May 2006, Chris Pressey
; For license information, see the file LICENSE in this directory.
;
;
; These are mostly Scheme builtins.
;
; We make some assumptions about this list. The basic assumption
; is that all of these builtins are implemented correctly and are
; thus guaranteed to return. Another assumption is that those
; builtins that operate on lists (for example, 'length', 'memv',
; 'list->vector', etc) always return, even when given a cyclic list
; (even though R5RS does not specify this behaviour.) Should this
; assumption fail for some given implementation of some of these
; builtins, those builtins should be removed from this list, and
; if those builtins are used in the totality checker itself
; (notably 'reverse' is used in several places,) "hand-rolled"
; versions that are guaranteed to terminate should be substituted.
;
; Note that this file should NOT be reloaded during bootstrapping.
;
; It might be nice if these were local to define-total, but
; it's more useful for testing purposes if we can access them
; from outside there too.
;
(define orig-known-total-env
(map (lambda (name) (cons name 'total-proc)) '(
eqv? eq? equal?
number? complex? real? rational? integer?
exact? inexact?
= < > <= >=
zero? positive? negative? odd? even? max min
+ * - /
abs quotient remainder modulo
gcd lcm
numerator denominator
floor ceiling truncate round
rationalize
exp log sin cos tan asin acos atan
sqrt expt
make-rectangular make-polar real-part imag-part magnitude angle
exact->inexact inexact->exact
number->string string->number
not boolean? and or
pair? cons car cdr
;set-car! set-cdr! ; no side effects
caar cadr cdar cddr
caaar caadr cadar caddr cdaar cdadr cddar cdddr
caaaar caaadr caadar caaddr cadaar cadadr caddar cadddr
cdaaar cdaadr cdadar cdaddr cddaar cddadr cdddar cddddr
null? list?
list length append reverse ; NOTE: can depend on implementation
list-tail list-ref ; NOTE: can depend on implementation
memq memv member ; NOTE: can depend on implementation
assq assv assoc ; NOTE: can depend on implementation
symbol? symbol->string string->symbol
char?
char=? char<? char>? char<=? char>=?
char-ci=? char-ci<? char-ci>? char-ci<=? char-ci>=?
char-alphabetic? char-numeric? char-whitespace?
char-upper-case? char-lower-case?
char->integer integer->char
char-upcase char-downcase
string? make-string string string-length string-ref
;string-set! ; no side effects
string=? string-ci=?
string<? string>? string<=? string>=?
string-ci<? string-ci>? string-ci<=? string-ci>=?
substring string-append
string->list list->string
string-copy
;string-fill! ; no side effects
vector? make-vector vector vector-length vector-ref
;vector-set! ; no side effects
vector->list list->vector
;vector-fill! ; no side effects
procedure?
;apply ; The following builtins call for
;map for-each ; more complex flow analysis than
;force ; our analyzer does at present.
;call-with-current-continuation values call-with-values dynamic-wind
;eval scheme-report-environment null-environment interaction-environment
;call-with-input-file call-with-output-file
input-port? output-port?
current-input-port current-output-port
;with-input-from-file with-output-to-file
;open-input-file open-output-file
;close-input-port close-output-port
read read-char peek-char
eof-object? char-ready?
write display newline write-char
;load transcript-on transcript-off
acyclic? ; part of the analyzer
)))
;
; This variable changes over time, as define-total and definerec-total
; 'learn' about new user-defined procedures which are also total.
;
(define known-total-env orig-known-total-env)