author blanchet Tue, 26 Jun 2012 11:14:40 +0200 changeset 48135 a44f34694406 parent 48134 fa23e699494c child 48136 0f9939676088
 src/HOL/Tools/ATP/atp_problem.ML file | annotate | diff | comparison | revisions src/HOL/Tools/ATP/atp_problem_generate.ML file | annotate | diff | comparison | revisions src/HOL/Tools/ATP/atp_proof.ML file | annotate | diff | comparison | revisions src/HOL/Tools/ATP/atp_proof_reconstruct.ML file | annotate | diff | comparison | revisions
```--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Jun 26 11:14:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Jun 26 11:14:40 2012 +0200
@@ -12,10 +12,10 @@
AAbs of (('a * 'b) * ('a, 'b) ho_term) * ('a, 'b) ho_term list
datatype quantifier = AForall | AExists
datatype connective = ANot | AAnd | AOr | AImplies | AIff
-  datatype ('a, 'b, 'c) formula =
-    ATyQuant of quantifier * 'b list * ('a, 'b, 'c) formula |
-    AQuant of quantifier * ('a * 'b option) list * ('a, 'b, 'c) formula |
-    AConn of connective * ('a, 'b, 'c) formula list |
+  datatype ('a, 'b, 'c, 'd) formula =
+    ATyQuant of quantifier * ('b * 'd list) list * ('a, 'b, 'c, 'd) formula |
+    AQuant of quantifier * ('a * 'b option) list * ('a, 'b, 'c, 'd) formula |
+    AConn of connective * ('a, 'b, 'c, 'd) formula list |
AAtom of 'c

datatype 'a ho_type =
@@ -46,7 +46,7 @@
datatype 'a problem_line =
Decl of string * 'a * 'a ho_type |
Formula of string * formula_role
-               * ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula
+               * ('a, 'a ho_type, ('a, 'a ho_type) ho_term, 'a) formula
* (string, string ho_type) ho_term option
* (string, string ho_type) ho_term list
type 'a problem = (string * 'a problem_line list) list
@@ -101,20 +101,21 @@
val atype_of_types : (string * string) ho_type
val bool_atype : (string * string) ho_type
val individual_atype : (string * string) ho_type
-  val mk_anot : ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula
+  val mk_anot : ('a, 'b, 'c, 'd) formula -> ('a, 'b, 'c, 'd) formula
val mk_aconn :
-    connective -> ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula
-    -> ('a, 'b, 'c) formula
+    connective -> ('a, 'b, 'c, 'd) formula -> ('a, 'b, 'c, 'd) formula
+    -> ('a, 'b, 'c, 'd) formula
val aconn_fold :
bool option -> (bool option -> 'a -> 'b -> 'b) -> connective * 'a list
-> 'b -> 'b
val aconn_map :
-    bool option -> (bool option -> 'a -> ('b, 'c, 'd) formula)
-    -> connective * 'a list -> ('b, 'c, 'd) formula
+    bool option -> (bool option -> 'a -> ('b, 'c, 'd, 'e) formula)
+    -> connective * 'a list -> ('b, 'c, 'd, 'e) formula
val formula_fold :
-    bool option -> (bool option -> 'c -> 'd -> 'd) -> ('a, 'b, 'c) formula
-    -> 'd -> 'd
-  val formula_map : ('c -> 'd) -> ('a, 'b, 'c) formula -> ('a, 'b, 'd) formula
+    bool option -> (bool option -> 'c -> 'e -> 'e) -> ('a, 'b, 'c, 'd) formula
+    -> 'e -> 'e
+  val formula_map :
+    ('c -> 'e) -> ('a, 'b, 'c, 'd) formula -> ('a, 'b, 'e, 'd) formula
val is_function_type : string ho_type -> bool
val is_predicate_type : string ho_type -> bool
val is_format_higher_order : atp_format -> bool
@@ -145,10 +146,10 @@
AAbs of (('a * 'b) * ('a, 'b) ho_term) * ('a, 'b) ho_term list
datatype quantifier = AForall | AExists
datatype connective = ANot | AAnd | AOr | AImplies | AIff
-datatype ('a, 'b, 'c) formula =
-  ATyQuant of quantifier * 'b list * ('a, 'b, 'c) formula |
-  AQuant of quantifier * ('a * 'b option) list * ('a, 'b, 'c) formula |
-  AConn of connective * ('a, 'b, 'c) formula list |
+datatype ('a, 'b, 'c, 'd) formula =
+  ATyQuant of quantifier * ('b * 'd list) list * ('a, 'b, 'c, 'd) formula |
+  AQuant of quantifier * ('a * 'b option) list * ('a, 'b, 'c, 'd) formula |
+  AConn of connective * ('a, 'b, 'c, 'd) formula list |
AAtom of 'c

datatype 'a ho_type =
@@ -179,7 +180,7 @@
datatype 'a problem_line =
Decl of string * 'a * 'a ho_type |
Formula of string * formula_role
-             * ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula
+             * ('a, 'a ho_type, ('a, 'a ho_type) ho_term, 'a) formula
* (string, string ho_type) ho_term option
* (string, string ho_type) ho_term list
type 'a problem = (string * 'a problem_line list) list
@@ -429,7 +430,8 @@
raise Fail "unexpected term in first-order format"
and tptp_string_for_formula format (ATyQuant (q, xs, phi)) =
tptp_string_for_quantifier q ^
-    "[" ^ commas (map (suffix_type_of_types o string_for_type format) xs) ^
+    "[" ^
+    commas (map (suffix_type_of_types o string_for_type format o fst) xs) ^
"]: " ^ tptp_string_for_formula format phi
|> enclose "(" ")"
| tptp_string_for_formula format (AQuant (q, xs, phi)) =
@@ -520,7 +522,7 @@
| str_for_conn _ AImplies = "implies"
| str_for_conn top_level AIff = "equiv" |> suffix_tag top_level
fun str_for_formula top_level (ATyQuant (q, xs, phi)) =
-        str_for_quant q ^ "_sorts([" ^ commas (map str_for_typ xs) ^
+        str_for_quant q ^ "_sorts([" ^ commas (map (str_for_typ o fst) xs) ^
"], " ^ str_for_formula top_level phi ^ ")"
| str_for_formula top_level (AQuant (q, xs, phi)) =
str_for_quant q ^ "([" ^
@@ -847,8 +849,9 @@
nice_name name ##>> nice_type ty ##>> nice_term tm
##>> pool_map nice_term args #>> AAbs
fun nice_formula (ATyQuant (q, xs, phi)) =
-        pool_map nice_type xs ##>> nice_formula phi
-        #>> (fn (xs, phi) => ATyQuant (q, xs, phi))
+        pool_map nice_type (map fst xs)
+        ##>> pool_map (pool_map nice_name) (map snd xs) ##>> nice_formula phi
+        #>> (fn ((tys, sorts), phi) => ATyQuant (q, tys ~~ sorts, phi))
| nice_formula (AQuant (q, xs, phi)) =
pool_map nice_name (map fst xs)
##>> pool_map (fn NONE => pair NONE```
```--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jun 26 11:14:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jun 26 11:14:40 2012 +0200
@@ -10,7 +10,7 @@
sig
type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
type connective = ATP_Problem.connective
-  type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
+  type ('a, 'b, 'c, 'd) formula = ('a, 'b, 'c, 'd) ATP_Problem.formula
type atp_format = ATP_Problem.atp_format
type formula_role = ATP_Problem.formula_role
type 'a problem = 'a ATP_Problem.problem
@@ -91,7 +91,7 @@
val type_enc_from_string : strictness -> string -> type_enc
val adjust_type_enc : atp_format -> type_enc -> type_enc
val mk_aconns :
-    connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
+    connective -> ('a, 'b, 'c, 'd) formula list -> ('a, 'b, 'c, 'd) formula
val unmangled_const : string -> string * (string, 'b) ho_term list
val unmangled_const_name : string -> string list
val helper_table : ((string * bool) * (status * thm) list) list
@@ -114,8 +114,6 @@
open ATP_Util
open ATP_Problem

-type name = string * string
-
datatype mode = Metis | Sledgehammer | Sledgehammer_Aggressive | Exporter

datatype scope = Global | Local | Assum | Chained
@@ -512,10 +510,10 @@

(* intermediate terms *)
datatype iterm =
-  IConst of name * typ * typ list |
-  IVar of name * typ |
+  IConst of (string * string) * typ * typ list |
+  IVar of (string * string) * typ |
IApp of iterm * iterm |
-  IAbs of (name * typ) * iterm
+  IAbs of ((string * string) * typ) * iterm

fun ityp_of (IConst (_, T, _)) = T
| ityp_of (IVar (_, T)) = T
@@ -829,7 +827,7 @@
{name : string,
stature : stature,
role : formula_role,
-   iformula : (name, typ, iterm) formula,
+   iformula : (string * string, typ, iterm, string * string) formula,
atomic_types : typ list}

fun update_iformula f ({name, stature, role, iformula, atomic_types} : ifact) =
@@ -1741,7 +1739,8 @@
(sorts ? mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts))
#> (if is_type_enc_native type_enc then
mk_atyquant AForall
-                      (map (fn TVar (x, _) => AType (tvar_name x, [])) Ts)
+              (map (fn TVar (x, S) =>
+                       (AType (tvar_name x, []), map (`make_type_class) S)) Ts)
else
mk_aquant AForall (map (fn TVar (x, _) => (tvar_name x, NONE)) Ts))

