<commit_before>(*----
  Name: context.mli
  Copyright <NAME> 2012
  Author: <NAME>  <<EMAIL>>

  This file is part of HSeq

  HSeq is free software; you can redistribute it and/or modify it under
  the terms of the Lesser GNU General Public License as published by
  the Free Software Foundation; either version 3, or (at your option)
  any later version.

  HSeq is distributed in the hope that it will be useful, but WITHOUT
  ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
  FITNESS FOR A PARTICULAR PURPOSE.  See the Lesser GNU General Public
  License for more details.

  You should have received a copy of the Lesser GNU General Public
  License along with HSeq.  If not see <http://www.gnu.org/licenses/>.
  ----*)

(** Default values. *)
module Default:
sig

  (** {6 File handling} *)

  (** [load n]: Load file [n]. *)
  val load : string -> unit

  (** [use ?silent n]: Use script [n]. *)
  val use : ?silent:bool -> string -> unit

  (** {6 Theories} *)

  (** The empty theory string. *)
  val empty_thy_name: string

  (** The name of the base theory. *)
  val base_thy_name:string
end

(** The theorem prover context. *)

(** Types *)

(** File handling functions *)
type file_t =
  {
    (** [load f]: Load a byte-code file [f] into memory. *)
    load_f: string -> unit;

    (** [use ?silent f]: Read file [f] as a script.  If
        [silent=true], do not report any information. *)
    use_f: ?silent:bool -> string -> unit;

    (** [build ?silent th]: Build theory [th] from a script.
        [silent=true], do not report any information.  @raise
        Failure on failure. *)
    build_f: ?silent:bool -> string -> unit;

    (** [path]: List of directories to search for theories,
        libraries and scripts.*)
    path_f: string list;

    (** suffix: List of possible suffixes for an object file. *)
    obj_suffix_f: string list;

    (** thy_suffix: Suffix for a theory file. *)
    thy_suffix_f: string;

    (** script_suffix: Suffix for a script file. *)
    script_suffix_f: string;
  }

(* The default value for [file_t]. *)
val empty_file_t: unit -> file_t

(** Theory data *)
type thy_t =
  {
    (** Name of the theory on which all user theories are based *)
    base_name_f: string option;

    (** The theory data-base. *)
    thydb_f: Thydb.thydb;

    (** Information needed for the theory database loader. *)
    loader_data_f: Thydb.Loader.data
  }

(** [empty_thy_t()]: The default value for [thy_t]. *)
val empty_thy_t: unit -> thy_t

(** Pretty printer *)
type pp_t =
  {
    pp_info_f: Printer.ppinfo ref;
  }

  (** Parsers *)
type parser_t =
  {
    parser_info_f: Parser.Table.t ref;
  }

(** [empty_pp_t()]: The default value for [pp_t]. *)
val empty_pp_t: unit -> pp_t

(** Top-level context *)
type t = 
  {
    (** Hooks for file handling functions *)
    file_f: file_t;

    (** Theory data *)
    thys_f: thy_t;

    (** Pretty printer *)
    pp_f: pp_t;

    (** Parsers *)
    parser_f: parser_t;
    
    (** A list of functions to invoke on a theory when it is added
        to the data-base. *)
    load_functions_f: (t -> Theory.contents -> t) list;

    (** Theorems caches *)
    thm_cache_f: (Ident.t, Logic.thm) Hashtbl.t;

    (** Scope attached to this context. *)
    scope_f: Scope.t;
  }

(** [empty()]: The empty context. *)
val empty: unit -> t

(** {6 Scoped contexts} *)

val scope_of: t -> Scope.t
(** Get the scope *)

val set_scope: t -> Scope.t -> t
(** Set the scope *)

(** {5 Accessor Functions} *)

(** {6 File handling} *)

val set_loader : t -> (string -> unit) -> t
(** [set_loader f t]: Set the file-loading function in context [t] to [f]. *)

val loader : t -> (string -> unit)
(** [loader t]: Get the file-loading function of context [t]. *)

val set_scripter : t -> (?silent:bool -> string -> unit) -> t
(** [set_use f t]: Set the script-loading function in context [t] to [f]. *)

val scripter: t -> (?silent:bool -> string -> unit)
(** [use t]: Get the script-loading function of context [t]. *)

val set_builder : t ->  (?silent:bool -> string -> unit) -> t
(** [set_use f t]: Set the script-loading function in context [t] to [f]. *)

