src/HOL/Tools/ATP/atp_proof.ML
changeset 67022 49309fe530fd
parent 67021 41f1f8c4259b
child 68250 c45067867860
     1.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Nov 07 15:16:41 2017 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Nov 07 15:16:42 2017 +0100
     1.3 @@ -91,7 +91,7 @@
     1.4    val nasty_atp_proof : string Symtab.table -> string atp_proof -> string atp_proof
     1.5  
     1.6    val skip_term: string list -> string * string list
     1.7 -  val parse_thf0_formula :string list ->
     1.8 +  val parse_thf_formula :string list ->
     1.9      ('a, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term, 'c) ATP_Problem.atp_formula *
    1.10      string list
    1.11    val dummy_atype : string ATP_Problem.atp_type
    1.12 @@ -344,14 +344,24 @@
    1.13  
    1.14  fun parse_type x =
    1.15    (($$ "(" |-- parse_type --| $$ ")"
    1.16 +    || Scan.this_string tptp_pi_binder |-- $$ "[" |-- skip_term --| $$ "]" --| $$ ":" -- parse_type
    1.17 +       >> (fn (_, ty) => ty (* currently ignoring type constructor declarations anyway *))
    1.18      || (scan_general_id -- Scan.optional ($$ "{" |-- parse_classes --| $$ "}") [])
    1.19          -- Scan.optional ($$ "(" |-- parse_types --| $$ ")") []
    1.20         >> AType)
    1.21 -   -- Scan.option (($$ tptp_fun_type || $$ tptp_product_type) -- parse_type)
    1.22 +   -- Scan.option (($$ tptp_app || $$ tptp_fun_type || $$ tptp_product_type) -- parse_type)
    1.23    >> (fn (a, NONE) => a
    1.24 -       | (a, SOME (fun_or_product, b)) =>
    1.25 -         if fun_or_product = tptp_fun_type then AFun (a, b)
    1.26 -         else AType ((tptp_product_type, []), [a, b]))) x
    1.27 +       | (a, SOME (bin_op, b)) =>
    1.28 +         if bin_op = tptp_app then
    1.29 +           (case a of
    1.30 +             AType (s_clss, tys) => AType (s_clss, tys @ [b])
    1.31 +           | _ => raise UNRECOGNIZED_ATP_PROOF ())
    1.32 +         else if bin_op = tptp_fun_type then
    1.33 +           AFun (a, b)
    1.34 +         else if bin_op = tptp_product_type then
    1.35 +           AType ((tptp_product_type, []), [a, b])
    1.36 +         else
    1.37 +           raise Fail "impossible case")) x
    1.38  and parse_types x =
    1.39    (parse_type ::: Scan.repeat ($$ "," |-- parse_type)) x
    1.40  
    1.41 @@ -527,8 +537,8 @@
    1.42       --| Scan.option (Scan.this_string ","))
    1.43     || $$ "(" |-- parse_typed_var --| $$ ")") x
    1.44  
    1.45 -fun parse_simple_thf0_term x =
    1.46 -  (parse_fo_quantifier -- ($$ "[" |-- parse_typed_var --| $$ "]" --| $$ ":") -- parse_thf0_term
    1.47 +fun parse_simple_thf_term x =
    1.48 +  (parse_fo_quantifier -- ($$ "[" |-- parse_typed_var --| $$ "]" --| $$ ":") -- parse_thf_term
    1.49        >> (fn ((q, ys), t) =>
    1.50            fold_rev
    1.51              (fn (var, ty) => fn r =>
    1.52 @@ -538,23 +548,24 @@
    1.53                                  |> mk_simple_aterm)
    1.54                      else I))
    1.55              ys t)
    1.56 -  || Scan.this_string tptp_not |-- parse_thf0_term >> mk_app (mk_simple_aterm tptp_not)
    1.57 +  || Scan.this_string tptp_not |-- parse_thf_term >> mk_app (mk_simple_aterm tptp_not)
    1.58    || scan_general_id -- Scan.option ($$ tptp_has_type |-- parse_type)
    1.59      >> (fn (var, typ_opt) => ATerm ((var, the_list typ_opt), []))
    1.60    || parse_ho_quantifier >> mk_simple_aterm
    1.61 -  || $$ "(" |-- parse_thf0_term --| $$ ")"
    1.62 +  || $$ "(" |-- parse_thf_term --| $$ ")"
    1.63    || parse_binary_op >> mk_simple_aterm) x
    1.64 -and parse_thf0_term x =
    1.65 -  (parse_simple_thf0_term -- Scan.option (parse_binary_op -- parse_thf0_term)
    1.66 +and parse_thf_term x =
    1.67 +  (parse_simple_thf_term -- Scan.option (parse_binary_op -- parse_thf_term)
    1.68      >> (fn (t1, SOME (c, t2)) =>
    1.69             if c = tptp_app then mk_app t1 t2 else mk_apps (mk_simple_aterm c) [t1, t2]
    1.70           | (t, NONE) => t)) x
    1.71  
    1.72 -fun parse_thf0_formula x = (parse_thf0_term #>> remove_thf_app #>> AAtom) x
    1.73 +fun parse_thf_formula x = (parse_thf_term #>> remove_thf_app #>> AAtom) x
    1.74  
    1.75 -fun parse_tstp_thf0_line problem =
    1.76 +fun parse_tstp_thf_line problem =
    1.77    (Scan.this_string tptp_thf -- $$ "(") |-- scan_general_id --| $$ ","
    1.78 -  -- Symbol.scan_ascii_id --| $$ "," -- parse_thf0_formula -- parse_tstp_extra_arguments --| $$ ")"
    1.79 +  -- Symbol.scan_ascii_id --| $$ "," -- (parse_thf_formula || skip_term >> K dummy_phi)
    1.80 +     -- parse_tstp_extra_arguments --| $$ ")"
    1.81    --| $$ "."
    1.82    >> (fn (((num, role), phi), deps) =>
    1.83        let
    1.84 @@ -683,7 +694,8 @@
    1.85     >> map (core_inference z3_tptp_core_rule)) x
    1.86  
    1.87  fun parse_line local_name problem =
    1.88 -  if local_name = leo2N orelse local_name = leo3N then parse_tstp_thf0_line problem
    1.89 +  (* Satallax is handled separately, in "atp_satallax.ML". *)
    1.90 +  if local_name = leo2N orelse local_name = leo3N then parse_tstp_thf_line problem
    1.91    else if local_name = spassN then parse_spass_line
    1.92    else if local_name = pirateN then parse_pirate_line
    1.93    else if local_name = z3_tptpN then parse_z3_tptp_core_line