<commit_before>(*  Title:      HOL/Tools/Nitpick/nitpick_mono.ML
    Author:     <NAME>, <NAME>
    Copyright   2009, 2010

Monotonicity inference for higher-order logic.
*)

signature NITPICK_MONO =
sig
  type hol_context = Nitpick_HOL.hol_context

  val trace : bool Unsynchronized.ref
  val formulas_monotonic :
    hol_context -> bool -> typ -> term list * term list -> bool
  val finitize_funs :
    hol_context -> bool -> (typ option * bool option) list -> typ
    -> term list * term list -> term list * term list
end;

structure Nitpick_Mono : NITPICK_MONO =
struct

open Nitpick_Util
open Nitpick_HOL

type var = int

datatype sign = Plus | Minus
datatype sign_atom = S of sign | V of var

type literal = var * sign

datatype mtyp =
  MAlpha |
  MFun of mtyp * sign_atom * mtyp |
  MPair of mtyp * mtyp |
  MType of string * mtyp list |
  MRec of string * typ list

datatype mterm =
  MRaw of term * mtyp |
  MAbs of string * typ * mtyp * sign_atom * mterm |
  MApp of mterm * mterm

type mdata =
  {hol_ctxt: hol_context,
   binarize: bool,
   alpha_T: typ,
   no_harmless: bool,
   max_fresh: int Unsynchronized.ref,
   datatype_mcache: ((string * typ list) * mtyp) list Unsynchronized.ref,
   constr_mcache: (styp * mtyp) list Unsynchronized.ref}

exception UNSOLVABLE of unit
exception MTYPE of string * mtyp list * typ list
exception MTERM of string * mterm list

val trace = Unsynchronized.ref false
fun trace_msg msg = if !trace then tracing (msg ()) else ()

val string_for_var = signed_string_of_int
fun string_for_vars sep [] = "0\<^bsub>" ^ sep ^ "\<^esub>"
  | string_for_vars sep xs = space_implode sep (map string_for_var xs)
fun subscript_string_for_vars sep xs =
  if null xs then "" else "\<^bsub>" ^ string_for_vars sep xs ^ "\<^esub>"

fun string_for_sign Plus = "+"
  | string_for_sign Minus = "-"

fun xor sn1 sn2 = if sn1 = sn2 then Plus else Minus
val negate = xor Minus

fun string_for_sign_atom (S sn) = string_for_sign sn
  | string_for_sign_atom (V x) = string_for_var x

fun string_for_literal (x, sn) = string_for_var x ^ " = " ^ string_for_sign sn

val bool_M = MType (@{type_name bool}, [])
val dummy_M = MType (nitpick_prefix ^ "dummy", [])

fun is_MRec (MRec _) = true
  | is_MRec _ = false
fun dest_MFun (MFun z) = z
  | dest_MFun M = raise MTYPE ("Nitpick_Mono.dest_MFun", [M], [])

val no_prec = 100

fun precedence_of_mtype (MFun _) = 1
  | precedence_of_mtype (MPair _) = 2
  | precedence_of_mtype _ = no_prec

val string_for_mtype =
  let
    fun aux outer_prec M =
      let
        val prec = precedence_of_mtype M
        val need_parens = (prec < outer_prec)
      in
        (if need_parens then "(" else "") ^
        (if M = dummy_M then
           "_"
         else case M of
             MAlpha => "\<alpha>"
           | MFun (M1, a, M2) =>
             aux (prec + 1) M1 ^ " \<Rightarrow>\<^bsup>" ^
             string_for_sign_atom a ^ "\<^esup> " ^ aux prec M2
           | MPair (M1, M2) => aux (prec + 1) M1 ^ " \<times> " ^ aux prec M2
           | MType (s, []) =>
             if s = @{type_name prop} orelse s = @{type_name bool} then "o"
             else s
           | MType (s, Ms) => "(" ^ commas (map (aux 0) Ms) ^ ") " ^ s
           | MRec (s, _) => "[" ^ s ^ "]") ^
        (if need_parens then ")" else "")
      end
  in aux 0 end

fun flatten_mtype (MPair (M1, M2)) = maps flatten_mtype [M1, M2]
  | flatten_mtype (MType (_, Ms)) = maps flatten_mtype Ms
  | flatten_mtype M = [M]

