15347
|
1 |
(* Author: Jia Meng, Cambridge University Computer Laboratory
|
|
2 |
ID: $Id$
|
|
3 |
Copyright 2004 University of Cambridge
|
|
4 |
|
|
5 |
transformation of Isabelle arities and class relations into clauses (defined in the structure Clause).
|
|
6 |
*)
|
|
7 |
|
|
8 |
signature RES_TYPES_SORTS =
|
|
9 |
sig
|
|
10 |
|
|
11 |
exception ARITIES of string
|
|
12 |
val arity_clause :
|
|
13 |
string * (string * string list list) list -> ResClause.arityClause list
|
|
14 |
val arity_clause_sig :
|
|
15 |
Sign.sg -> ResClause.arityClause list list * (string * 'a list) list
|
|
16 |
val arity_clause_thy :
|
|
17 |
Theory.theory ->
|
|
18 |
ResClause.arityClause list list * (string * 'a list) list
|
|
19 |
type classrelClauses
|
|
20 |
val classrel_clause : string * string list -> ResClause.classrelClause list
|
|
21 |
val classrel_clauses_classrel :
|
|
22 |
'a Graph.T -> ResClause.classrelClause list list
|
|
23 |
val classrel_clauses_sg : Sign.sg -> ResClause.classrelClause list list
|
|
24 |
val classrel_clauses_thy :
|
|
25 |
Theory.theory -> ResClause.classrelClause list list
|
|
26 |
val classrel_of_sg : Sign.sg -> Sorts.classes
|
|
27 |
val multi_arity_clause :
|
|
28 |
(string * (string * string list list) list) list ->
|
|
29 |
(string * 'a list) list ->
|
|
30 |
ResClause.arityClause list list * (string * 'a list) list
|
|
31 |
val tptp_arity_clause_thy : Theory.theory -> string list list
|
|
32 |
val tptp_classrel_clauses_sg : Sign.sg -> string list list
|
|
33 |
val tsig_of : Theory.theory -> Type.tsig
|
|
34 |
val tsig_of_sg : Sign.sg -> Type.tsig
|
|
35 |
|
|
36 |
end;
|
|
37 |
|
|
38 |
structure ResTypesSorts : RES_TYPES_SORTS =
|
|
39 |
|
|
40 |
struct
|
|
41 |
|
|
42 |
(**** Isabelle arities ****)
|
|
43 |
|
|
44 |
exception ARITIES of string;
|
|
45 |
|
|
46 |
|
|
47 |
fun arity_clause (tcons, []) = raise ARITIES(tcons)
|
|
48 |
| arity_clause (tcons,[ar]) = [ResClause.make_axiom_arity_clause (tcons,ar)]
|
|
49 |
| arity_clause (tcons,ar1::ars) = (ResClause.make_axiom_arity_clause (tcons,ar1)) :: (arity_clause (tcons,ars));
|
|
50 |
|
|
51 |
|
|
52 |
fun multi_arity_clause [] expts = ([], expts)
|
|
53 |
| multi_arity_clause ((tcon,[])::tcons_ars) expts =
|
|
54 |
multi_arity_clause tcons_ars ((tcon,[])::expts)
|
|
55 |
| multi_arity_clause (tcon_ar::tcons_ars) expts =
|
|
56 |
let val result = multi_arity_clause tcons_ars expts
|
|
57 |
in
|
|
58 |
(((arity_clause tcon_ar) :: (fst result)),snd result)
|
|
59 |
end;
|
|
60 |
|
|
61 |
|
|
62 |
fun tsig_of thy = #tsig(Sign.rep_sg (sign_of thy));
|
|
63 |
|
|
64 |
fun tsig_of_sg sg = #tsig(Sign.rep_sg sg);
|
|
65 |
|
|
66 |
|
|
67 |
(* Isabelle arities *)
|
|
68 |
fun arity_clause_thy thy =
|
|
69 |
let val tsig = tsig_of thy
|
|
70 |
val arities = #arities (Type.rep_tsig tsig)
|
|
71 |
val entries = Symtab.dest arities
|
|
72 |
in
|
|
73 |
multi_arity_clause entries []
|
|
74 |
end;
|
|
75 |
|
|
76 |
fun arity_clause_sig sg =
|
|
77 |
let val tsig = #tsig(Sign.rep_sg sg)
|
|
78 |
val arities = #arities (Type.rep_tsig tsig)
|
|
79 |
val entries = Symtab.dest arities
|
|
80 |
in
|
|
81 |
multi_arity_clause entries []
|
|
82 |
end;
|
|
83 |
|
|
84 |
|
|
85 |
fun tptp_arity_clause_thy thy =
|
|
86 |
let val (arclss,_) = arity_clause_thy thy
|
|
87 |
in
|
|
88 |
map (map ResClause.tptp_arity_clause) arclss
|
|
89 |
end;
|
|
90 |
|
|
91 |
|
|
92 |
|
|
93 |
(**** Isabelle classrel ****)
|
|
94 |
|
|
95 |
type classrelClauses = (ResClause.classrelClause list) Symtab.table;
|
|
96 |
|
|
97 |
|
|
98 |
|
|
99 |
(* The new version of finding class relations from a signature *)
|
|
100 |
fun classrel_of_sg sg = #classes (Type.rep_tsig (tsig_of_sg sg));
|
|
101 |
|
|
102 |
fun classrel_clause (sub, sups) = ResClause.classrelClauses_of (sub,sups);
|
|
103 |
|
|
104 |
|
|
105 |
|
|
106 |
(* new version of classrel_clauses_classrel *)
|
|
107 |
fun classrel_clauses_classrel classrel =
|
|
108 |
let val entries = Graph.dest classrel
|
|
109 |
in
|
|
110 |
map classrel_clause entries
|
|
111 |
end;
|
|
112 |
|
|
113 |
fun classrel_clauses_sg sg =
|
|
114 |
let val classrel = classrel_of_sg sg
|
|
115 |
in
|
|
116 |
classrel_clauses_classrel classrel
|
|
117 |
end;
|
|
118 |
|
|
119 |
|
|
120 |
val classrel_clauses_thy = classrel_clauses_sg o sign_of;
|
|
121 |
|
|
122 |
|
|
123 |
fun tptp_classrel_clauses_sg sg =
|
|
124 |
let val relclss = classrel_clauses_sg sg
|
|
125 |
in
|
|
126 |
map (map ResClause.tptp_classrelClause) relclss
|
|
127 |
end;
|
|
128 |
|
|
129 |
|
|
130 |
|
|
131 |
|
|
132 |
end;
|