author | mengj |
Thu, 23 Feb 2006 13:00:18 +0100 | |
changeset 19130 | b23479b80828 |
parent 18856 | 4669dec681f4 |
child 19198 | e6f1ff40ba99 |
permissions | -rw-r--r-- |
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
|
1 |
(* ID: $Id$ |
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 |
|
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
|
4 |
FOL clauses translated from HOL formulae. Combinators are used to represent lambda terms. |
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
|
5 |
|
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
|
6 |
*) |
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
|
7 |
|
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
|
8 |
structure ResHolClause = |
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 |
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
|
11 |
|
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
|
12 |
|
18276
c62ec94e326e
Added flags for setting and detecting whether a problem needs combinators.
mengj
parents:
18200
diff
changeset
|
13 |
val include_combS = ref false; |
c62ec94e326e
Added flags for setting and detecting whether a problem needs combinators.
mengj
parents:
18200
diff
changeset
|
14 |
val include_min_comb = ref false; |
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
|
15 |
|
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
16 |
val const_typargs = ref (Library.K [] : (string*typ -> typ list)); |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
17 |
|
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
18 |
fun init thy = (include_combS:=false;include_min_comb:=false;const_typargs := Sign.const_typargs thy); |
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
|
19 |
|
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
|
20 |
(**********************************************************************) |
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
|
21 |
(* convert a Term.term with lambdas into a Term.term with combinators *) |
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
|
22 |
(**********************************************************************) |
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
|
23 |
|
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
|
24 |
fun is_free (Bound(a)) n = (a = n) |
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
|
25 |
| is_free (Abs(x,_,b)) n = (is_free b (n+1)) |
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
|
26 |
| is_free (P $ Q) n = ((is_free P n) orelse (is_free Q n)) |
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
|
27 |
| is_free _ _ = 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
|
28 |
|
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
|
29 |
|
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
|
30 |
exception LAM2COMB of term; |
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
|
31 |
|
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
|
32 |
exception BND of term; |
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
|
33 |
|
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
|
34 |
fun decre_bndVar (Bound n) = Bound (n-1) |
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
|
35 |
| decre_bndVar (P $ Q) = (decre_bndVar P) $ (decre_bndVar Q) |
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
|
36 |
| decre_bndVar t = |
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
|
37 |
case t of Const(_,_) => t |
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
|
38 |
| Free(_,_) => t |
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 |
| Var(_,_) => t |
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
|
40 |
| Abs(_,_,_) => raise BND(t); (*should not occur*) |
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 |
|
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 |
|
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
|
43 |
(*******************************************) |
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
|
44 |
fun lam2comb (Abs(x,tp,Bound 0)) _ = |
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
|
45 |
let val tpI = Type("fun",[tp,tp]) |
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
|
46 |
in |
18276
c62ec94e326e
Added flags for setting and detecting whether a problem needs combinators.
mengj
parents:
18200
diff
changeset
|
47 |
include_min_comb:=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
|
48 |
Const("COMBI",tpI) |
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
|
49 |
end |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
50 |
| lam2comb (Abs(x,tp,Bound n)) Bnds = |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
51 |
let val (Bound n') = decre_bndVar (Bound n) |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
52 |
val tb = List.nth(Bnds,n') |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
53 |
val tK = Type("fun",[tb,Type("fun",[tp,tb])]) |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
54 |
in |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
55 |
include_min_comb:=true; |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
56 |
Const("COMBK",tK) $ (Bound n') |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
57 |
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
|
58 |
| lam2comb (Abs(x,t1,Const(c,t2))) _ = |
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
|
59 |
let val tK = Type("fun",[t2,Type("fun",[t1,t2])]) |
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
|
60 |
in |
18276
c62ec94e326e
Added flags for setting and detecting whether a problem needs combinators.
mengj
parents:
18200
diff
changeset
|
61 |
include_min_comb:=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
|
62 |
Const("COMBK",tK) $ Const(c,t2) |
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
|
63 |
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
|
64 |
| lam2comb (Abs(x,t1,Free(v,t2))) _ = |
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
|
65 |
let val tK = Type("fun",[t2,Type("fun",[t1,t2])]) |
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
|
66 |
in |
18276
c62ec94e326e
Added flags for setting and detecting whether a problem needs combinators.
mengj
parents:
18200
diff
changeset
|
67 |
include_min_comb:=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
|
68 |
Const("COMBK",tK) $ Free(v,t2) |
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
|
69 |
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
|
70 |
| lam2comb (Abs(x,t1,Var(ind,t2))) _= |
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
|
71 |
let val tK = Type("fun",[t2,Type("fun",[t1,t2])]) |
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
|
72 |
in |
18276
c62ec94e326e
Added flags for setting and detecting whether a problem needs combinators.
mengj
parents:
18200
diff
changeset
|
73 |
include_min_comb:=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
|
74 |
Const("COMBK",tK) $ Var(ind,t2) |
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
|
75 |
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
|
76 |
| lam2comb (t as (Abs(x,t1,P$(Bound 0)))) Bnds = |
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
|
77 |
let val nfreeP = not(is_free P 0) |
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
|
78 |
val tr = Term.type_of1(t1::Bnds,P) |
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
|
79 |
in |
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 |
if nfreeP then (decre_bndVar P) |
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 |
else ( |
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 |
let val tI = Type("fun",[t1,t1]) |
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 |
val P' = lam2comb (Abs(x,t1,P)) Bnds |
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 |
val tp' = Term.type_of1(Bnds,P') |
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 |
val tS = Type("fun",[tp',Type("fun",[tI,tr])]) |
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 |
in |
18276
c62ec94e326e
Added flags for setting and detecting whether a problem needs combinators.
mengj
parents:
18200
diff
changeset
|
87 |
include_min_comb:=true; |
c62ec94e326e
Added flags for setting and detecting whether a problem needs combinators.
mengj
parents:
18200
diff
changeset
|
88 |
include_combS:=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
|
89 |
Const("COMBS",tS) $ P' $ Const("COMBI",tI) |
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
|
90 |
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
|
91 |
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
|
92 |
|
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 |
| lam2comb (t as (Abs(x,t1,P$Q))) Bnds = |
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
|
94 |
let val (nfreeP,nfreeQ) = (not(is_free P 0),not(is_free Q 0)) |
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
|
95 |
val tpq = Term.type_of1(t1::Bnds, P$Q) |
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
|
96 |
in |
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
|
97 |
if(nfreeP andalso nfreeQ) then ( |
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
|
98 |
let val tK = Type("fun",[tpq,Type("fun",[t1,tpq])]) |
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
|
99 |
val PQ' = decre_bndVar(P $ Q) |
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
|
100 |
in |
18276
c62ec94e326e
Added flags for setting and detecting whether a problem needs combinators.
mengj
parents:
18200
diff
changeset
|
101 |
include_min_comb:=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
|
102 |
Const("COMBK",tK) $ PQ' |
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 |
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
|
104 |
else ( |
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 |
if nfreeP then ( |
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 |
let val Q' = lam2comb (Abs(x,t1,Q)) Bnds |
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 |
val P' = decre_bndVar P |
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 |
val tp = Term.type_of1(Bnds,P') |
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
|
109 |
val tq' = Term.type_of1(Bnds, Q') |
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 |
val tB = Type("fun",[tp,Type("fun",[tq',Type("fun",[t1,tpq])])]) |
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 |
in |
18276
c62ec94e326e
Added flags for setting and detecting whether a problem needs combinators.
mengj
parents:
18200
diff
changeset
|
112 |
include_min_comb:=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
|
113 |
Const("COMBB",tB) $ P' $ Q' |
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 |
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
|
115 |
else ( |
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 |
if nfreeQ then ( |
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 |
let val P' = lam2comb (Abs(x,t1,P)) Bnds |
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 |
val Q' = decre_bndVar Q |
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
|
119 |
val tq = Term.type_of1(Bnds,Q') |
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 |
val tp' = Term.type_of1(Bnds, P') |
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
|
121 |
val tC = Type("fun",[tp',Type("fun",[tq,Type("fun",[t1,tpq])])]) |
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
|
122 |
in |
18276
c62ec94e326e
Added flags for setting and detecting whether a problem needs combinators.
mengj
parents:
18200
diff
changeset
|
123 |
include_min_comb:=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
|
124 |
Const("COMBC",tC) $ P' $ Q' |
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
|
125 |
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
|
126 |
else( |
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
|
127 |
let val P' = lam2comb (Abs(x,t1,P)) Bnds |
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
|
128 |
val Q' = lam2comb (Abs(x,t1,Q)) Bnds |
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 |
val tp' = Term.type_of1(Bnds,P') |
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 |
val tq' = Term.type_of1(Bnds,Q') |
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 |
val tS = Type("fun",[tp',Type("fun",[tq',Type("fun",[t1,tpq])])]) |
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 |
in |
18276
c62ec94e326e
Added flags for setting and detecting whether a problem needs combinators.
mengj
parents:
18200
diff
changeset
|
133 |
include_min_comb:=true; |
c62ec94e326e
Added flags for setting and detecting whether a problem needs combinators.
mengj
parents:
18200
diff
changeset
|
134 |
include_combS:=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
|
135 |
Const("COMBS",tS) $ P' $ Q' |
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
|
136 |
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
|
137 |
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
|
138 |
| lam2comb (t as (Abs(x,t1,_))) _ = raise LAM2COMB (t); |
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
|
139 |
|
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
|
140 |
|
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 |
|
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
|
142 |
(*********************) |
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 |
|
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
|
144 |
fun to_comb (Abs(x,tp,b)) Bnds = |
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
|
145 |
let val b' = to_comb b (tp::Bnds) |
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
|
146 |
in lam2comb (Abs(x,tp,b')) Bnds 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
|
147 |
| to_comb (P $ Q) Bnds = ((to_comb P Bnds) $ (to_comb Q Bnds)) |
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
|
148 |
| to_comb t _ = t; |
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
|
149 |
|
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
|
150 |
|
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
|
151 |
fun comb_of t = to_comb t []; |
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
|
152 |
|
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
|
153 |
|
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
|
154 |
(* print a term containing combinators, used for debugging *) |
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
|
155 |
exception TERM_COMB of term; |
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
|
156 |
|
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
|
157 |
fun string_of_term (Const(c,t)) = c |
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
|
158 |
| string_of_term (Free(v,t)) = v |
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
|
159 |
| string_of_term (Var((x,n),t)) = |
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 |
let val xn = x ^ "_" ^ (string_of_int n) |
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
|
161 |
in xn 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
|
162 |
| string_of_term (P $ Q) = |
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 |
let val P' = string_of_term P |
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
|
164 |
val Q' = string_of_term Q |
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 |
in |
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
|
166 |
"(" ^ P' ^ " " ^ Q' ^ ")" 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
|
167 |
| string_of_term t = raise TERM_COMB (t); |
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
|
168 |
|
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
|
169 |
|
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
|
170 |
|
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
|
171 |
(******************************************************) |
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 |
(* 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
|
173 |
(******************************************************) |
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 |
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
|
176 |
datatype kind = Axiom | Conjecture; |
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 |
fun name_of_kind Axiom = "axiom" |
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 |
| name_of_kind Conjecture = "conjecture"; |
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
|
179 |
|
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
|
180 |
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
|
181 |
type indexname = Term.indexname; |
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
|
182 |
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
|
183 |
type csort = Term.sort; |
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
184 |
type ctyp = ResClause.fol_type; |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
185 |
|
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
186 |
val string_of_ctyp = ResClause.string_of_fol_type; |
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
|
187 |
|
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
|
188 |
type ctyp_var = ResClause.typ_var; |
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 |
|
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 |
type ctype_literal = ResClause.type_literal; |
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
|
191 |
|
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
|
192 |
|
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
193 |
datatype combterm = CombConst of string * ctyp * ctyp 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
|
194 |
| CombFree of string * ctyp |
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
|
195 |
| CombVar of string * ctyp |
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
|
196 |
| CombApp of combterm * combterm * ctyp |
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
|
197 |
| Bool of 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
|
198 |
| Equal of combterm * 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
|
199 |
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
|
200 |
|
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 |
datatype 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
|
204 |
Clause of {clause_id: clause_id, |
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 |
axiom_name: axiom_name, |
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 |
kind: kind, |
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 |
literals: literal list, |
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 |
ctypes_sorts: (ctyp_var * csort) list, |
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 |
ctvar_type_literals: ctype_literal list, |
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 |
ctfree_type_literals: ctype_literal list}; |
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
|
211 |
|
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 |
|
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
|
214 |
fun string_of_kind (Clause cls) = name_of_kind (#kind cls); |
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
|
215 |
fun get_axiomName (Clause cls) = #axiom_name cls; |
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 |
fun get_clause_id (Clause cls) = #clause_id cls; |
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
|
217 |
|
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
218 |
fun get_literals (c as Clause(cls)) = #literals cls; |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
219 |
|
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
|
220 |
|
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 |
|
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
222 |
exception TERM_ORD of string |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
223 |
|
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
224 |
fun term_ord (CombVar(_,_),CombVar(_,_)) = EQUAL |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
225 |
| term_ord (CombVar(_,_),_) = LESS |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
226 |
| term_ord (CombFree(_,_),CombVar(_,_)) = GREATER |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
227 |
| term_ord (CombFree(f1,tp1),CombFree(f2,tp2)) = |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
228 |
let val ord1 = string_ord(f1,f2) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
229 |
in |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
230 |
case ord1 of EQUAL => ResClause.types_ord ([tp1],[tp2]) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
231 |
| _ => ord1 |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
232 |
end |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
233 |
| term_ord (CombFree(_,_),_) = LESS |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
234 |
| term_ord (CombConst(_,_,_),CombVar(_,_)) = GREATER |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
235 |
| term_ord (CombConst(_,_,_),CombFree(_,_)) = GREATER |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
236 |
| term_ord (CombConst(c1,tp1,_),CombConst(c2,tp2,_)) = |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
237 |
let val ord1 = string_ord (c1,c2) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
238 |
in |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
239 |
case ord1 of EQUAL => ResClause.types_ord ([tp1],[tp2]) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
240 |
| _ => ord1 |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
241 |
end |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
242 |
| term_ord (CombConst(_,_,_),_) = LESS |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
243 |
| term_ord (CombApp(_,_,_),Bool(_)) = raise TERM_ORD("bool") |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
244 |
| term_ord (CombApp(_,_,_),Equal(_,_)) = LESS |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
245 |
| term_ord (CombApp(f1,arg1,tp1),CombApp(f2,arg2,tp2)) = |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
246 |
let val ord1 = term_ord (f1,f2) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
247 |
val ord2 = case ord1 of EQUAL => term_ord (arg1,arg2) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
248 |
| _ => ord1 |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
249 |
in |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
250 |
case ord2 of EQUAL => ResClause.types_ord ([tp1],[tp2]) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
251 |
| _ => ord2 |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
252 |
end |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
253 |
| term_ord (CombApp(_,_,_),_) = GREATER |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
254 |
| term_ord (Bool(_),_) = raise TERM_ORD("bool") |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
255 |
| term_ord (Equal(t1,t2),Equal(t3,t4)) = ResClause.list_ord term_ord ([t1,t2],[t3,t4]) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
256 |
| term_ord (Equal(_,_),_) = GREATER; |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
257 |
|
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
258 |
fun predicate_ord (Equal(_,_),Bool(_)) = LESS |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
259 |
| predicate_ord (Equal(t1,t2),Equal(t3,t4)) = |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
260 |
ResClause.list_ord term_ord ([t1,t2],[t3,t4]) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
261 |
| predicate_ord (Bool(_),Equal(_,_)) = GREATER |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
262 |
| predicate_ord (Bool(t1),Bool(t2)) = term_ord (t1,t2) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
263 |
|
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
264 |
|
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
265 |
fun literal_ord (Literal(false,_),Literal(true,_)) = LESS |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
266 |
| literal_ord (Literal(true,_),Literal(false,_)) = GREATER |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
267 |
| literal_ord (Literal(_,pred1),Literal(_,pred2)) = predicate_ord(pred1,pred2); |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
268 |
|
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
269 |
fun sort_lits lits = sort literal_ord 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
|
270 |
|
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
|
271 |
(*********************************************************************) |
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
|
272 |
(* 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
|
273 |
(*********************************************************************) |
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
|
274 |
|
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
275 |
fun isFalse (Literal(pol,Bool(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
|
276 |
(pol andalso c = "c_False") 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
|
277 |
(not pol andalso c = "c_True") |
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
|
278 |
| 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
|
279 |
|
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
|
280 |
|
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
281 |
fun isTrue (Literal (pol,Bool(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
|
282 |
(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
|
283 |
(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
|
284 |
| isTrue _ = 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
|
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 |
fun isTaut (Clause {literals,...}) = exists isTrue literals; |
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 |
|
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
|
288 |
|
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 |
|
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 |
fun make_clause(clause_id,axiom_name,kind,literals,ctypes_sorts,ctvar_type_literals,ctfree_type_literals) = |
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 |
if forall isFalse literals |
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
|
292 |
then error "Problem too trivial for resolution (empty 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
|
293 |
else |
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
|
294 |
Clause {clause_id = clause_id, axiom_name = axiom_name, kind = kind, |
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
|
295 |
literals = literals, ctypes_sorts = ctypes_sorts, |
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
|
296 |
ctvar_type_literals = ctvar_type_literals, |
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
|
297 |
ctfree_type_literals = ctfree_type_literals}; |
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
|
298 |
|
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
299 |
fun type_of (Type (a, Ts)) = |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
300 |
let val (folTypes,ts) = types_of Ts |
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
|
301 |
val t = ResClause.make_fixed_type_const a |
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
|
302 |
in |
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
303 |
(ResClause.mk_fol_type("Comp",t,folTypes),ts) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
304 |
end |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
305 |
| type_of (tp as (TFree(a,s))) = |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
306 |
let val t = ResClause.make_fixed_type_var a |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
307 |
in |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
308 |
(ResClause.mk_fol_type("Fixed",t,[]),[ResClause.mk_typ_var_sort tp]) |
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 |
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
|
310 |
| type_of (tp as (TVar(v,s))) = |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
311 |
let val t = ResClause.make_schematic_type_var v |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
312 |
in |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
313 |
(ResClause.mk_fol_type("Var",t,[]),[ResClause.mk_typ_var_sort tp]) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
314 |
end |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
315 |
|
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
316 |
and types_of Ts = |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
317 |
let val foltyps_ts = map type_of Ts |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
318 |
val (folTyps,ts) = ListPair.unzip foltyps_ts |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
319 |
in |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
320 |
(folTyps,ResClause.union_all ts) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
321 |
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
|
322 |
|
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
|
323 |
(* same as above, but no gathering of sort information *) |
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
324 |
fun simp_type_of (Type (a, Ts)) = |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
325 |
let val typs = map simp_type_of Ts |
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
|
326 |
val t = ResClause.make_fixed_type_const a |
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
|
327 |
in |
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
328 |
ResClause.mk_fol_type("Comp",t,typs) |
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
|
329 |
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
|
330 |
| simp_type_of (TFree (a,s)) = ResClause.mk_fol_type("Fixed",ResClause.make_fixed_type_var a,[]) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
331 |
| simp_type_of (TVar (v,s)) = ResClause.mk_fol_type("Var",ResClause.make_schematic_type_var v,[]); |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
332 |
|
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
333 |
fun comb_typ ("COMBI",t) = |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
334 |
let val t' = domain_type t |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
335 |
in |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
336 |
[simp_type_of t'] |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
337 |
end |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
338 |
| comb_typ ("COMBK",t) = |
18725 | 339 |
let val a = domain_type t |
340 |
val b = domain_type (range_type t) |
|
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
341 |
in |
18725 | 342 |
map simp_type_of [a,b] |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
343 |
end |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
344 |
| comb_typ ("COMBS",t) = |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
345 |
let val t' = domain_type t |
18725 | 346 |
val a = domain_type t' |
347 |
val b = domain_type (range_type t') |
|
348 |
val c = range_type (range_type t') |
|
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
349 |
in |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
350 |
map simp_type_of [a,b,c] |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
351 |
end |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
352 |
| comb_typ ("COMBB",t) = |
18725 | 353 |
let val ab = domain_type t |
354 |
val ca = domain_type (range_type t) |
|
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
355 |
val a = domain_type ab |
18725 | 356 |
val b = range_type ab |
357 |
val c = domain_type ca |
|
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
358 |
in |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
359 |
map simp_type_of [a,b,c] |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
360 |
end |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
361 |
| comb_typ ("COMBC",t) = |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
362 |
let val t1 = domain_type t |
18725 | 363 |
val a = domain_type t1 |
364 |
val b = domain_type (range_type t1) |
|
365 |
val c = range_type (range_type t1) |
|
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
366 |
in |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
367 |
map simp_type_of [a,b,c] |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
368 |
end; |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
369 |
|
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
370 |
fun const_type_of ("COMBI",t) = |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
371 |
let val (tp,ts) = type_of t |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
372 |
val I_var = comb_typ ("COMBI",t) |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
373 |
in |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
374 |
(tp,ts,I_var) |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
375 |
end |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
376 |
| const_type_of ("COMBK",t) = |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
377 |
let val (tp,ts) = type_of t |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
378 |
val K_var = comb_typ ("COMBK",t) |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
379 |
in |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
380 |
(tp,ts,K_var) |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
381 |
end |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
382 |
| const_type_of ("COMBS",t) = |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
383 |
let val (tp,ts) = type_of t |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
384 |
val S_var = comb_typ ("COMBS",t) |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
385 |
in |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
386 |
(tp,ts,S_var) |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
387 |
end |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
388 |
| const_type_of ("COMBB",t) = |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
389 |
let val (tp,ts) = type_of t |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
390 |
val B_var = comb_typ ("COMBB",t) |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
391 |
in |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
392 |
(tp,ts,B_var) |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
393 |
end |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
394 |
| const_type_of ("COMBC",t) = |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
395 |
let val (tp,ts) = type_of t |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
396 |
val C_var = comb_typ ("COMBC",t) |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
397 |
in |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
398 |
(tp,ts,C_var) |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
399 |
end |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
400 |
| const_type_of (c,t) = |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
401 |
let val (tp,ts) = type_of t |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
402 |
val tvars = !const_typargs(c,t) |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
403 |
val tvars' = map simp_type_of tvars |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
404 |
in |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
405 |
(tp,ts,tvars') |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
406 |
end; |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
407 |
|
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
408 |
fun is_bool_type (Type("bool",[])) = true |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
409 |
| is_bool_type _ = false; |
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
|
410 |
|
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
|
411 |
|
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
|
412 |
(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *) |
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
|
413 |
fun combterm_of (Const(c,t)) = |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
414 |
let val (tp,ts,tvar_list) = const_type_of (c,t) |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
415 |
val is_bool = is_bool_type t |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
416 |
val c' = CombConst(ResClause.make_fixed_const c,tp,tvar_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
|
417 |
val c'' = if is_bool then Bool(c') else c' |
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
|
418 |
in |
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
|
419 |
(c'',ts) |
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
|
420 |
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
|
421 |
| combterm_of (Free(v,t)) = |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
422 |
let val (tp,ts) = type_of t |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
423 |
val is_bool = is_bool_type 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
|
424 |
val v' = if ResClause.isMeta v then CombVar(ResClause.make_schematic_var(v,0),tp) |
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
|
425 |
else CombFree(ResClause.make_fixed_var v,tp) |
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
|
426 |
val v'' = if is_bool then Bool(v') else v' |
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
|
427 |
in |
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
|
428 |
(v'',ts) |
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
|
429 |
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
|
430 |
| combterm_of (Var(v,t)) = |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
431 |
let val (tp,ts) = type_of t |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
432 |
val is_bool = is_bool_type 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
|
433 |
val v' = CombVar(ResClause.make_schematic_var v,tp) |
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
|
434 |
val v'' = if is_bool then Bool(v') else v' |
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
|
435 |
in |
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
|
436 |
(v'',ts) |
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
|
437 |
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
|
438 |
| combterm_of (Const("op =",T) $ P $ Q) = (*FIXME: allow equal between bools?*) |
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
|
439 |
let val (P',tsP) = combterm_of P |
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
|
440 |
val (Q',tsQ) = combterm_of Q |
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
|
441 |
in |
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
|
442 |
(Equal(P',Q'),tsP union tsQ) |
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
|
443 |
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
|
444 |
| combterm_of (t as (P $ Q)) = |
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
|
445 |
let val (P',tsP) = combterm_of P |
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
|
446 |
val (Q',tsQ) = combterm_of Q |
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
|
447 |
val tp = Term.type_of t |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
448 |
val tp' = simp_type_of tp |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
449 |
val is_bool = is_bool_type tp |
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
|
450 |
val t' = CombApp(P',Q',tp') |
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
|
451 |
val t'' = if is_bool then Bool(t') else t' |
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
|
452 |
in |
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
|
453 |
(t'',tsP union tsQ) |
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
|
454 |
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
|
455 |
|
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
|
456 |
fun predicate_of ((Const("Not",_) $ P), polarity) = |
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
|
457 |
predicate_of (P, not polarity) |
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
|
458 |
| predicate_of (term,polarity) = (combterm_of term,polarity); |
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
|
459 |
|
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
|
460 |
|
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
|
461 |
fun literals_of_term1 args (Const("Trueprop",_) $ P) = literals_of_term1 args P |
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
|
462 |
| literals_of_term1 args (Const("op |",_) $ P $ Q) = |
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
|
463 |
let val args' = literals_of_term1 args P |
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
|
464 |
in |
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
|
465 |
literals_of_term1 args' Q |
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
|
466 |
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
|
467 |
| literals_of_term1 (lits,ts) P = |
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
|
468 |
let val ((pred,ts'),pol) = predicate_of (P,true) |
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
|
469 |
val lits' = Literal(pol,pred)::lits |
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
|
470 |
in |
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
|
471 |
(lits',ts union ts') |
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
|
472 |
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
|
473 |
|
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
|
474 |
|
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
|
475 |
fun literals_of_term P = literals_of_term1 ([],[]) P; |
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
|
476 |
|
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
|
477 |
|
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
|
478 |
(* making axiom and conjecture clauses *) |
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
|
479 |
fun make_axiom_clause term (ax_name,cls_id) = |
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
|
480 |
let val term' = comb_of term |
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
|
481 |
val (lits,ctypes_sorts) = literals_of_term term' |
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
482 |
val lits' = sort_lits lits |
18856
4669dec681f4
tidy-up of res_clause.ML, removing the "predicates" field
paulson
parents:
18725
diff
changeset
|
483 |
val (ctvar_lits,ctfree_lits) = ResClause.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
|
484 |
in |
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
|
485 |
make_clause(cls_id,ax_name,Axiom, |
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
486 |
lits',ctypes_sorts,ctvar_lits,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
|
487 |
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
|
488 |
|
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
|
489 |
|
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
|
490 |
fun make_conjecture_clause n t = |
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
|
491 |
let val t' = comb_of t |
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
|
492 |
val (lits,ctypes_sorts) = literals_of_term t' |
18856
4669dec681f4
tidy-up of res_clause.ML, removing the "predicates" field
paulson
parents:
18725
diff
changeset
|
493 |
val (ctvar_lits,ctfree_lits) = ResClause.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
|
494 |
in |
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
|
495 |
make_clause(n,"conjecture",Conjecture,lits,ctypes_sorts,ctvar_lits,ctfree_lits) |
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
|
496 |
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
|
497 |
|
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
|
498 |
|
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
|
499 |
|
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
|
500 |
fun make_conjecture_clauses_aux _ [] = [] |
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
|
501 |
| make_conjecture_clauses_aux n (t::ts) = |
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
|
502 |
make_conjecture_clause n t :: make_conjecture_clauses_aux (n+1) ts; |
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
|
503 |
|
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
|
504 |
val make_conjecture_clauses = make_conjecture_clauses_aux 0; |
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
|
505 |
|
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
|
506 |
|
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
|
507 |
(**********************************************************************) |
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
|
508 |
(* 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
|
509 |
(* TPTP used by Vampire and E *) |
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
|
510 |
(**********************************************************************) |
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
|
511 |
|
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
|
512 |
val type_wrapper = "typeinfo"; |
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
|
513 |
|
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
514 |
datatype type_level = T_FULL | T_PARTIAL | T_CONST | T_NONE; |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
515 |
|
19130 | 516 |
val typ_level = ref T_FULL; |
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
|
517 |
|
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
518 |
fun full_types () = (typ_level:=T_FULL); |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
519 |
fun partial_types () = (typ_level:=T_PARTIAL); |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
520 |
fun const_types_only () = (typ_level:=T_CONST); |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
521 |
fun no_types () = (typ_level:=T_NONE); |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
522 |
|
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
523 |
|
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
524 |
fun find_typ_level () = !typ_level; |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
525 |
|
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
526 |
fun wrap_type (c,t) = |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
527 |
case !typ_level of T_FULL => type_wrapper ^ (ResClause.paren_pack [c,t]) |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
528 |
| _ => c; |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
529 |
|
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
|
530 |
|
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
|
531 |
val bool_tp = ResClause.make_fixed_type_const "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
|
532 |
|
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
|
533 |
val app_str = "hAPP"; |
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
|
534 |
|
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
|
535 |
val bool_str = "hBOOL"; |
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
|
536 |
|
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
537 |
exception STRING_OF_COMBTERM of int; |
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
|
538 |
|
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
|
539 |
(* convert literals of clauses into strings *) |
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
540 |
fun string_of_combterm1_aux _ (CombConst(c,tp,_)) = |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
541 |
let val tp' = string_of_ctyp tp |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
542 |
in |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
543 |
(wrap_type (c,tp'),tp') |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
544 |
end |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
545 |
| string_of_combterm1_aux _ (CombFree(v,tp)) = |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
546 |
let val tp' = string_of_ctyp tp |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
547 |
in |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
548 |
(wrap_type (v,tp'),tp') |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
549 |
end |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
550 |
| string_of_combterm1_aux _ (CombVar(v,tp)) = |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
551 |
let val tp' = string_of_ctyp tp |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
552 |
in |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
553 |
(wrap_type (v,tp'),tp') |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
554 |
end |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
555 |
| string_of_combterm1_aux is_pred (CombApp(t1,t2,tp)) = |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
556 |
let val (s1,tp1) = string_of_combterm1_aux is_pred t1 |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
557 |
val (s2,tp2) = string_of_combterm1_aux is_pred t2 |
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
558 |
val tp' = ResClause.string_of_fol_type tp |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
559 |
val r = case !typ_level of T_FULL => type_wrapper ^ (ResClause.paren_pack [(app_str ^ (ResClause.paren_pack [s1,s2])),tp']) |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
560 |
| T_PARTIAL => app_str ^ (ResClause.paren_pack [s1,s2,tp1]) |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
561 |
| T_NONE => app_str ^ (ResClause.paren_pack [s1,s2]) |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
562 |
| T_CONST => raise STRING_OF_COMBTERM (1) (*should not happen, if happened may be a bug*) |
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
563 |
in (r,tp') |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
564 |
|
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
565 |
end |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
566 |
| string_of_combterm1_aux is_pred (Bool(t)) = |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
567 |
let val (t',_) = string_of_combterm1_aux false t |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
568 |
val r = if is_pred then bool_str ^ (ResClause.paren_pack [t']) |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
569 |
else 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
|
570 |
in |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
571 |
(r,bool_tp) |
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
|
572 |
end |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
573 |
| string_of_combterm1_aux _ (Equal(t1,t2)) = |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
574 |
let val (s1,_) = string_of_combterm1_aux false t1 |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
575 |
val (s2,_) = string_of_combterm1_aux false t2 |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
576 |
in |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
577 |
("equal" ^ (ResClause.paren_pack [s1,s2]),bool_tp) |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
578 |
end; |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
579 |
|
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
580 |
fun string_of_combterm1 is_pred term = fst (string_of_combterm1_aux is_pred term); |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
581 |
|
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
582 |
fun string_of_combterm2 _ (CombConst(c,tp,tvars)) = |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
583 |
let val tvars' = map string_of_ctyp tvars |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
584 |
in |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
585 |
c ^ (ResClause.paren_pack tvars') |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
586 |
end |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
587 |
| string_of_combterm2 _ (CombFree(v,tp)) = v |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
588 |
| string_of_combterm2 _ (CombVar(v,tp)) = v |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
589 |
| string_of_combterm2 is_pred (CombApp(t1,t2,tp)) = |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
590 |
let val s1 = string_of_combterm2 is_pred t1 |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
591 |
val s2 = string_of_combterm2 is_pred t2 |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
592 |
in |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
593 |
app_str ^ (ResClause.paren_pack [s1,s2]) |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
594 |
end |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
595 |
| string_of_combterm2 is_pred (Bool(t)) = |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
596 |
let val t' = string_of_combterm2 false 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
|
597 |
in |
18200 | 598 |
if is_pred then bool_str ^ (ResClause.paren_pack [t']) |
599 |
else 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
|
600 |
end |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
601 |
| string_of_combterm2 _ (Equal(t1,t2)) = |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
602 |
let val s1 = string_of_combterm2 false t1 |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
603 |
val s2 = string_of_combterm2 false t2 |
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
|
604 |
in |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
605 |
("equal" ^ (ResClause.paren_pack [s1,s2])) |
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
|
606 |
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
|
607 |
|
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
608 |
|
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
609 |
|
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
610 |
fun string_of_combterm is_pred term = |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
611 |
case !typ_level of T_CONST => string_of_combterm2 is_pred term |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
612 |
| _ => string_of_combterm1 is_pred term; |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
613 |
|
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
614 |
|
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
|
615 |
fun string_of_clausename (cls_id,ax_name) = |
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
|
616 |
ResClause.clause_prefix ^ ResClause.ascii_of ax_name ^ "_" ^ Int.toString cls_id; |
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
|
617 |
|
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
|
618 |
fun string_of_type_clsname (cls_id,ax_name,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
|
619 |
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
|
620 |
|
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
|
621 |
|
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
|
622 |
fun tptp_literal (Literal(pol,pred)) = |
18200 | 623 |
let val pred_string = string_of_combterm true pred |
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
|
624 |
val pol_str = if pol then "++" else "--" |
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
|
625 |
in |
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
|
626 |
pol_str ^ pred_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
|
627 |
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
|
628 |
|
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
|
629 |
|
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
|
630 |
fun tptp_type_lits (Clause cls) = |
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
|
631 |
let val lits = map tptp_literal (#literals cls) |
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
|
632 |
val ctvar_lits_strs = |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
633 |
case !typ_level of T_NONE => [] |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
634 |
| _ => (map ResClause.tptp_of_typeLit (#ctvar_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
|
635 |
val ctfree_lits = |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
636 |
case !typ_level of T_NONE => [] |
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
637 |
| _ => (map ResClause.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
|
638 |
in |
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
|
639 |
(ctvar_lits_strs @ lits, ctfree_lits) |
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
|
640 |
end; |
18356
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
641 |
|
443717b3a9ad
Added new type embedding methods for translating HOL clauses.
mengj
parents:
18276
diff
changeset
|
642 |
|
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
|
643 |
fun clause2tptp cls = |
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
|
644 |
let val (lits,ctfree_lits) = tptp_type_lits cls |
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
|
645 |
val cls_id = get_clause_id cls |
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
|
646 |
val ax_name = get_axiomName cls |
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
|
647 |
val knd = string_of_kind cls |
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
|
648 |
val lits_str = ResClause.bracket_pack lits |
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
|
649 |
val cls_str = ResClause.gen_tptp_cls(cls_id,ax_name,knd,lits_str) |
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
|
650 |
in |
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
|
651 |
(cls_str,ctfree_lits) |
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
|
652 |
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
|
653 |
|
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
|
654 |
|
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
655 |
|
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
656 |
(**********************************************************************) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
657 |
(* clause equalities and hashing functions *) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
658 |
(**********************************************************************) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
659 |
|
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
660 |
|
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
661 |
fun combterm_eq (CombConst(c1,tp1,tps1),CombConst(c2,tp2,tps2)) vtvars = |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
662 |
let val (eq1,vtvars1) = if c1 = c2 then ResClause.types_eq (tps1,tps2) vtvars |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
663 |
else (false,vtvars) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
664 |
in |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
665 |
(eq1,vtvars1) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
666 |
end |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
667 |
| combterm_eq (CombConst(_,_,_),_) vtvars = (false,vtvars) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
668 |
| combterm_eq (CombFree(a1,tp1),CombFree(a2,tp2)) vtvars = |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
669 |
if a1 = a2 then ResClause.types_eq ([tp1],[tp2]) vtvars |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
670 |
else (false,vtvars) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
671 |
| combterm_eq (CombFree(_,_),_) vtvars = (false,vtvars) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
672 |
| combterm_eq (CombVar(v1,tp1),CombVar(v2,tp2)) (vars,tvars) = |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
673 |
(case ResClause.check_var_pairs(v1,v2) vars of 0 => ResClause.types_eq ([tp1],[tp2]) ((v1,v2)::vars,tvars) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
674 |
| 1 => ResClause.types_eq ([tp1],[tp2]) (vars,tvars) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
675 |
| 2 => (false,(vars,tvars))) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
676 |
| combterm_eq (CombVar(_,_),_) vtvars = (false,vtvars) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
677 |
| combterm_eq (CombApp(f1,arg1,tp1),CombApp(f2,arg2,tp2)) vtvars = |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
678 |
let val (eq1,vtvars1) = combterm_eq (f1,f2) vtvars |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
679 |
val (eq2,vtvars2) = if eq1 then combterm_eq (arg1,arg2) vtvars1 |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
680 |
else (eq1,vtvars1) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
681 |
in |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
682 |
if eq2 then ResClause.types_eq ([tp1],[tp2]) vtvars2 |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
683 |
else (eq2,vtvars2) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
684 |
end |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
685 |
| combterm_eq (CombApp(_,_,_),_) vtvars = (false,vtvars) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
686 |
| combterm_eq (Bool(t1),Bool(t2)) vtvars = combterm_eq (t1,t2) vtvars |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
687 |
| combterm_eq (Bool(_),_) vtvars = (false,vtvars) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
688 |
| combterm_eq (Equal(t1,t2),Equal(t3,t4)) vtvars = |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
689 |
let val (eq1,vtvars1) = combterm_eq (t1,t3) vtvars |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
690 |
in |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
691 |
if eq1 then combterm_eq (t2,t4) vtvars1 |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
692 |
else (eq1,vtvars1) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
693 |
end |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
694 |
| combterm_eq (Equal(t1,t2),_) vtvars = (false,vtvars); |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
695 |
|
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
696 |
fun lit_eq (Literal(pol1,pred1),Literal(pol2,pred2)) vtvars = |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
697 |
if (pol1 = pol2) then combterm_eq (pred1,pred2) vtvars |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
698 |
else (false,vtvars); |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
699 |
|
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
700 |
fun lits_eq ([],[]) vtvars = (true,vtvars) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
701 |
| lits_eq (l1::ls1,l2::ls2) vtvars = |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
702 |
let val (eq1,vtvars1) = lit_eq (l1,l2) vtvars |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
703 |
in |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
704 |
if eq1 then lits_eq (ls1,ls2) vtvars1 |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
705 |
else (false,vtvars1) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
706 |
end; |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
707 |
|
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
708 |
fun clause_eq (cls1,cls2) = |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
709 |
let val lits1 = get_literals cls1 |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
710 |
val lits2 = get_literals cls2 |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
711 |
in |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
712 |
length lits1 = length lits2 andalso #1 (lits_eq (lits1,lits2) ([],[])) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
713 |
end; |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
714 |
|
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
715 |
val xor_words = List.foldl Word.xorb 0w0; |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
716 |
|
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
717 |
fun hash_combterm (CombVar(_,_),w) = w |
18449 | 718 |
| hash_combterm (CombFree(f,_),w) = Polyhash.hashw_string(f,w) |
719 |
| hash_combterm (CombConst(c,tp,tps),w) = Polyhash.hashw_string(c,w) |
|
720 |
| hash_combterm (CombApp(f,arg,tp),w) = hash_combterm (arg, hash_combterm (f,w)) |
|
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
721 |
| hash_combterm (Bool(t),w) = hash_combterm (t,w) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
722 |
| hash_combterm (Equal(t1,t2),w) = |
18449 | 723 |
List.foldl hash_combterm (Polyhash.hashw_string ("equal",w)) [t1,t2] |
18440
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
724 |
|
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
725 |
fun hash_literal (Literal(true,pred)) = hash_combterm(pred,0w0) |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
726 |
| hash_literal (Literal(false,pred)) = Word.notb(hash_combterm(pred,0w0)); |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
727 |
|
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
728 |
fun hash_clause clause = xor_words (map hash_literal (get_literals clause)); |
72ee07f4b56b
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
mengj
parents:
18356
diff
changeset
|
729 |
|
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
|
730 |
end |