# HG changeset patch
# User blanchet
# Date 1387403720 -3600
# Node ID df56a01f5684c667ae1ccdac7acf3a6ea48f23f7
# Parent  c05ed63333023e87e84340eab77cd4b59d6b0b22
parse SPASS-Pirate types

diff -r c05ed6333302 -r df56a01f5684 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Dec 18 17:27:17 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Dec 18 22:55:20 2013 +0100
@@ -8,6 +8,7 @@
 
 signature ATP_PROOF =
 sig
+  type 'a atp_type = 'a ATP_Problem.atp_type
   type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term
   type atp_formula_role = ATP_Problem.atp_formula_role
   type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula
@@ -38,8 +39,7 @@
   type ('a, 'b) atp_step =
     atp_step_name * atp_formula_role * 'a * 'b * atp_step_name list
 
-  type 'a atp_proof =
-    (('a, 'a, ('a, 'a) atp_term, 'a) atp_formula, string) atp_step list
+  type 'a atp_proof = (('a, 'a, ('a, 'a atp_type) atp_term, 'a) atp_formula, string) atp_step list
 
   val agsyhol_core_rule : string
   val satallax_core_rule : string
@@ -50,23 +50,18 @@
   val short_output : bool -> string -> string
   val string_of_atp_failure : atp_failure -> string
   val extract_important_message : string -> string
-  val extract_known_atp_failure :
-    (atp_failure * string) list -> string -> atp_failure option
+  val extract_known_atp_failure : (atp_failure * string) list -> string -> atp_failure option
   val extract_tstplike_proof_and_outcome :
     bool -> (string * string) list -> (atp_failure * string) list -> string
     -> string * atp_failure option
   val is_same_atp_step : atp_step_name -> atp_step_name -> bool
   val scan_general_id : string list -> string * string list
-  val parse_formula :
-    string list
-    -> (string, 'a, (string, 'a) atp_term, string) atp_formula * string list
-  val atp_proof_of_tstplike_proof :
-    string atp_problem -> string -> string atp_proof
+  val parse_formula : string list ->
+    (string, string atp_type, (string, string atp_type) atp_term, string) atp_formula * string list
+  val atp_proof_of_tstplike_proof : string atp_problem -> string -> string atp_proof
   val clean_up_atp_proof_dependencies : string atp_proof -> string atp_proof
-  val map_term_names_in_atp_proof :
-    (string -> string) -> string atp_proof -> string atp_proof
-  val nasty_atp_proof :
-    string Symtab.table -> string atp_proof -> string atp_proof
+  val map_term_names_in_atp_proof : (string -> string) -> string atp_proof -> string atp_proof
+  val nasty_atp_proof : string Symtab.table -> string atp_proof -> string atp_proof
 end;
 
 structure ATP_Proof : ATP_PROOF =
@@ -203,11 +198,9 @@
     | _ => raise Fail "not Vampire")
   end
 
-type ('a, 'b) atp_step =
-  atp_step_name * atp_formula_role * 'a * 'b * atp_step_name list
+type ('a, 'b) atp_step = atp_step_name * atp_formula_role * 'a * 'b * atp_step_name list
 
-type 'a atp_proof =
-  (('a, 'a, ('a, 'a) atp_term, 'a) atp_formula, string) atp_step list
+type 'a atp_proof = (('a, 'a, ('a, 'a atp_type) atp_term, 'a) atp_formula, string) atp_step list
 
 (**** PARSING OF TSTP FORMAT ****)
 
@@ -245,8 +238,7 @@
   (parse_inference_source >> snd
    || scan_general_id --| skip_term >> single) x
 and parse_dependencies x =
-  (parse_dependency ::: Scan.repeat ($$ "," |-- parse_dependency)
-   >> flat) x
+  (parse_dependency ::: Scan.repeat ($$ "," |-- parse_dependency) >> flat) x
 and parse_file_source x =
   (Scan.this_string "file" |-- $$ "(" |-- scan_general_id
    -- Scan.option ($$ "," |-- scan_general_id) --| $$ ")") x
