author blanchet Sun, 01 May 2011 18:37:24 +0200 changeset 42531 a462dbaa584f parent 42530 f64c546efe8c child 42532 7849e1d10584
added more rudimentary type support to Sledgehammer's ATP encoding
```--- a/src/HOL/Tools/ATP/atp_problem.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Sun May 01 18:37:24 2011 +0200
@@ -10,16 +10,15 @@
datatype 'a fo_term = ATerm of 'a * 'a fo_term list
datatype quantifier = AForall | AExists
datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
-  datatype ('a, 'b) formula =
-    AQuant of quantifier * ('a * 'b option) list * ('a, 'b) formula |
-    AConn of connective * ('a, 'b) formula list |
-    AAtom of 'b
-  type 'a uniform_formula = ('a, 'a fo_term) formula
+  datatype ('a, 'b, 'c) formula =
+    AQuant of quantifier * ('a * 'b option) list * ('a, 'b, 'c) formula |
+    AConn of connective * ('a, 'b, 'c) formula list |
+    AAtom of 'c

datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
Type_Decl of string * 'a * 'a list * 'a |
-    Formula of string * formula_kind * ('a, 'a fo_term) formula
+    Formula of string * formula_kind * ('a, 'a, 'a fo_term) formula
* string fo_term option * string fo_term option
type 'a problem = (string * 'a problem_line list) list

@@ -41,16 +40,15 @@
datatype 'a fo_term = ATerm of 'a * 'a fo_term list
datatype quantifier = AForall | AExists
datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
-datatype ('a, 'b) formula =
-  AQuant of quantifier * ('a * 'b option) list * ('a, 'b) formula |
-  AConn of connective * ('a, 'b) formula list |
-  AAtom of 'b
-type 'a uniform_formula = ('a, 'a fo_term) formula
+datatype ('a, 'b, 'c) formula =
+  AQuant of quantifier * ('a * 'b option) list * ('a, 'b, 'c) formula |
+  AConn of connective * ('a, 'b, 'c) formula list |
+  AAtom of 'c

datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
Type_Decl of string * 'a * 'a list * 'a |
-  Formula of string * formula_kind * ('a, 'a fo_term) formula
+  Formula of string * formula_kind * ('a, 'a, 'a fo_term) formula
* string fo_term option * string fo_term option
type 'a problem = (string * 'a problem_line list) list

@@ -80,7 +78,7 @@
| string_for_connective AIff = "<=>"
| string_for_connective ANotIff = "<~>"
fun string_for_bound_var (s, NONE) = s
-  | string_for_bound_var (s, SOME ty) = s ^ " : " ^ string_for_term ty
+  | string_for_bound_var (s, SOME ty) = s ^ " : " ^ ty
fun string_for_formula (AQuant (q, xs, phi)) =
"(" ^ string_for_quantifier q ^
"[" ^ commas (map string_for_bound_var xs) ^ "] : " ^
@@ -201,7 +199,7 @@
fun nice_formula (AQuant (q, xs, phi)) =
pool_map nice_name (map fst xs)
##>> pool_map (fn NONE => pair NONE
-                    | SOME ty => nice_term ty #>> SOME) (map snd xs)
+                    | SOME ty => nice_name ty #>> SOME) (map snd xs)
##>> nice_formula phi
#>> (fn ((ss, ts), phi) => AQuant (q, ss ~~ ts, phi))
| nice_formula (AConn (c, phis)) =```
```--- a/src/HOL/Tools/ATP/atp_proof.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Sun May 01 18:37:24 2011 +0200
@@ -9,7 +9,7 @@
signature ATP_PROOF =
sig
type 'a fo_term = 'a ATP_Problem.fo_term
-  type 'a uniform_formula = 'a ATP_Problem.uniform_formula
+  type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula

datatype failure =
Unprovable | IncompleteUnprovable | ProofMissing | UnsoundProof |
@@ -23,7 +23,7 @@
Definition of step_name * 'a * 'a |
Inference of step_name * 'a * step_name list

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

val strip_spaces : (char -> bool) -> string -> string
val short_output : bool -> string -> string
@@ -203,7 +203,7 @@
Definition of step_name * 'a * 'a |
Inference of step_name * 'a * step_name list

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

fun step_name (Definition (name, _, _)) = name
| step_name (Inference (name, _, _)) = name```
```--- a/src/HOL/Tools/Metis/metis_translate.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Sun May 01 18:37:24 2011 +0200
@@ -68,6 +68,7 @@
theory -> string list -> class list -> class list * arity_clause list
val combtyp_of : combterm -> combtyp
val strip_combterm_comb : combterm -> combterm * combterm list
+  val combtyp_from_typ : typ -> combtyp
val combterm_from_term :
theory -> (string * typ) list -> term -> combterm * typ list
val reveal_old_skolem_terms : (string * term) list -> term -> term
@@ -393,23 +394,24 @@
|   stripc  x =  x
in stripc(u,[]) end

-fun combtype_of (Type (a, Ts)) =
-    let val (folTypes, ts) = combtypes_of Ts in
-      (CombType (`make_fixed_type_const a, folTypes), ts)
+fun combtyp_and_sorts_from_type (Type (a, Ts)) =
+    let val (tys, ts) = combtyps_and_sorts_from_types Ts in
+      (CombType (`make_fixed_type_const a, tys), ts)
end
-  | combtype_of (tp as TFree (a, _)) = (CombTFree (`make_fixed_type_var a), [tp])
-  | combtype_of (tp as TVar (x, _)) =
+  | combtyp_and_sorts_from_type (tp as TFree (a, _)) =
+    (CombTFree (`make_fixed_type_var a), [tp])
+  | combtyp_and_sorts_from_type (tp as TVar (x, _)) =
(CombTVar (make_schematic_type_var x, string_of_indexname x), [tp])
-and combtypes_of Ts =
-  let val (folTyps, ts) = ListPair.unzip (map combtype_of Ts) in
-    (folTyps, union_all ts)
+and combtyps_and_sorts_from_types Ts =
+  let val (tys, ts) = ListPair.unzip (map combtyp_and_sorts_from_type Ts) in
+    (tys, union_all ts)
end

(* same as above, but no gathering of sort information *)
-fun simple_combtype_of (Type (a, Ts)) =
-    CombType (`make_fixed_type_const a, map simple_combtype_of Ts)
-  | simple_combtype_of (TFree (a, _)) = CombTFree (`make_fixed_type_var a)
-  | simple_combtype_of (TVar (x, _)) =
+fun combtyp_from_typ (Type (a, Ts)) =
+    CombType (`make_fixed_type_const a, map combtyp_from_typ Ts)
+  | combtyp_from_typ (TFree (a, _)) = CombTFree (`make_fixed_type_var a)
+  | combtyp_from_typ (TVar (x, _)) =
CombTVar (make_schematic_type_var x, string_of_indexname x)

fun new_skolem_const_name s num_T_args =
@@ -425,37 +427,35 @@
in (CombApp (P', Q'), union (op =) tsP tsQ) end
| combterm_from_term thy _ (Const (c, T)) =
let
-        val (tp, ts) = combtype_of T
+        val (tp, ts) = combtyp_and_sorts_from_type T
val tvar_list =
(if String.isPrefix old_skolem_const_prefix c then
[] |> Term.add_tvarsT T |> map TVar
else
(c, T) |> Sign.const_typargs thy)
-          |> map simple_combtype_of
+          |> map combtyp_from_typ
val c' = CombConst (`make_fixed_const c, tp, tvar_list)
in  (c',ts)  end
| combterm_from_term _ _ (Free (v, T)) =
-      let val (tp, ts) = combtype_of T
+      let val (tp, ts) = combtyp_and_sorts_from_type T
val v' = CombConst (`make_fixed_var v, tp, [])
in  (v',ts)  end
| combterm_from_term _ _ (Var (v as (s, _), T)) =
let
-      val (tp, ts) = combtype_of T
+      val (tp, ts) = combtyp_and_sorts_from_type T
val v' =
if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
let
val tys = T |> strip_type |> swap |> op ::
val s' = new_skolem_const_name s (length tys)
-          in
-            CombConst (`make_fixed_const s', tp, map simple_combtype_of tys)
-          end
+          in CombConst (`make_fixed_const s', tp, map combtyp_from_typ tys) end
else
CombVar ((make_schematic_var v, string_of_indexname v), tp)
in (v', ts) end
| combterm_from_term _ bs (Bound j) =
let
val (s, T) = nth bs j
-        val (tp, ts) = combtype_of T
+        val (tp, ts) = combtyp_and_sorts_from_type T
val v' = CombConst (`make_bound_var s, tp, [])
in (v', ts) end
| combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"```
```--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
@@ -272,7 +272,7 @@
(**** INTERPRETATION OF TSTP SYNTAX TREES ****)

exception FO_TERM of string fo_term list
-exception FORMULA of (string, string fo_term) formula list
+exception FORMULA of (string, string, string fo_term) formula list
exception SAME of unit

(* Type variables are given the basic sort "HOL.type". Some will later be```
```--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
@@ -49,13 +49,18 @@
val arity_clause_prefix = "arity_"
val tfree_prefix = "tfree_"

+val is_base = "is"
+val type_prefix = "ty_"
+
+fun make_type ty = type_prefix ^ ascii_of ty
+
(* Freshness almost guaranteed! *)
val sledgehammer_weak_prefix = "Sledgehammer:"

type translated_formula =
{name: string,
kind: formula_kind,
-   combformula: (name, combterm) formula,
+   combformula: (name, combtyp, combterm) formula,
ctypes_sorts: typ list}

datatype type_system =
@@ -75,13 +80,14 @@
| type_system_types_dangerous_types type_sys = is_type_system_sound type_sys

fun dont_need_type_args type_sys s =
-  member (op =) [@{const_name HOL.eq}, @{const_name Metis.fequal}] s orelse
-  case type_sys of
-    Many_Typed => true
-  | Tags full_types => full_types
-  | Args full_types => full_types
-  | Mangled full_types => full_types
-  | No_Types => true
+  s <> is_base andalso
+  (member (op =) [@{const_name HOL.eq}, @{const_name Metis.fequal}] s orelse
+   case type_sys of
+     Many_Typed => true
+   | Tags full_types => full_types
+   | Args full_types => full_types
+   | Mangled full_types => full_types
+   | No_Types => true)

datatype type_arg_policy = No_Type_Args | Explicit_Type_Args | Mangled_Types

@@ -90,8 +96,10 @@
else case type_sys of Mangled _ => Mangled_Types | _ => Explicit_Type_Args

fun num_atp_type_args thy type_sys s =
-  if type_arg_policy type_sys s = Explicit_Type_Args then num_type_args thy s
-  else 0
+  if type_arg_policy type_sys s = Explicit_Type_Args then
+    if s = is_base then 1 else num_type_args thy s
+  else
+    0

fun atp_type_literals_for_types type_sys kind Ts =
if type_sys = No_Types then
@@ -121,14 +129,13 @@
|> filter_out (member (op =) bounds o fst))
in mk_aquant AForall (formula_vars [] phi []) phi end

-fun combterm_vars (CombApp (ct, cu)) = fold combterm_vars [ct, cu]
+fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2]
| combterm_vars (CombConst _) = I
-  | combterm_vars (CombVar (name, _)) =
-    insert (op =) (name, NONE) (* FIXME: TFF *)
+  | combterm_vars (CombVar (name, ty)) = insert (op =) (name, SOME ty)
val close_combformula_universally = close_universally combterm_vars

fun term_vars (ATerm (name as (s, _), tms)) =
-  is_atp_variable s ? insert (op =) (name, NONE) (* FIXME: TFF *)
+  is_atp_variable s ? insert (op =) (name, NONE)
#> fold term_vars tms
val close_formula_universally = close_universally term_vars

@@ -140,16 +147,14 @@
fun do_quant bs q s T t' =
let val s = Name.variant (map fst bs) s in
do_formula ((s, T) :: bs) t'
-        (* FIXME: TFF *)
-        #>> (fn phi => AQuant (q, [(`make_bound_var s, NONE)], phi))
+        #>> mk_aquant q [(`make_bound_var s, SOME (combtyp_from_typ T))]
end
and do_conn bs c t1 t2 =
do_formula bs t1 ##>> do_formula bs t2
-      #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))
+      #>> uncurry (mk_aconn c)
and do_formula bs t =
case t of
-        @{const Not} \$ t1 =>
-        do_formula bs t1 #>> (fn phi => AConn (ANot, [phi]))
+        @{const Not} \$ t1 => do_formula bs t1 #>> mk_anot
| Const (@{const_name All}, _) \$ Abs (s, T, t') =>
do_quant bs AForall s T t'
| Const (@{const_name Ex}, _) \$ Abs (s, T, t') =>
@@ -414,16 +419,20 @@
(* We are crossing our fingers that it doesn't clash with anything else. *)
val mangled_type_sep = "\000"

-fun mangled_combtyp f (CombTFree name) = f name
-  | mangled_combtyp f (CombTVar name) =
+fun mangled_combtyp_component f (CombTFree name) = f name
+  | mangled_combtyp_component f (CombTVar name) =
f name (* FIXME: shouldn't happen *)
(* raise Fail "impossible schematic type variable" *)
-  | mangled_combtyp f (CombType (name, tys)) =
-    "(" ^ commas (map (mangled_combtyp f) tys) ^ ")" ^ f name
+  | mangled_combtyp_component f (CombType (name, tys)) =
+    "(" ^ commas (map (mangled_combtyp_component f) tys) ^ ")" ^ f name
+
+fun mangled_combtyp ty =
+  (make_type (mangled_combtyp_component fst ty),
+   mangled_combtyp_component snd ty)

fun mangled_type_suffix f g tys =
-  fold_rev (curry (op ^) o g o prefix mangled_type_sep o mangled_combtyp f)
-           tys ""
+  fold_rev (curry (op ^) o g o prefix mangled_type_sep
+            o mangled_combtyp_component f) tys ""

val parse_mangled_ident =
Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
@@ -447,6 +456,11 @@
(hd ss, map unmangled_type (tl ss))
end

+fun pred_combtyp ty =
+  case combtyp_from_typ @{typ "unit => bool"} of
+    CombType (name, [_, bool_ty]) => CombType (name, [ty, bool_ty])
+  | _ => raise Fail "expected two-argument type constructor"
+
fun formula_for_combformula ctxt type_sys =
let
fun do_term top_level u =
@@ -487,8 +501,25 @@
else
I)
end
+    val do_bound_type =
+      if type_sys = Many_Typed then SOME o mangled_combtyp else K NONE
+    val do_out_of_bound_type =
+      if member (op =) [Args true, Mangled true] type_sys then
+        (fn (s, ty) =>
+            CombApp (CombConst ((const_prefix ^ is_base, is_base),
+                                pred_combtyp ty, [ty]),
+                     CombVar (s, ty))
+            |> AAtom |> formula_for_combformula ctxt type_sys |> SOME)
+      else
+        K NONE
fun do_formula (AQuant (q, xs, phi)) =
-        AQuant (q, map (apsnd (Option.map (do_term true))) xs, do_formula phi)
+        AQuant (q, xs |> map (apsnd (fn NONE => NONE
+                                      | SOME ty => do_bound_type ty)),
+                (if q = AForall then mk_ahorn else fold (mk_aconn AAnd))
+                    (map_filter
+                         (fn (_, NONE) => NONE
+                           | (s, SOME ty) => do_out_of_bound_type (s, ty)) xs)
+                    (do_formula phi))
| do_formula (AConn (c, phis)) = AConn (c, map do_formula phis)
| do_formula (AAtom tm) = AAtom (do_term true tm)
in do_formula end```