branch for universe

[helm.git] / components / tptp_grafite / ast.ml

diff --git a/components/tptp_grafite/ast.ml b/components/tptp_grafite/ast.ml
new file mode 100644 (file)
index 0000000..b8f855d
--- /dev/null
+++ b/components/tptp_grafite/ast.ml
@@ -0,0 +1,31 @@
+type kinds_of_formulae = 
+  | Axiom | Hypothesis | Definition | Lemma | Theorem | Conjecture
+  | Lemma_conjecture | Negated_conjecture | Plain | Unknown
+
+type source = NoSource
+
+type info = NoInfo
+
+type term = 
+  | Variable of string
+  | Constant of string 
+  | Function of string * term list
+
+type atom = 
+  | Proposition of string
+  | Predicate of string * term list
+  | True
+  | False
+  | Eq of term * term
+  | NotEq of term * term
+
+type formulae = 
+  | Disjunction of formulae * formulae
+  | NegAtom of  atom
+  | Atom of atom
+  
+type ast = 
+  | Comment of string
+  | Inclusion of string * (string list)
+  | AnnotatedFormula of 
+      string * kinds_of_formulae * formulae * source * info list