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 text {*** 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" --"name is bound in trm1" |
12 | Lt1 "bp" "trm1" "trm1" |
12 | Lt1 "bp" "trm1" "trm1" --"all variables in bp are bound in the 2nd 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 |
21 where |
21 where |
22 "bv1 (BUnit) = {}" |
22 "bv1 (BUnit) = {}" |
23 | "bv1 (BVr x) = {x}" |
23 | "bv1 (BVr x) = {x}" |
24 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)" |
24 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)" |
25 |
25 |
26 (*** lets with single assignments ***) |
26 (* needs to be calculated by the package *) |
|
27 fun |
|
28 fv_trm1 and fv_bp |
|
29 where |
|
30 "fv_trm1 (Vr1 x) = {x}" |
|
31 | "fv_trm1 (Ap1 t1 t2) = (fv_trm1 t1) \<union> (fv_trm1 t2)" |
|
32 | "fv_trm1 (Lm1 x t) = (fv_trm1 t) - {x}" |
|
33 | "fv_trm1 (Lt1 bp t1 t2) = (fv_trm1 t1) \<union> (fv_trm1 t2 - bv1 bp)" |
|
34 | "fv_bp (BUnit) = {}" |
|
35 | "fv_bp (BVr x) = {x}" |
|
36 | "fv_bp (BPr b1 b2) = (fv_bp b1) \<union> (fv_bp b2)" |
|
37 |
|
38 text {*** lets with single assignments ***} |
27 datatype trm2 = |
39 datatype trm2 = |
28 Vr2 "name" |
40 Vr2 "name" |
29 | Ap2 "trm2" "trm2" |
41 | Ap2 "trm2" "trm2" |
30 | Lm2 "name" "trm2" |
42 | Lm2 "name" "trm2" |
31 | Lt2 "assign" "trm2" |
43 | Lt2 "assign" "trm2" |
36 fun |
48 fun |
37 bv2 |
49 bv2 |
38 where |
50 where |
39 "bv2 (As x t) = {x}" |
51 "bv2 (As x t) = {x}" |
40 |
52 |
|
53 (* needs to be calculated by the package *) |
|
54 fun |
|
55 fv_trm2 and fv_assign |
|
56 where |
|
57 "fv_trm2 (Vr2 x) = {x}" |
|
58 | "fv_trm2 (Ap2 t1 t2) = (fv_trm2 t1) \<union> (fv_trm2 t2)" |
|
59 | "fv_trm2 (Lm2 x t) = (fv_trm2 t) - {x}" |
|
60 | "fv_trm2 (Lt2 as t) = (fv_trm2 t - bv2 as) \<union> (fv_assign as)" |
|
61 | "fv_assign (As x t) = (fv_trm2 t)" |
41 |
62 |
42 (*** lets with many assignments ***) |
63 |
|
64 text {*** lets with many assignments ***} |
43 datatype trm3 = |
65 datatype trm3 = |
44 Vr3 "name" |
66 Vr3 "name" |
45 | Ap3 "trm3" "trm3" |
67 | Ap3 "trm3" "trm3" |
46 | Lm3 "name" "trm3" |
68 | Lm3 "name" "trm3" |
47 | Lt3 "assign" "trm3" |
69 | Lt3 "assigns" "trm3" |
48 and assigns = |
70 and assigns = |
49 ANil |
71 ANil |
50 | ACons "name" "trm3" "assigns" |
72 | ACons "name" "trm3" "assigns" |
51 |
73 |
52 (* to be given by the user *) |
74 (* to be given by the user *) |
54 bv3 |
76 bv3 |
55 where |
77 where |
56 "bv3 ANil = {}" |
78 "bv3 ANil = {}" |
57 | "bv3 (ACons x t as) = {x} \<union> (bv3 as)" |
79 | "bv3 (ACons x t as) = {x} \<union> (bv3 as)" |
58 |
80 |
|
81 fun |
|
82 fv_trm3 and fv_assigns |
|
83 where |
|
84 "fv_trm3 (Vr3 x) = {x}" |
|
85 | "fv_trm3 (Ap3 t1 t2) = (fv_trm3 t1) \<union> (fv_trm3 t2)" |
|
86 | "fv_trm3 (Lm3 x t) = (fv_trm3 t) - {x}" |
|
87 | "fv_trm3 (Lt3 as t) = (fv_trm3 t - bv3 as) \<union> (fv_assigns as)" |
|
88 | "fv_assigns (ANil) = {}" |
|
89 | "fv_assigns (ACons x t as) = (fv_trm3 t) \<union> (fv_assigns as)" |
|
90 |
59 end |
91 end |