1 files changed, 58 insertions, 0 deletions
diff --git a/plugins/dp/fol.mli b/plugins/dp/fol.mli
new file mode 100644
index 00000000..4fb763a6
--- /dev/null
+++ b/plugins/dp/fol.mli
@@ -0,0 +1,58 @@
+
+(* Polymorphic First-Order Logic (that is Why's input logic) *)
+
+type typ =
+  | Tvar of string
+  | Tid of string * typ list
+
+type term =
+  | Cst of Big_int.big_int
+  | RCst of Big_int.big_int
+  | Power2 of Big_int.big_int
+  | Plus of term * term
+  | Moins of term * term
+  | Mult of term * term
+  | Div of term * term
+  | Opp of 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 of string option
+  | Invalid
+  | DontKnow
+  | Timeout
+  | NoAnswer
+  | Failure of string
+