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 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172
|
term:=
\lst whitespace prev result_list FIRST_CHARS CHARS expected.
let (WORD,lst) = gnt lst whitespace prev in
let TOKENS = explode WORD in
debug_enter(`term`,expected,WORD);
if WORD = `CONJ` then
(let (term_0 , result_list , prev, lst) = term lst whitespace whitespace result_list FIRST_CHARS CHARS `nil` in
let (term_1 , result_list , prev, lst) = term lst whitespace prev result_list FIRST_CHARS CHARS expected in
let tmp_2 = mk_conj(term_0,term_1) in
let result_list = push tmp_2 result_list in
do_return result_list whitespace `term` prev lst `nil`)
else
fail
?
if WORD = `DISJ` then
(let (term_0 , result_list , prev, lst) = term lst whitespace whitespace result_list FIRST_CHARS CHARS `nil` in
let (term_1 , result_list , prev, lst) = term lst whitespace prev result_list FIRST_CHARS CHARS expected in
let tmp_2 = mk_disj(term_0,term_1) in
let result_list = push tmp_2 result_list in
do_return result_list whitespace `term` prev lst `nil`)
else
fail
?
if WORD = `NOT` then
(let (term_0 , result_list , prev, lst) = term lst whitespace whitespace result_list FIRST_CHARS CHARS expected in
let tmp_1 = mk_neg(term_0) in
let result_list = push tmp_1 result_list in
do_return result_list whitespace `term` prev lst `nil`)
else
fail
?
if WORD = `IMP` then
(let (term_0 , result_list , prev, lst) = term lst whitespace whitespace result_list FIRST_CHARS CHARS `nil` in
let (term_1 , result_list , prev, lst) = term lst whitespace prev result_list FIRST_CHARS CHARS expected in
let tmp_2 = mk_imp(term_0,term_1) in
let result_list = push tmp_2 result_list in
do_return result_list whitespace `term` prev lst `nil`)
else
fail
?
(let TOKEN_0 = TOKEN TOKENS FIRST_CHARS CHARS (hd lst) expected in
let tmp_1 = mk_var(TOKEN_0,":bool") in
let result_list = push tmp_1 result_list in
do_return result_list whitespace `term` whitespace lst `nil`);;
eof:=
\lst whitespace prev result_list FIRST_CHARS CHARS expected.
let (WORD,lst) = gnt lst whitespace prev in
let TOKENS = explode WORD in
debug_enter(`eof`,expected,WORD);
if WORD = `nil` then
(do_return result_list whitespace `eof` `nil` lst expected)
else
fail
? fail;;
conj:=
\lst whitespace prev result_list FIRST_CHARS CHARS expected.
let (WORD,lst) = gnt lst whitespace prev in
let TOKENS = explode WORD in
debug_enter(`conj`,expected,WORD);
if WORD = `CONJ` then
(let (term_0 , result_list , prev, lst) = term lst whitespace whitespace result_list FIRST_CHARS CHARS `nil` in
let (term_1 , result_list , prev, lst) = term lst whitespace prev result_list FIRST_CHARS CHARS `nil` in
let tmp_2 = mk_conj(term_0,term_1) in
let result_list = push tmp_2 result_list in
let (eof_2 , result_list , prev, lst) = eof lst whitespace prev result_list FIRST_CHARS CHARS expected in
let result_list = push eof_2 result_list in
do_return result_list whitespace `conj` prev lst `nil`)
else
fail
? fail;;
disj:=
\lst whitespace prev result_list FIRST_CHARS CHARS expected.
let (WORD,lst) = gnt lst whitespace prev in
let TOKENS = explode WORD in
debug_enter(`disj`,expected,WORD);
if WORD = `DISJ` then
(let (term_0 , result_list , prev, lst) = term lst whitespace whitespace result_list FIRST_CHARS CHARS `nil` in
let (term_1 , result_list , prev, lst) = term lst whitespace prev result_list FIRST_CHARS CHARS `nil` in
let tmp_2 = mk_disj(term_0,term_1) in
let result_list = push tmp_2 result_list in
let (eof_2 , result_list , prev, lst) = eof lst whitespace prev result_list FIRST_CHARS CHARS expected in
let result_list = push eof_2 result_list in
do_return result_list whitespace `disj` prev lst `nil`)
else
fail
? fail;;
neg:=
\lst whitespace prev result_list FIRST_CHARS CHARS expected.
let (WORD,lst) = gnt lst whitespace prev in
let TOKENS = explode WORD in
debug_enter(`neg`,expected,WORD);
if WORD = `NEG` then
(let (term_0 , result_list , prev, lst) = term lst whitespace whitespace result_list FIRST_CHARS CHARS `nil` in
let tmp_1 = mk_neg(term_0) in
let result_list = push tmp_1 result_list in
let (eof_1 , result_list , prev, lst) = eof lst whitespace prev result_list FIRST_CHARS CHARS expected in
let result_list = push eof_1 result_list in
do_return result_list whitespace `neg` prev lst `nil`)
else
fail
? fail;;
imp:=
\lst whitespace prev result_list FIRST_CHARS CHARS expected.
let (WORD,lst) = gnt lst whitespace prev in
let TOKENS = explode WORD in
debug_enter(`imp`,expected,WORD);
if WORD = `IMP` then
(let (term_0 , result_list , prev, lst) = term lst whitespace whitespace result_list FIRST_CHARS CHARS `nil` in
let (term_1 , result_list , prev, lst) = term lst whitespace prev result_list FIRST_CHARS CHARS `nil` in
let tmp_2 = mk_imp(term_0,term_1) in
let result_list = push tmp_2 result_list in
let (eof_2 , result_list , prev, lst) = eof lst whitespace prev result_list FIRST_CHARS CHARS expected in
let result_list = push eof_2 result_list in
do_return result_list whitespace `imp` prev lst `nil`)
else
fail
? fail;;
MAIN_LOOP:=
\lst whitespace prev result_list FIRST_CHARS CHARS expected.
let (WORD,lst) = gnt lst whitespace prev in
let TOKENS = explode WORD in
debug_enter(`MAIN_LOOP`,expected,WORD);
(let (conj_0 , result_list , prev, lst) = conj lst whitespace WORD result_list FIRST_CHARS CHARS expected in
let result_list = push conj_0 result_list in
do_return result_list whitespace `MAIN_LOOP` prev lst `nil`)
?
(let (disj_0 , result_list , prev, lst) = disj lst whitespace WORD result_list FIRST_CHARS CHARS expected in
let result_list = push disj_0 result_list in
do_return result_list whitespace `MAIN_LOOP` prev lst `nil`)
?
(let (neg_0 , result_list , prev, lst) = neg lst whitespace WORD result_list FIRST_CHARS CHARS expected in
let result_list = push neg_0 result_list in
do_return result_list whitespace `MAIN_LOOP` prev lst `nil`)
?
(let (imp_0 , result_list , prev, lst) = imp lst whitespace WORD result_list FIRST_CHARS CHARS expected in
let result_list = push imp_0 result_list in
do_return result_list whitespace `MAIN_LOOP` prev lst `nil`);;
let PARSE_file (in_file,whitespace,separators) =
let white = if null whitespace then
[` `;`\T`;`\L`]
else
whitespace and
inf = open_file `in` in_file in
let WORD = e_w_s inf (hd white) white in
let lst = read_input inf [] white separators WORD IGNORE USEFUL in
let (WORD,lst) = (hd lst,tl lst) in
let result = fst (MAIN_LOOP lst (hd white) WORD []
FIRST_CHARS CHARS `nil`) in
result
? fail;;
let PARSE_text (text,whitespace,separators) =
let outf = open_file `out` `/tmp/.000HOL` in
write_string text outf;
close_file outf;
let result = PARSE_file (`/tmp/.000HOL`,whitespace,separators) in
unlink `/tmp/.000HOL`; result;;
|