@@ -266,19 +258,28 @@
 
 fun list_app (f, args) = fold (fn arg => fn f => ATerm ((tptp_app, []), [f, arg])) args f
 
+fun parse_sort x = scan_general_id x
+and parse_sorts x = (parse_sort ::: Scan.repeat ($$ "&" |-- parse_sort)) x
+
+fun parse_type x =
+  (scan_general_id --| Scan.option ($$ "{" |-- parse_sorts --| $$ "}")
+    -- Scan.optional ($$ "(" |-- parse_types --| $$ ")") []
+   >> AType) x
+and parse_types x = (parse_type ::: Scan.repeat ($$ "," |-- parse_type)) x
+
 (* We currently ignore TFF and THF types. *)
-fun parse_type_stuff x = Scan.repeat (($$ tptp_has_type || $$ tptp_fun_type) |-- parse_arg) x
+fun parse_type_signature x = Scan.repeat (($$ tptp_has_type || $$ tptp_fun_type) |-- parse_arg) x
 and parse_arg x =
-  ($$ "(" |-- parse_term --| $$ ")" --| parse_type_stuff
-   || scan_general_id --| parse_type_stuff
-        -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") []
-      >> (ATerm o apfst (rpair []))) x
+  ($$ "(" |-- parse_term --| $$ ")" --| parse_type_signature
+   || scan_general_id --| parse_type_signature
+       -- Scan.optional ($$ "<" |-- parse_types --| $$ ">") []
+       -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") []
+     >> ATerm) x
 and parse_term x = (parse_arg -- Scan.repeat ($$ tptp_app |-- parse_arg) >> list_app) x
 and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x
 
 fun parse_atom x =
