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;