1 (* Title: CCL/terms.thy |
|
2 ID: $Id$ |
|
3 Author: Martin Coen |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 Definitions of usual program constructs in CCL. |
|
7 |
|
8 *) |
|
9 |
|
10 Term = CCL + |
|
11 |
|
12 consts |
|
13 |
|
14 one :: "i" |
|
15 |
|
16 if :: "[i,i,i]=>i" ("(3if _/ then _/ else _)" [] 60) |
|
17 |
|
18 inl,inr :: "i=>i" |
|
19 when :: "[i,i=>i,i=>i]=>i" |
|
20 |
|
21 split :: "[i,[i,i]=>i]=>i" |
|
22 fst,snd, |
|
23 thd :: "i=>i" |
|
24 |
|
25 zero :: "i" |
|
26 succ :: "i=>i" |
|
27 ncase :: "[i,i,i=>i]=>i" |
|
28 nrec :: "[i,i,[i,i]=>i]=>i" |
|
29 |
|
30 nil :: "i" ("([])") |
|
31 "$" :: "[i,i]=>i" (infixr 80) |
|
32 lcase :: "[i,i,[i,i]=>i]=>i" |
|
33 lrec :: "[i,i,[i,i,i]=>i]=>i" |
|
34 |
|
35 let :: "[i,i=>i]=>i" |
|
36 letrec :: "[[i,i=>i]=>i,(i=>i)=>i]=>i" |
|
37 letrec2 :: "[[i,i,i=>i=>i]=>i,(i=>i=>i)=>i]=>i" |
|
38 letrec3 :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i" |
|
39 |
|
40 "@let" :: "[id,i,i]=>i" ("(3let _ be _/ in _)" [] 60) |
|
41 "@letrec" :: "[id,id,i,i]=>i" ("(3letrec _ _ be _/ in _)" [] 60) |
|
42 "@letrec2" :: "[id,id,id,i,i]=>i" ("(3letrec _ _ _ be _/ in _)" [] 60) |
|
43 "@letrec3" :: "[id,id,id,id,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)" [] 60) |
|
44 |
|
45 napply :: "[i=>i,i,i]=>i" ("(_ ^ _ ` _)") |
|
46 |
|
47 rules |
|
48 |
|
49 one_def "one == true" |
|
50 if_def "if b then t else u == case(b,t,u,% x y.bot,%v.bot)" |
|
51 inl_def "inl(a) == <true,a>" |
|
52 inr_def "inr(b) == <false,b>" |
|
53 when_def "when(t,f,g) == split(t,%b x.if b then f(x) else g(x))" |
|
54 split_def "split(t,f) == case(t,bot,bot,f,%u.bot)" |
|
55 fst_def "fst(t) == split(t,%x y.x)" |
|
56 snd_def "snd(t) == split(t,%x y.y)" |
|
57 thd_def "thd(t) == split(t,%x p.split(p,%y z.z))" |
|
58 zero_def "zero == inl(one)" |
|
59 succ_def "succ(n) == inr(n)" |
|
60 ncase_def "ncase(n,b,c) == when(n,%x.b,%y.c(y))" |
|
61 nrec_def " nrec(n,b,c) == letrec g x be ncase(x,b,%y.c(y,g(y))) in g(n)" |
|
62 nil_def "[] == inl(one)" |
|
63 cons_def "h$t == inr(<h,t>)" |
|
64 lcase_def "lcase(l,b,c) == when(l,%x.b,%y.split(y,c))" |
|
65 lrec_def "lrec(l,b,c) == letrec g x be lcase(x,b,%h t.c(h,t,g(t))) in g(l)" |
|
66 |
|
67 let_def "let x be t in f(x) == case(t,f(true),f(false),%x y.f(<x,y>),%u.f(lam x.u(x)))" |
|
68 letrec_def |
|
69 "letrec g x be h(x,g) in b(g) == b(%x.fix(%f.lam x.h(x,%y.f`y))`x)" |
|
70 |
|
71 letrec2_def "letrec g x y be h(x,y,g) in f(g)== \ |
|
72 \ letrec g' p be split(p,%x y.h(x,y,%u v.g'(<u,v>))) \ |
|
73 \ in f(%x y.g'(<x,y>))" |
|
74 |
|
75 letrec3_def "letrec g x y z be h(x,y,z,g) in f(g) == \ |
|
76 \ letrec g' p be split(p,%x xs.split(xs,%y z.h(x,y,z,%u v w.g'(<u,<v,w>>)))) \ |
|
77 \ in f(%x y z.g'(<x,<y,z>>))" |
|
78 |
|
79 napply_def "f ^n` a == nrec(n,a,%x g.f(g))" |
|
80 |
|
81 end |
|
82 |
|
83 ML |
|
84 |
|
85 (** Quantifier translations: variable binding **) |
|
86 |
|
87 fun let_tr [Free(id,T),a,b] = Const("let",dummyT) $ a $ absfree(id,T,b); |
|
88 fun let_tr' [a,Abs(id,T,b)] = |
|
89 let val (id',b') = variant_abs(id,T,b) |
|
90 in Const("@let",dummyT) $ Free(id',T) $ a $ b' end; |
|
91 |
|
92 fun letrec_tr [Free(f,S),Free(x,T),a,b] = |
|
93 Const("letrec",dummyT) $ absfree(x,T,absfree(f,S,a)) $ absfree(f,S,b); |
|
94 fun letrec2_tr [Free(f,S),Free(x,T),Free(y,U),a,b] = |
|
95 Const("letrec2",dummyT) $ absfree(x,T,absfree(y,U,absfree(f,S,a))) $ absfree(f,S,b); |
|
96 fun letrec3_tr [Free(f,S),Free(x,T),Free(y,U),Free(z,V),a,b] = |
|
97 Const("letrec3",dummyT) $ absfree(x,T,absfree(y,U,absfree(z,U,absfree(f,S,a)))) $ absfree(f,S,b); |
|
98 |
|
99 fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] = |
|
100 let val (f',b') = variant_abs(ff,SS,b) |
|
101 val (_,a'') = variant_abs(f,S,a) |
|
102 val (x',a') = variant_abs(x,T,a'') |
|
103 in Const("@letrec",dummyT) $ Free(f',SS) $ Free(x',T) $ a' $ b' end; |
|
104 fun letrec2_tr' [Abs(x,T,Abs(y,U,Abs(f,S,a))),Abs(ff,SS,b)] = |
|
105 let val (f',b') = variant_abs(ff,SS,b) |
|
106 val ( _,a1) = variant_abs(f,S,a) |
|
107 val (y',a2) = variant_abs(y,U,a1) |
|
108 val (x',a') = variant_abs(x,T,a2) |
|
109 in Const("@letrec2",dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ a' $ b' |
|
110 end; |
|
111 fun letrec3_tr' [Abs(x,T,Abs(y,U,Abs(z,V,Abs(f,S,a)))),Abs(ff,SS,b)] = |
|
112 let val (f',b') = variant_abs(ff,SS,b) |
|
113 val ( _,a1) = variant_abs(f,S,a) |
|
114 val (z',a2) = variant_abs(z,V,a1) |
|
115 val (y',a3) = variant_abs(y,U,a2) |
|
116 val (x',a') = variant_abs(x,T,a3) |
|
117 in Const("@letrec3",dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b' |
|
118 end; |
|
119 |
|
120 val parse_translation= |
|
121 [("@let", let_tr), |
|
122 ("@letrec", letrec_tr), |
|
123 ("@letrec2", letrec2_tr), |
|
124 ("@letrec3", letrec3_tr) |
|
125 ]; |
|
126 val print_translation= |
|
127 [("let", let_tr'), |
|
128 ("letrec", letrec_tr'), |
|
129 ("letrec2", letrec2_tr'), |
|
130 ("letrec3", letrec3_tr') |
|
131 ]; |
|