-  (parse_term -- Scan.option (Scan.option ($$ tptp_not_infix) --| $$ tptp_equal
-                              -- parse_term)
+  (parse_term -- Scan.option (Scan.option ($$ tptp_not_infix) --| $$ tptp_equal -- parse_term)
    >> (fn (u1, NONE) => AAtom u1
         | (u1, SOME (neg, u2)) =>
           AAtom (ATerm (("equal", []), [u1, u2])) |> is_some neg ? mk_anot)) x
@@ -424,8 +425,7 @@
 val parse_dot_name = scan_general_id --| $$ "." --| scan_general_id
 
 val parse_spass_annotations =
-  Scan.optional ($$ ":" |-- Scan.repeat (parse_dot_name
-                                         --| Scan.option ($$ ","))) []
+  Scan.optional ($$ ":" |-- Scan.repeat (parse_dot_name --| Scan.option ($$ ","))) []
 
 (* It is not clear why some literals are followed by sequences of stars and/or
    pluses. We ignore them. *)
@@ -460,7 +460,7 @@
 
 fun parse_spass_pirate_dependency x = (Scan.option ($$ "-") |-- scan_general_id) x
 fun parse_spass_pirate_dependencies x =
-  (parse_spass_pirate_dependency ::: Scan.repeat ($$ "," |-- parse_spass_pirate_dependency)) x
+  Scan.repeat (parse_spass_pirate_dependency --| Scan.option ($$ "," || $$ " ")) x
 fun parse_spass_pirate_file_source x =
   ((Scan.this_string "Input" || Scan.this_string "Conj") |-- $$ "(" |-- scan_general_id
      --| $$ ")") x
@@ -517,28 +517,37 @@
     (case core_of_agsyhol_proof tstp of
       SOME facts => facts |> map (core_inference agsyhol_core_rule)
     | NONE =>
-      tstp ^ "$"  (* the $ sign acts as a sentinel (FIXME: needed?) *)
+      tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
       |> parse_proof problem
       |> perhaps (try (sort (vampire_step_name_ord o pairself #1))))
 
 fun clean_up_dependencies _ [] = []
   | clean_up_dependencies seen ((name, role, u, rule, deps) :: steps) =
-    (name, role, u, rule,
-     map_filter (fn dep => find_first (is_same_atp_step dep) seen) deps) ::
+    (name, role, u, rule, map_filter (fn dep => find_first (is_same_atp_step dep) seen) deps) ::
     clean_up_dependencies (name :: seen) steps
 
 fun clean_up_atp_proof_dependencies proof = clean_up_dependencies [] proof
 
 fun map_term_names_in_atp_proof f =
   let
-    fun do_term (ATerm ((s, tys), ts)) = ATerm ((f s, tys), map do_term ts)
-    fun do_formula (AQuant (q, xs, phi)) =
-        AQuant (q, map (apfst f) xs, do_formula phi)
-      | do_formula (AConn (c, phis)) = AConn (c, map do_formula phis)
-      | do_formula (AAtom t) = AAtom (do_term t)
-    fun do_step (name, role, phi, rule, deps) =
-      (name, role, do_formula phi, rule, deps)
-  in map do_step end
+    fun map_type (AType (s, tys)) = AType (f s, map map_type tys)
+      | map_type (AFun (ty, ty')) = AFun (map_type ty, map_type ty')
+      | map_type (APi (ss, ty)) = APi (map f ss, map_type ty)
+
+    fun map_term (ATerm ((s, tys), ts)) = ATerm ((f s, map map_type tys), map map_term ts)
+      | map_term (AAbs (((s, ty), tm), args)) =
+        AAbs (((f s, map_type ty), map_term tm), map map_term args)
+
+    fun map_formula (AQuant (q, xs, phi)) =
+        AQuant (q, map (apfst f) xs, map_formula phi)
+      | map_formula (AConn (c, phis)) = AConn (c, map map_formula phis)
+      | map_formula (AAtom t) = AAtom (map_term t)
+
+    fun map_step (name, role, phi, rule, deps) =
+      (name, role, map_formula phi, rule, deps)
+  in
+    map map_step
+  end
 
 fun nasty_name pool s = s |> Symtab.lookup pool |> the_default s
 
diff -r c05ed6333302 -r df56a01f5684 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Dec 18 17:27:17 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Dec 18 22:55:20 2013 +0100
@@ -8,6 +8,7 @@
 
 signature ATP_PROOF_RECONSTRUCT =
 sig
+  type 'a atp_type = 'a ATP_Problem.atp_type
   type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term
   type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula
   type stature = ATP_Problem_Generate.stature
@@ -32,9 +33,9 @@
   val exists_of : term -> term -> term
   val unalias_type_enc : string -> string list
   val term_of_atp : Proof.context -> bool -> int Symtab.table -> typ option ->
-    (string, string) atp_term -> term
+    (string, string atp_type) atp_term -> term
   val prop_of_atp : Proof.context -> bool -> int Symtab.table ->
-    (string, string, (string, string) atp_term, string) atp_formula -> term
+    (string, string, (string, string atp_type) atp_term, string) atp_formula -> term
 
   val used_facts_in_atp_proof :
     Proof.context -> (string * stature) list vector -> string atp_proof -> (string * stature) list
@@ -107,20 +108,20 @@
     TFree (ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1)))
   end
 
-exception ATP_TERM of (string, string) atp_term list
+exception ATP_TERM of (string, string atp_type) atp_term list
 exception ATP_FORMULA of
-    (string, string, (string, string) atp_term, string) atp_formula list
+  (string, string, (string, string atp_type) atp_term, string) atp_formula list
 exception SAME of unit
 
-(* Type variables are given the basic sort "HOL.type". Some will later be
-   constrained by information from type literals, or by type inference. *)
+(* Type variables are given the basic sort "HOL.type". Some will later be constrained by information
+   from type literals, or by type inference. *)
 fun typ_of_atp ctxt (u as ATerm ((a, _), us)) =
   let val Ts = map (typ_of_atp ctxt) us in
     (case unprefix_and_unascii type_const_prefix a of
       SOME b => Type (invert_const b, Ts)
     | NONE =>
       if not (null us) then
-        raise ATP_TERM [u]  (* only "tconst"s have type arguments *)
+        raise ATP_TERM [u] (* only "tconst"s have type arguments *)
       else
         (case unprefix_and_unascii tfree_prefix a of
           SOME b => make_tfree ctxt b
@@ -320,8 +321,8 @@
       | norm_var_types t = t
   in t |> map_aterms norm_var_types |> fold_rev quant_of (map Var normTs) end
 
-(* Interpret an ATP formula as a HOL term, extracting sort constraints as they
-   appear in the formula. *)
+(* Interpret an ATP formula as a HOL term, extracting sort constraints as they appear in the
+   formula. *)
 fun prop_of_atp ctxt textual sym_tab phi =
   let
     fun do_formula pos phi =
@@ -337,11 +338,11 @@
         do_formula (pos |> c = AImplies ? not) phi1
         ##>> do_formula pos phi2
         #>> (case c of
-               AAnd => s_conj
-             | AOr => s_disj
-             | AImplies => s_imp
-             | AIff => s_iff
-             | ANot => raise Fail "impossible connective")
+              AAnd => s_conj
+            | AOr => s_disj
+            | AImplies => s_imp
+            | AIff => s_iff
+            | ANot => raise Fail "impossible connective")
       | AAtom tm => term_of_atom ctxt textual sym_tab pos tm
       | _ => raise ATP_FORMULA [phi])
   in
diff -r c05ed6333302 -r df56a01f5684 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 18 17:27:17 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 18 22:55:20 2013 +0100
@@ -84,8 +84,7 @@
   val SledgehammerN : string
   val plain_metis : reconstructor
   val select_smt_solver : string -> Proof.context -> Proof.context
-  val extract_reconstructor :
-    params -> reconstructor -> string * (string * string list) list
+  val extract_reconstructor : params -> reconstructor -> string * (string * string list) list
   val is_reconstructor : string -> bool
   val is_atp : theory -> string -> bool
   val is_smt_prover : Proof.context -> string -> bool
@@ -719,8 +718,7 @@
             val ord = effective_term_order ctxt name
             val full_proof = isar_proofs |> the_default (mode = Minimize)
             val args =
-              arguments ctxt full_proof extra
-                        (slice_timeout |> the_default one_day)
+              arguments ctxt full_proof extra (slice_timeout |> the_default one_day)
                         (File.shell_path prob_path) (ord, ord_info, sel_weights)
             val command =
               "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ ")"
@@ -728,26 +726,18 @@
             val _ =
               atp_problem
               |> lines_of_atp_problem format ord ord_info
-              |> cons ("% " ^ command ^ "\n" ^
-                (if comment = "" then "" else "% " ^ comment ^ "\n"))
+              |> cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n"))
               |> File.write_list prob_path
             val ((output, run_time), (atp_proof, outcome)) =
-              time_limit generous_slice_timeout Isabelle_System.bash_output
-                         command
-              |>> (if overlord then
-                     prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
-                   else
-                     I)
+              time_limit generous_slice_timeout Isabelle_System.bash_output command
+              |>> (if overlord then prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") else I)
               |> fst |> split_time
               |> (fn accum as (output, _) =>
                      (accum,
-                      extract_tstplike_proof_and_outcome verbose proof_delims
-                                                         known_failures output
+                      extract_tstplike_proof_and_outcome verbose proof_delims known_failures output
                       |>> atp_proof_of_tstplike_proof atp_problem
-                      handle UNRECOGNIZED_ATP_PROOF () =>
-                             ([], SOME ProofIncomplete)))
-              handle TimeLimit.TimeOut =>
-                     (("", the slice_timeout), ([], SOME TimedOut))
+                      handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete)))
+              handle TimeLimit.TimeOut => (("", the slice_timeout), ([], SOME TimedOut))
             val outcome =
               case outcome of
                 NONE =>