<commit_before>(*  ID:         $Id$
    Author:     <NAME>
    Copyright   2004  University of Cambridge
*)

structure ReconTranslateProof =
struct

fun add_in_order (x:string) [] = [x]
|   add_in_order (x:string) ((y:string)::ys) = if (x < y) 
                             then 
                                  (x::(y::ys))
                             else
                                  (y::(add_in_order x ys))
fun add_once x [] = [x]
|   add_once x (y::ys) = if x mem (y::ys) then (y::ys)
                         else add_in_order x (y::ys)
     
fun thm_vars thm = map (fn ((name,ix),_) => name) (Drule.vars_of thm);

exception Reflex_equal;

(********************************)
(* Proofstep datatype           *)
(********************************)
(* Assume rewrite steps have only two clauses in them just now, but lcl109-5 has Rew[5,3,5,3]  *)

datatype Side = Left |Right

datatype Proofstep =  ExtraAxiom
                     | OrigAxiom
  		     | VampInput 
                     | Axiom
                     | Binary of (int * int) * (int * int)   (* (clause1,lit1), (clause2, lit2) *)
                     | MRR of (int * int) * (int * int) 
                     | Factor of (int * int * int)           (* (clause,lit1, lit2) *)
                     | Para of (int * int) * (int * int) 
		     | Super_l of (int * int) * (int * int)
		     | Super_r of (int * int) * (int * int)
                     (*| Rewrite of (int * int) * (int * int)  *)
                     | Rewrite of (int * int) list
		     | SortSimp of (int * int) * (int * int)  
		     | UnitConf of (int * int) * (int * int)  
                     | Obvious of (int * int)
  		     | AED of (int*int)
  		     | EqualRes of (int*int)
    		     | Condense of (int*int)
                     (*| Hyper of int list*)
                     | Unusedstep of unit


datatype Clausesimp = Binary_s of int * int
                      | Factor_s of unit
                      | Demod_s of (int * int) list
                      | Hyper_s of int list
                      | Unusedstep_s of unit



datatype Step_label = T_info
                     |P_info


fun is_alpha_space_digit_or_neg ch =
    (ch = "~") orelse (ReconOrderClauses.is_alpha ch) orelse 
    (ReconOrderClauses.is_digit ch) orelse ( ch = " ");

fun lit_string_with_nums t = let val termstr = Term.str_of_term t
                                 val exp_term = explode termstr
                             in
                                 implode(List.filter is_alpha_space_digit_or_neg exp_term)<commit_msg>added low-level string_of_term (back again from term.ML) -- should avoid this altogether;<commit_after>(*  ID:         $Id$
    Author:     <NAME>
    Copyright   2004  University of Cambridge
*)

structure ReconTranslateProof =
struct

fun add_in_order (x:string) [] = [x]
|   add_in_order (x:string) ((y:string)::ys) = if (x < y) 
                             then 
                                  (x::(y::ys))
                             else
                                  (y::(add_in_order x ys))
fun add_once x [] = [x]
|   add_once x (y::ys) = if x mem (y::ys) then (y::ys)
                         else add_in_order x (y::ys)
     
fun thm_vars thm = map (fn ((name,ix),_) => name) (Drule.vars_of thm);

exception Reflex_equal;

(********************************)
(* Proofstep datatype           *)
(********************************)
(* Assume rewrite steps have only two clauses in them just now, but lcl109-5 has Rew[5,3,5,3]  *)

datatype Side = Left |Right

datatype Proofstep =  ExtraAxiom
                     | OrigAxiom
  		     | VampInput 
                     | Axiom
                     | Binary of (int * int) * (int * int)   (* (clause1,lit1), (clause2, lit2) *)
                     | MRR of (int * int) * (int * int) 
                     | Factor of (int * int * int)           (* (clause,lit1, lit2) *)
                     | Para of (int * int) * (int * int) 
		     | Super_l of (int * int) * (int * int)
		     | Super_r of (int * int) * (int * int)
                     (*| Rewrite of (int * int) * (int * int)  *)
                     | Rewrite of (int * int) list
		     | SortSimp of (int * int) * (int * int)  
		     | UnitConf of (int * int) * (int * int)  
                     | Obvious of (int * int)
  		     | AED of (int*int)
  		     | EqualRes of (int*int)
    		     | Condense of (int*int)
                     (*| Hyper of int list*)
                     | Unusedstep of unit


datatype Clausesimp = Binary_s of int * int
                      | Factor_s of unit
                      | Demod_s of (int * int) list
                      | Hyper_s of int list
                      | Unusedstep_s of unit



datatype Step_label = T_info
                     |P_info


fun is_alpha_space_digit_or_neg ch =
    (ch = "~") orelse (ReconOrderClauses.is_alpha ch) orelse 
    (ReconOrderClauses.is_digit ch) orelse ( ch = " ");

fun string_of_term (Const(s,_)) = s
  | string_of_term (Free(s,_)) = s
  | string_of_term (Var(ix,_)) = Term.string_of_vname ix
  | string_of_term (Bound i) = string_of_int i
  | string_of_term (Abs(x,_,t)) = "%" ^ x ^ ". " ^ string_of_term t
  | string_of_term (s $ t) =
      "(" ^ string_of_term s ^ " " ^ string_of_term t ^ ")"

(* FIXME string_of_term is quite unreliable here *)
fun lit_string_with_nums t = let val termstr = string_of_term t
                                 val exp_term = explode termstr
                             in
                                 implode(List.filter is_alpha_space_digit_or_neg exp_term)
{'fraction_non_alphanumeric': 0.13243486073674754, 'fraction_numerical': 0.00646900269541779, 'mean_word_length': 1.5140018066847336, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 8, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6190766', 'n_tokens_mistral': 1871, 'n_tokens_neox': 1732, 'n_words': 483}