1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Fri Mar 19 06:14:37 2010 +0100
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Fri Mar 19 13:02:18 2010 +0100
1.3 @@ -6,67 +6,54 @@
1.4
1.5 signature SLEDGEHAMMER_HOL_CLAUSE =
1.6 sig
1.7 - val ext: thm
1.8 - val comb_I: thm
1.9 - val comb_K: thm
1.10 - val comb_B: thm
1.11 - val comb_C: thm
1.12 - val comb_S: thm
1.13 - val minimize_applies: bool
1.14 + type kind = Sledgehammer_FOL_Clause.kind
1.15 + type fol_type = Sledgehammer_FOL_Clause.fol_type
1.16 + type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
1.17 + type arity_clause = Sledgehammer_FOL_Clause.arity_clause
1.18 type axiom_name = string
1.19 type polarity = bool
1.20 - type clause_id = int
1.21 + type hol_clause_id = int
1.22 +
1.23 datatype combterm =
1.24 - CombConst of string * Sledgehammer_FOL_Clause.fol_type * Sledgehammer_FOL_Clause.fol_type list (*Const and Free*)
1.25 - | CombVar of string * Sledgehammer_FOL_Clause.fol_type
1.26 - | CombApp of combterm * combterm
1.27 + CombConst of string * fol_type * fol_type list (* Const and Free *) |
1.28 + CombVar of string * fol_type |
1.29 + CombApp of combterm * combterm
1.30 datatype literal = Literal of polarity * combterm
1.31 - datatype clause = Clause of {clause_id: clause_id, axiom_name: axiom_name, th: thm,
1.32 - kind: Sledgehammer_FOL_Clause.kind,literals: literal list, ctypes_sorts: typ list}
1.33 - val type_of_combterm: combterm -> Sledgehammer_FOL_Clause.fol_type
1.34 - val strip_comb: combterm -> combterm * combterm list
1.35 - val literals_of_term: theory -> term -> literal list * typ list
1.36 - exception TOO_TRIVIAL
1.37 - val make_conjecture_clauses: bool -> theory -> thm list -> clause list
1.38 - val make_axiom_clauses: bool ->
1.39 - theory ->
1.40 - (thm * (axiom_name * clause_id)) list -> (axiom_name * clause) list
1.41 - val get_helper_clauses: bool ->
1.42 - theory ->
1.43 - bool ->
1.44 - clause list * (thm * (axiom_name * clause_id)) list * string list ->
1.45 - clause list
1.46 - val tptp_write_file: bool -> Path.T ->
1.47 - clause list * clause list * clause list * clause list *
1.48 - Sledgehammer_FOL_Clause.classrelClause list * Sledgehammer_FOL_Clause.arityClause list ->
1.49 + datatype hol_clause =
1.50 + HOLClause of {clause_id: hol_clause_id, axiom_name: axiom_name, th: thm,
1.51 + kind: kind, literals: literal list, ctypes_sorts: typ list}
1.52 +
1.53 + val type_of_combterm : combterm -> fol_type
1.54 + val strip_combterm_comb : combterm -> combterm * combterm list
1.55 + val literals_of_term : theory -> term -> literal list * typ list
1.56 + exception TRIVIAL
1.57 + val make_conjecture_clauses : bool -> theory -> thm list -> hol_clause list
1.58 + val make_axiom_clauses : bool -> theory ->
1.59 + (thm * (axiom_name * hol_clause_id)) list -> (axiom_name * hol_clause) list
1.60 + val get_helper_clauses : bool -> theory -> bool ->
1.61 + hol_clause list * (thm * (axiom_name * hol_clause_id)) list * string list ->
1.62 + hol_clause list
1.63 + val write_tptp_file : bool -> Path.T ->
1.64 + hol_clause list * hol_clause list * hol_clause list * hol_clause list *
1.65 + classrel_clause list * arity_clause list ->
1.66 int * int
1.67 - val dfg_write_file: bool -> Path.T ->
1.68 - clause list * clause list * clause list * clause list *
1.69 - Sledgehammer_FOL_Clause.classrelClause list * Sledgehammer_FOL_Clause.arityClause list ->
1.70 - int * int
1.71 + val write_dfg_file : bool -> Path.T ->
1.72 + hol_clause list * hol_clause list * hol_clause list * hol_clause list *
1.73 + classrel_clause list * arity_clause list -> int * int
1.74 end
1.75
1.76 structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
1.77 struct
1.78
1.79 -structure SFC = Sledgehammer_FOL_Clause;
1.80 -
1.81 -(* theorems for combinators and function extensionality *)
1.82 -val ext = thm "HOL.ext";
1.83 -val comb_I = thm "Sledgehammer.COMBI_def";
1.84 -val comb_K = thm "Sledgehammer.COMBK_def";
1.85 -val comb_B = thm "Sledgehammer.COMBB_def";
1.86 -val comb_C = thm "Sledgehammer.COMBC_def";
1.87 -val comb_S = thm "Sledgehammer.COMBS_def";
1.88 -val fequal_imp_equal = thm "Sledgehammer.fequal_imp_equal";
1.89 -val equal_imp_fequal = thm "Sledgehammer.equal_imp_fequal";
1.90 -
1.91 +open Sledgehammer_FOL_Clause
1.92 +open Sledgehammer_Fact_Preprocessor
1.93
1.94 (* Parameter t_full below indicates that full type information is to be
1.95 exported *)
1.96
1.97 -(*If true, each function will be directly applied to as many arguments as possible, avoiding
1.98 - use of the "apply" operator. Use of hBOOL is also minimized.*)
1.99 +(* If true, each function will be directly applied to as many arguments as
1.100 + possible, avoiding use of the "apply" operator. Use of hBOOL is also
1.101 + minimized. *)
1.102 val minimize_applies = true;
1.103
1.104 fun min_arity_of const_min_arity c = the_default 0 (Symtab.lookup const_min_arity c);
1.105 @@ -84,21 +71,18 @@
1.106
1.107 type axiom_name = string;
1.108 type polarity = bool;
1.109 -type clause_id = int;
1.110 +type hol_clause_id = int;
1.111
1.112 -datatype combterm = CombConst of string * SFC.fol_type * SFC.fol_type list (*Const and Free*)
1.113 - | CombVar of string * SFC.fol_type
1.114 - | CombApp of combterm * combterm
1.115 +datatype combterm =
1.116 + CombConst of string * fol_type * fol_type list (* Const and Free *) |
1.117 + CombVar of string * fol_type |
1.118 + CombApp of combterm * combterm
1.119
1.120 datatype literal = Literal of polarity * combterm;
1.121
1.122 -datatype clause =
1.123 - Clause of {clause_id: clause_id,
1.124 - axiom_name: axiom_name,
1.125 - th: thm,
1.126 - kind: SFC.kind,
1.127 - literals: literal list,
1.128 - ctypes_sorts: typ list};
1.129 +datatype hol_clause =
1.130 + HOLClause of {clause_id: hol_clause_id, axiom_name: axiom_name, th: thm,
1.131 + kind: kind, literals: literal list, ctypes_sorts: typ list};
1.132
1.133
1.134 (*********************************************************************)
1.135 @@ -106,8 +90,7 @@
1.136 (*********************************************************************)
1.137
1.138 fun isFalse (Literal(pol, CombConst(c,_,_))) =
1.139 - (pol andalso c = "c_False") orelse
1.140 - (not pol andalso c = "c_True")
1.141 + (pol andalso c = "c_False") orelse (not pol andalso c = "c_True")
1.142 | isFalse _ = false;
1.143
1.144 fun isTrue (Literal (pol, CombConst(c,_,_))) =
1.145 @@ -115,24 +98,22 @@
1.146 (not pol andalso c = "c_False")
1.147 | isTrue _ = false;
1.148
1.149 -fun isTaut (Clause {literals,...}) = exists isTrue literals;
1.150 +fun isTaut (HOLClause {literals,...}) = exists isTrue literals;
1.151
1.152 fun type_of dfg (Type (a, Ts)) =
1.153 let val (folTypes,ts) = types_of dfg Ts
1.154 - in (SFC.Comp(SFC.make_fixed_type_const dfg a, folTypes), ts) end
1.155 - | type_of _ (tp as TFree (a, _)) =
1.156 - (SFC.AtomF (SFC.make_fixed_type_var a), [tp])
1.157 - | type_of _ (tp as TVar (v, _)) =
1.158 - (SFC.AtomV (SFC.make_schematic_type_var v), [tp])
1.159 + in (Comp(make_fixed_type_const dfg a, folTypes), ts) end
1.160 + | type_of _ (tp as TFree (a, _)) = (AtomF (make_fixed_type_var a), [tp])
1.161 + | type_of _ (tp as TVar (v, _)) = (AtomV (make_schematic_type_var v), [tp])
1.162 and types_of dfg Ts =
1.163 let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
1.164 - in (folTyps, SFC.union_all ts) end;
1.165 + in (folTyps, union_all ts) end;
1.166
1.167 (* same as above, but no gathering of sort information *)
1.168 fun simp_type_of dfg (Type (a, Ts)) =
1.169 - SFC.Comp(SFC.make_fixed_type_const dfg a, map (simp_type_of dfg) Ts)
1.170 - | simp_type_of _ (TFree (a, _)) = SFC.AtomF(SFC.make_fixed_type_var a)
1.171 - | simp_type_of _ (TVar (v, _)) = SFC.AtomV(SFC.make_schematic_type_var v);
1.172 + Comp(make_fixed_type_const dfg a, map (simp_type_of dfg) Ts)
1.173 + | simp_type_of _ (TFree (a, _)) = AtomF (make_fixed_type_var a)
1.174 + | simp_type_of _ (TVar (v, _)) = AtomV (make_schematic_type_var v);
1.175
1.176
1.177 fun const_type_of dfg thy (c,t) =
1.178 @@ -142,27 +123,27 @@
1.179 (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
1.180 fun combterm_of dfg thy (Const(c,t)) =
1.181 let val (tp,ts,tvar_list) = const_type_of dfg thy (c,t)
1.182 - val c' = CombConst(SFC.make_fixed_const dfg c, tp, tvar_list)
1.183 + val c' = CombConst(make_fixed_const dfg c, tp, tvar_list)
1.184 in (c',ts) end
1.185 | combterm_of dfg _ (Free(v,t)) =
1.186 let val (tp,ts) = type_of dfg t
1.187 - val v' = CombConst(SFC.make_fixed_var v, tp, [])
1.188 + val v' = CombConst(make_fixed_var v, tp, [])
1.189 in (v',ts) end
1.190 | combterm_of dfg _ (Var(v,t)) =
1.191 let val (tp,ts) = type_of dfg t
1.192 - val v' = CombVar(SFC.make_schematic_var v,tp)
1.193 + val v' = CombVar(make_schematic_var v,tp)
1.194 in (v',ts) end
1.195 | combterm_of dfg thy (P $ Q) =
1.196 let val (P',tsP) = combterm_of dfg thy P
1.197 val (Q',tsQ) = combterm_of dfg thy Q
1.198 in (CombApp(P',Q'), union (op =) tsP tsQ) end
1.199 - | combterm_of _ _ (t as Abs _) = raise SFC.CLAUSE ("HOL CLAUSE", t);
1.200 + | combterm_of _ _ (t as Abs _) = raise CLAUSE ("HOL CLAUSE", t);
1.201
1.202 -fun predicate_of dfg thy ((Const("Not",_) $ P), polarity) = predicate_of dfg thy (P, not polarity)
1.203 +fun predicate_of dfg thy ((@{const Not} $ P), polarity) = predicate_of dfg thy (P, not polarity)
1.204 | predicate_of dfg thy (t,polarity) = (combterm_of dfg thy (Envir.eta_contract t), polarity);
1.205
1.206 -fun literals_of_term1 dfg thy args (Const("Trueprop",_) $ P) = literals_of_term1 dfg thy args P
1.207 - | literals_of_term1 dfg thy args (Const("op |",_) $ P $ Q) =
1.208 +fun literals_of_term1 dfg thy args (@{const Trueprop} $ P) = literals_of_term1 dfg thy args P
1.209 + | literals_of_term1 dfg thy args (@{const "op |"} $ P $ Q) =
1.210 literals_of_term1 dfg thy (literals_of_term1 dfg thy args P) Q
1.211 | literals_of_term1 dfg thy (lits,ts) P =
1.212 let val ((pred,ts'),pol) = predicate_of dfg thy (P,true)
1.213 @@ -173,23 +154,23 @@
1.214 fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P;
1.215 val literals_of_term = literals_of_term_dfg false;
1.216
1.217 -(* Problem too trivial for resolution (empty clause) *)
1.218 -exception TOO_TRIVIAL;
1.219 +(* Trivial problem, which resolution cannot handle (empty clause) *)
1.220 +exception TRIVIAL;
1.221
1.222 (* making axiom and conjecture clauses *)
1.223 -fun make_clause dfg thy (clause_id,axiom_name,kind,th) =
1.224 +fun make_clause dfg thy (clause_id, axiom_name, kind, th) =
1.225 let val (lits,ctypes_sorts) = literals_of_term_dfg dfg thy (prop_of th)
1.226 in
1.227 - if forall isFalse lits
1.228 - then raise TOO_TRIVIAL
1.229 + if forall isFalse lits then
1.230 + raise TRIVIAL
1.231 else
1.232 - Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, kind = kind,
1.233 - literals = lits, ctypes_sorts = ctypes_sorts}
1.234 + HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
1.235 + kind = kind, literals = lits, ctypes_sorts = ctypes_sorts}
1.236 end;
1.237
1.238
1.239 fun add_axiom_clause dfg thy ((th,(name,id)), pairs) =
1.240 - let val cls = make_clause dfg thy (id, name, SFC.Axiom, th)
1.241 + let val cls = make_clause dfg thy (id, name, Axiom, th)
1.242 in
1.243 if isTaut cls then pairs else (name,cls)::pairs
1.244 end;
1.245 @@ -198,7 +179,7 @@
1.246
1.247 fun make_conjecture_clauses_aux _ _ _ [] = []
1.248 | make_conjecture_clauses_aux dfg thy n (th::ths) =
1.249 - make_clause dfg thy (n,"conjecture", SFC.Conjecture, th) ::
1.250 + make_clause dfg thy (n,"conjecture", Conjecture, th) ::
1.251 make_conjecture_clauses_aux dfg thy (n+1) ths;
1.252
1.253 fun make_conjecture_clauses dfg thy = make_conjecture_clauses_aux dfg thy 0;
1.254 @@ -211,7 +192,7 @@
1.255 (**********************************************************************)
1.256
1.257 (*Result of a function type; no need to check that the argument type matches.*)
1.258 -fun result_type (SFC.Comp ("tc_fun", [_, tp2])) = tp2
1.259 +fun result_type (Comp ("tc_fun", [_, tp2])) = tp2
1.260 | result_type _ = error "result_type"
1.261
1.262 fun type_of_combterm (CombConst (_, tp, _)) = tp
1.263 @@ -219,7 +200,7 @@
1.264 | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1);
1.265
1.266 (*gets the head of a combinator application, along with the list of arguments*)
1.267 -fun strip_comb u =
1.268 +fun strip_combterm_comb u =
1.269 let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
1.270 | stripc x = x
1.271 in stripc(u,[]) end;
1.272 @@ -231,10 +212,10 @@
1.273
1.274 fun wrap_type t_full (s, tp) =
1.275 if t_full then
1.276 - type_wrapper ^ SFC.paren_pack [s, SFC.string_of_fol_type tp]
1.277 + type_wrapper ^ paren_pack [s, string_of_fol_type tp]
1.278 else s;
1.279
1.280 -fun apply ss = "hAPP" ^ SFC.paren_pack ss;
1.281 +fun apply ss = "hAPP" ^ paren_pack ss;
1.282
1.283 fun rev_apply (v, []) = v
1.284 | rev_apply (v, arg::args) = apply [rev_apply (v, args), arg];
1.285 @@ -251,10 +232,9 @@
1.286 Int.toString nargs ^ " but is applied to " ^
1.287 space_implode ", " args)
1.288 val args2 = List.drop(args, nargs)
1.289 - val targs = if not t_full then map SFC.string_of_fol_type tvars
1.290 - else []
1.291 + val targs = if not t_full then map string_of_fol_type tvars else []
1.292 in
1.293 - string_apply (c ^ SFC.paren_pack (args1@targs), args2)
1.294 + string_apply (c ^ paren_pack (args1@targs), args2)
1.295 end
1.296 | string_of_applic _ _ (CombVar (v, _), args) = string_apply (v, args)
1.297 | string_of_applic _ _ _ = error "string_of_applic";
1.298 @@ -263,7 +243,7 @@
1.299 if head_needs_hBOOL cnh head then wrap_type t_full (s, tp) else s;
1.300
1.301 fun string_of_combterm (params as (t_full, cma, cnh)) t =
1.302 - let val (head, args) = strip_comb t
1.303 + let val (head, args) = strip_combterm_comb t
1.304 in wrap_type_if t_full cnh (head,
1.305 string_of_applic t_full cma (head, map (string_of_combterm (params)) args),
1.306 type_of_combterm t)
1.307 @@ -271,15 +251,15 @@
1.308
1.309 (*Boolean-valued terms are here converted to literals.*)
1.310 fun boolify params t =
1.311 - "hBOOL" ^ SFC.paren_pack [string_of_combterm params t];
1.312 + "hBOOL" ^ paren_pack [string_of_combterm params t];
1.313
1.314 fun string_of_predicate (params as (_,_,cnh)) t =
1.315 case t of
1.316 (CombApp(CombApp(CombConst("equal",_,_), t1), t2)) =>
1.317 (*DFG only: new TPTP prefers infix equality*)
1.318 - ("equal" ^ SFC.paren_pack [string_of_combterm params t1, string_of_combterm params t2])
1.319 + ("equal" ^ paren_pack [string_of_combterm params t1, string_of_combterm params t2])
1.320 | _ =>
1.321 - case #1 (strip_comb t) of
1.322 + case #1 (strip_combterm_comb t) of
1.323 CombConst(c,_,_) => if needs_hBOOL cnh c then boolify params t else string_of_combterm params t
1.324 | _ => boolify params t;
1.325
1.326 @@ -290,31 +270,31 @@
1.327 let val eqop = if pol then " = " else " != "
1.328 in string_of_combterm params t1 ^ eqop ^ string_of_combterm params t2 end;
1.329
1.330 -fun tptp_literal params (Literal(pol, CombApp(CombApp(CombConst("equal",_,_), t1), t2))) =
1.331 +fun tptp_literal params (Literal(pol, CombApp(CombApp(CombConst("equal", _, _), t1), t2))) =
1.332 tptp_of_equality params pol (t1,t2)
1.333 | tptp_literal params (Literal(pol,pred)) =
1.334 - SFC.tptp_sign pol (string_of_predicate params pred);
1.335 + tptp_sign pol (string_of_predicate params pred);
1.336
1.337 (*Given a clause, returns its literals paired with a list of literals concerning TFrees;
1.338 the latter should only occur in conjecture clauses.*)
1.339 -fun tptp_type_lits params pos (Clause{literals, ctypes_sorts, ...}) =
1.340 +fun tptp_type_lits params pos (HOLClause {literals, ctypes_sorts, ...}) =
1.341 (map (tptp_literal params) literals,
1.342 - map (SFC.tptp_of_typeLit pos) (SFC.add_typs ctypes_sorts));
1.343 + map (tptp_of_typeLit pos) (add_typs ctypes_sorts));
1.344
1.345 -fun clause2tptp params (cls as Clause {axiom_name, clause_id, kind, ...}) =
1.346 - let val (lits,tylits) = tptp_type_lits params (kind = SFC.Conjecture) cls
1.347 +fun clause2tptp params (cls as HOLClause {axiom_name, clause_id, kind, ...}) =
1.348 + let val (lits,tylits) = tptp_type_lits params (kind = Conjecture) cls
1.349 in
1.350 - (SFC.gen_tptp_cls(clause_id,axiom_name,kind,lits,tylits), tylits)
1.351 + (gen_tptp_cls (clause_id, axiom_name, kind, lits, tylits), tylits)
1.352 end;
1.353
1.354
1.355 (*** dfg format ***)
1.356
1.357 -fun dfg_literal params (Literal(pol,pred)) = SFC.dfg_sign pol (string_of_predicate params pred);
1.358 +fun dfg_literal params (Literal(pol,pred)) = dfg_sign pol (string_of_predicate params pred);
1.359
1.360 -fun dfg_type_lits params pos (Clause{literals, ctypes_sorts, ...}) =
1.361 +fun dfg_type_lits params pos (HOLClause {literals, ctypes_sorts, ...}) =
1.362 (map (dfg_literal params) literals,
1.363 - map (SFC.dfg_of_typeLit pos) (SFC.add_typs ctypes_sorts));
1.364 + map (dfg_of_typeLit pos) (add_typs ctypes_sorts));
1.365
1.366 fun get_uvars (CombConst _) vars = vars
1.367 | get_uvars (CombVar(v,_)) vars = (v::vars)
1.368 @@ -322,20 +302,21 @@
1.369
1.370 fun get_uvars_l (Literal(_,c)) = get_uvars c [];
1.371
1.372 -fun dfg_vars (Clause {literals,...}) = SFC.union_all (map get_uvars_l literals);
1.373 +fun dfg_vars (HOLClause {literals,...}) = union_all (map get_uvars_l literals);
1.374
1.375 -fun clause2dfg params (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
1.376 - let val (lits,tylits) = dfg_type_lits params (kind = SFC.Conjecture) cls
1.377 +fun clause2dfg params (cls as HOLClause {axiom_name, clause_id, kind,
1.378 + ctypes_sorts, ...}) =
1.379 + let val (lits,tylits) = dfg_type_lits params (kind = Conjecture) cls
1.380 val vars = dfg_vars cls
1.381 - val tvars = SFC.get_tvar_strs ctypes_sorts
1.382 + val tvars = get_tvar_strs ctypes_sorts
1.383 in
1.384 - (SFC.gen_dfg_cls(clause_id, axiom_name, kind, lits, tylits, tvars@vars), tylits)
1.385 + (gen_dfg_cls (clause_id, axiom_name, kind, lits, tylits, tvars@vars), tylits)
1.386 end;
1.387
1.388
1.389 (** For DFG format: accumulate function and predicate declarations **)
1.390
1.391 -fun addtypes tvars tab = List.foldl SFC.add_foltype_funcs tab tvars;
1.392 +fun addtypes tvars tab = List.foldl add_foltype_funcs tab tvars;
1.393
1.394 fun add_decls (t_full, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) =
1.395 if c = "equal" then (addtypes tvars funcs, preds)
1.396 @@ -348,33 +329,33 @@
1.397 else (addtypes tvars funcs, addit preds)
1.398 end
1.399 | add_decls _ (CombVar(_,ctp), (funcs,preds)) =
1.400 - (SFC.add_foltype_funcs (ctp,funcs), preds)
1.401 + (add_foltype_funcs (ctp,funcs), preds)
1.402 | add_decls params (CombApp(P,Q),decls) = add_decls params (P,add_decls params (Q,decls));
1.403
1.404 -fun add_literal_decls params (Literal(_,c), decls) = add_decls params (c,decls);
1.405 +fun add_literal_decls params (Literal (_,c), decls) = add_decls params (c,decls);
1.406
1.407 -fun add_clause_decls params (Clause {literals, ...}, decls) =
1.408 +fun add_clause_decls params (HOLClause {literals, ...}, decls) =
1.409 List.foldl (add_literal_decls params) decls literals
1.410 handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
1.411
1.412 fun decls_of_clauses params clauses arity_clauses =
1.413 - let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) SFC.init_functab)
1.414 + let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) init_functab)
1.415 val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty
1.416 val (functab,predtab) = (List.foldl (add_clause_decls params) (init_functab, init_predtab) clauses)
1.417 in
1.418 - (Symtab.dest (List.foldl SFC.add_arityClause_funcs functab arity_clauses),
1.419 + (Symtab.dest (List.foldl add_arity_clause_funcs functab arity_clauses),
1.420 Symtab.dest predtab)
1.421 end;
1.422
1.423 -fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) =
1.424 - List.foldl SFC.add_type_sort_preds preds ctypes_sorts
1.425 +fun add_clause_preds (HOLClause {ctypes_sorts, ...}, preds) =
1.426 + List.foldl add_type_sort_preds preds ctypes_sorts
1.427 handle Symtab.DUP a => error ("predicate " ^ a ^ " has multiple arities")
1.428
1.429 (*Higher-order clauses have only the predicates hBOOL and type classes.*)
1.430 fun preds_of_clauses clauses clsrel_clauses arity_clauses =
1.431 Symtab.dest
1.432 - (List.foldl SFC.add_classrelClause_preds
1.433 - (List.foldl SFC.add_arityClause_preds
1.434 + (List.foldl add_classrel_clause_preds
1.435 + (List.foldl add_arity_clause_preds
1.436 (List.foldl add_clause_preds Symtab.empty clauses)
1.437 arity_clauses)
1.438 clsrel_clauses)
1.439 @@ -385,9 +366,8 @@
1.440 (**********************************************************************)
1.441
1.442 val init_counters =
1.443 - Symtab.make [("c_COMBI", 0), ("c_COMBK", 0),
1.444 - ("c_COMBB", 0), ("c_COMBC", 0),
1.445 - ("c_COMBS", 0)];
1.446 + Symtab.make [("c_COMBI", 0), ("c_COMBK", 0), ("c_COMBB", 0), ("c_COMBC", 0),
1.447 + ("c_COMBS", 0)];
1.448
1.449 fun count_combterm (CombConst (c, _, _), ct) =
1.450 (case Symtab.lookup ct c of NONE => ct (*no counter*)
1.451 @@ -397,18 +377,18 @@
1.452
1.453 fun count_literal (Literal(_,t), ct) = count_combterm(t,ct);
1.454
1.455 -fun count_clause (Clause{literals,...}, ct) = List.foldl count_literal ct literals;
1.456 +fun count_clause (HOLClause {literals, ...}, ct) =
1.457 + List.foldl count_literal ct literals;
1.458
1.459 -fun count_user_clause user_lemmas (Clause{axiom_name,literals,...}, ct) =
1.460 +fun count_user_clause user_lemmas (HOLClause {axiom_name, literals, ...}, ct) =
1.461 if axiom_name mem_string user_lemmas then List.foldl count_literal ct literals
1.462 else ct;
1.463
1.464 -fun cnf_helper_thms thy =
1.465 - Sledgehammer_Fact_Preprocessor.cnf_rules_pairs thy
1.466 - o map Sledgehammer_Fact_Preprocessor.pairname
1.467 +fun cnf_helper_thms thy = cnf_rules_pairs thy o map pairname
1.468
1.469 fun get_helper_clauses dfg thy isFO (conjectures, axcls, user_lemmas) =
1.470 - if isFO then [] (*first-order*)
1.471 + if isFO then
1.472 + []
1.473 else
1.474 let
1.475 val axclauses = map #2 (make_axiom_clauses dfg thy axcls)
1.476 @@ -416,15 +396,15 @@
1.477 val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses
1.478 fun needed c = the (Symtab.lookup ct c) > 0
1.479 val IK = if needed "c_COMBI" orelse needed "c_COMBK"
1.480 - then cnf_helper_thms thy [comb_I,comb_K]
1.481 + then cnf_helper_thms thy [@{thm COMBI_def}, @{thm COMBK_def}]
1.482 else []
1.483 val BC = if needed "c_COMBB" orelse needed "c_COMBC"
1.484 - then cnf_helper_thms thy [comb_B,comb_C]
1.485 + then cnf_helper_thms thy [@{thm COMBB_def}, @{thm COMBC_def}]
1.486 else []
1.487 - val S = if needed "c_COMBS"
1.488 - then cnf_helper_thms thy [comb_S]
1.489 + val S = if needed "c_COMBS" then cnf_helper_thms thy [@{thm COMBS_def}]
1.490 else []
1.491 - val other = cnf_helper_thms thy [fequal_imp_equal,equal_imp_fequal]
1.492 + val other = cnf_helper_thms thy [@{thm fequal_imp_equal},
1.493 + @{thm equal_imp_fequal}]
1.494 in
1.495 map #2 (make_axiom_clauses dfg thy (other @ IK @ BC @ S))
1.496 end;
1.497 @@ -432,7 +412,7 @@
1.498 (*Find the minimal arity of each function mentioned in the term. Also, note which uses
1.499 are not at top level, to see if hBOOL is needed.*)
1.500 fun count_constants_term toplev t (const_min_arity, const_needs_hBOOL) =
1.501 - let val (head, args) = strip_comb t
1.502 + let val (head, args) = strip_combterm_comb t
1.503 val n = length args
1.504 val (const_min_arity, const_needs_hBOOL) = fold (count_constants_term false) args (const_min_arity, const_needs_hBOOL)
1.505 in
1.506 @@ -451,11 +431,12 @@
1.507 fun count_constants_lit (Literal (_,t)) (const_min_arity, const_needs_hBOOL) =
1.508 count_constants_term true t (const_min_arity, const_needs_hBOOL);
1.509
1.510 -fun count_constants_clause (Clause{literals,...}) (const_min_arity, const_needs_hBOOL) =
1.511 +fun count_constants_clause (HOLClause {literals, ...})
1.512 + (const_min_arity, const_needs_hBOOL) =
1.513 fold count_constants_lit literals (const_min_arity, const_needs_hBOOL);
1.514
1.515 fun display_arity const_needs_hBOOL (c,n) =
1.516 - Sledgehammer_Fact_Preprocessor.trace_msg (fn () => "Constant: " ^ c ^
1.517 + trace_msg (fn () => "Constant: " ^ c ^
1.518 " arity:\t" ^ Int.toString n ^
1.519 (if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else ""));
1.520
1.521 @@ -469,31 +450,31 @@
1.522 in (const_min_arity, const_needs_hBOOL) end
1.523 else (Symtab.empty, Symtab.empty);
1.524
1.525 -(* tptp format *)
1.526 +(* TPTP format *)
1.527
1.528 -fun tptp_write_file t_full file clauses =
1.529 +fun write_tptp_file t_full file clauses =
1.530 let
1.531 val (conjectures, axclauses, _, helper_clauses,
1.532 classrel_clauses, arity_clauses) = clauses
1.533 val (cma, cnh) = count_constants clauses
1.534 val params = (t_full, cma, cnh)
1.535 val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
1.536 - val tfree_clss = map SFC.tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
1.537 + val tfree_clss = map tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
1.538 val _ =
1.539 File.write_list file (
1.540 map (#1 o (clause2tptp params)) axclauses @
1.541 tfree_clss @
1.542 tptp_clss @
1.543 - map SFC.tptp_classrelClause classrel_clauses @
1.544 - map SFC.tptp_arity_clause arity_clauses @
1.545 + map tptp_classrel_clause classrel_clauses @
1.546 + map tptp_arity_clause arity_clauses @
1.547 map (#1 o (clause2tptp params)) helper_clauses)
1.548 in (length axclauses + 1, length tfree_clss + length tptp_clss)
1.549 end;
1.550
1.551
1.552 -(* dfg format *)
1.553 +(* DFG format *)
1.554
1.555 -fun dfg_write_file t_full file clauses =
1.556 +fun write_dfg_file t_full file clauses =
1.557 let
1.558 val (conjectures, axclauses, _, helper_clauses,
1.559 classrel_clauses, arity_clauses) = clauses
1.560 @@ -502,20 +483,20 @@
1.561 val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures)
1.562 and probname = Path.implode (Path.base file)
1.563 val axstrs = map (#1 o (clause2dfg params)) axclauses
1.564 - val tfree_clss = map SFC.dfg_tfree_clause (SFC.union_all tfree_litss)
1.565 + val tfree_clss = map dfg_tfree_clause (union_all tfree_litss)
1.566 val helper_clauses_strs = map (#1 o (clause2dfg params)) helper_clauses
1.567 val (funcs,cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
1.568 and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
1.569 val _ =
1.570 File.write_list file (
1.571 - SFC.string_of_start probname ::
1.572 - SFC.string_of_descrip probname ::
1.573 - SFC.string_of_symbols (SFC.string_of_funcs funcs)
1.574 - (SFC.string_of_preds (cl_preds @ ty_preds)) ::
1.575 + string_of_start probname ::
1.576 + string_of_descrip probname ::
1.577 + string_of_symbols (string_of_funcs funcs)
1.578 + (string_of_preds (cl_preds @ ty_preds)) ::
1.579 "list_of_clauses(axioms,cnf).\n" ::
1.580 axstrs @
1.581 - map SFC.dfg_classrelClause classrel_clauses @
1.582 - map SFC.dfg_arity_clause arity_clauses @
1.583 + map dfg_classrel_clause classrel_clauses @
1.584 + map dfg_arity_clause arity_clauses @
1.585 helper_clauses_strs @
1.586 ["end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"] @
1.587 tfree_clss @
1.588 @@ -530,4 +511,3 @@
1.589 end;
1.590
1.591 end;
1.592 -