@@ -2076,7 +2075,7 @@
else
NONE
fun do_formula pos (ATyQuant (q, xs, phi)) =
-        ATyQuant (q, map (ho_type_from_typ type_enc false 0) xs,
+        ATyQuant (q, map (apfst (ho_type_from_typ type_enc false 0)) xs,
do_formula pos phi)
| do_formula pos (AQuant (q, xs, phi)) =
let
@@ -2573,6 +2572,7 @@
val ind =
case type_enc of
Native _ =>
+        (* ### FIXME: get rid of that, and move to "atp_problem.ML" *)
if String.isPrefix type_const_prefix s orelse
String.isPrefix tfree_prefix s then
atype_of_types```
```--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Jun 26 11:14:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Jun 26 11:14:40 2012 +0200
@@ -9,7 +9,7 @@
signature ATP_PROOF =
sig
type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
-  type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
+  type ('a, 'b, 'c, 'd) formula = ('a, 'b, 'c, 'd) ATP_Problem.formula
type 'a problem = 'a ATP_Problem.problem

exception UNRECOGNIZED_ATP_PROOF of unit
@@ -40,7 +40,7 @@
Definition_Step of step_name * 'a * 'a |
Inference_Step of step_name * 'a * string * step_name list

-  type 'a proof = ('a, 'a, ('a, 'a) ho_term) formula step list
+  type 'a proof = ('a, 'a, ('a, 'a) ho_term, 'a) formula step list

val short_output : bool -> string -> string
val string_for_failure : failure -> string
@@ -55,7 +55,7 @@
val satallax_unsat_coreN : string
val parse_formula :
string list
-    -> (string, 'a, (string, 'a) ho_term) formula * string list
+    -> (string, 'a, (string, 'a) ho_term, string) formula * string list
val atp_proof_from_tstplike_proof : string problem -> string -> string proof
val clean_up_atp_proof_dependencies : string proof -> string proof
val map_term_names_in_atp_proof :
@@ -222,7 +222,7 @@
Definition_Step of step_name * 'a * 'a |
Inference_Step of step_name * 'a * string * step_name list

