Module TPTP_model_ast

module TPTP_model_ast: sig .. end

Simple Model AST

module T: Nunchaku_core.FO_tptp

type name = string

type id = string

type var = string

type term =

type statement =

`\|`	`Fi_domain of name * var * id list`
`\|`	`Fi_functors of name * id * var list * (var list * term list * term) list`
`\|`	`Fi_predicates of name * id * var list * (var list * term list * term) list`

val var : var -> term

val app : id -> term list -> term

val const : id -> term

val forall : var -> term -> term

val or_ : term -> term -> term

val and_ : term -> term -> term

val not_ : term -> term

val eq : term -> term -> term

val equiv : term -> term -> term

val atom : term -> term

val true_ : term

val false_ : term

module Conv: sig .. end

val mk_fi_domain : name -> term -> statement

val mk_fi_functors : name ->
       var list ->
       term list -> statement

val mk_fi_predicates : name ->
       var list ->
       term list -> statement

val pp_list_ : 'a CCFormat.printer -> 'a list CCFormat.printer

val pp_term : term CCFormat.printer

val pp_statement : Format.formatter -> statement -> unit

val pp_statements : Format.formatter -> statement list -> unit

val to_model : statement list -> (T.term, T.ty) Nunchaku_core.Model.t