58 sequence_name = "seq'=>seq'" |
57 sequence_name = "seq'=>seq'" |
59 |
58 |
60 |
59 |
61 syntax |
60 syntax |
62 (*Constant to allow definitions of SEQUENCES of formulas*) |
61 (*Constant to allow definitions of SEQUENCES of formulas*) |
63 "@Side" :: "seq=>(seq'=>seq')" ("<<(_)>>") |
62 "_Side" :: "seq=>(seq'=>seq')" ("<<(_)>>") |
64 |
63 |
65 ML {* |
64 ML {* |
66 |
65 |
67 (* parse translation for sequences *) |
66 (* parse translation for sequences *) |
68 |
67 |
69 fun abs_seq' t = Abs("s", Type("seq'",[]), t); |
68 fun abs_seq' t = Abs ("s", Type ("seq'", []), t); (* FIXME @{type_syntax} *) |
70 |
69 |
71 fun seqobj_tr(Const("SeqO",_) $ f) = Const("SeqO'",dummyT) $ f | |
70 fun seqobj_tr (Const (@{syntax_const "_SeqO"}, _) $ f) = |
72 seqobj_tr(_ $ i) = i; |
71 Const (@{const_syntax SeqO'}, dummyT) $ f |
|
72 | seqobj_tr (_ $ i) = i; |
73 |
73 |
74 fun seqcont_tr(Const("SeqContEmp",_)) = Bound 0 | |
74 fun seqcont_tr (Const (@{syntax_const "_SeqContEmp"}, _)) = Bound 0 |
75 seqcont_tr(Const("SeqContApp",_) $ so $ sc) = |
75 | seqcont_tr (Const (@{syntax_const "_SeqContApp"}, _) $ so $ sc) = |
76 (seqobj_tr so) $ (seqcont_tr sc); |
76 seqobj_tr so $ seqcont_tr sc; |
77 |
77 |
78 fun seq_tr(Const("SeqEmp",_)) = abs_seq'(Bound 0) | |
78 fun seq_tr (Const (@{syntax_const "_SeqEmp"}, _)) = abs_seq' (Bound 0) |
79 seq_tr(Const("SeqApp",_) $ so $ sc) = |
79 | seq_tr (Const (@{syntax_const "_SeqApp"}, _) $ so $ sc) = |
80 abs_seq'(seqobj_tr(so) $ seqcont_tr(sc)); |
80 abs_seq'(seqobj_tr so $ seqcont_tr sc); |
81 |
81 |
82 |
82 fun singlobj_tr (Const (@{syntax_const "_SeqO"},_) $ f) = |
83 fun singlobj_tr(Const("SeqO",_) $ f) = |
83 abs_seq' ((Const (@{const_syntax SeqO'}, dummyT) $ f) $ Bound 0); |
84 abs_seq' ((Const("SeqO'",dummyT) $ f) $ Bound 0); |
|
85 |
|
86 |
84 |
87 |
85 |
88 (* print translation for sequences *) |
86 (* print translation for sequences *) |
89 |
87 |
90 fun seqcont_tr' (Bound 0) = |
88 fun seqcont_tr' (Bound 0) = |
91 Const("SeqContEmp",dummyT) | |
89 Const (@{syntax_const "_SeqContEmp"}, dummyT) |
92 seqcont_tr' (Const("SeqO'",_) $ f $ s) = |
90 | seqcont_tr' (Const (@{const_syntax SeqO'}, _) $ f $ s) = |
93 Const("SeqContApp",dummyT) $ |
91 Const (@{syntax_const "_SeqContApp"}, dummyT) $ |
94 (Const("SeqO",dummyT) $ f) $ |
92 (Const (@{syntax_const "_SeqO"}, dummyT) $ f) $ seqcont_tr' s |
95 (seqcont_tr' s) | |
93 | seqcont_tr' (i $ s) = |
96 (* seqcont_tr' ((a as Abs(_,_,_)) $ s)= |
94 Const (@{syntax_const "_SeqContApp"}, dummyT) $ |
97 seqcont_tr'(Term.betapply(a,s)) | *) |
95 (Const (@{syntax_const "_SeqId"}, dummyT) $ i) $ seqcont_tr' s; |
98 seqcont_tr' (i $ s) = |
|
99 Const("SeqContApp",dummyT) $ |
|
100 (Const("SeqId",dummyT) $ i) $ |
|
101 (seqcont_tr' s); |
|
102 |
96 |
103 fun seq_tr' s = |
97 fun seq_tr' s = |
104 let fun seq_itr' (Bound 0) = |
98 let |
105 Const("SeqEmp",dummyT) | |
99 fun seq_itr' (Bound 0) = Const (@{syntax_const "_SeqEmp"}, dummyT) |
106 seq_itr' (Const("SeqO'",_) $ f $ s) = |
100 | seq_itr' (Const (@{const_syntax SeqO'}, _) $ f $ s) = |
107 Const("SeqApp",dummyT) $ |
101 Const (@{syntax_const "_SeqApp"}, dummyT) $ |
108 (Const("SeqO",dummyT) $ f) $ (seqcont_tr' s) | |
102 (Const (@{syntax_const "_SeqO"}, dummyT) $ f) $ seqcont_tr' s |
109 (* seq_itr' ((a as Abs(_,_,_)) $ s) = |
103 | seq_itr' (i $ s) = |
110 seq_itr'(Term.betapply(a,s)) | *) |
104 Const (@{syntax_const "_SeqApp"}, dummyT) $ |
111 seq_itr' (i $ s) = |
105 (Const (@{syntax_const "_SeqId"}, dummyT) $ i) $ seqcont_tr' s |
112 Const("SeqApp",dummyT) $ |
106 in |
113 (Const("SeqId",dummyT) $ i) $ |
107 case s of |
114 (seqcont_tr' s) |
108 Abs (_, _, t) => seq_itr' t |
115 in case s of |
109 | _ => s $ Bound 0 |
116 Abs(_,_,t) => seq_itr' t | |
110 end; |
117 _ => s $ (Bound 0) |
|
118 end; |
|
119 |
111 |
120 |
112 |
|
113 fun single_tr c [s1, s2] = |
|
114 Const (c, dummyT) $ seq_tr s1 $ singlobj_tr s2; |
|
115 |
|
116 fun two_seq_tr c [s1, s2] = |
|
117 Const (c, dummyT) $ seq_tr s1 $ seq_tr s2; |
|
118 |
|
119 fun three_seq_tr c [s1, s2, s3] = |
|
120 Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3; |
|
121 |
|
122 fun four_seq_tr c [s1, s2, s3, s4] = |
|
123 Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4; |
121 |
124 |
122 |
125 |
123 fun single_tr c [s1,s2] = |
126 fun singlobj_tr' (Const (@{const_syntax SeqO'},_) $ fm) = fm |
124 Const(c,dummyT) $ seq_tr s1 $ singlobj_tr s2; |
127 | singlobj_tr' id = Const (@{syntax_const "_SeqId"}, dummyT) $ id; |
125 |
|
126 fun two_seq_tr c [s1,s2] = |
|
127 Const(c,dummyT) $ seq_tr s1 $ seq_tr s2; |
|
128 |
|
129 fun three_seq_tr c [s1,s2,s3] = |
|
130 Const(c,dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3; |
|
131 |
|
132 fun four_seq_tr c [s1,s2,s3,s4] = |
|
133 Const(c,dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4; |
|
134 |
|
135 |
|
136 fun singlobj_tr'(Const("SeqO'",_) $ fm) = fm | |
|
137 singlobj_tr'(id) = Const("@SeqId",dummyT) $ id; |
|
138 |
128 |
139 |
129 |
140 fun single_tr' c [s1, s2] = |
130 fun single_tr' c [s1, s2] = |
141 (Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2 ); |
131 Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2; |
142 |
|
143 |
132 |
144 fun two_seq_tr' c [s1, s2] = |
133 fun two_seq_tr' c [s1, s2] = |
145 Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2; |
134 Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2; |
146 |
135 |
147 fun three_seq_tr' c [s1, s2, s3] = |
136 fun three_seq_tr' c [s1, s2, s3] = |