<commit_before>
(*
Copyright (c) 2013, <NAME>
All rights reserved.

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this
list of conditions and the following disclaimer.  Redistributions in binary
form must reproduce the above copyright notice, this list of conditions and the
following disclaimer in the documentation and/or other materials provided with
the distribution.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*)

(** {1 Simple and Lightweight Congruence and order} *)

module type S = sig
  type term

  type t
    (** Represents a congruence *)

  val create : ?size:int -> unit -> t
    (** New congruence *)

  val clear : t -> unit
    (** Clear the content of the congruence. It is now equivalent to
        the empty congruence. *)

  val find : t -> term -> term
    (** Current representative of this term *)

  val iter : t -> (mem:term -> repr:term -> unit) -> unit
    (** Iterate on terms that are explicitely present in the congruence.
        The callback is given [mem], the term itself, and [repr],
        the current representative of the term [mem].

        Invariant: when calling [iter cc f], if [f ~mem ~repr] is called,
        then [find cc mem == repr] holds.
    *)

  val mk_eq : t -> term -> term -> unit
    (** [mk_eq congruence t1 t2] asserts that [t1 = t2] belongs to
        the congruence *)

  val mk_less : t -> term -> term -> unit
    (** [mk_less congruence t1 t2] asserts that [t1 < t2] belongs to
        the congruence *)

  val is_eq : t -> term -> term -> bool
    (** Returns true if the two terms are equal in the congruence *)

  val is_less : t -> term -> term -> bool
    (** Returns true if the first term is lower than the second one in the
        congruence *)

  val no_cycles : t -> bool
    (** Checks whether there are cycles in inequalities.
        @return true if all calls to [mk_less] are compatible with
        irreflexivity and transitivity of less. *)
end

(** The graph used for the congruence *)

module type TERM = sig
  type t
  val eq : t -> t -> bool
  val hash : t -> int

  val subterms : t -> t list
    (** Subterms of the term, and possibly a head symbol *)

  val update_subterms : t -> t list -> t
    (** Replace immediate subterms by the given list.
        This is used to test for equality *)
end

