File: bool.ml

package info (click to toggle)
hol88 2.02.19940316dfsg-5
  • links: PTS
  • area: main
  • in suites: bookworm
  • size: 65,816 kB
  • sloc: ml: 199,939; ansic: 9,666; sh: 6,913; makefile: 6,032; lisp: 2,747; yacc: 894; sed: 201; cpp: 87; awk: 5
file content (172 lines) | stat: -rw-r--r-- 7,554 bytes parent folder | download | duplicates (11)
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;;