1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 10:17:18 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 10:26:04 2013 +0200
     1.3 @@ -197,7 +197,29 @@
     1.4      massage_call
     1.5    end;
     1.6  
     1.7 -fun massage_let_if ctxt has_call massage_leaf bound_Ts U =
     1.8 +(* TODO: also support old-style datatypes.
     1.9 +   (Ideally, we would have a proper registry for these things.) *)
    1.10 +fun case_of ctxt =
    1.11 +  fp_sugar_of ctxt #> Option.map (fst o dest_Const o #casex o of_fp_sugar #ctr_sugars);
    1.12 +
    1.13 +fun fold_rev_let_if_case ctxt f bound_Ts =
    1.14 +  let
    1.15 +    fun fld t =
    1.16 +      (case Term.strip_comb t of
    1.17 +        (Const (@{const_name Let}, _), [arg1, arg2]) => fld (betapply (arg2, arg1))
    1.18 +      | (Const (@{const_name If}, _), _ :: branches) => fold_rev fld branches
    1.19 +      | (Const (c, _), args as _ :: _) =>
    1.20 +        let val (branches, obj) = split_last args in
    1.21 +          (case fastype_of1 (bound_Ts, obj) of
    1.22 +            Type (T_name, _) => if case_of ctxt T_name = SOME c then fold_rev fld branches else f t
    1.23 +          | _ => f t)
    1.24 +        end
    1.25 +      | _ => f t)
    1.26 +  in
    1.27 +    fld
    1.28 +  end;
    1.29 +
    1.30 +fun massage_let_if_case ctxt has_call massage_leaf bound_Ts U =
    1.31    let
    1.32      val typof = curry fastype_of1 bound_Ts;
    1.33      val check_obj = ((not o has_call) orf unexpected_corec_call ctxt);
    1.34 @@ -207,22 +229,27 @@
    1.35          (Const (@{const_name Let}, _), [arg1, arg2]) => massage_rec (betapply (arg2, arg1))
    1.36        | (Const (@{const_name If}, _), obj :: branches) =>
    1.37          list_comb (If_const U $ tap check_obj obj, map massage_rec branches)
    1.38 -      | (Const (@{const_name nat_case}, _), args) =>
    1.39 -        (* Proof of concept -- should be extensible to all case-like constructs *)
    1.40 -        let
    1.41 -          val (branches, obj) = split_last args;
    1.42 -          val branches' = map massage_rec branches
    1.43 -          (* FIXME: bound_Ts *)
    1.44 -          val casex' = Const (@{const_name nat_case}, map typof branches' ---> typof obj);
    1.45 -        in
    1.46 -          list_comb (casex', branches') $ tap check_obj obj
    1.47 +      | (Const (c, _), args as _ :: _) =>
    1.48 +        let val (branches, obj) = split_last args in
    1.49 +          (case fastype_of1 (bound_Ts, obj) of
    1.50 +            Type (T_name, _) =>
    1.51 +            if case_of ctxt T_name = SOME c then
    1.52 +              let
    1.53 +                val branches' = map massage_rec branches;
    1.54 +                val casex' = Const (c, map typof branches' ---> typof obj);
    1.55 +              in
    1.56 +                list_comb (casex', branches') $ tap check_obj obj
    1.57 +              end
    1.58 +            else
    1.59 +              massage_leaf t
    1.60 +          | _ => massage_leaf t)
    1.61          end
    1.62        | _ => massage_leaf t)
    1.63    in
    1.64      massage_rec
    1.65    end;
    1.66  
    1.67 -val massage_direct_corec_call = massage_let_if;
    1.68 +val massage_direct_corec_call = massage_let_if_case;
    1.69  
    1.70  fun massage_indirect_corec_call ctxt has_call raw_massage_call bound_Ts U t =
    1.71    let
    1.72 @@ -258,7 +285,7 @@
    1.73          handle AINT_NO_MAP _ => massage_direct_fun U T t;
    1.74  
    1.75      fun massage_call U T =
    1.76 -      massage_let_if ctxt has_call (fn t =>
    1.77 +      massage_let_if_case ctxt has_call (fn t =>
    1.78          if has_call t then
    1.79            (case U of
    1.80              Type (s, Us) =>
    1.81 @@ -300,37 +327,17 @@
    1.82  fun expand_corec_code_rhs ctxt has_call bound_Ts t =
    1.83    (case fastype_of1 (bound_Ts, t) of
    1.84      T as Type (s, Ts) =>
    1.85 -    massage_let_if ctxt has_call (fn t =>
    1.86 -      if can (dest_ctr ctxt s) t then t
    1.87 -      else massage_let_if ctxt has_call I bound_Ts T (expand_ctr_term ctxt s Ts t)) bound_Ts T t
    1.88 +    massage_let_if_case ctxt has_call (fn t =>
    1.89 +      if can (dest_ctr ctxt s) t then
    1.90 +        t
    1.91 +      else
    1.92 +        massage_let_if_case ctxt has_call I bound_Ts T (expand_ctr_term ctxt s Ts t)) bound_Ts T t
    1.93    | _ => raise Fail "expand_corec_code_rhs");
    1.94  
    1.95  fun massage_corec_code_rhs ctxt massage_ctr =
    1.96 -  massage_let_if ctxt (K false) (uncurry massage_ctr o Term.strip_comb);
    1.97 +  massage_let_if_case ctxt (K false) (uncurry massage_ctr o Term.strip_comb);
    1.98  
    1.99 -(* TODO: also support old-style datatypes.
   1.100 -   (Ideally, we would have a proper registry for these things.) *)
   1.101 -fun case_of ctxt =
   1.102 -  fp_sugar_of ctxt #> Option.map (fst o dest_Const o #casex o of_fp_sugar #ctr_sugars);
   1.103 -
   1.104 -fun fold_rev_let_if ctxt f bound_Ts =
   1.105 -  let
   1.106 -    fun fld t =
   1.107 -      (case Term.strip_comb t of
   1.108 -        (Const (@{const_name Let}, _), [arg1, arg2]) => fld (betapply (arg2, arg1))
   1.109 -      | (Const (@{const_name If}, _), _ :: branches) => fold_rev fld branches
   1.110 -      | (Const (c, _), args as _ :: _) =>
   1.111 -        let val (branches, obj) = split_last args in
   1.112 -          (case fastype_of1 (bound_Ts, obj) of
   1.113 -            Type (T_name, _) => if case_of ctxt T_name = SOME c then fold_rev fld branches else f t
   1.114 -          | _ => f t)
   1.115 -        end
   1.116 -      | _ => f t)
   1.117 -  in
   1.118 -    fld
   1.119 -  end;
   1.120 -
   1.121 -fun fold_rev_corec_code_rhs ctxt f = fold_rev_let_if ctxt (uncurry f o Term.strip_comb);
   1.122 +fun fold_rev_corec_code_rhs ctxt f = fold_rev_let_if_case ctxt (uncurry f o Term.strip_comb);
   1.123  
   1.124  fun add_conjuncts (Const (@{const_name conj}, _) $ t $ t') = add_conjuncts t o add_conjuncts t'
   1.125    | add_conjuncts t = cons t;