# HG changeset patch # User blanchet # Date 1311115062 -7200 # Node ID 073ab5379842417e522c42913e167f84f3137f94 # Parent 14d34bd434b8cdba93cdd4f6bd8a4fdfb65203c8 pass type arguments to lambda-lifted Frees, to account for polymorphism diff -r 14d34bd434b8 -r 073ab5379842 src/HOL/Tools/ATP/atp_reconstruct.ML --- 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) diff -r 14d34bd434b8 -r 073ab5379842 src/HOL/Tools/ATP/atp_translate.ML --- 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)