fun precedence_of_mterm (MRaw _) = no_prec
  | precedence_of_mterm (MAbs _) = 1
  | precedence_of_mterm (MApp _) = 2

fun string_for_mterm ctxt =
  let
    fun mtype_annotation M = "\<^bsup>" ^ string_for_mtype M ^ "\<^esup>"
    fun aux outer_prec m =
      let
        val prec = precedence_of_mterm m
        val need_parens = (prec < outer_prec)
      in
        (if need_parens then "(" else "") ^
        (case m of
           MRaw (t, M) => Syntax.string_of_term ctxt t ^ mtype_annotation M
         | MAbs (s, _, M, a, m) =>
           "\<lambda>" ^ s ^ mtype_annotation M ^ ".\<^bsup>" ^
           string_for_sign_atom a ^ "\<^esup> " ^ aux prec m
         | MApp (m1, m2) => aux prec m1 ^ " " ^ aux (prec + 1) m2) ^
        (if need_parens then ")" else "")
      end
  in aux 0 end

fun mtype_of_mterm (MRaw (_, M)) = M
  | mtype_of_mterm (MAbs (_, _, M, a, m)) = MFun (M, a, mtype_of_mterm m)
  | mtype_of_mterm (MApp (m1, _)) =
    case mtype_of_mterm m1 of
      MFun (_, _, M12) => M12
    | M1 => raise MTYPE ("Nitpick_Mono.mtype_of_mterm", [M1], [])

fun strip_mcomb (MApp (m1, m2)) = strip_mcomb m1 ||> (fn ms => append ms [m2])
  | strip_mcomb m = (m, [])

fun initial_mdata hol_ctxt binarize no_harmless alpha_T =
  ({hol_ctxt = hol_ctxt, binarize = binarize, alpha_T = alpha_T,
    no_harmless = no_harmless, max_fresh = Unsynchronized.ref 0,
    datatype_mcache = Unsynchronized.ref [],
    constr_mcache = Unsynchronized.ref []} : mdata)

fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) =
    T = alpha_T orelse (not (is_fp_iterator_type T) andalso
                        exists (could_exist_alpha_subtype alpha_T) Ts)
  | could_exist_alpha_subtype alpha_T T = (T = alpha_T)
fun could_exist_alpha_sub_mtype _ (alpha_T as TFree _) T =
    could_exist_alpha_subtype alpha_T T
  | could_exist_alpha_sub_mtype ctxt alpha_T T =
    (T = alpha_T orelse is_datatype ctxt [(NONE, true)] T)

fun exists_alpha_sub_mtype MAlpha = true
  | exists_alpha_sub_mtype (MFun (M1, _, M2)) =
    exists exists_alpha_sub_mtype [M1, M2]
  | exists_alpha_sub_mtype (MPair (M1, M2)) =
    exists exists_alpha_sub_mtype [M1, M2]
  | exists_alpha_sub_mtype (MType (_, Ms)) = exists exists_alpha_sub_mtype Ms
  | exists_alpha_sub_mtype (MRec _) = true

fun exists_alpha_sub_mtype_fresh MAlpha = true
  | exists_alpha_sub_mtype_fresh (MFun (_, V _, _)) = true
  | exists_alpha_sub_mtype_fresh (MFun (_, _, M2)) =
    exists_alpha_sub_mtype_fresh M2
  | exists_alpha_sub_mtype_fresh (MPair (M1, M2)) =
    exists exists_alpha_sub_mtype_fresh [M1, M2]
  | exists_alpha_sub_mtype_fresh (MType (_, Ms)) =
    exists exists_alpha_sub_mtype_fresh Ms
  | exists_alpha_sub_mtype_fresh (MRec _) = true

fun constr_mtype_for_binders z Ms =
  fold_rev (fn M => curry3 MFun M (S Minus)) Ms (MRec z)

