src/HOL/Tools/res_clause.ML
changeset 18218 9a7ffce389c3
parent 18199 d236379ea408
child 18275 86cefba6d325
     1.1 --- a/src/HOL/Tools/res_clause.ML	Mon Nov 21 16:51:57 2005 +0100
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Tue Nov 22 10:09:11 2005 +0100
     1.3 @@ -143,7 +143,8 @@
     1.4  end;
     1.5  
     1.6  (* convert a list of strings into one single string; surrounded by brackets *)
     1.7 -fun paren_pack strings = "(" ^ commas strings ^ ")";
     1.8 +fun paren_pack [] = ""   (*empty argument list*)
     1.9 +  | paren_pack strings = "(" ^ commas strings ^ ")";
    1.10  
    1.11  fun bracket_pack strings = "[" ^ commas strings ^ "]";
    1.12  
    1.13 @@ -159,7 +160,6 @@
    1.14  fun make_schematic_var v = schematic_var_prefix ^ (ascii_of_indexname v);
    1.15  fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x);
    1.16  
    1.17 -(*Type variables contain _H because the character ' translates to that.*)
    1.18  fun make_schematic_type_var (x,i) = 
    1.19        tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
    1.20  fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
    1.21 @@ -208,13 +208,11 @@
    1.22  type sort = Term.sort;
    1.23  type fol_type = string;
    1.24  
    1.25 -
    1.26  datatype type_literal = LTVar of string | LTFree of string;
    1.27  
    1.28 -
    1.29  datatype folTerm = UVar of string * fol_type
    1.30 -                 | Fun of string * fol_type * folTerm list;
    1.31 -datatype predicate = Predicate of pred_name * fol_type * folTerm list;
    1.32 +                 | Fun of string * fol_type list * folTerm list;
    1.33 +datatype predicate = Predicate of pred_name * fol_type list * folTerm list;
    1.34  
    1.35  datatype literal = Literal of polarity * predicate * tag;
    1.36  
    1.37 @@ -283,75 +281,73 @@
    1.38  fun preds_of_cls (Clause cls) = #predicates cls;
    1.39  
    1.40  
    1.41 +(*Declarations of the current theory--to allow suppressing types.*)
    1.42 +val const_typargs = ref (Library.K [] : (string*typ -> typ list));
    1.43  
    1.44 -(*Declarations of the current theory--to allow suppressing types.*)
    1.45 -val monomorphic = ref (fn (_: string) => false);
    1.46 -fun no_types_needed s = ! monomorphic s;
    1.47 +fun num_typargs(s,T) = if !keep_types then length (!const_typargs (s,T)) else 0;
    1.48  
    1.49  (*Initialize the type suppression mechanism with the current theory before
    1.50      producing any clauses!*)
    1.51 -fun init thy = (monomorphic := Sign.const_monomorphic thy);
    1.52 +fun init thy = (const_typargs := Sign.const_typargs thy);
    1.53      
    1.54  
    1.55 -(*Flatten a type to a string while accumulating sort constraints on the TFress and
    1.56 +(*Flatten a type to a string while accumulating sort constraints on the TFrees and
    1.57    TVars it contains.*)    
    1.58 -fun type_of (Type (a, [])) = 
    1.59 -      let val t = make_fixed_type_const a
    1.60 -      in (t,([],[(t,0)]))  end
    1.61 -  | type_of (Type (a, Ts)) = 
    1.62 +fun type_of (Type (a, Ts)) = 
    1.63 +      let val (folTyps, (ts, funcs)) = types_of Ts 
    1.64 +	  val t = make_fixed_type_const a
    1.65 +      in    
    1.66 +	  ((t ^ paren_pack folTyps), (ts, (t, length Ts)::funcs))
    1.67 +      end
    1.68 +  | type_of (TFree (a,s)) = 
    1.69 +      let val t = make_fixed_type_var a
    1.70 +      in (t, ([((FOLTFree a),s)], [(t,0)])) end
    1.71 +  | type_of (TVar (v, s)) = (make_schematic_type_var v, ([((FOLTVar v),s)], []))
    1.72 +and types_of Ts =
    1.73        let val foltyps_ts = map type_of Ts 
    1.74  	  val (folTyps,ts_funcs) = ListPair.unzip foltyps_ts
    1.75  	  val (ts, funcslist) = ListPair.unzip ts_funcs
    1.76 -	  val ts' = union_all ts
    1.77 -	  val funcs' = union_all funcslist
    1.78 -	  val t = make_fixed_type_const a
    1.79        in    
    1.80 -	  ((t ^ paren_pack folTyps), (ts', (t, length Ts)::funcs'))
    1.81 -      end
    1.82 -  | type_of (TFree (a, s)) = 
    1.83 -      let val t = make_fixed_type_var a
    1.84 -      in (t, ([((FOLTFree a),s)],[(t,0)])) end
    1.85 -  | type_of (TVar (v, s)) = (make_schematic_type_var v, ([((FOLTVar v),s)], []))
    1.86 +	  (folTyps, (union_all ts, union_all funcslist))
    1.87 +      end;
    1.88  
    1.89  
    1.90 -fun maybe_type_of c T =
    1.91 - if no_types_needed c then ("",([],[])) else type_of T;
    1.92 +fun const_types_of (c,T) = types_of (!const_typargs (c,T));
    1.93  
    1.94  (* Any variables created via the METAHYPS tactical should be treated as
    1.95     universal vars, although it is represented as "Free(...)" by Isabelle *)
    1.96  val isMeta = String.isPrefix "METAHYP1_"
    1.97  
    1.98  fun pred_name_type (Const(c,T)) = 
    1.99 -      let val (typof,(folTyps,funcs)) = maybe_type_of c T
   1.100 -      in (make_fixed_const c, (typof,folTyps), funcs) end
   1.101 +      let val (contys,(folTyps,funcs)) = const_types_of (c,T)
   1.102 +      in (make_fixed_const c, (contys,folTyps), funcs) end
   1.103    | pred_name_type (Free(x,T))  = 
   1.104        if isMeta x then raise CLAUSE("Predicate Not First Order 1", Free(x,T)) 
   1.105 -      else (make_fixed_var x, ("",[]), [])
   1.106 +      else (make_fixed_var x, ([],[]), [])
   1.107    | pred_name_type (v as Var _) = raise CLAUSE("Predicate Not First Order 2", v)
   1.108    | pred_name_type t        = raise CLAUSE("Predicate input unexpected", t);
   1.109  
   1.110  
   1.111 -(* For type equality *)
   1.112 +(* For typed equality *)
   1.113  (* here "arg_typ" is the type of "="'s argument's type, not the type of the equality *)
   1.114  (* Find type of equality arg *)
   1.115  fun eq_arg_type (Type("fun",[T,_])) = 
   1.116      let val (folT,_) = type_of T;
   1.117      in  folT  end;
   1.118  
   1.119 -fun fun_name_type (Const(c,T)) args = 
   1.120 +fun fun_name_type (Const("op =",T)) args =   (*FIXME: Is this special treatment of = needed??*)
   1.121 +      let val t = make_fixed_const "op ="
   1.122 +      in (t, ([eq_arg_type T], []), [(t,2)]) end
   1.123 +  | fun_name_type (Const(c,T)) args = 
   1.124        let val t = make_fixed_const c
   1.125 -	val (typof, (folTyps,funcs)) = maybe_type_of c T
   1.126 -	val arity = if !keep_types andalso not (no_types_needed c)
   1.127 -	            then 1 + length args
   1.128 -	            else length args
   1.129 +	  val (contys, (folTyps,funcs)) = const_types_of (c,T)
   1.130 +	  val arity = num_typargs(c,T) + length args
   1.131        in
   1.132 -	  (t, (typof,folTyps), ((t,arity)::funcs))
   1.133 +	  (t, (contys,folTyps), ((t,arity)::funcs))
   1.134        end
   1.135   | fun_name_type (Free(x,T)) args  = 
   1.136        let val t = make_fixed_var x
   1.137 -      in
   1.138 -	    (t, ("",[]), [(t, length args)])
   1.139 -      end
   1.140 +      in  (t, ([],[]), [(t, length args)]) end
   1.141    | fun_name_type f args = raise CLAUSE("Function Not First Order 1", f);
   1.142  
   1.143  
   1.144 @@ -366,72 +362,57 @@
   1.145  	  if isMeta x then (UVar(make_schematic_var(x,0),folType),
   1.146  			    (ts, ((make_schematic_var(x,0)),0)::funcs))
   1.147  	  else
   1.148 -	      (Fun(make_fixed_var x, folType, []), 
   1.149 +	      (Fun(make_fixed_var x, [folType], []), 
   1.150  	       (ts, ((make_fixed_var x),0)::funcs))
   1.151        end
   1.152    | term_of (Const(c,T)) =  (* impossible to be equality *)
   1.153 -      let val (folType,(ts,funcs)) = type_of T
   1.154 +      let val (contys, (folTyps,funcs)) = const_types_of (c,T)
   1.155        in
   1.156 -	  (Fun(make_fixed_const c, folType, []),
   1.157 -	   (ts, ((make_fixed_const c),0)::funcs))
   1.158 +	  (Fun(make_fixed_const c, contys, []),
   1.159 +	   (folTyps, ((make_fixed_const c),0)::funcs))
   1.160        end    
   1.161 -  | term_of (app as (t $ a)) = 
   1.162 +  | term_of app = 
   1.163        let val (f,args) = strip_comb app
   1.164 -	  fun term_of_aux () = 
   1.165 -	      let val (funName,(funType,ts1),funcs) = fun_name_type f args
   1.166 -		  val (args',ts_funcs) = ListPair.unzip (map term_of args)
   1.167 -		  val (ts2,funcs') = ListPair.unzip ts_funcs
   1.168 -		  val ts3 = union_all (ts1::ts2)
   1.169 -		  val funcs'' = union_all(funcs::funcs')
   1.170 -	      in
   1.171 -		  (Fun(funName,funType,args'), (ts3,funcs''))
   1.172 -	      end
   1.173 -	  fun term_of_eq ((Const ("op =", typ)),args) =
   1.174 -	      let val arg_typ = eq_arg_type typ
   1.175 -		  val (args',ts_funcs) = ListPair.unzip (map term_of args)
   1.176 -		  val (ts,funcs) = ListPair.unzip ts_funcs
   1.177 -		  val equal_name = make_fixed_const ("op =")
   1.178 -	      in
   1.179 -		  (Fun(equal_name,arg_typ,args'),
   1.180 -		   (union_all ts, 
   1.181 -		    (make_fixed_var equal_name, 2):: union_all funcs))
   1.182 -	      end
   1.183 +          val _ = case f of Const(_,_) => ()
   1.184 +			  | Free(s,_)  => 
   1.185 +			      if isMeta s 
   1.186 +			      then raise CLAUSE("Function Not First Order 2", f)
   1.187 +			      else ()
   1.188 +			  | _ => raise CLAUSE("Function Not First Order 3", f);
   1.189 +	  val (funName,(contys,ts1),funcs) = fun_name_type f args
   1.190 +	  val (args',(ts2,funcs')) = terms_of args
   1.191        in
   1.192 -	 case f of Const ("op =", typ) => term_of_eq (f,args)
   1.193 -		 | Const(_,_) => term_of_aux ()
   1.194 -		 | Free(s,_)  => 
   1.195 -		     if isMeta s 
   1.196 -		     then raise CLAUSE("Function Not First Order 2", f)
   1.197 -		     else term_of_aux()
   1.198 -		 | _ => raise CLAUSE("Function Not First Order 3", f)
   1.199 +	  (Fun(funName,contys,args'), 
   1.200 +	   (union_all (ts1::ts2), 
   1.201 +	    union_all(funcs::funcs')))
   1.202        end
   1.203 -  | term_of t = raise CLAUSE("Function Not First Order 4", t); 
   1.204 +  | term_of t = raise CLAUSE("Function Not First Order 4", t)
   1.205 +and terms_of ts =  
   1.206 +      let val (args, ts_funcs) = ListPair.unzip (map term_of ts)
   1.207 +      in
   1.208 +	  (args, ListPair.unzip ts_funcs)
   1.209 +      end
   1.210  
   1.211  
   1.212  fun pred_of (Const("op =", typ), args) =
   1.213        let val arg_typ = eq_arg_type typ 
   1.214 -	  val (args',ts_funcs) = ListPair.unzip (map term_of args)
   1.215 -	  val (ts,funcs) = ListPair.unzip ts_funcs
   1.216 +	  val (args',(ts,funcs)) = terms_of args
   1.217  	  val equal_name = make_fixed_const "op ="
   1.218        in
   1.219 -	  (Predicate(equal_name,arg_typ,args'),
   1.220 +	  (Predicate(equal_name,[arg_typ],args'),
   1.221  	   union_all ts, 
   1.222  	   [((make_fixed_var equal_name), 2)], 
   1.223  	   union_all funcs)
   1.224        end
   1.225    | pred_of (pred,args) = 
   1.226        let val (predName,(predType,ts1), pfuncs) = pred_name_type pred
   1.227 -	  val (args',ts_funcs) = ListPair.unzip (map term_of args)
   1.228 -	  val (ts2,ffuncs) = ListPair.unzip ts_funcs
   1.229 +	  val (args',(ts2,ffuncs)) = terms_of args
   1.230  	  val ts3 = union_all (ts1::ts2)
   1.231  	  val ffuncs' = union_all ffuncs
   1.232  	  val newfuncs = pfuncs union ffuncs'
   1.233  	  val arity = 
   1.234  	    case pred of
   1.235 -		Const (c,_) => 
   1.236 -		      if !keep_types andalso not (no_types_needed c)
   1.237 -		      then 1 + length args
   1.238 -		      else length args
   1.239 +		Const (c,T) => num_typargs(c,T) + length args
   1.240  	      | _ => length args
   1.241        in
   1.242  	  (Predicate(predName,predType,args'), ts3, 
   1.243 @@ -692,7 +673,8 @@
   1.244  
   1.245  fun wrap_eq_type typ t = eq_typ_wrapper ^"(" ^ t ^ "," ^ typ ^ ")";
   1.246  
   1.247 -(* Only need to wrap equality's arguments with "typeinfo" if the output clauses are typed && if we specifically ask for types to be included.   *)
   1.248 +(*Only need to wrap equality's arguments with "typeinfo" if the output clauses are typed 
   1.249 + and if we specifically ask for types to be included.   *)
   1.250  fun string_of_equality (typ,terms) =
   1.251        let val [tstr1,tstr2] = map string_of_term terms
   1.252        in
   1.253 @@ -702,27 +684,19 @@
   1.254  	  else "equal(" ^ tstr1 ^ "," ^ tstr2 ^ ")"
   1.255        end
   1.256  and string_of_term (UVar(x,_)) = x
   1.257 -  | string_of_term (Fun("equal",typ,terms)) = string_of_equality(typ,terms)
   1.258 -  | string_of_term (Fun (name,typ,[])) = name
   1.259 -  | string_of_term (Fun (name,typ,terms)) = 
   1.260 -      let val terms' = map string_of_term terms
   1.261 -      in
   1.262 -	  if !keep_types andalso typ<>"" 
   1.263 -	  then name ^ (paren_pack (terms' @ [typ]))
   1.264 -	  else name ^ (paren_pack terms')
   1.265 -      end;
   1.266 +  | string_of_term (Fun("equal",[typ],terms)) = string_of_equality(typ,terms)
   1.267 +  | string_of_term (Fun (name,typs,[])) = name (*Overloaded consts like 0 don't get types!*)
   1.268 +  | string_of_term (Fun (name,typs,terms)) = 
   1.269 +      let val terms_as_strings = map string_of_term terms
   1.270 +      in  name ^ (paren_pack (terms_as_strings @ typs))  end
   1.271 +  | string_of_term _ = error "string_of_term";      
   1.272  
   1.273  (* before output the string of the predicate, check if the predicate corresponds to an equality or not. *)
   1.274 -fun string_of_predicate (Predicate("equal",typ,terms)) = 
   1.275 -      string_of_equality(typ,terms)
   1.276 -  | string_of_predicate (Predicate(name,_,[])) = name 
   1.277 -  | string_of_predicate (Predicate(name,typ,terms)) = 
   1.278 +fun string_of_predicate (Predicate("equal",[typ],terms)) = string_of_equality(typ,terms)
   1.279 +  | string_of_predicate (Predicate(name,typs,terms)) = 
   1.280        let val terms_as_strings = map string_of_term terms
   1.281 -      in
   1.282 -	  if !keep_types andalso typ<>""
   1.283 -	  then name ^ (paren_pack (terms_as_strings @ [typ]))
   1.284 -	  else name ^ (paren_pack terms_as_strings) 
   1.285 -      end;
   1.286 +      in  name ^ (paren_pack (terms_as_strings @ typs))  end
   1.287 +  | string_of_predicate _ = error "string_of_predicate";      
   1.288  
   1.289  
   1.290  fun string_of_clausename (cls_id,ax_name) = 
   1.291 @@ -781,10 +755,8 @@
   1.292  
   1.293  
   1.294  fun dfg_folterms (Literal(pol,pred,tag)) = 
   1.295 -  let val Predicate (predname, foltype, folterms) = pred
   1.296 -  in
   1.297 -      folterms
   1.298 -  end
   1.299 +  let val Predicate (predname, _, folterms) = pred
   1.300 +  in  folterms  end
   1.301  
   1.302   
   1.303  fun get_uvars (UVar(a,typ)) = [a] 
   1.304 @@ -797,12 +769,9 @@
   1.305  fun uvar_name (UVar(a,_)) = a
   1.306  |   uvar_name (Fun (a,_,_)) = raise CLAUSE("Not a variable", Const(a,dummyT));
   1.307  
   1.308 -fun mergelist [] = []
   1.309 -|   mergelist (x::xs) = x @ mergelist xs
   1.310 -
   1.311  fun dfg_vars (Clause cls) =
   1.312      let val lits = #literals cls
   1.313 -        val folterms = mergelist(map dfg_folterms lits)
   1.314 +        val folterms = List.concat (map dfg_folterms lits)
   1.315      in 
   1.316          union_all(map get_uvars folterms)
   1.317      end
   1.318 @@ -813,24 +782,10 @@
   1.319  
   1.320  	
   1.321  (* make this return funcs and preds too? *)
   1.322 -fun string_of_predname (Predicate("equal",typ,terms)) = "EQUALITY"
   1.323 -  | string_of_predname (Predicate(name,_,[])) = name 
   1.324 -  | string_of_predname (Predicate(name,typ,terms)) = name
   1.325 +fun string_of_predname (Predicate("equal",_,terms)) = "EQUALITY"
   1.326 +  | string_of_predname (Predicate(name,_,terms)) = name
   1.327      
   1.328  	
   1.329 -(* make this return funcs and preds too? *)
   1.330 -
   1.331 -fun string_of_predicate (Predicate("equal",typ,terms)) =  
   1.332 -      string_of_equality(typ,terms)
   1.333 -  | string_of_predicate (Predicate(name,_,[])) = name 
   1.334 -  | string_of_predicate (Predicate(name,typ,terms)) = 
   1.335 -      let val terms_as_strings = map string_of_term terms
   1.336 -      in
   1.337 -	  if !keep_types andalso typ<>""
   1.338 -	  then name ^ (paren_pack  (terms_as_strings @ [typ]))
   1.339 -	  else name ^ (paren_pack terms_as_strings) 
   1.340 -      end;
   1.341 -
   1.342  
   1.343  fun concat_with sep []  = ""
   1.344    | concat_with sep [x] = "(" ^ x ^ ")"
   1.345 @@ -959,7 +914,7 @@
   1.346  (*FIXME!!! currently is TPTP format!*)
   1.347  fun dfg_of_arLit (TConsLit(b,(c,t,args))) =
   1.348        let val pol = if b then "++" else "--"
   1.349 -	  val arg_strs = (case args of [] => "" | _ => paren_pack args)
   1.350 +	  val arg_strs = paren_pack args
   1.351        in 
   1.352  	  pol ^ c ^ "(" ^ t ^ arg_strs ^ ")"
   1.353        end
   1.354 @@ -1004,8 +959,6 @@
   1.355  	tagged_pol ^ pred_string
   1.356      end;
   1.357  
   1.358 -
   1.359 -
   1.360  fun tptp_of_typeLit (LTVar x) = "--" ^ x
   1.361    | tptp_of_typeLit (LTFree x) = "++" ^ x;
   1.362   
   1.363 @@ -1067,7 +1020,7 @@
   1.364  
   1.365  fun tptp_of_arLit (TConsLit(b,(c,t,args))) =
   1.366        let val pol = if b then "++" else "--"
   1.367 -	  val  arg_strs = (case args of [] => "" | _ => paren_pack args)
   1.368 +	  val  arg_strs = paren_pack args
   1.369        in 
   1.370  	  pol ^ c ^ "(" ^ t ^ arg_strs ^ ")"
   1.371        end
   1.372 @@ -1110,6 +1063,4 @@
   1.373  	"input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ")."
   1.374      end; 
   1.375  
   1.376 -
   1.377 -
   1.378  end;