src/HOL/Tools/res_clause.ML
changeset 21509 6c5755ad9cae
parent 21470 7c1b59ddcd56
child 21560 d92389321fa7
     1.1 --- a/src/HOL/Tools/res_clause.ML	Thu Nov 23 23:05:28 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Fri Nov 24 13:24:30 2006 +0100
     1.3 @@ -17,12 +17,14 @@
     1.4    datatype fol_term = UVar of string * fol_type
     1.5                      | Fun of string * fol_type list * fol_term list;
     1.6    datatype predicate = Predicate of string * fol_type list * fol_term list;
     1.7 +  datatype kind = Axiom | Conjecture;
     1.8 +  val name_of_kind : kind -> string
     1.9    type typ_var and type_literal and literal
    1.10    val literals_of_term: Term.term -> literal list * (typ_var * Term.sort) list
    1.11    val add_typs_aux : (typ_var * string list) list -> type_literal list * type_literal list
    1.12    val arity_clause_thy: theory -> arityClause list 
    1.13    val ascii_of : string -> string
    1.14 -  val bracket_pack : string list -> string
    1.15 +  val tptp_pack : string list -> string
    1.16    val make_classrel_clauses: theory -> class list -> class list -> classrelClause list 
    1.17    val clause_prefix : string 
    1.18    val clause2tptp : clause -> string * string list
    1.19 @@ -30,8 +32,7 @@
    1.20    val dfg_write_file:  thm list -> string -> 
    1.21         ((thm * (string * int)) list * classrelClause list * arityClause list) -> string list
    1.22    val fixed_var_prefix : string
    1.23 -  val gen_tptp_cls : int * string * string * string -> string
    1.24 -  val gen_tptp_type_cls : int * string * string * string * int -> string
    1.25 +  val gen_tptp_cls : int * string * string * string list -> string
    1.26    val get_axiomName : clause ->  string
    1.27    val get_literals : clause -> literal list
    1.28    val init : theory -> unit
    1.29 @@ -52,7 +53,6 @@
    1.30    val mk_typ_var_sort : Term.typ -> typ_var * sort
    1.31    val paren_pack : string list -> string
    1.32    val schematic_var_prefix : string
    1.33 -  val special_equal : bool ref
    1.34    val string_of_fol_type : fol_type -> string
    1.35    val tconst_prefix : string 
    1.36    val tfree_prefix : string
    1.37 @@ -86,11 +86,6 @@
    1.38  structure ResClause =
    1.39  struct
    1.40  
    1.41 -(* Added for typed equality *)
    1.42 -val special_equal = ref false; (* by default,equality does not carry type information *)
    1.43 -val eq_typ_wrapper = "typeinfo"; (* default string *)
    1.44 -
    1.45 -
    1.46  val schematic_var_prefix = "V_";
    1.47  val fixed_var_prefix = "v_";
    1.48  
    1.49 @@ -167,7 +162,8 @@
    1.50  fun paren_pack [] = ""   (*empty argument list*)
    1.51    | paren_pack strings = "(" ^ commas strings ^ ")";
    1.52  
    1.53 -fun bracket_pack strings = "[" ^ commas strings ^ "]";
    1.54 +(*TSTP format uses (...) rather than the old [...]*)
    1.55 +fun tptp_pack strings = "(" ^ space_implode " | " strings ^ ")";
    1.56  
    1.57  
    1.58  (*Remove the initial ' character from a type variable, if it is present*)
    1.59 @@ -207,10 +203,9 @@
    1.60  
    1.61  val keep_types = ref true;
    1.62  
    1.63 -datatype kind = Axiom | Hypothesis | Conjecture;
    1.64 +datatype kind = Axiom | Conjecture;
    1.65  fun name_of_kind Axiom = "axiom"
    1.66 -  | name_of_kind Hypothesis = "hypothesis"
    1.67 -  | name_of_kind Conjecture = "conjecture";
    1.68 +  | name_of_kind Conjecture = "negated_conjecture";
    1.69  
    1.70  type clause_id = int;
    1.71  type axiom_name = string;
    1.72 @@ -640,33 +635,24 @@
    1.73  
    1.74  (**** String-oriented operations ****)
    1.75  
    1.76 -fun wrap_eq_type typ t = eq_typ_wrapper ^"(" ^ t ^ "," ^ typ ^ ")";
    1.77 -
    1.78 -(*Only need to wrap equality's arguments with "typeinfo" if the output clauses are typed 
    1.79 - and if we specifically ask for types to be included.   *)
    1.80 -fun string_of_equality (typ,terms) =
    1.81 -      let val [tstr1,tstr2] = map string_of_term terms
    1.82 -	  val typ' = string_of_fol_type typ
    1.83 -      in
    1.84 -	  if !keep_types andalso !special_equal 
    1.85 -	  then "equal(" ^ (wrap_eq_type typ' tstr1) ^ "," ^ 
    1.86 -		 	  (wrap_eq_type typ' tstr2) ^ ")"
    1.87 -	  else "equal(" ^ tstr1 ^ "," ^ tstr2 ^ ")"
    1.88 -      end
    1.89 -and string_of_term (UVar(x,_)) = x
    1.90 -  | string_of_term (Fun("equal",[typ],terms)) = string_of_equality(typ,terms)
    1.91 +fun string_of_term (UVar(x,_)) = x
    1.92    | string_of_term (Fun (name,typs,[])) = name ^ (paren_pack (map string_of_fol_type typs))
    1.93    | string_of_term (Fun (name,typs,terms)) = 
    1.94 -      let val terms_as_strings = map string_of_term terms
    1.95 -	  val typs' = if !keep_types then map string_of_fol_type typs else []
    1.96 -      in  name ^ (paren_pack (terms_as_strings @ typs'))  end;
    1.97 +      let val typs' = if !keep_types then map string_of_fol_type typs else []
    1.98 +      in  name ^ (paren_pack (map string_of_term terms @ typs'))  end;
    1.99 +
   1.100 +fun string_of_pair [t1,t2] = (string_of_term t1, string_of_term t2)
   1.101 +  | string_of_pair _ = raise ERROR ("equality predicate requires two arguments");
   1.102 +
   1.103 +fun string_of_equality ts =
   1.104 +  let val (s1,s2) = string_of_pair ts
   1.105 +  in "equal(" ^ s1 ^ "," ^ s2 ^ ")" end;
   1.106  
   1.107  (* before output the string of the predicate, check if the predicate corresponds to an equality or not. *)
   1.108 -fun string_of_predicate (Predicate("equal",[typ],terms)) = string_of_equality(typ,terms)
   1.109 -  | string_of_predicate (Predicate(name,typs,terms)) = 
   1.110 -      let val terms_as_strings = map string_of_term terms
   1.111 -	  val typs' = if !keep_types then map string_of_fol_type typs else []
   1.112 -      in  name ^ (paren_pack (terms_as_strings @ typs'))  end;
   1.113 +fun string_of_predicate (Predicate("equal",_,ts)) = string_of_equality ts
   1.114 +  | string_of_predicate (Predicate(name,typs,ts)) = 
   1.115 +      let val typs' = if !keep_types then map string_of_fol_type typs else []
   1.116 +      in  name ^ (paren_pack (map string_of_term ts @ typs'))  end;
   1.117  
   1.118  fun string_of_clausename (cls_id,ax_name) = 
   1.119      clause_prefix ^ ascii_of ax_name ^ "_" ^ Int.toString cls_id;
   1.120 @@ -746,7 +732,7 @@
   1.121    "*}).\nauthor({*Isabelle*}).\nstatus(unknown).\ndescription({*auto-generated*}).\nend_of_list.\n\n"
   1.122  
   1.123  fun dfg_tfree_clause tfree_lit =
   1.124 -  "clause( %(conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ").\n\n"
   1.125 +  "clause( %(negated_conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ").\n\n"
   1.126  
   1.127  fun string_of_arClauseID (ArityClause {axiom_name,...}) =
   1.128      arclause_prefix ^ ascii_of axiom_name;
   1.129 @@ -807,22 +793,23 @@
   1.130  (**** Produce TPTP files ****)
   1.131  
   1.132  (*Attach sign in TPTP syntax: false means negate.*)
   1.133 -fun tptp_sign true s = "++" ^ s
   1.134 -  | tptp_sign false s = "--" ^ s
   1.135 +fun tptp_sign true s = s
   1.136 +  | tptp_sign false s = "~ " ^ s
   1.137  
   1.138 -fun tptp_literal (Literal(pol,pred)) = 
   1.139 -      (if pol then "++" else "--") ^ string_of_predicate pred;
   1.140 +fun tptp_of_equality pol ts =
   1.141 +  let val (s1,s2) = string_of_pair ts
   1.142 +      val eqop = if pol then " = " else " != "
   1.143 +  in  s1 ^ eqop ^ s2  end;
   1.144  
   1.145 -fun tptp_of_typeLit (LTVar (s,ty)) = "--" ^ s ^ "(" ^ ty ^ ")"
   1.146 -  | tptp_of_typeLit (LTFree (s,ty)) = "++" ^ s ^ "(" ^ ty ^ ")";
   1.147 +fun tptp_literal (Literal(pol,Predicate("equal",_,ts))) = tptp_of_equality pol ts
   1.148 +  | tptp_literal (Literal(pol,pred)) = tptp_sign pol (string_of_predicate pred);
   1.149 +
   1.150 +fun tptp_of_typeLit (LTVar (s,ty))  = tptp_sign false (s ^ "(" ^ ty ^ ")")
   1.151 +  | tptp_of_typeLit (LTFree (s,ty)) = tptp_sign true  (s ^ "(" ^ ty ^ ")");
   1.152   
   1.153  fun gen_tptp_cls (cls_id,ax_name,knd,lits) = 
   1.154 -    "input_clause(" ^ string_of_clausename (cls_id,ax_name) ^ "," ^ 
   1.155 -    knd ^ "," ^ lits ^ ").\n";
   1.156 -
   1.157 -fun gen_tptp_type_cls (cls_id,ax_name,knd,tfree_lit,idx) = 
   1.158 -    "input_clause(" ^ string_of_type_clsname (cls_id,ax_name,idx) ^ "," ^ 
   1.159 -    knd ^ ",[" ^ tfree_lit ^ "]).\n";
   1.160 +    "cnf(" ^ string_of_clausename (cls_id,ax_name) ^ "," ^ 
   1.161 +    name_of_kind knd ^ "," ^ tptp_pack lits ^ ").\n";
   1.162  
   1.163  fun tptp_type_lits (Clause {literals, types_sorts, ...}) = 
   1.164      let val lits = map tptp_literal literals
   1.165 @@ -838,15 +825,14 @@
   1.166  fun clause2tptp (cls as Clause {clause_id, axiom_name, kind, ...}) =
   1.167      let val (lits,tfree_lits) = tptp_type_lits cls 
   1.168              (*"lits" includes the typing assumptions (TVars)*)
   1.169 -	val knd = name_of_kind kind
   1.170 -	val cls_str = gen_tptp_cls(clause_id, axiom_name, knd, bracket_pack lits) 
   1.171 +	val cls_str = gen_tptp_cls(clause_id, axiom_name, kind, lits) 
   1.172      in
   1.173  	(cls_str,tfree_lits) 
   1.174      end;
   1.175  
   1.176  fun tptp_tfree_clause tfree_lit =
   1.177 -    "input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "]).\n";
   1.178 -
   1.179 +    "cnf(" ^ "tfree_tcs," ^ "negated_conjecture" ^ "," ^ tptp_pack[tfree_lit] ^ ").\n";
   1.180 +    
   1.181  fun tptp_of_arLit (TConsLit(b,(c,t,args))) =
   1.182        tptp_sign b (c ^ "(" ^ t ^ paren_pack args ^ ")")
   1.183    | tptp_of_arLit (TVarLit(b,(c,str))) =
   1.184 @@ -857,17 +843,15 @@
   1.185        val knd = name_of_kind kind
   1.186        val lits = map tptp_of_arLit (conclLit :: premLits)
   1.187    in
   1.188 -    "input_clause(" ^ arcls_id ^ "," ^ knd ^ "," ^ bracket_pack lits ^ ").\n"
   1.189 +    "cnf(" ^ arcls_id ^ "," ^ knd ^ "," ^ tptp_pack lits ^ ").\n"
   1.190    end;
   1.191  
   1.192  fun tptp_classrelLits sub sup = 
   1.193 -    let val tvar = "(T)"
   1.194 -    in 
   1.195 -	"[--" ^ sub ^ tvar ^ ",++" ^ sup ^ tvar ^ "]"
   1.196 -    end;
   1.197 +  let val tvar = "(T)"
   1.198 +  in  tptp_pack [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)]  end;
   1.199  
   1.200  fun tptp_classrelClause (ClassrelClause {axiom_name,subclass,superclass,...}) =
   1.201 -  "input_clause(" ^ axiom_name ^ ",axiom," ^ tptp_classrelLits subclass superclass ^ ").\n" 
   1.202 +  "cnf(" ^ axiom_name ^ ",axiom," ^ tptp_classrelLits subclass superclass ^ ").\n" 
   1.203  
   1.204  (* write out a subgoal as tptp clauses to the file "xxxx_N"*)
   1.205  fun tptp_write_file thms filename (ax_tuples,classrel_clauses,arity_clauses) =