--- 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