val builder : t -> (?silent:bool -> string -> unit)
(** [use t]: Get the theory function of context [t]. *)
<commit_msg>Commentary.<commit_after>(*----
  Name: context.mli
  Copyright <NAME> 2012
  Author: <NAME>  <<EMAIL>>

  This file is part of HSeq

  HSeq is free software; you can redistribute it and/or modify it under
  the terms of the Lesser GNU General Public License as published by
  the Free Software Foundation; either version 3, or (at your option)
  any later version.

  HSeq is distributed in the hope that it will be useful, but WITHOUT
  ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
  FITNESS FOR A PARTICULAR PURPOSE.  See the Lesser GNU General Public
  License for more details.

  You should have received a copy of the Lesser GNU General Public
  License along with HSeq.  If not see <http://www.gnu.org/licenses/>.
  ----*)

(** Default values. *)
module Default:
sig

  (** {6 File handling} *)

  (** [load n]: Load file [n]. *)
  val load : string -> unit

  (** [use ?silent n]: Use script [n]. *)
  val use : ?silent:bool -> string -> unit

  (** {6 Theories} *)

  (** The empty theory string. *)
  val empty_thy_name: string

  (** The name of the base theory. *)
  val base_thy_name:string
end

(** The theorem prover context. *)

(** Types *)

(** File handling functions *)
type file_t =
  {
    (** [load f]: Load a byte-code file [f] into memory. *)
    load_f: string -> unit;

    (** [use ?silent f]: Read file [f] as a script.  If
        [silent=true], do not report any information. *)
    use_f: ?silent:bool -> string -> unit;

    (** [build ?silent th]: Build theory [th] from a script.
        [silent=true], do not report any information.  @raise
        Failure on failure. *)
    build_f: ?silent:bool -> string -> unit;

    (** [path]: List of directories to search for theories,
        libraries and scripts.*)
    path_f: string list;

    (** suffix: List of possible suffixes for an object file. *)
    obj_suffix_f: string list;

    (** thy_suffix: Suffix for a theory file. *)
    thy_suffix_f: string;

    (** script_suffix: Suffix for a script file. *)
    script_suffix_f: string;
  }

(* The default value for [file_t]. *)
val empty_file_t: unit -> file_t

(** Theory data *)
type thy_t =
  {
    (** Name of the theory on which all user theories are based *)
    base_name_f: string option;

    (** The theory data-base. *)
    thydb_f: Thydb.thydb;

    (** Information needed for the theory database loader. *)
    loader_data_f: Thydb.Loader.data
  }

(** [empty_thy_t()]: The default value for [thy_t]. *)
val empty_thy_t: unit -> thy_t

(** Pretty printer *)
type pp_t =
  {
    pp_info_f: Printer.ppinfo ref;
  }

  (** Parsers *)
type parser_t =
  {
    parser_info_f: Parser.Table.t ref;
  }

(** [empty_pp_t()]: The default value for [pp_t]. *)
val empty_pp_t: unit -> pp_t

(** Top-level context *)
type t = 
  {
    (** Hooks for file handling functions *)
    file_f: file_t;

    (** Theory data *)
    thys_f: thy_t;

    (** Pretty printer *)
    pp_f: pp_t;

    (** Parsers *)
    parser_f: parser_t;
    
    (** A list of functions to invoke on a theory when it is added
        to the data-base. *)
    load_functions_f: (t -> Theory.contents -> t) list;

    (** Theorems caches *)
    thm_cache_f: (Ident.t, Logic.thm) Hashtbl.t;

    (** Scope attached to this context. *)
    scope_f: Scope.t;
  }

(** [empty()]: The empty context. *)
val empty: unit -> t

(** {6 Scoped contexts} *)

val scope_of: t -> Scope.t
(** Get the scope *)

val set_scope: t -> Scope.t -> t
(** Set the scope *)

(** {5 Accessor Functions} *)

(** {6 File handling} *)

val set_loader : t -> (string -> unit) -> t
(** [set_loader f t]: Set the file-loading function in context [t] to [f]. *)

val loader : t -> (string -> unit)
(** [loader t]: Get the file-loading function of context [t]. *)

val set_scripter : t -> (?silent:bool -> string -> unit) -> t
(** [set_use f t]: Set the script-loading function in context [t] to [f]. *)

val scripter: t -> (?silent:bool -> string -> unit)
(** [use t]: Get the script-loading function of context [t]. *)

val set_builder : t ->  (?silent:bool -> string -> unit) -> t
(** [set_use f t]: Set the script-loading function in context [t] to [f]. *)

val builder : t -> (?silent:bool -> string -> unit)
(** [builder t]: Get the theory builder function of context [t]. *)

{'fraction_non_alphanumeric': 0.14304063521718824, 'fraction_numerical': 0.002335357309668379, 'mean_word_length': 2.891412994093594, 'pattern_counts': {'":': 0, '<': 13, '<?xml version=': 0, '>': 85, 'https://': 0, 'lorem ipsum': 0, 'www.': 2, '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': '2606187', 'n_tokens_mistral': 2873, 'n_tokens_neox': 2744, 'n_words': 1053}