Previous  Up  Next

Module Statement

module Statement: sig .. end

Statement

The input problem is made of statements. Each statement can declare a type, assert a formula, or a conjecture, define a term, etc.

Those statements do not necessarily reflect exactly statements in the input language(s) (e.g., TPTP).

type 'ty data = {
   data_id : ID.t; (*
Name of the type
*)
   data_args : 'ty Var.t list; (*
type parameters
*)
   data_ty : 'ty; (*
type of Id, that is, type -> type -> ... -> type
*)
   data_cstors : (ID.t * 'ty) list; (*
Each constructor is id, ty. ty must be of the form ty1 -> ty2 -> ... -> id args
*)
}
A datatype declaration
type attr =
| A_AC 
type attrs = attr list 
type ('f, 't, 'ty) view =
| TyDecl of ID.t * 'ty (*
id: ty
*)
| Data of 'ty data list
| Def of ID.t * 'ty * 't
| RewriteTerm of ID.t * 'ty * 't list * 't
| RewriteForm of 't SLiteral.t * 'f list
| Assert of 'f (*
assert form
*)
| Lemma of 'f list (*
lemma to prove and use, using Avatar cut
*)
| Goal of 'f (*
goal to prove
*)
| NegatedGoal of 'f list (*
goal after negation
*) 
type ('f, 't, 'ty, 'meta) t = {
   view : ('f, 't, 'ty) view;
   attrs : attrs;
   src : 'meta; (*
additional data
*)
} 
type ('f, 't, 'ty) sourced_t = ('f, 't, 'ty, StatementSrc.t) t 
type clause = FOTerm.t SLiteral.t list 
type clause_t = (clause, FOTerm.t, Type.t) sourced_t 
val view : ('f, 't, 'ty, 'a) t -> ('f, 't, 'ty) view
val attrs : ('a, 'b, 'c, 'd) t -> attrs
val src : ('a, 'b, 'c, 'src) t -> 'src
val mk_data : ID.t -> args:'ty Var.t list -> 'ty -> (ID.t * 'ty) list -> 'ty data
val ty_decl : ?attrs:attrs ->
       src:'src -> ID.t -> 'ty -> ('a, 'b, 'ty, 'src) t
val def : ?attrs:attrs ->
       src:'src -> ID.t -> 'ty -> 't -> ('a, 't, 'ty, 'src) t
val rewrite_term : ?attrs:attrs ->
       src:'src -> ID.t -> 'ty -> 't list -> 't -> ('a, 't, 'ty, 'src) t
val rewrite_form : ?attrs:attrs ->
       src:'src -> 't SLiteral.t -> 'f list -> ('f, 't, 'a, 'src) t
val data : ?attrs:attrs ->
       src:'src -> 'ty data list -> ('a, 'b, 'ty, 'src) t
val assert_ : ?attrs:attrs -> src:'src -> 'f -> ('f, 'a, 'b, 'src) t
val lemma : ?attrs:attrs ->
       src:'src -> 'f list -> ('f, 'a, 'b, 'src) t
val goal : ?attrs:attrs -> src:'src -> 'f -> ('f, 'a, 'b, 'src) t
val neg_goal : ?attrs:attrs ->
       src:'src -> 'f list -> ('f, 'a, 'b, 'src) t
val signature : ?init:Signature.t ->
       ('a, 'b, Type.t, 'c) t Sequence.t -> Signature.t
Compute signature when the types are using Type
val add_src : file:string ->
       ('f, 't, 'ty, UntypedAST.attrs) t ->
       ('f, 't, 'ty, StatementSrc.t) t
val map_data : ty:('ty1 -> 'ty2) -> 'ty1 data -> 'ty2 data
val map : form:('f1 -> 'f2) ->
       term:('t1 -> 't2) ->
       ty:('ty1 -> 'ty2) ->
       ('f1, 't1, 'ty1, 'src) t -> ('f2, 't2, 'ty2, 'src) t
val map_src : f:('a -> 'b) ->
       ('f, 't, 'ty, 'a) t -> ('f, 't, 'ty, 'b) t

Defined Constants


val as_defined_cst : ID.t -> int option
as_defined_cst id returns Some level if id is a constant defined at stratification level level, None otherwise
val is_defined_cst : ID.t -> bool
val declare_defined_cst : ID.t -> int -> unit
val scan_stmt_for_defined_cst : ('a, FOTerm.t, 'b, 'c) t -> unit
Try and declare defined constants in the given statement