# HG changeset patch
# User blanchet
# Date 1321391619 -3600
# Node ID 624872fc47bfdfa46a5019da9356ed43ca32bb76
# Parent  b216dc1b36308cee7a909905776a5ac498e4dd8d
use consts, not frees, for lambda-lifting

diff -r b216dc1b3630 -r 624872fc47bf src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Nov 15 22:13:39 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Nov 15 22:13:39 2011 +0100
@@ -143,8 +143,12 @@
 val simple_type_prefix = "s_"
 val class_prefix = "cl_"
 
-val lambda_lifted_prefix = "lambda"
-val lambda_lifted_poly_prefix = lambda_lifted_prefix ^ "_poly"
+(* Freshness almost guaranteed! *)
+val atp_weak_prefix = "ATP:"
+
+val lambda_lifted_prefix = atp_weak_prefix ^ "Lam"
+val lambda_lifted_mono_prefix = lambda_lifted_prefix ^ "m"
+val lambda_lifted_poly_prefix = lambda_lifted_prefix ^ "p"
 
 val skolem_const_prefix = "ATP" ^ Long_Name.separator ^ "Sko"
 val old_skolem_const_prefix = skolem_const_prefix ^ "o"
@@ -175,9 +179,6 @@
 val prefixed_app_op_name = const_prefix ^ app_op_name
 val prefixed_type_tag_name = const_prefix ^ type_tag_name
 
