equal
deleted
inserted
replaced
2 imports Nominal "../QuotMain" "../QuotList" |
2 imports Nominal "../QuotMain" "../QuotList" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 (* lets with binding patterns *) |
7 (*** lets with binding patterns ***) |
8 datatype trm1 = |
8 datatype trm1 = |
9 Vr1 "name" |
9 Vr1 "name" |
10 | Ap1 "trm1" "trm1" |
10 | Ap1 "trm1" "trm1" |
11 | Lm1 "name" "trm1" |
11 | Lm1 "name" "trm1" |
12 | Lt1 "bp" "trm1" "trm1" |
12 | Lt1 "bp" "trm1" "trm1" |
13 and bp = |
13 and bp = |
14 BUnit |
14 BUnit |
15 | BVr "name" |
15 | BVr "name" |
16 | BPr "bp" "bp" |
16 | BPr "bp" "bp" |
17 |
17 |
18 (* lets with single assignments *) |
18 (* to be given by the user *) |
|
19 fun |
|
20 bv1 |
|
21 where |
|
22 "bv1 (BUnit) = {}" |
|
23 | "bv1 (BVr x) = {x}" |
|
24 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)" |
|
25 |
|
26 (*** lets with single assignments ***) |
19 datatype trm2 = |
27 datatype trm2 = |
20 Vr2 "name" |
28 Vr2 "name" |
21 | Ap2 "trm2" "trm2" |
29 | Ap2 "trm2" "trm2" |
22 | Lm2 "name" "trm2" |
30 | Lm2 "name" "trm2" |
23 | Lt2 "assign" "trm2" |
31 | Lt2 "assign" "trm2" |
24 and assign = |
32 and assign = |
25 As "name" "trm2" |
33 As "name" "trm2" |
26 |
34 |
|
35 (* to be given by the user *) |
|
36 fun |
|
37 bv2 |
|
38 where |
|
39 "bv2 (As x t) = {x}" |
27 |
40 |
28 (* lets with many assignments *) |
41 |
|
42 (*** lets with many assignments ***) |
29 datatype trm3 = |
43 datatype trm3 = |
30 Vr3 "name" |
44 Vr3 "name" |
31 | Ap3 "trm3" "trm3" |
45 | Ap3 "trm3" "trm3" |
32 | Lm3 "name" "trm3" |
46 | Lm3 "name" "trm3" |
33 | Lt3 "assign" "trm3" |
47 | Lt3 "assign" "trm3" |
34 and assigns = |
48 and assigns = |
35 ANil |
49 ANil |
36 | ACons "name" "trm3" "assigns" |
50 | ACons "name" "trm3" "assigns" |
37 |
51 |
|
52 (* to be given by the user *) |
|
53 fun |
|
54 bv3 |
|
55 where |
|
56 "bv3 ANil = {}" |
|
57 | "bv3 (ACons x t as) = {x} \<union> (bv3 as)" |
|
58 |
|
59 end |