fun repair_mtype _ _ MAlpha = MAlpha
  | repair_mtype cache seen (MFun (M1, a, M2)) =
    MFun (repair_mtype cache seen M1, a, repair_mtype cache seen M2)
  | repair_mtype cache seen (MPair Mp) =
    MPair (pairself (repair_mtype cache seen) Mp)
  | repair_mtype cache seen (MType (s, Ms)) =
    MType (s, maps (flatten_mtype o repair_mtype cache seen) Ms)
  | repair_mtype cache seen (MRec (z as (s, _))) =
    case AList.lookup (op =) cache z |> the of
      MRec _ => MType (s, [])
    | M => if member (op =) seen M then MType (s, [])
           else repair_mtype cache (M :: seen) M

fun repair_datatype_mcache cache =
  let
    fun repair_one (z, M) =
      Unsynchronized.change cache
          (AList.update (op =) (z, repair_mtype (!cache) [] M))
  in List.app repair_one (rev (!cache)) end

fun repair_constr_mcache dtype_cache constr_mcache =
  let
    fun repair_one (x, M) =
      Unsynchronized.change constr_mcache
          (AList.update (op =) (x, repair_mtype dtype_cache [] M))
  in List.app repair_one (!constr_mcache) end

fun is_fin_fun_supported_type @{typ prop} = true
  | is_fin_fun_supported_type @{typ bool} = true
  | is_fin_fun_supported_type (Type (@{type_name option}, _)) = true
  | is_fin_fun_supported_type _ = false
