Conversion of "equal" to "=" for TSTP format; big tidy-up
authorpaulson
Fri Nov 24 16:38:42 2006 +0100 (2006-11-24)
changeset 215139e9fff87dc6c
parent 21512 3786eb1b69d6
child 21514 e7dcae358d1a
Conversion of "equal" to "=" for TSTP format; big tidy-up
src/HOL/Tools/res_hol_clause.ML
     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Fri Nov 24 13:44:51 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Fri Nov 24 16:38:42 2006 +0100
     1.3 @@ -245,29 +245,21 @@
     1.4  fun const_types_only () = (typ_level:=T_CONST);
     1.5  fun no_types () = (typ_level:=T_NONE);
     1.6  
     1.7 -
     1.8  fun find_typ_level () = !typ_level;
     1.9  
    1.10 -
    1.11  type axiom_name = string;
    1.12 -
    1.13  type polarity = bool;
    1.14 -type indexname = Term.indexname;
    1.15  type clause_id = int;
    1.16 -type csort = Term.sort;
    1.17 -type ctyp = ResClause.fol_type;
    1.18 -
    1.19 -val string_of_ctyp = ResClause.string_of_fol_type;
    1.20  
    1.21  type ctyp_var = ResClause.typ_var;
    1.22  
    1.23  type ctype_literal = ResClause.type_literal;
    1.24  
    1.25  
    1.26 -datatype combterm = CombConst of string * ctyp * ctyp list
    1.27 -		  | CombFree of string * ctyp
    1.28 -		  | CombVar of string * ctyp
    1.29 -		  | CombApp of combterm * combterm * ctyp
    1.30 +datatype combterm = CombConst of string * ResClause.fol_type * ResClause.fol_type list
    1.31 +		  | CombFree of string * ResClause.fol_type
    1.32 +		  | CombVar of string * ResClause.fol_type
    1.33 +		  | CombApp of combterm * combterm * ResClause.fol_type
    1.34  		  | Bool of combterm;
    1.35  		  
    1.36  datatype literal = Literal of polarity * combterm;
    1.37 @@ -278,7 +270,7 @@
    1.38  		    th: thm,
    1.39  		    kind: ResClause.kind,
    1.40  		    literals: literal list,
    1.41 -		    ctypes_sorts: (ctyp_var * csort) list, 
    1.42 +		    ctypes_sorts: (ctyp_var * Term.sort) list, 
    1.43                      ctvar_type_literals: ctype_literal list, 
    1.44                      ctfree_type_literals: ctype_literal list};
    1.45  
    1.46 @@ -326,11 +318,11 @@
    1.47  
    1.48  (* same as above, but no gathering of sort information *)
    1.49  fun simp_type_of (Type (a, Ts)) = 
    1.50 -    let val typs = map simp_type_of Ts
    1.51 -	val t = ResClause.make_fixed_type_const a
    1.52 -    in
    1.53 -	ResClause.mk_fol_type("Comp",t,typs)
    1.54 -    end
    1.55 +      let val typs = map simp_type_of Ts
    1.56 +	  val t = ResClause.make_fixed_type_const a
    1.57 +      in
    1.58 +	  ResClause.mk_fol_type("Comp",t,typs)
    1.59 +      end
    1.60    | simp_type_of (TFree (a,s)) = ResClause.mk_fol_type("Fixed",ResClause.make_fixed_type_var a,[])
    1.61    | simp_type_of (TVar (v,s)) = ResClause.mk_fol_type("Var",ResClause.make_schematic_type_var v,[]);
    1.62  
    1.63 @@ -343,48 +335,42 @@
    1.64  	(tp,ts,tvars')
    1.65      end;
    1.66  
    1.67 -
    1.68  fun is_bool_type (Type("bool",[])) = true
    1.69    | is_bool_type _ = false;
    1.70  
    1.71  
    1.72  (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
    1.73  fun combterm_of (Const(c,t)) =
    1.74 -    let val (tp,ts,tvar_list) = const_type_of (c,t)
    1.75 -	val is_bool = is_bool_type t
    1.76 -	val c' = CombConst(ResClause.make_fixed_const c,tp,tvar_list)
    1.77 -	val c'' = if is_bool then Bool(c') else c'
    1.78 -    in
    1.79 -	(c'',ts)
    1.80 -    end
    1.81 +      let val (tp,ts,tvar_list) = const_type_of (c,t)
    1.82 +	  val c' = CombConst(ResClause.make_fixed_const c,tp,tvar_list)
    1.83 +	  val c'' = if is_bool_type t then Bool(c') else c'
    1.84 +      in
    1.85 +	  (c'',ts)
    1.86 +      end
    1.87    | combterm_of (Free(v,t)) =
    1.88 -    let val (tp,ts) = type_of t
    1.89 -	val is_bool = is_bool_type t
    1.90 -	val v' = if ResClause.isMeta v then CombVar(ResClause.make_schematic_var(v,0),tp)
    1.91 -		 else CombFree(ResClause.make_fixed_var v,tp)
    1.92 -	val v'' = if is_bool then Bool(v') else v'
    1.93 -    in
    1.94 -	(v'',ts)
    1.95 -    end
    1.96 +      let val (tp,ts) = type_of t
    1.97 +	  val v' = if ResClause.isMeta v then CombVar(ResClause.make_schematic_var(v,0),tp)
    1.98 +		   else CombFree(ResClause.make_fixed_var v,tp)
    1.99 +	  val v'' = if is_bool_type t then Bool(v') else v'
   1.100 +      in
   1.101 +	  (v'',ts)
   1.102 +      end
   1.103    | combterm_of (Var(v,t)) =
   1.104 -    let val (tp,ts) = type_of t
   1.105 -	val is_bool = is_bool_type t
   1.106 -	val v' = CombVar(ResClause.make_schematic_var v,tp)
   1.107 -	val v'' = if is_bool then Bool(v') else v'
   1.108 -    in
   1.109 -	(v'',ts)
   1.110 -    end
   1.111 +      let val (tp,ts) = type_of t
   1.112 +	  val v' = CombVar(ResClause.make_schematic_var v,tp)
   1.113 +	  val v'' = if is_bool_type t then Bool(v') else v'
   1.114 +      in
   1.115 +	  (v'',ts)
   1.116 +      end
   1.117    | combterm_of (t as (P $ Q)) =
   1.118 -    let val (P',tsP) = combterm_of P
   1.119 -	val (Q',tsQ) = combterm_of Q
   1.120 -	val tp = Term.type_of t
   1.121 -	val tp' = simp_type_of tp
   1.122 -	val is_bool = is_bool_type tp
   1.123 -	val t' = CombApp(P',Q',tp')
   1.124 -	val t'' = if is_bool then Bool(t') else t'
   1.125 -    in
   1.126 -	(t'',tsP union tsQ)
   1.127 -    end;
   1.128 +      let val (P',tsP) = combterm_of P
   1.129 +	  val (Q',tsQ) = combterm_of Q
   1.130 +	  val tp = Term.type_of t
   1.131 +	  val t' = CombApp(P',Q', simp_type_of tp)
   1.132 +	  val t'' = if is_bool_type tp then Bool(t') else t'
   1.133 +      in
   1.134 +	  (t'',tsP union tsQ)
   1.135 +      end;
   1.136  
   1.137  fun predicate_of ((Const("Not",_) $ P), polarity) =
   1.138      predicate_of (P, not polarity)
   1.139 @@ -447,9 +433,9 @@
   1.140  
   1.141  val type_wrapper = "typeinfo";
   1.142  
   1.143 -fun wrap_type (c,t) = 
   1.144 -    case !typ_level of T_FULL => type_wrapper ^ ResClause.paren_pack [c,t]
   1.145 -		     | _ => c;
   1.146 +fun wrap_type (c,tp) = case !typ_level of
   1.147 +	T_FULL => type_wrapper ^ ResClause.paren_pack [c, ResClause.string_of_fol_type tp]
   1.148 +      | _ => c;
   1.149      
   1.150  
   1.151  val bool_tp = ResClause.make_fixed_type_const "bool";
   1.152 @@ -458,91 +444,53 @@
   1.153  
   1.154  val bool_str = "hBOOL";
   1.155  
   1.156 -exception STRING_OF_COMBTERM of int;
   1.157 +fun type_of_combterm (CombConst(c,tp,_)) = tp
   1.158 +  | type_of_combterm (CombFree(v,tp)) = tp
   1.159 +  | type_of_combterm (CombVar(v,tp)) = tp
   1.160 +  | type_of_combterm (CombApp(t1,t2,tp)) = tp
   1.161 +  | type_of_combterm (Bool(t)) = type_of_combterm t;
   1.162  
   1.163 -(* convert literals of clauses into strings *)
   1.164 -fun string_of_combterm1_aux _ (CombConst(c,tp,_)) = 
   1.165 -    let val tp' = string_of_ctyp tp
   1.166 -	val c' = if c = "equal" then "c_fequal" else c
   1.167 -    in
   1.168 -	(wrap_type (c',tp'),tp')
   1.169 -    end
   1.170 -  | string_of_combterm1_aux _ (CombFree(v,tp)) = 
   1.171 -    let val tp' = string_of_ctyp tp
   1.172 -    in
   1.173 -	(wrap_type (v,tp'),tp')
   1.174 -    end
   1.175 -  | string_of_combterm1_aux _ (CombVar(v,tp)) = 
   1.176 -    let val tp' = string_of_ctyp tp
   1.177 -    in
   1.178 -	(wrap_type (v,tp'),tp')
   1.179 -    end
   1.180 -  | string_of_combterm1_aux is_pred (CombApp(t1,t2,tp)) =
   1.181 -    let val (s1,tp1) = string_of_combterm1_aux is_pred t1
   1.182 -	val (s2,tp2) = string_of_combterm1_aux is_pred t2
   1.183 -	val tp' = ResClause.string_of_fol_type tp
   1.184 -	val r =	case !typ_level of
   1.185 -	            T_FULL => type_wrapper ^ ResClause.paren_pack [(app_str ^ ResClause.paren_pack [s1,s2]),tp']
   1.186 -		  | T_PARTIAL => app_str ^ ResClause.paren_pack [s1,s2,tp1]
   1.187 -		  | T_NONE => app_str ^ ResClause.paren_pack [s1,s2]
   1.188 -		  | T_CONST => raise STRING_OF_COMBTERM 1 (*should not happen, if happened may be a bug*)
   1.189 -    in	(r,tp')   end
   1.190 -  | string_of_combterm1_aux is_pred (Bool(CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))) =
   1.191 -    if is_pred then 
   1.192 -	let val (s1,_) = string_of_combterm1_aux false t1
   1.193 -	    val (s2,_) = string_of_combterm1_aux false t2
   1.194 -	in
   1.195 -	    ("equal" ^ ResClause.paren_pack [s1,s2], bool_tp)
   1.196 -	end
   1.197 -    else
   1.198 -	let val (t,_) = string_of_combterm1_aux false (CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))
   1.199 -	in
   1.200 -	    (t,bool_tp)
   1.201 -	end
   1.202 -  | string_of_combterm1_aux is_pred (Bool(t)) = 
   1.203 -    let val (t',_) = string_of_combterm1_aux false t
   1.204 -	val r = if is_pred then bool_str ^ ResClause.paren_pack [t']
   1.205 -		else t'
   1.206 -    in
   1.207 -	(r,bool_tp)
   1.208 -    end;
   1.209 +fun string_of_combterm1 (CombConst(c,tp,_)) = 
   1.210 +      let val c' = if c = "equal" then "c_fequal" else c
   1.211 +      in  wrap_type (c',tp)  end
   1.212 +  | string_of_combterm1 (CombFree(v,tp)) = wrap_type (v,tp)
   1.213 +  | string_of_combterm1 (CombVar(v,tp)) = wrap_type (v,tp)
   1.214 +  | string_of_combterm1 (CombApp(t1,t2,tp)) =
   1.215 +      let val s1 = string_of_combterm1 t1
   1.216 +	  val s2 = string_of_combterm1 t2
   1.217 +      in
   1.218 +	  case !typ_level of
   1.219 +	      T_FULL => type_wrapper ^ 
   1.220 +	                ResClause.paren_pack 
   1.221 +	                  [app_str ^ ResClause.paren_pack [s1,s2], 
   1.222 +	                   ResClause.string_of_fol_type tp]
   1.223 +	    | T_PARTIAL => app_str ^ ResClause.paren_pack 
   1.224 +	                     [s1,s2, ResClause.string_of_fol_type (type_of_combterm t1)]
   1.225 +	    | T_NONE => app_str ^ ResClause.paren_pack [s1,s2]
   1.226 +	    | T_CONST => raise ERROR "string_of_combterm1"
   1.227 +      end
   1.228 +  | string_of_combterm1 (Bool(t)) = string_of_combterm1 t;
   1.229  
   1.230 -fun string_of_combterm1 is_pred term = fst (string_of_combterm1_aux is_pred term);
   1.231 +fun string_of_combterm2 (CombConst(c,tp,tvars)) = 
   1.232 +      let val tvars' = map ResClause.string_of_fol_type tvars
   1.233 +	  val c' = if c = "equal" then "c_fequal" else c
   1.234 +      in
   1.235 +	  c' ^ ResClause.paren_pack tvars'
   1.236 +      end
   1.237 +  | string_of_combterm2 (CombFree(v,tp)) = v
   1.238 +  | string_of_combterm2 (CombVar(v,tp)) = v
   1.239 +  | string_of_combterm2 (CombApp(t1,t2,_)) =
   1.240 +      app_str ^ ResClause.paren_pack [string_of_combterm2 t1, string_of_combterm2 t2]
   1.241 +  | string_of_combterm2 (Bool(t)) = string_of_combterm2 t
   1.242  
   1.243 -fun string_of_combterm2 _ (CombConst(c,tp,tvars)) = 
   1.244 -    let val tvars' = map string_of_ctyp tvars
   1.245 -	val c' = if c = "equal" then "c_fequal" else c
   1.246 -    in
   1.247 -	c' ^ ResClause.paren_pack tvars'
   1.248 -    end
   1.249 -  | string_of_combterm2 _ (CombFree(v,tp)) = v
   1.250 -  | string_of_combterm2 _ (CombVar(v,tp)) = v
   1.251 -  | string_of_combterm2 is_pred (CombApp(t1,t2,tp)) =
   1.252 -    let val s1 = string_of_combterm2 is_pred t1
   1.253 -	val s2 = string_of_combterm2 is_pred t2
   1.254 -    in
   1.255 -	app_str ^ ResClause.paren_pack [s1,s2]
   1.256 -    end
   1.257 -  | string_of_combterm2 is_pred (Bool(CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))) =
   1.258 -    if is_pred then 
   1.259 -	let val s1 = string_of_combterm2 false t1
   1.260 -	    val s2 = string_of_combterm2 false t2
   1.261 -	in
   1.262 -	    ("equal" ^ ResClause.paren_pack [s1,s2])
   1.263 -	end
   1.264 -    else
   1.265 -	string_of_combterm2 false (CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))
   1.266 - 
   1.267 -  | string_of_combterm2 is_pred (Bool(t)) = 
   1.268 -    let val t' = string_of_combterm2 false t
   1.269 -    in
   1.270 -	if is_pred then bool_str ^ ResClause.paren_pack [t']
   1.271 -	else t'
   1.272 -    end;
   1.273 -
   1.274 -fun string_of_combterm is_pred term = 
   1.275 -    case !typ_level of T_CONST => string_of_combterm2 is_pred term
   1.276 -		     | _ => string_of_combterm1 is_pred term;
   1.277 +fun string_of_combterm t = 
   1.278 +    case !typ_level of T_CONST => string_of_combterm2 t
   1.279 +		           | _ => string_of_combterm1 t;
   1.280 +		           
   1.281 +fun string_of_predicate (Bool(CombApp(CombApp(CombConst("equal",_,_),t1,_),t2,_))) =
   1.282 +      ("equal" ^ ResClause.paren_pack [string_of_combterm t1, string_of_combterm t2])
   1.283 +  | string_of_predicate (Bool(t)) = 
   1.284 +      bool_str ^ ResClause.paren_pack [string_of_combterm t]
   1.285  
   1.286  fun string_of_clausename (cls_id,ax_name) = 
   1.287      ResClause.clause_prefix ^ ResClause.ascii_of ax_name ^ "_" ^ Int.toString cls_id;
   1.288 @@ -553,7 +501,14 @@
   1.289  
   1.290  (* tptp format *)
   1.291  
   1.292 -fun tptp_literal (Literal(pol,pred)) = ResClause.tptp_sign pol (string_of_combterm true pred);
   1.293 +fun tptp_of_equality pol (t1,t2) =
   1.294 +  let val eqop = if pol then " = " else " != "
   1.295 +  in  string_of_combterm t1 ^ eqop ^ string_of_combterm t2  end;
   1.296 +
   1.297 +fun tptp_literal (Literal(pol, Bool(CombApp(CombApp(CombConst("equal",_,_),t1,_),t2,_)))) = 
   1.298 +      tptp_of_equality pol (t1,t2)
   1.299 +  | tptp_literal (Literal(pol,pred)) = 
   1.300 +      ResClause.tptp_sign pol (string_of_predicate pred);
   1.301   
   1.302  fun tptp_type_lits (Clause cls) = 
   1.303      let val lits = map tptp_literal (#literals cls)
   1.304 @@ -577,7 +532,7 @@
   1.305  
   1.306  
   1.307  (* dfg format *)
   1.308 -fun dfg_literal (Literal(pol,pred)) = ResClause.dfg_sign pol (string_of_combterm true pred);
   1.309 +fun dfg_literal (Literal(pol,pred)) = ResClause.dfg_sign pol (string_of_predicate pred);
   1.310  
   1.311  fun dfg_clause_aux (Clause{literals, ctypes_sorts, ...}) = 
   1.312    let val lits = map dfg_literal literals