Module Logtk.StatementSource

Statement

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

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

Sourcetype 'ty data = {
  1. data_id : ID.t;
    (*

    Name of the type

    *)
  2. data_args : 'ty Var.t list;
    (*

    type parameters

    *)
  3. data_ty : 'ty;
    (*

    type of Id, that is, type -> type -> ... -> type

    *)
  4. data_cstors : (ID.t * 'ty * ('ty * (ID.t * 'ty)) list) list;
    (*

    Each constructor is id, ty, args. ty must be of the form ty1 -> ty2 -> ... -> id args. args has the form (ty1, p1), (ty2,p2), … where each p is a projector.

    *)
}

A datatype declaration

Sourcetype attr =
  1. | A_AC
  2. | A_infix of string
  3. | A_prefix of string
  4. | A_sos
    (*

    set of support

    *)
Sourcetype attrs = attr list
Sourcetype 'ty skolem = ID.t * 'ty
Sourcetype polarity = [
  1. | `Equiv
  2. | `Imply
]

polarity for rewrite rules

Sourcetype ('f, 't, 'ty) def_rule =
  1. | Def_term of {
    1. vars : 'ty Var.t list;
    2. id : ID.t;
    3. ty : 'ty;
    4. args : 't list;
    5. rhs : 't;
    6. as_form : 'f;
    }
    (*

    forall vars, id args = rhs

    *)
  2. | Def_form of {
    1. vars : 'ty Var.t list;
    2. lhs : 't SLiteral.t;
    3. rhs : 'f list;
    4. polarity : polarity;
    5. as_form : 'f list;
    }
    (*

    forall vars, lhs op bigand rhs where op depends on polarity (in {=>, <=>, <=})

    *)
Sourcetype ('f, 't, 'ty) def = {
  1. def_id : ID.t;
  2. def_ty : 'ty;
  3. def_rules : ('f, 't, 'ty) def_rule list;
  4. def_rewrite : bool;
}
Sourcetype ('f, 't, 'ty) view =
  1. | TyDecl of ID.t * 'ty
    (*

    id: ty

    *)
  2. | Data of 'ty data list
  3. | Def of ('f, 't, 'ty) def list
  4. | Rewrite of ('f, 't, 'ty) def_rule
  5. | Assert of 'f
    (*

    assert form

    *)
  6. | Lemma of 'f list
    (*

    lemma to prove and use, using Avatar cut

    *)
  7. | Goal of 'f
    (*

    goal to prove

    *)
  8. | NegatedGoal of 'ty skolem list * 'f list
    (*

    goal after negation, with skolems

    *)
Sourcetype formula = TypedSTerm.t
Sourcetype clause = lit list
Sourcetype ('f, 't, 'ty) t = private {
  1. id : int;
  2. view : ('f, 't, 'ty) view;
  3. attrs : attrs;
  4. proof : proof;
  5. mutable name : string option;
}
Sourceand proof = Proof.Step.t
Sourceand clause_t = (clause, Term.t, Type.t) t
Sourceval compare : (_, _, _) t -> (_, _, _) t -> int
Sourceval view : ('f, 't, 'ty) t -> ('f, 't, 'ty) view
Sourceval attrs : (_, _, _) t -> attrs
Sourceval proof_step : (_, _, _) t -> proof
Sourceval name : (_, _, _) t -> string

Retrieve a name from the proof, or generate+save a new one

Sourceval as_proof_i : input_t -> Proof.t
Sourceval as_proof_c : clause_t -> Proof.t
Sourceval mk_data : ID.t -> args:'ty Var.t list -> 'ty -> (ID.t * 'ty * ('ty * (ID.t * 'ty)) list) list -> 'ty data
Sourceval mk_def : ?rewrite:bool -> ID.t -> 'ty -> ('f, 't, 'ty) def_rule list -> ('f, 't, 'ty) def
Sourceval attrs_ua : (_, _, _) t -> UntypedAST.attrs

All attributes, included these in the proof

Sourceval ty_decl : ?attrs:attrs -> proof:proof -> ID.t -> 'ty -> (_, _, 'ty) t
Sourceval def : ?attrs:attrs -> proof:proof -> ('f, 't, 'ty) def list -> ('f, 't, 'ty) t
Sourceval rewrite : ?attrs:attrs -> proof:proof -> ('f, 't, 'ty) def_rule -> ('f, 't, 'ty) t
Sourceval data : ?attrs:attrs -> proof:proof -> 'ty data list -> (_, _, 'ty) t
Sourceval assert_ : ?attrs:attrs -> proof:proof -> 'f -> ('f, _, _) t
Sourceval lemma : ?attrs:attrs -> proof:proof -> 'f list -> ('f, _, _) t
Sourceval goal : ?attrs:attrs -> proof:proof -> 'f -> ('f, _, _) t
Sourceval neg_goal : ?attrs:attrs -> proof:proof -> skolems:'ty skolem list -> 'f list -> ('f, _, 'ty) t
Sourceval signature : ?init:Signature.t -> (_, _, Type.t) t Iter.t -> Signature.t

Compute signature when the types are using Type

Sourceval conv_attrs : UntypedAST.attrs -> attrs
Sourceval attr_to_ua : attr -> UntypedAST.attr
Sourceval map_data : ty:('ty1 -> 'ty2) -> 'ty1 data -> 'ty2 data
Sourceval map_def : form:('f1 -> 'f2) -> term:('t1 -> 't2) -> ty:('ty1 -> 'ty2) -> ('f1, 't1, 'ty1) def -> ('f2, 't2, 'ty2) def
Sourceval map : form:('f1 -> 'f2) -> term:('t1 -> 't2) -> ty:('ty1 -> 'ty2) -> ('f1, 't1, 'ty1) t -> ('f2, 't2, 'ty2) t

Defined Constants

Sourcetype definition = Rewrite.rule_set
Sourceval as_defined_cst : ID.t -> (int * definition) option

as_defined_cst id returns Some level if id is a constant defined at stratification level level, None otherwise

Sourceval as_defined_cst_level : ID.t -> int option
Sourceval is_defined_cst : ID.t -> bool
Sourceval declare_defined_cst : ID.t -> level:int -> definition -> unit

declare_defined_cst id ~level states that id is a defined constant of given level. It means that it is defined based only on constants of strictly lower levels

Sourceval scan_stmt_for_defined_cst : clause_t -> unit

Try and declare defined constants in the given statement

Inductive Types

Sourceval scan_stmt_for_ind_ty : clause_t -> unit

scan_stmt_for_ind_ty stmt examines stmt, and, if the statement is a declaration of inductive types or constants, it declares them using declare_ty or declare_inductive_constant.

Sourceval scan_simple_stmt_for_ind_ty : input_t -> unit

Same as scan_stmt but on earlier statements

Iterators

Sourcemodule Seq : sig ... end

IO

Sourceval pp_def_rule : 'a CCFormat.printer -> 'b CCFormat.printer -> 'c CCFormat.printer -> ('a, 'b, 'c) def_rule CCFormat.printer
Sourceval to_string : 'a CCFormat.printer -> 'b CCFormat.printer -> 'c CCFormat.printer -> ('a, 'b, 'c) t -> string
Sourcemodule ZF : sig ... end
Sourcemodule TPTP : sig ... end