| Program | ::= |
Definition … Expression | a-program (defns exp1) |
| Definition | ::= |
define Identifier = proc (
Identifier … ) Expression |
proc-definition (id bvars body) |
| Expression | ::= |
Number | const-exp (num) |
::= |
Identifier | var-exp (var) |
|
::= |
Binop(Expression
, Expression) |
binop-exp (op exp1 exp2) |
|
::= |
if Expression
then Expression
else Expression |
if-exp (exp1 exp2 exp3) |
|
::= |
(Expression
Expression …
) |
call-exp (rator rands) |
|
| Binop | ::= |
+ |
op-plus () |
::= |
- |
op-minus () |
|
::= |
* |
op-times () |
|
::= |
< |
op-less() |
|
::= |
= |
op-equal () |
|
::= |
> |
op-greater () |
tenv0 = [true : bool, false : bool, x : int]
dom(tenv) = dom(tenv0) ∪ { f1, …, fn }
tenv(f1) = (τ11 × … × τk1 → τ1)
…
tenv(fn) = (τ1n × … × τkn → τn)
(type-of body1 [x11:τ11, …, xk1:τk1]tenv) = τ1
…
(type-of bodyn [x1n:τ1n, …, xkn:τkn]tenv) = τn
(type-of exp tenv) = τ
----------------------------------------------------------------
(type-of «define f1 = proc (x11 … xk1) body1
…
define fn = proc (x1n … xkn) bodyn
exp»
tenv)
= τ
(type-of (const-exp num) tenv) = int
(type-of (var-exp var) tenv) = tenv(var)
op : (τ1 × τ2 → τ)
(type-of exp1 tenv) = τ1
(type-of exp2 tenv) = τ2
----------------------------------------------------------------
(type-of (binop-exp op exp1 exp2) tenv) = τ
(type-of exp1 tenv) = bool
(type-of exp2 tenv) = τ
(type-of exp3 tenv) = τ
--------------------------------------------------------------------
(type-of (if-exp exp1 exp2 exp3) tenv) = τ
(type-of exp0 tenv) = (τ1 × … × τn → τ)
(type-of exp1 tenv) = τ1
…
(type-of expn tenv) = τn
----------------------------------------------------------------
(type-of (call-exp exp0 [exp1 … expn]) tenv) = τ
+ : (int × int → int) - : (int × int → int) * : (int × int → int) < : (int × int → bool) = : (int × int → bool) > : (int × int → bool)
define search = proc (x f i j)
if >(i,j)
then -1
else if =(x,(f i))
then i
else (search x f +(i,1) j)
define g = proc (square x a b c)
+(*(a,(square x)),+(*(b,x),c))
define square = proc (x) *(x,x)
define h = proc (x) (g square x 5 -13 7)
(search 1231 h 0 25)
Last updated 23 April 2008.