<commit_before>(*
    ||M||  This file is part of HELM, an Hypertextual, Electronic
    ||A||  Library of Mathematics, developed at the Computer Science
    ||T||  Department, University of Bologna, Italy.
    ||I||
    ||T||  HELM is free software; you can redistribute it and/or
    ||A||  modify it under the terms of the GNU General Public License
    \   /  version 2 or (at your option) any later version.
     \ /   This software is distributed as is, NO WARRANTY.
      V_______________________________________________________________ *)

open Types
open Hashcons
open Format

module T = Terms
module C = Clauses
module I = Index
module PS = ProofState

(* print a list of items using the printing function *)
let rec pp_list ?(sep=", ") pp_item  formatter = function
  | x::y::xs -> fprintf formatter "%a%s@,%a"
      pp_item x sep (pp_list ~sep:sep pp_item) (y::xs)
  | x::[] -> pp_item formatter x
  | [] -> ()

let rec pp_foterm formatter t = match t.node.term with
  | Leaf x -> Signature.pp_symbol formatter x
  | Var i -> fprintf formatter "X%d" i
  | Node (head::args) -> fprintf formatter
      "@[<h>%a(%a)@]" pp_foterm head (pp_list ~sep:", " pp_foterm) args
  | Node [] -> failwith "bad term"

let string_of_direction = function
    | Left2Right -> "Left to right"
    | Right2Left -> "Right to left"
    | Nodir -> "No direction"

let string_of_pos s = match s with
  | _ when s == C.left_pos -> "left"
  | _ when s == C.right_pos -> "right"
  | _ -> assert false

let pp_substitution formatter subst =
  fprintf formatter "@[<h>";
  List.iter
    (fun (v, t) ->
       fprintf formatter "?%a ->@, %a@;" pp_foterm v pp_foterm t)
    subst;
  fprintf formatter "@]"

(* print proof
let pp_proof bag ~formatter:f p =
  let rec aux eq = function
    | Terms.Exact t ->
        fprintf f "%d: Exact (" eq;
        pp_foterm f t;
        fprintf f ")@;";
    | Terms.Step (rule,eq1,eq2,dir,pos,subst) ->
        fprintf f "%d: %s("
          eq (string_of_rule rule);
      fprintf f "|%d with %d dir %s))" eq1 eq2
        (string_of_direction dir);
      let (_, _, _, proof1),_,_ = Terms.get_from_bag eq1 bag in
      let (_, _, _, proof2),_,_ = Terms.get_from_bag eq2 bag in
        fprintf f "@[<v 2>";
          aux eq1 proof1;
          aux eq2 proof2;
        fprintf f "@]";
  in
    fprintf f "@[<v>";
    aux 0 p;
    fprintf f "@]"
;;
*)

let string_of_comparison = function
  | Lt -> "=<="
  | Gt -> "=>="
  | Eq -> "==="
  | Incomparable -> "=?="
  | Invertible -> "=<->="

let pp_literal formatter = function
  | Equation (left, right, false, _) when right = T.true_symbol ->
    fprintf formatter "~%a" pp_foterm left
  | Equation (left, right, true, _) when right = T.true_symbol ->
    pp_foterm formatter left
  | Equation (left, right, true, _) when left = T.true_symbol ->
    pp_foterm formatter right
  | Equation (left, right, false, _) when left = T.true_symbol ->
    fprintf formatter "~%a" pp_foterm right
  | Equation (left, right, sign, ord) ->
    if sign
    then fprintf formatter "@[%a@ %a@ %a@]"
        pp_foterm left pp_foterm T.eq_symbol pp_foterm right
    else fprintf formatter "@[<hv 2>%a !%a@ %a@]"
        pp_foterm left pp_foterm T.eq_symbol pp_foterm right

let pp_clause formatter {clits=lits} =
  fprintf formatter "@[<hv 2>%a@]" (pp_list ~sep:" | " pp_literal) lits

let pp_clause_pos formatter (c, pos) =
  fprintf formatter "[%a at @[<h>%a@]]@;"
  pp_clause c (pp_list ~sep:"." pp_print_int) pos

let pp_hclause formatter c =
  fprintf formatter "@[<h>hclause(%d) %a@]" c.tag pp_clause c.node

let pp_hclause_pos formatter (c, pos) =
  fprintf formatter "[%a at @[<h>%a@]]@;"
  pp_hclause c (pp_list ~sep:"." pp_print_int) pos

let pp_bag formatter bag =
  fprintf formatter "@[<hov>";
  C.M.iter
    (fun _ hc -> fprintf formatter "%a@;" pp_clause hc.node)
    bag.C.bag_clauses;
  fprintf formatter "@]"<commit_msg>minor changes in pretty printing of clauses (always on one line now)<commit_after>(*
    ||M||  This file is part of HELM, an Hypertextual, Electronic
    ||A||  Library of Mathematics, developed at the Computer Science
    ||T||  Department, University of Bologna, Italy.
    ||I||
    ||T||  HELM is free software; you can redistribute it and/or
    ||A||  modify it under the terms of the GNU General Public License
    \   /  version 2 or (at your option) any later version.
     \ /   This software is distributed as is, NO WARRANTY.
      V_______________________________________________________________ *)

