CoAlgFormula.mli

(** This module implements coalgebraic formulae
    (e.g. parsing, printing, (de-)constructing, ...).
    @author Florian Widmann
 *)


exception CoAlgException of string

type sort = int

type rational = { nominator: int; denominator: int }

val rational_of_int : int -> int -> rational

type formula =
  | TRUE
  | FALSE
  | AP of string (* named atom *)
  | NOT of formula
  | AT of string * formula (* @ *)
  | OR of formula * formula
  | AND of formula * formula
  | EQU of formula * formula (* equivalence <=> *)
  | IMP of formula * formula (* implication <-> *)
  | EX of string * formula (* exists, diamond of K *)
  | AX of string * formula (* forall, box of K *)
  | ENFORCES of int list * formula (* CL *)
  | ALLOWS   of int list * formula (* CL *)
  | MIN of int * string * formula (* some more intuitive diamond for GML *)
  | MAX of int * string * formula (* some more intuitive box for GML *)
  | MORETHAN of int * string * formula (* diamond of GML *)
  | MAXEXCEPT of int * string * formula (* box of GML, means: ¬>_nR.¬C *)
  | ATLEASTPROB of rational * formula (* = {>= 1/2} C  ---> C occurs with *)
                                      (*  probability of at least 50% *) 
  | LESSPROBFAIL of rational * formula (* = [1/2] C = {< 1/2} ¬ C ---> C fails with *)
                                       (* probability of less than 50% *)
  | CONST of string  (* constant functor with value string *)
  | CONSTN of string  (* constant functor with value other than string *)
  | ID of formula (* modality of the identity functor *)
  | NORM of formula * formula (* default implication *)
  | NORMN of formula * formula (* \neg NORM (\neg A, \neg B) *)
  | CHC of formula * formula
  | FUS of bool * formula
  | MU of string * formula
  | NU of string * formula
  | VAR of string
  | AF of formula
  | EF of formula
  | AG of formula
  | EG of formula
  | AU of formula * formula
  | EU of formula * formula
  | AR of formula * formula
  | ER of formula * formula
  | AB of formula * formula
  | EB of formula * formula

exception ConversionException of formula

type sortedFormula = sort * formula

val iter : (formula -> unit) -> formula -> unit (* iterate over all sub formulas *)
val convert_post : (formula -> formula) -> formula -> formula (* run over all subformulas in post order *)
val convertToK : formula -> formula (* tries to convert a formula to a pure K formula *)
val convertToGML : formula -> formula (* tries to convert a formula to a pure GML formula *)
val convertToMu : formula -> formula (* tries to convert a formula to a pure Mu formula *)

val isNominal : string -> bool

val sizeFormula : formula -> int
val sizeSortedFormula : sortedFormula -> int
val depthFormula : formula -> int

val string_of_formula : formula -> string
val exportFormula : formula -> string
val exportTatlFormula : formula -> string
val exportSortedFormula : sortedFormula -> string
val exportQuery : sortedFormula list -> sortedFormula -> string
val exportQueryParsable : sortedFormula list -> sortedFormula -> string
val importFormula : string -> formula
val importSortedFormula : string -> sortedFormula
val importQuery : string -> sortedFormula list * sortedFormula

(** Decides whether a fomula is aconjunctive.

   A formula is aconjunctive if for every conjunction (a ʌ b), at most one of
   the conjuncts a, b contains a free μ-variable. *)
val isMuAconjunctive : formula -> bool

val verifyFormula : formula -> unit
val verifyMuAltFree : formula -> string * string list

val equals: formula -> formula -> bool
val nnfNeg : formula -> formula
val nnf : formula -> formula

val simplify : formula -> formula

val dest_ap : formula -> string
val dest_nom : formula -> string
val dest_not : formula -> formula
val dest_at : formula -> string * formula
val dest_or : formula -> formula * formula
val dest_and : formula -> formula * formula
val dest_equ : formula -> formula * formula
val dest_imp : formula -> formula * formula
val dest_ex : formula -> string * formula
val dest_ax : formula -> string * formula
val dest_min : formula -> int * string * formula
val dest_max : formula -> int * string * formula
val dest_choice : formula -> formula * formula
val dest_fusion : formula -> bool * formula

val is_true : formula -> bool
val is_false : formula -> bool
val is_ap : formula -> bool
val is_nom : formula -> bool
val is_not : formula -> bool
val is_at : formula -> bool
val is_or : formula -> bool
val is_and : formula -> bool
val is_equ : formula -> bool
val is_imp : formula -> bool
val is_ex : formula -> bool
val is_ax : formula -> bool
val is_min : formula -> bool
val is_max : formula -> bool
val is_choice : formula -> bool
val is_fusion : formula -> bool

val const_true : formula
val const_false : formula
val const_ap : string -> formula
val const_nom : string -> formula
val const_not : formula -> formula
val const_at : string -> formula -> formula
val const_or : formula -> formula -> formula
val const_and : formula -> formula -> formula
val const_equ : formula -> formula -> formula
val const_imp : formula -> formula -> formula
val const_ex : string -> formula -> formula
val const_ax : string -> formula -> formula
val const_min : int -> string -> formula -> formula
val const_max : int -> string -> formula -> formula
val const_enforces : int list -> formula -> formula
val const_allows : int list -> formula -> formula
val const_choice : formula -> formula -> formula
val const_fusion : bool -> formula -> formula

type hcFormula = (hcFormula_node, formula) HashConsing.hash_consed
and hcFormula_node =
  | HCTRUE
  | HCFALSE
  | HCAP of string
  | HCNOT of string
  | HCAT of string * hcFormula
  | HCOR of hcFormula * hcFormula
  | HCAND of hcFormula * hcFormula
  | HCEX of string * hcFormula
  | HCAX of string * hcFormula
  | HCENFORCES of int list * hcFormula
  | HCALLOWS of int list * hcFormula
  | HCMORETHAN of int * string * hcFormula (* GML Diamond *)
  | HCMAXEXCEPT of int * string * hcFormula (* GML Box *)
  | HCATLEASTPROB of rational * hcFormula
  | HCLESSPROBFAIL of rational * hcFormula (* the probability for failing is less than ... *)
  | HCCONST of string
  | HCCONSTN of string
  | HCID of hcFormula
  | HCNORM of hcFormula * hcFormula
  | HCNORMN of hcFormula * hcFormula
  | HCCHC of hcFormula * hcFormula
  | HCFUS of bool * hcFormula
  | HCMU of string * hcFormula
  | HCNU of string * hcFormula
  | HCVAR of string

module HcFormula : (HashConsing.S with type nde = hcFormula_node and type fml = formula)

val hc_formula : HcFormula.t -> formula -> hcFormula
val hc_replace : HcFormula.t -> string -> hcFormula -> hcFormula -> hcFormula
val hc_freeIn : string -> hcFormula -> bool

(* Variant of freeIn that respects bound variables
   FIXME: Merge into regular freeIn
 *)
val hc_freeIn2 : string -> hcFormula -> bool

module HcFHt : (Hashtbl.S with type key = hcFormula)

(**
Parses a formula into a tree representation, where each node contains a connective. The tree structure then supports simplification and recombination of formulae.    
**)
val parseFormulaToTree: formula -> formula CoolUtils.Tree.tree

val formula_of_string: string -> formula

(* vim: set et sw=2 sts=2 ts=8 : *)