src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
changeset 35826 1590abc3d42a
parent 35825 a6aad5a70ed4
child 35827 f552152d7747
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Wed Mar 17 18:16:31 2010 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Wed Mar 17 19:26:05 2010 +0100
     1.3 @@ -1,10 +1,10 @@
     1.4 -(*  Title:      HOL/Tools/res_hol_clause.ML
     1.5 +(*  Title:      HOL/Sledgehammer/sledgehammer_hol_clause.ML
     1.6      Author:     Jia Meng, NICTA
     1.7  
     1.8  FOL clauses translated from HOL formulae.
     1.9  *)
    1.10  
    1.11 -signature RES_HOL_CLAUSE =
    1.12 +signature SLEDGEHAMMER_HOL_CLAUSE =
    1.13  sig
    1.14    val ext: thm
    1.15    val comb_I: thm
    1.16 @@ -17,13 +17,13 @@
    1.17    type polarity = bool
    1.18    type clause_id = int
    1.19    datatype combterm =
    1.20 -      CombConst of string * Res_Clause.fol_type * Res_Clause.fol_type list (*Const and Free*)
    1.21 -    | CombVar of string * Res_Clause.fol_type
    1.22 +      CombConst of string * Sledgehammer_FOL_Clause.fol_type * Sledgehammer_FOL_Clause.fol_type list (*Const and Free*)
    1.23 +    | CombVar of string * Sledgehammer_FOL_Clause.fol_type
    1.24      | CombApp of combterm * combterm
    1.25    datatype literal = Literal of polarity * combterm
    1.26    datatype clause = Clause of {clause_id: clause_id, axiom_name: axiom_name, th: thm,
    1.27 -                    kind: Res_Clause.kind,literals: literal list, ctypes_sorts: typ list}
    1.28 -  val type_of_combterm: combterm -> Res_Clause.fol_type
    1.29 +                    kind: Sledgehammer_FOL_Clause.kind,literals: literal list, ctypes_sorts: typ list}
    1.30 +  val type_of_combterm: combterm -> Sledgehammer_FOL_Clause.fol_type
    1.31    val strip_comb: combterm -> combterm * combterm list
    1.32    val literals_of_term: theory -> term -> literal list * typ list
    1.33    exception TOO_TRIVIAL
    1.34 @@ -38,18 +38,18 @@
    1.35         clause list
    1.36    val tptp_write_file: bool -> Path.T ->
    1.37      clause list * clause list * clause list * clause list *
    1.38 -    Res_Clause.classrelClause list * Res_Clause.arityClause list ->
    1.39 +    Sledgehammer_FOL_Clause.classrelClause list * Sledgehammer_FOL_Clause.arityClause list ->
    1.40      int * int
    1.41    val dfg_write_file: bool -> Path.T ->
    1.42      clause list * clause list * clause list * clause list *
    1.43 -    Res_Clause.classrelClause list * Res_Clause.arityClause list ->
    1.44 +    Sledgehammer_FOL_Clause.classrelClause list * Sledgehammer_FOL_Clause.arityClause list ->
    1.45      int * int
    1.46  end
    1.47  
    1.48 -structure Res_HOL_Clause: RES_HOL_CLAUSE =
    1.49 +structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
    1.50  struct
    1.51  
    1.52 -structure RC = Res_Clause;   (* FIXME avoid structure alias *)
    1.53 +structure SFC = Sledgehammer_FOL_Clause;
    1.54  
    1.55  (* theorems for combinators and function extensionality *)
    1.56  val ext = thm "HOL.ext";
    1.57 @@ -86,8 +86,8 @@
    1.58  type polarity = bool;
    1.59  type clause_id = int;
    1.60  
    1.61 -datatype combterm = CombConst of string * RC.fol_type * RC.fol_type list (*Const and Free*)
    1.62 -                  | CombVar of string * RC.fol_type
    1.63 +datatype combterm = CombConst of string * SFC.fol_type * SFC.fol_type list (*Const and Free*)
    1.64 +                  | CombVar of string * SFC.fol_type
    1.65                    | CombApp of combterm * combterm
    1.66  
    1.67  datatype literal = Literal of polarity * combterm;
    1.68 @@ -96,7 +96,7 @@
    1.69           Clause of {clause_id: clause_id,
    1.70                      axiom_name: axiom_name,
    1.71                      th: thm,
    1.72 -                    kind: RC.kind,
    1.73 +                    kind: SFC.kind,
    1.74                      literals: literal list,
    1.75                      ctypes_sorts: typ list};
    1.76  
    1.77 @@ -119,20 +119,20 @@
    1.78  
    1.79  fun type_of dfg (Type (a, Ts)) =
    1.80        let val (folTypes,ts) = types_of dfg Ts
    1.81 -      in  (RC.Comp(RC.make_fixed_type_const dfg a, folTypes), ts)  end
    1.82 +      in  (SFC.Comp(SFC.make_fixed_type_const dfg a, folTypes), ts)  end
    1.83    | type_of _ (tp as TFree (a, _)) =
    1.84 -      (RC.AtomF (RC.make_fixed_type_var a), [tp])
    1.85 +      (SFC.AtomF (SFC.make_fixed_type_var a), [tp])
    1.86    | type_of _ (tp as TVar (v, _)) =
    1.87 -      (RC.AtomV (RC.make_schematic_type_var v), [tp])
    1.88 +      (SFC.AtomV (SFC.make_schematic_type_var v), [tp])
    1.89  and types_of dfg Ts =
    1.90        let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
    1.91 -      in  (folTyps, RC.union_all ts)  end;
    1.92 +      in  (folTyps, SFC.union_all ts)  end;
    1.93  
    1.94  (* same as above, but no gathering of sort information *)
    1.95  fun simp_type_of dfg (Type (a, Ts)) =
    1.96 -      RC.Comp(RC.make_fixed_type_const dfg a, map (simp_type_of dfg) Ts)
    1.97 -  | simp_type_of _ (TFree (a, _)) = RC.AtomF(RC.make_fixed_type_var a)
    1.98 -  | simp_type_of _ (TVar (v, _)) = RC.AtomV(RC.make_schematic_type_var v);
    1.99 +      SFC.Comp(SFC.make_fixed_type_const dfg a, map (simp_type_of dfg) Ts)
   1.100 +  | simp_type_of _ (TFree (a, _)) = SFC.AtomF(SFC.make_fixed_type_var a)
   1.101 +  | simp_type_of _ (TVar (v, _)) = SFC.AtomV(SFC.make_schematic_type_var v);
   1.102  
   1.103  
   1.104  fun const_type_of dfg thy (c,t) =
   1.105 @@ -142,21 +142,21 @@
   1.106  (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
   1.107  fun combterm_of dfg thy (Const(c,t)) =
   1.108        let val (tp,ts,tvar_list) = const_type_of dfg thy (c,t)
   1.109 -          val c' = CombConst(RC.make_fixed_const dfg c, tp, tvar_list)
   1.110 +          val c' = CombConst(SFC.make_fixed_const dfg c, tp, tvar_list)
   1.111        in  (c',ts)  end
   1.112    | combterm_of dfg _ (Free(v,t)) =
   1.113        let val (tp,ts) = type_of dfg t
   1.114 -          val v' = CombConst(RC.make_fixed_var v, tp, [])
   1.115 +          val v' = CombConst(SFC.make_fixed_var v, tp, [])
   1.116        in  (v',ts)  end
   1.117    | combterm_of dfg _ (Var(v,t)) =
   1.118        let val (tp,ts) = type_of dfg t
   1.119 -          val v' = CombVar(RC.make_schematic_var v,tp)
   1.120 +          val v' = CombVar(SFC.make_schematic_var v,tp)
   1.121        in  (v',ts)  end
   1.122    | combterm_of dfg thy (P $ Q) =
   1.123        let val (P',tsP) = combterm_of dfg thy P
   1.124            val (Q',tsQ) = combterm_of dfg thy Q
   1.125        in  (CombApp(P',Q'), union (op =) tsP tsQ)  end
   1.126 -  | combterm_of _ _ (t as Abs _) = raise RC.CLAUSE ("HOL CLAUSE", t);
   1.127 +  | combterm_of _ _ (t as Abs _) = raise SFC.CLAUSE ("HOL CLAUSE", t);
   1.128  
   1.129  fun predicate_of dfg thy ((Const("Not",_) $ P), polarity) = predicate_of dfg thy (P, not polarity)
   1.130    | predicate_of dfg thy (t,polarity) = (combterm_of dfg thy (Envir.eta_contract t), polarity);
   1.131 @@ -189,7 +189,7 @@
   1.132  
   1.133  
   1.134  fun add_axiom_clause dfg thy ((th,(name,id)), pairs) =
   1.135 -  let val cls = make_clause dfg thy (id, name, RC.Axiom, th)
   1.136 +  let val cls = make_clause dfg thy (id, name, SFC.Axiom, th)
   1.137    in
   1.138        if isTaut cls then pairs else (name,cls)::pairs
   1.139    end;
   1.140 @@ -198,7 +198,7 @@
   1.141  
   1.142  fun make_conjecture_clauses_aux _ _ _ [] = []
   1.143    | make_conjecture_clauses_aux dfg thy n (th::ths) =
   1.144 -      make_clause dfg thy (n,"conjecture", RC.Conjecture, th) ::
   1.145 +      make_clause dfg thy (n,"conjecture", SFC.Conjecture, th) ::
   1.146        make_conjecture_clauses_aux dfg thy (n+1) ths;
   1.147  
   1.148  fun make_conjecture_clauses dfg thy = make_conjecture_clauses_aux dfg thy 0;
   1.149 @@ -211,7 +211,7 @@
   1.150  (**********************************************************************)
   1.151  
   1.152  (*Result of a function type; no need to check that the argument type matches.*)
   1.153 -fun result_type (RC.Comp ("tc_fun", [_, tp2])) = tp2
   1.154 +fun result_type (SFC.Comp ("tc_fun", [_, tp2])) = tp2
   1.155    | result_type _ = error "result_type"
   1.156  
   1.157  fun type_of_combterm (CombConst (_, tp, _)) = tp
   1.158 @@ -231,10 +231,10 @@
   1.159  
   1.160  fun wrap_type t_full (s, tp) =
   1.161    if t_full then
   1.162 -      type_wrapper ^ RC.paren_pack [s, RC.string_of_fol_type tp]
   1.163 +      type_wrapper ^ SFC.paren_pack [s, SFC.string_of_fol_type tp]
   1.164    else s;
   1.165  
   1.166 -fun apply ss = "hAPP" ^ RC.paren_pack ss;
   1.167 +fun apply ss = "hAPP" ^ SFC.paren_pack ss;
   1.168  
   1.169  fun rev_apply (v, []) = v
   1.170    | rev_apply (v, arg::args) = apply [rev_apply (v, args), arg];
   1.171 @@ -251,10 +251,10 @@
   1.172                                           Int.toString nargs ^ " but is applied to " ^
   1.173                                           space_implode ", " args)
   1.174            val args2 = List.drop(args, nargs)
   1.175 -          val targs = if not t_full then map RC.string_of_fol_type tvars
   1.176 +          val targs = if not t_full then map SFC.string_of_fol_type tvars
   1.177                        else []
   1.178        in
   1.179 -          string_apply (c ^ RC.paren_pack (args1@targs), args2)
   1.180 +          string_apply (c ^ SFC.paren_pack (args1@targs), args2)
   1.181        end
   1.182    | string_of_applic _ _ (CombVar (v, _), args) = string_apply (v, args)
   1.183    | string_of_applic _ _ _ = error "string_of_applic";
   1.184 @@ -271,13 +271,13 @@
   1.185  
   1.186  (*Boolean-valued terms are here converted to literals.*)
   1.187  fun boolify params t =
   1.188 -  "hBOOL" ^ RC.paren_pack [string_of_combterm params t];
   1.189 +  "hBOOL" ^ SFC.paren_pack [string_of_combterm params t];
   1.190  
   1.191  fun string_of_predicate (params as (_,_,cnh)) t =
   1.192    case t of
   1.193        (CombApp(CombApp(CombConst("equal",_,_), t1), t2)) =>
   1.194            (*DFG only: new TPTP prefers infix equality*)
   1.195 -          ("equal" ^ RC.paren_pack [string_of_combterm params t1, string_of_combterm params t2])
   1.196 +          ("equal" ^ SFC.paren_pack [string_of_combterm params t1, string_of_combterm params t2])
   1.197      | _ =>
   1.198            case #1 (strip_comb t) of
   1.199                CombConst(c,_,_) => if needs_hBOOL cnh c then boolify params t else string_of_combterm params t
   1.200 @@ -293,28 +293,28 @@
   1.201  fun tptp_literal params (Literal(pol, CombApp(CombApp(CombConst("equal",_,_), t1), t2))) =
   1.202        tptp_of_equality params pol (t1,t2)
   1.203    | tptp_literal params (Literal(pol,pred)) =
   1.204 -      RC.tptp_sign pol (string_of_predicate params pred);
   1.205 +      SFC.tptp_sign pol (string_of_predicate params pred);
   1.206  
   1.207  (*Given a clause, returns its literals paired with a list of literals concerning TFrees;
   1.208    the latter should only occur in conjecture clauses.*)
   1.209  fun tptp_type_lits params pos (Clause{literals, ctypes_sorts, ...}) =
   1.210        (map (tptp_literal params) literals, 
   1.211 -       map (RC.tptp_of_typeLit pos) (RC.add_typs ctypes_sorts));
   1.212 +       map (SFC.tptp_of_typeLit pos) (SFC.add_typs ctypes_sorts));
   1.213  
   1.214  fun clause2tptp params (cls as Clause {axiom_name, clause_id, kind, ...}) =
   1.215 -  let val (lits,tylits) = tptp_type_lits params (kind = RC.Conjecture) cls
   1.216 +  let val (lits,tylits) = tptp_type_lits params (kind = SFC.Conjecture) cls
   1.217    in
   1.218 -      (RC.gen_tptp_cls(clause_id,axiom_name,kind,lits,tylits), tylits)
   1.219 +      (SFC.gen_tptp_cls(clause_id,axiom_name,kind,lits,tylits), tylits)
   1.220    end;
   1.221  
   1.222  
   1.223  (*** dfg format ***)
   1.224  
   1.225 -fun dfg_literal params (Literal(pol,pred)) = RC.dfg_sign pol (string_of_predicate params pred);
   1.226 +fun dfg_literal params (Literal(pol,pred)) = SFC.dfg_sign pol (string_of_predicate params pred);
   1.227  
   1.228  fun dfg_type_lits params pos (Clause{literals, ctypes_sorts, ...}) =
   1.229        (map (dfg_literal params) literals, 
   1.230 -       map (RC.dfg_of_typeLit pos) (RC.add_typs ctypes_sorts));
   1.231 +       map (SFC.dfg_of_typeLit pos) (SFC.add_typs ctypes_sorts));
   1.232  
   1.233  fun get_uvars (CombConst _) vars = vars
   1.234    | get_uvars (CombVar(v,_)) vars = (v::vars)
   1.235 @@ -322,20 +322,20 @@
   1.236  
   1.237  fun get_uvars_l (Literal(_,c)) = get_uvars c [];
   1.238  
   1.239 -fun dfg_vars (Clause {literals,...}) = RC.union_all (map get_uvars_l literals);
   1.240 +fun dfg_vars (Clause {literals,...}) = SFC.union_all (map get_uvars_l literals);
   1.241  
   1.242  fun clause2dfg params (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
   1.243 -  let val (lits,tylits) = dfg_type_lits params (kind = RC.Conjecture) cls
   1.244 +  let val (lits,tylits) = dfg_type_lits params (kind = SFC.Conjecture) cls
   1.245        val vars = dfg_vars cls
   1.246 -      val tvars = RC.get_tvar_strs ctypes_sorts
   1.247 +      val tvars = SFC.get_tvar_strs ctypes_sorts
   1.248    in
   1.249 -      (RC.gen_dfg_cls(clause_id, axiom_name, kind, lits, tylits, tvars@vars), tylits)
   1.250 +      (SFC.gen_dfg_cls(clause_id, axiom_name, kind, lits, tylits, tvars@vars), tylits)
   1.251    end;
   1.252  
   1.253  
   1.254  (** For DFG format: accumulate function and predicate declarations **)
   1.255  
   1.256 -fun addtypes tvars tab = List.foldl RC.add_foltype_funcs tab tvars;
   1.257 +fun addtypes tvars tab = List.foldl SFC.add_foltype_funcs tab tvars;
   1.258  
   1.259  fun add_decls (t_full, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) =
   1.260        if c = "equal" then (addtypes tvars funcs, preds)
   1.261 @@ -348,7 +348,7 @@
   1.262              else (addtypes tvars funcs, addit preds)
   1.263          end
   1.264    | add_decls _ (CombVar(_,ctp), (funcs,preds)) =
   1.265 -      (RC.add_foltype_funcs (ctp,funcs), preds)
   1.266 +      (SFC.add_foltype_funcs (ctp,funcs), preds)
   1.267    | add_decls params (CombApp(P,Q),decls) = add_decls params (P,add_decls params (Q,decls));
   1.268  
   1.269  fun add_literal_decls params (Literal(_,c), decls) = add_decls params (c,decls);
   1.270 @@ -358,23 +358,23 @@
   1.271      handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
   1.272  
   1.273  fun decls_of_clauses params clauses arity_clauses =
   1.274 -  let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) RC.init_functab)
   1.275 +  let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) SFC.init_functab)
   1.276        val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty
   1.277        val (functab,predtab) = (List.foldl (add_clause_decls params) (init_functab, init_predtab) clauses)
   1.278    in
   1.279 -      (Symtab.dest (List.foldl RC.add_arityClause_funcs functab arity_clauses),
   1.280 +      (Symtab.dest (List.foldl SFC.add_arityClause_funcs functab arity_clauses),
   1.281         Symtab.dest predtab)
   1.282    end;
   1.283  
   1.284  fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) =
   1.285 -  List.foldl RC.add_type_sort_preds preds ctypes_sorts
   1.286 +  List.foldl SFC.add_type_sort_preds preds ctypes_sorts
   1.287    handle Symtab.DUP a => error ("predicate " ^ a ^ " has multiple arities")
   1.288  
   1.289  (*Higher-order clauses have only the predicates hBOOL and type classes.*)
   1.290  fun preds_of_clauses clauses clsrel_clauses arity_clauses =
   1.291      Symtab.dest
   1.292 -        (List.foldl RC.add_classrelClause_preds
   1.293 -               (List.foldl RC.add_arityClause_preds
   1.294 +        (List.foldl SFC.add_classrelClause_preds
   1.295 +               (List.foldl SFC.add_arityClause_preds
   1.296                        (List.foldl add_clause_preds Symtab.empty clauses)
   1.297                        arity_clauses)
   1.298                 clsrel_clauses)
   1.299 @@ -404,7 +404,8 @@
   1.300    else ct;
   1.301  
   1.302  fun cnf_helper_thms thy =
   1.303 -  Res_Axioms.cnf_rules_pairs thy o map Res_Axioms.pairname
   1.304 +  Sledgehammer_Fact_Preprocessor.cnf_rules_pairs thy
   1.305 +  o map Sledgehammer_Fact_Preprocessor.pairname
   1.306  
   1.307  fun get_helper_clauses dfg thy isFO (conjectures, axcls, user_lemmas) =
   1.308    if isFO then []  (*first-order*)
   1.309 @@ -454,7 +455,8 @@
   1.310    fold count_constants_lit literals (const_min_arity, const_needs_hBOOL);
   1.311  
   1.312  fun display_arity const_needs_hBOOL (c,n) =
   1.313 -  Res_Axioms.trace_msg (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^
   1.314 +  Sledgehammer_Fact_Preprocessor.trace_msg (fn () => "Constant: " ^ c ^
   1.315 +                " arity:\t" ^ Int.toString n ^
   1.316                  (if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else ""));
   1.317  
   1.318  fun count_constants (conjectures, _, extra_clauses, helper_clauses, _, _) =
   1.319 @@ -476,14 +478,14 @@
   1.320      val (cma, cnh) = count_constants clauses
   1.321      val params = (t_full, cma, cnh)
   1.322      val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
   1.323 -    val tfree_clss = map RC.tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
   1.324 +    val tfree_clss = map SFC.tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
   1.325      val _ =
   1.326        File.write_list file (
   1.327          map (#1 o (clause2tptp params)) axclauses @
   1.328          tfree_clss @
   1.329          tptp_clss @
   1.330 -        map RC.tptp_classrelClause classrel_clauses @
   1.331 -        map RC.tptp_arity_clause arity_clauses @
   1.332 +        map SFC.tptp_classrelClause classrel_clauses @
   1.333 +        map SFC.tptp_arity_clause arity_clauses @
   1.334          map (#1 o (clause2tptp params)) helper_clauses)
   1.335      in (length axclauses + 1, length tfree_clss + length tptp_clss)
   1.336    end;
   1.337 @@ -500,20 +502,20 @@
   1.338      val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures)
   1.339      and probname = Path.implode (Path.base file)
   1.340      val axstrs = map (#1 o (clause2dfg params)) axclauses
   1.341 -    val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss)
   1.342 +    val tfree_clss = map SFC.dfg_tfree_clause (SFC.union_all tfree_litss)
   1.343      val helper_clauses_strs = map (#1 o (clause2dfg params)) helper_clauses
   1.344      val (funcs,cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
   1.345      and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
   1.346      val _ =
   1.347        File.write_list file (
   1.348 -        RC.string_of_start probname ::
   1.349 -        RC.string_of_descrip probname ::
   1.350 -        RC.string_of_symbols (RC.string_of_funcs funcs)
   1.351 -          (RC.string_of_preds (cl_preds @ ty_preds)) ::
   1.352 +        SFC.string_of_start probname ::
   1.353 +        SFC.string_of_descrip probname ::
   1.354 +        SFC.string_of_symbols (SFC.string_of_funcs funcs)
   1.355 +          (SFC.string_of_preds (cl_preds @ ty_preds)) ::
   1.356          "list_of_clauses(axioms,cnf).\n" ::
   1.357          axstrs @
   1.358 -        map RC.dfg_classrelClause classrel_clauses @
   1.359 -        map RC.dfg_arity_clause arity_clauses @
   1.360 +        map SFC.dfg_classrelClause classrel_clauses @
   1.361 +        map SFC.dfg_arity_clause arity_clauses @
   1.362          helper_clauses_strs @
   1.363          ["end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"] @
   1.364          tfree_clss @