src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
changeset 36167 c1a35be8e476
parent 36063 cdc6855a6387
child 36168 0a6ed065683d
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Wed Apr 14 21:22:48 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Thu Apr 15 13:49:46 2010 +0200
     1.3 @@ -495,22 +495,24 @@
     1.4  
     1.5  (**** Produce TPTP files ****)
     1.6  
     1.7 -(*Attach sign in TPTP syntax: false means negate.*)
     1.8  fun tptp_sign true s = s
     1.9    | tptp_sign false s = "~ " ^ s
    1.10  
    1.11 -fun tptp_of_typeLit pos (LTVar (s,ty))  = tptp_sign pos (s ^ "(" ^ ty ^ ")")
    1.12 -  | tptp_of_typeLit pos (LTFree (s,ty)) = tptp_sign pos  (s ^ "(" ^ ty ^ ")");
    1.13 +fun tptp_of_typeLit pos (LTVar (s, ty))  = tptp_sign pos (s ^ "(" ^ ty ^ ")")
    1.14 +  | tptp_of_typeLit pos (LTFree (s, ty)) = tptp_sign pos (s ^ "(" ^ ty ^ ")")
    1.15 +
    1.16 +fun tptp_cnf name kind formula =
    1.17 +  "cnf(" ^ name ^ ", " ^ kind ^ ",\n    " ^ formula ^ ").\n"
    1.18  
    1.19 -fun gen_tptp_cls (cls_id,ax_name,Axiom,lits,tylits) =
    1.20 -      "cnf(" ^ string_of_clausename (cls_id,ax_name) ^ ",axiom," ^ 
    1.21 -               tptp_pack (tylits@lits) ^ ").\n"
    1.22 -  | gen_tptp_cls (cls_id,ax_name,Conjecture,lits,_) =
    1.23 -      "cnf(" ^ string_of_clausename (cls_id,ax_name) ^ ",negated_conjecture," ^ 
    1.24 -               tptp_pack lits ^ ").\n";
    1.25 +fun gen_tptp_cls (cls_id, ax_name, Axiom, lits, tylits) =
    1.26 +      tptp_cnf (string_of_clausename (cls_id, ax_name)) "axiom"
    1.27 +               (tptp_pack (tylits @ lits))
    1.28 +  | gen_tptp_cls (cls_id, ax_name, Conjecture, lits, _) =
    1.29 +      tptp_cnf (string_of_clausename (cls_id, ax_name)) "negated_conjecture"
    1.30 +               (tptp_pack lits)
    1.31  
    1.32  fun tptp_tfree_clause tfree_lit =
    1.33 -    "cnf(" ^ "tfree_tcs," ^ "negated_conjecture" ^ "," ^ tptp_pack[tfree_lit] ^ ").\n";
    1.34 +    tptp_cnf "tfree_tcs" "negated_conjecture" (tptp_pack [tfree_lit])
    1.35  
    1.36  fun tptp_of_arLit (TConsLit (c,t,args)) =
    1.37        tptp_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")")
    1.38 @@ -518,14 +520,14 @@
    1.39        tptp_sign false (make_type_class c ^ "(" ^ str ^ ")")
    1.40  
    1.41  fun tptp_arity_clause (ArityClause{axiom_name,conclLit,premLits,...}) =
    1.42 -  "cnf(" ^ string_of_ar axiom_name ^ ",axiom," ^
    1.43 -  tptp_pack (map tptp_of_arLit (conclLit :: premLits)) ^ ").\n";
    1.44 +  tptp_cnf (string_of_ar axiom_name) "axiom"
    1.45 +           (tptp_pack (map tptp_of_arLit (conclLit :: premLits)))
    1.46  
    1.47  fun tptp_classrelLits sub sup =
    1.48    let val tvar = "(T)"
    1.49    in  tptp_pack [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)]  end;
    1.50  
    1.51  fun tptp_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) =
    1.52 -  "cnf(" ^ axiom_name ^ ",axiom," ^ tptp_classrelLits subclass superclass ^ ").\n"
    1.53 +  tptp_cnf axiom_name "axiom" (tptp_classrelLits subclass superclass)
    1.54  
    1.55  end;