simplify Skolem handling;
authorblanchet
Fri Sep 17 00:54:56 2010 +0200 (2010-09-17)
changeset 3949940bf0f66b994
parent 39498 e8aef7ea9cbb
child 39500 d91ef7fbc500
simplify Skolem handling;
things are much easier now that Sledgehammer doesn't skolemize, only Metis
src/HOL/Tools/Sledgehammer/metis_translate.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/metis_translate.ML	Fri Sep 17 00:35:19 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/metis_translate.ML	Fri Sep 17 00:54:56 2010 +0200
     1.3 @@ -57,29 +57,23 @@
     1.4    val make_fixed_const : string -> string
     1.5    val make_fixed_type_const : string -> string
     1.6    val make_type_class : string -> string
     1.7 -  val skolem_theory_name: string
     1.8 -  val skolem_prefix: string
     1.9 -  val skolem_infix: string
    1.10 -  val is_skolem_const_name: string -> bool
    1.11    val num_type_args: theory -> string -> int
    1.12    val type_literals_for_types : typ list -> type_literal list
    1.13 -  val make_class_rel_clauses: theory -> class list -> class list -> class_rel_clause list
    1.14 -  val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
    1.15 +  val make_class_rel_clauses :
    1.16 +    theory -> class list -> class list -> class_rel_clause list
    1.17 +  val make_arity_clauses :
    1.18 +    theory -> string list -> class list -> class list * arity_clause list
    1.19    val combtyp_of : combterm -> combtyp
    1.20    val strip_combterm_comb : combterm -> combterm * combterm list
    1.21    val combterm_from_term :
    1.22      theory -> (string * typ) list -> term -> combterm * typ list
    1.23 -  val literals_of_term : theory -> term -> fol_literal list * typ list
    1.24 -  val conceal_skolem_terms :
    1.25 -    int -> (string * term) list -> term -> (string * term) list * term
    1.26    val reveal_skolem_terms : (string * term) list -> term -> term
    1.27    val tfree_classes_of_terms : term list -> string list
    1.28    val tvar_classes_of_terms : term list -> string list
    1.29    val type_consts_of_terms : theory -> term list -> string list
    1.30    val string_of_mode : mode -> string
    1.31    val build_logic_map :
    1.32 -    mode -> Proof.context -> bool -> thm list -> thm list
    1.33 -    -> mode * logic_map
    1.34 +    mode -> Proof.context -> bool -> thm list -> thm list -> mode * logic_map
    1.35  end
    1.36  
    1.37  structure Metis_Translate : METIS_TRANSLATE =
    1.38 @@ -204,24 +198,14 @@
    1.39  
    1.40  fun make_type_class clas = class_prefix ^ ascii_of clas;
    1.41  
    1.42 -val skolem_theory_name = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
    1.43 -val skolem_prefix = "sko_"
    1.44 -val skolem_infix = "$"
    1.45 -
    1.46 -(* Hack: Could return false positives (e.g., a user happens to declare a
    1.47 -   constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
    1.48 -val is_skolem_const_name =
    1.49 -  Long_Name.base_name
    1.50 -  #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
    1.51 +val skolem_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
    1.52  
    1.53  (* The number of type arguments of a constant, zero if it's monomorphic. For
    1.54     (instances of) Skolem pseudoconstants, this information is encoded in the
    1.55     constant name. *)
    1.56  fun num_type_args thy s =
    1.57 -  if String.isPrefix skolem_theory_name s then
    1.58 -    s |> unprefix skolem_theory_name
    1.59 -      |> space_explode skolem_infix |> hd
    1.60 -      |> space_explode "_" |> List.last |> Int.fromString |> the
    1.61 +  if String.isPrefix skolem_prefix s then
    1.62 +    s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
    1.63    else
    1.64      (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
    1.65  
    1.66 @@ -410,7 +394,7 @@
    1.67        let
    1.68          val (tp, ts) = combtype_of T
    1.69          val tvar_list =
    1.70 -          (if String.isPrefix skolem_theory_name c then
    1.71 +          (if String.isPrefix skolem_prefix c then
    1.72               [] |> Term.add_tvarsT T |> map TVar
    1.73             else
    1.74               (c, T) |> Sign.const_typargs thy)
    1.75 @@ -448,8 +432,8 @@
    1.76  val literals_of_term = literals_of_term1 ([], [])
    1.77  
    1.78  fun skolem_name i j num_T_args =
    1.79 -  skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^
    1.80 -  skolem_infix ^ "g"
    1.81 +  skolem_prefix ^ Long_Name.separator ^
    1.82 +  (space_implode Long_Name.separator (map Int.toString [i, j, num_T_args]))
    1.83  
    1.84  fun conceal_skolem_terms i skolems t =
    1.85    if exists_Const (curry (op =) @{const_name skolem} o fst) t then
    1.86 @@ -464,9 +448,8 @@
    1.87                  s :: _ => (skolems, s)
    1.88                | [] =>
    1.89                  let
    1.90 -                  val s = skolem_theory_name ^ "." ^
    1.91 -                          skolem_name i (length skolems)
    1.92 -                                        (length (Term.add_tvarsT T []))
    1.93 +                  val s = skolem_name i (length skolems)
    1.94 +                                      (length (Term.add_tvarsT T []))
    1.95                  in ((s, t) :: skolems, s) end
    1.96            in (skolems, Const (s, T)) end
    1.97          | aux skolems (t1 $ t2) =
    1.98 @@ -485,7 +468,7 @@
    1.99  
   1.100  fun reveal_skolem_terms skolems =
   1.101    map_aterms (fn t as Const (s, _) =>
   1.102 -                 if String.isPrefix skolem_theory_name s then
   1.103 +                 if String.isPrefix skolem_prefix s then
   1.104                     AList.lookup (op =) skolems s |> the
   1.105                     |> map_types Type_Infer.paramify_vars
   1.106                   else