<commit_before>(*  Title:      Pure/General/same.ML
    Author:     Makarius

Support for copy-avoiding functions on pure values, at the cost of
readability.
*)

signature SAME =
sig
  exception SAME
  type ('a, 'b) function = 'a -> 'b  (*exception SAME*)
  type 'a operation = ('a, 'a) function  (*exception SAME*)
  val commit: 'a operation -> 'a -> 'a
  val function: ('a -> 'b option) -> ('a, 'b) function
  val capture: ('a, 'b) function -> 'a -> 'b option
  val map: 'a operation -> 'a list operation
  val map_option: ('a, 'b) function -> ('a option, 'b option) function
end;

structure Same: SAME =
struct

exception SAME;

type ('a, 'b) function = 'a -> 'b;
type 'a operation = ('a, 'a) function;

fun commit f x = f x handle SAME => x;

fun capture f x = SOME (f x) handle SAME => NONE;

fun function f x =<commit_msg>added same;<commit_after>(*  Title:      Pure/General/same.ML
    Author:     Makarius

Support for copy-avoiding functions on pure values, at the cost of
readability.
*)

signature SAME =
sig
  exception SAME
  type ('a, 'b) function = 'a -> 'b  (*exception SAME*)
  type 'a operation = ('a, 'a) function  (*exception SAME*)
  val same: ('a, 'b) function
  val commit: 'a operation -> 'a -> 'a
  val function: ('a -> 'b option) -> ('a, 'b) function
  val capture: ('a, 'b) function -> 'a -> 'b option
  val map: 'a operation -> 'a list operation
  val map_option: ('a, 'b) function -> ('a option, 'b option) function
end;

structure Same: SAME =
struct

exception SAME;

type ('a, 'b) function = 'a -> 'b;
type 'a operation = ('a, 'a) function;

fun same _ = raise SAME;
fun commit f x = f x handle SAME => x;

fun capture f x = SOME (f x) handle SAME => NONE;

fun function f x =
{'fraction_non_alphanumeric': 0.15389116442363956, 'fraction_numerical': 0.0, 'mean_word_length': 3.2222222222222223, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 27, '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': '323699', 'n_tokens_mistral': 602, 'n_tokens_neox': 581, 'n_words': 248}