src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
changeset 37498 b426cbdb5a23
parent 37479 f6b1ee5b420b
child 37500 7587b6e63454
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Tue Jun 22 13:17:59 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Tue Jun 22 14:28:22 2010 +0200
     1.3 @@ -28,8 +28,8 @@
     1.4    val make_fixed_var : string -> string
     1.5    val make_schematic_type_var : string * int -> string
     1.6    val make_fixed_type_var : string -> string
     1.7 -  val make_fixed_const : bool -> string -> string
     1.8 -  val make_fixed_type_const : bool -> string -> string
     1.9 +  val make_fixed_const : string -> string
    1.10 +  val make_fixed_type_const : string -> string
    1.11    val make_type_class : string -> string
    1.12    type name = string * string
    1.13    type name_pool = string Symtab.table * string Symtab.table
    1.14 @@ -49,7 +49,6 @@
    1.15      TyLitFree of string * name
    1.16    exception CLAUSE of string * term
    1.17    val type_literals_for_types : typ list -> type_literal list
    1.18 -  val get_tvar_strs: typ list -> string list
    1.19    datatype arLit =
    1.20        TConsLit of class * string * string list
    1.21      | TVarLit of class * string
    1.22 @@ -58,28 +57,7 @@
    1.23    datatype classrel_clause = ClassrelClause of
    1.24     {axiom_name: axiom_name, subclass: class, superclass: class}
    1.25    val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list
    1.26 -  val make_arity_clauses_dfg: bool -> theory -> string list -> class list -> class list * arity_clause list
    1.27    val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
    1.28 -  val add_type_sort_preds: typ -> int Symtab.table -> int Symtab.table
    1.29 -  val add_classrel_clause_preds :
    1.30 -    classrel_clause -> int Symtab.table -> int Symtab.table
    1.31 -  val class_of_arityLit: arLit -> class
    1.32 -  val add_arity_clause_preds: arity_clause -> int Symtab.table -> int Symtab.table
    1.33 -  val add_fol_type_funcs: fol_type -> int Symtab.table -> int Symtab.table
    1.34 -  val add_arity_clause_funcs:
    1.35 -    arity_clause -> int Symtab.table -> int Symtab.table
    1.36 -  val init_functab: int Symtab.table
    1.37 -  val dfg_sign: bool -> string -> string
    1.38 -  val dfg_of_type_literal: bool -> type_literal -> string
    1.39 -  val gen_dfg_cls: int * string * kind * string list * string list * string list -> string
    1.40 -  val string_of_preds: (string * Int.int) list -> string
    1.41 -  val string_of_funcs: (string * int) list -> string
    1.42 -  val string_of_symbols: string -> string -> string
    1.43 -  val string_of_start: string -> string
    1.44 -  val string_of_descrip : string -> string
    1.45 -  val dfg_tfree_clause : string -> string
    1.46 -  val dfg_classrel_clause: classrel_clause -> string
    1.47 -  val dfg_arity_clause: arity_clause -> string
    1.48    val tptp_sign: bool -> string -> string
    1.49    val tptp_of_type_literal :
    1.50      bool -> type_literal -> name_pool option -> string * name_pool option
    1.51 @@ -196,31 +174,21 @@
    1.52        tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
    1.53  fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
    1.54  
    1.55 -val max_dfg_symbol_length = 63
    1.56 -
    1.57 -(* HACK because SPASS 3.0 truncates identifiers to 63 characters. *)
    1.58 -fun controlled_length dfg s =
    1.59 -  if dfg andalso size s > max_dfg_symbol_length then
    1.60 -    String.extract (s, 0, SOME (max_dfg_symbol_length div 2 - 1)) ^ "__" ^
    1.61 -    String.extract (s, size s - max_dfg_symbol_length div 2 + 1, NONE)
    1.62 -  else
    1.63 -    s
    1.64 +fun lookup_const c =
    1.65 +  case Symtab.lookup const_trans_table c of
    1.66 +    SOME c' => c'
    1.67 +  | NONE => ascii_of c
    1.68  
    1.69 -fun lookup_const dfg c =
    1.70 -    case Symtab.lookup const_trans_table c of
    1.71 -        SOME c' => c'
    1.72 -      | NONE => controlled_length dfg (ascii_of c);
    1.73 -
    1.74 -fun lookup_type_const dfg c =
    1.75 -    case Symtab.lookup type_const_trans_table c of
    1.76 -        SOME c' => c'
    1.77 -      | NONE => controlled_length dfg (ascii_of c);
    1.78 +fun lookup_type_const c =
    1.79 +  case Symtab.lookup type_const_trans_table c of
    1.80 +    SOME c' => c'
    1.81 +  | NONE => ascii_of c
    1.82  
    1.83  (* "op =" MUST BE "equal" because it's built into ATPs. *)
    1.84 -fun make_fixed_const _ (@{const_name "op ="}) = "equal"
    1.85 -  | make_fixed_const dfg c = const_prefix ^ lookup_const dfg c;
    1.86 +fun make_fixed_const @{const_name "op ="} = "equal"
    1.87 +  | make_fixed_const c = const_prefix ^ lookup_const c
    1.88  
    1.89 -fun make_fixed_type_const dfg c = tconst_prefix ^ lookup_type_const dfg c;
    1.90 +fun make_fixed_type_const c = tconst_prefix ^ lookup_type_const c
    1.91  
    1.92  fun make_type_class clas = class_prefix ^ ascii_of clas;
    1.93  
    1.94 @@ -287,8 +255,7 @@
    1.95                              the_pool
    1.96                |> apsnd SOME
    1.97  
    1.98 -(**** Definitions and functions for FOL clauses, for conversion to TPTP or DFG
    1.99 -      format ****)
   1.100 +(**** Definitions and functions for FOL clauses for TPTP format output ****)
   1.101  
   1.102  datatype kind = Axiom | Conjecture;
   1.103  
   1.104 @@ -329,30 +296,12 @@
   1.105  fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s)
   1.106    | sorts_on_typs (TVar (v,s))  = sorts_on_typs_aux (v,s);
   1.107  
   1.108 -fun pred_of_sort (TyLitVar (s, _)) = (s, 1)
   1.109 -  | pred_of_sort (TyLitFree (s, _)) = (s, 1)
   1.110 -
   1.111  (*Given a list of sorted type variables, return a list of type literals.*)
   1.112  fun type_literals_for_types Ts =
   1.113    fold (union (op =)) (map sorts_on_typs Ts) []
   1.114  
   1.115 -(*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear.
   1.116 -  *  Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a
   1.117 -    in a lemma has the same sort as 'a in the conjecture.
   1.118 -  * Deleting such clauses will lead to problems with locales in other use of local results
   1.119 -    where 'a is fixed. Probably we should delete clauses unless the sorts agree.
   1.120 -  * Currently we include a class constraint in the clause, exactly as with TVars.
   1.121 -*)
   1.122 -
   1.123  (** make axiom and conjecture clauses. **)
   1.124  
   1.125 -fun get_tvar_strs [] = []
   1.126 -  | get_tvar_strs ((TVar (indx,s))::Ts) =
   1.127 -      insert (op =) (make_schematic_type_var indx) (get_tvar_strs Ts)
   1.128 -  | get_tvar_strs((TFree _)::Ts) = get_tvar_strs Ts
   1.129 -
   1.130 -
   1.131 -
   1.132  (**** Isabelle arities ****)
   1.133  
   1.134  datatype arLit = TConsLit of class * string * string list
   1.135 @@ -372,13 +321,13 @@
   1.136    | pack_sort(tvar, cls::srt) =  (cls, tvar) :: pack_sort(tvar, srt);
   1.137  
   1.138  (*Arity of type constructor tcon :: (arg1,...,argN)res*)
   1.139 -fun make_axiom_arity_clause dfg (tcons, axiom_name, (cls,args)) =
   1.140 +fun make_axiom_arity_clause (tcons, axiom_name, (cls,args)) =
   1.141     let val tvars = gen_TVars (length args)
   1.142         val tvars_srts = ListPair.zip (tvars,args)
   1.143     in
   1.144 -      ArityClause {axiom_name = axiom_name, 
   1.145 -                   conclLit = TConsLit (cls, make_fixed_type_const dfg tcons, tvars),
   1.146 -                   premLits = map TVarLit (union_all(map pack_sort tvars_srts))}
   1.147 +     ArityClause {axiom_name = axiom_name, 
   1.148 +                  conclLit = TConsLit (cls, make_fixed_type_const tcons, tvars),
   1.149 +                  premLits = map TVarLit (union_all(map pack_sort tvars_srts))}
   1.150     end;
   1.151  
   1.152  
   1.153 @@ -390,7 +339,7 @@
   1.154                              superclass: class};
   1.155  
   1.156  (*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
   1.157 -fun class_pairs thy [] supers = []
   1.158 +fun class_pairs _ [] _ = []
   1.159    | class_pairs thy subs supers =
   1.160        let
   1.161          val class_less = Sorts.class_less (Sign.classes_of thy)
   1.162 @@ -409,20 +358,20 @@
   1.163  
   1.164  (** Isabelle arities **)
   1.165  
   1.166 -fun arity_clause dfg _ _ (tcons, []) = []
   1.167 -  | arity_clause dfg seen n (tcons, ("HOL.type",_)::ars) =  (*ignore*)
   1.168 -      arity_clause dfg seen n (tcons,ars)
   1.169 -  | arity_clause dfg seen n (tcons, (ar as (class,_)) :: ars) =
   1.170 +fun arity_clause _ _ (_, []) = []
   1.171 +  | arity_clause seen n (tcons, ("HOL.type",_)::ars) =  (*ignore*)
   1.172 +      arity_clause seen n (tcons,ars)
   1.173 +  | arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
   1.174        if member (op =) seen class then (*multiple arities for the same tycon, class pair*)
   1.175 -          make_axiom_arity_clause dfg (tcons, lookup_type_const dfg tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
   1.176 -          arity_clause dfg seen (n+1) (tcons,ars)
   1.177 +          make_axiom_arity_clause (tcons, lookup_type_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
   1.178 +          arity_clause seen (n+1) (tcons,ars)
   1.179        else
   1.180 -          make_axiom_arity_clause dfg (tcons, lookup_type_const dfg tcons ^ "_" ^ class, ar) ::
   1.181 -          arity_clause dfg (class::seen) n (tcons,ars)
   1.182 +          make_axiom_arity_clause (tcons, lookup_type_const tcons ^ "_" ^ class, ar) ::
   1.183 +          arity_clause (class::seen) n (tcons,ars)
   1.184  
   1.185 -fun multi_arity_clause dfg [] = []
   1.186 -  | multi_arity_clause dfg ((tcons, ars) :: tc_arlists) =
   1.187 -      arity_clause dfg [] 1 (tcons, ars) @ multi_arity_clause dfg tc_arlists
   1.188 +fun multi_arity_clause [] = []
   1.189 +  | multi_arity_clause ((tcons, ars) :: tc_arlists) =
   1.190 +      arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
   1.191  
   1.192  (*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
   1.193    provided its arguments have the corresponding sorts.*)
   1.194 @@ -436,7 +385,7 @@
   1.195    in  map try_classes tycons  end;
   1.196  
   1.197  (*Proving one (tycon, class) membership may require proving others, so iterate.*)
   1.198 -fun iter_type_class_pairs thy tycons [] = ([], [])
   1.199 +fun iter_type_class_pairs _ _ [] = ([], [])
   1.200    | iter_type_class_pairs thy tycons classes =
   1.201        let val cpairs = type_class_pairs thy tycons classes
   1.202            val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))
   1.203 @@ -444,130 +393,16 @@
   1.204            val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
   1.205        in (union (op =) classes' classes, union (op =) cpairs' cpairs) end;
   1.206  
   1.207 -fun make_arity_clauses_dfg dfg thy tycons classes =
   1.208 +fun make_arity_clauses thy tycons classes =
   1.209    let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
   1.210 -  in  (classes', multi_arity_clause dfg cpairs)  end;
   1.211 -val make_arity_clauses = make_arity_clauses_dfg false;
   1.212 -
   1.213 -(**** Find occurrences of predicates in clauses ****)
   1.214 -
   1.215 -(*FIXME: multiple-arity checking doesn't work, as update_new is the wrong
   1.216 -  function (it flags repeated declarations of a function, even with the same arity)*)
   1.217 -
   1.218 -fun update_many keypairs = fold Symtab.update keypairs
   1.219 -
   1.220 -val add_type_sort_preds = update_many o map pred_of_sort o sorts_on_typs
   1.221 -
   1.222 -fun add_classrel_clause_preds (ClassrelClause {subclass, superclass, ...}) =
   1.223 -  Symtab.update (subclass, 1) #> Symtab.update (superclass, 1)
   1.224 -
   1.225 -fun class_of_arityLit (TConsLit (tclass, _, _)) = tclass
   1.226 -  | class_of_arityLit (TVarLit (tclass, _)) = tclass;
   1.227 -
   1.228 -fun add_arity_clause_preds (ArityClause {conclLit, premLits, ...}) =
   1.229 -  let
   1.230 -    val classes = map (make_type_class o class_of_arityLit)
   1.231 -                      (conclLit :: premLits)
   1.232 -  in fold (Symtab.update o rpair 1) classes end;
   1.233 -
   1.234 -(*** Find occurrences of functions in clauses ***)
   1.235 -
   1.236 -fun add_fol_type_funcs (TyVar _) = I
   1.237 -  | add_fol_type_funcs (TyFree (s, _)) = Symtab.update (s, 0)
   1.238 -  | add_fol_type_funcs (TyConstr ((s, _), tys)) =
   1.239 -    Symtab.update (s, length tys) #> fold add_fol_type_funcs tys
   1.240 -
   1.241 -(*TFrees are recorded as constants*)
   1.242 -fun add_type_sort_funcs (TVar _, funcs) = funcs
   1.243 -  | add_type_sort_funcs (TFree (a, _), funcs) =
   1.244 -      Symtab.update (make_fixed_type_var a, 0) funcs
   1.245 -
   1.246 -fun add_arity_clause_funcs (ArityClause {conclLit,...}) funcs =
   1.247 -  let val TConsLit (_, tcons, tvars) = conclLit
   1.248 -  in  Symtab.update (tcons, length tvars) funcs  end;
   1.249 -
   1.250 -(*This type can be overlooked because it is built-in...*)
   1.251 -val init_functab = Symtab.update ("tc_itself", 1) Symtab.empty;
   1.252 -
   1.253 -
   1.254 -(**** String-oriented operations ****)
   1.255 -
   1.256 -fun string_of_clausename (cls_id,ax_name) =
   1.257 -    clause_prefix ^ ascii_of ax_name ^ "_" ^ Int.toString cls_id;
   1.258 -
   1.259 -fun string_of_type_clsname (cls_id,ax_name,idx) =
   1.260 -    string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx);
   1.261 -
   1.262 -
   1.263 -(**** Producing DFG files ****)
   1.264 -
   1.265 -(*Attach sign in DFG syntax: false means negate.*)
   1.266 -fun dfg_sign true s = s
   1.267 -  | dfg_sign false s = "not(" ^ s ^ ")"
   1.268 -
   1.269 -fun dfg_of_type_literal pos (TyLitVar (s, (s', _))) =
   1.270 -    dfg_sign pos (s ^ "(" ^ s' ^ ")")
   1.271 -  | dfg_of_type_literal pos (TyLitFree (s, (s', _))) =
   1.272 -    dfg_sign pos (s ^ "(" ^ s' ^ ")");
   1.273 -
   1.274 -(*Enclose the clause body by quantifiers, if necessary*)
   1.275 -fun dfg_forall [] body = body
   1.276 -  | dfg_forall vars body = "forall([" ^ commas vars ^ "],\n" ^ body ^ ")"
   1.277 -
   1.278 -fun gen_dfg_cls (cls_id, ax_name, Axiom, lits, tylits, vars) =
   1.279 -      "clause( %(axiom)\n" ^
   1.280 -      dfg_forall vars ("or(" ^ commas (tylits@lits) ^ ")") ^ ",\n" ^
   1.281 -      string_of_clausename (cls_id,ax_name) ^  ").\n\n"
   1.282 -  | gen_dfg_cls (cls_id, ax_name, Conjecture, lits, _, vars) =
   1.283 -      "clause( %(negated_conjecture)\n" ^
   1.284 -      dfg_forall vars ("or(" ^ commas lits ^ ")") ^ ",\n" ^
   1.285 -      string_of_clausename (cls_id,ax_name) ^  ").\n\n";
   1.286 -
   1.287 -fun string_of_arity (name, arity) =  "(" ^ name ^ ", " ^ Int.toString arity ^ ")"
   1.288 -
   1.289 -fun string_of_preds [] = ""
   1.290 -  | string_of_preds preds = "predicates[" ^ commas(map string_of_arity preds) ^ "].\n";
   1.291 -
   1.292 -fun string_of_funcs [] = ""
   1.293 -  | string_of_funcs funcs = "functions[" ^ commas(map string_of_arity funcs) ^ "].\n" ;
   1.294 -
   1.295 -fun string_of_symbols predstr funcstr =
   1.296 -  "list_of_symbols.\n" ^ predstr  ^ funcstr  ^ "end_of_list.\n\n";
   1.297 -
   1.298 -fun string_of_start name = "begin_problem(" ^ name ^ ").\n\n";
   1.299 -
   1.300 -fun string_of_descrip name =
   1.301 -  "list_of_descriptions.\nname({*" ^ name ^
   1.302 -  "*}).\nauthor({*Isabelle*}).\nstatus(unknown).\ndescription({*auto-generated*}).\nend_of_list.\n\n"
   1.303 -
   1.304 -fun dfg_tfree_clause tfree_lit =
   1.305 -  "clause( %(negated_conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ").\n\n"
   1.306 -
   1.307 -fun dfg_of_arLit (TConsLit (c,t,args)) =
   1.308 -      dfg_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")")
   1.309 -  | dfg_of_arLit (TVarLit (c,str)) =
   1.310 -      dfg_sign false (make_type_class c ^ "(" ^ str ^ ")")
   1.311 -
   1.312 -fun dfg_classrelLits sub sup =  "not(" ^ sub ^ "(T)), " ^ sup ^ "(T)";
   1.313 -
   1.314 -fun dfg_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) =
   1.315 -  "clause(forall([T],\nor( " ^ dfg_classrelLits subclass superclass ^ ")),\n" ^
   1.316 -  axiom_name ^ ").\n\n";
   1.317 -
   1.318 -fun string_of_ar axiom_name = arclause_prefix ^ ascii_of axiom_name;
   1.319 -
   1.320 -fun dfg_arity_clause (ArityClause{axiom_name,conclLit,premLits,...}) =
   1.321 -  let val TConsLit (_,_,tvars) = conclLit
   1.322 -      val lits = map dfg_of_arLit (conclLit :: premLits)
   1.323 -  in
   1.324 -      "clause( %(axiom)\n" ^
   1.325 -      dfg_forall tvars ("or( " ^ commas lits ^ ")") ^ ",\n" ^
   1.326 -      string_of_ar axiom_name ^ ").\n\n"
   1.327 -  end;
   1.328 +  in  (classes', multi_arity_clause cpairs)  end;
   1.329  
   1.330  
   1.331  (**** Produce TPTP files ****)
   1.332  
   1.333 +fun string_of_clausename (cls_id, ax_name) =
   1.334 +    clause_prefix ^ ascii_of ax_name ^ "_" ^ Int.toString cls_id
   1.335 +
   1.336  fun tptp_sign true s = s
   1.337    | tptp_sign false s = "~ " ^ s
   1.338  
   1.339 @@ -594,8 +429,8 @@
   1.340    | tptp_of_arLit (TVarLit (c,str)) =
   1.341        tptp_sign false (make_type_class c ^ "(" ^ str ^ ")")
   1.342  
   1.343 -fun tptp_arity_clause (ArityClause{axiom_name,conclLit,premLits,...}) =
   1.344 -  tptp_cnf (string_of_ar axiom_name) "axiom"
   1.345 +fun tptp_arity_clause (ArityClause {axiom_name, conclLit, premLits, ...}) =
   1.346 +  tptp_cnf (arclause_prefix ^ ascii_of axiom_name) "axiom"
   1.347             (tptp_clause (map tptp_of_arLit (conclLit :: premLits)))
   1.348  
   1.349  fun tptp_classrelLits sub sup =