1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Mon Sep 30 17:53:44 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Mon Sep 30 18:08:35 2013 +0200
     1.3 @@ -189,7 +189,7 @@
     1.4        primrec_error_eqn "recursive call not directly applied to constructor argument" t)
     1.5    end;
     1.6  
     1.7 -fun build_rec_arg lthy (funs_data : eqn_data list) has_call ctr_spec maybe_eqn_data =
     1.8 +fun build_rec_arg lthy (funs_data : eqn_data list list) has_call ctr_spec maybe_eqn_data =
     1.9    if is_none maybe_eqn_data then undef_const else
    1.10      let
    1.11        val eqn_data = the maybe_eqn_data;
    1.12 @@ -243,7 +243,7 @@
    1.13        |> fold_rev lambda abstractions
    1.14      end;
    1.15  
    1.16 -fun build_defs lthy bs mxs (funs_data : eqn_data list) rec_specs has_call =
    1.17 +fun build_defs lthy bs mxs (funs_data : eqn_data list list) rec_specs has_call =
    1.18    let
    1.19      val n_funs = length funs_data;
    1.20  
    1.21 @@ -412,7 +412,8 @@
    1.22    Disc of co_eqn_data_disc |
    1.23    Sel of co_eqn_data_sel;
    1.24  
    1.25 -fun co_dissect_eqn_disc sequential fun_names corec_specs prems' concl matchedsss =
    1.26 +fun co_dissect_eqn_disc sequential fun_names (corec_specs : corec_spec list) prems' concl
    1.27 +    matchedsss =
    1.28    let
    1.29      fun find_subterm p = let (* FIXME \<exists>? *)
    1.30        fun f (t as u $ v) = if p t then SOME t else merge_options (f u, f v)
    1.31 @@ -470,7 +471,7 @@
    1.32      }, matchedsss')
    1.33    end;
    1.34  
    1.35 -fun co_dissect_eqn_sel fun_names corec_specs eqn' of_spec eqn =
    1.36 +fun co_dissect_eqn_sel fun_names (corec_specs : corec_spec list) eqn' of_spec eqn =
    1.37    let
    1.38      val (lhs, rhs) = HOLogic.dest_eq eqn
    1.39        handle TERM _ =>
    1.40 @@ -499,7 +500,8 @@
    1.41      }
    1.42    end;
    1.43  
    1.44 -fun co_dissect_eqn_ctr sequential fun_names corec_specs eqn' imp_prems imp_rhs matchedsss =
    1.45 +fun co_dissect_eqn_ctr sequential fun_names (corec_specs : corec_spec list) eqn' imp_prems imp_rhs
    1.46 +    matchedsss =
    1.47    let
    1.48      val (lhs, rhs) = HOLogic.dest_eq imp_rhs;
    1.49      val fun_name = head_of lhs |> fst o dest_Free;
    1.50 @@ -529,7 +531,7 @@
    1.51      (the_list maybe_eqn_data_disc @ eqns_data_sel, matchedsss')
    1.52    end;
    1.53  
    1.54 -fun co_dissect_eqn sequential fun_names corec_specs eqn' of_spec matchedsss =
    1.55 +fun co_dissect_eqn sequential fun_names (corec_specs : corec_spec list) eqn' of_spec matchedsss =
    1.56    let
    1.57      val eqn = drop_All eqn'
    1.58        handle TERM _ => primrec_error_eqn "malformed function equation" eqn';
    1.59 @@ -559,20 +561,21 @@
    1.60        primrec_error_eqn "malformed function equation" eqn
    1.61    end;
    1.62  
    1.63 -fun build_corec_arg_disc ctr_specs {fun_args, ctr_no, prems, ...} =
    1.64 +fun build_corec_arg_disc (ctr_specs : corec_ctr_spec list)
    1.65 +    ({fun_args, ctr_no, prems, ...} : co_eqn_data_disc) =
    1.66    if is_none (#pred (nth ctr_specs ctr_no)) then I else
    1.67      mk_conjs prems
    1.68      |> curry subst_bounds (List.rev fun_args)
    1.69      |> HOLogic.tupled_lambda (HOLogic.mk_tuple fun_args)
    1.70      |> K |> nth_map (the (#pred (nth ctr_specs ctr_no)));
    1.71  
    1.72 -fun build_corec_arg_no_call sel_eqns sel =
    1.73 +fun build_corec_arg_no_call (sel_eqns : co_eqn_data_sel list) sel =
    1.74    find_first (equal sel o #sel) sel_eqns
    1.75    |> try (fn SOME {fun_args, rhs_term, ...} => abs_tuple fun_args rhs_term)
    1.76    |> the_default undef_const
    1.77    |> K;
    1.78  
    1.79 -fun build_corec_args_direct_call lthy has_call sel_eqns sel =
    1.80 +fun build_corec_args_direct_call lthy has_call (sel_eqns : co_eqn_data_sel list) sel =
    1.81    let
    1.82      val maybe_sel_eqn = find_first (equal sel o #sel) sel_eqns;
    1.83    in
    1.84 @@ -591,7 +594,7 @@
    1.85      end
    1.86    end;
    1.87  
    1.88 -fun build_corec_arg_indirect_call lthy has_call sel_eqns sel =
    1.89 +fun build_corec_arg_indirect_call lthy has_call (sel_eqns : co_eqn_data_sel list) sel =
    1.90    let
    1.91      val maybe_sel_eqn = find_first (equal sel o #sel) sel_eqns;
    1.92    in
    1.93 @@ -618,7 +621,8 @@
    1.94      end
    1.95    end;
    1.96  
    1.97 -fun build_corec_args_sel lthy has_call all_sel_eqns ctr_spec =
    1.98 +fun build_corec_args_sel lthy has_call (all_sel_eqns : co_eqn_data_sel list)
    1.99 +    (ctr_spec : corec_ctr_spec) =
   1.100    let val sel_eqns = filter (equal (#ctr ctr_spec) o #ctr) all_sel_eqns in
   1.101      if null sel_eqns then I else
   1.102        let
   1.103 @@ -638,7 +642,8 @@
   1.104        end
   1.105    end;
   1.106  
   1.107 -fun co_build_defs lthy bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss =
   1.108 +fun co_build_defs lthy bs mxs has_call arg_Tss (corec_specs : corec_spec list)
   1.109 +    (disc_eqnss : co_eqn_data_disc list list) (sel_eqnss : co_eqn_data_sel list list) =
   1.110    let
   1.111      val corec_specs' = take (length bs) corec_specs;
   1.112      val corecs = map #corec corec_specs';
   1.113 @@ -676,7 +681,8 @@
   1.114      |> rpair exclss'
   1.115    end;
   1.116  
   1.117 -fun mk_real_disc_eqns fun_binding arg_Ts {ctr_specs, ...} sel_eqns disc_eqns =
   1.118 +fun mk_real_disc_eqns fun_binding arg_Ts ({ctr_specs, ...} : corec_spec)
   1.119 +    (sel_eqns : co_eqn_data_sel list) (disc_eqns : co_eqn_data_disc list) =
   1.120    if length disc_eqns <> length ctr_specs - 1 then disc_eqns else
   1.121      let
   1.122        val n = 0 upto length ctr_specs
   1.123 @@ -764,8 +770,8 @@
   1.124          val exclssss = (exclss' ~~ taut_thmss |> map (op @), fun_names ~~ corec_specs)
   1.125            |-> map2 (fn excls => fn (_, {ctr_specs, ...}) => mk_exclsss excls (length ctr_specs));
   1.126  
   1.127 -        fun prove_disc {ctr_specs, ...} exclsss
   1.128 -            {fun_name, fun_T, fun_args, ctr_no, prems, user_eqn, ...} =
   1.129 +        fun prove_disc ({ctr_specs, ...} : corec_spec) exclsss
   1.130 +            ({fun_name, fun_T, fun_args, ctr_no, prems, ...} : co_eqn_data_disc) =
   1.131            if Term.aconv_untyped (#disc (nth ctr_specs ctr_no), @{term "\<lambda>x. x = x"}) then [] else
   1.132              let
   1.133                val {disc_corec, ...} = nth ctr_specs ctr_no;
   1.134 @@ -784,8 +790,9 @@
   1.135                |> single
   1.136              end;
   1.137  
   1.138 -        fun prove_sel {ctr_specs, nested_maps, nested_map_idents, nested_map_comps, ...}
   1.139 -            disc_eqns exclsss {fun_name, fun_T, fun_args, ctr, sel, rhs_term, ...} =
   1.140 +        fun prove_sel ({nested_maps, nested_map_idents, nested_map_comps, ctr_specs, ...}
   1.141 +            : corec_spec) (disc_eqns : co_eqn_data_disc list) exclsss
   1.142 +            ({fun_name, fun_T, fun_args, ctr, sel, rhs_term, ...} : co_eqn_data_sel) =
   1.143            let
   1.144              val SOME ctr_spec = find_first (equal ctr o #ctr) ctr_specs;
   1.145              val ctr_no = find_index (equal ctr o #ctr) ctr_specs;
   1.146 @@ -810,7 +817,8 @@
   1.147              |> pair sel
   1.148            end;
   1.149  
   1.150 -        fun prove_ctr disc_alist sel_alist disc_eqns sel_eqns {ctr, disc, sels, collapse, ...} =
   1.151 +        fun prove_ctr disc_alist sel_alist (disc_eqns : co_eqn_data_disc list)
   1.152 +            (sel_eqns : co_eqn_data_sel list) ({ctr, disc, sels, collapse, ...} : corec_ctr_spec) =
   1.153            if not (exists (equal ctr o #ctr) disc_eqns)
   1.154                andalso not (exists (equal ctr o #ctr) sel_eqns)
   1.155              orelse (* don't try to prove theorems when some sel_eqns are missing *)