<commit_before>(*----
  Name: basic.mli
  Copyright <NAME> 2005-2018
  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/>.
  ----*)

(** Basic constants and data structures. *)

(** {5 Base representation of logic types} *)

(*
type typ_const = Ident.t
(** Representation of user-defined type constructors (could merged
    into [pre_typ]).
*)
*)

type gtype_id
(** Type identifers. *)

val mk_gtype_id: string -> gtype_id
(** Make a type identifier. *)
val gtype_id_string: gtype_id -> string
(** Get a string representation of a type identifier. *)
val gtype_id_copy: gtype_id -> gtype_id
(** Make a new, unique with the same string representation as another. *)
val gtype_id_equal: gtype_id -> gtype_id -> bool
(** Equality of gtype_id. *)
val gtype_id_greaterthan: gtype_id -> gtype_id -> bool
val gtype_id_lessthan: gtype_id -> gtype_id -> bool
val gtype_id_compare: gtype_id -> gtype_id -> Order.t
(** Orderings on gtype_id.

    Maintains the invariant:
    - [gtype_id_equal x y]
      =>
      [not (gtype_id_lessthan x y)] and [not (gtype_id_greaterthan x y)].
    - [gtype_id_lessthan x y = not(gtype_id_greaterthan x y)]
*)

(** The base representation of types. *)
type ('a) pre_typ =
  | Atom of 'a
  (** Atomic variables. *)
  | TApp of (('a) pre_typ * ('a) pre_typ)
  (** Applications *)

type atomtype =
  | Var of gtype_id
  | Weak of gtype_id
  | Ident of Ident.t
(** [atomtype] Kinds of atomic type

   [Var(v)] is type variable. Can be bound (in a type environment) to any other
   type.

   [Weak(v)] is a weak type variable. Can bind to anything except a non-weak
   variable. They are used in a sequent calculus when a variable type 'x can
   occur in more than one sequent. If 'x is bound in one sequent, then it must
   have that binding in every sequent in which it occurs.

   [Ident(i)] is the name of a type constructor.
 *)

type gtype = (atomtype)pre_typ
(** The actual representation of types. *)

val mk_vartype: gtype_id -> gtype
val mk_weakvartype: gtype_id -> gtype
val mk_identtype: Ident.t -> gtype
val mk_apptype: gtype -> gtype -> gtype

val flatten_apptype: gtype -> (gtype)list
(**
   [flatten_apptype ty]: flatten an application in [ty] to a list of
   types.  [flatten_apptype (((f a1) a2) a3)] is [[f; a1; a2; a3]] and
   [flatten_apptype (((f a1) (g a2)) a3)] is [[f; a1; (g a2); a3]]

   If [ty] is not an applictaion then returns [[ty]].
*)

val split_apptype: gtype -> (gtype *(gtype)list)
(** Split an application [x a1 .. an] into [(x, [a1; .. an])] *)

val map_atomtype: (gtype -> gtype) -> gtype -> gtype
(* [map_atomtype f ty] Apply [f] to each [Atom] in [ty] returning the resulting
   type. *)

val iter_atomtype: (gtype -> unit) -> gtype -> unit
(* [iter_atomtype f ty] Apply [f] to each [Atom(x)] in [ty]. *)

val fold_atomtype: ('a -> gtype -> 'a) -> 'a -> gtype -> 'a
(* [fold_atomtype f z ty] Fold [f] over each [Atom(x)] in [ty] returning the
   result. The fold is top-down, left-to-right *)

val exists_atomtype: (gtype -> bool) -> gtype -> bool
(* [exists_atomtype p ty] Apply [p] to each [Atom(x)] in [ty], return [true] if
   any [Atom(x)] satisfies [p]. The check is top-down, left-to-right *)

val exists_type: (gtype -> bool) -> gtype -> bool
(* [exists_type p ty] Apply [p] to each sub-type of [ty], return [true] if any
   satisfies [p]. The check is top-down, left-to-right *)

val exists_type_data:
  (gtype -> (bool * ('a)option)) -> gtype -> (bool * ('a)option)
(* [exists_type_data p ty] Apply [p] to each sub-type of [ty], return [true] if
   any satisfies [p]. The check is top-down, left-to-right *)

(** {5 Base Representation of logic terms} *)

(** Built-in constants that can appear in terms  *)
type const_ty =
  | Cnum of Num.num    (* big numbers *)
  | Cbool of bool

val const_compare: const_ty -> const_ty -> Order.t
(** Total ordering on constants. *)
val const_lt: const_ty -> const_ty -> bool
(** Less-than ordering on constants. *)
val const_leq: const_ty -> const_ty -> bool<commit_msg>[hsq] Weaken some type declarastions in Basic<commit_after>(*----
  Name: basic.mli
  Copyright <NAME> 2005-2018
  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/>.
  ----*)

(** Basic constants and data structures. *)

(** {5 Base representation of logic types} *)

(*
type typ_const = Ident.t
(** Representation of user-defined type constructors (could merged
    into [pre_typ]).
*)
*)

type gtype_id
(** Type identifers. *)

val mk_gtype_id: string -> gtype_id
(** Make a type identifier. *)
val gtype_id_string: gtype_id -> string
(** Get a string representation of a type identifier. *)
val gtype_id_copy: gtype_id -> gtype_id
(** Make a new, unique with the same string representation as another. *)
val gtype_id_equal: gtype_id -> gtype_id -> bool
(** Equality of gtype_id. *)
val gtype_id_greaterthan: gtype_id -> gtype_id -> bool
val gtype_id_lessthan: gtype_id -> gtype_id -> bool
val gtype_id_compare: gtype_id -> gtype_id -> Order.t
(** Orderings on gtype_id.

    Maintains the invariant:
    - [gtype_id_equal x y]
      =>
      [not (gtype_id_lessthan x y)] and [not (gtype_id_greaterthan x y)].
    - [gtype_id_lessthan x y = not(gtype_id_greaterthan x y)]
*)

(** The base representation of types. *)
type ('a) pre_typ =
  | Atom of 'a
  (** Atomic variables. *)
  | TApp of (('a) pre_typ * ('a) pre_typ)
  (** Applications *)

type atomtype =
  | Var of gtype_id
  | Weak of gtype_id
  | Ident of Ident.t
(** [atomtype] Kinds of atomic type

   [Var(v)] is type variable. Can be bound (in a type environment) to any other
   type.

   [Weak(v)] is a weak type variable. Can bind to anything except a non-weak
   variable. They are used in a sequent calculus when a variable type 'x can
   occur in more than one sequent. If 'x is bound in one sequent, then it must
   have that binding in every sequent in which it occurs.

   [Ident(i)] is the name of a type constructor.
 *)

type gtype = (atomtype)pre_typ
(** The actual representation of types. *)

val mk_vartype: gtype_id -> gtype
val mk_weakvartype: gtype_id -> gtype
val mk_identtype: Ident.t -> gtype
val mk_apptype: gtype -> gtype -> gtype

val flatten_apptype: gtype -> (gtype)list
(**
   [flatten_apptype ty]: flatten an application in [ty] to a list of
   types.  [flatten_apptype (((f a1) a2) a3)] is [[f; a1; a2; a3]] and
   [flatten_apptype (((f a1) (g a2)) a3)] is [[f; a1; (g a2); a3]]

   If [ty] is not an applictaion then returns [[ty]].
*)

val split_apptype: gtype -> (gtype *(gtype)list)
(** Split an application [x a1 .. an] into [(x, [a1; .. an])] *)

val map_atomtype: (('a)pre_typ -> ('a)pre_typ) -> ('a)pre_typ -> ('a)pre_typ
(* [map_atomtype f ty] Apply [f] to each [Atom] in [ty] returning the resulting
   type. *)

val iter_atomtype: (('a)pre_typ -> unit) -> ('a)pre_typ -> unit
(* [iter_atomtype f ty] Apply [f] to each [Atom(x)] in [ty]. *)

val fold_atomtype: ('a -> ('b)pre_typ -> 'a) -> 'a -> ('b)pre_typ -> 'a
(* [fold_atomtype f z ty] Fold [f] over each [Atom(x)] in [ty] returning the
   result. The fold is top-down, left-to-right *)

val exists_atomtype: (('a)pre_typ -> bool) -> ('a)pre_typ -> bool
(* [exists_atomtype p ty] Apply [p] to each [Atom(x)] in [ty], return [true] if
   any [Atom(x)] satisfies [p]. The check is top-down, left-to-right *)

val exists_type: (('a)pre_typ -> bool) -> ('a)pre_typ -> bool
(* [exists_type p ty] Apply [p] to each sub-type of [ty], return [true] if any
   satisfies [p]. The check is top-down, left-to-right *)

val exists_type_data:
  (('a)pre_typ -> (bool * ('a)option)) -> ('a)pre_typ -> (bool * ('a)option)
(* [exists_type_data p ty] Apply [p] to each sub-type of [ty], return [true] if
   any satisfies [p]. The check is top-down, left-to-right *)

(** {5 Base Representation of logic terms} *)

(** Built-in constants that can appear in terms  *)
type const_ty =
  | Cnum of Num.num    (* big numbers *)
  | Cbool of bool

val const_compare: const_ty -> const_ty -> Order.t
(** Total ordering on constants. *)
val const_lt: const_ty -> const_ty -> bool
(** Less-than ordering on constants. *)
val const_leq: const_ty -> const_ty -> bool
{'fraction_non_alphanumeric': 0.13058419243986255, 'fraction_numerical': 0.0053694158075601375, 'mean_word_length': 3.5407118478790833, 'pattern_counts': {'":': 0, '<': 13, '<?xml version=': 0, '>': 103, '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': '7269439', 'n_tokens_mistral': 3265, 'n_tokens_neox': 3161, 'n_words': 1231}