Module FO

module FO: sig .. end

First-Order Monomorphic Terms and Formulas

This is the end of the chain, where formulas and terms are ready to be sent to some SMT solver. Types are monomorphic, formulas are first-order

type id = ID.t

type 'a var = 'a Var.t

type 'a printer = Format.formatter -> 'a -> unit

type 'a or_error = ('a, string) CCResult.t

type metadata = ProblemMetadata.t

type ('a, 'b) res = ('a, 'b) Problem.Res.t

module TyBuiltin: sig .. end

module Builtin: sig .. end

type ('t, 'ty) view =

`\|`	`Builtin of Builtin.t`
`\|`	`Var of 'ty var`
`\|`	`App of id * 't list`
`\|`	`DataTest of id * 't`
`\|`	`DataSelect of id * int * 't`
`\|`	`Undefined of id * 't`	`(*`	`'t` is not defined here	`*)`
`\|`	`Undefined_atom of id * 'ty toplevel_ty * 't list`	`(*`	some undefined term of given topleveltype, + args	`*)`
`\|`	`Unparsable of 'ty`	`(*`	could not parse term	`*)`
`\|`	`Fun of 'ty var * 't`	`(*`	caution, not supported everywhere	`*)`
`\|`	`Mu of 'ty var * 't`	`(*`	caution, not supported everywhere	`*)`
`\|`	`Let of 'ty var * 't * 't`
`\|`	`Ite of 't * 't * 't`
`\|`	`True`
`\|`	`False`
`\|`	`Eq of 't * 't`
`\|`	`And of 't list`
`\|`	`Or of 't list`
`\|`	`Not of 't`
`\|`	`Imply of 't * 't`
`\|`	`Equiv of 't * 't`
`\|`	`Forall of 'ty var * 't`
`\|`	`Exists of 'ty var * 't`

Term

type 'ty toplevel_ty = 'ty list * 'ty

Toplevel type: an arrow of atomic types

type 'ty ty_view =

`\|`	`TyBuiltin of TyBuiltin.t`
`\|`	`TyApp of id * 'ty list`

Type

type 'ty constructor = {

	`cstor_name : id;`
	`cstor_args : 'ty list;`

}

type 'ty tydef = {

	`ty_name : id;`
	`ty_cstors : 'ty constructor ID.Map.t;`

}

type 'ty mutual_types = {

	`tys_vars : id list;`
	`tys_defs : 'ty tydef list;`

}

type attr =

`\|`	`Attr_pseudo_prop`
`\|`	`Attr_pseudo_true`

type ('t, 'ty) statement =

`\|`	`TyDecl of id * int * attr list`	`(*`	number of arguments	`*)`
`\|`	`Decl of id * 'ty toplevel_ty * attr list`
`\|`	`Axiom of 't`
`\|`	CardBound of id * [ `Max \| `Min ] * int	`(*`	cardinality bound	`*)`
`\|`	MutualTypes of [ `Codata \| `Data ] * 'ty mutual_types
`\|`	`Goal of 't`

Statement

module Ty: sig .. end

module T: sig .. end

module Problem: sig .. end

Problem

module Util: sig .. end

Utils

val tys_of_toplevel_ty : 'ty toplevel_ty -> 'ty Sequence.t

val terms_of_statement : ('t, 'a) statement -> 't Sequence.t

val tys_of_statement : ('a, 'ty) statement -> 'ty Sequence.t

val print_ty : Ty.t printer

val print_toplevel_ty : Ty.toplevel_ty printer

val print_term : T.t printer

val print_term' : 'a -> T.t printer

val print_statement : (T.t, Ty.t) statement printer

val print_model : (T.t * T.t) list printer

val print_problem : (T.t, Ty.t) Problem.t printer

module To_tptp: sig .. end

Assume there are no types (other than `Unitype), no datatypes, no pattern match...

module Of_tptp: sig .. end

val pipe_tptp : ((T.t, Ty.t) Problem.t, FO_tptp.problem,
        (FO_tptp.term, FO_tptp.ty) res, (T.t, Ty.t) res)
       Transform.t