(*  Title:      HOL/BNF/Tools/bnf_lfp_compat.ML

    Author:     Jasmin Blanchette, TU Muenchen

    Copyright   2013

Compatibility layer with the old datatype package.

*)

signature BNF_LFP_COMPAT =

sig

  val datatype_new_compat_cmd : string list -> local_theory -> local_theory

end;

structure BNF_LFP_Compat : BNF_LFP_COMPAT =

struct

open Ctr_Sugar

open BNF_Util

open BNF_FP_Util

open BNF_FP_Def_Sugar

open BNF_FP_N2M_Sugar

fun dtyp_of_typ _ (TFree a) = Datatype_Aux.DtTFree a

  | dtyp_of_typ recTs (T as Type (s, Ts)) =

    (case find_index (curry (op =) T) recTs of

      ~1 => Datatype_Aux.DtType (s, map (dtyp_of_typ recTs) Ts)

    | kk => Datatype_Aux.DtRec kk);

val compatN = "compat_";

(* TODO: graceful failure for local datatypes -- perhaps by making the command global *)

fun datatype_new_compat_cmd raw_fpT_names lthy =

  let

    val thy = Proof_Context.theory_of lthy;

    fun not_datatype s = error (quote s ^ " is not a new-style datatype");

    fun not_mutually_recursive ss =

      error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive new-style datatypes");

    val (fpT_names as fpT_name1 :: _) =

      map (fst o dest_Type o Proof_Context.read_type_name_proper lthy false) raw_fpT_names;

    val Ss = Sign.arity_sorts thy fpT_name1 HOLogic.typeS;

    val (unsorted_As, _) = lthy |> mk_TFrees (length Ss);

    val As = map2 resort_tfree Ss unsorted_As;

    fun lfp_sugar_of s =

      (case fp_sugar_of lthy s of

        SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar

      | _ => not_datatype s);

    val fp_sugar0 as {fp_res = {Ts = fpTs0, ...}, ...} = lfp_sugar_of fpT_name1;

    val fpT_names' = map (fst o dest_Type) fpTs0;

    val _ = eq_set (op =) (fpT_names, fpT_names') orelse not_mutually_recursive fpT_names;

    val fpTs as fpT1 :: _ = map (fn s => Type (s, As)) fpT_names';

    fun add_nested_types_of (T as Type (s, _)) seen =

      if member (op =) seen T then

        seen

      else if s = @{type_name fun} then

        (warning "Partial support for recursion through functions -- 'primrec' will fail"; seen)

      else

        (case try lfp_sugar_of s of

          SOME ({T = T0, fp_res = {Ts = mutual_Ts0, ...}, ctr_sugars, ...}) =>

          let

            val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T0, T) Vartab.empty) [];

            val substT = Term.typ_subst_TVars rho;

            val mutual_Ts = map substT mutual_Ts0;

            fun add_interesting_subtypes (U as Type (_, Us)) =

                (case filter (exists_subtype_in mutual_Ts) Us of [] => I

                | Us' => insert (op =) U #> fold add_interesting_subtypes Us')

              | add_interesting_subtypes _ = I;

            val ctrs = maps #ctrs ctr_sugars;

            val ctr_Ts = maps (binder_types o substT o fastype_of) ctrs |> distinct (op =);

            val subTs = fold add_interesting_subtypes ctr_Ts [];

          in

            fold add_nested_types_of subTs (seen @ mutual_Ts)

          end

        | NONE => error ("Unsupported recursion via type constructor " ^ quote s ^

            " not associated with new-style datatype (cf. \"datatype_new\")"));

    val Ts = add_nested_types_of fpT1 [];

    val b_names = map base_name_of_typ Ts;

    val compat_b_names = map (prefix compatN) b_names;

    val compat_bs = map Binding.name compat_b_names;

    val common_name = compatN ^ mk_common_name b_names;

    val nn_fp = length fpTs;

    val nn = length Ts;

    val get_indices = K [];

    val fp_sugars0 = if nn = 1 then [fp_sugar0] else map (lfp_sugar_of o fst o dest_Type) Ts;

    val callssss = map (fn fp_sugar0 => indexify_callsss fp_sugar0 []) fp_sugars0;

    val ((fp_sugars, (lfp_sugar_thms, _)), lthy) =

      if nn > nn_fp then

        mutualize_fp_sugars Least_FP compat_bs Ts get_indices callssss fp_sugars0 lthy

      else

        ((fp_sugars0, (NONE, NONE)), lthy);

    val {ctr_sugars, co_inducts = [induct], co_iterss, co_iter_thmsss = iter_thmsss, ...} :: _ =

      fp_sugars;

    val inducts = conj_dests nn induct;

    val frozen_Ts = map Type.legacy_freeze_type Ts;

    val mk_dtyp = dtyp_of_typ frozen_Ts;

    fun mk_ctr_descr (Const (s, T)) =

      (s, map mk_dtyp (binder_types (Type.legacy_freeze_type T)));

    fun mk_typ_descr index (Type (T_name, Ts)) ({ctrs, ...} : ctr_sugar) =

      (index, (T_name, map mk_dtyp Ts, map mk_ctr_descr ctrs));

    val descr = map3 mk_typ_descr (0 upto nn - 1) frozen_Ts ctr_sugars;

    val recs = map (fst o dest_Const o co_rec_of) co_iterss;

    val rec_thms = flat (map co_rec_of iter_thmsss);

    fun mk_info ({T = Type (T_name0, _), index, ...} : fp_sugar) =

      let

        val {casex, exhaust, nchotomy, injects, distincts, case_thms, case_cong, weak_case_cong,

          split, split_asm, ...} = nth ctr_sugars index;

      in

        (T_name0,

         {index = index, descr = descr, inject = injects, distinct = distincts, induct = induct,

         inducts = inducts, exhaust = exhaust, nchotomy = nchotomy, rec_names = recs,

         rec_rewrites = rec_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms,

         case_cong = case_cong, weak_case_cong = weak_case_cong, split = split,

         split_asm = split_asm})

      end;

    val infos = map mk_info (take nn_fp fp_sugars);

    val all_notes =

      (case lfp_sugar_thms of

        NONE => []

      | SOME ((induct_thms, induct_thm, induct_attrs), (fold_thmss, rec_thmss, _)) =>

        let

          val common_notes =

            (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else [])

            |> filter_out (null o #2)

            |> map (fn (thmN, thms, attrs) =>

              ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])]));

          val notes =

            [(foldN, fold_thmss, []),

             (inductN, map single induct_thms, induct_attrs),

             (recN, rec_thmss, [])]

            |> filter_out (null o #2)

            |> maps (fn (thmN, thmss, attrs) =>

              if forall null thmss then

                []

              else

                map2 (fn b_name => fn thms =>

                    ((Binding.qualify true b_name (Binding.name thmN), attrs), [(thms, [])]))

                  compat_b_names thmss);

        in

          common_notes @ notes

        end);

    val register_interpret =

      Datatype_Data.register infos

      #> Datatype_Data.interpretation_data (Datatype_Aux.default_config, map fst infos)

  in

    lthy

    |> Local_Theory.raw_theory register_interpret

    |> Local_Theory.notes all_notes |> snd

  end;

val _ =

  Outer_Syntax.local_theory @{command_spec "datatype_new_compat"}

    "register new-style datatypes as old-style datatypes"

    (Scan.repeat1 Parse.type_const >> datatype_new_compat_cmd);

end;