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 "-a->" :: [i,i] => o (infixl 50) |
27 translations |
27 translations |
28 "<ae,sig> -a-> n" == "<ae,sig,n> : evala" |
28 "p -a-> n" == "<p,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 |] |
50 | ori ("b0 : bexp", "b1 : bexp") (infixl 60) |
50 | ori ("b0 : bexp", "b1 : bexp") (infixl 60) |
51 |
51 |
52 |
52 |
53 (** Evaluation of boolean expressions **) |
53 (** Evaluation of boolean expressions **) |
54 consts evalb :: i |
54 consts evalb :: i |
55 "@evalb" :: [i,i,i] => o ("<_,_>/ -b-> _" [0,0,50] 50) |
55 "-b->" :: [i,i] => o (infixl 50) |
56 |
56 |
57 translations |
57 translations |
58 "<be,sig> -b-> b" == "<be,sig,b> : evalb" |
58 "p -b-> b" == "<p,b> : evalb" |
59 |
59 |
60 inductive |
60 inductive |
61 domains "evalb" <= "bexp * (loc -> nat) * bool" |
61 domains "evalb" <= "(bexp * (loc -> nat)) * bool" |
62 intrs (*avoid clash with ML constructors true, false*) |
62 intrs (*avoid clash with ML constructors true, false*) |
63 tru "[| sigma:loc -> nat |] ==> <true,sigma> -b-> 1" |
63 tru "[| sigma:loc -> nat |] ==> <true,sigma> -b-> 1" |
64 fls "[| sigma:loc -> nat |] ==> <false,sigma> -b-> 0" |
64 fls "[| sigma:loc -> nat |] ==> <false,sigma> -b-> 0" |
65 ROp "[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f: (nat*nat)->bool |] |
65 ROp "[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f: (nat*nat)->bool |] |
66 ==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> " |
66 ==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> " |
88 (*Constructor ";" has low precedence to avoid syntactic ambiguities |
88 (*Constructor ";" has low precedence to avoid syntactic ambiguities |
89 with [| m: nat; x: loc; ... |] ==> ... It usually will need parentheses.*) |
89 with [| m: nat; x: loc; ... |] ==> ... It usually will need parentheses.*) |
90 |
90 |
91 (** Execution of commands **) |
91 (** Execution of commands **) |
92 consts evalc :: i |
92 consts evalc :: i |
93 "@evalc" :: [i,i,i] => o ("<_,_>/ -c-> _" [0,0,50] 50) |
93 "-c->" :: [i,i] => o (infixl 50) |
94 "assign" :: [i,i,i] => i ("_[_'/_]" [95,0,0] 95) |
94 "assign" :: [i,i,i] => i ("_[_'/_]" [95,0,0] 95) |
95 |
95 |
96 translations |
96 translations |
97 "<ce,sig> -c-> s" == "<ce,sig,s> : evalc" |
97 "p -c-> s" == "<p,s> : evalc" |
98 |
98 |
99 defs |
99 defs |
100 assign_def "sigma[m/x] == lam y:loc. if(y=x,m,sigma`y)" |
100 assign_def "sigma[m/x] == lam y:loc. if(y=x,m,sigma`y)" |
101 |
101 |
102 inductive |
102 inductive |
103 domains "evalc" <= "com * (loc -> nat) * (loc -> nat)" |
103 domains "evalc" <= "(com * (loc -> nat)) * (loc -> nat)" |
104 intrs |
104 intrs |
105 skip "[| sigma: loc -> nat |] ==> <skip,sigma> -c-> sigma" |
105 skip "[| sigma: loc -> nat |] ==> <skip,sigma> -c-> sigma" |
106 |
106 |
107 assign "[| m: nat; x: loc; <a,sigma> -a-> m |] ==> |
107 assign "[| m: nat; x: loc; <a,sigma> -a-> m |] ==> |
108 <x := a,sigma> -c-> sigma[m/x]" |
108 <x := a,sigma> -c-> sigma[m/x]" |