--- a/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Jul 20 00:37:42 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Jul 20 00:37:42 2011 +0200
@@ -307,7 +307,7 @@
(SOME b, [T]) => (b, T)
| _ => raise HO_TERM [u]
-(** Accumulate type constraints in a formula: negative type literals **)
+(* Accumulate type constraints in a formula: negative type literals. *)
fun add_var (key, z) = Vartab.map_default (key, []) (cons z)
fun add_type_constraint false (cl, TFree (a ,_)) = add_var ((a, ~1), cl)
| add_type_constraint false (cl, TVar (ix, _)) = add_var (ix, cl)
@@ -330,6 +330,15 @@
| _ => s
end
+(* The number of type arguments of a constant, zero if it's monomorphic. For
+ (instances of) Skolem pseudoconstants, this information is encoded in the
+ constant name. *)
+fun num_type_args thy s =
+ if String.isPrefix skolem_const_prefix s then
+ s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
+ else
+ (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
+
fun slack_fastype_of t = fastype_of t handle TERM _ => HOLogic.typeT
(* First-order translation. No types are known for variables. "HOLogic.typeT"
@@ -417,7 +426,9 @@
val T = map slack_fastype_of ts ---> HOLogic.typeT
val t =
case strip_prefix_and_unascii fixed_var_prefix a of
- SOME b => Free (b, T)
+ SOME b =>
+ (* FIXME: reconstruction of lambda-lifting *)
+ Free (b, T)
| NONE =>
case strip_prefix_and_unascii schematic_var_prefix a of
SOME b => Var ((b, var_index), T)
--- a/src/HOL/Tools/ATP/atp_translate.ML Wed Jul 20 00:37:42 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Jul 20 00:37:42 2011 +0200
@@ -71,7 +71,6 @@
val invert_const : string -> string
val unproxify_const : string -> string
val new_skolem_var_name_from_const : string -> string
- val num_type_args : theory -> string -> int
val atp_irrelevant_consts : string list
val atp_schematic_consts_of : term -> typ list Symtab.table
val is_locality_global : locality -> bool
@@ -126,6 +125,9 @@
val type_const_prefix = "tc_"
val class_prefix = "cl_"
+(* TODO: Use a more descriptive prefix in "SMT_Translate.lift_lambdas". *)
+val lambda_lifted_prefix = Name.uu
+
val skolem_const_prefix = "ATP" ^ Long_Name.separator ^ "Sko"
val old_skolem_const_prefix = skolem_const_prefix ^ "o"
val new_skolem_const_prefix = skolem_const_prefix ^ "n"
@@ -301,15 +303,6 @@
nth ss (length ss - 2)
end
-(* The number of type arguments of a constant, zero if it's monomorphic. For
- (instances of) Skolem pseudoconstants, this information is encoded in the
- constant name. *)
-fun num_type_args thy s =
- if String.isPrefix skolem_const_prefix s then
- s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
- else
- (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
-
(* These are either simplified away by "Meson.presimplify" (most of the time) or
handled specially via "fFalse", "fTrue", ..., "fequal". *)
val atp_irrelevant_consts =
@@ -479,16 +472,16 @@
val (Q', Q_atomics_Ts) = iterm_from_term thy bs Q
in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
| iterm_from_term thy _ (Const (c, T)) =
- let
- 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)
- val c' = IConst (`make_fixed_const c, T, tvar_list)
- in (c', atyps_of T) end
- | iterm_from_term _ _ (Free (v, T)) =
- (IConst (`make_fixed_var v, T, []), atyps_of T)
+ (IConst (`make_fixed_const c, T,
+ if String.isPrefix old_skolem_const_prefix c then
+ [] |> Term.add_tvarsT T |> map TVar
+ else
+ (c, T) |> Sign.const_typargs thy),
+ atyps_of T)
+ | iterm_from_term _ _ (Free (s, T)) =
+ (IConst (`make_fixed_var s, T,
+ if String.isPrefix lambda_lifted_prefix s then [T] else []),
+ atyps_of T)
| iterm_from_term _ _ (Var (v as (s, _), T)) =
(if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
let
@@ -1414,7 +1407,8 @@
fold (fold_type_constrs f) Ts (f (s, x))
| fold_type_constrs _ _ x = x
-(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
+(* Type constructors used to instantiate overloaded constants are the only ones
+ needed. *)
fun add_type_constrs_in_term thy =
let
fun add (Const (@{const_name Meson.skolem}, _) $ _) = I
@@ -1422,6 +1416,11 @@
| add (Const (x as (s, _))) =
if String.isPrefix skolem_const_prefix s then I
else x |> Sign.const_typargs thy |> fold (fold_type_constrs set_insert)
+ | add (Free (s, T)) =
+ if String.isPrefix lambda_lifted_prefix s then
+ T |> fold_type_constrs set_insert
+ else
+ I
| add (Abs (_, _, u)) = add u
| add _ = I
in add end
@@ -1733,7 +1732,7 @@
1 upto num_args |> map (`I o make_bound_var o string_of_int)
val bounds =
bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, []))
- val sym_needs_arg_types = exists (curry (op =) dummyT) T_args)
+ val sym_needs_arg_types = exists (curry (op =) dummyT) T_args
fun should_keep_arg_type T =
sym_needs_arg_types orelse
not (should_predicate_on_type ctxt nonmono_Ts type_enc (K false) T)