module Make(T : TERM) = struct
  type term = T.t

  (** Definition of the congruence closure graph nodes *)

  type node = {
    term : term;
    mutable subnodes : node array;  (* subnodes *)
    mutable lower : node list; (* only for representative *)
    mutable next : node;  (* union-find representative *)
    mutable waiters : (int * int * node) list
      (* (arity,position, waiter) list, only for representative *)
  } (** node of the graph *)

  module H = Hashtbl.Make(struct
    type t = term
    let equal = T.eq
    let hash = T.hash
  end)

  type t = node H.t

  let create ?(size=17) () = H.create size

  let clear h = H.clear h

  (* find representative *)
  let rec _find node =
    if node.next == node
      then node
      else (* path compression *)
        let root = _find node.next in
        let _ = node.next <- root in
        root

  (* are two nodes, with their subterm lists, congruent? To
      check this, we compute the representative of subnodes
      and we check whether updated subterms are equal *)
  let _are_congruent n1 n2 =
    assert (Array.length n1.subnodes = Array.length n2.subnodes);
    let l1' = List.map (fun n -> (_find n).term) (Array.to_list n1.subnodes) in
    let l2' = List.map (fun n -> (_find n).term) (Array.to_list n2.subnodes) in
    let t1 = T.update_subterms n1.term l1' in
    let t2 = T.update_subterms n2.term l2' in
    T.eq t1 t2

  (* check whether all congruences of [node] are computed, by
      looking at equivalence classes of [subnodes] *)
  let rec _check_congruence node =
    let arity = Array.length node.subnodes in
    for i = 0 to arity - 1 do
      let subnode = _find node.subnodes.(i) in
      List.iter
        (fun (arity', i', node') ->
          if i = i' && arity = arity' && _are_congruent node node'
            then _merge node node')
        subnode.waiters<commit_msg>Congruence: check for type errors<commit_after>
(*
Copyright (c) 2013, <NAME>
All rights reserved.

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this
list of conditions and the following disclaimer.  Redistributions in binary
form must reproduce the above copyright notice, this list of conditions and the
following disclaimer in the documentation and/or other materials provided with
the distribution.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*)

(** {1 Simple and Lightweight Congruence and order} *)

module type S = sig
  type term

  type t
    (** Represents a congruence *)

  val create : ?size:int -> unit -> t
    (** New congruence *)

  val clear : t -> unit
    (** Clear the content of the congruence. It is now equivalent to
        the empty congruence. *)

  val find : t -> term -> term
    (** Current representative of this term *)

  val iter : t -> (mem:term -> repr:term -> unit) -> unit
    (** Iterate on terms that are explicitely present in the congruence.
        The callback is given [mem], the term itself, and [repr],
        the current representative of the term [mem].

        Invariant: when calling [iter cc f], if [f ~mem ~repr] is called,
        then [find cc mem == repr] holds.
    *)

  val mk_eq : t -> term -> term -> unit
    (** [mk_eq congruence t1 t2] asserts that [t1 = t2] belongs to
        the congruence *)

  val mk_less : t -> term -> term -> unit
    (** [mk_less congruence t1 t2] asserts that [t1 < t2] belongs to
        the congruence *)

  val is_eq : t -> term -> term -> bool
    (** Returns true if the two terms are equal in the congruence *)

  val is_less : t -> term -> term -> bool
    (** Returns true if the first term is lower than the second one in the
        congruence *)

  val no_cycles : t -> bool
    (** Checks whether there are cycles in inequalities.
        @return true if all calls to [mk_less] are compatible with
        irreflexivity and transitivity of less. *)
end

(** The graph used for the congruence *)

module type TERM = sig
  type t
  val eq : t -> t -> bool
  val hash : t -> int

  val subterms : t -> t list
    (** Subterms of the term, and possibly a head symbol *)

  val update_subterms : t -> t list -> t
    (** Replace immediate subterms by the given list.
        This is used to test for equality *)
end

module Make(T : TERM) = struct
  type term = T.t

  (** Definition of the congruence closure graph nodes *)

  type node = {
    term : term;
    mutable subnodes : node array;  (* subnodes *)
    mutable lower : node list; (* only for representative *)
    mutable next : node;  (* union-find representative *)
    mutable waiters : (int * int * node) list
      (* (arity,position, waiter) list, only for representative *)
  } (** node of the graph *)

  module H = Hashtbl.Make(struct
    type t = term
    let equal = T.eq
    let hash = T.hash
  end)

  type t = node H.t

  let create ?(size=17) () = H.create size

  let clear h = H.clear h

  (* find representative *)
  let rec _find node =
    if node.next == node
      then node
      else (* path compression *)
        let root = _find node.next in
        let _ = node.next <- root in
        root

  (* are two nodes, with their subterm lists, congruent? To
      check this, we compute the representative of subnodes
      and we check whether updated subterms are equal *)
  let _are_congruent n1 n2 =
    assert (Array.length n1.subnodes = Array.length n2.subnodes);
    let l1' = List.map (fun n -> (_find n).term) (Array.to_list n1.subnodes) in
    let l2' = List.map (fun n -> (_find n).term) (Array.to_list n2.subnodes) in
    try
      let t1 = T.update_subterms n1.term l1' in
      let t2 = T.update_subterms n2.term l2' in
      T.eq t1 t2
    with Type.Error _ ->
      false

  (* check whether all congruences of [node] are computed, by
      looking at equivalence classes of [subnodes] *)
  let rec _check_congruence node =
    let arity = Array.length node.subnodes in
    for i = 0 to arity - 1 do
      let subnode = _find node.subnodes.(i) in
      List.iter
        (fun (arity', i', node') ->
          if i = i' && arity = arity' && _are_congruent node node'
            then _merge node node')
        subnode.waiters
{'fraction_non_alphanumeric': 0.08513154005320721, 'fraction_numerical': 0.00650310375406444, 'mean_word_length': 2.820097854723372, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 68, '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': '7613925', 'n_tokens_mistral': 3063, 'n_tokens_neox': 2847, 'n_words': 1363}