store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
authorblanchet
Fri Apr 16 14:48:34 2010 +0200 (2010-04-16)
changeset 3616927b1cc58715e
parent 36168 0a6ed065683d
child 36170 0cdb76723c88
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
src/HOL/Tools/ATP_Manager/atp_wrapper.ML
src/HOL/Tools/Sledgehammer/metis_tactics.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Thu Apr 15 13:57:17 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Fri Apr 16 14:48:34 2010 +0200
     1.3 @@ -65,8 +65,8 @@
     1.4            else SOME "Ill-formed ATP output"
     1.5    | (failure :: _) => SOME failure
     1.6  
     1.7 -fun generic_prover overlord get_facts prepare write cmd args failure_strs
     1.8 -        produce_answer name ({full_types, ...} : params)
     1.9 +fun generic_prover overlord get_facts prepare write_file cmd args failure_strs
    1.10 +        produce_answer name ({debug, full_types, ...} : params)
    1.11          ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
    1.12           : problem) =
    1.13    let
    1.14 @@ -100,7 +100,7 @@
    1.15          if destdir' = "" then File.tmp_path probfile
    1.16          else if File.exists (Path.explode destdir')
    1.17          then Path.append  (Path.explode destdir') probfile
    1.18 -        else error ("No such directory: " ^ destdir')
    1.19 +        else error ("No such directory: " ^ destdir' ^ ".")
    1.20        end;
    1.21  
    1.22      (* write out problem file and call prover *)
    1.23 @@ -127,7 +127,7 @@
    1.24        if Config.get ctxt measure_runtime then split_time s else (s, 0)
    1.25      fun run_on probfile =
    1.26        if File.exists cmd then
    1.27 -        write full_types probfile clauses
    1.28 +        write_file debug full_types probfile clauses
    1.29          |> pair (apfst split_time' (bash_output (cmd_line probfile)))
    1.30        else error ("Bad executable: " ^ Path.implode cmd ^ ".");
    1.31  
     2.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Apr 15 13:57:17 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Apr 16 14:48:34 2010 +0200
     2.3 @@ -69,10 +69,10 @@
     2.4  
     2.5  fun metis_lit b c args = (b, (c, args));
     2.6  
     2.7 -fun hol_type_to_fol (TyVar x) = Metis.Term.Var x
     2.8 -  | hol_type_to_fol (TyFree x) = Metis.Term.Fn (x, [])
     2.9 -  | hol_type_to_fol (TyConstr (tc, tps)) =
    2.10 -    Metis.Term.Fn (tc, map hol_type_to_fol tps);
    2.11 +fun hol_type_to_fol (TyVar (x, _)) = Metis.Term.Var x
    2.12 +  | hol_type_to_fol (TyFree (s, _)) = Metis.Term.Fn (s, [])
    2.13 +  | hol_type_to_fol (TyConstr ((s, _), tps)) =
    2.14 +    Metis.Term.Fn (s, map hol_type_to_fol tps);
    2.15  
    2.16  (*These two functions insert type literals before the real literals. That is the
    2.17    opposite order from TPTP linkup, but maybe OK.*)
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Thu Apr 15 13:57:17 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Fri Apr 16 14:48:34 2010 +0200
     3.3 @@ -30,12 +30,17 @@
     3.4    val make_fixed_const : bool -> string -> string
     3.5    val make_fixed_type_const : bool -> string -> string
     3.6    val make_type_class : string -> string
     3.7 +  type name = string * string
     3.8 +  type name_pool = string Symtab.table * string Symtab.table
     3.9 +  val empty_name_pool : bool -> name_pool option
    3.10 +  val pool_map : ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
    3.11 +  val nice_name : name -> name_pool option -> string * name_pool option
    3.12    datatype kind = Axiom | Conjecture
    3.13    type axiom_name = string
    3.14    datatype fol_type =
    3.15 -    TyVar of string |
    3.16 -    TyFree of string |
    3.17 -    TyConstr of string * fol_type list
    3.18 +    TyVar of name |
    3.19 +    TyFree of name |
    3.20 +    TyConstr of name * fol_type list
    3.21    val string_of_fol_type : fol_type -> string
    3.22    datatype type_literal = LTVar of string * string | LTFree of string * string
    3.23    exception CLAUSE of string * term
    3.24 @@ -207,7 +212,65 @@
    3.25  fun make_type_class clas = class_prefix ^ ascii_of clas;
    3.26  
    3.27  
    3.28 -(***** definitions and functions for FOL clauses, for conversion to TPTP or DFG format. *****)
    3.29 +(**** name pool ****)
    3.30 + 
    3.31 +type name = string * string
    3.32 +type name_pool = string Symtab.table * string Symtab.table
    3.33 +
    3.34 +fun empty_name_pool debug = if debug then SOME (`I Symtab.empty) else NONE
    3.35 +
    3.36 +fun pool_map f xs =
    3.37 +  fold (fn x => fn (ys, pool) => f x pool |>> (fn y => y :: ys)) xs o pair []
    3.38 +
    3.39 +fun add_nice_name full_name nice_prefix j the_pool =
    3.40 +  let
    3.41 +    val nice_name = nice_prefix ^ (if j = 0 then "" else "_" ^ Int.toString j)
    3.42 +  in
    3.43 +    case Symtab.lookup (snd the_pool) nice_name of
    3.44 +      SOME full_name' =>
    3.45 +      if full_name = full_name' then (nice_name, the_pool)
    3.46 +      else add_nice_name full_name nice_prefix (j + 1) the_pool
    3.47 +    | NONE =>
    3.48 +      (nice_name, (Symtab.update_new (full_name, nice_name) (fst the_pool),
    3.49 +                   Symtab.update_new (nice_name, full_name) (snd the_pool)))
    3.50 +  end
    3.51 +
    3.52 +fun translate_first_char f s =
    3.53 +  String.str (f (String.sub (s, 0))) ^ String.extract (s, 1, NONE)
    3.54 +
    3.55 +fun clean_short_name full_name s =
    3.56 +  let
    3.57 +    val s = s |> Long_Name.base_name
    3.58 +              |> fold remove_all ["\<^sub>", "\<^bsub>", "\<^esub>", "\<^isub>"]
    3.59 +    val s' = s |> explode |> rev |> dropwhile (curry (op =) "'")
    3.60 +    val s' =
    3.61 +      (s' |> rev
    3.62 +          |> implode
    3.63 +          |> String.translate
    3.64 +                 (fn c => if Char.isAlphaNum c then String.str c else ""))
    3.65 +      ^ replicate_string (String.size s - length s') "_"
    3.66 +    val s' =
    3.67 +      if s' = "" orelse not (Char.isAlpha (String.sub (s', 0))) then "X" ^ s'
    3.68 +      else s'
    3.69 +    val s' = if s' = "op" then full_name else s'
    3.70 +  in
    3.71 +    case (Char.isLower (String.sub (full_name, 0)),
    3.72 +          Char.isLower (String.sub (s', 0))) of
    3.73 +      (true, false) => translate_first_char Char.toLower s'
    3.74 +    | (false, true) => translate_first_char Char.toUpper s'
    3.75 +    | _ => s'
    3.76 +  end
    3.77 +
    3.78 +fun nice_name (full_name, _) NONE = (full_name, NONE)
    3.79 +  | nice_name (full_name, desired_name) (SOME the_pool) =
    3.80 +    case Symtab.lookup (fst the_pool) full_name of
    3.81 +      SOME nice_name => (nice_name, SOME the_pool)
    3.82 +    | NONE => add_nice_name full_name (clean_short_name full_name desired_name)
    3.83 +                            0 the_pool
    3.84 +              |> apsnd SOME
    3.85 +
    3.86 +(**** Definitions and functions for FOL clauses, for conversion to TPTP or DFG
    3.87 +      format ****)
    3.88  
    3.89  datatype kind = Axiom | Conjecture;
    3.90  
    3.91 @@ -216,13 +279,13 @@
    3.92  (**** Isabelle FOL clauses ****)
    3.93  
    3.94  datatype fol_type =
    3.95 -  TyVar of string |
    3.96 -  TyFree of string |
    3.97 -  TyConstr of string * fol_type list
    3.98 +  TyVar of name |
    3.99 +  TyFree of name |
   3.100 +  TyConstr of name * fol_type list
   3.101  
   3.102 -fun string_of_fol_type (TyVar s) = s
   3.103 -  | string_of_fol_type (TyFree s) = s
   3.104 -  | string_of_fol_type (TyConstr (tcon, tps)) =
   3.105 +fun string_of_fol_type (TyVar (s, _)) = s
   3.106 +  | string_of_fol_type (TyFree (s, _)) = s
   3.107 +  | string_of_fol_type (TyConstr ((tcon, _), tps)) =
   3.108        tcon ^ (paren_pack (map string_of_fol_type tps));
   3.109  
   3.110  (*First string is the type class; the second is a TVar or TFfree*)
   3.111 @@ -230,19 +293,9 @@
   3.112  
   3.113  exception CLAUSE of string * term;
   3.114  
   3.115 -fun atomic_type (TFree (a,_)) = TyFree(make_fixed_type_var a)
   3.116 -  | atomic_type (TVar (v,_))  = TyVar(make_schematic_type_var v);
   3.117 -
   3.118 -(*Flatten a type to a fol_type while accumulating sort constraints on the TFrees and
   3.119 -  TVars it contains.*)
   3.120 -fun type_of dfg (Type (a, Ts)) =
   3.121 -      let val (folTyps, ts) = types_of dfg Ts
   3.122 -          val t = make_fixed_type_const dfg a
   3.123 -      in (TyConstr (t, folTyps), ts) end
   3.124 -  | type_of dfg T = (atomic_type T, [T])
   3.125 -and types_of dfg Ts =
   3.126 -      let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
   3.127 -      in (folTyps, union_all ts) end;
   3.128 +fun atomic_type (TFree (a,_)) = TyFree (`make_fixed_type_var a)
   3.129 +  | atomic_type (TVar (x, _)) =
   3.130 +    TyVar (make_schematic_type_var x, string_of_indexname x)
   3.131  
   3.132  (*Make literals for sorted type variables*)
   3.133  fun sorts_on_typs_aux (_, [])   = []
   3.134 @@ -402,9 +455,9 @@
   3.135  (*** Find occurrences of functions in clauses ***)
   3.136  
   3.137  fun add_foltype_funcs (TyVar _, funcs) = funcs
   3.138 -  | add_foltype_funcs (TyFree a, funcs) = Symtab.update (a,0) funcs
   3.139 -  | add_foltype_funcs (TyConstr (a, tys), funcs) =
   3.140 -      List.foldl add_foltype_funcs (Symtab.update (a, length tys) funcs) tys;
   3.141 +  | add_foltype_funcs (TyFree (s, _), funcs) = Symtab.update (s, 0) funcs
   3.142 +  | add_foltype_funcs (TyConstr ((s, _), tys), funcs) =
   3.143 +      List.foldl add_foltype_funcs (Symtab.update (s, length tys) funcs) tys;
   3.144  
   3.145  (*TFrees are recorded as constants*)
   3.146  fun add_type_sort_funcs (TVar _, funcs) = funcs
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Thu Apr 15 13:57:17 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Fri Apr 16 14:48:34 2010 +0200
     4.3 @@ -33,11 +33,11 @@
     4.4    val get_helper_clauses : bool -> theory -> bool ->
     4.5         hol_clause list * (thm * (axiom_name * hol_clause_id)) list * string list ->
     4.6         hol_clause list
     4.7 -  val write_tptp_file : bool -> Path.T ->
     4.8 +  val write_tptp_file : bool -> bool -> Path.T ->
     4.9      hol_clause list * hol_clause list * hol_clause list * hol_clause list *
    4.10      classrel_clause list * arity_clause list ->
    4.11      int * int
    4.12 -  val write_dfg_file : bool -> Path.T ->
    4.13 +  val write_dfg_file : bool -> bool -> Path.T ->
    4.14      hol_clause list * hol_clause list * hol_clause list * hol_clause list *
    4.15      classrel_clause list * arity_clause list -> int * int
    4.16  end
    4.17 @@ -102,19 +102,22 @@
    4.18  fun isTaut (HOLClause {literals,...}) = exists isTrue literals;
    4.19  
    4.20  fun type_of dfg (Type (a, Ts)) =
    4.21 -      let val (folTypes,ts) = types_of dfg Ts
    4.22 -      in  (TyConstr (make_fixed_type_const dfg a, folTypes), ts)  end
    4.23 -  | type_of _ (tp as TFree (a, _)) = (TyFree (make_fixed_type_var a), [tp])
    4.24 -  | type_of _ (tp as TVar (v, _)) = (TyVar (make_schematic_type_var v), [tp])
    4.25 +    let val (folTypes,ts) = types_of dfg Ts in
    4.26 +      (TyConstr (`(make_fixed_type_const dfg) a, folTypes), ts)
    4.27 +    end
    4.28 +  | type_of _ (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp])
    4.29 +  | type_of _ (tp as TVar (x, _)) =
    4.30 +    (TyVar (make_schematic_type_var x, string_of_indexname x), [tp])
    4.31  and types_of dfg Ts =
    4.32        let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
    4.33        in  (folTyps, union_all ts)  end;
    4.34  
    4.35  (* same as above, but no gathering of sort information *)
    4.36  fun simp_type_of dfg (Type (a, Ts)) =
    4.37 -      TyConstr (make_fixed_type_const dfg a, map (simp_type_of dfg) Ts)
    4.38 -  | simp_type_of _ (TFree (a, _)) = TyFree (make_fixed_type_var a)
    4.39 -  | simp_type_of _ (TVar (v, _)) = TyVar (make_schematic_type_var v);
    4.40 +      TyConstr (`(make_fixed_type_const dfg) a, map (simp_type_of dfg) Ts)
    4.41 +  | simp_type_of _ (TFree (a, _)) = TyFree (`make_fixed_type_var a)
    4.42 +  | simp_type_of _ (TVar (x, _)) =
    4.43 +    TyVar (make_schematic_type_var x, string_of_indexname x);
    4.44  
    4.45  
    4.46  fun const_type_of dfg thy (c,t) =
    4.47 @@ -193,7 +196,7 @@
    4.48  (**********************************************************************)
    4.49  
    4.50  (*Result of a function type; no need to check that the argument type matches.*)
    4.51 -fun result_type (TyConstr ("tc_fun", [_, tp2])) = tp2
    4.52 +fun result_type (TyConstr (("tc_fun", _), [_, tp2])) = tp2
    4.53    | result_type _ = raise Fail "Non-function type"
    4.54  
    4.55  fun type_of_combterm (CombConst (_, tp, _)) = tp
    4.56 @@ -452,7 +455,7 @@
    4.57  
    4.58  (* TPTP format *)
    4.59  
    4.60 -fun write_tptp_file full_types file clauses =
    4.61 +fun write_tptp_file debug full_types file clauses =
    4.62    let
    4.63      fun section _ [] = []
    4.64        | section name ss = "\n% " ^ name ^ plural_s (length ss) ^ "\n" :: ss
    4.65 @@ -480,7 +483,7 @@
    4.66  
    4.67  (* DFG format *)
    4.68  
    4.69 -fun write_dfg_file full_types file clauses =
    4.70 +fun write_dfg_file debug full_types file clauses =
    4.71    let
    4.72      val (conjectures, axclauses, _, helper_clauses,
    4.73        classrel_clauses, arity_clauses) = clauses
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Apr 15 13:57:17 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Apr 16 14:48:34 2010 +0200
     5.3 @@ -8,6 +8,8 @@
     5.4  sig
     5.5    val plural_s : int -> string
     5.6    val serial_commas : string -> string list -> string list
     5.7 +  val replace_all : string -> string -> string -> string
     5.8 +  val remove_all : string -> string -> string
     5.9    val parse_bool_option : bool -> string -> string -> bool option
    5.10    val parse_time_option : string -> string -> Time.time option
    5.11    val hashw : word * word -> word
    5.12 @@ -26,6 +28,18 @@
    5.13    | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
    5.14    | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
    5.15  
    5.16 +fun replace_all bef aft =
    5.17 +  let
    5.18 +    fun aux seen "" = String.implode (rev seen)
    5.19 +      | aux seen s =
    5.20 +      if String.isPrefix bef s then
    5.21 +          aux seen "" ^ aft ^ aux [] (unprefix bef s)
    5.22 +        else
    5.23 +          aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))
    5.24 +  in aux [] end
    5.25 +
    5.26 +fun remove_all bef = replace_all bef ""
    5.27 +
    5.28  fun parse_bool_option option name s =
    5.29    (case s of
    5.30       "smart" => if option then NONE else raise Option