<commit_before>(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open CErrors
open Util
open Names
open Constr
open Context
open Termops
open Univ
open Evd
open Environ
open EConstr
open Vars
open Context.Rel.Declaration

exception Elimconst

(** This module implements a call by name reduction used by (at
    least) evarconv unification and cbn tactic.

    It has an ability to "refold" constants by storing constants and
    their parameters in its stack.
*)

let () = Goptions.(declare_bool_option {
  optdepr = false;
  optname =
    "Generate weak constraints between Irrelevant universes";
  optkey = ["Cumulativity";"Weak";"Constraints"];
  optread = (fun () -> not !UState.drop_weak_constraints);
  optwrite = (fun a -> UState.drop_weak_constraints:=not a);
})


(** Support for reduction effects *)

open Mod_subst
open Libobject

type effect_name = string

(** create a persistent set to store effect functions *)

(* Table bindings a constant to an effect *)
let constant_effect_table = Summary.ref ~name:"reduction-side-effect" Cmap.empty

(* Table bindings function key to effective functions *)
let effect_table = Summary.ref ~name:"reduction-function-effect" String.Map.empty

(** a test to know whether a constant is actually the effect function *)
let reduction_effect_hook env sigma con c =
  try
    let funkey = Cmap.find con !constant_effect_table in
    let effect = String.Map.find funkey !effect_table in
    effect env sigma (Lazy.force c)
  with Not_found -> ()

let cache_reduction_effect (_,(con,funkey)) =
  constant_effect_table := Cmap.add con funkey !constant_effect_table

let subst_reduction_effect (subst,(con,funkey)) =
  (subst_constant subst con,funkey)

let inReductionEffect : Constant.t * string -> obj =
  declare_object @@ global_object_nodischarge "REDUCTION-EFFECT"
    ~cache:cache_reduction_effect
    ~subst:(Some subst_reduction_effect)

let declare_reduction_effect funkey f =
  if String.Map.mem funkey !effect_table then
    CErrors.anomaly Pp.(str "Cannot redeclare effect function " ++ qstring funkey ++ str ".");
  effect_table := String.Map.add funkey f !effect_table

(** A function to set the value of the print function *)
let set_reduction_effect x funkey =
  Lib.add_anonymous_leaf (inReductionEffect (x,funkey))


(** Machinery to custom the behavior of the reduction *)<commit_msg>Don't store closures in summary (reduction effects)<commit_after>(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open CErrors
open Util
open Names
open Constr
open Context
open Termops
open Univ
open Evd
open Environ
open EConstr
open Vars
open Context.Rel.Declaration

exception Elimconst

(** This module implements a call by name reduction used by (at
    least) evarconv unification and cbn tactic.

    It has an ability to "refold" constants by storing constants and
    their parameters in its stack.
*)

let () = Goptions.(declare_bool_option {
  optdepr = false;
  optname =
    "Generate weak constraints between Irrelevant universes";
  optkey = ["Cumulativity";"Weak";"Constraints"];
  optread = (fun () -> not !UState.drop_weak_constraints);
  optwrite = (fun a -> UState.drop_weak_constraints:=not a);
})


(** Support for reduction effects *)

open Mod_subst
open Libobject

type effect_name = string

(** create a persistent set to store effect functions *)

(* Table bindings a constant to an effect *)
let constant_effect_table = Summary.ref ~name:"reduction-side-effect" Cmap.empty

(* Table bindings function key to effective functions *)
let effect_table = ref String.Map.empty

(** a test to know whether a constant is actually the effect function *)
let reduction_effect_hook env sigma con c =
  try
    let funkey = Cmap.find con !constant_effect_table in
    let effect = String.Map.find funkey !effect_table in
    effect env sigma (Lazy.force c)
  with Not_found -> ()

let cache_reduction_effect (_,(con,funkey)) =
  constant_effect_table := Cmap.add con funkey !constant_effect_table

let subst_reduction_effect (subst,(con,funkey)) =
  (subst_constant subst con,funkey)

let inReductionEffect : Constant.t * string -> obj =
  declare_object @@ global_object_nodischarge "REDUCTION-EFFECT"
    ~cache:cache_reduction_effect
    ~subst:(Some subst_reduction_effect)

let declare_reduction_effect funkey f =
  if String.Map.mem funkey !effect_table then
    CErrors.anomaly Pp.(str "Cannot redeclare effect function " ++ qstring funkey ++ str ".");
  effect_table := String.Map.add funkey f !effect_table

(** A function to set the value of the print function *)
let set_reduction_effect x funkey =
  Lib.add_anonymous_leaf (inReductionEffect (x,funkey))


(** Machinery to custom the behavior of the reduction *)
{'fraction_non_alphanumeric': 0.15286195286195287, 'fraction_numerical': 0.003367003367003367, 'mean_word_length': 3.9798826487845766, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 11, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4979202', 'n_tokens_mistral': 1715, 'n_tokens_neox': 1615, 'n_words': 579}