src/HOL/Tools/res_hol_clause.ML
changeset 21561 cfd2258f0b23
parent 21513 9e9fff87dc6c
child 21573 8a7a68c0096c
     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Mon Nov 27 18:18:05 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Mon Nov 27 18:18:25 2006 +0100
     1.3 @@ -2,7 +2,6 @@
     1.4     Author: Jia Meng, NICTA
     1.5  
     1.6  FOL clauses translated from HOL formulae.  Combinators are used to represent lambda terms.
     1.7 -
     1.8  *)
     1.9  
    1.10  structure ResHolClause =
    1.11 @@ -251,16 +250,10 @@
    1.12  type polarity = bool;
    1.13  type clause_id = int;
    1.14  
    1.15 -type ctyp_var = ResClause.typ_var;
    1.16 -
    1.17 -type ctype_literal = ResClause.type_literal;
    1.18 -
    1.19 -
    1.20  datatype combterm = CombConst of string * ResClause.fol_type * ResClause.fol_type list
    1.21  		  | CombFree of string * ResClause.fol_type
    1.22  		  | CombVar of string * ResClause.fol_type
    1.23  		  | CombApp of combterm * combterm * ResClause.fol_type
    1.24 -		  | Bool of combterm;
    1.25  		  
    1.26  datatype literal = Literal of polarity * combterm;
    1.27  
    1.28 @@ -270,22 +263,21 @@
    1.29  		    th: thm,
    1.30  		    kind: ResClause.kind,
    1.31  		    literals: literal list,
    1.32 -		    ctypes_sorts: (ctyp_var * Term.sort) list, 
    1.33 -                    ctvar_type_literals: ctype_literal list, 
    1.34 -                    ctfree_type_literals: ctype_literal list};
    1.35 +		    ctypes_sorts: (ResClause.typ_var * Term.sort) list, 
    1.36 +                    ctvar_type_literals: ResClause.type_literal list, 
    1.37 +                    ctfree_type_literals: ResClause.type_literal list};
    1.38  
    1.39  
    1.40  (*********************************************************************)
    1.41  (* convert a clause with type Term.term to a clause with type clause *)
    1.42  (*********************************************************************)
    1.43  
    1.44 -fun isFalse (Literal(pol,Bool(CombConst(c,_,_)))) =
    1.45 +fun isFalse (Literal(pol, CombConst(c,_,_))) =
    1.46        (pol andalso c = "c_False") orelse
    1.47        (not pol andalso c = "c_True")
    1.48    | isFalse _ = false;
    1.49  
    1.50 -
    1.51 -fun isTrue (Literal (pol,Bool(CombConst(c,_,_)))) =
    1.52 +fun isTrue (Literal (pol, CombConst(c,_,_))) =
    1.53        (pol andalso c = "c_True") orelse
    1.54        (not pol andalso c = "c_False")
    1.55    | isTrue _ = false;
    1.56 @@ -293,28 +285,27 @@
    1.57  fun isTaut (Clause {literals,...}) = exists isTrue literals;  
    1.58  
    1.59  fun type_of (Type (a, Ts)) =
    1.60 -    let val (folTypes,ts) = types_of Ts
    1.61 -	val t = ResClause.make_fixed_type_const a
    1.62 -    in
    1.63 -	(ResClause.mk_fol_type("Comp",t,folTypes),ts)
    1.64 -    end
    1.65 +      let val (folTypes,ts) = types_of Ts
    1.66 +	  val t = ResClause.make_fixed_type_const a
    1.67 +      in
    1.68 +	  (ResClause.mk_fol_type("Comp",t,folTypes),ts)
    1.69 +      end
    1.70    | type_of (tp as (TFree(a,s))) =
    1.71 -    let val t = ResClause.make_fixed_type_var a
    1.72 -    in
    1.73 -	(ResClause.mk_fol_type("Fixed",t,[]),[ResClause.mk_typ_var_sort tp])
    1.74 -    end
    1.75 +      let val t = ResClause.make_fixed_type_var a
    1.76 +      in
    1.77 +	  (ResClause.mk_fol_type("Fixed",t,[]),[ResClause.mk_typ_var_sort tp])
    1.78 +      end
    1.79    | type_of (tp as (TVar(v,s))) =
    1.80 -    let val t = ResClause.make_schematic_type_var v
    1.81 -    in
    1.82 -	(ResClause.mk_fol_type("Var",t,[]),[ResClause.mk_typ_var_sort tp])
    1.83 -    end
    1.84 -
    1.85 +      let val t = ResClause.make_schematic_type_var v
    1.86 +      in
    1.87 +	  (ResClause.mk_fol_type("Var",t,[]),[ResClause.mk_typ_var_sort tp])
    1.88 +      end
    1.89  and types_of Ts =
    1.90 -    let val foltyps_ts = map type_of Ts
    1.91 -	val (folTyps,ts) = ListPair.unzip foltyps_ts
    1.92 -    in
    1.93 -	(folTyps,ResClause.union_all ts)
    1.94 -    end;
    1.95 +      let val foltyps_ts = map type_of Ts
    1.96 +	  val (folTyps,ts) = ListPair.unzip foltyps_ts
    1.97 +      in
    1.98 +	  (folTyps,ResClause.union_all ts)
    1.99 +      end;
   1.100  
   1.101  (* same as above, but no gathering of sort information *)
   1.102  fun simp_type_of (Type (a, Ts)) = 
   1.103 @@ -330,46 +321,37 @@
   1.104  fun const_type_of (c,t) =
   1.105      let val (tp,ts) = type_of t
   1.106  	val tvars = !const_typargs(c,t)
   1.107 -	val tvars' = map simp_type_of tvars
   1.108      in
   1.109 -	(tp,ts,tvars')
   1.110 +	(tp, ts, map simp_type_of tvars)
   1.111      end;
   1.112  
   1.113 -fun is_bool_type (Type("bool",[])) = true
   1.114 -  | is_bool_type _ = false;
   1.115 -
   1.116 -
   1.117  (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
   1.118  fun combterm_of (Const(c,t)) =
   1.119        let val (tp,ts,tvar_list) = const_type_of (c,t)
   1.120  	  val c' = CombConst(ResClause.make_fixed_const c,tp,tvar_list)
   1.121 -	  val c'' = if is_bool_type t then Bool(c') else c'
   1.122        in
   1.123 -	  (c'',ts)
   1.124 +	  (c',ts)
   1.125        end
   1.126    | combterm_of (Free(v,t)) =
   1.127        let val (tp,ts) = type_of t
   1.128  	  val v' = if ResClause.isMeta v then CombVar(ResClause.make_schematic_var(v,0),tp)
   1.129  		   else CombFree(ResClause.make_fixed_var v,tp)
   1.130 -	  val v'' = if is_bool_type t then Bool(v') else v'
   1.131        in
   1.132 -	  (v'',ts)
   1.133 +	  (v',ts)
   1.134        end
   1.135    | combterm_of (Var(v,t)) =
   1.136        let val (tp,ts) = type_of t
   1.137  	  val v' = CombVar(ResClause.make_schematic_var v,tp)
   1.138 -	  val v'' = if is_bool_type t then Bool(v') else v'
   1.139        in
   1.140 -	  (v'',ts)
   1.141 +	  (v',ts)
   1.142        end
   1.143    | combterm_of (t as (P $ Q)) =
   1.144        let val (P',tsP) = combterm_of P
   1.145  	  val (Q',tsQ) = combterm_of Q
   1.146  	  val tp = Term.type_of t
   1.147  	  val t' = CombApp(P',Q', simp_type_of tp)
   1.148 -	  val t'' = if is_bool_type tp then Bool(t') else t'
   1.149        in
   1.150 -	  (t'',tsP union tsQ)
   1.151 +	  (t',tsP union tsQ)
   1.152        end;
   1.153  
   1.154  fun predicate_of ((Const("Not",_) $ P), polarity) =
   1.155 @@ -447,8 +429,7 @@
   1.156  fun type_of_combterm (CombConst(c,tp,_)) = tp
   1.157    | type_of_combterm (CombFree(v,tp)) = tp
   1.158    | type_of_combterm (CombVar(v,tp)) = tp
   1.159 -  | type_of_combterm (CombApp(t1,t2,tp)) = tp
   1.160 -  | type_of_combterm (Bool(t)) = type_of_combterm t;
   1.161 +  | type_of_combterm (CombApp(t1,t2,tp)) = tp;
   1.162  
   1.163  fun string_of_combterm1 (CombConst(c,tp,_)) = 
   1.164        let val c' = if c = "equal" then "c_fequal" else c
   1.165 @@ -468,8 +449,7 @@
   1.166  	                     [s1,s2, ResClause.string_of_fol_type (type_of_combterm t1)]
   1.167  	    | T_NONE => app_str ^ ResClause.paren_pack [s1,s2]
   1.168  	    | T_CONST => raise ERROR "string_of_combterm1"
   1.169 -      end
   1.170 -  | string_of_combterm1 (Bool(t)) = string_of_combterm1 t;
   1.171 +      end;
   1.172  
   1.173  fun string_of_combterm2 (CombConst(c,tp,tvars)) = 
   1.174        let val tvars' = map ResClause.string_of_fol_type tvars
   1.175 @@ -480,16 +460,15 @@
   1.176    | string_of_combterm2 (CombFree(v,tp)) = v
   1.177    | string_of_combterm2 (CombVar(v,tp)) = v
   1.178    | string_of_combterm2 (CombApp(t1,t2,_)) =
   1.179 -      app_str ^ ResClause.paren_pack [string_of_combterm2 t1, string_of_combterm2 t2]
   1.180 -  | string_of_combterm2 (Bool(t)) = string_of_combterm2 t
   1.181 +      app_str ^ ResClause.paren_pack [string_of_combterm2 t1, string_of_combterm2 t2];
   1.182  
   1.183  fun string_of_combterm t = 
   1.184      case !typ_level of T_CONST => string_of_combterm2 t
   1.185  		           | _ => string_of_combterm1 t;
   1.186  		           
   1.187 -fun string_of_predicate (Bool(CombApp(CombApp(CombConst("equal",_,_),t1,_),t2,_))) =
   1.188 +fun string_of_predicate (CombApp(CombApp(CombConst("equal",_,_),t1,_),t2,_)) =
   1.189        ("equal" ^ ResClause.paren_pack [string_of_combterm t1, string_of_combterm t2])
   1.190 -  | string_of_predicate (Bool(t)) = 
   1.191 +  | string_of_predicate t = 
   1.192        bool_str ^ ResClause.paren_pack [string_of_combterm t]
   1.193  
   1.194  fun string_of_clausename (cls_id,ax_name) = 
   1.195 @@ -499,13 +478,13 @@
   1.196      string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx);
   1.197  
   1.198  
   1.199 -(* tptp format *)
   1.200 +(*** tptp format ***)
   1.201  
   1.202  fun tptp_of_equality pol (t1,t2) =
   1.203    let val eqop = if pol then " = " else " != "
   1.204    in  string_of_combterm t1 ^ eqop ^ string_of_combterm t2  end;
   1.205  
   1.206 -fun tptp_literal (Literal(pol, Bool(CombApp(CombApp(CombConst("equal",_,_),t1,_),t2,_)))) = 
   1.207 +fun tptp_literal (Literal(pol, CombApp(CombApp(CombConst("equal",_,_),t1,_),t2,_))) = 
   1.208        tptp_of_equality pol (t1,t2)
   1.209    | tptp_literal (Literal(pol,pred)) = 
   1.210        ResClause.tptp_sign pol (string_of_predicate pred);
   1.211 @@ -531,7 +510,8 @@
   1.212      end;
   1.213  
   1.214  
   1.215 -(* dfg format *)
   1.216 +(*** dfg format ***)
   1.217 +
   1.218  fun dfg_literal (Literal(pol,pred)) = ResClause.dfg_sign pol (string_of_predicate pred);
   1.219  
   1.220  fun dfg_clause_aux (Clause{literals, ctypes_sorts, ...}) = 
   1.221 @@ -550,9 +530,7 @@
   1.222  fun get_uvars (CombConst(_,_,_)) vars = vars
   1.223    | get_uvars (CombFree(_,_)) vars = vars
   1.224    | get_uvars (CombVar(v,tp)) vars = (v::vars)
   1.225 -  | get_uvars (CombApp(P,Q,tp)) vars = get_uvars P (get_uvars Q vars)
   1.226 -  | get_uvars (Bool(c)) vars = get_uvars c vars;
   1.227 -
   1.228 +  | get_uvars (CombApp(P,Q,tp)) vars = get_uvars P (get_uvars Q vars);
   1.229  
   1.230  fun get_uvars_l (Literal(_,c)) = get_uvars c [];
   1.231  
   1.232 @@ -569,26 +547,22 @@
   1.233  
   1.234  
   1.235  fun init_funcs_tab funcs = 
   1.236 -    let val tp = !typ_level
   1.237 -	val funcs1 = case tp of T_PARTIAL => Symtab.update ("hAPP",3) funcs
   1.238 +    let val funcs1 = case !typ_level of T_PARTIAL => Symtab.update ("hAPP",3) funcs
   1.239  				      | _ => Symtab.update ("hAPP",2) funcs
   1.240 -	val funcs2 = case tp of T_FULL => Symtab.update ("typeinfo",2) funcs1
   1.241 -				      | _ => funcs1
   1.242      in
   1.243 -	funcs2
   1.244 +	Symtab.update ("typeinfo",2) funcs1
   1.245      end;
   1.246  
   1.247  
   1.248  fun add_funcs (CombConst(c,_,tvars),funcs) =
   1.249 -    if c = "equal" then foldl ResClause.add_foltype_funcs funcs tvars
   1.250 -    else
   1.251 -	(case !typ_level of T_CONST => foldl ResClause.add_foltype_funcs (Symtab.update(c,length tvars) funcs) tvars
   1.252 -			  | _ => foldl ResClause.add_foltype_funcs (Symtab.update(c,0) funcs) tvars)
   1.253 +      if c = "equal" then foldl ResClause.add_foltype_funcs funcs tvars
   1.254 +      else
   1.255 +	(case !typ_level of
   1.256 +	     T_CONST => foldl ResClause.add_foltype_funcs (Symtab.update(c,length tvars) funcs) tvars
   1.257 +           | _ => foldl ResClause.add_foltype_funcs (Symtab.update(c,0) funcs) tvars)
   1.258    | add_funcs (CombFree(v,ctp),funcs) = ResClause.add_foltype_funcs (ctp,Symtab.update (v,0) funcs) 
   1.259    | add_funcs (CombVar(_,ctp),funcs) = ResClause.add_foltype_funcs (ctp,funcs)
   1.260 -  | add_funcs (CombApp(P,Q,_),funcs) = add_funcs(P,add_funcs (Q,funcs))
   1.261 -  | add_funcs (Bool(t),funcs) = add_funcs (t,funcs);
   1.262 -
   1.263 +  | add_funcs (CombApp(P,Q,_),funcs) = add_funcs(P,add_funcs (Q,funcs));
   1.264  
   1.265  fun add_literal_funcs (Literal(_,c), funcs) = add_funcs (c,funcs);
   1.266