src/HOL/Tools/res_hol_clause.ML
author paulson
Tue, 21 Aug 2007 18:27:14 +0200
changeset 24385 ab62948281a9
parent 24323 9aa7b5708eac
child 24937 340523598914
permissions -rw-r--r--
Deleted the partially-typed translation and the combinator code. Minimize_applies now uses the same translation code, which handles both cases anyway.
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,
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   100
                    ctypes_sorts: (RC.typ_var * Term.sort) list,
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   101
                    ctvar_type_literals: RC.type_literal list,
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   102
                    ctfree_type_literals: RC.type_literal 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
   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
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
(* 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
   107
(*********************************************************************)
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
   108
21561
cfd2258f0b23 Tidied code. Bool constructor is not needed.
paulson
parents: 21513
diff changeset
   109
fun isFalse (Literal(pol, CombConst(c,_,_))) =
20360
8c8c824dccdc tidying
paulson
parents: 20281
diff changeset
   110
      (pol andalso c = "c_False") orelse
8c8c824dccdc tidying
paulson
parents: 20281
diff changeset
   111
      (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
   112
  | 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
   113
21561
cfd2258f0b23 Tidied code. Bool constructor is not needed.
paulson
parents: 21513
diff changeset
   114
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
   115
      (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
   116
      (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
   117
  | isTrue _ = false;
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   118
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   119
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
   120
18440
72ee07f4b56b Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents: 18356
diff changeset
   121
fun type_of (Type (a, Ts)) =
21561
cfd2258f0b23 Tidied code. Bool constructor is not needed.
paulson
parents: 21513
diff changeset
   122
      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
   123
      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
   124
  | 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
   125
      (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
   126
  | 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
   127
      (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
   128
and types_of Ts =
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   129
      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
   130
      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
   131
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
   132
(* same as above, but no gathering of sort information *)
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   133
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
   134
      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
   135
  | 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
   136
  | 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
   137
18356
443717b3a9ad Added new type embedding methods for translating HOL clauses.
mengj
parents: 18276
diff changeset
   138
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   139
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
   140
      let val (tp,ts) = type_of t
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   141
      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
   142
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
   143
(* 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
   144
fun combterm_of thy (Const(c,t)) =
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   145
      let val (tp,ts,tvar_list) = const_type_of thy (c,t)
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   146
          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
   147
      in  (c',ts)  end
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   148
  | combterm_of thy (Free(v,t)) =
21513
9e9fff87dc6c Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents: 21509
diff changeset
   149
      let val (tp,ts) = type_of t
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   150
          val v' = if RC.isMeta v then CombVar(RC.make_schematic_var(v,0),tp)
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   151
                   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
   152
      in  (v',ts)  end
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   153
  | combterm_of thy (Var(v,t)) =
21513
9e9fff87dc6c Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents: 21509
diff changeset
   154
      let val (tp,ts) = type_of t
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   155
          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
   156
      in  (v',ts)  end
24385
ab62948281a9 Deleted the partially-typed translation and the combinator code.
paulson
parents: 24323
diff changeset
   157
  | combterm_of thy (P $ Q) =
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   158
      let val (P',tsP) = combterm_of thy P
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   159
          val (Q',tsQ) = combterm_of thy Q
24385
ab62948281a9 Deleted the partially-typed translation and the combinator code.
paulson
parents: 24323
diff changeset
   160
      in  (CombApp(P',Q'), tsP union tsQ)  end
ab62948281a9 Deleted the partially-typed translation and the combinator code.
paulson
parents: 24323
diff changeset
   161
  | 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
   162
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   163
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
   164
  | 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
   165
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   166
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
   167
  | literals_of_term1 thy args (Const("op |",_) $ P $ Q) =
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   168
      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
   169
  | literals_of_term1 thy (lits,ts) P =
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   170
      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
   171
      in
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   172
          (Literal(pol,pred)::lits, ts union ts')
21509
6c5755ad9cae ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents: 21470
diff changeset
   173
      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
   174
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   175
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
   176
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
   177
(* making axiom and conjecture clauses *)
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   178
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
   179
    let val (lits,ctypes_sorts) = literals_of_term thy (prop_of th)
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   180
        val (ctvar_lits,ctfree_lits) = RC.add_typs_aux 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
   181
    in
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   182
        if forall isFalse lits
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   183
        then error "Problem too trivial for resolution (empty clause)"
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   184
        else
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   185
            Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, kind = kind,
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   186
                    literals = lits, ctypes_sorts = ctypes_sorts,
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   187
                    ctvar_type_literals = ctvar_lits,
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   188
                    ctfree_type_literals = ctfree_lits}
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
   189
    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
   190
20016
9a005f7d95e6 Literals aren't sorted any more.
mengj
parents: 19964
diff changeset
   191
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   192
fun add_axiom_clause thy ((th,(name,id)), pairs) =
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   193
  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
   194
  in
8a7a68c0096c Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents: 21561
diff changeset
   195
      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
   196
  end;
19354
aebf9dddccd7 tptp_write_file accepts axioms as thm.
mengj
parents: 19198
diff changeset
   197
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   198
fun make_axiom_clauses thy = foldl (add_axiom_clause thy) [];
19354
aebf9dddccd7 tptp_write_file accepts axioms as thm.
mengj
parents: 19198
diff changeset
   199
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   200
fun make_conjecture_clauses_aux _ _ [] = []
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   201
  | make_conjecture_clauses_aux thy n (th::ths) =
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   202
      make_clause thy (n,"conjecture", RC.Conjecture, th) ::
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   203
      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
   204
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   205
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
   206
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
(**********************************************************************)
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
   209
(* 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
   210
(* TPTP used by Vampire and E                                         *)
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   211
(* 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
   212
(**********************************************************************)
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
   213
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   214
(*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
   215
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
   216
  | result_type _ = raise ERROR "result_type"
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   217
21513
9e9fff87dc6c Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents: 21509
diff changeset
   218
fun type_of_combterm (CombConst(c,tp,_)) = tp
9e9fff87dc6c Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents: 21509
diff changeset
   219
  | 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
   220
  | 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
   221
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   222
(*gets the head of a combinator application, along with the list of arguments*)
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   223
fun strip_comb u =
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   224
    let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   225
        |   stripc  x =  x
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   226
    in  stripc(u,[])  end;
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   227
22851
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   228
val type_wrapper = "ti";
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   229
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   230
fun head_needs_hBOOL (CombConst(c,_,_)) = needs_hBOOL c
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   231
  | head_needs_hBOOL _ = true;
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   232
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   233
fun wrap_type (s, tp) =
22851
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   234
  if !typ_level=T_FULL then
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   235
      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
   236
  else s;
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   237
22851
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   238
fun apply ss = "hAPP" ^ RC.paren_pack ss;
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   239
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   240
fun rev_apply (v, []) = v
22851
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   241
  | rev_apply (v, arg::args) = apply [rev_apply (v, args), arg];
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   242
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   243
fun string_apply (v, args) = rev_apply (v, rev args);
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   244
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   245
(*Apply an operator to the argument strings, using either the "apply" operator or
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   246
  direct function application.*)
22851
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   247
fun string_of_applic (CombConst(c,tp,tvars), args) =
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   248
      let val c = if c = "equal" then "c_fequal" else c
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   249
          val nargs = min_arity_of c
22851
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   250
          val args1 = List.take(args, nargs)
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   251
            handle Subscript => raise ERROR ("string_of_applic: " ^ c ^ " has arity " ^
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   252
                                             Int.toString nargs ^ " but is applied to " ^
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   253
                                             space_implode ", " args)
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   254
          val args2 = List.drop(args, nargs)
22851
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   255
          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
   256
                      else []
21513
9e9fff87dc6c Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents: 21509
diff changeset
   257
      in
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   258
          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
   259
      end
22851
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   260
  | string_of_applic (CombVar(v,tp), args) = string_apply (v, args)
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   261
  | string_of_applic _ = raise ERROR "string_of_applic";
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   262
22851
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   263
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
   264
24385
ab62948281a9 Deleted the partially-typed translation and the combinator code.
paulson
parents: 24323
diff changeset
   265
fun string_of_combterm t =
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   266
  let val (head, args) = strip_comb t
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   267
  in  wrap_type_if (head,
24385
ab62948281a9 Deleted the partially-typed translation and the combinator code.
paulson
parents: 24323
diff changeset
   268
                    string_of_applic (head, map string_of_combterm args),
22851
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   269
                    type_of_combterm t)
7b7d6e1c70b6 First-order variant of the fully-typed translation
paulson
parents: 22825
diff changeset
   270
  end;
18356
443717b3a9ad Added new type embedding methods for translating HOL clauses.
mengj
parents: 18276
diff changeset
   271
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   272
(*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
   273
fun boolify t = "hBOOL" ^ RC.paren_pack [string_of_combterm t];
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   274
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   275
fun string_of_predicate t =
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   276
  case t of
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   277
      (CombApp(CombApp(CombConst("equal",_,_), t1), t2)) =>
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   278
          (*DFG only: new TPTP prefers infix equality*)
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   279
          ("equal" ^ RC.paren_pack [string_of_combterm t1, string_of_combterm t2])
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   280
    | _ =>
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   281
          case #1 (strip_comb t) of
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   282
              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
   283
            | _ => boolify t;
18356
443717b3a9ad Added new type embedding methods for translating HOL clauses.
mengj
parents: 18276
diff changeset
   284
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   285
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
   286
    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
   287
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   288
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
   289
    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
   290
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
   291
21561
cfd2258f0b23 Tidied code. Bool constructor is not needed.
paulson
parents: 21513
diff changeset
   292
(*** tptp format ***)
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   293
21513
9e9fff87dc6c Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents: 21509
diff changeset
   294
fun tptp_of_equality pol (t1,t2) =
9e9fff87dc6c Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents: 21509
diff changeset
   295
  let val eqop = if pol then " = " else " != "
9e9fff87dc6c Conversion of "equal" to "=" for TSTP format; big tidy-up
paulson
parents: 21509
diff changeset
   296
  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
   297
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   298
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
   299
      tptp_of_equality pol (t1,t2)
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   300
  | tptp_literal (Literal(pol,pred)) =
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   301
      RC.tptp_sign pol (string_of_predicate pred);
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   302
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   303
(*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
   304
  the latter should only occur in conjecture clauses.*)
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   305
fun tptp_type_lits (Clause cls) =
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
   306
    let val lits = map tptp_literal (#literals cls)
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   307
        val ctvar_lits_strs = map RC.tptp_of_typeLit (#ctvar_type_literals cls)
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   308
        val ctfree_lits = map RC.tptp_of_typeLit (#ctfree_type_literals cls)
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
    in
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   310
        (ctvar_lits_strs @ lits, ctfree_lits)
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   311
    end;
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   312
21509
6c5755ad9cae ATP linkup now generates "new TPTP" rather than "old TPTP"
paulson
parents: 21470
diff changeset
   313
fun clause2tptp (cls as Clause{axiom_name,clause_id,kind,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
   314
    let val (lits,ctfree_lits) = tptp_type_lits cls
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   315
        val cls_str = RC.gen_tptp_cls(clause_id,axiom_name,kind,lits)
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
   316
    in
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   317
        (cls_str,ctfree_lits)
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
   318
    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
   319
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
   320
21561
cfd2258f0b23 Tidied code. Bool constructor is not needed.
paulson
parents: 21513
diff changeset
   321
(*** dfg format ***)
cfd2258f0b23 Tidied code. Bool constructor is not needed.
paulson
parents: 21513
diff changeset
   322
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   323
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
   324
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   325
fun dfg_clause_aux (Clause{literals, ctypes_sorts, ...}) =
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   326
  let val lits = map dfg_literal literals
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   327
      val (tvar_lits,tfree_lits) = RC.add_typs_aux ctypes_sorts
22825
bd774e01d6d5 Fixing bugs in the partial-typed and fully-typed translations
paulson
parents: 22130
diff changeset
   328
      val tvar_lits_strs = map RC.dfg_of_typeLit tvar_lits
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   329
      val tfree_lits = map RC.dfg_of_typeLit tfree_lits
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   330
  in
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   331
      (tvar_lits_strs @ lits, tfree_lits)
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   332
  end;
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   333
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   334
fun get_uvars (CombConst _) vars = vars
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   335
  | get_uvars (CombVar(v,_)) vars = (v::vars)
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   336
  | 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
   337
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   338
fun get_uvars_l (Literal(_,c)) = get_uvars c [];
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   339
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   340
fun dfg_vars (Clause {literals,...}) = RC.union_all (map get_uvars_l literals);
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   341
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   342
fun clause2dfg (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   343
    let val (lits,tfree_lits) = dfg_clause_aux cls
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   344
        val vars = dfg_vars cls
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   345
        val tvars = RC.get_tvar_strs ctypes_sorts
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   346
        val knd = RC.name_of_kind kind
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   347
        val lits_str = commas lits
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   348
        val cls_str = RC.gen_dfg_cls(clause_id, axiom_name, knd, lits_str, tvars@vars)
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   349
    in (cls_str, tfree_lits) end;
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   350
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   351
(** For DFG format: accumulate function and predicate declarations **)
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   352
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   353
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
   354
22825
bd774e01d6d5 Fixing bugs in the partial-typed and fully-typed translations
paulson
parents: 22130
diff changeset
   355
fun add_decls (CombConst(c,tp,tvars), (funcs,preds)) =
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   356
      if c = "equal" then (addtypes tvars funcs, preds)
21561
cfd2258f0b23 Tidied code. Bool constructor is not needed.
paulson
parents: 21513
diff changeset
   357
      else
24385
ab62948281a9 Deleted the partially-typed translation and the combinator code.
paulson
parents: 24323
diff changeset
   358
	let val arity = min_arity_of c
ab62948281a9 Deleted the partially-typed translation and the combinator code.
paulson
parents: 24323
diff changeset
   359
	    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
   360
	    val addit = Symtab.update(c, arity+ntys)
ab62948281a9 Deleted the partially-typed translation and the combinator code.
paulson
parents: 24323
diff changeset
   361
	in
ab62948281a9 Deleted the partially-typed translation and the combinator code.
paulson
parents: 24323
diff changeset
   362
	    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
   363
	    else (addtypes tvars funcs, addit preds)
ab62948281a9 Deleted the partially-typed translation and the combinator code.
paulson
parents: 24323
diff changeset
   364
	end
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   365
  | add_decls (CombVar(_,ctp), (funcs,preds)) =
22078
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   366
      (RC.add_foltype_funcs (ctp,funcs), preds)
5084f53cef39 Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
paulson
parents: 22064
diff changeset
   367
  | 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
   368
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   369
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
   370
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   371
fun add_clause_decls (Clause {literals, ...}, decls) =
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   372
    foldl add_literal_decls decls literals
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   373
    handle Symtab.DUP a => raise ERROR ("function " ^ a ^ " has multiple arities")
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   374
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   375
fun decls_of_clauses clauses arity_clauses =
24385
ab62948281a9 Deleted the partially-typed translation and the combinator code.
paulson
parents: 24323
diff changeset
   376
  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
   377
      val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   378
      val (functab,predtab) = (foldl add_clause_decls (init_functab, init_predtab) clauses)
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   379
  in
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   380
      (Symtab.dest (foldl RC.add_arityClause_funcs functab arity_clauses),
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   381
       Symtab.dest predtab)
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   382
  end;
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   383
21398
11996e938dfe Includes type:sort constraints in its code to collect predicates in axiom clauses.
paulson
parents: 21254
diff changeset
   384
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
   385
  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
   386
  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
   387
11996e938dfe Includes type:sort constraints in its code to collect predicates in axiom clauses.
paulson
parents: 21254
diff changeset
   388
(*Higher-order clauses have only the predicates hBOOL and type classes.*)
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   389
fun preds_of_clauses clauses clsrel_clauses arity_clauses =
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   390
    Symtab.dest
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   391
        (foldl RC.add_classrelClause_preds
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   392
               (foldl RC.add_arityClause_preds
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   393
                      (foldl add_clause_preds Symtab.empty clauses)
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   394
                      arity_clauses)
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   395
               clsrel_clauses)
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   396
18440
72ee07f4b56b Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents: 18356
diff changeset
   397
72ee07f4b56b Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents: 18356
diff changeset
   398
(**********************************************************************)
19198
e6f1ff40ba99 Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents: 19130
diff changeset
   399
(* write clauses to files                                             *)
e6f1ff40ba99 Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents: 19130
diff changeset
   400
(**********************************************************************)
e6f1ff40ba99 Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents: 19130
diff changeset
   401
21573
8a7a68c0096c Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents: 21561
diff changeset
   402
val init_counters =
8a7a68c0096c Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents: 21561
diff changeset
   403
    Symtab.make [("c_COMBI", 0), ("c_COMBK", 0),
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   404
                 ("c_COMBB", 0), ("c_COMBC", 0),
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   405
                 ("c_COMBS", 0), ("c_COMBB_e", 0),
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   406
                 ("c_COMBC_e", 0), ("c_COMBS_e", 0)];
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   407
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   408
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
   409
     (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
   410
                               | 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
   411
  | 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
   412
  | 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
   413
8a7a68c0096c Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents: 21561
diff changeset
   414
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
   415
8a7a68c0096c Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents: 21561
diff changeset
   416
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
   417
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   418
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
   419
  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
   420
  else ct;
8a7a68c0096c Removed the references for counting combinators. Instead they are counted in actual clauses.
paulson
parents: 21561
diff changeset
   421
20791
497e1c9d4a9f Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents: 20660
diff changeset
   422
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
   423
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   424
fun get_helper_clauses thy isFO (conjectures, axclauses, user_lemmas) =
23386
9255c1a75ba9 Now also handles FO problems
paulson
parents: 22851
diff changeset
   425
  if isFO then []  (*first-order*)
9255c1a75ba9 Now also handles FO problems
paulson
parents: 22851
diff changeset
   426
  else
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   427
    let val ct0 = foldl count_clause init_counters conjectures
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   428
        val ct = foldl (count_user_clause user_lemmas) ct0 axclauses
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   429
        fun needed c = valOf (Symtab.lookup ct c) > 0
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   430
        val IK = if needed "c_COMBI" orelse needed "c_COMBK"
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   431
                 then (Output.debug (fn () => "Include combinator I K"); cnf_helper_thms [comb_I,comb_K])
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   432
                 else []
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   433
        val BC = if needed "c_COMBB" orelse needed "c_COMBC"
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   434
                 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
   435
                 else []
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   436
        val S = if needed "c_COMBS"
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   437
                then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms [comb_S])
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   438
                else []
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   439
        val B'C' = if needed "c_COMBB_e" orelse needed "c_COMBC_e"
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   440
                   then (Output.debug (fn () => "Include combinator B' C'"); cnf_helper_thms [comb_B', comb_C'])
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   441
                   else []
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   442
        val S' = if needed "c_COMBS_e"
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   443
                 then (Output.debug (fn () => "Include combinator S'"); cnf_helper_thms [comb_S'])
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   444
                 else []
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   445
        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
   446
    in
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   447
        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
   448
    end;
20791
497e1c9d4a9f Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents: 20660
diff changeset
   449
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   450
(*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
   451
  are not at top level, to see if hBOOL is needed.*)
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   452
fun count_constants_term toplev t =
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   453
  let val (head, args) = strip_comb t
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   454
      val n = length args
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   455
      val _ = List.app (count_constants_term false) args
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   456
  in
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   457
      case head of
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   458
          CombConst (a,_,_) => (*predicate or function version of "equal"?*)
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   459
            let val a = if a="equal" andalso not toplev then "c_fequal" else a
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   460
            in
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   461
              const_min_arity := Symtab.map_default (a,n) (curry Int.min n) (!const_min_arity);
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   462
              if toplev then ()
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   463
              else const_needs_hBOOL := Symtab.update (a,true) (!const_needs_hBOOL)
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   464
            end
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   465
        | ts => ()
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   466
  end;
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   467
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   468
(*A literal is a top-level term*)
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   469
fun count_constants_lit (Literal (_,t)) = count_constants_term true t;
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   470
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   471
fun count_constants_clause (Clause{literals,...}) = List.app count_constants_lit literals;
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   472
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   473
fun display_arity (c,n) =
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   474
  Output.debug (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   475
                (if needs_hBOOL c then " needs hBOOL" else ""));
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   476
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   477
fun count_constants (conjectures, axclauses, helper_clauses) =
24385
ab62948281a9 Deleted the partially-typed translation and the combinator code.
paulson
parents: 24323
diff changeset
   478
  if !minimize_applies then
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   479
    (const_min_arity := Symtab.empty;
23386
9255c1a75ba9 Now also handles FO problems
paulson
parents: 22851
diff changeset
   480
     const_needs_hBOOL := Symtab.empty;
9255c1a75ba9 Now also handles FO problems
paulson
parents: 22851
diff changeset
   481
     List.app count_constants_clause conjectures;
22064
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   482
     List.app count_constants_clause axclauses;
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   483
     List.app count_constants_clause helper_clauses;
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   484
     List.app display_arity (Symtab.dest (!const_min_arity)))
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   485
  else ();
3d716cc9bd7a optimized translation of HO problems
paulson
parents: 21858
diff changeset
   486
20791
497e1c9d4a9f Combinator axioms are now from Isabelle theorems, no need to use helper files.
mengj
parents: 20660
diff changeset
   487
(* tptp format *)
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   488
19198
e6f1ff40ba99 Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents: 19130
diff changeset
   489
(* write TPTP format to a single file *)
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   490
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
   491
    let val _ = Output.debug (fn () => ("Preparing to write the TPTP file " ^ filename))
9255c1a75ba9 Now also handles FO problems
paulson
parents: 22851
diff changeset
   492
        val _ = RC.dfg_format := false
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   493
        val conjectures = make_conjecture_clauses thy thms
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   494
        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
   495
        val helper_clauses = get_helper_clauses thy isFO (conjectures, axclauses, user_lemmas)
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   496
        val _ = count_constants (conjectures, axclauses, helper_clauses);
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   497
        val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp conjectures)
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   498
        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
   499
        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
   500
    in
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   501
        List.app (curry TextIO.output out o #1 o clause2tptp) axclauses;
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   502
        RC.writeln_strs out tfree_clss;
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   503
        RC.writeln_strs out tptp_clss;
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   504
        List.app (curry TextIO.output out o RC.tptp_classrelClause) classrel_clauses;
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   505
        List.app (curry TextIO.output out o RC.tptp_arity_clause) arity_clauses;
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   506
        List.app (curry TextIO.output out o #1 o clause2tptp) helper_clauses;
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   507
        TextIO.closeOut out;
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   508
        clnames
19198
e6f1ff40ba99 Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents: 19130
diff changeset
   509
    end;
e6f1ff40ba99 Added tptp_write_file to write all necessary ATP input clauses to one file.
mengj
parents: 19130
diff changeset
   510
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   511
20644
ff938c7b15e8 Introduced combinators B', C' and S'.
mengj
parents: 20421
diff changeset
   512
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   513
(* dfg format *)
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   514
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   515
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
   516
    let val _ = Output.debug (fn () => ("Preparing to write the DFG file " ^ filename))
9255c1a75ba9 Now also handles FO problems
paulson
parents: 22851
diff changeset
   517
        val _ = RC.dfg_format := true
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   518
        val conjectures = make_conjecture_clauses thy thms
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   519
        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
   520
        val helper_clauses = get_helper_clauses thy isFO (conjectures, axclauses, user_lemmas)
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   521
        val _ = count_constants (conjectures, axclauses, helper_clauses);
24323
9aa7b5708eac removed stateful init: operations take proper theory argument;
wenzelm
parents: 24311
diff changeset
   522
        val (dfg_clss, tfree_litss) = ListPair.unzip (map clause2dfg conjectures)
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   523
        and probname = Path.implode (Path.base (Path.explode filename))
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   524
        val axstrs = map (#1 o clause2dfg) axclauses
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   525
        val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss)
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   526
        val out = TextIO.openOut filename
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   527
        val helper_clauses_strs = map (#1 o clause2dfg) helper_clauses
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   528
        val (funcs,cl_preds) = decls_of_clauses (helper_clauses @ conjectures @ axclauses) arity_clauses
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   529
        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
   530
    in
24311
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   531
        TextIO.output (out, RC.string_of_start probname);
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   532
        TextIO.output (out, RC.string_of_descrip probname);
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   533
        TextIO.output (out, RC.string_of_symbols
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   534
                              (RC.string_of_funcs funcs)
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   535
                              (RC.string_of_preds (cl_preds @ ty_preds)));
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   536
        TextIO.output (out, "list_of_clauses(axioms,cnf).\n");
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   537
        RC.writeln_strs out axstrs;
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   538
        List.app (curry TextIO.output out o RC.dfg_classrelClause) classrel_clauses;
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   539
        List.app (curry TextIO.output out o RC.dfg_arity_clause) arity_clauses;
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   540
        RC.writeln_strs out helper_clauses_strs;
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   541
        TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n");
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   542
        RC.writeln_strs out tfree_clss;
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   543
        RC.writeln_strs out dfg_clss;
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   544
        TextIO.output (out, "end_of_list.\n\n");
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   545
        (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   546
        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
   547
        TextIO.output (out, "end_problem.\n");
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   548
        TextIO.closeOut out;
d6864b34eecd proper signature;
wenzelm
parents: 24215
diff changeset
   549
        clnames
19720
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   550
    end;
f68f6f958a1d HOL problems now have DFG output format.
mengj
parents: 19491
diff changeset
   551
21254
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents: 21135
diff changeset
   552
end