blob: a069cbd5fab5d750e01b359a70bc55bcd926bb4e (
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
|
(* Data types useful for our theorem prover *)
(* logical proposition *)
type proposition =
| True
| False
| Lit of string
| Not of proposition
| And of proposition * proposition
| Or of proposition * proposition
| Implies of proposition * proposition
| Iff of proposition * proposition
(* interpretation of propositional symbols *)
type interpretation = (string * bool) list (* note: we're using OCaml booleans here *)
(* allows us to substitute any proposition for any atomic literal *)
type substitution = (string * proposition) list
(* tokens used by lexer and parser *)
type tok =
| TRUE
| FALSE
| LIT of string
| NOT
| AND
| OR
| IMPLIES
| IFF
| LEFT_PAREN
| RIGHT_PAREN
| SKIP
(* sequent *)
type seq = Seq of proposition list * proposition list
(* tree of sequents where Conclusion(s, l) represents a sequent s and a list l of
* strees that together prove s *)
type stree = Concl of seq * stree list
|
