12 |
12 |
13 structure Nitrox : NITROX = |
13 structure Nitrox : NITROX = |
14 struct |
14 struct |
15 |
15 |
16 open ATP_Problem |
16 open ATP_Problem |
|
17 open ATP_Proof |
17 |
18 |
18 exception SYNTAX of string |
19 exception SYNTAX of string |
19 |
20 |
20 fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" |
|
21 |
|
22 fun takewhile _ [] = [] |
|
23 | takewhile p (x :: xs) = if p x then x :: takewhile p xs else [] |
|
24 |
|
25 fun dropwhile _ [] = [] |
|
26 | dropwhile p (x :: xs) = if p x then dropwhile p xs else x :: xs |
|
27 |
|
28 fun strip_c_style_comment [] = "" |
|
29 | strip_c_style_comment (#"*" :: #"/" :: cs) = strip_spaces_in_list cs |
|
30 | strip_c_style_comment (_ :: cs) = strip_c_style_comment cs |
|
31 and strip_spaces_in_list [] = "" |
|
32 | strip_spaces_in_list (#"%" :: cs) = |
|
33 strip_spaces_in_list (dropwhile (not_equal #"\n") cs) |
|
34 | strip_spaces_in_list (#"/" :: #"*" :: cs) = strip_c_style_comment cs |
|
35 | strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1 |
|
36 | strip_spaces_in_list [c1, c2] = |
|
37 strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2] |
|
38 | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) = |
|
39 if Char.isSpace c1 then |
|
40 strip_spaces_in_list (c2 :: c3 :: cs) |
|
41 else if Char.isSpace c2 then |
|
42 if Char.isSpace c3 then |
|
43 strip_spaces_in_list (c1 :: c3 :: cs) |
|
44 else |
|
45 str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^ |
|
46 strip_spaces_in_list (c3 :: cs) |
|
47 else |
|
48 str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs) |
|
49 val strip_spaces = strip_spaces_in_list o String.explode |
|
50 |
|
51 val parse_keyword = Scan.this_string |
21 val parse_keyword = Scan.this_string |
52 |
22 |
53 fun parse_file_path ("'" :: ss) = |
23 fun parse_file_path (c :: ss) = |
54 (takewhile (not_equal "'") ss |> implode, |
24 if c = "'" orelse c = "\"" then |
55 List.drop (dropwhile (not_equal "'") ss, 1)) |
25 ss |> chop_while (curry (op <>) c) |>> implode ||> tl |
56 | parse_file_path ("\"" :: ss) = |
26 else |
57 (takewhile (not_equal "\"") ss |> implode, |
27 raise SYNTAX "invalid file path" |
58 List.drop (dropwhile (not_equal "\"") ss, 1)) |
28 | parse_file_path [] = raise SYNTAX "invalid file path" |
59 | parse_file_path _ = raise SYNTAX "invalid file path" |
|
60 |
29 |
61 fun parse_include x = |
30 fun parse_include x = |
62 let |
31 let |
63 val (file_name, rest) = |
32 val (file_name, rest) = |
64 (parse_keyword "include" |-- $$ "(" |-- parse_file_path --| $$ ")" |
33 (parse_keyword "include" |-- $$ "(" |-- parse_file_path --| $$ ")" |
65 --| $$ ".") x |
34 --| $$ ".") x |
66 in |
35 in |
67 ((), raw_explode (strip_spaces (File.read (Path.explode file_name))) @ rest) |
36 ((), (file_name |> Path.explode |> File.read |
|
37 |> strip_spaces true (K true) |
|
38 |> raw_explode) @ rest) |
68 end |
39 end |
69 |
|
70 val parse_dollar_name = |
|
71 Scan.repeat ($$ "$") -- Symbol.scan_id >> (fn (ss, s) => implode ss ^ s) |
|
72 |
|
73 fun parse_term x = |
|
74 (parse_dollar_name |
|
75 -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") [] >> ATerm) x |
|
76 and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x |
|
77 |
|
78 (* Apply equal or not-equal to a term. *) |
|
79 val parse_predicate_term = |
|
80 parse_term -- Scan.option (Scan.option ($$ "!") --| $$ "=" -- parse_term) |
|
81 >> (fn (u, NONE) => AAtom u |
|
82 | (u1, SOME (NONE, u2)) => AAtom (ATerm ("=", [u1, u2])) |
|
83 | (u1, SOME (SOME _, u2)) => mk_anot (AAtom (ATerm ("=", [u1, u2])))) |
|
84 |
|
85 fun fo_term_head (ATerm (s, _)) = s |
|
86 |
|
87 fun parse_formula x = |
|
88 (($$ "(" |-- parse_formula --| $$ ")" |
|
89 || ($$ "!" >> K AForall || $$ "?" >> K AExists) |
|
90 --| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_formula |
|
91 >> (fn ((q, ts), phi) => |
|
92 AQuant (q, map (rpair NONE o fo_term_head) ts, phi)) |
|
93 || $$ "~" |-- parse_formula >> mk_anot |
|
94 || parse_predicate_term) |
|
95 -- Scan.option ((Scan.this_string "=>" >> K AImplies |
|
96 || Scan.this_string "<=>" >> K AIff |
|
97 || Scan.this_string "<~>" >> K ANotIff |
|
98 || Scan.this_string "<=" >> K AIf |
|
99 || $$ "|" >> K AOr || $$ "&" >> K AAnd) -- parse_formula) |
|
100 >> (fn (phi1, NONE) => phi1 |
|
101 | (phi1, SOME (c, phi2)) => mk_aconn c phi1 phi2)) x |
|
102 |
40 |
103 val parse_fof_or_cnf = |
41 val parse_fof_or_cnf = |
104 (parse_keyword "fof" || parse_keyword "cnf") |-- $$ "(" |-- |
42 (parse_keyword "fof" || parse_keyword "cnf") |-- $$ "(" |-- |
105 Scan.many (not_equal ",") |-- $$ "," |-- |
43 Scan.many (not_equal ",") |-- $$ "," |-- |
106 (parse_keyword "axiom" || parse_keyword "definition" |
44 (parse_keyword "axiom" || parse_keyword "definition" |