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
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
|
open Opname
open Jterm
type rule =
| Ax | Andr | Andl | Orr | Orr1 | Orr2 | Orl | Impr | Impl | Negr | Negl
| Allr | Alll| Exr | Exl | Fail | Falsel | Truer
let ruletable = function
| Fail -> "Fail"
| Ax -> "Ax"
| Negl -> "Negl"
| Negr -> "Negr"
| Andl -> "Andl"
| Andr -> "Andr"
| Orl -> "Orl"
| Orr -> "Orr"
| Orr1 -> "Orr1"
| Orr2 -> "Orr2"
| Impl -> "Impl"
| Impr -> "Impr"
| Exl -> "Exl"
| Exr -> "Exr"
| Alll -> "Alll"
| Allr -> "Allr"
| Falsel -> "Falsel"
| Truer -> "Truer"
module type JLogicSig =
sig
(* understanding the input *)
val is_all_term : term -> bool
val dest_all : term -> string * term * term
val is_exists_term : term -> bool
val dest_exists : term -> string * term * term
val is_and_term : term -> bool
val dest_and : term -> term * term
val is_or_term : term -> bool
val dest_or : term -> term * term
val is_implies_term : term -> bool
val dest_implies : term -> term * term
val is_not_term : term -> bool
val dest_not : term -> term
(* processing the output *)
type inf_step = rule * (string * term) * (string * term)
type inference = inf_step list
(* type inference *)
val empty_inf : inference
val append_inf : inference -> (string * term) -> (string * term) -> rule -> inference
val print_inf : inference -> unit
end;;
(* Copy from [term_op_std.ml]: *)
let rec print_address int_list =
match int_list with
| [] ->
Format.print_string ""
| hd::rest ->
begin
Format.print_int hd;
print_address rest
end
module JLogic: JLogicSig =
struct
let is_all_term = Jterm.is_all_term
let dest_all = Jterm.dest_all
let is_exists_term = Jterm.is_exists_term
let dest_exists = Jterm.dest_exists
let is_and_term = Jterm.is_and_term
let dest_and = Jterm.dest_and
let is_or_term = Jterm.is_or_term
let dest_or = Jterm.dest_or
let is_implies_term = Jterm.is_implies_term
let dest_implies = Jterm.dest_implies
let is_not_term = Jterm.is_not_term
let dest_not = Jterm.dest_not
type inf_step = rule * (string * term) * (string * term)
type inference = inf_step list
let empty_inf = []
let append_inf inf t1 t2 rule =
(rule, t1, t2)::inf
let rec print_inf inf =
match inf with
| [] -> print_string "."; Format.print_flush ()
| (rule, (n1,t1), (n2,t2))::d ->
print_string (ruletable rule);
print_string (":("^n1^":");
print_term stdout t1;
print_string (","^n2^":");
print_term stdout t2;
print_string ")\n";
print_inf d
end;;
let show_loading s = print_string s
type my_Debug = { mutable debug_name: string;
mutable debug_description: string;
debug_value: bool
}
let create_debug x = ref false
|