open Types
open Hashcons
open Format

module T = Terms
module C = Clauses
module I = Index
module PS = ProofState

(* print a list of items using the printing function *)
let rec pp_list ?(sep=", ") pp_item  formatter = function
  | x::y::xs -> fprintf formatter "%a%s@,%a"
      pp_item x sep (pp_list ~sep:sep pp_item) (y::xs)
  | x::[] -> pp_item formatter x
  | [] -> ()

let rec pp_foterm formatter t = match t.node.term with
  | Leaf x -> Signature.pp_symbol formatter x
  | Var i -> fprintf formatter "X%d" i
  | Node (head::args) -> fprintf formatter
      "@[<h>%a(%a)@]" pp_foterm head (pp_list ~sep:", " pp_foterm) args
  | Node [] -> failwith "bad term"

let string_of_direction = function
    | Left2Right -> "Left to right"
    | Right2Left -> "Right to left"
    | Nodir -> "No direction"

let string_of_pos s = match s with
  | _ when s == C.left_pos -> "left"
  | _ when s == C.right_pos -> "right"
  | _ -> assert false

let pp_substitution formatter subst =
  fprintf formatter "@[<h>";
  List.iter
    (fun (v, t) ->
       fprintf formatter "?%a ->@, %a@;" pp_foterm v pp_foterm t)
    subst;
  fprintf formatter "@]"

(* print proof
let pp_proof bag ~formatter:f p =
  let rec aux eq = function
    | Terms.Exact t ->
        fprintf f "%d: Exact (" eq;
        pp_foterm f t;
        fprintf f ")@;";
    | Terms.Step (rule,eq1,eq2,dir,pos,subst) ->
        fprintf f "%d: %s("
          eq (string_of_rule rule);
      fprintf f "|%d with %d dir %s))" eq1 eq2
        (string_of_direction dir);
      let (_, _, _, proof1),_,_ = Terms.get_from_bag eq1 bag in
      let (_, _, _, proof2),_,_ = Terms.get_from_bag eq2 bag in
        fprintf f "@[<v 2>";
          aux eq1 proof1;
          aux eq2 proof2;
        fprintf f "@]";
  in
    fprintf f "@[<v>";
    aux 0 p;
    fprintf f "@]"
;;
*)

let string_of_comparison = function
  | Lt -> "=<="
  | Gt -> "=>="
  | Eq -> "==="
  | Incomparable -> "=?="
  | Invertible -> "=<->="

let pp_literal formatter = function
  | Equation (left, right, false, _) when right = T.true_symbol ->
    fprintf formatter "~%a" pp_foterm left
  | Equation (left, right, true, _) when right = T.true_symbol ->
    pp_foterm formatter left
  | Equation (left, right, true, _) when left = T.true_symbol ->
    pp_foterm formatter right
  | Equation (left, right, false, _) when left = T.true_symbol ->
    fprintf formatter "~%a" pp_foterm right
  | Equation (left, right, sign, ord) ->
    if sign
    then fprintf formatter "@[%a@ %a@ %a@]"
        pp_foterm left pp_foterm T.eq_symbol pp_foterm right
    else fprintf formatter "@[<hv 2>%a !%a@ %a@]"
        pp_foterm left pp_foterm T.eq_symbol pp_foterm right

let pp_clause formatter {clits=lits} =
  fprintf formatter "@[<h>%a@]" (pp_list ~sep:" | " pp_literal) lits

let pp_clause_pos formatter (c, pos) =
  fprintf formatter "[%a at @[<h>%a@]]@;"
  pp_clause c (pp_list ~sep:"." pp_print_int) pos

let pp_hclause formatter c =
  fprintf formatter "@[<h>hclause(%d) %a@]" c.tag pp_clause c.node

let pp_hclause_pos formatter (c, pos) =
  fprintf formatter "[%a at @[<h>%a@]]@;"
  pp_hclause c (pp_list ~sep:"." pp_print_int) pos

let pp_bag formatter bag =
  fprintf formatter "@[<v>";
  C.M.iter
    (fun _ hc -> fprintf formatter "%a@;" pp_clause hc.node)
    bag.C.bag_clauses;
  fprintf formatter "@]"
{'fraction_non_alphanumeric': 0.14201637666325487, 'fraction_numerical': 0.0047338792221084955, 'mean_word_length': 3.0066632496155816, 'pattern_counts': {'":': 0, '<': 27, '<?xml version=': 0, '>': 83, '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': '5458249', 'n_tokens_mistral': 2832, 'n_tokens_neox': 2836, 'n_words': 890}