APPENDICES: PPL 2010
Abstract Syntax Parser (ASP)…………………………………………….2-7
Date Structures (DS)..……………………………….………………….....8-10
Core of the imperative environment interpreter………………………11-13
Core of the imperative compiler…………………………………………14-16
Typechecking rules…….……………………………………….…………17-18
Abstract Syntax Parser (ASP)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;; Parser procedures ;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (tagged-list? exp tag)
(and (list? exp) (eq? (car exp) tag)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Booleans
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (boolean? exp)
(or (eq? exp '#t) (eq? exp '#f)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Variable
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (variable? exp) (symbol? exp))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Atomic
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (atomic? exp)
(or (number? exp) (boolean? exp) (variable? exp) (null? exp)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Quoted
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (quoted? exp)
(tagged-list? exp 'quote))
(define (text-of-quotation exp) (cadr exp))
(define (make-quote text)
(list 'quote text))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Definition
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (definition? exp)
(tagged-list? exp 'define))
(define (definition-variable exp)
(if (symbol? (cadr exp))
(cadr exp)
(caadr exp)))
(define (definition-value exp)
(if (symbol? (cadr exp))
(caddr exp)
(make-lambda (cdadr exp)
(cddr exp))))
(define (make-definition var val)
(list 'define var val))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Function-definition
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (function-definition? exp)
(and (tagged-list? exp 'define) (list? (cadr exp))))
(define (function-definition-variable exp)
(caadr exp))
(define (function-definition-parameters exp)
(cdadr exp))
(define (function-definition-body exp)
(cddr exp))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Lambda
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (lambda? exp) (tagged-list? exp 'lambda))
(define (lambda-parameters exp) (cadr exp))
(define (lambda-body exp) (cddr exp))
(define (make-lambda parameters body)
(cons 'lambda (cons parameters body)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Cond
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (cond? exp) (tagged-list? exp 'cond))
(define (cond-clauses exp) (cdr exp))
(define (cond-predicate clause) (car clause))
(define (cond-actions clause) (cdr clause))
(define (cond-first-clause clauses) (car clauses))
(define (cond-rest-clauses clauses) (cdr clauses))
(define (cond-last-clause? clauses) (null? (cdr clauses)))
(define (cond-empty-clauses? clauses) (null? clauses))
; A constructor for cond clauses
(define (make-cond-clause predicate exps)
(cons predicate exps))
; A constructor for cond
(define (make-cond cond-clauses)
(cons 'cond cond-clauses))
(define (cond-else-clause? clause)
(eq? (cond-predicate clause) 'else))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Application
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Any composite expression that is not one of the above.
(define (application? exp) (list? exp))
(define (make-application operator operands)
(cons operator operands))
(define (operator exp) (car exp))
(define (operands exp) (cdr exp))
(define (no-operands? ops) (null? ops))
(define (first-operand ops) (car ops))
(define (rest-operands ops) (cdr ops))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Begin
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (begin? exp) (tagged-list? exp 'begin))
(define (begin-actions exp) (cdr exp))
(define (make-begin seq) (cons 'begin seq))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; If
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (if? exp) (tagged-list? exp 'if))
(define (if-predicate exp) (cadr exp))
(define (if-consequent exp) (caddr exp))
(define (if-alternative exp)
(if (not (null? (cdddr exp)))
(cadddr exp)
'unspecified))
(define (make-if predicate consequent alternative)
(list 'if predicate consequent alternative))
(define (make-short-if predicate consequent)
(list 'if predicate consequent))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Assignment
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (assignment? exp)
(tagged-list? exp 'set!))
(define (assignment-variable exp) (cadr exp))
(define (assignment-value exp) (caddr exp))
(define (make-assignment variable value)
(list 'set! variable value))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Let
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (let? exp) (tagged-list? exp 'let))
(define let-bindings cadr)
(define let-body cddr)
(define (let-variables exp)
(map car (let-bindings exp)))
(define (let-initial-values exp)
(map cadr (let-bindings exp)))
;bindings is a list of <symbol,exp> lists.
(define (make-let-bindings vars vals)
(map list vars vals))
(define (make-let bindings body)
(cons 'let (cons bindings body)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Letrec
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (letrec? exp)
(tagged-list? exp 'letrec))
(define letrec-bindings cadr)
(define letrec-body cddr)
(define (letrec-variables exp)
(map car (letrec-bindings exp)))
(define (letrec-values exp)
(map cadr (letrec-bindings exp)))
;bindings is a list of <symbol,exp> lists.
(define (make-letrec bindings body)
(cons 'letrec (cons bindings body)))
(define (letrec-first-variable exp)
(car (letrec-variables exp)))
(define (letrec-rest-variables exp)
(cdr (letrec-variables exp)))
(define (letrec-first-value exp)
(car (letrec-values exp)))
(define (letrec-rest-values exp)
(cdr (letrec-values exp)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Sequence
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (make-sequence exp1 exp2)
(cons exp1 exp2))
(define (sequence-last-exp? exp)
(null? (cdr exp)))
(define (sequence-first-exp exps)
(car exps))
(define (sequence-rest-exps exps)
(cdr exps))
(define (sequence-empty? exp)
(null? exp))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;; Derived expression handling ;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (derive exp)
(if (atomic? exp)
exp
(let ((mapped-derive-exp (map derive exp)))
(if (not (derived? exp))
mapped-derive-exp
(shallow-derive mapped-derive-exp)))))
(define (derived? exp)
(or (cond? exp) (function-definition? exp) (let? exp)))
(define (shallow-derive exp)
(cond ((cond? exp) (cond->if exp))
((function-definition? exp) (function-define->define exp))
((let? exp) (let->combination exp))
((letrec? exp) (letrec->combination exp))
(else "Unhandled derivision" exp)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Deriv handlers
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (cond->if exp)
(letrec ((sequence->exp (lambda (seq)
(cond ((sequence-empty? seq) seq)
((sequence-last-exp? seq) (sequence-first-exp seq))
(else (make-begin seq)))))
(expand-clauses (lambda (clauses)
(if (cond-empty-clauses? clauses)
'false ; no else clause
(let ((first (cond-first-clause clauses))
(rest (cond-rest-clauses clauses)))
(if (cond-else-clause? first)
(if (cond-empty-clauses? rest)
(sequence->exp (cond-actions first))
(error
"ELSE clause isn't last -- COND->IF"
clauses))
(make-if (cond-predicate first)
(sequence->exp (cond-actions first))
(expand-clauses rest))))))))
(expand-clauses (cond-clauses exp))))
(define (function-define->define exp)
(let ((var (function-definition-variable exp))
(params (function-definition-parameters exp))
(body (function-definition-body exp)))
(make-definition var (make-lambda params body))))
(define (let->combination exp)
(make-application (make-lambda (let-variables exp) (let-body exp))
(let-initial-values exp)))
(define (letrec->combination exp)
(letrec ((make-body (lambda (vars vals)
(if (null? vars)
(letrec-body exp)
(make-sequence
(make-assignment (car vars)
(car vals))
(make-body (cdr vars)
(cdr vals)))))))
(make-application (make-lambda (letrec-variables exp)
(make-body (letrec-variables exp)
(letrec-values exp)))
(letrec-values exp))))
Date Structures
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;; Data structures ;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Procedure representation
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (make-primitive-procedure proc)
(list 'primitive proc))
(define (primitive-implementation proc) (cadr proc))
(define (primitive-procedure? proc)
(tagged-list? proc 'primitive))
(define (make-procedure parameters body env)
(list 'procedure parameters body env))
(define (compound-procedure? p)
(tagged-list? p 'procedure))
(define (procedure-parameters p) (cadr p))
(define (procedure-body p) (caddr p))
(define (procedure-environment p) (cadddr p))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Frames
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Post-conditions: produces a pair of <variables,values> or error if (#vars != #vals)
(define (make-frame variables values)
(if (null? variables)
()
(cons variables values)))
(define (make-frame-precondition vars vals)
(= (length vars) (length vals)))
(define (frame-variables frame) (car frame))
(define (frame-values frame) (cdr frame))
(define (first-var-in-frame frame) (car (frame-variables frame)))
(define (first-val-in-frame frame) (car (frame-values frame)))
(define (rest-vars-in-frame frame) (cdr (frame-variables frame)))
(define (rest-vals-in-frame frame) (cdr (frame-values frame)))
(define empty-frame? null?)
(define (add-binding-to-frame! binding frame)
(let ((var (binding-variable binding))
(val (binding-value binding)))
(set-car! frame (cons var (car frame)))
(set-cdr! frame (cons val (cdr frame)))))
; If var was found in the frame, it is replaced, otherwise an error is thrown
(define (set-binding-in-frame! var val frame)
(letrec ((get-sub-frame (lambda (var frame)
(if (eq? var (first-var-in-frame frame))
frame
(get-sub-frame
var
(make-frame (rest-vars-in-frame frame)
(rest-vals-in-frame frame))))))
(set-frame-first-value! (lambda (frame value)
(let ((vals (frame-values frame)))
(set-car! vals value)))))
(if (empty-frame? (lookup-variable-value-in-frame var frame))
(error "The variable ,var was not found in the frame" frame)
(set-frame-first-value! (get-sub-frame var frame) val))))
(define (lookup-variable-value-in-frame var frame)
(cond ((or (empty-frame? frame)
(eq? var (first-var-in-frame frame))) frame)
(else (lookup-variable-value-in-frame
var
(make-frame (rest-vars-in-frame frame)
(rest-vals-in-frame frame))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Bindings
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (make-binding var val)
(cons var val))
(define (binding-variable binding)
(car binding))
(define (binding-value binding)
(cdr binding))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Environment
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (enclosing-env env) (cdr env))
(define (first-frame env) (car env))
(define the-empty-environment '())
(define (empty-env? env)
(eq? env the-empty-environment))
(define (extend-env frame base-env)
(cons frame base-env))
; TYPE: var*env->frame
(define (defined-in-env var env)
(if (empty-env? env)
env
(let ((f (lookup-variable-value-in-frame var (first-frame env))))
(if (empty-frame? f)
(defined-in-env var (enclosing-env env))
f))))
(define (lookup-variable-value var env)
(let ((f (defined-in-env var env)))
(if (empty-frame? f)
(error "Variable not found -- LOOKUP")
(first-val-in-frame f))))
(define (set-binding-in-env! var val env)
(let ((f (defined-in-env var env)))
(if (empty-frame? f)
(error "Variable not declared -- SET-BINDING" var env)
(set-binding-in-frame! var val f))))
(define (add-binding! binding)
(add-binding-to-frame! binding (first-frame the-global-environment)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;; Global environment construction ;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; The global environment ADT
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define primitive-procedures
(list (list 'car car)
(list 'cdr cdr)
(list 'cons cons)
(list 'null? null?)
(list '+ +)
(list '* *)
(list '/ /)
(list '> >)
(list '< <)
(list '- -)
(list '= =)
(list 'list list)
;; more primitives
))
(define the-global-environment
(extend-env (make-frame (map car primitive-procedures)
(map (lambda (x)
(make-primitive-procedure (cadr x)))
primitive-procedures))
the-empty-environment))
Core of the imperative environment interpreter
(load "env DS.scm")
(load "ASP.scm")
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;; IMP-ENV-EVALUATOR ;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (derive-eval exp)
(env-eval (derive exp) the-global-environment))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Main imperative-environment-evaluation
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Type: <EXP> * ENV --> VAL (union of Number, Symbol, Boolean, Procedure,
;;; Pair, List)
;;; Pre-conditions: The given expression is legal according to the concrete syntax,
;;; Inner
;;; 'define' expressions are not legal.
(define (env-eval exp env)
(cond ((atomic? exp) (eval-atomic exp env))
((special-form? exp) (eval-special-form exp env))
((application? exp)
(apply-procedure (env-eval (operator exp) env)
(list-of-values (operands exp) env)))
(else
(error "Unknown expression type -- EVAL" exp))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Atomic
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (eval-atomic exp env)
(if (or (number? exp) (boolean? exp) (null? exp))
exp
(lookup-variable-value exp env)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Special form handling
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (special-form? exp)
(or (quoted? exp) (lambda? exp) (assignment? exp)
(definition? exp) (if? exp) (begin? exp) ))
(define (eval-special-form exp env)
(cond ((quoted? exp) (text-of-quotation exp))
((lambda? exp) (eval-lambda exp env))
((assignment? exp) (eval-assignment exp env))
((definition? exp)
(if (not (eq? env the-global-environment))
(error "Non global definition" exp)
(eval-definition exp)))
((if? exp) (eval-if exp env))
((begin? exp) (eval-begin exp env))
))
(define (eval-lambda exp env)
(make-procedure (lambda-parameters exp)
(lambda-body exp)
env))
(define (eval-assignment exp env)
(set-binding-in-env! (assignment-variable exp)
(env-eval (assignment-value exp) env)
env)
'ok)
(define (eval-definition exp)
(add-binding! (make-binding (definition-variable exp)
(env-eval (definition-value exp)
the-global-environment)))
'ok)
(define (eval-if exp env)
(if (true? (env-eval (if-predicate exp) env))
(env-eval (if-consequent exp) env)
(env-eval (if-alternative exp) env)))
(define (eval-begin exp env)
(eval-sequence (begin-actions exp) env))
(define (eval-sequence exps env)
(cond ((sequence-last-exp? exps) (env-eval (sequence-first-exp exps) env))
(else (env-eval (sequence-first-exp exps) env)
(eval-sequence (sequence-rest-exps exps) env))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Application handling
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (apply-procedure procedure arguments)
(cond ((primitive-procedure? procedure)
(apply-primitive-procedure procedure arguments))
((compound-procedure? procedure)
(let ((parameters (procedure-parameters procedure)))
(if (make-frame-precondition parameters arguments)
(eval-sequence
(procedure-body procedure)
(extend-env
(make-frame parameters arguments)
(procedure-environment procedure)))
(error
"make-frame-precondition violation:
# of variables does not match # of values
while attempting to create a frame"))))
(else
(error
"Unknown procedure type -- APPLY" procedure))))
(define (list-of-values exps env)
(if (no-operands? exps)
'()
(cons (env-eval (first-operand exps) env)
(list-of-values (rest-operands exps) env))))
;;; The primitive procedures will be captured as data structures of
;;; the evaluator. Therefore, their implementation should be
;;; retrieved from these objects.
(define (apply-primitive-procedure proc args)
(apply (primitive-implementation proc) args))
(define (true? x)
(not (eq? x #f)))
(define (false? x)
(eq? x #f))
Core of the imperative compiler
(load "env DS.scm")
(load "ASP.scm")
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;; IMP-ENV-ANALYZER ;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (derive-analyze-eval exp)
((analyze (derive exp)) the-global-environment))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Main imperative-environment-analyzer
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Type: <EXP> --> (ENV --> VAL) (union of Number, Symbol, Boolean, Procedure,
;;; Pair, List)
;;; Pre-conditions: The given expression is legal according to the concrete syntax,
;;; Inner 'define' expressions are not legal.
(define (analyze exp)
(cond ((atomic? exp) (analyze-atomic exp))
((special-form? exp) (analyze-special-form exp))
((application? exp) (analyze-application exp))
(else
(error "Unknown expression type -- EVAL" exp))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Atomic
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (analyze-atomic exp)
(if (or (number? exp) (boolean? exp) (null? exp))
(lambda (env) exp)
(lambda (env) (lookup-variable-value exp env))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Special form handling
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (special-form? exp)
(or (quoted? exp) (lambda? exp) (assignment? exp)
(definition? exp) (if? exp) (begin? exp) ))
(define (analyze-special-form exp)
(cond ((quoted? exp) (analyze-quoted exp))
((lambda? exp) (analyze-lambda exp))
((assignment? exp) (analyze-assignment exp))
((definition? exp) (analyze-definition exp))
((if? exp) (analyze-if exp))
((begin? exp) (analyze-begin exp))
))
(define (analyze-quoted exp)
(let ((text (text-of-quotation exp)))
(lambda (env)
text)))
(define (analyze-lambda exp)
(let ((parameters (lambda-parameters exp))
(body (analyze-sequence (lambda-body exp))))
(lambda (env)
(make-procedure parameters body env))))
(define (analyze-assignment exp)
(let ((var (assignment-variable exp))
(val (analyze (assignment-value exp))))
(lambda (env)
(set-binding-in-env! var (val env) env)
'ok)))
(define (analyze-definition exp)
(let ((var (definition-variable exp))
(val (analyze (definition-value exp))))
(lambda (env)
(if (not (eq? env the-global-environment))
(error "Non global definition" exp)
(begin (add-binding! (make-binding var (val the-global-environment)))
'ok)))))
(define (analyze-if exp)
(let ((pred (analyze (if-predicate exp)))
(consequent (analyze (if-consequent exp)))
(alternative (analyze (if-alternative exp))))
(lambda (env)
(if (true? (pred env))
(consequent env)
(alternative env)))))
(define (analyze-begin exp)
(let ((actions (analyze-sequence (begin-actions exp))))
(lambda (env)
(actions env))))
(define (analyze-sequence exps)
(let ((procs (map analyze exps))
(last-in-list (lambda (lst) (car (reverse lst)))))
(if (null? procs)
(error "Empty sequence -- ANALYZE"))
(lambda (env)
(let ((vals (map (lambda (proc)(proc env)) procs)))
(last-in-list vals)))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Application handling
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (analyze-application exp)
(let ((application-operator (analyze (operator exp)))
(application-operands (map analyze (operands exp))))
(lambda (env)
(apply-procedure (application-operator env)
(map (lambda (operand) (operand env)) application-operands)))))
(define (apply-procedure procedure arguments)
(cond ((primitive-procedure? procedure)
(apply-primitive-procedure procedure arguments))
((compound-procedure? procedure)
(let ((parameters (procedure-parameters procedure)))
(if (make-frame-precondition parameters arguments)
((procedure-body procedure)
(extend-env (make-frame parameters arguments)
(procedure-environment procedure)))
(error
"make-frame-precondition violation:
# of variables does not match
# of values while attempting to create a frame"))))
(else
(error
"Unknown procedure type -- APPLY" procedure))))
;;; The primitive procedures will be captured as data structures of
;;; the evaluator. Therefore, their implementation should be
;;; retrieved from these objects.
(define (apply-primitive-procedure proc args)
(apply (primitive-implementation proc) args))
(define (true? x)
(not (eq? x #f)))
(define (false? x)
(eq? x #f))
TYPE CHECKING RULES
1. NUMBER:
For every type environment T_ENV and number n:
T_ENV |- n : NUMBER
2. BOOLEAN:
For every type environment T_ENV and boolean b:
T_ENV |- b : BOOLEAN
3. SYMBOL:
For every type environment T_ENV and symbol s:
T_ENV |- 's : SYMBOL
4. VARIABLE:
For every type environment T_ENV and variable v:
T_ENV |- v : T_ENV(v)
i.e., the assumption for 'v' is the type that T_ENV assigns to it.
5. PRIMITIVE PROCEDURE:
Every primitive procedure has its own function type.
Examples:
The '+' procedure has the type assumption: