56 |
56 |
57 ML \<open> |
57 ML \<open> |
58 |
58 |
59 (* parse translation for sequences *) |
59 (* parse translation for sequences *) |
60 |
60 |
61 fun abs_seq' t = Abs ("s", Type (@{type_name seq'}, []), t); |
61 fun abs_seq' t = Abs ("s", Type (\<^type_name>\<open>seq'\<close>, []), t); |
62 |
62 |
63 fun seqobj_tr (Const (@{syntax_const "_SeqO"}, _) $ f) = |
63 fun seqobj_tr (Const (\<^syntax_const>\<open>_SeqO\<close>, _) $ f) = |
64 Const (@{const_syntax SeqO'}, dummyT) $ f |
64 Const (\<^const_syntax>\<open>SeqO'\<close>, dummyT) $ f |
65 | seqobj_tr (_ $ i) = i; |
65 | seqobj_tr (_ $ i) = i; |
66 |
66 |
67 fun seqcont_tr (Const (@{syntax_const "_SeqContEmp"}, _)) = Bound 0 |
67 fun seqcont_tr (Const (\<^syntax_const>\<open>_SeqContEmp\<close>, _)) = Bound 0 |
68 | seqcont_tr (Const (@{syntax_const "_SeqContApp"}, _) $ so $ sc) = |
68 | seqcont_tr (Const (\<^syntax_const>\<open>_SeqContApp\<close>, _) $ so $ sc) = |
69 seqobj_tr so $ seqcont_tr sc; |
69 seqobj_tr so $ seqcont_tr sc; |
70 |
70 |
71 fun seq_tr (Const (@{syntax_const "_SeqEmp"}, _)) = abs_seq' (Bound 0) |
71 fun seq_tr (Const (\<^syntax_const>\<open>_SeqEmp\<close>, _)) = abs_seq' (Bound 0) |
72 | seq_tr (Const (@{syntax_const "_SeqApp"}, _) $ so $ sc) = |
72 | seq_tr (Const (\<^syntax_const>\<open>_SeqApp\<close>, _) $ so $ sc) = |
73 abs_seq'(seqobj_tr so $ seqcont_tr sc); |
73 abs_seq'(seqobj_tr so $ seqcont_tr sc); |
74 |
74 |
75 fun singlobj_tr (Const (@{syntax_const "_SeqO"},_) $ f) = |
75 fun singlobj_tr (Const (\<^syntax_const>\<open>_SeqO\<close>,_) $ f) = |
76 abs_seq' ((Const (@{const_syntax SeqO'}, dummyT) $ f) $ Bound 0); |
76 abs_seq' ((Const (\<^const_syntax>\<open>SeqO'\<close>, dummyT) $ f) $ Bound 0); |
77 |
77 |
78 |
78 |
79 (* print translation for sequences *) |
79 (* print translation for sequences *) |
80 |
80 |
81 fun seqcont_tr' (Bound 0) = |
81 fun seqcont_tr' (Bound 0) = |
82 Const (@{syntax_const "_SeqContEmp"}, dummyT) |
82 Const (\<^syntax_const>\<open>_SeqContEmp\<close>, dummyT) |
83 | seqcont_tr' (Const (@{const_syntax SeqO'}, _) $ f $ s) = |
83 | seqcont_tr' (Const (\<^const_syntax>\<open>SeqO'\<close>, _) $ f $ s) = |
84 Const (@{syntax_const "_SeqContApp"}, dummyT) $ |
84 Const (\<^syntax_const>\<open>_SeqContApp\<close>, dummyT) $ |
85 (Const (@{syntax_const "_SeqO"}, dummyT) $ f) $ seqcont_tr' s |
85 (Const (\<^syntax_const>\<open>_SeqO\<close>, dummyT) $ f) $ seqcont_tr' s |
86 | seqcont_tr' (i $ s) = |
86 | seqcont_tr' (i $ s) = |
87 Const (@{syntax_const "_SeqContApp"}, dummyT) $ |
87 Const (\<^syntax_const>\<open>_SeqContApp\<close>, dummyT) $ |
88 (Const (@{syntax_const "_SeqId"}, dummyT) $ i) $ seqcont_tr' s; |
88 (Const (\<^syntax_const>\<open>_SeqId\<close>, dummyT) $ i) $ seqcont_tr' s; |
89 |
89 |
90 fun seq_tr' s = |
90 fun seq_tr' s = |
91 let |
91 let |
92 fun seq_itr' (Bound 0) = Const (@{syntax_const "_SeqEmp"}, dummyT) |
92 fun seq_itr' (Bound 0) = Const (\<^syntax_const>\<open>_SeqEmp\<close>, dummyT) |
93 | seq_itr' (Const (@{const_syntax SeqO'}, _) $ f $ s) = |
93 | seq_itr' (Const (\<^const_syntax>\<open>SeqO'\<close>, _) $ f $ s) = |
94 Const (@{syntax_const "_SeqApp"}, dummyT) $ |
94 Const (\<^syntax_const>\<open>_SeqApp\<close>, dummyT) $ |
95 (Const (@{syntax_const "_SeqO"}, dummyT) $ f) $ seqcont_tr' s |
95 (Const (\<^syntax_const>\<open>_SeqO\<close>, dummyT) $ f) $ seqcont_tr' s |
96 | seq_itr' (i $ s) = |
96 | seq_itr' (i $ s) = |
97 Const (@{syntax_const "_SeqApp"}, dummyT) $ |
97 Const (\<^syntax_const>\<open>_SeqApp\<close>, dummyT) $ |
98 (Const (@{syntax_const "_SeqId"}, dummyT) $ i) $ seqcont_tr' s |
98 (Const (\<^syntax_const>\<open>_SeqId\<close>, dummyT) $ i) $ seqcont_tr' s |
99 in |
99 in |
100 case s of |
100 case s of |
101 Abs (_, _, t) => seq_itr' t |
101 Abs (_, _, t) => seq_itr' t |
102 | _ => s $ Bound 0 |
102 | _ => s $ Bound 0 |
103 end; |
103 end; |
114 |
114 |
115 fun four_seq_tr c [s1, s2, s3, s4] = |
115 fun four_seq_tr c [s1, s2, s3, s4] = |
116 Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4; |
116 Const (c, dummyT) $ seq_tr s1 $ seq_tr s2 $ seq_tr s3 $ seq_tr s4; |
117 |
117 |
118 |
118 |
119 fun singlobj_tr' (Const (@{const_syntax SeqO'},_) $ fm) = fm |
119 fun singlobj_tr' (Const (\<^const_syntax>\<open>SeqO'\<close>,_) $ fm) = fm |
120 | singlobj_tr' id = Const (@{syntax_const "_SeqId"}, dummyT) $ id; |
120 | singlobj_tr' id = Const (\<^syntax_const>\<open>_SeqId\<close>, dummyT) $ id; |
121 |
121 |
122 |
122 |
123 fun single_tr' c [s1, s2] = |
123 fun single_tr' c [s1, s2] = |
124 Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2; |
124 Const (c, dummyT) $ seq_tr' s1 $ seq_tr' s2; |
125 |
125 |