4 Copyright 1995 University of Cambridge |
4 Copyright 1995 University of Cambridge |
5 *) |
5 *) |
6 |
6 |
7 Language ="Datatype" + QUniv + |
7 Language ="Datatype" + QUniv + |
8 |
8 |
9 (* Abstract type of constants *) |
9 consts |
|
10 Const :: "i" (* Abstract type of constants *) |
|
11 c_app :: "[i,i] => i" (*Abstract constructor for fun application*) |
|
12 |
|
13 rules |
|
14 constNEE "c:Const ==> c ~= 0" |
|
15 c_appI "[| c1:Const; c2:Const |] ==> c_app(c1,c2):Const" |
|
16 |
10 |
17 |
11 consts |
18 consts |
12 Const :: "i" |
19 Exp :: "i" (* Datatype of expressions *) |
13 rules |
20 ExVar :: "i" (* Abstract type of variables *) |
14 constU "c:Const ==> c:univ(A)" |
21 datatype <= "univ(Const Un ExVar)" |
15 constNEE "c:Const ==> c ~= 0" |
22 "Exp" = e_const("c:Const") |
16 |
23 | e_var("x:ExVar") |
17 (* A function that captures how constant functions are applied to |
24 | e_fn("x:ExVar","e:Exp") |
18 constants *) |
25 | e_fix("x1:ExVar","x2:ExVar","e:Exp") |
19 |
26 | e_app("e1:Exp","e2:Exp") |
20 consts |
|
21 c_app :: "[i,i] => i" |
|
22 rules |
|
23 c_appI "[| c1:Const; c2:Const |] ==> c_app(c1,c2):Const" |
|
24 |
|
25 |
|
26 (* Abstract type of variables *) |
|
27 |
|
28 consts |
|
29 ExVar :: "i" |
|
30 rules |
|
31 exvarU "x:ExVar ==> x:univ(A)" |
|
32 |
|
33 |
|
34 (* Datatype of expressions *) |
|
35 |
|
36 consts |
|
37 Exp :: "i" |
|
38 datatype |
|
39 "Exp" = |
|
40 e_const("c:Const") | |
|
41 e_var("x:ExVar") | |
|
42 e_fn("x:ExVar","e:Exp") | |
|
43 e_fix("x1:ExVar","x2:ExVar","e:Exp") | |
|
44 e_app("e1:Exp","e2:Exp") |
|
45 type_intrs "[constU,exvarU]" |
|
46 |
27 |
47 end |
28 end |
48 |
|
49 |
|
50 |
|
51 |
|