X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=components%2Ftptp_grafite%2Fast.ml;fp=components%2Ftptp_grafite%2Fast.ml;h=b8f855dd12b1da00f6b67974b2932b8256876ec0;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/components/tptp_grafite/ast.ml b/components/tptp_grafite/ast.ml
new file mode 100644
index 000000000..b8f855dd1
--- /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