<commit_before>(*  Title:      HOL/BNF/Tools/bnf_lfp_compat.ML
    Author:     <NAME>, <NAME>
    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 orelse s = @{type_name fun} then
        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\")"));<commit_msg>warn about incompatible recursor signature<commit_after>(*  Title:      HOL/BNF/Tools/bnf_lfp_compat.ML
    Author:     <NAME>, <NAME>
    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\")"));
{'fraction_non_alphanumeric': 0.0981368454866688, 'fraction_numerical': 0.0057822036620623195, 'mean_word_length': 2.6824364281490243, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 35, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '911943', 'n_tokens_mistral': 2341, 'n_tokens_neox': 2248, 'n_words': 656}