<commit_before>(*-----
 Name: formula.ml
 Author: <NAME> <<EMAIL>>
 Copyright <NAME> 2005
----*)

open Basic
exception Error


(** The type for formulas *)
type form =  { thy : Scope.marker; term : Basic.term }

let term_of x = x.term
(** Convert a formula to a term *)

let thy_of x = x.thy
(** Get the theory marker of a formula. *)


(***
* Error handling 
***)

class formError s ts =
  object (self)
    inherit Result.error s
    val forms = (ts :form list)
    method get() = forms
    method print st = 
      Format.printf "@[%s@ @[" (self#msg()); 
      Printer.print_sep_list 
	((fun f-> Term.print st (term_of f)), ",") (self#get());
      Format.printf "@]@]"
  end

let error s t = Result.mk_error((new formError s t):>Result.error)
let add_error s t es = raise (Result.add_error (error s t) es)


(***
* Conversion from a term
***)

(** 
   [mk_scoped_formula scp f]: make [f] a formula of [scp]. 
   Currently does nothing. Must not be exposed for general use.
*)
let mk_scoped_formula scp f = { thy = Scope.marker_of scp; term = f }

(** Convert a term to a formula *)
let make ?env scp t= 
  let t1=
    try Term.resolve_closed_term scp t
    with x -> raise
	(Result.add_error x
	   (Term.term_error 
	      "Formula.make: Can't make formula, not a closed term" [t]))
  in 
  try
    let tyenv = Lib.apply_option (fun x -> !x) env (Gtypes.empty_subst())
    in 
    let tyenv1 = 
      Typing.typecheck_top scp tyenv t1 (Gtypes.mk_null())
    in 
    mk_scoped_formula scp (Term.retype tyenv1 t1)
  with x -> 
    raise (Result.add_error x 
	     (Term.term_error "Formula.make: incorrect types" [t1]))


(*** Fast conversion to formulas for internal use ***)


(** 
   [mk_subterm_unsafe f t]: Make [t] a formula with the same theory
   marker as [f].  This is only safe if [t] is a subterm of [f] and
   [f] is not a quantifier.
*)
let mk_subterm_unsafe f t = {thy = thy_of f; term = t}

(**
   [mk_subterm f t]: Make [t] a formula with the same theory marker as
   [f]. Checks that [t] is a closed subterm of [f], fails otherwise. 
*)
let mk_subterm f t = 
  if (Term.is_subterm t (term_of f)) && (Term.is_closed [] t)
  then 
    {thy = thy_of f; term = t}
  else 
    raise (add_error "Can't make a formula as a subterm of formula" [f]
	     (Term.term_error "term isn't a subterm" [t]))

(**
   [formula_in_scope scp f]: true if formula [f] is in scope [scp].

   In the current implementation, this always returns [false].
   Future implementations will hopefully do something useful here.
*)   
let formula_in_scope scp f = Scope.in_scope_marker scp (thy_of f)

(**
   [valid_forms scp fs]: Return true if all formulas in [fs] are in
   scope [scp]. Return false otherwise. Used to test whether the
   formulas can be used e.g. with conjunction to make a new formula
   without the expense of going through [make].
*)
let valid_forms scp fs =
  let test() =
    List.iter 
      (fun f -> 
	if (formula_in_scope scp f) 
	then () else raise (error "invalid formula" [f])) fs
  in 
  try test(); true with _ -> false

(** 
   [fast_make scp fs t]: make a formula without any checks, if
   possible. This function must not be exposed for general use. It is
   only for use by the constructors.

   If [fs] are valid formulas then make [t] a formula of [scp] without
   doing any checks. Otherwise make [t] a formula using [make].
*)
let fast_make ?env scp fs t = 
  if (valid_forms scp fs) 
  then mk_scoped_formula scp t 
  else make scp t

(***
* Representation for permanent storage
***)

type saved_form =  Dbterm.dbterm
let to_save x =  Dbterm.of_term (term_of x)
let from_save scp x = make scp (Dbterm.to_term x)

(***
* Operations on formulas 
***)

let equals x y = Term.equals (term_of x) (term_of y)
<commit_msg>Minor changes.<commit_after>(*-----
 Name: formula.ml
 Author: <NAME> <<EMAIL>>
 Copyright <NAME> 2005
----*)

open Basic
exception Error


(** The type for formulas *)
type form =  { thy : Scope.marker; term : Basic.term }

let term_of x = x.term
(** Convert a formula to a term *)

let thy_of x = x.thy
(** Get the theory marker of a formula. *)


(***
* Error handling 
***)

class formError s ts =
  object (self)
    inherit Result.error s
    val forms = (ts :form list)
    method get() = forms
    method print st = 
      Format.printf "@[%s@ @[" (self#msg()); 
      Printer.print_sep_list 
	((fun f-> Term.print st (term_of f)), ",") (self#get());
      Format.printf "@]@]"
  end

let error s t = Result.mk_error((new formError s t):>Result.error)
let add_error s t es = raise (Result.add_error (error s t) es)


(***
* Conversion from a term
***)

(** 
   [mk_scoped_formula scp f]: make [f] a formula of [scp]. 
   Currently does nothing. Must not be exposed for general use.
*)
let mk_scoped_formula scp f = { thy = Scope.marker_of scp; term = f }

(** Convert a term to a formula *)
let make ?env scp t= 
  let t1=
    try Term.resolve_closed_term scp t
    with x -> raise
	(Result.add_error x
	   (Term.term_error 
	      "Formula.make: Can't make formula, not a closed term" [t]))
  in 
  try
    let tyenv = Lib.apply_option (fun x -> !x) env (Gtypes.empty_subst())
    in 
    let tyenv1 = 
      Typing.typecheck_top scp tyenv t1 (Gtypes.mk_null())
    in 
    mk_scoped_formula scp (Term.retype tyenv1 t1)
  with x -> 
    raise (Result.add_error x 
	     (Term.term_error "Formula.make: incorrect types" [t1]))


(*** Fast conversion to formulas for internal use ***)


(** 
   [mk_subterm_unsafe f t]: Make [t] a formula with the same theory
   marker as [f].  This is only safe if [t] is a subterm of [f] and
   [f] is not a quantifier.
*)
let mk_subterm_unsafe f t = {thy = thy_of f; term = t}

(**
   [mk_subterm f t]: Make [t] a formula with the same theory marker as
   [f]. Checks that [t] is a closed subterm of [f], fails otherwise. 
*)
let mk_subterm f t = 
  if (Term.is_subterm t (term_of f)) && (Term.is_closed [] t)
  then 
    {thy = thy_of f; term = t}
  else 
    raise (add_error "Can't make a formula as a subterm of formula" [f]
	     (Term.term_error "term isn't a subterm" [t]))

(**
   [formula_in_scope scp f]: true if formula [f] is in scope [scp].

   In the current implementation, this always returns [false].
   Future implementations will hopefully do something useful here.
*)   
let formula_in_scope scp f = Scope.in_scope_marker scp (thy_of f)

(**
   [valid_forms scp fs]: Return true if all formulas in [fs] are in
   scope [scp]. Return false otherwise. Used to test whether the
   formulas can be used e.g. with conjunction to make a new formula
   without the expense of going through [make].
*)
let valid_forms scp fs =
  let test() =
    List.iter 
      (fun f -> 
	if (formula_in_scope scp f) 
	then () else raise (error "invalid formula" [f])) fs
  in 
  try test(); true with _ -> false

(** 
   [fast_make scp fs t]: make a formula without any checks, if
   possible. This function must not be exposed for general use. It is
   only for use by the constructors.

   If [fs] are valid formulas then make [t] a formula of [scp] without
   doing any checks. Otherwise make [t] a formula using [make].
*)
let fast_make ?env scp fs t = 
  if (valid_forms scp fs) 
  then (mk_scoped_formula scp  t)
  else (make scp t)

(***
* Representation for permanent storage
***)

type saved_form =  Dbterm.dbterm
let to_save x =  Dbterm.of_term (term_of x)
let from_save scp x = make scp (Dbterm.to_term x)

(***
* Operations on formulas 
***)

let equals x y = Term.equals (term_of x) (term_of y)

{'fraction_non_alphanumeric': 0.11751367213552087, 'fraction_numerical': 0.0026677337601707348, 'mean_word_length': 3.0203753351206433, 'pattern_counts': {'":': 0, '<': 11, '<?xml version=': 0, '>': 25, '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': '471535', 'n_tokens_mistral': 2699, 'n_tokens_neox': 2557, 'n_words': 1021}