1.1 --- a/src/HOL/Tools/res_clause.ML Wed Jul 27 11:28:18 2005 +0200
1.2 +++ b/src/HOL/Tools/res_clause.ML Wed Jul 27 11:30:34 2005 +0200
1.3 @@ -12,20 +12,18 @@
1.4 exception CLAUSE of string
1.5 type arityClause
1.6 type classrelClause
1.7 - val classrelClauses_of :
1.8 - string * string list -> classrelClause list
1.9 + val classrelClauses_of : string * string list -> classrelClause list
1.10 type clause
1.11 + val init : theory -> unit
1.12 val keep_types : bool ref
1.13 val make_axiom_arity_clause :
1.14 string * (string * string list list) -> arityClause
1.15 val make_axiom_classrelClause :
1.16 string * string option -> classrelClause
1.17 val make_axiom_clause : Term.term -> string * int -> clause
1.18 - val make_axiom_clause_thm : Thm.thm -> string * int -> clause
1.19 val make_conjecture_clause : Term.term -> clause
1.20 val make_conjecture_clause_thm : Thm.thm -> clause
1.21 val make_hypothesis_clause : Term.term -> clause
1.22 - val make_hypothesis_clause_thm : Thm.thm -> clause
1.23 val special_equal : bool ref
1.24 val tptp_arity_clause : arityClause -> string
1.25 val tptp_classrelClause : classrelClause -> string
1.26 @@ -103,6 +101,11 @@
1.27
1.28 end;
1.29
1.30 +(*Remove the initial ' character from a type variable, if it is present*)
1.31 +fun trim_type_var s =
1.32 + if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
1.33 + else error ("trim_type: Malformed type variable encountered: " ^ s);
1.34 +
1.35 fun ascii_of_indexname (v,0) = ascii_of v
1.36 | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ string_of_int i;
1.37
1.38 @@ -110,8 +113,9 @@
1.39 fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x);
1.40
1.41 (*Type variables contain _H because the character ' translates to that.*)
1.42 -fun make_schematic_type_var v = tvar_prefix ^ (ascii_of_indexname v);
1.43 -fun make_fixed_type_var x = tfree_prefix ^ (ascii_of x);
1.44 +fun make_schematic_type_var (x,i) =
1.45 + tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
1.46 +fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
1.47
1.48 fun make_fixed_const c =
1.49 case Symtab.lookup (const_trans_table,c) of
1.50 @@ -209,6 +213,22 @@
1.51 tvar_type_literals = tvar_type_literals,
1.52 tfree_type_literals = tfree_type_literals};
1.53
1.54 +
1.55 +(*Definitions of the current theory--to allow suppressing types.*)
1.56 +val curr_defs = ref Defs.empty;
1.57 +
1.58 +(*Initialize the type suppression mechanism with the current theory before
1.59 + producing any clauses!*)
1.60 +fun init thy = (curr_defs := Theory.defs_of thy);
1.61 +
1.62 +(*Types aren't needed if the constant has at most one definition and is monomorphic*)
1.63 +fun no_types_needed s =
1.64 + (case Defs.fast_overloading_info (!curr_defs) s of
1.65 + NONE => true
1.66 + | SOME (T,len,_) => len <= 1 andalso null (typ_tvars T))
1.67 +
1.68 +(*Flatten a type to a string while accumulating sort constraints on the TFress and
1.69 + TVars it contains.*)
1.70 fun type_of (Type (a, [])) = (make_fixed_type_const a,[])
1.71 | type_of (Type (a, Ts)) =
1.72 let val foltyps_ts = map type_of Ts
1.73 @@ -220,11 +240,14 @@
1.74 | type_of (TFree (a, s)) = (make_fixed_type_var a, [((FOLTFree a),s)])
1.75 | type_of (TVar (v, s)) = (make_schematic_type_var v, [((FOLTVar v),s)]);
1.76
1.77 +fun maybe_type_of c T =
1.78 + if no_types_needed c then ("",[]) else type_of T;
1.79 +
1.80 (* Any variables created via the METAHYPS tactical should be treated as
1.81 universal vars, although it is represented as "Free(...)" by Isabelle *)
1.82 val isMeta = String.isPrefix "METAHYP1_"
1.83
1.84 -fun pred_name_type (Const(c,T)) = (make_fixed_const c,type_of T)
1.85 +fun pred_name_type (Const(c,T)) = (make_fixed_const c, maybe_type_of c T)
1.86 | pred_name_type (Free(x,T)) =
1.87 if isMeta x then raise CLAUSE("Predicate Not First Order")
1.88 else (make_fixed_var x, type_of T)
1.89 @@ -241,9 +264,7 @@
1.90 folT
1.91 end;
1.92
1.93 -
1.94 -
1.95 -fun fun_name_type (Const(c,T)) = (make_fixed_const c,type_of T)
1.96 +fun fun_name_type (Const(c,T)) = (make_fixed_const c, maybe_type_of c T)
1.97 | fun_name_type (Free(x,T)) = (make_fixed_var x,type_of T)
1.98 | fun_name_type _ = raise CLAUSE("Function Not First Order");
1.99
1.100 @@ -322,30 +343,28 @@
1.101 | _ => pred_of_nonEq (pred,args)
1.102 end;
1.103
1.104 -
1.105
1.106 -fun literals_of_term ((Const("Trueprop",_) $ P),lits_ts) = literals_of_term(P,lits_ts)
1.107 +fun literals_of_term ((Const("Trueprop",_) $ P),lits_ts) = literals_of_term (P,lits_ts)
1.108 | literals_of_term ((Const("op |",_) $ P $ Q),(lits,ts)) =
1.109 - let val (lits',ts') = literals_of_term(P,(lits,ts))
1.110 - in
1.111 - literals_of_term(Q,(lits',ts'))
1.112 - end
1.113 + let val (lits',ts') = literals_of_term (P,(lits,ts))
1.114 + in
1.115 + literals_of_term (Q, (lits',ts'))
1.116 + end
1.117 | literals_of_term ((Const("Not",_) $ P),(lits,ts)) =
1.118 - let val (pred,ts') = predicate_of P
1.119 - val lits' = Literal(false,pred,false) :: lits
1.120 - val ts'' = ResLib.no_rep_app ts ts'
1.121 - in
1.122 - (lits',ts'')
1.123 - end
1.124 + let val (pred,ts') = predicate_of P
1.125 + val lits' = Literal(false,pred,false) :: lits
1.126 + val ts'' = ResLib.no_rep_app ts ts'
1.127 + in
1.128 + (lits',ts'')
1.129 + end
1.130 | literals_of_term (P,(lits,ts)) =
1.131 - let val (pred,ts') = predicate_of P
1.132 - val lits' = Literal(true,pred,false) :: lits
1.133 - val ts'' = ResLib.no_rep_app ts ts'
1.134 - in
1.135 - (lits',ts'')
1.136 - end;
1.137 + let val (pred,ts') = predicate_of P
1.138 + val lits' = Literal(true,pred,false) :: lits
1.139 + val ts'' = ResLib.no_rep_app ts ts'
1.140 + in
1.141 + (lits',ts'')
1.142 + end;
1.143
1.144 -
1.145 fun literals_of_thm thm = literals_of_term (prop_of thm, ([],[]));
1.146
1.147 (*Make literals for sorted type variables*)
1.148 @@ -380,22 +399,7 @@
1.149
1.150
1.151 (** make axiom clauses, hypothesis clauses and conjecture clauses. **)
1.152 -
1.153 -fun make_axiom_clause_thm thm (axname,cls_id)=
1.154 - let val (lits,types_sorts) = literals_of_thm thm
1.155 - val (tvar_lits,tfree_lits) = add_typs_aux types_sorts
1.156 - in
1.157 - make_clause(cls_id,axname,Axiom,lits,types_sorts,tvar_lits,tfree_lits)
1.158 - end;
1.159
1.160 -fun make_hypothesis_clause_thm thm =
1.161 - let val (lits,types_sorts) = literals_of_thm thm
1.162 - val cls_id = generate_id()
1.163 - val (tvar_lits,tfree_lits) = add_typs_aux types_sorts
1.164 - in
1.165 - make_clause(cls_id,"",Hypothesis,lits,types_sorts,tvar_lits,tfree_lits)
1.166 - end;
1.167 -
1.168
1.169 fun make_conjecture_clause_thm thm =
1.170 let val (lits,types_sorts) = literals_of_thm thm
1.171 @@ -549,7 +553,7 @@
1.172 | string_of_term (Fun (name,typ,terms)) =
1.173 let val terms' = map string_of_term terms
1.174 in
1.175 - if (!keep_types) then name ^ (ResLib.list_to_string (terms' @ [typ]))
1.176 + if !keep_types andalso typ<>"" then name ^ (ResLib.list_to_string (terms' @ [typ]))
1.177 else name ^ (ResLib.list_to_string terms')
1.178 end;
1.179
1.180 @@ -563,7 +567,7 @@
1.181 | string_of_predicate (Predicate(name,typ,terms)) =
1.182 let val terms_as_strings = map string_of_term terms
1.183 in
1.184 - if (!keep_types)
1.185 + if !keep_types andalso typ<>""
1.186 then name ^ (ResLib.list_to_string (terms_as_strings @ [typ]))
1.187 else name ^ (ResLib.list_to_string terms_as_strings)
1.188 end;