author  clasohm 
Mon, 05 Feb 1996 14:44:09 +0100  
changeset 1474  3f7d67927fe2 
parent 1149  5750eba8820d 
child 2709  241fffc25284 
permissions  rwrr 
1474  1 
(* Title: CCL/terms.thy 
0  2 
ID: $Id$ 
1474  3 
Author: Martin Coen 
0  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 

998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

14 
one :: "i" 
0  15 

998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

16 
if :: "[i,i,i]=>i" ("(3if _/ then _/ else _)" [0,0,60] 60) 
0  17 

998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

18 
inl,inr :: "i=>i" 
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

19 
when :: "[i,i=>i,i=>i]=>i" 
0  20 

998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

21 
split :: "[i,[i,i]=>i]=>i" 
0  22 
fst,snd, 
998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

23 
thd :: "i=>i" 
0  24 

998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

25 
zero :: "i" 
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

26 
succ :: "i=>i" 
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

27 
ncase :: "[i,i,i=>i]=>i" 
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

28 
nrec :: "[i,i,[i,i]=>i]=>i" 
0  29 

998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

30 
nil :: "i" ("([])") 
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

31 
"$" :: "[i,i]=>i" (infixr 80) 
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

32 
lcase :: "[i,i,[i,i]=>i]=>i" 
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

33 
lrec :: "[i,i,[i,i,i]=>i]=>i" 
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

34 

91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

35 
let :: "[i,i=>i]=>i" 
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

36 
letrec :: "[[i,i=>i]=>i,(i=>i)=>i]=>i" 
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

37 
letrec2 :: "[[i,i,i=>i=>i]=>i,(i=>i=>i)=>i]=>i" 
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

38 
letrec3 :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i" 
0  39 

998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

40 
"@let" :: "[idt,i,i]=>i" ("(3let _ be _/ in _)" 
1474  41 
[0,0,60] 60) 
998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

42 

91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

43 
"@letrec" :: "[idt,idt,i,i]=>i" ("(3letrec _ _ be _/ in _)" 
1474  44 
[0,0,0,60] 60) 
0  45 

998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

46 
"@letrec2" :: "[idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ be _/ in _)" 
1474  47 
[0,0,0,0,60] 60) 
0  48 

998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

49 
"@letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)" 
1474  50 
[0,0,0,0,0,60] 60) 
998
91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

51 

91d09e262799
Gave tighter priorities to if, napply and the letforms to
lcp
parents:
610
diff
changeset

52 
napply :: "[i=>i,i,i]=>i" ("(_ ^ _ ` _)" [56,56,56] 56) 
0  53 

54 
rules 

55 

56 
one_def "one == true" 

57 
if_def "if b then t else u == case(b,t,u,% x y.bot,%v.bot)" 

58 
inl_def "inl(a) == <true,a>" 

59 
inr_def "inr(b) == <false,b>" 

60 
when_def "when(t,f,g) == split(t,%b x.if b then f(x) else g(x))" 

61 
split_def "split(t,f) == case(t,bot,bot,f,%u.bot)" 

62 
fst_def "fst(t) == split(t,%x y.x)" 

63 
snd_def "snd(t) == split(t,%x y.y)" 

64 
thd_def "thd(t) == split(t,%x p.split(p,%y z.z))" 

65 
zero_def "zero == inl(one)" 

66 
succ_def "succ(n) == inr(n)" 

67 
ncase_def "ncase(n,b,c) == when(n,%x.b,%y.c(y))" 

68 
nrec_def " nrec(n,b,c) == letrec g x be ncase(x,b,%y.c(y,g(y))) in g(n)" 

1474  69 
nil_def "[] == inl(one)" 
289  70 
cons_def "h$t == inr(<h,t>)" 
0  71 
lcase_def "lcase(l,b,c) == when(l,%x.b,%y.split(y,c))" 
72 
lrec_def "lrec(l,b,c) == letrec g x be lcase(x,b,%h t.c(h,t,g(t))) in g(l)" 

73 

74 
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)))" 

75 
letrec_def 

76 
"letrec g x be h(x,g) in b(g) == b(%x.fix(%f.lam x.h(x,%y.f`y))`x)" 

77 

1149  78 
letrec2_def "letrec g x y be h(x,y,g) in f(g)== 
79 
letrec g' p be split(p,%x y.h(x,y,%u v.g'(<u,v>))) 

80 
in f(%x y.g'(<x,y>))" 

0  81 

1149  82 
letrec3_def "letrec g x y z be h(x,y,z,g) in f(g) == 
83 
letrec g' p be split(p,%x xs.split(xs,%y z.h(x,y,z,%u v w.g'(<u,<v,w>>)))) 

84 
in f(%x y z.g'(<x,<y,z>>))" 

0  85 

86 
napply_def "f ^n` a == nrec(n,a,%x g.f(g))" 

87 

88 
end 

89 

90 
ML 

91 

92 
(** Quantifier translations: variable binding **) 

93 

94 
fun let_tr [Free(id,T),a,b] = Const("let",dummyT) $ a $ absfree(id,T,b); 

95 
fun let_tr' [a,Abs(id,T,b)] = 

96 
let val (id',b') = variant_abs(id,T,b) 

97 
in Const("@let",dummyT) $ Free(id',T) $ a $ b' end; 

98 

99 
fun letrec_tr [Free(f,S),Free(x,T),a,b] = 

100 
Const("letrec",dummyT) $ absfree(x,T,absfree(f,S,a)) $ absfree(f,S,b); 

101 
fun letrec2_tr [Free(f,S),Free(x,T),Free(y,U),a,b] = 

102 
Const("letrec2",dummyT) $ absfree(x,T,absfree(y,U,absfree(f,S,a))) $ absfree(f,S,b); 

103 
fun letrec3_tr [Free(f,S),Free(x,T),Free(y,U),Free(z,V),a,b] = 

104 
Const("letrec3",dummyT) $ absfree(x,T,absfree(y,U,absfree(z,U,absfree(f,S,a)))) $ absfree(f,S,b); 

105 

106 
fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] = 

107 
let val (f',b') = variant_abs(ff,SS,b) 

108 
val (_,a'') = variant_abs(f,S,a) 

109 
val (x',a') = variant_abs(x,T,a'') 

110 
in Const("@letrec",dummyT) $ Free(f',SS) $ Free(x',T) $ a' $ b' end; 

111 
fun letrec2_tr' [Abs(x,T,Abs(y,U,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 (y',a2) = variant_abs(y,U,a1) 

115 
val (x',a') = variant_abs(x,T,a2) 

116 
in Const("@letrec2",dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ a' $ b' 

117 
end; 

118 
fun letrec3_tr' [Abs(x,T,Abs(y,U,Abs(z,V,Abs(f,S,a)))),Abs(ff,SS,b)] = 

119 
let val (f',b') = variant_abs(ff,SS,b) 

120 
val ( _,a1) = variant_abs(f,S,a) 

121 
val (z',a2) = variant_abs(z,V,a1) 

122 
val (y',a3) = variant_abs(y,U,a2) 

123 
val (x',a') = variant_abs(x,T,a3) 

124 
in Const("@letrec3",dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b' 

125 
end; 

126 

127 
val parse_translation= 

128 
[("@let", let_tr), 

129 
("@letrec", letrec_tr), 

130 
("@letrec2", letrec2_tr), 

131 
("@letrec3", letrec3_tr) 

132 
]; 

133 
val print_translation= 

134 
[("let", let_tr'), 

135 
("letrec", letrec_tr'), 

136 
("letrec2", letrec2_tr'), 

137 
("letrec3", letrec3_tr') 

138 
]; 