summaryrefslogtreecommitdiff
path: root/contrib/dp/fol.mli
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/dp/fol.mli')
-rw-r--r--contrib/dp/fol.mli48
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