equal
deleted
inserted
replaced
40 val dest_mem: term -> term * term |
40 val dest_mem: term -> term * term |
41 val mk_binop: string -> term * term -> term |
41 val mk_binop: string -> term * term -> term |
42 val mk_binrel: string -> term * term -> term |
42 val mk_binrel: string -> term * term -> term |
43 val dest_bin: string -> typ -> term -> term * term |
43 val dest_bin: string -> typ -> term -> term * term |
44 val unitT: typ |
44 val unitT: typ |
|
45 val is_unitT: typ -> bool |
45 val unit: term |
46 val unit: term |
46 val is_unit: term -> bool |
47 val is_unit: term -> bool |
47 val mk_prodT: typ * typ -> typ |
48 val mk_prodT: typ * typ -> typ |
48 val dest_prodT: typ -> typ * typ |
49 val dest_prodT: typ -> typ * typ |
49 val mk_prod: term * term -> term |
50 val mk_prod: term * term -> term |
165 |
166 |
166 (* unit *) |
167 (* unit *) |
167 |
168 |
168 val unitT = Type ("unit", []); |
169 val unitT = Type ("unit", []); |
169 |
170 |
|
171 fun is_unitT (Type ("unit", [])) = true |
|
172 | is_unitT _ = false; |
|
173 |
170 val unit = Const ("()", unitT); |
174 val unit = Const ("()", unitT); |
171 |
175 |
172 fun is_unit (Const ("()", _)) = true |
176 fun is_unit (Const ("()", _)) = true |
173 | is_unit _ = false; |
177 | is_unit _ = false; |
174 |
178 |
211 mk_tuple T2 (drop (length (prodT_factors T1), tms))) |
215 mk_tuple T2 (drop (length (prodT_factors T1), tms))) |
212 | mk_tuple T (t::_) = t; |
216 | mk_tuple T (t::_) = t; |
213 |
217 |
214 |
218 |
215 |
219 |
|
220 (* proper tuples *) |
|
221 |
|
222 local (*currently unused*) |
|
223 |
|
224 fun mk_tupleT Ts = foldr mk_prodT (Ts, unitT); |
|
225 |
|
226 fun dest_tupleT (Type ("unit", [])) = [] |
|
227 | dest_tupleT (Type ("*", [T, U])) = T :: dest_tupleT U |
|
228 | dest_tupleT T = raise TYPE ("dest_tupleT", [T], []); |
|
229 |
|
230 fun mk_tuple ts = foldr mk_prod (ts, unit); |
|
231 |
|
232 fun dest_tuple (Const ("()", _)) = [] |
|
233 | dest_tuple (Const ("Pair", _) $ t $ u) = t :: dest_tuple u |
|
234 | dest_tuple t = raise TERM ("dest_tuple", [t]); |
|
235 |
|
236 in val _ = unit end; |
|
237 |
|
238 |
216 (* nat *) |
239 (* nat *) |
217 |
240 |
218 val natT = Type ("nat", []); |
241 val natT = Type ("nat", []); |
219 |
242 |
220 val zero = Const ("0", natT); |
243 val zero = Const ("0", natT); |