1 files changed, 48 insertions, 0 deletions
diff --git a/contrib/dp/fol.mli b/contrib/dp/fol.mli
new file mode 100644
index 00000000..a85469cc
--- /dev/null
+++ b/contrib/dp/fol.mli
@@ -0,0 +1,48 @@
+
+(* Polymorphic First-Order Logic (that is Why's input logic) *)
+
+type typ = 
+  | Tvar of string
+  | Tid of string * typ list
+
+type term =   
+  | Cst of int
+  | Plus of term * term
+  | Moins of term * term
+  | Mult of term * term
+  | Div of term * term
+  | App of string * term list
+
+and atom =   
+  | Eq of term * term
+  | Le of term * term
+  | Lt of term * term
+  | Ge of term * term
+  | Gt of term * term
+  | Pred of string * term list
+
+and form = 
+  | Fatom of atom
+  | Imp of form * form
+  | Iff of form * form
+  | And of form * form
+  | Or of form * form
+  | Not of form
+  | Forall of string * typ * form
+  | Exists of string * typ * form
+  | True
+  | False
+
+(* the integer indicates the number of type variables *)
+type decl =
+  | DeclType of string * int
+  | DeclFun of string * int * typ list * typ
+  | DeclPred of string * int * typ list
+  | Axiom of string * form
+
+type query = decl list * form
+
+
+(* prover result *)
+
+type prover_answer = Valid | Invalid | DontKnow | Timeout