--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Tue Apr 17 16:14:07 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Tue Apr 17 16:14:07 2012 +0100
@@ -825,21 +825,16 @@
{cautious = cautious,
problem_name =
SOME (TPTP_Problem_Name.parse_problem_name ((Path.base #> Path.implode)
- file_name))
- }
- handle _(*FIXME*) =>
- {cautious = cautious,
- problem_name = NONE
- }
+ file_name))}
in interpret_file' config [] path_prefix file_name end
fun import_file cautious path_prefix file_name type_map const_map thy =
let
val prob_name =
TPTP_Problem_Name.parse_problem_name (Path.implode (Path.base file_name))
- handle _(*FIXME*) => TPTP_Problem_Name.Nonstandard (Path.implode file_name)
val (result, thy') =
interpret_file cautious path_prefix file_name type_map const_map thy
+ (*FIXME doesn't check if problem has already been interpreted*)
in TPTP_Data.map (cons ((prob_name, result))) thy' end
val _ =
--- a/src/HOL/TPTP/TPTP_Parser/tptp_problem_name.ML Tue Apr 17 16:14:07 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_problem_name.ML Tue Apr 17 16:14:07 2012 +0100
@@ -56,7 +56,7 @@
datatype suffix =
Problem of
((*version*)int *
- (*size parameter*)int option) *
+ (*size parameter*)int option) *
(*extension*)string
| Axiom of
(*specialisation*)int *
@@ -94,10 +94,10 @@
(*NOTE there's an ambiguity in the spec: there's no way of knowing if a
file ending in "rm" used to be "ax" or "p". Here we default to "p".*)
val ((((prob_domain, prob_number), prob_form), suffix), rest) =
- Scan.finite Symbol.stopper
- ((alpha ^^ alpha ^^ alpha) --
- (numer ^^ numer ^^ numer >> to_int) --
- lift forms -- (prob_suffix || ax_ending)) str
+ Scan.finite Symbol.stopper
+ ((alpha ^^ alpha ^^ alpha) --
+ (numer ^^ numer ^^ numer >> to_int) --
+ lift forms -- (prob_suffix || ax_ending)) str
fun parse_form str =
case str of
@@ -115,36 +115,41 @@
prob_number = prob_number,
prob_form = parse_form prob_form,
suffix = suffix}
- handle _ => Nonstandard str'
else raise TPTP_PROBLEM_NAME ("Parse error")
end
+ handle exn =>
+ (*FIXME brittle*)
+ if General.exnName exn = "FAIL" andalso General.exnMessage exn = "FAIL NONE" then
+ (*It's very likely that the scanner failed*)
+ Nonstandard str'
+ else reraise exn
(*Produces an ASCII encoding of a TPTP problem-file name.*)
fun mangle_problem_name (prob : problem_name) : string =
case prob of
- Standard tptp_prob =>
- let
- val prob_form =
- case #prob_form tptp_prob of
- TPTP_Syntax.THF => "_thf_"
- | TPTP_Syntax.TFF => "_tff_"
- | TPTP_Syntax.TFF_with_arithmetic => "_thfwa_"
- | TPTP_Syntax.FOF => "_fof_"
- | TPTP_Syntax.CNF => "_cnf_"
- val suffix =
- case #suffix tptp_prob of
- Problem ((version, size), extension) =>
- Int.toString version ^ "_" ^
- (if is_some size then Int.toString (the size) ^ "_" else "") ^
- extension
- | Axiom (specialisation, extension) =>
- Int.toString specialisation ^ "_" ^ extension
- in
- #prob_domain tptp_prob ^
- Int.toString (#prob_number tptp_prob) ^
- prob_form ^
- suffix
- end
- | Nonstandard str => str
+ Standard tptp_prob =>
+ let
+ val prob_form =
+ case #prob_form tptp_prob of
+ TPTP_Syntax.THF => "_thf_"
+ | TPTP_Syntax.TFF => "_tff_"
+ | TPTP_Syntax.TFF_with_arithmetic => "_thfwa_"
+ | TPTP_Syntax.FOF => "_fof_"
+ | TPTP_Syntax.CNF => "_cnf_"
+ val suffix =
+ case #suffix tptp_prob of
+ Problem ((version, size), extension) =>
+ Int.toString version ^ "_" ^
+ (if is_some size then Int.toString (the size) ^ "_" else "") ^
+ extension
+ | Axiom (specialisation, extension) =>
+ Int.toString specialisation ^ "_" ^ extension
+ in
+ #prob_domain tptp_prob ^
+ Int.toString (#prob_number tptp_prob) ^
+ prob_form ^
+ suffix
+ end
+ | Nonstandard str => str
end