|
1 (* Title: HOL/TPTP/TPTP_Parser/tptp_problem_name.ML |
|
2 Author: Nik Sultana, Cambridge University Computer Laboratory |
|
3 |
|
4 Scans a TPTP problem name. Naming convention is described |
|
5 http://www.cs.miami.edu/~tptp/TPTP/TR/TPTPTR.shtml#Problem and Axiomatization Naming |
|
6 *) |
|
7 |
|
8 signature TPTP_PROBLEM_NAME = |
|
9 sig |
|
10 datatype suffix = |
|
11 Problem of |
|
12 ((*version*)int * |
|
13 (*size parameter*)int option) * |
|
14 (*extension*)string |
|
15 | Axiom of |
|
16 (*specialisation*)int * |
|
17 (*extension*)string |
|
18 |
|
19 type tptp_problem_name = |
|
20 {prob_domain : string, |
|
21 prob_number : int, |
|
22 prob_form : TPTP_Syntax.language, |
|
23 suffix : suffix} |
|
24 |
|
25 datatype problem_name = |
|
26 Standard of tptp_problem_name |
|
27 | Nonstandard of string |
|
28 |
|
29 exception TPTP_PROBLEM_NAME of string |
|
30 |
|
31 val parse_problem_name : string -> problem_name |
|
32 val mangle_problem_name : problem_name -> string |
|
33 end |
|
34 |
|
35 structure TPTP_Problem_Name: TPTP_PROBLEM_NAME = |
|
36 struct |
|
37 |
|
38 (*some basic tokens*) |
|
39 val numerics = map Char.chr (48 upto 57) (*0..9*) |
|
40 val alphabetics = |
|
41 map Char.chr (65 upto 90) @ (*A..Z*) |
|
42 map Char.chr (97 upto 122) (*a..z*) |
|
43 (*TPTP formula forms*) |
|
44 val forms = [#"^", #"_", #"=", #"+", #"-"] |
|
45 |
|
46 (*lift a list of characters into a scanner combinator matching any one of the |
|
47 characters in that list.*) |
|
48 fun lift l = |
|
49 (map (Char.toString #> ($$)) l, Scan.fail) |
|
50 |-> fold (fn x => fn y => x || y) |
|
51 |
|
52 (*combinators for parsing letters and numbers*) |
|
53 val alpha = lift alphabetics |
|
54 val numer = lift numerics |
|
55 |
|
56 datatype suffix = |
|
57 Problem of |
|
58 ((*version*)int * |
|
59 (*size parameter*)int option) * |
|
60 (*extension*)string |
|
61 | Axiom of |
|
62 (*specialisation*)int * |
|
63 (*extension*)string |
|
64 |
|
65 val to_int = Int.fromString #> the |
|
66 val rm_ending = Scan.this_string "rm" |
|
67 val ax_ending = |
|
68 ((numer >> to_int) --| |
|
69 $$ "." -- (Scan.this_string "eq" || Scan.this_string "ax" || rm_ending)) |
|
70 >> Axiom |
|
71 val prob_ending = $$ "p" || $$ "g" || rm_ending |
|
72 val prob_suffix = |
|
73 ((numer >> to_int) -- |
|
74 Scan.option ($$ "." |-- numer ^^ numer ^^ numer >> to_int) --| $$ "." |
|
75 -- prob_ending) |
|
76 >> Problem |
|
77 |
|
78 type tptp_problem_name = |
|
79 {prob_domain : string, |
|
80 prob_number : int, |
|
81 prob_form : TPTP_Syntax.language, |
|
82 suffix : suffix} |
|
83 |
|
84 datatype problem_name = |
|
85 Standard of tptp_problem_name |
|
86 | Nonstandard of string |
|
87 |
|
88 exception TPTP_PROBLEM_NAME of string |
|
89 |
|
90 (*FIXME add graceful handling on non-wellformed TPTP filenames*) |
|
91 fun parse_problem_name str' : problem_name = |
|
92 let |
|
93 val str = Symbol.explode str' |
|
94 (*NOTE there's an ambiguity in the spec: there's no way of knowing if a |
|
95 file ending in "rm" used to be "ax" or "p". Here we default to "p".*) |
|
96 val ((((prob_domain, prob_number), prob_form), suffix), rest) = |
|
97 Scan.finite Symbol.stopper |
|
98 ((alpha ^^ alpha ^^ alpha) -- |
|
99 (numer ^^ numer ^^ numer >> to_int) -- |
|
100 lift forms -- (prob_suffix || ax_ending)) str |
|
101 |
|
102 fun parse_form str = |
|
103 case str of |
|
104 "^" => TPTP_Syntax.THF |
|
105 | "_" => TPTP_Syntax.TFF |
|
106 | "=" => TPTP_Syntax.TFF_with_arithmetic |
|
107 | "+" => TPTP_Syntax.FOF |
|
108 | "-" => TPTP_Syntax.CNF |
|
109 | _ => raise TPTP_PROBLEM_NAME ("Unknown TPTP form: " ^ str) |
|
110 in |
|
111 if null rest (*check if the whole name was parsed*) |
|
112 then |
|
113 Standard |
|
114 {prob_domain = prob_domain, |
|
115 prob_number = prob_number, |
|
116 prob_form = parse_form prob_form, |
|
117 suffix = suffix} |
|
118 handle _ => Nonstandard str' |
|
119 else raise TPTP_PROBLEM_NAME ("Parse error") |
|
120 end |
|
121 |
|
122 (*Produces an ASCII encoding of a TPTP problem-file name.*) |
|
123 fun mangle_problem_name (prob : problem_name) : string = |
|
124 case prob of |
|
125 Standard tptp_prob => |
|
126 let |
|
127 val prob_form = |
|
128 case #prob_form tptp_prob of |
|
129 TPTP_Syntax.THF => "_thf_" |
|
130 | TPTP_Syntax.TFF => "_tff_" |
|
131 | TPTP_Syntax.TFF_with_arithmetic => "_thfwa_" |
|
132 | TPTP_Syntax.FOF => "_fof_" |
|
133 | TPTP_Syntax.CNF => "_cnf_" |
|
134 val suffix = |
|
135 case #suffix tptp_prob of |
|
136 Problem ((version, size), extension) => |
|
137 Int.toString version ^ "_" ^ |
|
138 (if is_some size then Int.toString (the size) ^ "_" else "") ^ |
|
139 extension |
|
140 | Axiom (specialisation, extension) => |
|
141 Int.toString specialisation ^ "_" ^ extension |
|
142 in |
|
143 #prob_domain tptp_prob ^ |
|
144 Int.toString (#prob_number tptp_prob) ^ |
|
145 prob_form ^ |
|
146 suffix |
|
147 end |
|
148 | Nonstandard str => str |
|
149 |
|
150 end |