-(* Freshness almost guaranteed! *)
-val atp_weak_prefix = "ATP:"
-
 (*Escaping of special characters.
   Alphanumeric characters are left unchanged.
   The character _ goes to __
@@ -472,18 +473,37 @@
 
 fun atomic_types_of T = fold_atyps (insert (op =)) T []
 
+val tvar_a_str = "'a"
+val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)
+val tvar_a_name = (make_schematic_type_var (tvar_a_str, 0), tvar_a_str)
+val itself_name = `make_fixed_type_const @{type_name itself}
+val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
+val tvar_a_atype = AType (tvar_a_name, [])
+val a_itself_atype = AType (itself_name, [tvar_a_atype])
+
 fun new_skolem_const_name s num_T_args =
   [new_skolem_const_prefix, s, string_of_int num_T_args]
   |> space_implode Long_Name.separator
 
 fun robust_const_type thy s =
-  if s = app_op_name then Logic.varifyT_global @{typ "('a => 'b) => 'a => 'b"}
-  else s |> Sign.the_const_type thy
+  if s = app_op_name then
+    Logic.varifyT_global @{typ "('a => 'b) => 'a => 'b"}
+  else if String.isPrefix lambda_lifted_poly_prefix s then
+    Logic.varifyT_global @{typ "'a => 'b"}
+  else
+    (* Old Skolems throw a "TYPE" exception here, which will be caught. *)
+    s |> Sign.the_const_type thy
 
 (* This function only makes sense if "T" is as general as possible. *)
 fun robust_const_typargs thy (s, T) =
-  (s, T) |> Sign.const_typargs thy
-  handle TYPE _ => [] |> Term.add_tvarsT T |> rev |> map TVar
+  if s = app_op_name then
+    let val (T1, T2) = T |> domain_type |> dest_funT in [T1, T2] end
+  else if String.isPrefix old_skolem_const_prefix s then
+    [] |> Term.add_tvarsT T |> rev |> map TVar
+  else if String.isPrefix lambda_lifted_poly_prefix s then
+    let val (T1, T2) = T |> dest_funT in [T1, T2] end
+  else
+    (s, T) |> Sign.const_typargs thy
 
 (* Converts an Isabelle/HOL term (with combinators) into an intermediate term.
    Also accumulates sort infomation. *)
@@ -497,9 +517,7 @@
              robust_const_typargs thy (c, T)),
      atomic_types_of T)
   | iterm_from_term _ _ _ (Free (s, T)) =
-    (IConst (`make_fixed_var s, T,
-             if String.isPrefix lambda_lifted_poly_prefix s then [T] else []),
-     atomic_types_of T)
+    (IConst (`make_fixed_var s, T, []), atomic_types_of T)
   | iterm_from_term _ format _ (Var (v as (s, _), T)) =
     (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
        let
@@ -654,15 +672,22 @@
     (if is_type_enc_fairly_sound type_enc then Tags else Guards) stuff
   | adjust_type_enc _ type_enc = type_enc
 
+fun constify_lifted (t $ u) = constify_lifted t $ constify_lifted u
+  | constify_lifted (Abs (s, T, t)) = Abs (s, T, constify_lifted t)
+  | constify_lifted (Free (x as (s, _))) =
+    (if String.isPrefix lambda_lifted_prefix s then Const else Free) x
+  | constify_lifted t = t
+
 fun lift_lambdas ctxt type_enc =
   map (close_form o Envir.eta_contract) #> rpair ctxt
   #-> Lambda_Lifting.lift_lambdas
           (SOME (if polymorphism_of_type_enc type_enc = Polymorphic then
                    lambda_lifted_poly_prefix
                  else
-                   lambda_lifted_prefix))
+                   lambda_lifted_mono_prefix))
           Lambda_Lifting.is_quantifier
   #> fst
+  #> pairself (map constify_lifted)
 
 fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
     intentionalize_def t
@@ -741,14 +766,6 @@
 fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
   | add_sorts_on_tvar _ = I
 
-val tvar_a_str = "'a"
-val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)
-val tvar_a_name = (make_schematic_type_var (tvar_a_str, 0), tvar_a_str)
-val itself_name = `make_fixed_type_const @{type_name itself}
-val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
-val tvar_a_atype = AType (tvar_a_name, [])
-val a_itself_atype = AType (itself_name, [tvar_a_atype])
-
 fun type_class_formula type_enc class arg =
   AAtom (ATerm (class, arg ::
       (case type_enc of
@@ -1121,8 +1138,8 @@
     do_cheaply_conceal_lambdas Ts t1
     $ do_cheaply_conceal_lambdas Ts t2
   | do_cheaply_conceal_lambdas Ts (Abs (_, T, t)) =
-    Free (lambda_lifted_poly_prefix ^ serial_string (),
-          T --> fastype_of1 (T :: Ts, t))
+    Const (lambda_lifted_poly_prefix ^ serial_string (),
+           T --> fastype_of1 (T :: Ts, t))
   | do_cheaply_conceal_lambdas _ t = t
 
 fun do_introduce_combinators ctxt Ts t =
@@ -1633,11 +1650,6 @@
       | add (t $ u) = add t #> add u
       | add (Const x) =
         x |> robust_const_typargs thy |> fold (fold_type_constrs set_insert)
-      | add (Free (s, T)) =
-        if String.isPrefix lambda_lifted_poly_prefix s then
-          T |> fold_type_constrs set_insert
-        else
-          I
       | add (Abs (_, _, u)) = add u
       | add _ = I
   in add end
@@ -1651,7 +1663,7 @@
       | extr bs (Const (@{const_name All}, _) $ Abs (s, T, t)) =
         extr ((s, T) :: bs) t
       | extr bs (Const (@{const_name HOL.eq}, _) $ t $ u) =
-        (t |> head_of |> dest_Free |> fst,
+        (t |> head_of |> dest_Const |> fst,
          fold_rev (fn (s, T) => fn u => Abs (s, T, u)) bs u)
       | extr _ _ = raise Fail "malformed lifted lambda"
   in extr [] end
@@ -2109,14 +2121,7 @@
           val s' = s' |> invert_const
           val T = s' |> robust_const_type thy
         in (T, robust_const_typargs thy (s', T)) end
-      | NONE =>
-        case strip_prefix_and_unascii fixed_var_prefix s of
-          SOME s' =>
-          if String.isPrefix lambda_lifted_poly_prefix s' then
-            (tvar_a, [tvar_a])
-          else
-            raise Fail "unexpected type arguments to free variable"
-        | NONE => raise Fail "unexpected type arguments"
+      | NONE => raise Fail "unexpected type arguments"
   in
     Decl (sym_decl_prefix ^ s, (s, s'),
           T |> fused_type ctxt mono (level_of_type_enc type_enc) ary