fun fin_fun_body _ _ (t as @{term False}) = SOME t
  | fin_fun_body _ _ (t as Const (@{const_name None}, _)) = SOME t
  | fin_fun_body dom_T ran_T
                 ((t0 as Const (@{const_name If}, _))
                  $ (t1 as Const (@{const_name HOL.eq}, _) $ Bound 0 $ t1')
                  $ t2 $ t3) =
    (if loose_bvar1 (t1', 0) then
       NONE
     else case fin_fun_body dom_T ran_T t3 of
       NONE => NONE
     | SOME t3 =>
       SOME (t0 $ (Const (@{const_name is_unknown}, dom_T --> bool_T) $ t1')
                $ (Const (@{const_name unknown}, ran_T)) $ (t0 $ t1 $ t2 $ t3)))
  | fin_fun_body _ _ _ = NONE

fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) all_minus
                            T1 T2 =
  let
    val M1 = fresh_mtype_for_type mdata all_minus T1
    val M2 = fresh_mtype_for_type mdata all_minus T2
    val a = if not all_minus andalso exists_alpha_sub_mtype_fresh M1 andalso
               is_fin_fun_supported_type (body_type T2) then
              V (Unsynchronized.inc max_fresh)
            else
              S Minus
  in (M1, a, M2) end
and fresh_mtype_for_type (mdata as {hol_ctxt as {ctxt, ...}, binarize, alpha_T,
                                    datatype_mcache, constr_mcache, ...})
                         all_minus =
  let
    fun do_type T =
      if T = alpha_T then
        MAlpha
      else case T of
        Type (@{type_name fun}, [T1, T2]) =>
        MFun (fresh_mfun_for_fun_type mdata false T1 T2)
      | Type (@{type_name prod}, [T1, T2]) => MPair (pairself do_type (T1, T2))
      | Type (z as (s, _)) =>
        if could_exist_alpha_sub_mtype ctxt alpha_T T then
          case AList.lookup (op =) (!datatype_mcache) z of
            SOME M => M
          | NONE =>
            let
              val _ = Unsynchronized.change datatype_mcache (cons (z, MRec z))
              val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T
              val (all_Ms, constr_Ms) =
                fold_rev (fn (_, T') => fn (all_Ms, constr_Ms) =>
                             let
                               val binder_Ms = map do_type (binder_types T')
                               val new_Ms = filter exists_alpha_sub_mtype_fresh
                                                   binder_Ms
                               val constr_M = constr_mtype_for_binders z
                                                                       binder_Ms
                             in
                               (union (op =) new_Ms all_Ms,
                                constr_M :: constr_Ms)
                             end)
                         xs ([], [])
              val M = MType (s, all_Ms)<commit_msg>correctly thread parameter through<commit_after>(*  Title:      HOL/Tools/Nitpick/nitpick_mono.ML
    Author:     <NAME>, <NAME>
    Copyright   2009, 2010

Monotonicity inference for higher-order logic.
*)

signature NITPICK_MONO =
sig
  type hol_context = Nitpick_HOL.hol_context

  val trace : bool Unsynchronized.ref
  val formulas_monotonic :
    hol_context -> bool -> typ -> term list * term list -> bool
  val finitize_funs :
    hol_context -> bool -> (typ option * bool option) list -> typ
    -> term list * term list -> term list * term list
end;

structure Nitpick_Mono : NITPICK_MONO =
struct

open Nitpick_Util
open Nitpick_HOL

type var = int

datatype sign = Plus | Minus
datatype sign_atom = S of sign | V of var

type literal = var * sign

datatype mtyp =
  MAlpha |
  MFun of mtyp * sign_atom * mtyp |
  MPair of mtyp * mtyp |
  MType of string * mtyp list |
  MRec of string * typ list

datatype mterm =
  MRaw of term * mtyp |
  MAbs of string * typ * mtyp * sign_atom * mterm |
  MApp of mterm * mterm

type mdata =
  {hol_ctxt: hol_context,
   binarize: bool,
   alpha_T: typ,
   no_harmless: bool,
   max_fresh: int Unsynchronized.ref,
   datatype_mcache: ((string * typ list) * mtyp) list Unsynchronized.ref,
   constr_mcache: (styp * mtyp) list Unsynchronized.ref}

exception UNSOLVABLE of unit
exception MTYPE of string * mtyp list * typ list
exception MTERM of string * mterm list

val trace = Unsynchronized.ref false
fun trace_msg msg = if !trace then tracing (msg ()) else ()

val string_for_var = signed_string_of_int
fun string_for_vars sep [] = "0\<^bsub>" ^ sep ^ "\<^esub>"
  | string_for_vars sep xs = space_implode sep (map string_for_var xs)
fun subscript_string_for_vars sep xs =
  if null xs then "" else "\<^bsub>" ^ string_for_vars sep xs ^ "\<^esub>"

fun string_for_sign Plus = "+"
  | string_for_sign Minus = "-"

fun xor sn1 sn2 = if sn1 = sn2 then Plus else Minus
val negate = xor Minus

fun string_for_sign_atom (S sn) = string_for_sign sn
  | string_for_sign_atom (V x) = string_for_var x

fun string_for_literal (x, sn) = string_for_var x ^ " = " ^ string_for_sign sn

val bool_M = MType (@{type_name bool}, [])
val dummy_M = MType (nitpick_prefix ^ "dummy", [])

fun is_MRec (MRec _) = true
  | is_MRec _ = false
fun dest_MFun (MFun z) = z
  | dest_MFun M = raise MTYPE ("Nitpick_Mono.dest_MFun", [M], [])

val no_prec = 100

fun precedence_of_mtype (MFun _) = 1
  | precedence_of_mtype (MPair _) = 2
  | precedence_of_mtype _ = no_prec

val string_for_mtype =
  let
    fun aux outer_prec M =
      let
        val prec = precedence_of_mtype M
        val need_parens = (prec < outer_prec)
      in
        (if need_parens then "(" else "") ^
        (if M = dummy_M then
           "_"
         else case M of
             MAlpha => "\<alpha>"
           | MFun (M1, a, M2) =>
             aux (prec + 1) M1 ^ " \<Rightarrow>\<^bsup>" ^
             string_for_sign_atom a ^ "\<^esup> " ^ aux prec M2
           | MPair (M1, M2) => aux (prec + 1) M1 ^ " \<times> " ^ aux prec M2
           | MType (s, []) =>
             if s = @{type_name prop} orelse s = @{type_name bool} then "o"
             else s
           | MType (s, Ms) => "(" ^ commas (map (aux 0) Ms) ^ ") " ^ s
           | MRec (s, _) => "[" ^ s ^ "]") ^
        (if need_parens then ")" else "")
      end
  in aux 0 end

fun flatten_mtype (MPair (M1, M2)) = maps flatten_mtype [M1, M2]
  | flatten_mtype (MType (_, Ms)) = maps flatten_mtype Ms
  | flatten_mtype M = [M]

fun precedence_of_mterm (MRaw _) = no_prec
  | precedence_of_mterm (MAbs _) = 1
  | precedence_of_mterm (MApp _) = 2

fun string_for_mterm ctxt =
  let
    fun mtype_annotation M = "\<^bsup>" ^ string_for_mtype M ^ "\<^esup>"
    fun aux outer_prec m =
      let
        val prec = precedence_of_mterm m
        val need_parens = (prec < outer_prec)
      in
        (if need_parens then "(" else "") ^
        (case m of
           MRaw (t, M) => Syntax.string_of_term ctxt t ^ mtype_annotation M
         | MAbs (s, _, M, a, m) =>
           "\<lambda>" ^ s ^ mtype_annotation M ^ ".\<^bsup>" ^
           string_for_sign_atom a ^ "\<^esup> " ^ aux prec m
         | MApp (m1, m2) => aux prec m1 ^ " " ^ aux (prec + 1) m2) ^
        (if need_parens then ")" else "")
      end
  in aux 0 end

fun mtype_of_mterm (MRaw (_, M)) = M
  | mtype_of_mterm (MAbs (_, _, M, a, m)) = MFun (M, a, mtype_of_mterm m)
  | mtype_of_mterm (MApp (m1, _)) =
    case mtype_of_mterm m1 of
      MFun (_, _, M12) => M12
    | M1 => raise MTYPE ("Nitpick_Mono.mtype_of_mterm", [M1], [])

fun strip_mcomb (MApp (m1, m2)) = strip_mcomb m1 ||> (fn ms => append ms [m2])
  | strip_mcomb m = (m, [])

fun initial_mdata hol_ctxt binarize no_harmless alpha_T =
  ({hol_ctxt = hol_ctxt, binarize = binarize, alpha_T = alpha_T,
    no_harmless = no_harmless, max_fresh = Unsynchronized.ref 0,
    datatype_mcache = Unsynchronized.ref [],
    constr_mcache = Unsynchronized.ref []} : mdata)

fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) =
    T = alpha_T orelse (not (is_fp_iterator_type T) andalso
                        exists (could_exist_alpha_subtype alpha_T) Ts)
  | could_exist_alpha_subtype alpha_T T = (T = alpha_T)
fun could_exist_alpha_sub_mtype _ (alpha_T as TFree _) T =
    could_exist_alpha_subtype alpha_T T
  | could_exist_alpha_sub_mtype ctxt alpha_T T =
    (T = alpha_T orelse is_datatype ctxt [(NONE, true)] T)

fun exists_alpha_sub_mtype MAlpha = true
  | exists_alpha_sub_mtype (MFun (M1, _, M2)) =
    exists exists_alpha_sub_mtype [M1, M2]
  | exists_alpha_sub_mtype (MPair (M1, M2)) =
    exists exists_alpha_sub_mtype [M1, M2]
  | exists_alpha_sub_mtype (MType (_, Ms)) = exists exists_alpha_sub_mtype Ms
  | exists_alpha_sub_mtype (MRec _) = true

fun exists_alpha_sub_mtype_fresh MAlpha = true
  | exists_alpha_sub_mtype_fresh (MFun (_, V _, _)) = true
  | exists_alpha_sub_mtype_fresh (MFun (_, _, M2)) =
    exists_alpha_sub_mtype_fresh M2
  | exists_alpha_sub_mtype_fresh (MPair (M1, M2)) =
    exists exists_alpha_sub_mtype_fresh [M1, M2]
  | exists_alpha_sub_mtype_fresh (MType (_, Ms)) =
    exists exists_alpha_sub_mtype_fresh Ms
  | exists_alpha_sub_mtype_fresh (MRec _) = true

fun constr_mtype_for_binders z Ms =
  fold_rev (fn M => curry3 MFun M (S Minus)) Ms (MRec z)

fun repair_mtype _ _ MAlpha = MAlpha
  | repair_mtype cache seen (MFun (M1, a, M2)) =
    MFun (repair_mtype cache seen M1, a, repair_mtype cache seen M2)
  | repair_mtype cache seen (MPair Mp) =
    MPair (pairself (repair_mtype cache seen) Mp)
  | repair_mtype cache seen (MType (s, Ms)) =
    MType (s, maps (flatten_mtype o repair_mtype cache seen) Ms)
  | repair_mtype cache seen (MRec (z as (s, _))) =
    case AList.lookup (op =) cache z |> the of
      MRec _ => MType (s, [])
    | M => if member (op =) seen M then MType (s, [])
           else repair_mtype cache (M :: seen) M

fun repair_datatype_mcache cache =
  let
    fun repair_one (z, M) =
      Unsynchronized.change cache
          (AList.update (op =) (z, repair_mtype (!cache) [] M))
  in List.app repair_one (rev (!cache)) end

fun repair_constr_mcache dtype_cache constr_mcache =
  let
    fun repair_one (x, M) =
      Unsynchronized.change constr_mcache
          (AList.update (op =) (x, repair_mtype dtype_cache [] M))
  in List.app repair_one (!constr_mcache) end

fun is_fin_fun_supported_type @{typ prop} = true
  | is_fin_fun_supported_type @{typ bool} = true
  | is_fin_fun_supported_type (Type (@{type_name option}, _)) = true
  | is_fin_fun_supported_type _ = false
fun fin_fun_body _ _ (t as @{term False}) = SOME t
  | fin_fun_body _ _ (t as Const (@{const_name None}, _)) = SOME t
  | fin_fun_body dom_T ran_T
                 ((t0 as Const (@{const_name If}, _))
                  $ (t1 as Const (@{const_name HOL.eq}, _) $ Bound 0 $ t1')
                  $ t2 $ t3) =
    (if loose_bvar1 (t1', 0) then
       NONE
     else case fin_fun_body dom_T ran_T t3 of
       NONE => NONE
     | SOME t3 =>
       SOME (t0 $ (Const (@{const_name is_unknown}, dom_T --> bool_T) $ t1')
                $ (Const (@{const_name unknown}, ran_T)) $ (t0 $ t1 $ t2 $ t3)))
  | fin_fun_body _ _ _ = NONE

fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) all_minus
                            T1 T2 =
  let
    val M1 = fresh_mtype_for_type mdata all_minus T1
    val M2 = fresh_mtype_for_type mdata all_minus T2
    val a = if not all_minus andalso exists_alpha_sub_mtype_fresh M1 andalso
               is_fin_fun_supported_type (body_type T2) then
              V (Unsynchronized.inc max_fresh)
            else
              S Minus
  in (M1, a, M2) end
and fresh_mtype_for_type (mdata as {hol_ctxt as {ctxt, ...}, binarize, alpha_T,
                                    datatype_mcache, constr_mcache, ...})
                         all_minus =
  let
    fun do_type T =
      if T = alpha_T then
        MAlpha
      else case T of
        Type (@{type_name fun}, [T1, T2]) =>
        MFun (fresh_mfun_for_fun_type mdata all_minus T1 T2)
      | Type (@{type_name prod}, [T1, T2]) => MPair (pairself do_type (T1, T2))
      | Type (z as (s, _)) =>
        if could_exist_alpha_sub_mtype ctxt alpha_T T then
          case AList.lookup (op =) (!datatype_mcache) z of
            SOME M => M
          | NONE =>
            let
              val _ = Unsynchronized.change datatype_mcache (cons (z, MRec z))
              val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T
              val (all_Ms, constr_Ms) =
                fold_rev (fn (_, T') => fn (all_Ms, constr_Ms) =>
                             let
                               val binder_Ms = map do_type (binder_types T')
                               val new_Ms = filter exists_alpha_sub_mtype_fresh
                                                   binder_Ms
                               val constr_M = constr_mtype_for_binders z
                                                                       binder_Ms
                             in
                               (union (op =) new_Ms all_Ms,
                                constr_M :: constr_Ms)
                             end)
                         xs ([], [])
              val M = MType (s, all_Ms)
{'fraction_non_alphanumeric': 0.1043878100083158, 'fraction_numerical': 0.01066379689869393, 'mean_word_length': 2.396013289036545, 'pattern_counts': {'":': 0, '<': 39, '<?xml version=': 0, '>': 107, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 18, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2349475', 'n_tokens_mistral': 7597, 'n_tokens_neox': 7461, 'n_words': 2078}