blob: 5299f8ad77a7726801d49bc47162a675698f0368 (
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
|
type typ =
| 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 form
| Exists of form
| True
| False
type hyp =
| Assert of string * form
| DeclVar of string * typ
| DeclProp of string
| DeclType of string
type query = hyp list * form
(* prover result *)
type prover_answer = Valid | Invalid | DontKnow | Timeout
|
