src/HOL/Tools/ATP/atp_proof.ML
changeset 42536 a513730db7b0
parent 42531 a462dbaa584f
child 42543 f9d402d144d4
equal deleted inserted replaced
42535:3c1f302b3ee6 42536:a513730db7b0
   208 fun step_name (Definition (name, _, _)) = name
   208 fun step_name (Definition (name, _, _)) = name
   209   | step_name (Inference (name, _, _)) = name
   209   | step_name (Inference (name, _, _)) = name
   210 
   210 
   211 (**** PARSING OF TSTP FORMAT ****)
   211 (**** PARSING OF TSTP FORMAT ****)
   212 
   212 
   213 (*Strings enclosed in single quotes, e.g. filenames*)
   213 (* Strings enclosed in single quotes (e.g., file names) *)
   214 val scan_general_id =
   214 val scan_general_id =
   215   $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode
   215   $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode
   216   || Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig
   216   || Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig
   217      >> (fn (ss1, ss2) => implode ss1 ^ implode ss2)
   217      >> (fn (ss1, ss2) => implode ss1 ^ implode ss2)
   218 
   218 
   275 val parse_tstp_extra_arguments =
   275 val parse_tstp_extra_arguments =
   276   Scan.optional ($$ "," |-- parse_annotation false
   276   Scan.optional ($$ "," |-- parse_annotation false
   277                  --| Scan.option ($$ "," |-- parse_annotations false)) []
   277                  --| Scan.option ($$ "," |-- parse_annotations false)) []
   278 
   278 
   279 val vampire_unknown_fact = "unknown"
   279 val vampire_unknown_fact = "unknown"
       
   280 val tofof_fact_prefix = "fof_"
   280 
   281 
   281 (* Syntax: (cnf|fof|tff)\(<num>, <formula_role>, <formula> <extra_arguments>\).
   282 (* Syntax: (cnf|fof|tff)\(<num>, <formula_role>, <formula> <extra_arguments>\).
   282    The <num> could be an identifier, but we assume integers. *)
   283    The <num> could be an identifier, but we assume integers. *)
   283 val parse_tstp_line =
   284 val parse_tstp_line =
   284   ((Scan.this_string "cnf" || Scan.this_string "fof" || Scan.this_string "tff")
   285   ((Scan.this_string "cnf" || Scan.this_string "fof" || Scan.this_string "tff")
   288    >> (fn (((num, role), phi), deps) =>
   289    >> (fn (((num, role), phi), deps) =>
   289           let
   290           let
   290             val (name, deps) =
   291             val (name, deps) =
   291               case deps of
   292               case deps of
   292                 ["file", _, s] =>
   293                 ["file", _, s] =>
   293                 ((num, if s = vampire_unknown_fact then NONE else SOME s), [])
   294                 ((num,
       
   295                   if s = vampire_unknown_fact then NONE
       
   296                   else SOME (s |> perhaps (try (unprefix tofof_fact_prefix)))),
       
   297                  [])
   294               | _ => ((num, NONE), deps)
   298               | _ => ((num, NONE), deps)
   295           in
   299           in
   296             case role of
   300             case role of
   297               "definition" =>
   301               "definition" =>
   298               (case phi of
   302               (case phi of