<commit_before>(*  Title:      HOL/Tools/SMT/smt_utils.ML
    Author:     <NAME>, <NAME>

General utility functions.
*)

signature SMT_UTILS =
sig
  (*basic combinators*)
  val repeat: ('a -> 'a option) -> 'a -> 'a
  val repeat_yield: ('a -> 'b -> ('a * 'b) option) -> 'a -> 'b -> 'a * 'b

  (*class dictionaries*)
  type class = string list
  val basicC: class
  val string_of_class: class -> string
  type 'a dict = (class * 'a) Ord_List.T
  val dict_map_default: class * 'a -> ('a -> 'a) -> 'a dict -> 'a dict
  val dict_update: class * 'a -> 'a dict -> 'a dict
  val dict_merge: ('a * 'a -> 'a) -> 'a dict * 'a dict -> 'a dict
  val dict_lookup: 'a dict -> class -> 'a list
  val dict_get: 'a dict -> class -> 'a option

  (*types*)
  val dest_funT: int -> typ -> typ list * typ

  (*terms*)
  val dest_conj: term -> term * term
  val dest_disj: term -> term * term
  val under_quant: (term -> 'a) -> term -> 'a
  val is_number: term -> bool

  (*patterns and instantiations*)
  val mk_const_pat: theory -> string -> (ctyp -> 'a) -> 'a * cterm
  val destT1: ctyp -> ctyp
  val destT2: ctyp -> ctyp
  val instTs: ctyp list -> ctyp list * cterm -> cterm
  val instT: ctyp -> ctyp * cterm -> cterm
  val instT': cterm -> ctyp * cterm -> cterm

  (*certified terms*)
  val certify: Proof.context -> term -> cterm
  val typ_of: cterm -> typ
  val dest_cabs: cterm -> Proof.context -> cterm * Proof.context
  val dest_all_cabs: cterm -> Proof.context -> cterm * Proof.context
  val dest_cbinder: cterm -> Proof.context -> cterm * Proof.context
  val dest_all_cbinders: cterm -> Proof.context -> cterm * Proof.context
  val mk_cprop: cterm -> cterm
  val dest_cprop: cterm -> cterm
  val mk_cequals: cterm -> cterm -> cterm
  val term_of: cterm -> term
  val prop_of: thm -> term

  (*conversions*)
  val if_conv: (term -> bool) -> conv -> conv -> conv
  val if_true_conv: (term -> bool) -> conv -> conv
  val if_exists_conv: (term -> bool) -> conv -> conv
  val binders_conv: (Proof.context -> conv) -> Proof.context -> conv
  val under_quant_conv: (Proof.context * cterm list -> conv) ->
    Proof.context -> conv
  val prop_conv: conv -> conv
end

structure SMT_Utils: SMT_UTILS =
struct

(* basic combinators *)

fun repeat f =
  let fun rep x = (case f x of SOME y => rep y | NONE => x)
  in rep end

fun repeat_yield f =
  let fun rep x y = (case f x y of SOME (x', y') => rep x' y' | NONE => (x, y))
  in rep end


(* class dictionaries *)

type class = string list

val basicC = []

fun string_of_class [] = "basic"
  | string_of_class cs = "basic." ^ space_implode "." cs

type 'a dict = (class * 'a) Ord_List.T

fun class_ord ((cs1, _), (cs2, _)) = list_ord fast_string_ord (cs1, cs2)

fun dict_insert (cs, x) d =
  if AList.defined (op =) d cs then d
  else Ord_List.insert class_ord (cs, x) d

fun dict_map_default (cs, x) f =
  dict_insert (cs, x) #> AList.map_entry (op =) cs f

fun dict_update (e as (_, x)) = dict_map_default e (K x)

fun dict_merge val_merge = sort class_ord o AList.join (op =) (K val_merge)<commit_msg>derived SMT solver classes override inherited properties (properties of derived classes have a higher priority than properties of base classes)<commit_after>(*  Title:      HOL/Tools/SMT/smt_utils.ML
    Author:     <NAME>, <NAME>

General utility functions.
*)

signature SMT_UTILS =
sig
  (*basic combinators*)
  val repeat: ('a -> 'a option) -> 'a -> 'a
  val repeat_yield: ('a -> 'b -> ('a * 'b) option) -> 'a -> 'b -> 'a * 'b

  (*class dictionaries*)
  type class = string list
  val basicC: class
  val string_of_class: class -> string
  type 'a dict = (class * 'a) Ord_List.T
  val dict_map_default: class * 'a -> ('a -> 'a) -> 'a dict -> 'a dict
  val dict_update: class * 'a -> 'a dict -> 'a dict
  val dict_merge: ('a * 'a -> 'a) -> 'a dict * 'a dict -> 'a dict
  val dict_lookup: 'a dict -> class -> 'a list
  val dict_get: 'a dict -> class -> 'a option

  (*types*)
  val dest_funT: int -> typ -> typ list * typ

  (*terms*)
  val dest_conj: term -> term * term
  val dest_disj: term -> term * term
  val under_quant: (term -> 'a) -> term -> 'a
  val is_number: term -> bool

  (*patterns and instantiations*)
  val mk_const_pat: theory -> string -> (ctyp -> 'a) -> 'a * cterm
  val destT1: ctyp -> ctyp
  val destT2: ctyp -> ctyp
  val instTs: ctyp list -> ctyp list * cterm -> cterm
  val instT: ctyp -> ctyp * cterm -> cterm
  val instT': cterm -> ctyp * cterm -> cterm

  (*certified terms*)
  val certify: Proof.context -> term -> cterm
  val typ_of: cterm -> typ
  val dest_cabs: cterm -> Proof.context -> cterm * Proof.context
  val dest_all_cabs: cterm -> Proof.context -> cterm * Proof.context
  val dest_cbinder: cterm -> Proof.context -> cterm * Proof.context
  val dest_all_cbinders: cterm -> Proof.context -> cterm * Proof.context
  val mk_cprop: cterm -> cterm
  val dest_cprop: cterm -> cterm
  val mk_cequals: cterm -> cterm -> cterm
  val term_of: cterm -> term
  val prop_of: thm -> term

  (*conversions*)
  val if_conv: (term -> bool) -> conv -> conv -> conv
  val if_true_conv: (term -> bool) -> conv -> conv
  val if_exists_conv: (term -> bool) -> conv -> conv
  val binders_conv: (Proof.context -> conv) -> Proof.context -> conv
  val under_quant_conv: (Proof.context * cterm list -> conv) ->
    Proof.context -> conv
  val prop_conv: conv -> conv
end

structure SMT_Utils: SMT_UTILS =
struct

(* basic combinators *)

fun repeat f =
  let fun rep x = (case f x of SOME y => rep y | NONE => x)
  in rep end

fun repeat_yield f =
  let fun rep x y = (case f x y of SOME (x', y') => rep x' y' | NONE => (x, y))
  in rep end


(* class dictionaries *)

type class = string list

val basicC = []

fun string_of_class [] = "basic"
  | string_of_class cs = "basic." ^ space_implode "." cs

type 'a dict = (class * 'a) Ord_List.T

fun class_ord ((cs1, _), (cs2, _)) =
  rev_order (list_ord fast_string_ord (cs1, cs2))

fun dict_insert (cs, x) d =
  if AList.defined (op =) d cs then d
  else Ord_List.insert class_ord (cs, x) d

fun dict_map_default (cs, x) f =
  dict_insert (cs, x) #> AList.map_entry (op =) cs f

fun dict_update (e as (_, x)) = dict_map_default e (K x)

fun dict_merge val_merge = sort class_ord o AList.join (op =) (K val_merge)
{'fraction_non_alphanumeric': 0.145799806887673, 'fraction_numerical': 0.0019311232700354038, 'mean_word_length': 2.956078930617441, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 169, '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': '1053996', 'n_tokens_mistral': 2335, 'n_tokens_neox': 2276, 'n_words': 793}