blob: cce593cf440ca814325c60eadcceccacd485d799 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
|
type typ = string
(***
| Base of string
| Arrow of typ * typ
| Tuple of typ list
***)
type term =
| Cst of int
| Db of int
| Tvar of string
| 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
| Fvar of string
| Imp of form * form
| And of form * form
| Or of form * form
| Not of form
| Forall of string * (typ list * typ) * form
| Exists of string * (typ list * typ) * form
| True
| False
type hyp =
| Assert of string * form
| DeclVar of string * typ list * typ
| DeclPred of string * typ list
| DeclType of string
type query = hyp list * form
(* prover result *)
type prover_answer = Valid | Invalid | DontKnow | Timeout
|