-type 'a proof = ('a, 'a, ('a, 'a) ho_term) formula step list
+type 'a proof = ('a, 'a, ('a, 'a) ho_term, 'a) formula step list

fun step_name (Definition_Step (name, _, _)) = name
| step_name (Inference_Step (name, _, _, _)) = name```
```--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Jun 26 11:14:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Jun 26 11:14:40 2012 +0200
@@ -9,7 +9,7 @@
signature ATP_PROOF_RECONSTRUCT =
sig
type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
-  type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
+  type ('a, 'b, 'c, 'd) formula = ('a, 'b, 'c, 'd) ATP_Problem.formula
type 'a proof = 'a ATP_Proof.proof
type stature = ATP_Problem_Generate.stature

@@ -60,7 +60,7 @@
-> (string, string) ho_term -> term
val prop_from_atp :
Proof.context -> bool -> int Symtab.table
-    -> (string, string, (string, string) ho_term) formula -> term
+    -> (string, string, (string, string) ho_term, string) formula -> term
val isar_proof_text :
Proof.context -> bool -> isar_params -> one_line_params -> string
val proof_text :
@@ -326,7 +326,8 @@
(**** INTERPRETATION OF TSTP SYNTAX TREES ****)

exception HO_TERM of (string, string) ho_term list
-exception FORMULA of (string, string, (string, string) ho_term) formula list
+exception FORMULA of
+    (string, string, (string, string) ho_term, string) formula list
exception SAME of unit

(* Type variables are given the basic sort "HOL.type". Some will later be```