src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
changeset 35865 2f8fb5242799
parent 35827 f552152d7747
child 35963 943e2582dc87
     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 -