137 val Inl_const: typ -> typ -> term |
137 val Inl_const: typ -> typ -> term |
138 val Inr_const: typ -> typ -> term |
138 val Inr_const: typ -> typ -> term |
139 |
139 |
140 val mk_case_sum: term * term -> term |
140 val mk_case_sum: term * term -> term |
141 val mk_case_sumN: term list -> term |
141 val mk_case_sumN: term list -> term |
142 val mk_case_absumprod: typ -> term -> term list -> term list -> term list list -> term |
142 val mk_case_absumprod: typ -> term -> term list -> term list list -> term list list -> term |
143 |
143 |
144 val mk_Inl: typ -> term -> term |
144 val mk_Inl: typ -> term -> term |
145 val mk_Inr: typ -> term -> term |
145 val mk_Inr: typ -> term -> term |
146 val mk_tuple_balanced: term list -> term |
|
147 val mk_absumprod: typ -> term -> int -> int -> term list -> term |
146 val mk_absumprod: typ -> term -> int -> int -> term list -> term |
148 |
147 |
149 val dest_sumT: typ -> typ * typ |
148 val dest_sumT: typ -> typ * typ |
150 val dest_absumprodT: typ -> typ -> int -> int list -> typ -> typ list list |
149 val dest_absumprodT: typ -> typ -> int -> int list -> typ -> typ list list |
151 |
150 |
372 fun mk_Inl RT t = Inl_const (fastype_of t) RT $ t; |
371 fun mk_Inl RT t = Inl_const (fastype_of t) RT $ t; |
373 |
372 |
374 fun Inr_const LT RT = Const (@{const_name Inr}, RT --> mk_sumT (LT, RT)); |
373 fun Inr_const LT RT = Const (@{const_name Inr}, RT --> mk_sumT (LT, RT)); |
375 fun mk_Inr LT t = Inr_const LT (fastype_of t) $ t; |
374 fun mk_Inr LT t = Inr_const LT (fastype_of t) $ t; |
376 |
375 |
377 (* FIXME: reuse "mk_inj" in function package *) |
|
378 fun mk_InN_balanced sum_T n t k = |
|
379 let |
|
380 fun repair_types T (Const (s as @{const_name Inl}, _) $ t) = repair_inj_types T s fst t |
|
381 | repair_types T (Const (s as @{const_name Inr}, _) $ t) = repair_inj_types T s snd t |
|
382 | repair_types _ t = t |
|
383 and repair_inj_types T s get t = |
|
384 let val T' = get (dest_sumT T) in |
|
385 Const (s, T' --> T) $ repair_types T' t |
|
386 end; |
|
387 in |
|
388 Balanced_Tree.access {left = mk_Inl dummyT, right = mk_Inr dummyT, init = t} n k |
|
389 |> repair_types sum_T |
|
390 end; |
|
391 |
|
392 fun mk_tuple_balanced [] = HOLogic.unit |
376 fun mk_tuple_balanced [] = HOLogic.unit |
393 | mk_tuple_balanced ts = Balanced_Tree.make HOLogic.mk_prod ts; |
377 | mk_tuple_balanced ts = Balanced_Tree.make HOLogic.mk_prod ts; |
394 |
378 |
395 fun mk_absumprod absT abs0 n k ts = |
379 fun mk_absumprod absT abs0 n k ts = |
396 let val abs = mk_abs absT abs0; |
380 let val abs = mk_abs absT abs0; |
397 in abs $ mk_InN_balanced (domain_type (fastype_of abs)) n (mk_tuple_balanced ts) k end; |
381 in abs $ Sum_Tree.mk_inj (domain_type (fastype_of abs)) n k (mk_tuple_balanced ts) end; |
398 |
382 |
399 fun mk_case_sum (f, g) = |
383 fun mk_case_sum (f, g) = |
400 let |
384 let |
401 val fT = fastype_of f; |
385 val (fT, T') = dest_funT (fastype_of f); |
402 val gT = fastype_of g; |
386 val (gT, _) = dest_funT (fastype_of g); |
403 in |
387 in |
404 Const (@{const_name case_sum}, |
388 Sum_Tree.mk_sumcase fT gT T' f g |
405 fT --> gT --> mk_sumT (domain_type fT, domain_type gT) --> range_type fT) $ f $ g |
|
406 end; |
389 end; |
407 |
390 |
408 val mk_case_sumN = Library.foldr1 mk_case_sum; |
391 val mk_case_sumN = Library.foldr1 mk_case_sum; |
409 val mk_case_sumN_balanced = Balanced_Tree.make mk_case_sum; |
392 val mk_case_sumN_balanced = Balanced_Tree.make mk_case_sum; |
410 |
393 |
411 fun mk_tupled_fun f x xs = |
394 fun mk_tupled_fun f x xs = |
412 if xs = [x] then f else HOLogic.tupled_lambda x (Term.list_comb (f, xs)); |
395 if xs = [x] then f else HOLogic.tupled_lambda x (Term.list_comb (f, xs)); |
413 |
396 |
414 fun mk_case_absumprod absT rep fs xs xss = |
397 fun mk_case_absumprod absT rep fs xss xss' = |
415 HOLogic.mk_comp (mk_case_sumN_balanced (map3 mk_tupled_fun fs xs xss), mk_rep absT rep); |
398 HOLogic.mk_comp (mk_case_sumN_balanced (map3 mk_tupled_fun fs (map mk_tuple_balanced xss) xss'), |
|
399 mk_rep absT rep); |
416 |
400 |
417 fun If_const T = Const (@{const_name If}, HOLogic.boolT --> T --> T --> T); |
401 fun If_const T = Const (@{const_name If}, HOLogic.boolT --> T --> T --> T); |
418 fun mk_If p t f = let val T = fastype_of t in If_const T $ p $ t $ f end; |
402 fun mk_If p t f = let val T = fastype_of t in If_const T $ p $ t $ f end; |
419 |
403 |
420 fun mk_Field r = |
404 fun mk_Field r = |