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.mli55
1 files changed, 0 insertions, 55 deletions
diff --git a/contrib/dp/fol.mli b/contrib/dp/fol.mli
deleted file mode 100644
index b94bd3e3..00000000
--- a/contrib/dp/fol.mli
+++ /dev/null
@@ -1,55 +0,0 @@
-
-(* 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 of string option
- | Invalid
- | DontKnow
- | Timeout
- | NoAnswer
- | Failure of string
-