1.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Thu Sep 16 11:59:45 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Thu Sep 16 13:44:41 2010 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4      Author:     Claire Quigley, Cambridge University Computer Laboratory
     1.5      Author:     Jasmin Blanchette, TU Muenchen
     1.6  
     1.7 -Abstract representation of ATP proofs and TSTP/SPASS/Vampire syntax.
     1.8 +Abstract representation of ATP proofs and TSTP/Vampire/SPASS syntax.
     1.9  *)
    1.10  
    1.11  signature ATP_PROOF =
    1.12 @@ -21,8 +21,10 @@
    1.13  
    1.14    val step_num : step_name -> string
    1.15    val is_same_step : step_name * step_name -> bool
    1.16 -  val atp_proof_from_tstplike_string :
    1.17 -    string Symtab.table -> string -> string proof
    1.18 +  val atp_proof_from_tstplike_string : string -> string proof
    1.19 +  val map_term_names_in_atp_proof :
    1.20 +    (string -> string) -> string proof -> string proof
    1.21 +  val nasty_atp_proof : string Symtab.table -> string proof -> string proof
    1.22  end;
    1.23  
    1.24  structure ATP_Proof : ATP_PROOF =
    1.25 @@ -92,18 +94,6 @@
    1.26    || Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig
    1.27       >> (fn (ss1, ss2) => implode ss1 ^ implode ss2)
    1.28  
    1.29 -fun repair_name _ "$true" = "c_True"
    1.30 -  | repair_name _ "$false" = "c_False"
    1.31 -  | repair_name _ "$$e" = "c_equal" (* seen in Vampire proofs *)
    1.32 -  | repair_name _ "equal" = "c_equal" (* needed by SPASS? *)
    1.33 -  | repair_name pool s =
    1.34 -    case Symtab.lookup pool s of
    1.35 -      SOME s' => s'
    1.36 -    | NONE =>
    1.37 -      if String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s then
    1.38 -        "c_equal" (* seen in Vampire proofs *)
    1.39 -      else
    1.40 -        s
    1.41  (* Generalized first-order terms, which include file names, numbers, etc. *)
    1.42  fun parse_annotation strict x =
    1.43    ((scan_general_id ::: Scan.repeat ($$ " " |-- scan_general_id)
    1.44 @@ -123,18 +113,16 @@
    1.45  fun parse_vampire_detritus x =
    1.46    (scan_general_id |-- $$ ":" --| scan_general_id >> K []) x
    1.47  
    1.48 -fun parse_term pool x =
    1.49 -  ((scan_general_id >> repair_name pool)
    1.50 -    -- Scan.optional ($$ "(" |-- (parse_vampire_detritus || parse_terms pool)
    1.51 +fun parse_term x =
    1.52 +  (scan_general_id
    1.53 +    -- Scan.optional ($$ "(" |-- (parse_vampire_detritus || parse_terms)
    1.54                        --| $$ ")") []
    1.55      --| Scan.optional ($$ "(" |-- parse_vampire_detritus --| $$ ")") []
    1.56     >> ATerm) x
    1.57 -and parse_terms pool x =
    1.58 -  (parse_term pool ::: Scan.repeat ($$ "," |-- parse_term pool)) x
    1.59 +and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x
    1.60  
    1.61 -fun parse_atom pool =
    1.62 -  parse_term pool -- Scan.option (Scan.option ($$ "!") --| $$ "="
    1.63 -                                  -- parse_term pool)
    1.64 +val parse_atom =
    1.65 +  parse_term -- Scan.option (Scan.option ($$ "!") --| $$ "=" -- parse_term)
    1.66    >> (fn (u1, NONE) => AAtom u1
    1.67         | (u1, SOME (NONE, u2)) => AAtom (ATerm ("c_equal", [u1, u2]))
    1.68         | (u1, SOME (SOME _, u2)) =>
    1.69 @@ -144,20 +132,19 @@
    1.70  
    1.71  (* TPTP formulas are fully parenthesized, so we don't need to worry about
    1.72     operator precedence. *)
    1.73 -fun parse_formula pool x =
    1.74 -  (($$ "(" |-- parse_formula pool --| $$ ")"
    1.75 +fun parse_formula x =
    1.76 +  (($$ "(" |-- parse_formula --| $$ ")"
    1.77      || ($$ "!" >> K AForall || $$ "?" >> K AExists)
    1.78 -       --| $$ "[" -- parse_terms pool --| $$ "]" --| $$ ":"
    1.79 -       -- parse_formula pool
    1.80 +       --| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_formula
    1.81         >> (fn ((q, ts), phi) => AQuant (q, map fo_term_head ts, phi))
    1.82 -    || $$ "~" |-- parse_formula pool >> mk_anot
    1.83 -    || parse_atom pool)
    1.84 +    || $$ "~" |-- parse_formula >> mk_anot
    1.85 +    || parse_atom)
    1.86     -- Scan.option ((Scan.this_string "=>" >> K AImplies
    1.87                      || Scan.this_string "<=>" >> K AIff
    1.88                      || Scan.this_string "<~>" >> K ANotIff
    1.89                      || Scan.this_string "<=" >> K AIf
    1.90                      || $$ "|" >> K AOr || $$ "&" >> K AAnd)
    1.91 -                   -- parse_formula pool)
    1.92 +                   -- parse_formula)
    1.93     >> (fn (phi1, NONE) => phi1
    1.94          | (phi1, SOME (c, phi2)) => mk_aconn c (phi1, phi2))) x
    1.95  
    1.96 @@ -167,34 +154,34 @@
    1.97  
    1.98  (* Syntax: (fof|cnf)\(<num>, <formula_role>, <formula> <extra_arguments>\).
    1.99     The <num> could be an identifier, but we assume integers. *)
   1.100 - fun parse_tstp_line pool =
   1.101 -   ((Scan.this_string "fof" || Scan.this_string "cnf") -- $$ "(")
   1.102 -     |-- scan_general_id --| $$ "," -- Symbol.scan_id --| $$ ","
   1.103 -     -- parse_formula pool -- parse_tstp_extra_arguments --| $$ ")" --| $$ "."
   1.104 -    >> (fn (((num, role), phi), deps) =>
   1.105 -           let
   1.106 -             val (name, deps) =
   1.107 -               case deps of
   1.108 -                 ["file", _, s] => (Str (num, s), [])
   1.109 -               | _ => (Num num, deps)
   1.110 -           in
   1.111 -             case role of
   1.112 -               "definition" =>
   1.113 -               (case phi of
   1.114 -                  AConn (AIff, [phi1 as AAtom _, phi2]) =>
   1.115 -                  Definition (name, phi1, phi2)
   1.116 -                | AAtom (ATerm ("c_equal", _)) =>
   1.117 -                  (* Vampire's equality proxy axiom *)
   1.118 -                  Inference (name, phi, map Num deps)
   1.119 -                | _ => raise Fail "malformed definition")
   1.120 -             | _ => Inference (name, phi, map Num deps)
   1.121 -           end)
   1.122 +val parse_tstp_line =
   1.123 +  ((Scan.this_string "fof" || Scan.this_string "cnf") -- $$ "(")
   1.124 +    |-- scan_general_id --| $$ "," -- Symbol.scan_id --| $$ ","
   1.125 +    -- parse_formula -- parse_tstp_extra_arguments --| $$ ")" --| $$ "."
   1.126 +   >> (fn (((num, role), phi), deps) =>
   1.127 +          let
   1.128 +            val (name, deps) =
   1.129 +              case deps of
   1.130 +                ["file", _, s] => (Str (num, s), [])
   1.131 +              | _ => (Num num, deps)
   1.132 +          in
   1.133 +            case role of
   1.134 +              "definition" =>
   1.135 +              (case phi of
   1.136 +                 AConn (AIff, [phi1 as AAtom _, phi2]) =>
   1.137 +                 Definition (name, phi1, phi2)
   1.138 +               | AAtom (ATerm ("c_equal", _)) =>
   1.139 +                 (* Vampire's equality proxy axiom *)
   1.140 +                 Inference (name, phi, map Num deps)
   1.141 +               | _ => raise Fail "malformed definition")
   1.142 +            | _ => Inference (name, phi, map Num deps)
   1.143 +          end)
   1.144  
   1.145  (**** PARSING OF VAMPIRE OUTPUT ****)
   1.146  
   1.147  (* Syntax: <num>. <formula> <annotation> *)
   1.148 -fun parse_vampire_line pool =
   1.149 -  scan_general_id --| $$ "." -- parse_formula pool -- parse_annotation true
   1.150 +val parse_vampire_line =
   1.151 +  scan_general_id --| $$ "." -- parse_formula -- parse_annotation true
   1.152    >> (fn ((num, phi), deps) => Inference (Num num, phi, map Num deps))
   1.153  
   1.154  (**** PARSING OF SPASS OUTPUT ****)
   1.155 @@ -209,8 +196,8 @@
   1.156  
   1.157  (* It is not clear why some literals are followed by sequences of stars and/or
   1.158     pluses. We ignore them. *)
   1.159 -fun parse_decorated_atom pool =
   1.160 -  parse_atom pool --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")
   1.161 +val parse_decorated_atom =
   1.162 +  parse_atom --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")
   1.163  
   1.164  fun mk_horn ([], []) = AAtom (ATerm ("c_False", []))
   1.165    | mk_horn ([], pos_lits) = foldr1 (mk_aconn AOr) pos_lits
   1.166 @@ -219,26 +206,24 @@
   1.167      mk_aconn AImplies (foldr1 (mk_aconn AAnd) neg_lits,
   1.168                         foldr1 (mk_aconn AOr) pos_lits)
   1.169  
   1.170 -fun parse_horn_clause pool =
   1.171 -  Scan.repeat (parse_decorated_atom pool) --| $$ "|" --| $$ "|"
   1.172 -    -- Scan.repeat (parse_decorated_atom pool) --| $$ "-" --| $$ ">"
   1.173 -    -- Scan.repeat (parse_decorated_atom pool)
   1.174 +val parse_horn_clause =
   1.175 +  Scan.repeat parse_decorated_atom --| $$ "|" --| $$ "|"
   1.176 +    -- Scan.repeat parse_decorated_atom --| $$ "-" --| $$ ">"
   1.177 +    -- Scan.repeat parse_decorated_atom
   1.178    >> (mk_horn o apfst (op @))
   1.179  
   1.180  (* Syntax: <num>[0:<inference><annotations>]
   1.181     <atoms> || <atoms> -> <atoms>. *)
   1.182 -fun parse_spass_line pool =
   1.183 +val parse_spass_line =
   1.184    scan_general_id --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
   1.185 -    -- parse_spass_annotations --| $$ "]" -- parse_horn_clause pool --| $$ "."
   1.186 +    -- parse_spass_annotations --| $$ "]" -- parse_horn_clause --| $$ "."
   1.187    >> (fn ((num, deps), u) => Inference (Num num, u, map Num deps))
   1.188  
   1.189 -fun parse_line pool =
   1.190 -  parse_tstp_line pool || parse_vampire_line pool || parse_spass_line pool
   1.191 -fun parse_lines pool = Scan.repeat1 (parse_line pool)
   1.192 -fun parse_proof pool =
   1.193 +val parse_line = parse_tstp_line || parse_vampire_line || parse_spass_line
   1.194 +val parse_proof =
   1.195    fst o Scan.finite Symbol.stopper
   1.196              (Scan.error (!! (fn _ => raise Fail "unrecognized ATP output")
   1.197 -                            (parse_lines pool)))
   1.198 +                            (Scan.repeat1 parse_line)))
   1.199    o explode o strip_spaces_except_between_ident_chars (*### FIXME: why isn't strip_spaces enough?*)
   1.200  
   1.201  fun clean_up_dependency seen dep = find_first (curry is_same_step dep) seen
   1.202 @@ -249,10 +234,29 @@
   1.203      Inference (name, u, map_filter (clean_up_dependency seen) deps) ::
   1.204      clean_up_dependencies (name :: seen) steps
   1.205  
   1.206 -fun atp_proof_from_tstplike_string pool =
   1.207 +val atp_proof_from_tstplike_string =
   1.208    suffix "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
   1.209 -  #> parse_proof pool
   1.210 +  #> parse_proof
   1.211    #> sort (step_name_ord o pairself step_name)
   1.212    #> clean_up_dependencies []
   1.213  
   1.214 +fun map_term_names_in_term f (ATerm (s, ts)) =
   1.215 +  ATerm (f s, map (map_term_names_in_term f) ts)
   1.216 +fun map_term_names_in_formula f (AQuant (q, xs, phi)) =
   1.217 +    AQuant (q, xs, map_term_names_in_formula f phi)
   1.218 +  | map_term_names_in_formula f (AConn (c, phis)) =
   1.219 +    AConn (c, map (map_term_names_in_formula f) phis)
   1.220 +  | map_term_names_in_formula f (AAtom t) = AAtom (map_term_names_in_term f t)
   1.221 +fun map_term_names_in_step f (Definition (name, phi1, phi2)) =
   1.222 +    Definition (name, map_term_names_in_formula f phi1,
   1.223 +                map_term_names_in_formula f phi2)
   1.224 +  | map_term_names_in_step f (Inference (name, phi, deps)) =
   1.225 +    Inference (name, map_term_names_in_formula f phi, deps)
   1.226 +fun map_term_names_in_atp_proof f = map (map_term_names_in_step f)
   1.227 +
   1.228 +fun nasty_name pool s = s |> Symtab.lookup pool |> the_default s
   1.229 +fun nasty_atp_proof pool =
   1.230 +  if Symtab.is_empty pool then I
   1.231 +  else map_term_names_in_atp_proof (nasty_name pool)
   1.232 +
   1.233  end;

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Sep 16 11:59:45 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Sep 16 13:44:41 2010 +0200
     2.3 @@ -88,8 +88,7 @@
     2.4    | add_fact _ _ = I
     2.5  
     2.6  fun used_facts_in_tstplike_proof axiom_names =
     2.7 -  atp_proof_from_tstplike_string Symtab.empty
     2.8 -  #> rpair [] #-> fold (add_fact axiom_names)
     2.9 +  atp_proof_from_tstplike_string #> rpair [] #-> fold (add_fact axiom_names)
    2.10  
    2.11  fun used_facts axiom_names =
    2.12    used_facts_in_tstplike_proof axiom_names
    2.13 @@ -525,12 +524,24 @@
    2.14            ByMetis (fold (add_fact_from_dependency conjecture_shape axiom_names)
    2.15                          deps ([], [])))
    2.16  
    2.17 +fun repair_name "$true" = "c_True"
    2.18 +  | repair_name "$false" = "c_False"
    2.19 +  | repair_name "$$e" = "c_equal" (* seen in Vampire proofs *)
    2.20 +  | repair_name "equal" = "c_equal" (* needed by SPASS? *)
    2.21 +  | repair_name s =
    2.22 +    if String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s then
    2.23 +      "c_equal" (* seen in Vampire proofs *)
    2.24 +    else
    2.25 +      s
    2.26 +
    2.27  fun isar_proof_from_tstplike_proof pool ctxt full_types tfrees isar_shrink_factor
    2.28          tstplike_proof conjecture_shape axiom_names params frees =
    2.29    let
    2.30      val lines =
    2.31        tstplike_proof
    2.32 -      |> atp_proof_from_tstplike_string pool
    2.33 +      |> atp_proof_from_tstplike_string
    2.34 +      |> nasty_atp_proof pool
    2.35 +      |> map_term_names_in_atp_proof repair_name
    2.36        |> decode_lines ctxt full_types tfrees
    2.37        |> rpair [] |-> fold_rev (add_line conjecture_shape axiom_names)
    2.38        |> rpair [] |-> fold_rev add_nontrivial_line