src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
changeset 36169 27b1cc58715e
parent 36168 0a6ed065683d
child 36170 0cdb76723c88
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Thu Apr 15 13:57:17 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Fri Apr 16 14:48:34 2010 +0200
     1.3 @@ -30,12 +30,17 @@
     1.4    val make_fixed_const : bool -> string -> string
     1.5    val make_fixed_type_const : bool -> string -> string
     1.6    val make_type_class : string -> string
     1.7 +  type name = string * string
     1.8 +  type name_pool = string Symtab.table * string Symtab.table
     1.9 +  val empty_name_pool : bool -> name_pool option
    1.10 +  val pool_map : ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
    1.11 +  val nice_name : name -> name_pool option -> string * name_pool option
    1.12    datatype kind = Axiom | Conjecture
    1.13    type axiom_name = string
    1.14    datatype fol_type =
    1.15 -    TyVar of string |
    1.16 -    TyFree of string |
    1.17 -    TyConstr of string * fol_type list
    1.18 +    TyVar of name |
    1.19 +    TyFree of name |
    1.20 +    TyConstr of name * fol_type list
    1.21    val string_of_fol_type : fol_type -> string
    1.22    datatype type_literal = LTVar of string * string | LTFree of string * string
    1.23    exception CLAUSE of string * term
    1.24 @@ -207,7 +212,65 @@
    1.25  fun make_type_class clas = class_prefix ^ ascii_of clas;
    1.26  
    1.27  
    1.28 -(***** definitions and functions for FOL clauses, for conversion to TPTP or DFG format. *****)
    1.29 +(**** name pool ****)
    1.30 + 
    1.31 +type name = string * string
    1.32 +type name_pool = string Symtab.table * string Symtab.table
    1.33 +
    1.34 +fun empty_name_pool debug = if debug then SOME (`I Symtab.empty) else NONE
    1.35 +
    1.36 +fun pool_map f xs =
    1.37 +  fold (fn x => fn (ys, pool) => f x pool |>> (fn y => y :: ys)) xs o pair []
    1.38 +
    1.39 +fun add_nice_name full_name nice_prefix j the_pool =
    1.40 +  let
    1.41 +    val nice_name = nice_prefix ^ (if j = 0 then "" else "_" ^ Int.toString j)
    1.42 +  in
    1.43 +    case Symtab.lookup (snd the_pool) nice_name of
    1.44 +      SOME full_name' =>
    1.45 +      if full_name = full_name' then (nice_name, the_pool)
    1.46 +      else add_nice_name full_name nice_prefix (j + 1) the_pool
    1.47 +    | NONE =>
    1.48 +      (nice_name, (Symtab.update_new (full_name, nice_name) (fst the_pool),
    1.49 +                   Symtab.update_new (nice_name, full_name) (snd the_pool)))
    1.50 +  end
    1.51 +
    1.52 +fun translate_first_char f s =
    1.53 +  String.str (f (String.sub (s, 0))) ^ String.extract (s, 1, NONE)
    1.54 +
    1.55 +fun clean_short_name full_name s =
    1.56 +  let
    1.57 +    val s = s |> Long_Name.base_name
    1.58 +              |> fold remove_all ["\<^sub>", "\<^bsub>", "\<^esub>", "\<^isub>"]
    1.59 +    val s' = s |> explode |> rev |> dropwhile (curry (op =) "'")
    1.60 +    val s' =
    1.61 +      (s' |> rev
    1.62 +          |> implode
    1.63 +          |> String.translate
    1.64 +                 (fn c => if Char.isAlphaNum c then String.str c else ""))
    1.65 +      ^ replicate_string (String.size s - length s') "_"
    1.66 +    val s' =
    1.67 +      if s' = "" orelse not (Char.isAlpha (String.sub (s', 0))) then "X" ^ s'
    1.68 +      else s'
    1.69 +    val s' = if s' = "op" then full_name else s'
    1.70 +  in
    1.71 +    case (Char.isLower (String.sub (full_name, 0)),
    1.72 +          Char.isLower (String.sub (s', 0))) of
    1.73 +      (true, false) => translate_first_char Char.toLower s'
    1.74 +    | (false, true) => translate_first_char Char.toUpper s'
    1.75 +    | _ => s'
    1.76 +  end
    1.77 +
    1.78 +fun nice_name (full_name, _) NONE = (full_name, NONE)
    1.79 +  | nice_name (full_name, desired_name) (SOME the_pool) =
    1.80 +    case Symtab.lookup (fst the_pool) full_name of
    1.81 +      SOME nice_name => (nice_name, SOME the_pool)
    1.82 +    | NONE => add_nice_name full_name (clean_short_name full_name desired_name)
    1.83 +                            0 the_pool
    1.84 +              |> apsnd SOME
    1.85 +
    1.86 +(**** Definitions and functions for FOL clauses, for conversion to TPTP or DFG
    1.87 +      format ****)
    1.88  
    1.89  datatype kind = Axiom | Conjecture;
    1.90  
    1.91 @@ -216,13 +279,13 @@
    1.92  (**** Isabelle FOL clauses ****)
    1.93  
    1.94  datatype fol_type =
    1.95 -  TyVar of string |
    1.96 -  TyFree of string |
    1.97 -  TyConstr of string * fol_type list
    1.98 +  TyVar of name |
    1.99 +  TyFree of name |
   1.100 +  TyConstr of name * fol_type list
   1.101  
   1.102 -fun string_of_fol_type (TyVar s) = s
   1.103 -  | string_of_fol_type (TyFree s) = s
   1.104 -  | string_of_fol_type (TyConstr (tcon, tps)) =
   1.105 +fun string_of_fol_type (TyVar (s, _)) = s
   1.106 +  | string_of_fol_type (TyFree (s, _)) = s
   1.107 +  | string_of_fol_type (TyConstr ((tcon, _), tps)) =
   1.108        tcon ^ (paren_pack (map string_of_fol_type tps));
   1.109  
   1.110  (*First string is the type class; the second is a TVar or TFfree*)
   1.111 @@ -230,19 +293,9 @@
   1.112  
   1.113  exception CLAUSE of string * term;
   1.114  
   1.115 -fun atomic_type (TFree (a,_)) = TyFree(make_fixed_type_var a)
   1.116 -  | atomic_type (TVar (v,_))  = TyVar(make_schematic_type_var v);
   1.117 -
   1.118 -(*Flatten a type to a fol_type while accumulating sort constraints on the TFrees and
   1.119 -  TVars it contains.*)
   1.120 -fun type_of dfg (Type (a, Ts)) =
   1.121 -      let val (folTyps, ts) = types_of dfg Ts
   1.122 -          val t = make_fixed_type_const dfg a
   1.123 -      in (TyConstr (t, folTyps), ts) end
   1.124 -  | type_of dfg T = (atomic_type T, [T])
   1.125 -and types_of dfg Ts =
   1.126 -      let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
   1.127 -      in (folTyps, union_all ts) end;
   1.128 +fun atomic_type (TFree (a,_)) = TyFree (`make_fixed_type_var a)
   1.129 +  | atomic_type (TVar (x, _)) =
   1.130 +    TyVar (make_schematic_type_var x, string_of_indexname x)
   1.131  
   1.132  (*Make literals for sorted type variables*)
   1.133  fun sorts_on_typs_aux (_, [])   = []
   1.134 @@ -402,9 +455,9 @@
   1.135  (*** Find occurrences of functions in clauses ***)
   1.136  
   1.137  fun add_foltype_funcs (TyVar _, funcs) = funcs
   1.138 -  | add_foltype_funcs (TyFree a, funcs) = Symtab.update (a,0) funcs
   1.139 -  | add_foltype_funcs (TyConstr (a, tys), funcs) =
   1.140 -      List.foldl add_foltype_funcs (Symtab.update (a, length tys) funcs) tys;
   1.141 +  | add_foltype_funcs (TyFree (s, _), funcs) = Symtab.update (s, 0) funcs
   1.142 +  | add_foltype_funcs (TyConstr ((s, _), tys), funcs) =
   1.143 +      List.foldl add_foltype_funcs (Symtab.update (s, length tys) funcs) tys;
   1.144  
   1.145  (*TFrees are recorded as constants*)
   1.146  fun add_type_sort_funcs (TVar _, funcs) = funcs