250 sscase_const (T, U, U) ` mk_bottom (T ->> U) ` mk_ID U; |
250 sscase_const (T, U, U) ` mk_bottom (T ->> U) ` mk_ID U; |
251 |
251 |
252 |
252 |
253 (*** pattern match monad type ***) |
253 (*** pattern match monad type ***) |
254 |
254 |
255 fun mk_matchT T = Type (@{type_name "maybe"}, [T]); |
255 fun mk_matchT T = Type (@{type_name "match"}, [T]); |
256 |
256 |
257 fun dest_matchT (Type(@{type_name "maybe"}, [T])) = T |
257 fun dest_matchT (Type(@{type_name "match"}, [T])) = T |
258 | dest_matchT T = raise TYPE ("dest_matchT", [T], []); |
258 | dest_matchT T = raise TYPE ("dest_matchT", [T], []); |
259 |
259 |
260 fun mk_fail T = Const (@{const_name "Fixrec.fail"}, mk_matchT T); |
260 fun mk_fail T = Const (@{const_name "Fixrec.fail"}, mk_matchT T); |
261 |
261 |
262 fun return_const T = Const (@{const_name "Fixrec.return"}, T ->> mk_matchT T); |
262 fun succeed_const T = Const (@{const_name "Fixrec.succeed"}, T ->> mk_matchT T); |
263 fun mk_return t = return_const (fastype_of t) ` t; |
263 fun mk_succeed t = succeed_const (fastype_of t) ` t; |
264 |
264 |
265 |
265 |
266 (*** lifted boolean type ***) |
266 (*** lifted boolean type ***) |
267 |
267 |
268 val trT = @{typ "tr"}; |
268 val trT = @{typ "tr"}; |