Import GC benchmarks from Larceny, by Hansen, Clinger, et al.
[bpt/guile.git] / gc-benchmarks / larceny / dynamic.sch
diff --git a/gc-benchmarks/larceny/dynamic.sch b/gc-benchmarks/larceny/dynamic.sch
new file mode 100644 (file)
index 0000000..779ad76
--- /dev/null
@@ -0,0 +1,2348 @@
+; This benchmark was obtained from Andrew Wright,
+; based on Fritz Henglein's code.
+; 970215 / wdc Removed most i/o and added dynamic-benchmark.
+; 990707 / lth Added a quote and changed the call to run-benchmark.
+; 010404 / wdc Changed the input file path name to "dynamic-input.sch".
+
+;; Fritz's dynamic type inferencer, set up to run on itself
+;; (see the end of this file).
+
+;----------------------------------------------------------------------------
+; Environment management
+;----------------------------------------------------------------------------
+
+;; environments are lists of pairs, the first component being the key
+
+;; general environment operations
+;;
+;; empty-env: Env
+;; gen-binding: Key x Value -> Binding
+;; binding-key: Binding -> Key
+;; binding-value: Binding -> Value
+;; binding-show: Binding -> Symbol*
+;; extend-env-with-binding: Env x Binding -> Env
+;; extend-env-with-env: Env x Env -> Env
+;; lookup: Key x Env -> (Binding + False)
+;; env->list: Env -> Binding*
+;; env-show: Env -> Symbol*
+
+
+; bindings
+
+(define gen-binding cons)
+; generates a type binding, binding a symbol to a type variable
+
+(define binding-key car)
+; returns the key of a type binding
+
+(define binding-value cdr)
+; returns the tvariable of a type binding
+
+(define (key-show key)
+  ; default show procedure for keys
+  key)
+
+(define (value-show value)
+  ; default show procedure for values
+  value)
+
+(define (binding-show binding)
+  ; returns a printable representation of a type binding
+  (cons (key-show (binding-key binding))
+       (cons ': (value-show (binding-value binding)))))
+
+
+; environments
+
+(define dynamic-empty-env '())
+; returns the empty environment
+
+(define (extend-env-with-binding env binding)
+  ; extends env with a binding, which hides any other binding in env
+  ; for the same key (see dynamic-lookup)
+  ; returns the extended environment
+  (cons binding env))
+
+(define (extend-env-with-env env ext-env)
+  ; extends environment env with environment ext-env 
+  ; a binding for a key in ext-env hides any binding in env for
+  ; the same key (see dynamic-lookup)
+  ; returns the extended environment
+  (append ext-env env))
+
+(define dynamic-lookup (lambda (x l) (assv x l)))
+; returns the first pair in env that matches the key; returns #f
+; if no such pair exists
+
+(define (env->list e)
+  ; converts an environment to a list of bindings
+  e)
+
+(define (env-show env)
+  ; returns a printable list representation of a type environment
+  (map binding-show env))
+;----------------------------------------------------------------------------
+;      Parsing for Scheme
+;----------------------------------------------------------------------------
+
+
+;; Needed packages: environment management
+
+;(load "env-mgmt.ss")
+;(load "pars-act.ss")
+
+;; Lexical notions
+
+(define syntactic-keywords
+  ;; source: IEEE Scheme, 7.1, <expression keyword>, <syntactic keyword>
+  '(lambda if set! begin cond and or case let let* letrec do
+         quasiquote else => define unquote unquote-splicing))
+
+
+;; Parse routines
+
+; Datum
+
+; dynamic-parse-datum: parses nonterminal <datum>
+
+(define (dynamic-parse-datum e)
+  ;; Source: IEEE Scheme, sect. 7.2, <datum>
+  ;; Note: "'" is parsed as 'quote, "`" as 'quasiquote, "," as
+  ;; 'unquote, ",@" as 'unquote-splicing (see sect. 4.2.5, p. 18)
+  ;; ***Note***: quasi-quotations are not permitted! (It would be
+  ;; necessary to pass the environment to dynamic-parse-datum.)
+  (cond
+   ((null? e)
+    (dynamic-parse-action-null-const))
+   ((boolean? e)
+    (dynamic-parse-action-boolean-const e))
+   ((char? e)
+    (dynamic-parse-action-char-const e))
+   ((number? e)
+    (dynamic-parse-action-number-const e))
+   ((string? e)
+    (dynamic-parse-action-string-const e))
+   ((symbol? e)
+    (dynamic-parse-action-symbol-const e))
+   ((vector? e)
+    (dynamic-parse-action-vector-const (map dynamic-parse-datum (vector->list e))))
+   ((pair? e)
+    (dynamic-parse-action-pair-const (dynamic-parse-datum (car e))
+                            (dynamic-parse-datum (cdr e))))
+   (else (error 'dynamic-parse-datum "Unknown datum: ~s" e))))
+
+
+; VarDef
+
+; dynamic-parse-formal: parses nonterminal <variable> in defining occurrence position
+
+(define (dynamic-parse-formal f-env e)
+  ; e is an arbitrary object, f-env is a forbidden environment;
+  ; returns: a variable definition (a binding for the symbol), plus
+  ; the value of the binding as a result
+  (if (symbol? e)
+      (cond
+       ((memq e syntactic-keywords)
+       (error 'dynamic-parse-formal "Illegal identifier (keyword): ~s" e))
+       ((dynamic-lookup e f-env)
+       (error 'dynamic-parse-formal "Duplicate variable definition: ~s" e))
+       (else (let ((dynamic-parse-action-result (dynamic-parse-action-var-def e)))
+              (cons (gen-binding e dynamic-parse-action-result)
+                    dynamic-parse-action-result))))
+      (error 'dynamic-parse-formal "Not an identifier: ~s" e)))
+
+; dynamic-parse-formal*
+
+(define (dynamic-parse-formal* formals)
+  ;; parses a list of formals and returns a pair consisting of generated
+  ;; environment and list of parsing action results
+  (letrec
+      ((pf*
+       (lambda (f-env results formals)
+         ;; f-env: "forbidden" environment (to avoid duplicate defs)
+         ;; results: the results of the parsing actions
+         ;; formals: the unprocessed formals
+         ;; Note: generates the results of formals in reverse order!
+         (cond
+          ((null? formals)
+           (cons f-env results))
+          ((pair? formals)
+           (let* ((fst-formal (car formals))
+                  (binding-result (dynamic-parse-formal f-env fst-formal))
+                  (binding (car binding-result))
+                  (var-result (cdr binding-result)))
+             (pf*
+              (extend-env-with-binding f-env binding)
+              (cons var-result results)
+              (cdr formals))))
+          (else (error 'dynamic-parse-formal* "Illegal formals: ~s" formals))))))
+    (let ((renv-rres (pf* dynamic-empty-env '() formals)))
+      (cons (car renv-rres) (reverse (cdr renv-rres))))))
+
+
+; dynamic-parse-formals: parses <formals>
+
+(define (dynamic-parse-formals formals)
+  ;; parses <formals>; see IEEE Scheme, sect. 7.3
+  ;; returns a pair: env and result
+  (letrec ((pfs (lambda (f-env formals)
+                 (cond
+                  ((null? formals)
+                   (cons dynamic-empty-env (dynamic-parse-action-null-formal)))
+                  ((pair? formals)
+                   (let* ((fst-formal (car formals))
+                          (rem-formals (cdr formals))
+                          (bind-res (dynamic-parse-formal f-env fst-formal))
+                          (bind (car bind-res))
+                          (res (cdr bind-res))
+                          (nf-env (extend-env-with-binding f-env bind))
+                          (renv-res* (pfs nf-env rem-formals))
+                          (renv (car renv-res*))
+                          (res* (cdr renv-res*)))
+                     (cons
+                      (extend-env-with-binding renv bind)
+                      (dynamic-parse-action-pair-formal res res*))))
+                  (else
+                   (let* ((bind-res (dynamic-parse-formal f-env formals))
+                          (bind (car bind-res))
+                          (res (cdr bind-res)))
+                     (cons
+                      (extend-env-with-binding dynamic-empty-env bind)
+                      res)))))))
+    (pfs dynamic-empty-env formals)))
+
+
+; Expr
+
+; dynamic-parse-expression: parses nonterminal <expression>
+
+(define (dynamic-parse-expression env e)
+  (cond
+   ((symbol? e)
+    (dynamic-parse-variable env e))
+   ((pair? e)
+    (let ((op (car e)) (args (cdr e)))
+      (case op
+       ((quote) (dynamic-parse-quote env args))
+       ((lambda) (dynamic-parse-lambda env args))
+       ((if) (dynamic-parse-if env args))
+       ((set!) (dynamic-parse-set env args))
+       ((begin) (dynamic-parse-begin env args))
+       ((cond) (dynamic-parse-cond env args))
+       ((case) (dynamic-parse-case env args))
+       ((and) (dynamic-parse-and env args))
+       ((or) (dynamic-parse-or env args))
+       ((let) (dynamic-parse-let env args))
+       ((let*) (dynamic-parse-let* env args))
+       ((letrec) (dynamic-parse-letrec env args))
+       ((do) (dynamic-parse-do env args))
+       ((quasiquote) (dynamic-parse-quasiquote env args))
+        (else (dynamic-parse-procedure-call env op args)))))
+   (else (dynamic-parse-datum e))))
+
+; dynamic-parse-expression*
+
+(define (dynamic-parse-expression* env exprs)
+  ;; Parses lists of expressions (returns them in the right order!)
+  (letrec ((pe*
+           (lambda (results es)
+             (cond
+              ((null? es) results)
+              ((pair? es) (pe* (cons (dynamic-parse-expression env (car es)) results) (cdr es)))
+              (else (error 'dynamic-parse-expression* "Not a list of expressions: ~s" es))))))
+    (reverse (pe* '() exprs))))
+
+
+; dynamic-parse-expressions
+
+(define (dynamic-parse-expressions env exprs)
+  ;; parses lists of arguments of a procedure call
+  (cond
+   ((null? exprs) (dynamic-parse-action-null-arg))
+   ((pair? exprs) (let* ((fst-expr (car exprs))
+                        (rem-exprs (cdr exprs))
+                        (fst-res (dynamic-parse-expression env fst-expr))
+                        (rem-res (dynamic-parse-expressions env rem-exprs)))
+                   (dynamic-parse-action-pair-arg fst-res rem-res)))
+   (else (error 'dynamic-parse-expressions "Illegal expression list: ~s"
+               exprs))))
+
+
+; dynamic-parse-variable: parses variables (applied occurrences)
+
+(define (dynamic-parse-variable env e)
+  (if (symbol? e)
+      (if (memq e syntactic-keywords)
+         (error 'dynamic-parse-variable "Illegal identifier (keyword): ~s" e)
+         (let ((assoc-var-def (dynamic-lookup e env)))
+           (if assoc-var-def
+               (dynamic-parse-action-variable (binding-value assoc-var-def))
+               (dynamic-parse-action-identifier e))))
+      (error 'dynamic-parse-variable "Not an identifier: ~s" e)))
+
+
+; dynamic-parse-procedure-call
+
+(define (dynamic-parse-procedure-call env op args)
+  (dynamic-parse-action-procedure-call
+   (dynamic-parse-expression env op)
+   (dynamic-parse-expressions env args)))
+
+
+; dynamic-parse-quote
+
+(define (dynamic-parse-quote env args)
+  (if (list-of-1? args)
+      (dynamic-parse-datum (car args))
+      (error 'dynamic-parse-quote "Not a datum (multiple arguments): ~s" args)))
+
+
+; dynamic-parse-lambda
+
+(define (dynamic-parse-lambda env args)
+  (if (pair? args)
+      (let* ((formals (car args))
+            (body (cdr args))
+            (nenv-fresults (dynamic-parse-formals formals))
+            (nenv (car nenv-fresults))
+            (fresults (cdr nenv-fresults)))
+       (dynamic-parse-action-lambda-expression
+        fresults
+        (dynamic-parse-body (extend-env-with-env env nenv) body)))
+      (error 'dynamic-parse-lambda "Illegal formals/body: ~s" args)))
+
+
+; dynamic-parse-body
+
+(define (dynamic-parse-body env body)
+  ; <body> = <definition>* <expression>+
+  (define (def-var* f-env body)
+    ; finds the defined variables in a body and returns an 
+    ; environment containing them
+    (if (pair? body)
+        (let ((n-env (def-var f-env (car body))))
+          (if n-env
+              (def-var* n-env (cdr body))
+              f-env))
+        f-env))
+  (define (def-var f-env clause)
+    ; finds the defined variables in a single clause and extends
+    ; f-env accordingly; returns false if it's not a definition
+    (if (pair? clause)
+        (case (car clause)
+          ((define) (if (pair? (cdr clause))
+                        (let ((pattern (cadr clause)))
+                          (cond
+                          ((symbol? pattern)
+                           (extend-env-with-binding 
+                            f-env 
+                            (gen-binding pattern
+                                         (dynamic-parse-action-var-def pattern))))
+                          ((and (pair? pattern) (symbol? (car pattern)))
+                           (extend-env-with-binding
+                            f-env
+                            (gen-binding (car pattern)
+                                         (dynamic-parse-action-var-def 
+                                          (car pattern)))))
+                          (else f-env)))
+                        f-env))
+          ((begin) (def-var* f-env (cdr clause)))
+          (else #f))
+        #f))
+  (if (pair? body)
+      (dynamic-parse-command* (def-var* env body) body)
+      (error 'dynamic-parse-body "Illegal body: ~s" body)))
+
+; dynamic-parse-if
+
+(define (dynamic-parse-if env args)
+  (cond
+   ((list-of-3? args)
+    (dynamic-parse-action-conditional
+     (dynamic-parse-expression env (car args))
+     (dynamic-parse-expression env (cadr args))
+     (dynamic-parse-expression env (caddr args))))
+   ((list-of-2? args)
+    (dynamic-parse-action-conditional
+     (dynamic-parse-expression env (car args))
+     (dynamic-parse-expression env (cadr args))
+     (dynamic-parse-action-empty)))
+   (else (error 'dynamic-parse-if "Not an if-expression: ~s" args))))
+
+
+; dynamic-parse-set
+
+(define (dynamic-parse-set env args)
+  (if (list-of-2? args)
+      (dynamic-parse-action-assignment
+       (dynamic-parse-variable env (car args))
+       (dynamic-parse-expression env (cadr args)))
+      (error 'dynamic-parse-set "Not a variable/expression pair: ~s" args)))
+
+
+; dynamic-parse-begin
+
+(define (dynamic-parse-begin env args)
+  (dynamic-parse-action-begin-expression
+   (dynamic-parse-body env args)))
+
+
+; dynamic-parse-cond
+
+(define (dynamic-parse-cond env args)
+  (if (and (pair? args) (list? args))
+      (dynamic-parse-action-cond-expression
+       (map (lambda (e)
+             (dynamic-parse-cond-clause env e))
+           args))
+      (error 'dynamic-parse-cond "Not a list of cond-clauses: ~s" args)))
+
+; dynamic-parse-cond-clause
+
+(define (dynamic-parse-cond-clause env e)
+  ;; ***Note***: Only (<test> <sequence>) is permitted!
+  (if (pair? e)
+      (cons
+       (if (eqv? (car e) 'else)
+          (dynamic-parse-action-empty)
+          (dynamic-parse-expression env (car e)))
+       (dynamic-parse-body env (cdr e)))
+      (error 'dynamic-parse-cond-clause "Not a cond-clause: ~s" e)))
+
+
+; dynamic-parse-and
+
+(define (dynamic-parse-and env args)
+  (if (list? args)
+      (dynamic-parse-action-and-expression
+       (dynamic-parse-expression* env args))
+      (error 'dynamic-parse-and "Not a list of arguments: ~s" args)))
+
+
+; dynamic-parse-or
+
+(define (dynamic-parse-or env args)
+  (if (list? args)
+      (dynamic-parse-action-or-expression
+       (dynamic-parse-expression* env args))
+      (error 'dynamic-parse-or "Not a list of arguments: ~s" args)))
+
+
+; dynamic-parse-case
+
+(define (dynamic-parse-case env args)
+  (if (and (list? args) (> (length args) 1))
+      (dynamic-parse-action-case-expression
+       (dynamic-parse-expression env (car args))
+       (map (lambda (e)
+              (dynamic-parse-case-clause env e))
+            (cdr args)))
+      (error 'dynamic-parse-case "Not a list of clauses: ~s" args)))
+
+; dynamic-parse-case-clause
+
+(define (dynamic-parse-case-clause env e)
+  (if (pair? e)
+      (cons
+       (cond
+       ((eqv? (car e) 'else)
+        (list (dynamic-parse-action-empty)))
+       ((list? (car e))
+        (map dynamic-parse-datum (car e)))
+       (else (error 'dynamic-parse-case-clause "Not a datum list: ~s" (car e))))
+       (dynamic-parse-body env (cdr e)))
+      (error 'dynamic-parse-case-clause "Not case clause: ~s" e)))
+
+
+; dynamic-parse-let
+
+(define (dynamic-parse-let env args)
+  (if (pair? args)
+      (if (symbol? (car args))
+         (dynamic-parse-named-let env args)
+         (dynamic-parse-normal-let env args))
+      (error 'dynamic-parse-let "Illegal bindings/body: ~s" args)))
+
+
+; dynamic-parse-normal-let
+
+(define (dynamic-parse-normal-let env args)
+  ;; parses "normal" let-expressions
+  (let* ((bindings (car args))
+        (body (cdr args))
+        (env-ast (dynamic-parse-parallel-bindings env bindings))
+        (nenv (car env-ast))
+        (bresults (cdr env-ast)))
+    (dynamic-parse-action-let-expression
+     bresults
+     (dynamic-parse-body (extend-env-with-env env nenv) body))))
+
+; dynamic-parse-named-let
+
+(define (dynamic-parse-named-let env args)
+  ;; parses a named let-expression
+  (if (pair? (cdr args))
+      (let* ((variable (car args))
+            (bindings (cadr args))
+            (body (cddr args))
+            (vbind-vres (dynamic-parse-formal dynamic-empty-env variable))
+            (vbind (car vbind-vres))
+            (vres (cdr vbind-vres))
+            (env-ast (dynamic-parse-parallel-bindings env bindings))
+            (nenv (car env-ast))
+            (bresults (cdr env-ast)))
+       (dynamic-parse-action-named-let-expression
+        vres bresults
+        (dynamic-parse-body (extend-env-with-env 
+                     (extend-env-with-binding env vbind)
+                     nenv) body)))
+      (error 'dynamic-parse-named-let "Illegal named let-expression: ~s" args)))
+
+
+; dynamic-parse-parallel-bindings
+
+(define (dynamic-parse-parallel-bindings env bindings)
+  ; returns a pair consisting of an environment
+  ; and a list of pairs (variable . asg)
+  ; ***Note***: the list of pairs is returned in reverse unzipped form!
+  (if (list-of-list-of-2s? bindings)
+      (let* ((env-formals-asg
+            (dynamic-parse-formal* (map car bindings)))
+           (nenv (car env-formals-asg))
+           (bresults (cdr env-formals-asg))
+           (exprs-asg
+            (dynamic-parse-expression* env (map cadr bindings))))
+       (cons nenv (cons bresults exprs-asg)))
+      (error 'dynamic-parse-parallel-bindings
+            "Not a list of bindings: ~s" bindings)))
+
+
+; dynamic-parse-let*
+
+(define (dynamic-parse-let* env args)
+  (if (pair? args)
+      (let* ((bindings (car args))
+            (body (cdr args))
+            (env-ast (dynamic-parse-sequential-bindings env bindings))
+            (nenv (car env-ast))
+            (bresults (cdr env-ast)))
+       (dynamic-parse-action-let*-expression
+        bresults
+        (dynamic-parse-body (extend-env-with-env env nenv) body)))
+      (error 'dynamic-parse-let* "Illegal bindings/body: ~s" args)))
+
+; dynamic-parse-sequential-bindings
+
+(define (dynamic-parse-sequential-bindings env bindings)
+  ; returns a pair consisting of an environment
+  ; and a list of pairs (variable . asg)
+  ;; ***Note***: the list of pairs is returned in reverse unzipped form!
+  (letrec
+      ((psb
+       (lambda (f-env c-env var-defs expr-asgs binds)
+         ;; f-env: forbidden environment
+         ;; c-env: constructed environment
+         ;; var-defs: results of formals
+         ;; expr-asgs: results of corresponding expressions
+         ;; binds: reminding bindings to process
+         (cond
+          ((null? binds)
+           (cons f-env (cons var-defs expr-asgs)))
+          ((pair? binds)
+           (let ((fst-bind (car binds)))
+             (if (list-of-2? fst-bind)
+                 (let* ((fbinding-bres
+                         (dynamic-parse-formal f-env (car fst-bind)))
+                        (fbind (car fbinding-bres))
+                        (bres (cdr fbinding-bres))
+                        (new-expr-asg
+                         (dynamic-parse-expression c-env (cadr fst-bind))))
+                   (psb
+                    (extend-env-with-binding f-env fbind)
+                    (extend-env-with-binding c-env fbind)
+                    (cons bres var-defs)
+                    (cons new-expr-asg expr-asgs)
+                    (cdr binds)))
+                 (error 'dynamic-parse-sequential-bindings
+                        "Illegal binding: ~s" fst-bind))))
+          (else (error 'dynamic-parse-sequential-bindings
+                       "Illegal bindings: ~s" binds))))))
+    (let ((env-vdefs-easgs (psb dynamic-empty-env env '() '() bindings)))
+      (cons (car env-vdefs-easgs)
+           (cons (reverse (cadr env-vdefs-easgs))
+                 (reverse (cddr env-vdefs-easgs)))))))
+
+
+; dynamic-parse-letrec
+
+(define (dynamic-parse-letrec env args)
+  (if (pair? args)
+      (let* ((bindings (car args))
+            (body (cdr args))
+            (env-ast (dynamic-parse-recursive-bindings env bindings))
+            (nenv (car env-ast))
+            (bresults (cdr env-ast)))
+       (dynamic-parse-action-letrec-expression
+         bresults
+         (dynamic-parse-body (extend-env-with-env env nenv) body)))
+      (error 'dynamic-parse-letrec "Illegal bindings/body: ~s" args)))
+
+; dynamic-parse-recursive-bindings
+
+(define (dynamic-parse-recursive-bindings env bindings)
+  ;; ***Note***: the list of pairs is returned in reverse unzipped form!
+  (if (list-of-list-of-2s? bindings)
+      (let* ((env-formals-asg
+             (dynamic-parse-formal* (map car bindings)))
+            (formals-env
+             (car env-formals-asg))
+            (formals-res
+             (cdr env-formals-asg))
+            (exprs-asg
+             (dynamic-parse-expression*
+              (extend-env-with-env env formals-env)
+              (map cadr bindings))))
+       (cons
+        formals-env
+        (cons formals-res exprs-asg)))
+      (error 'dynamic-parse-recursive-bindings "Illegal bindings: ~s" bindings)))
+
+
+; dynamic-parse-do
+
+(define (dynamic-parse-do env args)
+  ;; parses do-expressions
+  ;; ***Note***: Not implemented!
+  (error 'dynamic-parse-do "Nothing yet..."))
+
+; dynamic-parse-quasiquote
+
+(define (dynamic-parse-quasiquote env args)
+  ;; ***Note***: Not implemented!
+  (error 'dynamic-parse-quasiquote "Nothing yet..."))
+
+
+;; Command
+
+; dynamic-parse-command
+
+(define (dynamic-parse-command env c)
+  (if (pair? c)
+      (let ((op (car c))
+           (args (cdr c)))
+       (case op
+        ((define) (dynamic-parse-define env args))
+;       ((begin) (dynamic-parse-command* env args))  ;; AKW
+        ((begin) (dynamic-parse-action-begin-expression (dynamic-parse-command* env args)))
+        (else (dynamic-parse-expression env c))))
+      (dynamic-parse-expression env c)))
+
+
+; dynamic-parse-command*
+
+(define (dynamic-parse-command* env commands)
+  ;; parses a sequence of commands
+  (if (list? commands)
+      (map (lambda (command) (dynamic-parse-command env command)) commands)
+      (error 'dynamic-parse-command* "Invalid sequence of commands: ~s" commands)))
+
+
+; dynamic-parse-define
+
+(define (dynamic-parse-define env args)
+  ;; three cases -- see IEEE Scheme, sect. 5.2
+  ;; ***Note***: the parser admits forms (define (x . y) ...)
+  ;; ***Note***: Variables are treated as applied occurrences!
+  (if (pair? args)
+      (let ((pattern (car args))
+           (exp-or-body (cdr args)))
+       (cond
+        ((symbol? pattern)
+         (if (list-of-1? exp-or-body)
+             (dynamic-parse-action-definition
+              (dynamic-parse-variable env pattern)
+              (dynamic-parse-expression env (car exp-or-body)))
+             (error 'dynamic-parse-define "Not a single expression: ~s" exp-or-body)))
+        ((pair? pattern)
+         (let* ((function-name (car pattern))
+                (function-arg-names (cdr pattern))
+                (env-ast (dynamic-parse-formals function-arg-names))
+                (formals-env (car env-ast))
+                (formals-ast (cdr env-ast)))
+           (dynamic-parse-action-function-definition
+            (dynamic-parse-variable env function-name)
+            formals-ast
+            (dynamic-parse-body (extend-env-with-env env formals-env) exp-or-body))))
+        (else (error 'dynamic-parse-define "Not a valid pattern: ~s" pattern))))
+      (error 'dynamic-parse-define "Not a valid definition: ~s" args)))
+
+;; Auxiliary routines
+
+; forall?
+
+(define (forall? pred list)
+  (if (null? list)
+      #t
+      (and (pred (car list)) (forall? pred (cdr list)))))
+
+; list-of-1?
+
+(define (list-of-1? l)
+  (and (pair? l) (null? (cdr l))))
+
+; list-of-2?
+
+(define (list-of-2? l)
+  (and (pair? l) (pair? (cdr l)) (null? (cddr l))))
+
+; list-of-3?
+
+(define (list-of-3? l)
+  (and (pair? l) (pair? (cdr l)) (pair? (cddr l)) (null? (cdddr l))))
+
+; list-of-list-of-2s?
+
+(define (list-of-list-of-2s? e)
+  (cond
+   ((null? e)
+    #t)
+   ((pair? e)
+    (and (list-of-2? (car e)) (list-of-list-of-2s? (cdr e))))
+   (else #f)))
+
+
+;; File processing
+
+; dynamic-parse-from-port
+
+(define (dynamic-parse-from-port port)
+  (let ((next-input (read port)))
+    (if (eof-object? next-input)
+       '()
+       (dynamic-parse-action-commands
+        (dynamic-parse-command dynamic-empty-env next-input)
+        (dynamic-parse-from-port port)))))
+
+; dynamic-parse-file
+
+(define (dynamic-parse-file file-name)
+  (let ((input-port (open-input-file file-name)))
+    (dynamic-parse-from-port input-port)))
+;----------------------------------------------------------------------------
+; Implementation of Union/find data structure in Scheme
+;----------------------------------------------------------------------------
+
+;; for union/find the following attributes are necessary: rank, parent 
+;; (see Tarjan, "Data structures and network algorithms", 1983)
+;; In the Scheme realization an element is represented as a single
+;; cons cell; its address is the element itself; the car field contains 
+;; the parent, the cdr field is an address for a cons
+;; cell containing the rank (car field) and the information (cdr field)
+
+
+;; general union/find data structure
+;; 
+;; gen-element: Info -> Elem
+;; find: Elem -> Elem
+;; link: Elem! x Elem! -> Elem
+;; asymm-link: Elem! x Elem! -> Elem
+;; info: Elem -> Info
+;; set-info!: Elem! x Info -> Void
+
+
+(define (gen-element info)
+  ; generates a new element: the parent field is initialized to '(),
+  ; the rank field to 0
+  (cons '() (cons 0 info)))
+
+(define info (lambda (l) (cddr l)))
+  ; returns the information stored in an element
+
+(define (set-info! elem info)
+  ; sets the info-field of elem to info
+  (set-cdr! (cdr elem) info))
+
+; (define (find! x)
+;   ; finds the class representative of x and sets the parent field 
+;   ; directly to the class representative (a class representative has
+;   ; '() as its parent) (uses path halving)
+;   ;(display "Find!: ")
+;   ;(display (pretty-print (info x)))
+;   ;(newline)
+;   (let ((px (car x)))
+;     (if (null? px)
+;      x
+;      (let ((ppx (car px)))
+;        (if (null? ppx)
+;            px
+;            (begin
+;              (set-car! x ppx)
+;              (find! ppx)))))))
+
+(define (find! elem)
+  ; finds the class representative of elem and sets the parent field 
+  ; directly to the class representative (a class representative has
+  ; '() as its parent)
+  ;(display "Find!: ")
+  ;(display (pretty-print (info elem)))
+  ;(newline)
+  (let ((p-elem (car elem)))
+    (if (null? p-elem)
+       elem
+       (let ((rep-elem (find! p-elem)))
+         (set-car! elem rep-elem)
+         rep-elem))))
+
+(define (link! elem-1 elem-2)
+  ; links class elements by rank
+  ; they must be distinct class representatives
+  ; returns the class representative of the merged equivalence classes
+  ;(display "Link!: ")
+  ;(display (pretty-print (list (info elem-1) (info elem-2))))
+  ;(newline)
+  (let ((rank-1 (cadr elem-1))
+       (rank-2 (cadr elem-2)))
+    (cond
+     ((= rank-1 rank-2)
+      (set-car! (cdr elem-2) (+ rank-2 1))
+      (set-car! elem-1 elem-2)
+      elem-2)
+     ((> rank-1 rank-2)
+      (set-car! elem-2 elem-1)
+      elem-1)
+     (else
+      (set-car! elem-1 elem-2)
+      elem-2))))
+
+(define asymm-link! (lambda (l x) (set-car! l x)))
+
+;(define (asymm-link! elem-1 elem-2)
+  ; links elem-1 onto elem-2 no matter what rank; 
+  ; does not update the rank of elem-2 and does not return a value
+  ; the two arguments must be distinct
+  ;(display "AsymmLink: ")
+  ;(display (pretty-print (list (info elem-1) (info elem-2))))
+  ;(newline)
+  ;(set-car! elem-1 elem-2))
+
+;----------------------------------------------------------------------------
+; Type management
+;----------------------------------------------------------------------------
+
+; introduces type variables and types for Scheme,
+
+
+;; type TVar (type variables)
+;;
+;; gen-tvar:          () -> TVar
+;; gen-type:          TCon x TVar* -> TVar
+;; dynamic:           TVar
+;; tvar-id:           TVar -> Symbol
+;; tvar-def:          TVar -> Type + Null
+;; tvar-show:         TVar -> Symbol*
+;;
+;; set-def!:          !TVar x TCon x TVar* -> Null
+;; equiv!:            !TVar x !TVar -> Null
+;;
+;;
+;; type TCon (type constructors)
+;;
+;; ...
+;;
+;; type Type (types)
+;;
+;; gen-type:          TCon x TVar* -> Type
+;; type-con:          Type -> TCon
+;; type-args:         Type -> TVar*
+;;
+;; boolean:           TVar
+;; character:         TVar
+;; null:              TVar
+;; pair:              TVar x TVar -> TVar
+;; procedure:         TVar x TVar* -> TVar
+;; charseq:           TVar
+;; symbol:            TVar
+;; array:             TVar -> TVar
+
+
+; Needed packages: union/find
+
+;(load "union-fi.so")
+
+; TVar
+
+(define counter 0)
+; counter for generating tvar id's
+
+(define (gen-id)
+  ; generates a new id (for printing purposes)
+  (set! counter (+ counter 1))
+  counter)
+
+(define (gen-tvar)
+  ; generates a new type variable from a new symbol
+  ; uses union/find elements with two info fields
+  ; a type variable has exactly four fields:
+  ; car:     TVar (the parent field; initially null)
+  ; cadr:    Number (the rank field; is always nonnegative)
+  ; caddr:   Symbol (the type variable identifier; used only for printing)
+  ; cdddr:   Type (the leq field; initially null)
+  (gen-element (cons (gen-id) '())))
+
+(define (gen-type tcon targs)
+  ; generates a new type variable with an associated type definition
+  (gen-element (cons (gen-id) (cons tcon targs))))
+
+(define dynamic (gen-element (cons 0 '())))
+; the special type variable dynamic
+; Generic operations
+
+(define (tvar-id tvar)
+  ; returns the (printable) symbol representing the type variable
+  (car (info tvar)))
+
+(define (tvar-def tvar)
+  ; returns the type definition (if any) of the type variable
+  (cdr (info tvar)))
+
+(define (set-def! tvar tcon targs)
+  ; sets the type definition part of tvar to type
+  (set-cdr! (info tvar) (cons tcon targs))
+  '())
+
+(define (reset-def! tvar)
+  ; resets the type definition part of tvar to nil
+  (set-cdr! (info tvar) '()))
+
+(define type-con (lambda (l) (car l)))
+; returns the type constructor of a type definition
+
+(define type-args (lambda (l) (cdr l)))
+; returns the type variables of a type definition
+
+(define (tvar->string tvar)
+  ; converts a tvar's id to a string
+  (if (eqv? (tvar-id tvar) 0)
+      "Dynamic"
+      (string-append "t#" (number->string (tvar-id tvar) 10))))
+
+(define (tvar-show tv)
+  ; returns a printable list representation of type variable tv
+  (let* ((tv-rep (find! tv))
+        (tv-def (tvar-def tv-rep)))
+    (cons (tvar->string tv-rep)
+         (if (null? tv-def)
+             '()
+             (cons 'is (type-show tv-def))))))
+
+(define (type-show type)
+  ; returns a printable list representation of type definition type
+  (cond
+   ((eqv? (type-con type) ptype-con)
+    (let ((new-tvar (gen-tvar)))
+      (cons ptype-con
+           (cons (tvar-show new-tvar)
+                 (tvar-show ((type-args type) new-tvar))))))
+   (else
+    (cons (type-con type)
+         (map (lambda (tv)
+                (tvar->string (find! tv)))
+              (type-args type))))))
+
+
+
+; Special type operations
+
+; type constructor literals
+
+(define boolean-con 'boolean)
+(define char-con 'char)
+(define null-con 'null)
+(define number-con 'number)
+(define pair-con 'pair)
+(define procedure-con 'procedure)
+(define string-con 'string)
+(define symbol-con 'symbol)
+(define vector-con 'vector)
+
+; type constants and type constructors
+
+(define (null)
+  ; ***Note***: Temporarily changed to be a pair!
+  ; (gen-type null-con '())
+  (pair (gen-tvar) (gen-tvar)))
+(define (boolean)
+  (gen-type boolean-con '()))
+(define (character)
+  (gen-type char-con '()))
+(define (number)
+  (gen-type number-con '()))
+(define (charseq)
+  (gen-type string-con '()))
+(define (symbol)
+  (gen-type symbol-con '()))
+(define (pair tvar-1 tvar-2)
+  (gen-type pair-con (list tvar-1 tvar-2)))
+(define (array tvar)
+  (gen-type vector-con (list tvar)))
+(define (procedure arg-tvar res-tvar)
+  (gen-type procedure-con (list arg-tvar res-tvar)))
+
+
+; equivalencing of type variables
+
+(define (equiv! tv1 tv2)
+  (let* ((tv1-rep (find! tv1))
+        (tv2-rep (find! tv2))
+        (tv1-def (tvar-def tv1-rep))
+        (tv2-def (tvar-def tv2-rep)))
+    (cond
+     ((eqv? tv1-rep tv2-rep)
+      '())
+     ((eqv? tv2-rep dynamic)
+      (equiv-with-dynamic! tv1-rep))
+     ((eqv? tv1-rep dynamic)
+      (equiv-with-dynamic! tv2-rep))
+     ((null? tv1-def)
+      (if (null? tv2-def)
+         ; both tv1 and tv2 are distinct type variables
+         (link! tv1-rep tv2-rep)
+         ; tv1 is a type variable, tv2 is a (nondynamic) type
+         (asymm-link! tv1-rep tv2-rep)))
+     ((null? tv2-def)
+      ; tv1 is a (nondynamic) type, tv2 is a type variable
+      (asymm-link! tv2-rep tv1-rep))
+     ((eqv? (type-con tv1-def) (type-con tv2-def))
+      ; both tv1 and tv2 are (nondynamic) types with equal numbers of
+      ; arguments
+      (link! tv1-rep tv2-rep)
+      (map equiv! (type-args tv1-def) (type-args tv2-def)))
+     (else
+      ; tv1 and tv2 are types with distinct type constructors or different
+      ; numbers of arguments
+      (equiv-with-dynamic! tv1-rep)
+      (equiv-with-dynamic! tv2-rep))))
+  '())
+
+(define (equiv-with-dynamic! tv)
+  (let ((tv-rep (find! tv)))
+    (if (not (eqv? tv-rep dynamic))
+       (let ((tv-def (tvar-def tv-rep)))
+         (asymm-link! tv-rep dynamic)
+         (if (not (null? tv-def))
+             (map equiv-with-dynamic! (type-args tv-def))))))
+  '())
+;----------------------------------------------------------------------------
+; Polymorphic type management
+;----------------------------------------------------------------------------
+
+; introduces parametric polymorphic types
+
+
+;; forall: (Tvar -> Tvar) -> TVar
+;; fix: (Tvar -> Tvar) -> Tvar
+;;  
+;; instantiate-type: TVar -> TVar
+
+; type constructor literal for polymorphic types
+
+(define ptype-con 'forall)
+
+(define (forall tv-func)
+  (gen-type ptype-con tv-func))
+
+(define (forall2 tv-func2)
+  (forall (lambda (tv1)
+           (forall (lambda (tv2)
+                     (tv-func2 tv1 tv2))))))
+
+(define (forall3 tv-func3)
+  (forall (lambda (tv1)
+           (forall2 (lambda (tv2 tv3)
+                      (tv-func3 tv1 tv2 tv3))))))
+
+(define (forall4 tv-func4)
+  (forall (lambda (tv1)
+           (forall3 (lambda (tv2 tv3 tv4)
+                      (tv-func4 tv1 tv2 tv3 tv4))))))
+
+(define (forall5 tv-func5)
+  (forall (lambda (tv1)
+           (forall4 (lambda (tv2 tv3 tv4 tv5)
+                      (tv-func5 tv1 tv2 tv3 tv4 tv5))))))
+
+
+; (polymorphic) instantiation
+
+(define (instantiate-type tv)
+  ; instantiates type tv and returns a generic instance
+  (let* ((tv-rep (find! tv))
+        (tv-def (tvar-def tv-rep)))
+    (cond 
+     ((null? tv-def)
+      tv-rep)
+     ((eqv? (type-con tv-def) ptype-con)
+      (instantiate-type ((type-args tv-def) (gen-tvar))))
+     (else
+      tv-rep))))
+
+(define (fix tv-func)
+  ; forms a recursive type: the fixed point of type mapping tv-func
+  (let* ((new-tvar (gen-tvar))
+        (inst-tvar (tv-func new-tvar))
+        (inst-def (tvar-def inst-tvar)))
+    (if (null? inst-def)
+       (error 'fix "Illegal recursive type: ~s"
+              (list (tvar-show new-tvar) '= (tvar-show inst-tvar)))
+       (begin
+         (set-def! new-tvar 
+                   (type-con inst-def)
+                   (type-args inst-def))
+         new-tvar))))
+
+  
+;----------------------------------------------------------------------------
+;      Constraint management 
+;----------------------------------------------------------------------------
+
+
+; constraints
+
+(define gen-constr (lambda (a b) (cons a b)))
+; generates an equality between tvar1 and tvar2
+
+(define constr-lhs (lambda (c) (car c)))
+; returns the left-hand side of a constraint
+
+(define constr-rhs (lambda (c) (cdr c)))
+; returns the right-hand side of a constraint
+
+(define (constr-show c)
+  (cons (tvar-show (car c)) 
+       (cons '= 
+             (cons (tvar-show (cdr c)) '()))))
+
+
+; constraint set management
+
+(define global-constraints '())
+
+(define (init-global-constraints!)
+  (set! global-constraints '()))
+
+(define (add-constr! lhs rhs)
+  (set! global-constraints
+       (cons (gen-constr lhs rhs) global-constraints))
+  '())
+
+(define (glob-constr-show) 
+  ; returns printable version of global constraints
+  (map constr-show global-constraints))
+
+
+; constraint normalization
+
+; Needed packages: type management
+
+;(load "typ-mgmt.so")
+
+(define (normalize-global-constraints!) 
+  (normalize! global-constraints)
+  (init-global-constraints!))
+
+(define (normalize! constraints)
+  (map (lambda (c)
+        (equiv! (constr-lhs c) (constr-rhs c))) constraints))
+; ----------------------------------------------------------------------------
+; Abstract syntax definition and parse actions
+; ----------------------------------------------------------------------------
+
+; Needed packages: ast-gen.ss
+;(load "ast-gen.ss")
+
+;; Abstract syntax
+;;
+;; VarDef
+;;
+;; Identifier =                Symbol - SyntacticKeywords
+;; SyntacticKeywords = { ... } (see Section 7.1, IEEE Scheme Standard)
+;;
+;; Datum
+;;
+;; null-const:         Null            -> Datum
+;; boolean-const:      Bool            -> Datum
+;; char-const:         Char            -> Datum
+;; number-const:       Number          -> Datum
+;; string-const:       String          -> Datum
+;; vector-const:       Datum*          -> Datum
+;; pair-const:         Datum x Datum   -> Datum
+;;
+;; Expr
+;;
+;; Datum <             Expr
+;;
+;; var-def:             Identifier              -> VarDef
+;; variable:           VarDef                  -> Expr
+;; identifier:         Identifier              -> Expr
+;; procedure-call:     Expr x Expr*            -> Expr
+;; lambda-expression:  Formals x Body          -> Expr
+;; conditional:                Expr x Expr x Expr      -> Expr
+;; assignment:         Variable x Expr         -> Expr
+;; cond-expression:    CondClause+             -> Expr
+;; case-expression:    Expr x CaseClause*      -> Expr
+;; and-expression:     Expr*                   -> Expr
+;; or-expression:      Expr*                   -> Expr
+;; let-expression:     (VarDef* x Expr*) x Body -> Expr
+;; named-let-expression: VarDef x (VarDef* x Expr*) x Body -> Expr
+;; let*-expression:    (VarDef* x Expr*) x Body -> Expr
+;; letrec-expression:  (VarDef* x Expr*) x Body -> Expr
+;; begin-expression:   Expr+                   -> Expr
+;; do-expression:      IterDef* x CondClause x Expr* -> Expr
+;; empty:                                      -> Expr
+;;
+;; VarDef* <           Formals
+;;
+;; simple-formal:      VarDef                  -> Formals
+;; dotted-formals:     VarDef* x VarDef        -> Formals
+;;
+;; Body =              Definition* x Expr+     (reversed)
+;; CondClause =                Expr x Expr+
+;; CaseClause =                Datum* x Expr+
+;; IterDef =           VarDef x Expr x Expr
+;;
+;; Definition
+;;
+;; definition:         Identifier x Expr       -> Definition
+;; function-definition: Identifier x Formals x Body -> Definition
+;; begin-command:      Definition*             -> Definition
+;;
+;; Expr <              Command
+;; Definition <                Command
+;;
+;; Program =           Command*
+
+
+;; Abstract syntax operators
+
+; Datum
+
+(define null-const 0)
+(define boolean-const 1)
+(define char-const 2)
+(define number-const 3)
+(define string-const 4)
+(define symbol-const 5)
+(define vector-const 6)
+(define pair-const 7)
+
+; Bindings
+
+(define var-def 8)
+(define null-def 29)
+(define pair-def 30)
+
+; Expr
+
+(define variable 9)
+(define identifier 10)
+(define procedure-call 11)
+(define lambda-expression 12)
+(define conditional 13)
+(define assignment 14)
+(define cond-expression 15)
+(define case-expression 16)
+(define and-expression 17)
+(define or-expression 18)
+(define let-expression 19)
+(define named-let-expression 20)
+(define let*-expression 21)
+(define letrec-expression 22)
+(define begin-expression 23)
+(define do-expression 24)
+(define empty 25)
+(define null-arg 31)
+(define pair-arg 32)
+
+; Command
+
+(define definition 26)
+(define function-definition 27)
+(define begin-command 28)
+
+
+;; Parse actions for abstract syntax construction
+
+(define (dynamic-parse-action-null-const)
+  ;; dynamic-parse-action for '()
+  (ast-gen null-const '()))
+
+(define (dynamic-parse-action-boolean-const e)
+  ;; dynamic-parse-action for #f and #t
+  (ast-gen boolean-const e))
+
+(define (dynamic-parse-action-char-const e)
+  ;; dynamic-parse-action for character constants
+  (ast-gen char-const e))
+
+(define (dynamic-parse-action-number-const e)
+  ;; dynamic-parse-action for number constants
+  (ast-gen number-const e))
+
+(define (dynamic-parse-action-string-const e)
+  ;; dynamic-parse-action for string literals
+  (ast-gen string-const e))
+
+(define (dynamic-parse-action-symbol-const e)
+  ;; dynamic-parse-action for symbol constants
+  (ast-gen symbol-const e))
+
+(define (dynamic-parse-action-vector-const e)
+  ;; dynamic-parse-action for vector literals
+  (ast-gen vector-const e))
+
+(define (dynamic-parse-action-pair-const e1 e2)
+  ;; dynamic-parse-action for pairs
+  (ast-gen pair-const (cons e1 e2)))
+
+(define (dynamic-parse-action-var-def e)
+  ;; dynamic-parse-action for defining occurrences of variables;
+  ;; e is a symbol
+  (ast-gen var-def e))
+
+(define (dynamic-parse-action-null-formal)
+  ;; dynamic-parse-action for null-list of formals
+  (ast-gen null-def '()))
+
+(define (dynamic-parse-action-pair-formal d1 d2)
+  ;; dynamic-parse-action for non-null list of formals;
+  ;; d1 is the result of parsing the first formal,
+  ;; d2 the result of parsing the remaining formals
+  (ast-gen pair-def (cons d1 d2)))
+
+(define (dynamic-parse-action-variable e)
+  ;; dynamic-parse-action for applied occurrences of variables
+  ;; ***Note***: e is the result of a dynamic-parse-action on the
+  ;; corresponding variable definition!
+  (ast-gen variable e))
+
+(define (dynamic-parse-action-identifier e)
+  ;; dynamic-parse-action for undeclared identifiers (free variable
+  ;; occurrences)
+  ;; ***Note***: e is a symbol (legal identifier)
+  (ast-gen identifier e))
+(define (dynamic-parse-action-null-arg)
+  ;; dynamic-parse-action for a null list of arguments in a procedure call
+  (ast-gen null-arg '()))
+
+(define (dynamic-parse-action-pair-arg a1 a2)
+  ;; dynamic-parse-action for a non-null list of arguments in a procedure call
+  ;; a1 is the result of parsing the first argument, 
+  ;; a2 the result of parsing the remaining arguments
+  (ast-gen pair-arg (cons a1 a2)))
+
+(define (dynamic-parse-action-procedure-call op args)
+  ;; dynamic-parse-action for procedure calls: op function, args list of arguments
+  (ast-gen procedure-call (cons op args)))
+
+(define (dynamic-parse-action-lambda-expression formals body)
+  ;; dynamic-parse-action for lambda-abstractions
+  (ast-gen lambda-expression (cons formals body)))
+
+(define (dynamic-parse-action-conditional test then-branch else-branch)
+  ;; dynamic-parse-action for conditionals (if-then-else expressions)
+  (ast-gen conditional (cons test (cons then-branch else-branch))))
+
+(define (dynamic-parse-action-empty)
+  ;; dynamic-parse-action for missing or empty field
+  (ast-gen empty '()))
+
+(define (dynamic-parse-action-assignment lhs rhs)
+  ;; dynamic-parse-action for assignment
+  (ast-gen assignment (cons lhs rhs)))
+
+(define (dynamic-parse-action-begin-expression body)
+  ;; dynamic-parse-action for begin-expression
+  (ast-gen begin-expression body))
+
+(define (dynamic-parse-action-cond-expression clauses)
+  ;; dynamic-parse-action for cond-expressions
+  (ast-gen cond-expression clauses))
+
+(define (dynamic-parse-action-and-expression args)
+  ;; dynamic-parse-action for and-expressions
+  (ast-gen and-expression args))
+
+(define (dynamic-parse-action-or-expression args)
+  ;; dynamic-parse-action for or-expressions
+  (ast-gen or-expression args))
+
+(define (dynamic-parse-action-case-expression key clauses)
+  ;; dynamic-parse-action for case-expressions
+  (ast-gen case-expression (cons key clauses)))
+
+(define (dynamic-parse-action-let-expression bindings body)
+  ;; dynamic-parse-action for let-expressions
+  (ast-gen let-expression (cons bindings body)))
+
+(define (dynamic-parse-action-named-let-expression variable bindings body)
+  ;; dynamic-parse-action for named-let expressions
+  (ast-gen named-let-expression (cons variable (cons bindings body))))
+
+(define (dynamic-parse-action-let*-expression bindings body)
+  ;; dynamic-parse-action for let-expressions
+  (ast-gen let*-expression (cons bindings body)))
+
+(define (dynamic-parse-action-letrec-expression bindings body)
+  ;; dynamic-parse-action for let-expressions
+  (ast-gen letrec-expression (cons bindings body)))
+
+(define (dynamic-parse-action-definition variable expr)
+  ;; dynamic-parse-action for simple definitions
+  (ast-gen definition (cons variable expr)))
+
+(define (dynamic-parse-action-function-definition variable formals body)
+  ;; dynamic-parse-action for function definitions
+  (ast-gen function-definition (cons variable (cons formals body))))
+
+
+(define dynamic-parse-action-commands (lambda (a b) (cons a b)))
+;; dynamic-parse-action for processing a command result followed by a the
+;; result of processing the remaining commands
+
+
+;; Pretty-printing abstract syntax trees
+
+(define (ast-show ast)
+  ;; converts abstract syntax tree to list representation (Scheme program)
+  ;; ***Note***: check translation of constructors to numbers at the top of the file
+  (let ((syntax-op (ast-con ast))
+       (syntax-arg (ast-arg ast)))
+    (case syntax-op
+      ((0 1 2 3 4 8 10) syntax-arg)
+      ((29 31) '())
+      ((30 32) (cons (ast-show (car syntax-arg)) (ast-show (cdr syntax-arg))))
+      ((5) (list 'quote syntax-arg))
+      ((6) (list->vector (map ast-show syntax-arg)))
+      ((7) (list 'cons (ast-show (car syntax-arg)) (ast-show (cdr syntax-arg))))
+      ((9) (ast-arg syntax-arg))
+      ((11) (cons (ast-show (car syntax-arg)) (ast-show (cdr syntax-arg))))
+      ((12) (cons 'lambda (cons (ast-show (car syntax-arg)) 
+                               (map ast-show (cdr syntax-arg)))))
+      ((13) (cons 'if (cons (ast-show (car syntax-arg))
+                           (cons (ast-show (cadr syntax-arg))
+                                 (let ((alt (cddr syntax-arg)))
+                                   (if (eqv? (ast-con alt) empty)
+                                       '()
+                                       (list (ast-show alt))))))))
+      ((14) (list 'set! (ast-show (car syntax-arg)) (ast-show (cdr syntax-arg))))
+      ((15) (cons 'cond
+                 (map (lambda (cc)
+                        (let ((guard (car cc))
+                              (body (cdr cc)))
+                          (cons
+                           (if (eqv? (ast-con guard) empty)
+                               'else
+                               (ast-show guard))
+                           (map ast-show body))))
+                      syntax-arg)))
+      ((16) (cons 'case
+                 (cons (ast-show (car syntax-arg))
+                       (map (lambda (cc)
+                              (let ((data (car cc)))
+                                (if (and (pair? data)
+                                         (eqv? (ast-con (car data)) empty))
+                                    (cons 'else
+                                          (map ast-show (cdr cc)))
+                                    (cons (map datum-show data)
+                                          (map ast-show (cdr cc))))))
+                            (cdr syntax-arg)))))
+      ((17) (cons 'and (map ast-show syntax-arg)))
+      ((18) (cons 'or (map ast-show syntax-arg)))
+      ((19) (cons 'let
+                 (cons (map
+                        (lambda (vd e)
+                          (list (ast-show vd) (ast-show e)))
+                        (caar syntax-arg)
+                        (cdar syntax-arg))
+                       (map ast-show (cdr syntax-arg)))))
+      ((20) (cons 'let
+                 (cons (ast-show (car syntax-arg))
+                       (cons (map
+                              (lambda (vd e)
+                                (list (ast-show vd) (ast-show e)))
+                              (caadr syntax-arg)
+                              (cdadr syntax-arg))
+                             (map ast-show (cddr syntax-arg))))))
+      ((21) (cons 'let*
+                 (cons (map
+                        (lambda (vd e)
+                          (list (ast-show vd) (ast-show e)))
+                        (caar syntax-arg)
+                        (cdar syntax-arg))
+                       (map ast-show (cdr syntax-arg)))))
+      ((22) (cons 'letrec
+                 (cons (map
+                        (lambda (vd e)
+                          (list (ast-show vd) (ast-show e)))
+                        (caar syntax-arg)
+                        (cdar syntax-arg))
+                       (map ast-show (cdr syntax-arg)))))
+      ((23) (cons 'begin
+                 (map ast-show syntax-arg)))
+      ((24) (error 'ast-show "Do expressions not handled! (~s)" syntax-arg))
+      ((25) (error 'ast-show "This can't happen: empty encountered!"))
+      ((26) (list 'define
+                 (ast-show (car syntax-arg))
+                 (ast-show (cdr syntax-arg))))
+      ((27) (cons 'define
+                 (cons
+                  (cons (ast-show (car syntax-arg))
+                        (ast-show (cadr syntax-arg)))
+                  (map ast-show (cddr syntax-arg)))))
+      ((28) (cons 'begin
+                 (map ast-show syntax-arg)))
+      (else (error 'ast-show "Unknown abstract syntax operator: ~s"
+                  syntax-op)))))
+
+
+;; ast*-show
+
+(define (ast*-show p)
+  ;; shows a list of abstract syntax trees
+  (map ast-show p))
+
+
+;; datum-show
+
+(define (datum-show ast)
+  ;; prints an abstract syntax tree as a datum
+  (case (ast-con ast)
+    ((0 1 2 3 4 5) (ast-arg ast))
+    ((6) (list->vector (map datum-show (ast-arg ast))))
+    ((7) (cons (datum-show (car (ast-arg ast))) (datum-show (cdr (ast-arg ast)))))
+    (else (error 'datum-show "This should not happen!"))))
+
+; write-to-port
+
+(define (write-to-port prog port)
+  ; writes a program to a port
+  (for-each
+   (lambda (command)
+     (pretty-print command port)
+     (newline port))
+   prog)
+  '())
+
+; write-file 
+
+(define (write-to-file prog filename)
+  ; write a program to a file
+  (let ((port (open-output-file filename)))
+    (write-to-port prog port)
+    (close-output-port port)
+    '()))
+
+; ----------------------------------------------------------------------------
+; Typed abstract syntax tree management: constraint generation, display, etc.
+; ----------------------------------------------------------------------------
+
+
+;; Abstract syntax operations, incl. constraint generation
+
+(define (ast-gen syntax-op arg)
+  ; generates all attributes and performs semantic side effects
+  (let ((ntvar
+        (case syntax-op
+          ((0 29 31) (null))
+          ((1) (boolean))
+          ((2) (character))
+          ((3) (number))
+          ((4) (charseq))
+          ((5) (symbol))
+          ((6) (let ((aux-tvar (gen-tvar)))
+                 (for-each (lambda (t)
+                             (add-constr! t aux-tvar))
+                           (map ast-tvar arg))
+                 (array aux-tvar)))
+          ((7 30 32) (let ((t1 (ast-tvar (car arg)))
+                           (t2 (ast-tvar (cdr arg))))
+                       (pair t1 t2)))
+          ((8) (gen-tvar))
+          ((9) (ast-tvar arg))
+          ((10) (let ((in-env (dynamic-lookup arg dynamic-top-level-env)))
+                  (if in-env
+                      (instantiate-type (binding-value in-env))
+                      (let ((new-tvar (gen-tvar)))
+                        (set! dynamic-top-level-env (extend-env-with-binding
+                                             dynamic-top-level-env
+                                             (gen-binding arg new-tvar)))
+                        new-tvar))))
+          ((11) (let ((new-tvar (gen-tvar)))
+                  (add-constr! (procedure (ast-tvar (cdr arg)) new-tvar)
+                               (ast-tvar (car arg)))
+                  new-tvar))
+          ((12) (procedure (ast-tvar (car arg))
+                           (ast-tvar (tail (cdr arg)))))
+          ((13) (let ((t-test (ast-tvar (car arg)))
+                      (t-consequent (ast-tvar (cadr arg)))
+                      (t-alternate (ast-tvar (cddr arg))))
+                  (add-constr! (boolean) t-test)
+                  (add-constr! t-consequent t-alternate)
+                  t-consequent))
+          ((14) (let ((var-tvar (ast-tvar (car arg)))
+                      (exp-tvar (ast-tvar (cdr arg))))
+                  (add-constr! var-tvar exp-tvar)
+                  var-tvar))
+          ((15) (let ((new-tvar (gen-tvar)))
+                  (for-each (lambda (body)
+                              (add-constr! (ast-tvar (tail body)) new-tvar))
+                            (map cdr arg))
+                  (for-each (lambda (e)
+                              (add-constr! (boolean) (ast-tvar e)))
+                            (map car arg))
+                  new-tvar))
+          ((16) (let* ((new-tvar (gen-tvar))
+                       (t-key (ast-tvar (car arg)))
+                       (case-clauses (cdr arg)))
+                  (for-each (lambda (exprs)
+                              (for-each (lambda (e)
+                                          (add-constr! (ast-tvar e) t-key))
+                                        exprs))
+                            (map car case-clauses))
+                  (for-each (lambda (body)
+                              (add-constr! (ast-tvar (tail body)) new-tvar))
+                            (map cdr case-clauses))
+                  new-tvar))
+          ((17 18) (for-each (lambda (e)
+                               (add-constr! (boolean) (ast-tvar e)))
+                             arg)
+                   (boolean))
+          ((19 21 22) (let ((var-def-tvars (map ast-tvar (caar arg)))
+                            (def-expr-types (map ast-tvar (cdar arg)))
+                            (body-type (ast-tvar (tail (cdr arg)))))
+                        (for-each add-constr! var-def-tvars def-expr-types)
+                        body-type))
+          ((20) (let ((var-def-tvars (map ast-tvar (caadr arg)))
+                      (def-expr-types (map ast-tvar (cdadr arg)))
+                      (body-type (ast-tvar (tail (cddr arg))))
+                      (named-var-type (ast-tvar (car arg))))
+                  (for-each add-constr! var-def-tvars def-expr-types)
+                  (add-constr! (procedure (convert-tvars var-def-tvars) body-type)
+                               named-var-type)
+                  body-type))
+          ((23) (ast-tvar (tail arg)))
+          ((24) (error 'ast-gen
+                       "Do-expressions not handled! (Argument: ~s) arg"))
+          ((25) (gen-tvar))
+          ((26) (let ((t-var (ast-tvar (car arg)))
+                      (t-exp (ast-tvar (cdr arg))))
+                  (add-constr! t-var t-exp)
+                  t-var))
+          ((27) (let ((t-var (ast-tvar (car arg)))
+                      (t-formals (ast-tvar (cadr arg)))
+                      (t-body (ast-tvar (tail (cddr arg)))))
+                  (add-constr! (procedure t-formals t-body) t-var)
+                  t-var))
+          ((28) (gen-tvar))
+          (else (error 'ast-gen "Can't handle syntax operator: ~s" syntax-op)))))
+    (cons syntax-op (cons ntvar arg))))
+
+(define ast-con car)
+;; extracts the ast-constructor from an abstract syntax tree
+
+(define ast-arg cddr)
+;; extracts the ast-argument from an abstract syntax tree
+
+(define ast-tvar cadr)
+;; extracts the tvar from an abstract syntax tree
+
+
+;; tail
+
+(define (tail l)
+  ;; returns the tail of a nonempty list
+  (if (null? (cdr l))
+      (car l)
+      (tail (cdr l))))
+
+; convert-tvars
+
+(define (convert-tvars tvar-list)
+  ;; converts a list of tvars to a single tvar
+  (cond
+   ((null? tvar-list) (null))
+   ((pair? tvar-list) (pair (car tvar-list)
+                           (convert-tvars (cdr tvar-list))))
+   (else (error 'convert-tvars "Not a list of tvars: ~s" tvar-list))))
+
+
+;; Pretty-printing abstract syntax trees
+
+(define (tast-show ast)
+  ;; converts abstract syntax tree to list representation (Scheme program)
+  (let ((syntax-op (ast-con ast))
+        (syntax-tvar (tvar-show (ast-tvar ast)))
+       (syntax-arg (ast-arg ast)))
+    (cons
+     (case syntax-op
+       ((0 1 2 3 4 8 10) syntax-arg)
+       ((29 31) '())
+       ((30 32) (cons (tast-show (car syntax-arg))
+                     (tast-show (cdr syntax-arg))))
+       ((5) (list 'quote syntax-arg))
+       ((6) (list->vector (map tast-show syntax-arg)))
+       ((7) (list 'cons (tast-show (car syntax-arg))
+                 (tast-show (cdr syntax-arg))))
+       ((9) (ast-arg syntax-arg))
+       ((11) (cons (tast-show (car syntax-arg)) (tast-show (cdr syntax-arg))))
+       ((12) (cons 'lambda (cons (tast-show (car syntax-arg))
+                                (map tast-show (cdr syntax-arg)))))
+       ((13) (cons 'if (cons (tast-show (car syntax-arg))
+                            (cons (tast-show (cadr syntax-arg))
+                                  (let ((alt (cddr syntax-arg)))
+                                    (if (eqv? (ast-con alt) empty)
+                                        '()
+                                        (list (tast-show alt))))))))
+       ((14) (list 'set! (tast-show (car syntax-arg))
+                  (tast-show (cdr syntax-arg))))
+       ((15) (cons 'cond
+                  (map (lambda (cc)
+                         (let ((guard (car cc))
+                               (body (cdr cc)))
+                           (cons
+                            (if (eqv? (ast-con guard) empty)
+                                'else
+                                (tast-show guard))
+                            (map tast-show body))))
+                       syntax-arg)))
+       ((16) (cons 'case
+                  (cons (tast-show (car syntax-arg))
+                        (map (lambda (cc)
+                               (let ((data (car cc)))
+                                 (if (and (pair? data)
+                                          (eqv? (ast-con (car data)) empty))
+                                     (cons 'else
+                                           (map tast-show (cdr cc)))
+                                     (cons (map datum-show data)
+                                           (map tast-show (cdr cc))))))
+                             (cdr syntax-arg)))))
+       ((17) (cons 'and (map tast-show syntax-arg)))
+       ((18) (cons 'or (map tast-show syntax-arg)))
+       ((19) (cons 'let
+                  (cons (map
+                         (lambda (vd e)
+                           (list (tast-show vd) (tast-show e)))
+                         (caar syntax-arg)
+                         (cdar syntax-arg))
+                        (map tast-show (cdr syntax-arg)))))
+       ((20) (cons 'let
+                  (cons (tast-show (car syntax-arg))
+                        (cons (map
+                               (lambda (vd e)
+                                 (list (tast-show vd) (tast-show e)))
+                               (caadr syntax-arg)
+                               (cdadr syntax-arg))
+                              (map tast-show (cddr syntax-arg))))))
+       ((21) (cons 'let*
+                  (cons (map
+                         (lambda (vd e)
+                           (list (tast-show vd) (tast-show e)))
+                         (caar syntax-arg)
+                         (cdar syntax-arg))
+                        (map tast-show (cdr syntax-arg)))))
+       ((22) (cons 'letrec
+                  (cons (map
+                         (lambda (vd e)
+                           (list (tast-show vd) (tast-show e)))
+                         (caar syntax-arg)
+                         (cdar syntax-arg))
+                        (map tast-show (cdr syntax-arg)))))
+       ((23) (cons 'begin
+                  (map tast-show syntax-arg)))
+       ((24) (error 'tast-show "Do expressions not handled! (~s)" syntax-arg))
+       ((25) (error 'tast-show "This can't happen: empty encountered!"))
+       ((26) (list 'define
+                  (tast-show (car syntax-arg))
+                  (tast-show (cdr syntax-arg))))
+       ((27) (cons 'define
+                  (cons
+                   (cons (tast-show (car syntax-arg))
+                         (tast-show (cadr syntax-arg)))
+                   (map tast-show (cddr syntax-arg)))))
+       ((28) (cons 'begin
+                  (map tast-show syntax-arg)))
+       (else (error 'tast-show "Unknown abstract syntax operator: ~s"
+                   syntax-op)))
+     syntax-tvar)))
+
+;; tast*-show
+
+(define (tast*-show p)
+  ;; shows a list of abstract syntax trees
+  (map tast-show p))
+
+
+;; counters for tagging/untagging
+
+(define untag-counter 0)
+(define no-untag-counter 0)
+(define tag-counter 0)
+(define no-tag-counter 0)
+(define may-untag-counter 0)
+(define no-may-untag-counter 0)
+
+(define (reset-counters!)
+  (set! untag-counter 0)
+  (set! no-untag-counter 0)
+  (set! tag-counter 0)
+  (set! no-tag-counter 0)
+  (set! may-untag-counter 0)
+  (set! no-may-untag-counter 0))
+
+(define (counters-show)
+  (list
+   (cons tag-counter no-tag-counter)
+   (cons untag-counter no-untag-counter)
+   (cons may-untag-counter no-may-untag-counter)))  
+
+
+;; tag-show
+
+(define (tag-show tvar-rep prog)
+  ; display prog with tagging operation
+  (if (eqv? tvar-rep dynamic)
+      (begin
+       (set! tag-counter (+ tag-counter 1))
+       (list 'tag prog))
+      (begin
+       (set! no-tag-counter (+ no-tag-counter 1))
+       (list 'no-tag prog))))
+
+
+;; untag-show
+
+(define (untag-show tvar-rep prog)
+  ; display prog with untagging operation
+  (if (eqv? tvar-rep dynamic)
+      (begin
+       (set! untag-counter (+ untag-counter 1))
+       (list 'untag prog))
+      (begin
+       (set! no-untag-counter (+ no-untag-counter 1))
+       (list 'no-untag prog))))
+
+(define (may-untag-show tvar-rep prog)
+  ; display possible untagging in actual arguments
+  (if (eqv? tvar-rep dynamic)
+      (begin
+       (set! may-untag-counter (+ may-untag-counter 1))
+       (list 'may-untag prog))
+      (begin
+       (set! no-may-untag-counter (+ no-may-untag-counter 1))
+       (list 'no-may-untag prog))))
+
+
+;; tag-ast-show
+
+(define (tag-ast-show ast)
+  ;; converts typed and normalized abstract syntax tree to
+  ;; a Scheme program with explicit tagging and untagging operations
+  (let ((syntax-op (ast-con ast))
+        (syntax-tvar (find! (ast-tvar ast)))
+       (syntax-arg (ast-arg ast)))
+    (case syntax-op
+      ((0 1 2 3 4)
+       (tag-show syntax-tvar syntax-arg))
+      ((8 10) syntax-arg)
+      ((29 31) '())
+      ((30) (cons (tag-ast-show (car syntax-arg))
+                  (tag-ast-show (cdr syntax-arg))))
+      ((32) (cons (may-untag-show (find! (ast-tvar (car syntax-arg)))
+                              (tag-ast-show (car syntax-arg)))
+                  (tag-ast-show (cdr syntax-arg))))
+      ((5) (tag-show syntax-tvar (list 'quote syntax-arg)))
+      ((6) (tag-show syntax-tvar (list->vector (map tag-ast-show syntax-arg))))
+      ((7) (tag-show syntax-tvar (list 'cons (tag-ast-show (car syntax-arg))
+                                      (tag-ast-show (cdr syntax-arg)))))
+      ((9) (ast-arg syntax-arg))
+      ((11) (let ((proc-tvar (find! (ast-tvar (car syntax-arg)))))
+             (cons (untag-show proc-tvar 
+                               (tag-ast-show (car syntax-arg)))
+                   (tag-ast-show (cdr syntax-arg)))))
+      ((12) (tag-show syntax-tvar
+                     (cons 'lambda (cons (tag-ast-show (car syntax-arg))
+                                         (map tag-ast-show (cdr syntax-arg))))))
+      ((13) (let ((test-tvar (find! (ast-tvar (car syntax-arg)))))
+             (cons 'if (cons (untag-show test-tvar
+                                         (tag-ast-show (car syntax-arg)))
+                             (cons (tag-ast-show (cadr syntax-arg))
+                                   (let ((alt (cddr syntax-arg)))
+                                     (if (eqv? (ast-con alt) empty)
+                                         '()
+                                         (list (tag-ast-show alt)))))))))
+      ((14) (list 'set! (tag-ast-show (car syntax-arg))
+                  (tag-ast-show (cdr syntax-arg))))
+      ((15) (cons 'cond
+                 (map (lambda (cc)
+                        (let ((guard (car cc))
+                              (body (cdr cc)))
+                          (cons
+                           (if (eqv? (ast-con guard) empty)
+                               'else
+                               (untag-show (find! (ast-tvar guard))
+                                           (tag-ast-show guard)))
+                           (map tag-ast-show body))))
+                      syntax-arg)))
+      ((16) (cons 'case
+                 (cons (tag-ast-show (car syntax-arg))
+                       (map (lambda (cc)
+                              (let ((data (car cc)))
+                                (if (and (pair? data)
+                                         (eqv? (ast-con (car data)) empty))
+                                    (cons 'else
+                                          (map tag-ast-show (cdr cc)))
+                                    (cons (map datum-show data)
+                                          (map tag-ast-show (cdr cc))))))
+                            (cdr syntax-arg)))))
+      ((17) (cons 'and (map
+                       (lambda (ast)
+                         (let ((bool-tvar (find! (ast-tvar ast))))
+                           (untag-show bool-tvar (tag-ast-show ast))))
+                       syntax-arg)))
+      ((18) (cons 'or (map
+                      (lambda (ast)
+                        (let ((bool-tvar (find! (ast-tvar ast))))
+                          (untag-show bool-tvar (tag-ast-show ast))))
+                      syntax-arg)))
+      ((19) (cons 'let
+                 (cons (map
+                        (lambda (vd e)
+                          (list (tag-ast-show vd) (tag-ast-show e)))
+                        (caar syntax-arg)
+                        (cdar syntax-arg))
+                       (map tag-ast-show (cdr syntax-arg)))))
+      ((20) (cons 'let
+                 (cons (tag-ast-show (car syntax-arg))
+                       (cons (map
+                              (lambda (vd e)
+                                (list (tag-ast-show vd) (tag-ast-show e)))
+                              (caadr syntax-arg)
+                              (cdadr syntax-arg))
+                             (map tag-ast-show (cddr syntax-arg))))))
+      ((21) (cons 'let*
+                 (cons (map
+                        (lambda (vd e)
+                          (list (tag-ast-show vd) (tag-ast-show e)))
+                        (caar syntax-arg)
+                        (cdar syntax-arg))
+                       (map tag-ast-show (cdr syntax-arg)))))
+      ((22) (cons 'letrec
+                 (cons (map
+                        (lambda (vd e)
+                          (list (tag-ast-show vd) (tag-ast-show e)))
+                        (caar syntax-arg)
+                        (cdar syntax-arg))
+                       (map tag-ast-show (cdr syntax-arg)))))
+      ((23) (cons 'begin
+                 (map tag-ast-show syntax-arg)))
+      ((24) (error 'tag-ast-show "Do expressions not handled! (~s)" syntax-arg))
+      ((25) (error 'tag-ast-show "This can't happen: empty encountered!"))
+      ((26) (list 'define
+                 (tag-ast-show (car syntax-arg))
+                 (tag-ast-show (cdr syntax-arg))))
+      ((27) (let ((func-tvar (find! (ast-tvar (car syntax-arg)))))
+             (list 'define
+                   (tag-ast-show (car syntax-arg))
+                   (tag-show func-tvar
+                             (cons 'lambda
+                                   (cons (tag-ast-show (cadr syntax-arg))
+                                         (map tag-ast-show (cddr syntax-arg))))))))
+      ((28) (cons 'begin
+                 (map tag-ast-show syntax-arg)))
+      (else (error 'tag-ast-show "Unknown abstract syntax operator: ~s"
+                  syntax-op)))))
+
+
+; tag-ast*-show
+
+(define (tag-ast*-show p)
+  ; display list of commands/expressions with tagging/untagging
+  ; operations
+  (map tag-ast-show p))
+; ----------------------------------------------------------------------------
+; Top level type environment
+; ----------------------------------------------------------------------------
+
+
+; Needed packages: type management (monomorphic and polymorphic)
+
+;(load "typ-mgmt.ss")
+;(load "ptyp-mgm.ss")
+
+
+; type environment for miscellaneous
+
+(define misc-env
+  (list
+   (cons 'quote (forall (lambda (tv) tv)))
+   (cons 'eqv? (forall (lambda (tv) (procedure (convert-tvars (list tv tv))
+                                              (boolean)))))
+   (cons 'eq? (forall (lambda (tv) (procedure (convert-tvars (list tv tv))
+                                             (boolean)))))
+   (cons 'equal? (forall (lambda (tv) (procedure (convert-tvars (list tv tv))
+                                                (boolean)))))
+   ))
+
+; type environment for input/output
+
+(define io-env
+  (list
+   (cons 'open-input-file (procedure (convert-tvars (list (charseq))) dynamic))
+   (cons 'eof-object? (procedure (convert-tvars (list dynamic)) (boolean)))
+   (cons 'read (forall (lambda (tv)
+                        (procedure (convert-tvars (list tv)) dynamic))))
+   (cons 'write (forall (lambda (tv)
+                         (procedure (convert-tvars (list tv)) dynamic))))
+   (cons 'display (forall (lambda (tv)
+                           (procedure (convert-tvars (list tv)) dynamic))))
+   (cons 'newline (procedure (null) dynamic))
+   (cons 'pretty-print (forall (lambda (tv)
+                                (procedure (convert-tvars (list tv)) dynamic))))))
+
+
+; type environment for Booleans
+
+(define boolean-env
+  (list
+   (cons 'boolean? (forall (lambda (tv)
+                            (procedure (convert-tvars (list tv)) (boolean)))))
+   ;(cons #f (boolean))
+   ; #f doesn't exist in Chez Scheme, but gets mapped to null!
+   (cons #t (boolean))
+   (cons 'not (procedure (convert-tvars (list (boolean))) (boolean)))
+   ))
+
+
+; type environment for pairs and lists
+
+(define (list-type tv)
+  (fix (lambda (tv2) (pair tv tv2))))
+
+(define list-env
+  (list
+   (cons 'pair? (forall2 (lambda (tv1 tv2)
+                          (procedure (convert-tvars (list (pair tv1 tv2)))
+                                     (boolean)))))
+   (cons 'null? (forall2 (lambda (tv1 tv2)
+                          (procedure (convert-tvars (list (pair tv1 tv2)))
+                                     (boolean)))))
+   (cons 'list? (forall2 (lambda (tv1 tv2)
+                          (procedure (convert-tvars (list (pair tv1 tv2)))
+                                     (boolean)))))
+   (cons 'cons (forall2 (lambda (tv1 tv2)
+                         (procedure (convert-tvars (list tv1 tv2))
+                                    (pair tv1 tv2)))))
+   (cons 'car (forall2 (lambda (tv1 tv2)
+                        (procedure (convert-tvars (list (pair tv1 tv2)))
+                                   tv1))))
+   (cons 'cdr (forall2 (lambda (tv1 tv2)
+                        (procedure (convert-tvars (list (pair tv1 tv2)))
+                                   tv2))))
+   (cons 'set-car! (forall2 (lambda (tv1 tv2)
+                             (procedure (convert-tvars (list (pair tv1 tv2)
+                                                             tv1))
+                                        dynamic))))
+   (cons 'set-cdr! (forall2 (lambda (tv1 tv2)
+                             (procedure (convert-tvars (list (pair tv1 tv2)
+                                                             tv2))
+                                        dynamic))))
+   (cons 'caar (forall3 (lambda (tv1 tv2 tv3)
+                         (procedure (convert-tvars
+                                     (list (pair (pair tv1 tv2) tv3)))
+                                    tv1))))
+   (cons 'cdar (forall3 (lambda (tv1 tv2 tv3)
+                         (procedure (convert-tvars
+                                     (list (pair (pair tv1 tv2) tv3)))
+                                    tv2))))
+
+   (cons 'cadr (forall3 (lambda (tv1 tv2 tv3)
+                         (procedure (convert-tvars
+                                     (list (pair tv1 (pair tv2 tv3))))
+                                    tv2))))
+   (cons 'cddr (forall3 (lambda (tv1 tv2 tv3)
+                         (procedure (convert-tvars
+                                     (list (pair tv1 (pair tv2 tv3))))
+                                    tv3))))
+   (cons 'caaar (forall4
+                (lambda (tv1 tv2 tv3 tv4)
+                  (procedure (convert-tvars
+                              (list (pair (pair (pair tv1 tv2) tv3) tv4)))
+                             tv1))))
+   (cons 'cdaar (forall4
+                (lambda (tv1 tv2 tv3 tv4)
+                  (procedure (convert-tvars
+                              (list (pair (pair (pair tv1 tv2) tv3) tv4)))
+                             tv2))))
+   (cons 'cadar (forall4
+                (lambda (tv1 tv2 tv3 tv4)
+                  (procedure (convert-tvars
+                              (list (pair (pair tv1 (pair tv2 tv3)) tv4)))
+                             tv2))))
+   (cons 'cddar (forall4
+                (lambda (tv1 tv2 tv3 tv4)
+                  (procedure (convert-tvars
+                              (list (pair (pair tv1 (pair tv2 tv3)) tv4)))
+                             tv3))))
+   (cons 'caadr (forall4
+                (lambda (tv1 tv2 tv3 tv4)
+                  (procedure (convert-tvars
+                              (list (pair tv1 (pair (pair tv2 tv3) tv4))))
+                             tv2))))
+   (cons 'cdadr (forall4
+                (lambda (tv1 tv2 tv3 tv4)
+                  (procedure (convert-tvars
+                              (list (pair tv1 (pair (pair tv2 tv3) tv4))))
+                             tv3))))
+   (cons 'caddr (forall4
+                (lambda (tv1 tv2 tv3 tv4)
+                  (procedure (convert-tvars
+                              (list (pair tv1 (pair tv2 (pair tv3 tv4)))))
+                             tv3))))
+   (cons 'cdddr (forall4
+                (lambda (tv1 tv2 tv3 tv4)
+                  (procedure (convert-tvars
+                              (list (pair tv1 (pair tv2 (pair tv3 tv4)))))
+                             tv4))))
+   (cons 'cadddr
+         (forall5 (lambda (tv1 tv2 tv3 tv4 tv5)
+                    (procedure (convert-tvars
+                               (list (pair tv1
+                                           (pair tv2
+                                                 (pair tv3
+                                                       (pair tv4 tv5))))))
+                              tv4))))
+   (cons 'cddddr
+         (forall5 (lambda (tv1 tv2 tv3 tv4 tv5)
+                    (procedure (convert-tvars
+                               (list (pair tv1
+                                           (pair tv2
+                                                 (pair tv3
+                                                       (pair tv4 tv5))))))
+                              tv5))))
+   (cons 'list (forall (lambda (tv)
+                        (procedure tv tv))))
+   (cons 'length (forall (lambda (tv)
+                          (procedure (convert-tvars (list (list-type tv)))
+                                     (number)))))
+   (cons 'append (forall (lambda (tv)
+                          (procedure (convert-tvars (list (list-type tv)
+                                                          (list-type tv)))
+                                     (list-type tv)))))
+   (cons 'reverse (forall (lambda (tv)
+                           (procedure (convert-tvars (list (list-type tv)))
+                                      (list-type tv)))))
+   (cons 'list-ref (forall (lambda (tv)
+                            (procedure (convert-tvars (list (list-type tv)
+                                                            (number)))
+                                       tv))))
+   (cons 'memq (forall (lambda (tv)
+                        (procedure (convert-tvars (list tv
+                                                        (list-type tv)))
+                                   (boolean)))))
+   (cons 'memv (forall (lambda (tv)
+                        (procedure (convert-tvars (list tv
+                                                        (list-type tv)))
+                                   (boolean)))))
+   (cons 'member (forall (lambda (tv)
+                          (procedure (convert-tvars (list tv
+                                                          (list-type tv)))
+                                     (boolean)))))
+   (cons 'assq (forall2 (lambda (tv1 tv2)
+                         (procedure (convert-tvars
+                                     (list tv1
+                                           (list-type (pair tv1 tv2))))
+                                    (pair tv1 tv2)))))
+   (cons 'assv (forall2 (lambda (tv1 tv2)
+                         (procedure (convert-tvars
+                                     (list tv1
+                                           (list-type (pair tv1 tv2))))
+                                    (pair tv1 tv2)))))
+   (cons 'assoc (forall2 (lambda (tv1 tv2)
+                          (procedure (convert-tvars
+                                      (list tv1
+                                            (list-type (pair tv1 tv2))))
+                                     (pair tv1 tv2)))))
+   ))
+
+
+(define symbol-env
+  (list
+   (cons 'symbol? (forall (lambda (tv)
+                           (procedure (convert-tvars (list tv)) (boolean)))))
+   (cons 'symbol->string (procedure (convert-tvars (list (symbol))) (charseq)))
+   (cons 'string->symbol (procedure (convert-tvars (list (charseq))) (symbol)))
+   ))
+
+(define number-env
+  (list
+   (cons 'number? (forall (lambda (tv)
+                           (procedure (convert-tvars (list tv)) (boolean)))))
+   (cons '+ (procedure (convert-tvars (list (number) (number))) (number)))
+   (cons '- (procedure (convert-tvars (list (number) (number))) (number)))
+   (cons '* (procedure (convert-tvars (list (number) (number))) (number)))
+   (cons '/ (procedure (convert-tvars (list (number) (number))) (number)))
+   (cons 'number->string (procedure (convert-tvars (list (number))) (charseq)))
+   (cons 'string->number (procedure (convert-tvars (list (charseq))) (number)))
+   ))
+
+(define char-env
+  (list
+   (cons 'char? (forall (lambda (tv)
+                         (procedure (convert-tvars (list tv)) (boolean)))))
+   (cons 'char->integer (procedure (convert-tvars (list (character)))
+                                   (number)))
+   (cons 'integer->char (procedure (convert-tvars (list (number)))
+                                   (character)))
+   ))
+
+(define string-env
+  (list
+   (cons 'string? (forall (lambda (tv)
+                           (procedure (convert-tvars (list tv)) (boolean)))))
+   ))
+
+(define vector-env
+  (list
+   (cons 'vector? (forall (lambda (tv)
+                           (procedure (convert-tvars (list tv)) (boolean)))))
+   (cons 'make-vector (forall (lambda (tv)
+                               (procedure (convert-tvars (list (number)))
+                                          (array tv)))))
+   (cons 'vector-length (forall (lambda (tv)
+                                 (procedure (convert-tvars (list (array tv)))
+                                            (number)))))
+   (cons 'vector-ref (forall (lambda (tv)
+                              (procedure (convert-tvars (list (array tv)
+                                                              (number)))
+                                         tv))))
+   (cons 'vector-set! (forall (lambda (tv)
+                               (procedure (convert-tvars (list (array tv)
+                                                               (number)
+                                                               tv))
+                                          dynamic))))
+   ))
+
+(define procedure-env
+  (list
+   (cons 'procedure? (forall (lambda (tv)
+                              (procedure (convert-tvars (list tv)) (boolean)))))
+   (cons 'map (forall2 (lambda (tv1 tv2)
+                        (procedure (convert-tvars
+                                    (list (procedure (convert-tvars
+                                                      (list tv1)) tv2)
+                                          (list-type tv1)))
+                                   (list-type tv2)))))
+   (cons 'foreach (forall2 (lambda (tv1 tv2)
+                            (procedure (convert-tvars
+                                        (list (procedure (convert-tvars
+                                                          (list tv1)) tv2)
+                                              (list-type tv1)))
+                                       (list-type tv2)))))
+   (cons 'call-with-current-continuation
+        (forall2 (lambda (tv1 tv2) 
+                  (procedure (convert-tvars
+                              (list (procedure
+                                     (convert-tvars
+                                      (list (procedure (convert-tvars
+                                                        (list tv1)) tv2)))
+                                     tv2)))
+                             tv2))))
+   ))
+
+
+; global top level environment
+
+(define (global-env)
+  (append misc-env
+         io-env
+         boolean-env
+         symbol-env
+         number-env
+         char-env
+         string-env
+         vector-env
+         procedure-env
+         list-env))
+
+(define dynamic-top-level-env (global-env))
+
+(define (init-dynamic-top-level-env!)
+  (set! dynamic-top-level-env (global-env))
+  '())
+
+(define (dynamic-top-level-env-show)
+  ; displays the top level environment
+  (map (lambda (binding)
+        (cons (key-show (binding-key binding))
+              (cons ': (tvar-show (binding-value binding)))))
+       (env->list dynamic-top-level-env)))
+; ----------------------------------------------------------------------------
+; Dynamic type inference for Scheme
+; ----------------------------------------------------------------------------
+
+; Needed packages:
+
+(define (ic!) (init-global-constraints!))
+(define (pc) (glob-constr-show))
+(define (lc) (length global-constraints))
+(define (n!) (normalize-global-constraints!))
+(define (pt) (dynamic-top-level-env-show))
+(define (it!) (init-dynamic-top-level-env!))
+(define (io!) (set! tag-ops 0) (set! no-ops 0))
+(define (i!) (ic!) (it!) (io!) '())
+
+(define tag-ops 0)
+(define no-ops 0)
+
+
+; This wasn't intended to be an i/o benchmark,
+; so let's read the file just once.
+
+(define *forms*
+  (call-with-input-file
+    "dynamic-input.sch"
+    (lambda (port)
+      (define (loop forms)
+        (let ((form (read port)))
+          (if (eof-object? form)
+              (reverse forms)
+              (loop (cons form forms)))))
+      (loop '()))))
+
+(define (dynamic-parse-forms forms)
+  (if (null? forms)
+      '()
+      (let ((next-input (car forms)))
+       (dynamic-parse-action-commands
+        (dynamic-parse-command dynamic-empty-env next-input)
+        (dynamic-parse-forms (cdr forms))))))
+
+(define doit 
+  (lambda ()
+    (i!)
+    (let ((foo (dynamic-parse-forms *forms*)))
+      (normalize-global-constraints!)
+      (reset-counters!)
+      (tag-ast*-show foo)
+      (counters-show))))
+
+(define (dynamic-benchmark . rest)
+  (let ((n (if (null? rest) 1 (car rest))))
+    (run-benchmark "dynamic"
+                   n
+                   doit 
+                   (lambda (result) 
+                     #t))))
+
+; eof