# HG changeset patch
# User blanchet
# Date 1380097564 -7200
# Node ID 7c23df53af01a5ae339c87f71443b43c08865213
# Parent  cadccda5be038fe12eaee409c5bbb494d3b3d26c
generalized case-handling code a bit

diff -r cadccda5be03 -r 7c23df53af01 src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 10:17:18 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 10:26:04 2013 +0200
@@ -197,7 +197,29 @@
     massage_call
   end;
 
-fun massage_let_if ctxt has_call massage_leaf bound_Ts U =
+(* TODO: also support old-style datatypes.
+   (Ideally, we would have a proper registry for these things.) *)
+fun case_of ctxt =
+  fp_sugar_of ctxt #> Option.map (fst o dest_Const o #casex o of_fp_sugar #ctr_sugars);
+
+fun fold_rev_let_if_case ctxt f bound_Ts =
+  let
+    fun fld t =
+      (case Term.strip_comb t of
+        (Const (@{const_name Let}, _), [arg1, arg2]) => fld (betapply (arg2, arg1))
+      | (Const (@{const_name If}, _), _ :: branches) => fold_rev fld branches
+      | (Const (c, _), args as _ :: _) =>
+        let val (branches, obj) = split_last args in
+          (case fastype_of1 (bound_Ts, obj) of
+            Type (T_name, _) => if case_of ctxt T_name = SOME c then fold_rev fld branches else f t
+          | _ => f t)
+        end
+      | _ => f t)
+  in
+    fld
+  end;
+
+fun massage_let_if_case ctxt has_call massage_leaf bound_Ts U =
   let
     val typof = curry fastype_of1 bound_Ts;
     val check_obj = ((not o has_call) orf unexpected_corec_call ctxt);
@@ -207,22 +229,27 @@
         (Const (@{const_name Let}, _), [arg1, arg2]) => massage_rec (betapply (arg2, arg1))
       | (Const (@{const_name If}, _), obj :: branches) =>
         list_comb (If_const U $ tap check_obj obj, map massage_rec branches)
-      | (Const (@{const_name nat_case}, _), args) =>
-        (* Proof of concept -- should be extensible to all case-like constructs *)
-        let
-          val (branches, obj) = split_last args;
-          val branches' = map massage_rec branches
-          (* FIXME: bound_Ts *)
-          val casex' = Const (@{const_name nat_case}, map typof branches' ---> typof obj);
-        in
-          list_comb (casex', branches') $ tap check_obj obj
+      | (Const (c, _), args as _ :: _) =>
+        let val (branches, obj) = split_last args in
+          (case fastype_of1 (bound_Ts, obj) of
+            Type (T_name, _) =>
+            if case_of ctxt T_name = SOME c then
+              let
+                val branches' = map massage_rec branches;
+                val casex' = Const (c, map typof branches' ---> typof obj);
+              in
+                list_comb (casex', branches') $ tap check_obj obj
+              end
+            else
+              massage_leaf t
+          | _ => massage_leaf t)
         end
       | _ => massage_leaf t)
   in
     massage_rec
   end;
 
-val massage_direct_corec_call = massage_let_if;
+val massage_direct_corec_call = massage_let_if_case;
 
 fun massage_indirect_corec_call ctxt has_call raw_massage_call bound_Ts U t =
   let
@@ -258,7 +285,7 @@
         handle AINT_NO_MAP _ => massage_direct_fun U T t;
 
     fun massage_call U T =
-      massage_let_if ctxt has_call (fn t =>
+      massage_let_if_case ctxt has_call (fn t =>
         if has_call t then
           (case U of
             Type (s, Us) =>
@@ -300,37 +327,17 @@
 fun expand_corec_code_rhs ctxt has_call bound_Ts t =
   (case fastype_of1 (bound_Ts, t) of
     T as Type (s, Ts) =>
-    massage_let_if ctxt has_call (fn t =>
-      if can (dest_ctr ctxt s) t then t
-      else massage_let_if ctxt has_call I bound_Ts T (expand_ctr_term ctxt s Ts t)) bound_Ts T t
+    massage_let_if_case ctxt has_call (fn t =>
+      if can (dest_ctr ctxt s) t then
+        t
+      else
+        massage_let_if_case ctxt has_call I bound_Ts T (expand_ctr_term ctxt s Ts t)) bound_Ts T t
   | _ => raise Fail "expand_corec_code_rhs");
 
 fun massage_corec_code_rhs ctxt massage_ctr =
-  massage_let_if ctxt (K false) (uncurry massage_ctr o Term.strip_comb);
-
-(* TODO: also support old-style datatypes.
-   (Ideally, we would have a proper registry for these things.) *)
-fun case_of ctxt =
-  fp_sugar_of ctxt #> Option.map (fst o dest_Const o #casex o of_fp_sugar #ctr_sugars);
+  massage_let_if_case ctxt (K false) (uncurry massage_ctr o Term.strip_comb);
 
-fun fold_rev_let_if ctxt f bound_Ts =
-  let
-    fun fld t =
-      (case Term.strip_comb t of
-        (Const (@{const_name Let}, _), [arg1, arg2]) => fld (betapply (arg2, arg1))
-      | (Const (@{const_name If}, _), _ :: branches) => fold_rev fld branches
-      | (Const (c, _), args as _ :: _) =>
-        let val (branches, obj) = split_last args in
-          (case fastype_of1 (bound_Ts, obj) of
-            Type (T_name, _) => if case_of ctxt T_name = SOME c then fold_rev fld branches else f t
-          | _ => f t)
-        end
-      | _ => f t)
-  in
-    fld
-  end;
-
-fun fold_rev_corec_code_rhs ctxt f = fold_rev_let_if ctxt (uncurry f o Term.strip_comb);
+fun fold_rev_corec_code_rhs ctxt f = fold_rev_let_if_case ctxt (uncurry f o Term.strip_comb);
 
 fun add_conjuncts (Const (@{const_name conj}, _) $ t $ t') = add_conjuncts t o add_conjuncts t'
   | add_conjuncts t = cons t;