1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 19 01:09:25 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 19 01:09:25 2013 +0200
     1.3 @@ -57,6 +57,8 @@
     1.4      term
     1.5    val massage_indirect_corec_call: Proof.context -> (term -> bool) ->
     1.6      (typ -> typ -> term -> term) -> typ list -> typ -> term -> term
     1.7 +  val massage_corec_code_rhs: Proof.context -> (term -> bool) -> (term -> term list -> term) ->
     1.8 +    typ list -> typ -> term -> term
     1.9    val rec_specs_of: binding list -> typ list -> typ list -> (term -> int list) ->
    1.10      ((term * term list list) list) list -> local_theory ->
    1.11      (bool * rec_spec list * typ list * thm * thm list) * local_theory
    1.12 @@ -126,9 +128,6 @@
    1.13    error ("Ill-formed recursive call: " ^ quote (Syntax.string_of_term ctxt t));
    1.14  fun ill_formed_corec_call ctxt t =
    1.15    error ("Ill-formed corecursive call: " ^ quote (Syntax.string_of_term ctxt t));
    1.16 -fun ill_formed_corec_code_rhs ctxt t =
    1.17 -  error ("Ill-formed corecursive equation right-hand side: " ^
    1.18 -    quote (Syntax.string_of_term ctxt t));
    1.19  fun invalid_map ctxt t =
    1.20    error ("Invalid map function in " ^ quote (Syntax.string_of_term ctxt t));
    1.21  fun unexpected_rec_call ctxt t =
    1.22 @@ -196,8 +195,9 @@
    1.23      massage_call
    1.24    end;
    1.25  
    1.26 -fun massage_let_and_if ctxt check_cond massage_leaf U =
    1.27 +fun massage_let_and_if ctxt has_call massage_leaf U =
    1.28    let
    1.29 +    val check_cond = ((not o has_call) orf unexpected_corec_call ctxt);
    1.30      fun massage_rec t =
    1.31        (case Term.strip_comb t of
    1.32          (Const (@{const_name Let}, _), [arg1, arg2]) => massage_rec (betapply (arg2, arg1))
    1.33 @@ -209,8 +209,7 @@
    1.34    end;
    1.35  
    1.36  fun massage_direct_corec_call ctxt has_call massage_direct_call U t =
    1.37 -  massage_let_and_if ctxt ((not o has_call) orf unexpected_corec_call ctxt) massage_direct_call
    1.38 -    U t;
    1.39 +  massage_let_and_if ctxt has_call massage_direct_call U t;
    1.40  
    1.41  fun massage_indirect_corec_call ctxt has_call massage_direct_call bound_Ts U t =
    1.42    let
    1.43 @@ -246,30 +245,59 @@
    1.44          handle AINT_NO_MAP _ => check_and_massage_unapplied_direct_call U T t;
    1.45  
    1.46      fun massage_call U T =
    1.47 -      massage_let_and_if ctxt ((not o has_call) orf unexpected_corec_call ctxt)
    1.48 -        (fn t =>
    1.49 -            (case U of
    1.50 -              Type (s, Us) =>
    1.51 -              (case try (dest_ctr ctxt s) t of
    1.52 -                SOME (f, args) =>
    1.53 -                let val f' = mk_ctr Us f in
    1.54 -                  list_comb (f', map3 massage_call (binder_types (typof f')) (map typof args) args)
    1.55 -                end
    1.56 -              | NONE =>
    1.57 -                (case t of
    1.58 -                  t1 $ t2 =>
    1.59 -                  (if has_call t2 then
    1.60 -                    check_and_massage_direct_call U T t
    1.61 -                  else
    1.62 -                    massage_map U T t1 $ t2
    1.63 -                    handle AINT_NO_MAP _ => check_and_massage_direct_call U T t)
    1.64 -                | _ => check_and_massage_direct_call U T t))
    1.65 -            | _ => ill_formed_corec_call ctxt t))
    1.66 -        U
    1.67 +      massage_let_and_if ctxt has_call (fn t =>
    1.68 +        (case U of
    1.69 +          Type (s, Us) =>
    1.70 +          (case try (dest_ctr ctxt s) t of
    1.71 +            SOME (f, args) =>
    1.72 +            let val f' = mk_ctr Us f in
    1.73 +              list_comb (f', map3 massage_call (binder_types (typof f')) (map typof args) args)
    1.74 +            end
    1.75 +          | NONE =>
    1.76 +            (case t of
    1.77 +              t1 $ t2 =>
    1.78 +              (if has_call t2 then
    1.79 +                check_and_massage_direct_call U T t
    1.80 +              else
    1.81 +                massage_map U T t1 $ t2
    1.82 +                handle AINT_NO_MAP _ => check_and_massage_direct_call U T t)
    1.83 +            | _ => check_and_massage_direct_call U T t))
    1.84 +        | _ => ill_formed_corec_call ctxt t)) U
    1.85    in
    1.86      massage_call U (typof t) t
    1.87    end;
    1.88  
    1.89 +fun explode_ctr_term ctxt s Ts t =
    1.90 +  (case fp_sugar_of ctxt s of
    1.91 +    SOME fp_sugar =>
    1.92 +    let
    1.93 +      val T = Type (s, Ts);
    1.94 +      val x = Bound 0;
    1.95 +      val {ctrs = ctrs0, discs = discs0, selss = selss0, ...} = of_fp_sugar #ctr_sugars fp_sugar;
    1.96 +      val ctrs = map (mk_ctr Ts) ctrs0;
    1.97 +      val discs = map (mk_disc_or_sel Ts) discs0;
    1.98 +      val selss = map (map (mk_disc_or_sel Ts)) selss0;
    1.99 +      val xdiscs = map (rapp x) discs;
   1.100 +      val xselss = map (map (rapp x)) selss;
   1.101 +      val xsel_ctrs = map2 (curry Term.list_comb) ctrs xselss;
   1.102 +      val xif = mk_IfN T xdiscs xsel_ctrs;
   1.103 +    in
   1.104 +      Const (@{const_name Let}, T --> (T --> T) --> T) $ t $ Abs (Name.uu, T, xif)
   1.105 +    end
   1.106 +  | NONE => raise Fail "explode_ctr_term");
   1.107 +
   1.108 +fun massage_corec_code_rhs ctxt has_call massage_ctr bound_Ts U t =
   1.109 +  let val typof = curry fastype_of1 bound_Ts in
   1.110 +    (case typof t of
   1.111 +      T as Type (s, Ts) =>
   1.112 +      massage_let_and_if ctxt has_call (fn t =>
   1.113 +        (case try (dest_ctr ctxt s) t of
   1.114 +          SOME (f, args) => massage_ctr f args
   1.115 +        | NONE => massage_let_and_if ctxt has_call (uncurry massage_ctr o Term.strip_comb) T
   1.116 +            (explode_ctr_term ctxt s Ts t))) U t
   1.117 +    | _ => raise Fail "massage_corec_code_rhs")
   1.118 +  end;
   1.119 +
   1.120  fun indexed xs h = let val h' = h + length xs in (h upto h' - 1, h') end;
   1.121  fun indexedd xss = fold_map indexed xss;
   1.122  fun indexeddd xsss = fold_map indexedd xsss;