15 aexp :: i |
15 aexp :: i |
16 |
16 |
17 datatype <= "univ(loc Un (nat->nat) Un ((nat*nat) -> nat) )" |
17 datatype <= "univ(loc Un (nat->nat) Un ((nat*nat) -> nat) )" |
18 "aexp" = N ("n: nat") |
18 "aexp" = N ("n: nat") |
19 | X ("x: loc") |
19 | X ("x: loc") |
20 | Op1 ("f: nat -> nat", "a : aexp") |
20 | Op1 ("f : nat -> nat", "a : aexp") |
21 | Op2 ("f: (nat*nat) -> nat", "a0 : aexp", "a1 : aexp") |
21 | Op2 ("f : (nat*nat) -> nat", "a0 : aexp", "a1 : aexp") |
22 |
22 |
23 |
23 |
24 (** Evaluation of arithmetic expressions **) |
24 (** Evaluation of arithmetic expressions **) |
25 consts evala :: i |
25 consts evala :: i |
26 "@evala" :: [i,i,i] => o ("<_,_>/ -a-> _" [0,0,50] 50) |
26 "@evala" :: [i,i,i] => o ("<_,_>/ -a-> _" [0,0,50] 50) |
27 translations |
27 translations |
28 "<ae,sig> -a-> n" == "<ae,sig,n> : evala" |
28 "<ae,sig> -a-> n" == "<ae,sig,n> : evala" |
29 inductive |
29 inductive |
30 domains "evala" <= "aexp * (loc -> nat) * nat" |
30 domains "evala" <= "aexp * (loc -> nat) * nat" |
31 intrs |
31 intrs |
32 N "[| n:nat ; sigma:loc->nat |] ==> <N(n),sigma> -a-> n" |
32 N "[| n:nat; sigma:loc->nat |] ==> <N(n),sigma> -a-> n" |
33 X "[| x:loc; sigma:loc->nat |] ==> <X(x),sigma> -a-> sigma`x" |
33 X "[| x:loc; sigma:loc->nat |] ==> <X(x),sigma> -a-> sigma`x" |
34 Op1 "[| <e,sigma> -a-> n; f: nat -> nat |] ==> <Op1(f,e),sigma> -a-> f`n" |
34 Op1 "[| <e,sigma> -a-> n; f: nat -> nat |] ==> <Op1(f,e),sigma> -a-> f`n" |
35 Op2 "[| <e0,sigma> -a-> n0; <e1,sigma> -a-> n1; f: (nat*nat) -> nat |] |
35 Op2 "[| <e0,sigma> -a-> n0; <e1,sigma> -a-> n1; f: (nat*nat) -> nat |] |
36 ==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>" |
36 ==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>" |
37 |
37 |
42 consts bexp :: i |
42 consts bexp :: i |
43 |
43 |
44 datatype <= "univ(aexp Un ((nat*nat)->bool) )" |
44 datatype <= "univ(aexp Un ((nat*nat)->bool) )" |
45 "bexp" = true |
45 "bexp" = true |
46 | false |
46 | false |
47 | ROp ("f: (nat*nat)->bool", "a0 : aexp", "a1 : aexp") |
47 | ROp ("f : (nat*nat)->bool", "a0 : aexp", "a1 : aexp") |
48 | noti ("b : bexp") |
48 | noti ("b : bexp") |
49 | andi ("b0 : bexp", "b1 : bexp") (infixl 60) |
49 | andi ("b0 : bexp", "b1 : bexp") (infixl 60) |
50 | ori ("b0 : bexp", "b1 : bexp") (infixl 60) |
50 | ori ("b0 : bexp", "b1 : bexp") (infixl 60) |
51 |
51 |
52 |
52 |