helm/software/components/tptp_grafite/ast.ml

   1 type kinds_of_formulae =
   2   | Axiom | Hypothesis | Definition | Lemma | Theorem | Conjecture
   3   | Lemma_conjecture | Negated_conjecture | Plain | Unknown
   4
   5 type source = NoSource
   6
   7 type info = NoInfo
   8
   9 type term =
  10   | Variable of string
  11   | Constant of string
  12   | Function of string * term list
  13
  14 type atom =
  15   | Proposition of string
  16   | Predicate of string * term list
  17   | True
  18   | False
  19   | Eq of term * term
  20   | NotEq of term * term
  21
  22 type formulae =
  23   | Disjunction of formulae * formulae
  24   | NegAtom of  atom
  25   | Atom of atom
  26
  27 type ast =
  28   | Comment of string
  29   | Inclusion of string * (string list)
  30   | AnnotatedFormula of
  31       string * kinds_of_formulae * formulae * source * info list