src/HOL/Tools/res_hol_clause.ML
author paulson
Tue, 09 Oct 2007 18:14:00 +0200
changeset 24937 340523598914
parent 24385 ab62948281a9
child 24940 8f9dea697b8d
permissions -rw-r--r--
context-based treatment of generalization; also handling TFrees in axiom clauses
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
     1
(* ID: $Id$
17998
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
     2
   Author: Jia Meng, NICTA
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
     3
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
     4
FOL clauses translated from HOL formulae.
22825
bd774e01d6d5 Fixing bugs in the partial-typed and fully-typed translations
paulson
parents: 22130
diff changeset
     5
bd774e01d6d5 Fixing bugs in the partial-typed and fully-typed translations
paulson
parents: 22130
diff changeset
     6
The combinator code needs to be deleted after the translation paper has been published.
bd774e01d6d5 Fixing bugs in the partial-typed and fully-typed translations
paulson
parents: 22130
diff changeset
     7
It cannot be used with proof reconstruction because combinators are not introduced by proof.
bd774e01d6d5 Fixing bugs in the partial-typed and fully-typed translations
paulson
parents: 22130
diff changeset
     8
The Turner combinators (B', C', S') yield no improvement and should be deleted.
17998
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
     9
*)
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
    10
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    11
signature RES_HOL_CLAUSE =
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    12
sig
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    13
  val ext: thm
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    14
  val comb_I: thm
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    15
  val comb_K: thm
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    16
  val comb_B: thm
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    17
  val comb_C: thm
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    18
  val comb_S: thm
24385
ab62948281a9 Deleted the partially-typed translation and the combinator code.
paulson
parents: 24323
diff changeset
    19
  datatype type_level = T_FULL | T_CONST
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    20
  val typ_level: type_level ref
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    21
  val minimize_applies: bool ref
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    22
  type axiom_name = string
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    23
  type polarity = bool
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    24
  type clause_id = int
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    25
  datatype combterm =
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    26
      CombConst of string * ResClause.fol_type * ResClause.fol_type list (*Const and Free*)
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    27
    | CombVar of string * ResClause.fol_type
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    28
    | CombApp of combterm * combterm
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    29
  datatype literal = Literal of polarity * combterm
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    30
  val strip_comb: combterm -> combterm * combterm list
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
    31
  val literals_of_term: theory -> term -> literal list * (ResClause.typ_var * sort) list
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
    32
  val tptp_write_file: theory -> bool -> thm list -> string ->
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    33
    (thm * (axiom_name * clause_id)) list * ResClause.classrelClause list *
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    34
      ResClause.arityClause list -> string list -> axiom_name list
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
    35
  val dfg_write_file: theory -> bool -> thm list -> string ->
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    36
    (thm * (axiom_name * clause_id)) list * ResClause.classrelClause list *
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    37
      ResClause.arityClause list -> string list -> axiom_name list
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    38
end
17998
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
    39
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    40
structure ResHolClause: RES_HOL_CLAUSE =
17998
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
    41
struct
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
    42
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
    43
structure RC = ResClause;
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
    44
20791
497e1c9d4a9f Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents: 20660
diff changeset
    45
(* theorems for combinators and function extensionality *)
497e1c9d4a9f Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents: 20660
diff changeset
    46
val ext = thm "HOL.ext";
21254
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents: 21135
diff changeset
    47
val comb_I = thm "ATP_Linkup.COMBI_def";
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents: 21135
diff changeset
    48
val comb_K = thm "ATP_Linkup.COMBK_def";
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents: 21135
diff changeset
    49
val comb_B = thm "ATP_Linkup.COMBB_def";
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents: 21135
diff changeset
    50
val comb_C = thm "ATP_Linkup.COMBC_def";
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents: 21135
diff changeset
    51
val comb_S = thm "ATP_Linkup.COMBS_def";
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents: 21135
diff changeset
    52
val comb_B' = thm "ATP_Linkup.COMBB'_def";
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents: 21135
diff changeset
    53
val comb_C' = thm "ATP_Linkup.COMBC'_def";
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents: 21135
diff changeset
    54
val comb_S' = thm "ATP_Linkup.COMBS'_def";
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents: 21135
diff changeset
    55
val fequal_imp_equal = thm "ATP_Linkup.fequal_imp_equal";
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents: 21135
diff changeset
    56
val equal_imp_fequal = thm "ATP_Linkup.equal_imp_fequal";
20791
497e1c9d4a9f Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents: 20660
diff changeset
    57
22825
bd774e01d6d5 Fixing bugs in the partial-typed and fully-typed translations
paulson
parents: 22130
diff changeset
    58
bd774e01d6d5 Fixing bugs in the partial-typed and fully-typed translations
paulson
parents: 22130
diff changeset
    59
(*The different translations of types*)
24385
ab62948281a9 Deleted the partially-typed translation and the combinator code.
paulson
parents: 24323
diff changeset
    60
datatype type_level = T_FULL | T_CONST;
22825
bd774e01d6d5 Fixing bugs in the partial-typed and fully-typed translations
paulson
parents: 22130
diff changeset
    61
bd774e01d6d5 Fixing bugs in the partial-typed and fully-typed translations
paulson
parents: 22130
diff changeset
    62
val typ_level = ref T_CONST;
bd774e01d6d5 Fixing bugs in the partial-typed and fully-typed translations
paulson
parents: 22130
diff changeset
    63
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
    64
(*If true, each function will be directly applied to as many arguments as possible, avoiding
24385
ab62948281a9 Deleted the partially-typed translation and the combinator code.
paulson
parents: 24323
diff changeset
    65
  use of the "apply" operator. Use of hBOOL is also minimized.*)
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
    66
val minimize_applies = ref true;
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
    67
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
    68
val const_min_arity = ref (Symtab.empty : int Symtab.table);
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
    69
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
    70
val const_needs_hBOOL = ref (Symtab.empty : bool Symtab.table);
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
    71
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
    72
fun min_arity_of c = getOpt (Symtab.lookup(!const_min_arity) c, 0);
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
    73
22825
bd774e01d6d5 Fixing bugs in the partial-typed and fully-typed translations
paulson
parents: 22130
diff changeset
    74
(*True if the constant ever appears outside of the top-level position in literals.
bd774e01d6d5 Fixing bugs in the partial-typed and fully-typed translations
paulson
parents: 22130
diff changeset
    75
  If false, the constant always receives all of its arguments and is used as a predicate.*)
24385
ab62948281a9 Deleted the partially-typed translation and the combinator code.
paulson
parents: 24323
diff changeset
    76
fun needs_hBOOL c = not (!minimize_applies) orelse
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
    77
                    getOpt (Symtab.lookup(!const_needs_hBOOL) c, false);
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
    78
19198
e6f1ff40ba99 Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents: 19130
diff changeset
    79
17998
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
    80
(******************************************************)
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
    81
(* data types for typed combinator expressions        *)
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
    82
(******************************************************)
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
    83
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
    84
type axiom_name = string;
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
    85
type polarity = bool;
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
    86
type clause_id = int;
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
    87
23386
9255c1a75ba9 Now also handles FO problems
paulson
parents: 22851
diff changeset
    88
datatype combterm = CombConst of string * RC.fol_type * RC.fol_type list (*Const and Free*)
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    89
                  | CombVar of string * RC.fol_type
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    90
                  | CombApp of combterm * combterm
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    91
17998
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
    92
datatype literal = Literal of polarity * combterm;
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
    93
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    94
datatype clause =
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    95
         Clause of {clause_id: clause_id,
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    96
                    axiom_name: axiom_name,
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    97
                    th: thm,
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    98
                    kind: RC.kind,
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
    99
                    literals: literal list,
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24385
diff changeset
   100
                    ctypes_sorts: (RC.typ_var * Term.sort) list};
17998
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   101
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   102
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   103
(*********************************************************************)
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   104
(* convert a clause with type Term.term to a clause with type clause *)
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   105
(*********************************************************************)
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   106
21561
cfd2258f0b23 Tidied code. Bool constructor is not needed.
paulson
parents: 21513
diff changeset
   107
fun isFalse (Literal(pol, CombConst(c,_,_))) =
20360
8c8c824dccdc tidying
paulson
parents: 20281
diff changeset
   108
      (pol andalso c = "c_False") orelse
8c8c824dccdc tidying
paulson
parents: 20281
diff changeset
   109
      (not pol andalso c = "c_True")
17998
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   110
  | isFalse _ = false;
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   111
21561
cfd2258f0b23 Tidied code. Bool constructor is not needed.
paulson
parents: 21513
diff changeset
   112
fun isTrue (Literal (pol, CombConst(c,_,_))) =
17998
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   113
      (pol andalso c = "c_True") orelse
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   114
      (not pol andalso c = "c_False")
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   115
  | isTrue _ = false;
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   116
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   117
fun isTaut (Clause {literals,...}) = exists isTrue literals;
17998
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   118
18440
72ee07f4b56b Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents: 18356
diff changeset
   119
fun type_of (Type (a, Ts)) =
21561
cfd2258f0b23 Tidied code. Bool constructor is not needed.
paulson
parents: 21513
diff changeset
   120
      let val (folTypes,ts) = types_of Ts
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   121
      in  (RC.Comp(RC.make_fixed_type_const a, folTypes), ts)  end
18440
72ee07f4b56b Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents: 18356
diff changeset
   122
  | type_of (tp as (TFree(a,s))) =
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   123
      (RC.AtomF (RC.make_fixed_type_var a), [RC.mk_typ_var_sort tp])
18440
72ee07f4b56b Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents: 18356
diff changeset
   124
  | type_of (tp as (TVar(v,s))) =
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   125
      (RC.AtomV (RC.make_schematic_type_var v), [RC.mk_typ_var_sort tp])
18440
72ee07f4b56b Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents: 18356
diff changeset
   126
and types_of Ts =
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   127
      let val (folTyps,ts) = ListPair.unzip (map type_of Ts)
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   128
      in  (folTyps, RC.union_all ts)  end;
17998
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   129
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   130
(* same as above, but no gathering of sort information *)
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   131
fun simp_type_of (Type (a, Ts)) =
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   132
      RC.Comp(RC.make_fixed_type_const a, map simp_type_of Ts)
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   133
  | simp_type_of (TFree (a,s)) = RC.AtomF(RC.make_fixed_type_var a)
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   134
  | simp_type_of (TVar (v,s)) = RC.AtomV(RC.make_schematic_type_var v);
18440
72ee07f4b56b Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents: 18356
diff changeset
   135
18356
443717b3a9ad Added new type embedding methods for translating HOL clauses.
mengj
parents: 18276
diff changeset
   136
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   137
fun const_type_of thy (c,t) =
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   138
      let val (tp,ts) = type_of t
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   139
      in  (tp, ts, map simp_type_of (Sign.const_typargs thy (c,t))) end;
18356
443717b3a9ad Added new type embedding methods for translating HOL clauses.
mengj
parents: 18276
diff changeset
   140
17998
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   141
(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   142
fun combterm_of thy (Const(c,t)) =
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   143
      let val (tp,ts,tvar_list) = const_type_of thy (c,t)
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   144
          val c' = CombConst(RC.make_fixed_const c, tp, tvar_list)
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   145
      in  (c',ts)  end
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   146
  | combterm_of thy (Free(v,t)) =
21513
9e9fff87dc6c Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents: 21509
diff changeset
   147
      let val (tp,ts) = type_of t
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   148
          val v' = if RC.isMeta v then CombVar(RC.make_schematic_var(v,0),tp)
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   149
                   else CombConst(RC.make_fixed_var v, tp, [])
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   150
      in  (v',ts)  end
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   151
  | combterm_of thy (Var(v,t)) =
21513
9e9fff87dc6c Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents: 21509
diff changeset
   152
      let val (tp,ts) = type_of t
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   153
          val v' = CombVar(RC.make_schematic_var v,tp)
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   154
      in  (v',ts)  end
24385
ab62948281a9 Deleted the partially-typed translation and the combinator code.
paulson
parents: 24323
diff changeset
   155
  | combterm_of thy (P $ Q) =
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   156
      let val (P',tsP) = combterm_of thy P
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   157
          val (Q',tsQ) = combterm_of thy Q
24385
ab62948281a9 Deleted the partially-typed translation and the combinator code.
paulson
parents: 24323
diff changeset
   158
      in  (CombApp(P',Q'), tsP union tsQ)  end
ab62948281a9 Deleted the partially-typed translation and the combinator code.
paulson
parents: 24323
diff changeset
   159
  | combterm_of thy (t as Abs _) = raise RC.CLAUSE("HOL CLAUSE",t);
17998
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   160
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   161
fun predicate_of thy ((Const("Not",_) $ P), polarity) = predicate_of thy (P, not polarity)
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   162
  | predicate_of thy (t,polarity) = (combterm_of thy t, polarity);
17998
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   163
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   164
fun literals_of_term1 thy args (Const("Trueprop",_) $ P) = literals_of_term1 thy args P
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   165
  | literals_of_term1 thy args (Const("op |",_) $ P $ Q) =
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   166
      literals_of_term1 thy (literals_of_term1 thy args P) Q
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   167
  | literals_of_term1 thy (lits,ts) P =
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   168
      let val ((pred,ts'),pol) = predicate_of thy (P,true)
21509
6c5755ad9cae ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents: 21470
diff changeset
   169
      in
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   170
          (Literal(pol,pred)::lits, ts union ts')
21509
6c5755ad9cae ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents: 21470
diff changeset
   171
      end;
17998
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   172
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   173
fun literals_of_term thy P = literals_of_term1 thy ([],[]) P;
17998
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   174
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   175
(* making axiom and conjecture clauses *)
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   176
fun make_clause thy (clause_id,axiom_name,kind,th) =
24385
ab62948281a9 Deleted the partially-typed translation and the combinator code.
paulson
parents: 24323
diff changeset
   177
    let val (lits,ctypes_sorts) = literals_of_term thy (prop_of th)
17998
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   178
    in
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   179
        if forall isFalse lits
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   180
        then error "Problem too trivial for resolution (empty clause)"
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   181
        else
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   182
            Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, kind = kind,
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24385
diff changeset
   183
                    literals = lits, ctypes_sorts = ctypes_sorts}
17998
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   184
    end;
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   185
20016
9a005f7d95e6 Literals aren't sorted any more.
mengj
parents: 19964
diff changeset
   186
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   187
fun add_axiom_clause thy ((th,(name,id)), pairs) =
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   188
  let val cls = make_clause thy (id, name, RC.Axiom, th)
21573
8a7a68c0096c Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents: 21561
diff changeset
   189
  in
8a7a68c0096c Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents: 21561
diff changeset
   190
      if isTaut cls then pairs else (name,cls)::pairs
8a7a68c0096c Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents: 21561
diff changeset
   191
  end;
19354
aebf9dddccd7 tptp_write_file accepts axioms as thm.
mengj
parents: 19198
diff changeset
   192
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   193
fun make_axiom_clauses thy = foldl (add_axiom_clause thy) [];
19354
aebf9dddccd7 tptp_write_file accepts axioms as thm.
mengj
parents: 19198
diff changeset
   194
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   195
fun make_conjecture_clauses_aux _ _ [] = []
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   196
  | make_conjecture_clauses_aux thy n (th::ths) =
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   197
      make_clause thy (n,"conjecture", RC.Conjecture, th) ::
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   198
      make_conjecture_clauses_aux thy (n+1) ths;
17998
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   199
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   200
fun make_conjecture_clauses thy = make_conjecture_clauses_aux thy 0;
17998
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   201
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   202
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   203
(**********************************************************************)
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   204
(* convert clause into ATP specific formats:                          *)
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   205
(* TPTP used by Vampire and E                                         *)
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   206
(* DFG used by SPASS                                                  *)
17998
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   207
(**********************************************************************)
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   208
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   209
(*Result of a function type; no need to check that the argument type matches.*)
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   210
fun result_type (RC.Comp ("tc_fun", [_, tp2])) = tp2
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   211
  | result_type _ = raise ERROR "result_type"
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   212
21513
9e9fff87dc6c Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents: 21509
diff changeset
   213
fun type_of_combterm (CombConst(c,tp,_)) = tp
9e9fff87dc6c Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents: 21509
diff changeset
   214
  | type_of_combterm (CombVar(v,tp)) = tp
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   215
  | type_of_combterm (CombApp(t1,t2)) = result_type (type_of_combterm t1);
17998
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   216
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   217
(*gets the head of a combinator application, along with the list of arguments*)
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   218
fun strip_comb u =
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   219
    let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   220
        |   stripc  x =  x
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   221
    in  stripc(u,[])  end;
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   222
22851
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   223
val type_wrapper = "ti";
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   224
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   225
fun head_needs_hBOOL (CombConst(c,_,_)) = needs_hBOOL c
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   226
  | head_needs_hBOOL _ = true;
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   227
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   228
fun wrap_type (s, tp) =
22851
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   229
  if !typ_level=T_FULL then
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   230
      type_wrapper ^ RC.paren_pack [s, RC.string_of_fol_type tp]
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   231
  else s;
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   232
22851
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   233
fun apply ss = "hAPP" ^ RC.paren_pack ss;
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   234
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   235
fun rev_apply (v, []) = v
22851
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   236
  | rev_apply (v, arg::args) = apply [rev_apply (v, args), arg];
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   237
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   238
fun string_apply (v, args) = rev_apply (v, rev args);
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   239
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   240
(*Apply an operator to the argument strings, using either the "apply" operator or
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   241
  direct function application.*)
22851
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   242
fun string_of_applic (CombConst(c,tp,tvars), args) =
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   243
      let val c = if c = "equal" then "c_fequal" else c
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   244
          val nargs = min_arity_of c
22851
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   245
          val args1 = List.take(args, nargs)
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   246
            handle Subscript => raise ERROR ("string_of_applic: " ^ c ^ " has arity " ^
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   247
                                             Int.toString nargs ^ " but is applied to " ^
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   248
                                             space_implode ", " args)
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   249
          val args2 = List.drop(args, nargs)
22851
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   250
          val targs = if !typ_level = T_CONST then map RC.string_of_fol_type tvars
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   251
                      else []
21513
9e9fff87dc6c Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents: 21509
diff changeset
   252
      in
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   253
          string_apply (c ^ RC.paren_pack (args1@targs), args2)
21513
9e9fff87dc6c Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents: 21509
diff changeset
   254
      end
22851
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   255
  | string_of_applic (CombVar(v,tp), args) = string_apply (v, args)
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   256
  | string_of_applic _ = raise ERROR "string_of_applic";
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   257
22851
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   258
fun wrap_type_if (head, s, tp) = if head_needs_hBOOL head then wrap_type (s, tp) else s;
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   259
24385
ab62948281a9 Deleted the partially-typed translation and the combinator code.
paulson
parents: 24323
diff changeset
   260
fun string_of_combterm t =
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   261
  let val (head, args) = strip_comb t
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   262
  in  wrap_type_if (head,
24385
ab62948281a9 Deleted the partially-typed translation and the combinator code.
paulson
parents: 24323
diff changeset
   263
                    string_of_applic (head, map string_of_combterm args),
22851
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   264
                    type_of_combterm t)
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   265
  end;
18356
443717b3a9ad Added new type embedding methods for translating HOL clauses.
mengj
parents: 18276
diff changeset
   266
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   267
(*Boolean-valued terms are here converted to literals.*)
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   268
fun boolify t = "hBOOL" ^ RC.paren_pack [string_of_combterm t];
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   269
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   270
fun string_of_predicate t =
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   271
  case t of
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   272
      (CombApp(CombApp(CombConst("equal",_,_), t1), t2)) =>
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   273
          (*DFG only: new TPTP prefers infix equality*)
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   274
          ("equal" ^ RC.paren_pack [string_of_combterm t1, string_of_combterm t2])
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   275
    | _ =>
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   276
          case #1 (strip_comb t) of
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   277
              CombConst(c,_,_) => if needs_hBOOL c then boolify t else string_of_combterm t
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   278
            | _ => boolify t;
18356
443717b3a9ad Added new type embedding methods for translating HOL clauses.
mengj
parents: 18276
diff changeset
   279
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   280
fun string_of_clausename (cls_id,ax_name) =
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   281
    RC.clause_prefix ^ RC.ascii_of ax_name ^ "_" ^ Int.toString cls_id;
17998
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   282
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   283
fun string_of_type_clsname (cls_id,ax_name,idx) =
17998
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   284
    string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx);
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   285
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   286
21561
cfd2258f0b23 Tidied code. Bool constructor is not needed.
paulson
parents: 21513
diff changeset
   287
(*** tptp format ***)
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   288
21513
9e9fff87dc6c Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents: 21509
diff changeset
   289
fun tptp_of_equality pol (t1,t2) =
9e9fff87dc6c Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents: 21509
diff changeset
   290
  let val eqop = if pol then " = " else " != "
9e9fff87dc6c Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents: 21509
diff changeset
   291
  in  string_of_combterm t1 ^ eqop ^ string_of_combterm t2  end;
9e9fff87dc6c Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents: 21509
diff changeset
   292
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   293
fun tptp_literal (Literal(pol, CombApp(CombApp(CombConst("equal",_,_), t1), t2))) =
21513
9e9fff87dc6c Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents: 21509
diff changeset
   294
      tptp_of_equality pol (t1,t2)
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   295
  | tptp_literal (Literal(pol,pred)) =
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   296
      RC.tptp_sign pol (string_of_predicate pred);
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   297
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   298
(*Given a clause, returns its literals paired with a list of literals concerning TFrees;
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   299
  the latter should only occur in conjecture clauses.*)
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24385
diff changeset
   300
fun tptp_type_lits pos (Clause{literals, ctypes_sorts, ...}) =
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24385
diff changeset
   301
      (map tptp_literal literals, 
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24385
diff changeset
   302
       map (RC.tptp_of_typeLit pos) (RC.add_typs ctypes_sorts));
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   303
21509
6c5755ad9cae ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents: 21470
diff changeset
   304
fun clause2tptp (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24385
diff changeset
   305
  let val (lits,tylits) = tptp_type_lits (kind = RC.Conjecture) cls
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24385
diff changeset
   306
  in
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24385
diff changeset
   307
      (RC.gen_tptp_cls(clause_id,axiom_name,kind,lits,tylits), tylits)
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24385
diff changeset
   308
  end;
17998
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   309
0a869029ca58 A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
mengj
parents:
diff changeset
   310
21561
cfd2258f0b23 Tidied code. Bool constructor is not needed.
paulson
parents: 21513
diff changeset
   311
(*** dfg format ***)
cfd2258f0b23 Tidied code. Bool constructor is not needed.
paulson
parents: 21513
diff changeset
   312
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   313
fun dfg_literal (Literal(pol,pred)) = RC.dfg_sign pol (string_of_predicate pred);
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   314
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24385
diff changeset
   315
fun dfg_type_lits pos (Clause{literals, ctypes_sorts, ...}) =
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24385
diff changeset
   316
      (map dfg_literal literals, 
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24385
diff changeset
   317
       map (RC.dfg_of_typeLit pos) (RC.add_typs ctypes_sorts));
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   318
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   319
fun get_uvars (CombConst _) vars = vars
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   320
  | get_uvars (CombVar(v,_)) vars = (v::vars)
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   321
  | get_uvars (CombApp(P,Q)) vars = get_uvars P (get_uvars Q vars);
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   322
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   323
fun get_uvars_l (Literal(_,c)) = get_uvars c [];
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   324
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   325
fun dfg_vars (Clause {literals,...}) = RC.union_all (map get_uvars_l literals);
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   326
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   327
fun clause2dfg (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24385
diff changeset
   328
  let val (lits,tylits) = dfg_type_lits (kind = RC.Conjecture) cls
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24385
diff changeset
   329
      val vars = dfg_vars cls
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24385
diff changeset
   330
      val tvars = RC.get_tvar_strs ctypes_sorts
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24385
diff changeset
   331
  in
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24385
diff changeset
   332
      (RC.gen_dfg_cls(clause_id, axiom_name, kind, lits, tylits, tvars@vars), tylits)
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24385
diff changeset
   333
  end;
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24385
diff changeset
   334
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   335
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   336
(** For DFG format: accumulate function and predicate declarations **)
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   337
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   338
fun addtypes tvars tab = foldl RC.add_foltype_funcs tab tvars;
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   339
22825
bd774e01d6d5 Fixing bugs in the partial-typed and fully-typed translations
paulson
parents: 22130
diff changeset
   340
fun add_decls (CombConst(c,tp,tvars), (funcs,preds)) =
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   341
      if c = "equal" then (addtypes tvars funcs, preds)
21561
cfd2258f0b23 Tidied code. Bool constructor is not needed.
paulson
parents: 21513
diff changeset
   342
      else
24385
ab62948281a9 Deleted the partially-typed translation and the combinator code.
paulson
parents: 24323
diff changeset
   343
	let val arity = min_arity_of c
ab62948281a9 Deleted the partially-typed translation and the combinator code.
paulson
parents: 24323
diff changeset
   344
	    val ntys = if !typ_level = T_CONST then length tvars else 0
ab62948281a9 Deleted the partially-typed translation and the combinator code.
paulson
parents: 24323
diff changeset
   345
	    val addit = Symtab.update(c, arity+ntys)
ab62948281a9 Deleted the partially-typed translation and the combinator code.
paulson
parents: 24323
diff changeset
   346
	in
ab62948281a9 Deleted the partially-typed translation and the combinator code.
paulson
parents: 24323
diff changeset
   347
	    if needs_hBOOL c then (addtypes tvars (addit funcs), preds)
ab62948281a9 Deleted the partially-typed translation and the combinator code.
paulson
parents: 24323
diff changeset
   348
	    else (addtypes tvars funcs, addit preds)
ab62948281a9 Deleted the partially-typed translation and the combinator code.
paulson
parents: 24323
diff changeset
   349
	end
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   350
  | add_decls (CombVar(_,ctp), (funcs,preds)) =
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   351
      (RC.add_foltype_funcs (ctp,funcs), preds)
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   352
  | add_decls (CombApp(P,Q),decls) = add_decls(P,add_decls (Q,decls));
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   353
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   354
fun add_literal_decls (Literal(_,c), decls) = add_decls (c,decls);
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   355
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   356
fun add_clause_decls (Clause {literals, ...}, decls) =
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   357
    foldl add_literal_decls decls literals
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   358
    handle Symtab.DUP a => raise ERROR ("function " ^ a ^ " has multiple arities")
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   359
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   360
fun decls_of_clauses clauses arity_clauses =
24385
ab62948281a9 Deleted the partially-typed translation and the combinator code.
paulson
parents: 24323
diff changeset
   361
  let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) RC.init_functab)
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   362
      val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   363
      val (functab,predtab) = (foldl add_clause_decls (init_functab, init_predtab) clauses)
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   364
  in
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   365
      (Symtab.dest (foldl RC.add_arityClause_funcs functab arity_clauses),
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   366
       Symtab.dest predtab)
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   367
  end;
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   368
21398
11996e938dfe Includes type:sort constraints in its code to collect predicates in axiom clauses.
paulson
parents: 21254
diff changeset
   369
fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) =
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   370
  foldl RC.add_type_sort_preds preds ctypes_sorts
21398
11996e938dfe Includes type:sort constraints in its code to collect predicates in axiom clauses.
paulson
parents: 21254
diff changeset
   371
  handle Symtab.DUP a => raise ERROR ("predicate " ^ a ^ " has multiple arities")
11996e938dfe Includes type:sort constraints in its code to collect predicates in axiom clauses.
paulson
parents: 21254
diff changeset
   372
11996e938dfe Includes type:sort constraints in its code to collect predicates in axiom clauses.
paulson
parents: 21254
diff changeset
   373
(*Higher-order clauses have only the predicates hBOOL and type classes.*)
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   374
fun preds_of_clauses clauses clsrel_clauses arity_clauses =
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   375
    Symtab.dest
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   376
        (foldl RC.add_classrelClause_preds
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   377
               (foldl RC.add_arityClause_preds
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   378
                      (foldl add_clause_preds Symtab.empty clauses)
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   379
                      arity_clauses)
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   380
               clsrel_clauses)
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   381
18440
72ee07f4b56b Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents: 18356
diff changeset
   382
72ee07f4b56b Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents: 18356
diff changeset
   383
(**********************************************************************)
19198
e6f1ff40ba99 Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents: 19130
diff changeset
   384
(* write clauses to files                                             *)
e6f1ff40ba99 Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents: 19130
diff changeset
   385
(**********************************************************************)
e6f1ff40ba99 Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents: 19130
diff changeset
   386
21573
8a7a68c0096c Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents: 21561
diff changeset
   387
val init_counters =
8a7a68c0096c Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents: 21561
diff changeset
   388
    Symtab.make [("c_COMBI", 0), ("c_COMBK", 0),
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   389
                 ("c_COMBB", 0), ("c_COMBC", 0),
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   390
                 ("c_COMBS", 0), ("c_COMBB_e", 0),
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   391
                 ("c_COMBC_e", 0), ("c_COMBS_e", 0)];
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   392
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   393
fun count_combterm (CombConst(c,tp,_), ct) =
21573
8a7a68c0096c Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents: 21561
diff changeset
   394
     (case Symtab.lookup ct c of NONE => ct  (*no counter*)
8a7a68c0096c Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents: 21561
diff changeset
   395
                               | SOME n => Symtab.update (c,n+1) ct)
8a7a68c0096c Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents: 21561
diff changeset
   396
  | count_combterm (CombVar(v,tp), ct) = ct
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   397
  | count_combterm (CombApp(t1,t2), ct) = count_combterm(t1, count_combterm(t2, ct));
21573
8a7a68c0096c Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents: 21561
diff changeset
   398
8a7a68c0096c Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents: 21561
diff changeset
   399
fun count_literal (Literal(_,t), ct) = count_combterm(t,ct);
8a7a68c0096c Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents: 21561
diff changeset
   400
8a7a68c0096c Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents: 21561
diff changeset
   401
fun count_clause (Clause{literals,...}, ct) = foldl count_literal ct literals;
8a7a68c0096c Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents: 21561
diff changeset
   402
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   403
fun count_user_clause user_lemmas (Clause{axiom_name,literals,...}, ct) =
21573
8a7a68c0096c Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents: 21561
diff changeset
   404
  if axiom_name mem_string user_lemmas then foldl count_literal ct literals
8a7a68c0096c Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents: 21561
diff changeset
   405
  else ct;
8a7a68c0096c Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents: 21561
diff changeset
   406
20791
497e1c9d4a9f Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents: 20660
diff changeset
   407
val cnf_helper_thms = ResAxioms.cnf_rules_pairs o (map ResAxioms.pairname)
20644
ff938c7b15e8 Introduced combinators B', C' and S'.
mengj
parents: 20421
diff changeset
   408
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   409
fun get_helper_clauses thy isFO (conjectures, axclauses, user_lemmas) =
23386
9255c1a75ba9 Now also handles FO problems
paulson
parents: 22851
diff changeset
   410
  if isFO then []  (*first-order*)
9255c1a75ba9 Now also handles FO problems
paulson
parents: 22851
diff changeset
   411
  else
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   412
    let val ct0 = foldl count_clause init_counters conjectures
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   413
        val ct = foldl (count_user_clause user_lemmas) ct0 axclauses
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   414
        fun needed c = valOf (Symtab.lookup ct c) > 0
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   415
        val IK = if needed "c_COMBI" orelse needed "c_COMBK"
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   416
                 then (Output.debug (fn () => "Include combinator I K"); cnf_helper_thms [comb_I,comb_K])
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   417
                 else []
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   418
        val BC = if needed "c_COMBB" orelse needed "c_COMBC"
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   419
                 then (Output.debug (fn () => "Include combinator B C"); cnf_helper_thms [comb_B,comb_C])
21135
07549f79d19c Numerous cosmetic changes.
paulson
parents: 21108
diff changeset
   420
                 else []
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   421
        val S = if needed "c_COMBS"
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   422
                then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms [comb_S])
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   423
                else []
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   424
        val B'C' = if needed "c_COMBB_e" orelse needed "c_COMBC_e"
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   425
                   then (Output.debug (fn () => "Include combinator B' C'"); cnf_helper_thms [comb_B', comb_C'])
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   426
                   else []
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   427
        val S' = if needed "c_COMBS_e"
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   428
                 then (Output.debug (fn () => "Include combinator S'"); cnf_helper_thms [comb_S'])
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   429
                 else []
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   430
        val other = cnf_helper_thms [ext,fequal_imp_equal,equal_imp_fequal]
20791
497e1c9d4a9f Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents: 20660
diff changeset
   431
    in
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   432
        map #2 (make_axiom_clauses thy (other @ IK @ BC @ S @ B'C' @ S'))
23386
9255c1a75ba9 Now also handles FO problems
paulson
parents: 22851
diff changeset
   433
    end;
20791
497e1c9d4a9f Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents: 20660
diff changeset
   434
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   435
(*Find the minimal arity of each function mentioned in the term. Also, note which uses
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   436
  are not at top level, to see if hBOOL is needed.*)
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   437
fun count_constants_term toplev t =
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   438
  let val (head, args) = strip_comb t
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   439
      val n = length args
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   440
      val _ = List.app (count_constants_term false) args
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   441
  in
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   442
      case head of
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   443
          CombConst (a,_,_) => (*predicate or function version of "equal"?*)
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   444
            let val a = if a="equal" andalso not toplev then "c_fequal" else a
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   445
            in
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   446
              const_min_arity := Symtab.map_default (a,n) (curry Int.min n) (!const_min_arity);
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   447
              if toplev then ()
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   448
              else const_needs_hBOOL := Symtab.update (a,true) (!const_needs_hBOOL)
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   449
            end
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   450
        | ts => ()
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   451
  end;
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   452
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   453
(*A literal is a top-level term*)
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   454
fun count_constants_lit (Literal (_,t)) = count_constants_term true t;
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   455
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   456
fun count_constants_clause (Clause{literals,...}) = List.app count_constants_lit literals;
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   457
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   458
fun display_arity (c,n) =
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   459
  Output.debug (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   460
                (if needs_hBOOL c then " needs hBOOL" else ""));
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   461
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   462
fun count_constants (conjectures, axclauses, helper_clauses) =
24385
ab62948281a9 Deleted the partially-typed translation and the combinator code.
paulson
parents: 24323
diff changeset
   463
  if !minimize_applies then
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   464
    (const_min_arity := Symtab.empty;
23386
9255c1a75ba9 Now also handles FO problems
paulson
parents: 22851
diff changeset
   465
     const_needs_hBOOL := Symtab.empty;
9255c1a75ba9 Now also handles FO problems
paulson
parents: 22851
diff changeset
   466
     List.app count_constants_clause conjectures;
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   467
     List.app count_constants_clause axclauses;
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   468
     List.app count_constants_clause helper_clauses;
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   469
     List.app display_arity (Symtab.dest (!const_min_arity)))
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   470
  else ();
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   471
20791
497e1c9d4a9f Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents: 20660
diff changeset
   472
(* tptp format *)
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   473
19198
e6f1ff40ba99 Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents: 19130
diff changeset
   474
(* write TPTP format to a single file *)
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   475
fun tptp_write_file thy isFO thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas =
23386
9255c1a75ba9 Now also handles FO problems
paulson
parents: 22851
diff changeset
   476
    let val _ = Output.debug (fn () => ("Preparing to write the TPTP file " ^ filename))
9255c1a75ba9 Now also handles FO problems
paulson
parents: 22851
diff changeset
   477
        val _ = RC.dfg_format := false
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   478
        val conjectures = make_conjecture_clauses thy thms
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   479
        val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses thy ax_tuples)
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   480
        val helper_clauses = get_helper_clauses thy isFO (conjectures, axclauses, user_lemmas)
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   481
        val _ = count_constants (conjectures, axclauses, helper_clauses);
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   482
        val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp conjectures)
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   483
        val tfree_clss = map RC.tptp_tfree_clause (foldl (op union_string) [] tfree_litss)
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   484
        val out = TextIO.openOut filename
19198
e6f1ff40ba99 Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents: 19130
diff changeset
   485
    in
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   486
        List.app (curry TextIO.output out o #1 o clause2tptp) axclauses;
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   487
        RC.writeln_strs out tfree_clss;
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   488
        RC.writeln_strs out tptp_clss;
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   489
        List.app (curry TextIO.output out o RC.tptp_classrelClause) classrel_clauses;
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   490
        List.app (curry TextIO.output out o RC.tptp_arity_clause) arity_clauses;
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   491
        List.app (curry TextIO.output out o #1 o clause2tptp) helper_clauses;
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   492
        TextIO.closeOut out;
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   493
        clnames
19198
e6f1ff40ba99 Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents: 19130
diff changeset
   494
    end;
e6f1ff40ba99 Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents: 19130
diff changeset
   495
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   496
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   497
(* dfg format *)
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   498
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   499
fun dfg_write_file thy isFO thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas =
23386
9255c1a75ba9 Now also handles FO problems
paulson
parents: 22851
diff changeset
   500
    let val _ = Output.debug (fn () => ("Preparing to write the DFG file " ^ filename))
9255c1a75ba9 Now also handles FO problems
paulson
parents: 22851
diff changeset
   501
        val _ = RC.dfg_format := true
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   502
        val conjectures = make_conjecture_clauses thy thms
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   503
        val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses thy ax_tuples)
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   504
        val helper_clauses = get_helper_clauses thy isFO (conjectures, axclauses, user_lemmas)
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   505
        val _ = count_constants (conjectures, axclauses, helper_clauses);
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   506
        val (dfg_clss, tfree_litss) = ListPair.unzip (map clause2dfg conjectures)
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   507
        and probname = Path.implode (Path.base (Path.explode filename))
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   508
        val axstrs = map (#1 o clause2dfg) axclauses
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   509
        val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss)
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   510
        val out = TextIO.openOut filename
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   511
        val helper_clauses_strs = map (#1 o clause2dfg) helper_clauses
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   512
        val (funcs,cl_preds) = decls_of_clauses (helper_clauses @ conjectures @ axclauses) arity_clauses
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   513
        and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   514
    in
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   515
        TextIO.output (out, RC.string_of_start probname);
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   516
        TextIO.output (out, RC.string_of_descrip probname);
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   517
        TextIO.output (out, RC.string_of_symbols
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   518
                              (RC.string_of_funcs funcs)
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   519
                              (RC.string_of_preds (cl_preds @ ty_preds)));
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   520
        TextIO.output (out, "list_of_clauses(axioms,cnf).\n");
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   521
        RC.writeln_strs out axstrs;
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   522
        List.app (curry TextIO.output out o RC.dfg_classrelClause) classrel_clauses;
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   523
        List.app (curry TextIO.output out o RC.dfg_arity_clause) arity_clauses;
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   524
        RC.writeln_strs out helper_clauses_strs;
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   525
        TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n");
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   526
        RC.writeln_strs out tfree_clss;
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   527
        RC.writeln_strs out dfg_clss;
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   528
        TextIO.output (out, "end_of_list.\n\n");
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   529
        (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   530
        TextIO.output (out, "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n");
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   531
        TextIO.output (out, "end_problem.\n");
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   532
        TextIO.closeOut out;
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   533
        clnames
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   534
    end;
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   535
21254
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents: 21135
diff changeset
   536
end