src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
changeset 36556 81dc2c20f052
parent 36493 a3357a631b96
child 36692 54b64d4ad524
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Thu Apr 29 01:17:14 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Thu Apr 29 10:25:26 2010 +0200
     1.3 @@ -44,9 +44,11 @@
     1.4      TyConstr of name * fol_type list
     1.5    val string_of_fol_type :
     1.6      fol_type -> name_pool option -> string * name_pool option
     1.7 -  datatype type_literal = LTVar of string * string | LTFree of string * string
     1.8 +  datatype type_literal =
     1.9 +    TyLitVar of string * name |
    1.10 +    TyLitFree of string * name
    1.11    exception CLAUSE of string * term
    1.12 -  val add_typs : typ list -> type_literal list
    1.13 +  val add_type_literals : typ list -> type_literal list
    1.14    val get_tvar_strs: typ list -> string list
    1.15    datatype arLit =
    1.16        TConsLit of class * string * string list
    1.17 @@ -68,7 +70,7 @@
    1.18      arity_clause -> int Symtab.table -> int Symtab.table
    1.19    val init_functab: int Symtab.table
    1.20    val dfg_sign: bool -> string -> string
    1.21 -  val dfg_of_typeLit: bool -> type_literal -> string
    1.22 +  val dfg_of_type_literal: bool -> type_literal -> string
    1.23    val gen_dfg_cls: int * string * kind * string list * string list * string list -> string
    1.24    val string_of_preds: (string * Int.int) list -> string
    1.25    val string_of_funcs: (string * int) list -> string
    1.26 @@ -79,7 +81,8 @@
    1.27    val dfg_classrel_clause: classrel_clause -> string
    1.28    val dfg_arity_clause: arity_clause -> string
    1.29    val tptp_sign: bool -> string -> string
    1.30 -  val tptp_of_typeLit : bool -> type_literal -> string
    1.31 +  val tptp_of_type_literal :
    1.32 +    bool -> type_literal -> name_pool option -> string * name_pool option
    1.33    val gen_tptp_cls : int * string * kind * string list * string list -> string
    1.34    val tptp_tfree_clause : string -> string
    1.35    val tptp_arity_clause : arity_clause -> string
    1.36 @@ -173,9 +176,7 @@
    1.37  fun paren_pack [] = ""   (*empty argument list*)
    1.38    | paren_pack strings = "(" ^ commas strings ^ ")";
    1.39  
    1.40 -(*TSTP format uses (...) rather than the old [...]*)
    1.41 -fun tptp_pack strings = "(" ^ space_implode " | " strings ^ ")";
    1.42 -
    1.43 +fun tptp_clause strings = "(" ^ space_implode " | " strings ^ ")"
    1.44  
    1.45  (*Remove the initial ' character from a type variable, if it is present*)
    1.46  fun trim_type_var s =
    1.47 @@ -230,9 +231,9 @@
    1.48  fun empty_name_pool readable_names =
    1.49    if readable_names then SOME (`I Symtab.empty) else NONE
    1.50  
    1.51 +fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs
    1.52  fun pool_map f xs =
    1.53 -  fold_rev (fn x => fn (ys, pool) => f x pool |>> (fn y => y :: ys)) xs
    1.54 -  o pair []
    1.55 +  pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
    1.56  
    1.57  fun add_nice_name full_name nice_prefix j the_pool =
    1.58    let
    1.59 @@ -306,8 +307,10 @@
    1.60        val (ss, pool) = pool_map string_of_fol_type tys pool
    1.61      in (s ^ paren_pack ss, pool) end
    1.62  
    1.63 -(*First string is the type class; the second is a TVar or TFfree*)
    1.64 -datatype type_literal = LTVar of string * string | LTFree of string * string;
    1.65 +(* The first component is the type class; the second is a TVar or TFree. *)
    1.66 +datatype type_literal =
    1.67 +  TyLitVar of string * name |
    1.68 +  TyLitFree of string * name
    1.69  
    1.70  exception CLAUSE of string * term;
    1.71  
    1.72 @@ -317,21 +320,21 @@
    1.73        let val sorts = sorts_on_typs_aux ((x,i), ss)
    1.74        in
    1.75            if s = "HOL.type" then sorts
    1.76 -          else if i = ~1 then LTFree(make_type_class s, make_fixed_type_var x) :: sorts
    1.77 -          else LTVar(make_type_class s, make_schematic_type_var (x,i)) :: sorts
    1.78 +          else if i = ~1 then TyLitFree (make_type_class s, `make_fixed_type_var x) :: sorts
    1.79 +          else TyLitVar (make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts
    1.80        end;
    1.81  
    1.82  fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s)
    1.83    | sorts_on_typs (TVar (v,s))  = sorts_on_typs_aux (v,s);
    1.84  
    1.85 -fun pred_of_sort (LTVar (s,ty)) = (s,1)
    1.86 -  | pred_of_sort (LTFree (s,ty)) = (s,1)
    1.87 +fun pred_of_sort (TyLitVar (s, _)) = (s, 1)
    1.88 +  | pred_of_sort (TyLitFree (s, _)) = (s, 1)
    1.89  
    1.90  (*Given a list of sorted type variables, return a list of type literals.*)
    1.91 -fun add_typs Ts = fold (union (op =)) (map sorts_on_typs Ts) []
    1.92 +fun add_type_literals Ts = fold (union (op =)) (map sorts_on_typs Ts) []
    1.93  
    1.94  (*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear.
    1.95 -  * Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a
    1.96 +  *  Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a
    1.97      in a lemma has the same sort as 'a in the conjecture.
    1.98    * Deleting such clauses will lead to problems with locales in other use of local results
    1.99      where 'a is fixed. Probably we should delete clauses unless the sorts agree.
   1.100 @@ -499,8 +502,10 @@
   1.101  fun dfg_sign true s = s
   1.102    | dfg_sign false s = "not(" ^ s ^ ")"
   1.103  
   1.104 -fun dfg_of_typeLit pos (LTVar (s,ty))  = dfg_sign pos (s ^ "(" ^ ty ^ ")")
   1.105 -  | dfg_of_typeLit pos (LTFree (s,ty)) = dfg_sign pos (s ^ "(" ^ ty ^ ")");
   1.106 +fun dfg_of_type_literal pos (TyLitVar (s, (s', _))) =
   1.107 +    dfg_sign pos (s ^ "(" ^ s' ^ ")")
   1.108 +  | dfg_of_type_literal pos (TyLitFree (s, (s', _))) =
   1.109 +    dfg_sign pos (s ^ "(" ^ s' ^ ")");
   1.110  
   1.111  (*Enclose the clause body by quantifiers, if necessary*)
   1.112  fun dfg_forall [] body = body
   1.113 @@ -563,21 +568,23 @@
   1.114  fun tptp_sign true s = s
   1.115    | tptp_sign false s = "~ " ^ s
   1.116  
   1.117 -fun tptp_of_typeLit pos (LTVar (s, ty))  = tptp_sign pos (s ^ "(" ^ ty ^ ")")
   1.118 -  | tptp_of_typeLit pos (LTFree (s, ty)) = tptp_sign pos (s ^ "(" ^ ty ^ ")")
   1.119 +fun tptp_of_type_literal pos (TyLitVar (s, name)) =
   1.120 +    nice_name name #>> (fn s' => tptp_sign pos (s ^ "(" ^ s' ^ ")"))
   1.121 +  | tptp_of_type_literal pos (TyLitFree (s, name)) =
   1.122 +    nice_name name #>> (fn s' => tptp_sign pos (s ^ "(" ^ s' ^ ")"))
   1.123  
   1.124  fun tptp_cnf name kind formula =
   1.125    "cnf(" ^ name ^ ", " ^ kind ^ ",\n    " ^ formula ^ ").\n"
   1.126  
   1.127  fun gen_tptp_cls (cls_id, ax_name, Axiom, lits, tylits) =
   1.128        tptp_cnf (string_of_clausename (cls_id, ax_name)) "axiom"
   1.129 -               (tptp_pack (tylits @ lits))
   1.130 +               (tptp_clause (tylits @ lits))
   1.131    | gen_tptp_cls (cls_id, ax_name, Conjecture, lits, _) =
   1.132        tptp_cnf (string_of_clausename (cls_id, ax_name)) "negated_conjecture"
   1.133 -               (tptp_pack lits)
   1.134 +               (tptp_clause lits)
   1.135  
   1.136  fun tptp_tfree_clause tfree_lit =
   1.137 -    tptp_cnf "tfree_tcs" "negated_conjecture" (tptp_pack [tfree_lit])
   1.138 +    tptp_cnf "tfree_tcs" "negated_conjecture" (tptp_clause [tfree_lit])
   1.139  
   1.140  fun tptp_of_arLit (TConsLit (c,t,args)) =
   1.141        tptp_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")")
   1.142 @@ -586,11 +593,11 @@
   1.143  
   1.144  fun tptp_arity_clause (ArityClause{axiom_name,conclLit,premLits,...}) =
   1.145    tptp_cnf (string_of_ar axiom_name) "axiom"
   1.146 -           (tptp_pack (map tptp_of_arLit (conclLit :: premLits)))
   1.147 +           (tptp_clause (map tptp_of_arLit (conclLit :: premLits)))
   1.148  
   1.149  fun tptp_classrelLits sub sup =
   1.150    let val tvar = "(T)"
   1.151 -  in  tptp_pack [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)]  end;
   1.152 +  in  tptp_clause [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)]  end;
   1.153  
   1.154  fun tptp_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) =
   1.155    tptp_cnf axiom_name "axiom" (tptp_classrelLits subclass superclass)