38 letrec :: "[[i,i=>i]=>i,(i=>i)=>i]=>i" |
38 letrec :: "[[i,i=>i]=>i,(i=>i)=>i]=>i" |
39 letrec2 :: "[[i,i,i=>i=>i]=>i,(i=>i=>i)=>i]=>i" |
39 letrec2 :: "[[i,i,i=>i=>i]=>i,(i=>i=>i)=>i]=>i" |
40 letrec3 :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i" |
40 letrec3 :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i" |
41 |
41 |
42 syntax |
42 syntax |
43 "@let" :: "[idt,i,i]=>i" ("(3let _ be _/ in _)" |
43 "_let" :: "[idt,i,i]=>i" ("(3let _ be _/ in _)" |
44 [0,0,60] 60) |
44 [0,0,60] 60) |
45 |
45 |
46 "@letrec" :: "[idt,idt,i,i]=>i" ("(3letrec _ _ be _/ in _)" |
46 "_letrec" :: "[idt,idt,i,i]=>i" ("(3letrec _ _ be _/ in _)" |
47 [0,0,0,60] 60) |
47 [0,0,0,60] 60) |
48 |
48 |
49 "@letrec2" :: "[idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ be _/ in _)" |
49 "_letrec2" :: "[idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ be _/ in _)" |
50 [0,0,0,0,60] 60) |
50 [0,0,0,0,60] 60) |
51 |
51 |
52 "@letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)" |
52 "_letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)" |
53 [0,0,0,0,0,60] 60) |
53 [0,0,0,0,0,60] 60) |
54 |
54 |
55 ML {* |
55 ML {* |
56 (** Quantifier translations: variable binding **) |
56 (** Quantifier translations: variable binding **) |
57 |
57 |
58 (* FIXME does not handle "_idtdummy" *) |
58 (* FIXME does not handle "_idtdummy" *) |
59 (* FIXME should use Syntax.mark_bound(T), Syntax.variant_abs' *) |
59 (* FIXME should use Syntax.mark_bound(T), Syntax.variant_abs' *) |
60 |
60 |
61 fun let_tr [Free(id,T),a,b] = Const("let",dummyT) $ a $ absfree(id,T,b); |
61 fun let_tr [Free(id,T),a,b] = Const(@{const_syntax let},dummyT) $ a $ absfree(id,T,b); |
62 fun let_tr' [a,Abs(id,T,b)] = |
62 fun let_tr' [a,Abs(id,T,b)] = |
63 let val (id',b') = variant_abs(id,T,b) |
63 let val (id',b') = variant_abs(id,T,b) |
64 in Const("@let",dummyT) $ Free(id',T) $ a $ b' end; |
64 in Const(@{syntax_const "_let"},dummyT) $ Free(id',T) $ a $ b' end; |
65 |
65 |
66 fun letrec_tr [Free(f,S),Free(x,T),a,b] = |
66 fun letrec_tr [Free(f,S),Free(x,T),a,b] = |
67 Const("letrec",dummyT) $ absfree(x,T,absfree(f,S,a)) $ absfree(f,S,b); |
67 Const(@{const_syntax letrec},dummyT) $ absfree(x,T,absfree(f,S,a)) $ absfree(f,S,b); |
68 fun letrec2_tr [Free(f,S),Free(x,T),Free(y,U),a,b] = |
68 fun letrec2_tr [Free(f,S),Free(x,T),Free(y,U),a,b] = |
69 Const("letrec2",dummyT) $ absfree(x,T,absfree(y,U,absfree(f,S,a))) $ absfree(f,S,b); |
69 Const(@{const_syntax letrec2},dummyT) $ absfree(x,T,absfree(y,U,absfree(f,S,a))) $ absfree(f,S,b); |
70 fun letrec3_tr [Free(f,S),Free(x,T),Free(y,U),Free(z,V),a,b] = |
70 fun letrec3_tr [Free(f,S),Free(x,T),Free(y,U),Free(z,V),a,b] = |
71 Const("letrec3",dummyT) $ absfree(x,T,absfree(y,U,absfree(z,U,absfree(f,S,a)))) $ absfree(f,S,b); |
71 Const(@{const_syntax letrec3},dummyT) $ |
|
72 absfree(x,T,absfree(y,U,absfree(z,U,absfree(f,S,a)))) $ absfree(f,S,b); |
72 |
73 |
73 fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] = |
74 fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] = |
74 let val (f',b') = variant_abs(ff,SS,b) |
75 let val (f',b') = variant_abs(ff,SS,b) |
75 val (_,a'') = variant_abs(f,S,a) |
76 val (_,a'') = variant_abs(f,S,a) |
76 val (x',a') = variant_abs(x,T,a'') |
77 val (x',a') = variant_abs(x,T,a'') |
77 in Const("@letrec",dummyT) $ Free(f',SS) $ Free(x',T) $ a' $ b' end; |
78 in Const(@{syntax_const "_letrec"},dummyT) $ Free(f',SS) $ Free(x',T) $ a' $ b' end; |
78 fun letrec2_tr' [Abs(x,T,Abs(y,U,Abs(f,S,a))),Abs(ff,SS,b)] = |
79 fun letrec2_tr' [Abs(x,T,Abs(y,U,Abs(f,S,a))),Abs(ff,SS,b)] = |
79 let val (f',b') = variant_abs(ff,SS,b) |
80 let val (f',b') = variant_abs(ff,SS,b) |
80 val ( _,a1) = variant_abs(f,S,a) |
81 val ( _,a1) = variant_abs(f,S,a) |
81 val (y',a2) = variant_abs(y,U,a1) |
82 val (y',a2) = variant_abs(y,U,a1) |
82 val (x',a') = variant_abs(x,T,a2) |
83 val (x',a') = variant_abs(x,T,a2) |
83 in Const("@letrec2",dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ a' $ b' |
84 in Const(@{syntax_const "_letrec2"},dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ a' $ b' |
84 end; |
85 end; |
85 fun letrec3_tr' [Abs(x,T,Abs(y,U,Abs(z,V,Abs(f,S,a)))),Abs(ff,SS,b)] = |
86 fun letrec3_tr' [Abs(x,T,Abs(y,U,Abs(z,V,Abs(f,S,a)))),Abs(ff,SS,b)] = |
86 let val (f',b') = variant_abs(ff,SS,b) |
87 let val (f',b') = variant_abs(ff,SS,b) |
87 val ( _,a1) = variant_abs(f,S,a) |
88 val ( _,a1) = variant_abs(f,S,a) |
88 val (z',a2) = variant_abs(z,V,a1) |
89 val (z',a2) = variant_abs(z,V,a1) |
89 val (y',a3) = variant_abs(y,U,a2) |
90 val (y',a3) = variant_abs(y,U,a2) |
90 val (x',a') = variant_abs(x,T,a3) |
91 val (x',a') = variant_abs(x,T,a3) |
91 in Const("@letrec3",dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b' |
92 in Const(@{syntax_const "_letrec3"},dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b' |
92 end; |
93 end; |
93 |
94 |
94 *} |
95 *} |
95 |
96 |
96 parse_translation {* |
97 parse_translation {* |
97 [("@let", let_tr), |
98 [(@{syntax_const "_let"}, let_tr), |
98 ("@letrec", letrec_tr), |
99 (@{syntax_const "_letrec"}, letrec_tr), |
99 ("@letrec2", letrec2_tr), |
100 (@{syntax_const "_letrec2"}, letrec2_tr), |
100 ("@letrec3", letrec3_tr)] *} |
101 (@{syntax_const "_letrec3"}, letrec3_tr)] |
|
102 *} |
101 |
103 |
102 print_translation {* |
104 print_translation {* |
103 [("let", let_tr'), |
105 [(@{const_syntax let}, let_tr'), |
104 ("letrec", letrec_tr'), |
106 (@{const_syntax letrec}, letrec_tr'), |
105 ("letrec2", letrec2_tr'), |
107 (@{const_syntax letrec2}, letrec2_tr'), |
106 ("letrec3", letrec3_tr')] *} |
108 (@{const_syntax letrec3}, letrec3_tr')] |
|
109 *} |
107 |
110 |
108 consts |
111 consts |
109 napply :: "[i=>i,i,i]=>i" ("(_ ^ _ ` _)" [56,56,56] 56) |
112 napply :: "[i=>i,i,i]=>i" ("(_ ^ _ ` _)" [56,56,56] 56) |
110 |
113 |
111 axioms |
114 axioms |