# HG changeset patch # User paulson # Date 1132650551 -3600 # Node ID 9a7ffce389c310852c1aeefc9bdb180657fd8788 # Parent e0b08c9534ff4047bb1e5996f6e87ecf6f70aad5 new treatment of polymorphic types, using Sign.const_typargs diff -r e0b08c9534ff -r 9a7ffce389c3 src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Mon Nov 21 16:51:57 2005 +0100 +++ b/src/HOL/Tools/res_clause.ML Tue Nov 22 10:09:11 2005 +0100 @@ -143,7 +143,8 @@ end; (* convert a list of strings into one single string; surrounded by brackets *) -fun paren_pack strings = "(" ^ commas strings ^ ")"; +fun paren_pack [] = "" (*empty argument list*) + | paren_pack strings = "(" ^ commas strings ^ ")"; fun bracket_pack strings = "[" ^ commas strings ^ "]"; @@ -159,7 +160,6 @@ fun make_schematic_var v = schematic_var_prefix ^ (ascii_of_indexname v); fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x); -(*Type variables contain _H because the character ' translates to that.*) fun make_schematic_type_var (x,i) = tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i)); fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)); @@ -208,13 +208,11 @@ type sort = Term.sort; type fol_type = string; - datatype type_literal = LTVar of string | LTFree of string; - datatype folTerm = UVar of string * fol_type - | Fun of string * fol_type * folTerm list; -datatype predicate = Predicate of pred_name * fol_type * folTerm list; + | Fun of string * fol_type list * folTerm list; +datatype predicate = Predicate of pred_name * fol_type list * folTerm list; datatype literal = Literal of polarity * predicate * tag; @@ -283,75 +281,73 @@ fun preds_of_cls (Clause cls) = #predicates cls; +(*Declarations of the current theory--to allow suppressing types.*) +val const_typargs = ref (Library.K [] : (string*typ -> typ list)); -(*Declarations of the current theory--to allow suppressing types.*) -val monomorphic = ref (fn (_: string) => false); -fun no_types_needed s = ! monomorphic s; +fun num_typargs(s,T) = if !keep_types then length (!const_typargs (s,T)) else 0; (*Initialize the type suppression mechanism with the current theory before producing any clauses!*) -fun init thy = (monomorphic := Sign.const_monomorphic thy); +fun init thy = (const_typargs := Sign.const_typargs thy); -(*Flatten a type to a string while accumulating sort constraints on the TFress and +(*Flatten a type to a string while accumulating sort constraints on the TFrees and TVars it contains.*) -fun type_of (Type (a, [])) = - let val t = make_fixed_type_const a - in (t,([],[(t,0)])) end - | type_of (Type (a, Ts)) = +fun type_of (Type (a, Ts)) = + let val (folTyps, (ts, funcs)) = types_of Ts + val t = make_fixed_type_const a + in + ((t ^ paren_pack folTyps), (ts, (t, length Ts)::funcs)) + end + | type_of (TFree (a,s)) = + let val t = make_fixed_type_var a + in (t, ([((FOLTFree a),s)], [(t,0)])) end + | type_of (TVar (v, s)) = (make_schematic_type_var v, ([((FOLTVar v),s)], [])) +and types_of Ts = let val foltyps_ts = map type_of Ts val (folTyps,ts_funcs) = ListPair.unzip foltyps_ts val (ts, funcslist) = ListPair.unzip ts_funcs - val ts' = union_all ts - val funcs' = union_all funcslist - val t = make_fixed_type_const a in - ((t ^ paren_pack folTyps), (ts', (t, length Ts)::funcs')) - end - | type_of (TFree (a, s)) = - let val t = make_fixed_type_var a - in (t, ([((FOLTFree a),s)],[(t,0)])) end - | type_of (TVar (v, s)) = (make_schematic_type_var v, ([((FOLTVar v),s)], [])) + (folTyps, (union_all ts, union_all funcslist)) + end; -fun maybe_type_of c T = - if no_types_needed c then ("",([],[])) else type_of T; +fun const_types_of (c,T) = types_of (!const_typargs (c,T)); (* Any variables created via the METAHYPS tactical should be treated as universal vars, although it is represented as "Free(...)" by Isabelle *) val isMeta = String.isPrefix "METAHYP1_" fun pred_name_type (Const(c,T)) = - let val (typof,(folTyps,funcs)) = maybe_type_of c T - in (make_fixed_const c, (typof,folTyps), funcs) end + let val (contys,(folTyps,funcs)) = const_types_of (c,T) + in (make_fixed_const c, (contys,folTyps), funcs) end | pred_name_type (Free(x,T)) = if isMeta x then raise CLAUSE("Predicate Not First Order 1", Free(x,T)) - else (make_fixed_var x, ("",[]), []) + else (make_fixed_var x, ([],[]), []) | pred_name_type (v as Var _) = raise CLAUSE("Predicate Not First Order 2", v) | pred_name_type t = raise CLAUSE("Predicate input unexpected", t); -(* For type equality *) +(* For typed equality *) (* here "arg_typ" is the type of "="'s argument's type, not the type of the equality *) (* Find type of equality arg *) fun eq_arg_type (Type("fun",[T,_])) = let val (folT,_) = type_of T; in folT end; -fun fun_name_type (Const(c,T)) args = +fun fun_name_type (Const("op =",T)) args = (*FIXME: Is this special treatment of = needed??*) + let val t = make_fixed_const "op =" + in (t, ([eq_arg_type T], []), [(t,2)]) end + | fun_name_type (Const(c,T)) args = let val t = make_fixed_const c - val (typof, (folTyps,funcs)) = maybe_type_of c T - val arity = if !keep_types andalso not (no_types_needed c) - then 1 + length args - else length args + val (contys, (folTyps,funcs)) = const_types_of (c,T) + val arity = num_typargs(c,T) + length args in - (t, (typof,folTyps), ((t,arity)::funcs)) + (t, (contys,folTyps), ((t,arity)::funcs)) end | fun_name_type (Free(x,T)) args = let val t = make_fixed_var x - in - (t, ("",[]), [(t, length args)]) - end + in (t, ([],[]), [(t, length args)]) end | fun_name_type f args = raise CLAUSE("Function Not First Order 1", f); @@ -366,72 +362,57 @@ if isMeta x then (UVar(make_schematic_var(x,0),folType), (ts, ((make_schematic_var(x,0)),0)::funcs)) else - (Fun(make_fixed_var x, folType, []), + (Fun(make_fixed_var x, [folType], []), (ts, ((make_fixed_var x),0)::funcs)) end | term_of (Const(c,T)) = (* impossible to be equality *) - let val (folType,(ts,funcs)) = type_of T + let val (contys, (folTyps,funcs)) = const_types_of (c,T) in - (Fun(make_fixed_const c, folType, []), - (ts, ((make_fixed_const c),0)::funcs)) + (Fun(make_fixed_const c, contys, []), + (folTyps, ((make_fixed_const c),0)::funcs)) end - | term_of (app as (t $ a)) = + | term_of app = let val (f,args) = strip_comb app - fun term_of_aux () = - let val (funName,(funType,ts1),funcs) = fun_name_type f args - val (args',ts_funcs) = ListPair.unzip (map term_of args) - val (ts2,funcs') = ListPair.unzip ts_funcs - val ts3 = union_all (ts1::ts2) - val funcs'' = union_all(funcs::funcs') - in - (Fun(funName,funType,args'), (ts3,funcs'')) - end - fun term_of_eq ((Const ("op =", typ)),args) = - let val arg_typ = eq_arg_type typ - val (args',ts_funcs) = ListPair.unzip (map term_of args) - val (ts,funcs) = ListPair.unzip ts_funcs - val equal_name = make_fixed_const ("op =") - in - (Fun(equal_name,arg_typ,args'), - (union_all ts, - (make_fixed_var equal_name, 2):: union_all funcs)) - end + val _ = case f of Const(_,_) => () + | Free(s,_) => + if isMeta s + then raise CLAUSE("Function Not First Order 2", f) + else () + | _ => raise CLAUSE("Function Not First Order 3", f); + val (funName,(contys,ts1),funcs) = fun_name_type f args + val (args',(ts2,funcs')) = terms_of args in - case f of Const ("op =", typ) => term_of_eq (f,args) - | Const(_,_) => term_of_aux () - | Free(s,_) => - if isMeta s - then raise CLAUSE("Function Not First Order 2", f) - else term_of_aux() - | _ => raise CLAUSE("Function Not First Order 3", f) + (Fun(funName,contys,args'), + (union_all (ts1::ts2), + union_all(funcs::funcs'))) end - | term_of t = raise CLAUSE("Function Not First Order 4", t); + | term_of t = raise CLAUSE("Function Not First Order 4", t) +and terms_of ts = + let val (args, ts_funcs) = ListPair.unzip (map term_of ts) + in + (args, ListPair.unzip ts_funcs) + end fun pred_of (Const("op =", typ), args) = let val arg_typ = eq_arg_type typ - val (args',ts_funcs) = ListPair.unzip (map term_of args) - val (ts,funcs) = ListPair.unzip ts_funcs + val (args',(ts,funcs)) = terms_of args val equal_name = make_fixed_const "op =" in - (Predicate(equal_name,arg_typ,args'), + (Predicate(equal_name,[arg_typ],args'), union_all ts, [((make_fixed_var equal_name), 2)], union_all funcs) end | pred_of (pred,args) = let val (predName,(predType,ts1), pfuncs) = pred_name_type pred - val (args',ts_funcs) = ListPair.unzip (map term_of args) - val (ts2,ffuncs) = ListPair.unzip ts_funcs + val (args',(ts2,ffuncs)) = terms_of args val ts3 = union_all (ts1::ts2) val ffuncs' = union_all ffuncs val newfuncs = pfuncs union ffuncs' val arity = case pred of - Const (c,_) => - if !keep_types andalso not (no_types_needed c) - then 1 + length args - else length args + Const (c,T) => num_typargs(c,T) + length args | _ => length args in (Predicate(predName,predType,args'), ts3, @@ -692,7 +673,8 @@ fun wrap_eq_type typ t = eq_typ_wrapper ^"(" ^ t ^ "," ^ typ ^ ")"; -(* Only need to wrap equality's arguments with "typeinfo" if the output clauses are typed && if we specifically ask for types to be included. *) +(*Only need to wrap equality's arguments with "typeinfo" if the output clauses are typed + and if we specifically ask for types to be included. *) fun string_of_equality (typ,terms) = let val [tstr1,tstr2] = map string_of_term terms in @@ -702,27 +684,19 @@ else "equal(" ^ tstr1 ^ "," ^ tstr2 ^ ")" end and string_of_term (UVar(x,_)) = x - | string_of_term (Fun("equal",typ,terms)) = string_of_equality(typ,terms) - | string_of_term (Fun (name,typ,[])) = name - | string_of_term (Fun (name,typ,terms)) = - let val terms' = map string_of_term terms - in - if !keep_types andalso typ<>"" - then name ^ (paren_pack (terms' @ [typ])) - else name ^ (paren_pack terms') - end; + | string_of_term (Fun("equal",[typ],terms)) = string_of_equality(typ,terms) + | string_of_term (Fun (name,typs,[])) = name (*Overloaded consts like 0 don't get types!*) + | string_of_term (Fun (name,typs,terms)) = + let val terms_as_strings = map string_of_term terms + in name ^ (paren_pack (terms_as_strings @ typs)) end + | string_of_term _ = error "string_of_term"; (* before output the string of the predicate, check if the predicate corresponds to an equality or not. *) -fun string_of_predicate (Predicate("equal",typ,terms)) = - string_of_equality(typ,terms) - | string_of_predicate (Predicate(name,_,[])) = name - | string_of_predicate (Predicate(name,typ,terms)) = +fun string_of_predicate (Predicate("equal",[typ],terms)) = string_of_equality(typ,terms) + | string_of_predicate (Predicate(name,typs,terms)) = let val terms_as_strings = map string_of_term terms - in - if !keep_types andalso typ<>"" - then name ^ (paren_pack (terms_as_strings @ [typ])) - else name ^ (paren_pack terms_as_strings) - end; + in name ^ (paren_pack (terms_as_strings @ typs)) end + | string_of_predicate _ = error "string_of_predicate"; fun string_of_clausename (cls_id,ax_name) = @@ -781,10 +755,8 @@ fun dfg_folterms (Literal(pol,pred,tag)) = - let val Predicate (predname, foltype, folterms) = pred - in - folterms - end + let val Predicate (predname, _, folterms) = pred + in folterms end fun get_uvars (UVar(a,typ)) = [a] @@ -797,12 +769,9 @@ fun uvar_name (UVar(a,_)) = a | uvar_name (Fun (a,_,_)) = raise CLAUSE("Not a variable", Const(a,dummyT)); -fun mergelist [] = [] -| mergelist (x::xs) = x @ mergelist xs - fun dfg_vars (Clause cls) = let val lits = #literals cls - val folterms = mergelist(map dfg_folterms lits) + val folterms = List.concat (map dfg_folterms lits) in union_all(map get_uvars folterms) end @@ -813,24 +782,10 @@ (* make this return funcs and preds too? *) -fun string_of_predname (Predicate("equal",typ,terms)) = "EQUALITY" - | string_of_predname (Predicate(name,_,[])) = name - | string_of_predname (Predicate(name,typ,terms)) = name +fun string_of_predname (Predicate("equal",_,terms)) = "EQUALITY" + | string_of_predname (Predicate(name,_,terms)) = name -(* make this return funcs and preds too? *) - -fun string_of_predicate (Predicate("equal",typ,terms)) = - string_of_equality(typ,terms) - | string_of_predicate (Predicate(name,_,[])) = name - | string_of_predicate (Predicate(name,typ,terms)) = - let val terms_as_strings = map string_of_term terms - in - if !keep_types andalso typ<>"" - then name ^ (paren_pack (terms_as_strings @ [typ])) - else name ^ (paren_pack terms_as_strings) - end; - fun concat_with sep [] = "" | concat_with sep [x] = "(" ^ x ^ ")" @@ -959,7 +914,7 @@ (*FIXME!!! currently is TPTP format!*) fun dfg_of_arLit (TConsLit(b,(c,t,args))) = let val pol = if b then "++" else "--" - val arg_strs = (case args of [] => "" | _ => paren_pack args) + val arg_strs = paren_pack args in pol ^ c ^ "(" ^ t ^ arg_strs ^ ")" end @@ -1004,8 +959,6 @@ tagged_pol ^ pred_string end; - - fun tptp_of_typeLit (LTVar x) = "--" ^ x | tptp_of_typeLit (LTFree x) = "++" ^ x; @@ -1067,7 +1020,7 @@ fun tptp_of_arLit (TConsLit(b,(c,t,args))) = let val pol = if b then "++" else "--" - val arg_strs = (case args of [] => "" | _ => paren_pack args) + val arg_strs = paren_pack args in pol ^ c ^ "(" ^ t ^ arg_strs ^ ")" end @@ -1110,6 +1063,4 @@ "input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ")." end; - - end;