<commit_before>(*
Zipperposition: a functional superposition prover for prototyping
Copyright (C) 2012 <NAME>

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

This 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
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
02110-1301 USA.
*)

(** Most of the useful types *)

(** a symbol is just a string *)
open Symbols

(* TODO: (maybe) substitutions as list of pairs of *bound* terms,
  where bound term = (int * term), the int being an offset for renaming vars.
  mk_hclause would then perform normalization of variables, and renaming of
  terms/vars would been useless but for normalization and instantiation *)

(* TODO: in Clauses, constructors from clauses for inferences and simplifications,
         that take care of the parent/child and proof bookeeping *)

(* TODO: a 'type_' type for simple types, like
  type_ = Sort of symbol | Arrow of type_t list * type_. Problem is for "or" and "and"
  that are n-ary; also, "=" is polymorphic... Maybe polymorphism then? *)
(* TODO: a literal should be (term, term, int) where the int is a set of flags. It's enough
   to tell well the lit is positive/negative, and if it's oriented (a > b) or eq/incomparable.
   Always orient with the bigger term on left. *)
(* TODO: remove proof from clauses, make it external (a proof is a tree that
   contains clauses). This should allow to disable proof-handling. *)
(* TODO: do not compute set of variables for clause, only groundness and max variable (offset) *)

module Json = Yojson.Basic
type json = Json.json

(** term with a simple sort *)
type term = {
  term : term_cell;             (** the term itself *)
  sort : sort;                  (** the sort of the term *)
  mutable flags : int;          (** boolean flags about the term *)
  mutable tsize : int;          (** number of symbol/vars occurrences in the term (weight) *)
  mutable tag : int;            (** hashconsing tag *)
  mutable hkey : int;           (** hash *)
}
(** content of the term *)
and term_cell =
  | Var of int                  (** variable *)
  | BoundVar of int             (** bound variable (De Bruijn index) *)
  | Bind of symbol * term       (** bind one variable, with the symbol *)
  | Node of symbol * term list  (** term application *)

(** list of variables *)
type varlist = term list            

(** A logical first order object, with a context for its free variables.
    The context is an offset, so that X_i inside the 'a really is X_{i+offset} *)
type 'a bind = ('a * int)
let bind_with x offset = (x, offset)

(** substitution, a list of (variable -> term) *)
type substitution =
  | SubstBind of (term * int * term * int * substitution)
  | SubstEmpty

(** (Church-Rosser) term rewriting system *)
type rewriting_system = term -> term

(** partial order comparison *)<commit_msg>cleaned up Types. Also added the 'a parametrized type.<commit_after>(*
Zipperposition: a functional superposition prover for prototyping
Copyright (C) 2012 <NAME>

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

This 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
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
02110-1301 USA.
*)

(** Most of the useful types *)

(** a symbol is just a string *)
open Symbols

(* TODO: a literal should be (term, term, int) where the int is a set of flags. It's enough
   to tell well the lit is positive/negative, and if it's oriented (a > b) or eq/incomparable.
   Always orient with the bigger term on left. *)

module Json = Yojson.Basic
type json = Json.json

(** term with a simple sort *)
type term = {
  term : term_cell;             (** the term itself *)
  sort : sort;                  (** the sort of the term *)
  mutable flags : int;          (** boolean flags about the term *)
  mutable tsize : int;          (** number of symbol/vars occurrences in the term (weight) *)
  mutable tag : int;            (** hashconsing tag *)
  mutable hkey : int;           (** hash *)
}
(** content of the term *)
and term_cell =
  | Var of int                  (** variable *)
  | BoundVar of int             (** bound variable (De Bruijn index) *)
  | Bind of symbol * term       (** bind one variable, with the symbol *)
  | Node of symbol * term list  (** term application *)

(** list of variables *)
type varlist = term list            

(** A logical first order object, with a context for its free variables.
    The context is an offset, so that X_i inside the 'a really is X_{i+offset} *)
type 'a bind = ('a * int)

(** An object parametrized by a list of variables *)
type 'a parametrized = ('a * varlist)
type 'a parametrize = 'a -> 'a parametrized
type 'a specialize = 'a parametrized -> term list -> 'a

(** substitution, a list of (variable -> term) *)
type substitution =
  | SubstBind of (term * int * term * int * substitution)
  | SubstEmpty

(** (Church-Rosser) term rewriting system *)
type rewriting_system = term -> term

(** partial order comparison *)
{'fraction_non_alphanumeric': 0.08955979085849215, 'fraction_numerical': 0.0053972002023950074, 'mean_word_length': 3.2086586231369765, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 14, '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': '4572883', 'n_tokens_mistral': 1664, 'n_tokens_neox': 1553, 'n_words': 831}