blob: bf6a34de399db2151edb20ffd1d627ca58c56e69 (
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
|
(* 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
(* 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
|
