--- a/src/HOL/Tools/res_types_sorts.ML Sat Jun 11 22:15:51 2005 +0200
+++ b/src/HOL/Tools/res_types_sorts.ML Sat Jun 11 22:15:52 2005 +0200
@@ -1,132 +1,71 @@
-(* Author: Jia Meng, Cambridge University Computer Laboratory
+(* Author: Jia Meng, Cambridge University Computer Laboratory
ID: $Id$
Copyright 2004 University of Cambridge
-transformation of Isabelle arities and class relations into clauses (defined in the structure Clause).
+Transformation of Isabelle arities and class relations into clauses
+(defined in the structure Clause).
*)
signature RES_TYPES_SORTS =
sig
-
-exception ARITIES of string
-val arity_clause :
- string * (string * string list list) list -> ResClause.arityClause list
-val arity_clause_sig :
- Sign.sg -> ResClause.arityClause list list * (string * 'a list) list
-val arity_clause_thy :
- Theory.theory ->
- ResClause.arityClause list list * (string * 'a list) list
-type classrelClauses
-val classrel_clause : string * string list -> ResClause.classrelClause list
-val classrel_clauses_classrel :
- 'a Graph.T -> ResClause.classrelClause list list
-val classrel_clauses_sg : Sign.sg -> ResClause.classrelClause list list
-val classrel_clauses_thy :
- Theory.theory -> ResClause.classrelClause list list
-val classrel_of_sg : Sign.sg -> Sorts.classes
-val multi_arity_clause :
+ exception ARITIES of string
+ val arity_clause: string * (string * string list list) list -> ResClause.arityClause list
+ val arity_clause_sg: Sign.sg -> ResClause.arityClause list list * (string * 'a list) list
+ val arity_clause_thy: theory -> ResClause.arityClause list list * (string * 'a list) list
+ type classrelClauses
+ val classrel_clause: string * string list -> ResClause.classrelClause list
+ val classrel_clauses_classrel: Sorts.classes -> ResClause.classrelClause list list
+ val classrel_clauses_sg: Sign.sg -> ResClause.classrelClause list list
+ val classrel_clauses_thy: theory -> ResClause.classrelClause list list
+ val classrel_of_sg: Sign.sg -> Sorts.classes
+ val multi_arity_clause:
(string * (string * string list list) list) list ->
(string * 'a list) list ->
ResClause.arityClause list list * (string * 'a list) list
-val tptp_arity_clause_thy : Theory.theory -> string list list
-val tptp_classrel_clauses_sg : Sign.sg -> string list list
-val tsig_of : Theory.theory -> Type.tsig
-val tsig_of_sg : Sign.sg -> Type.tsig
-
+ val tptp_arity_clause_thy: theory -> string list list
+ val tptp_classrel_clauses_sg : Sign.sg -> string list list
end;
-
-structure ResTypesSorts : RES_TYPES_SORTS =
-
-struct
-
-(**** Isabelle arities ****)
-
-exception ARITIES of string;
-
-fun arity_clause (tcons, []) = raise ARITIES(tcons)
- | arity_clause (tcons,[ar]) = [ResClause.make_axiom_arity_clause (tcons,ar)]
- | arity_clause (tcons,ar1::ars) = (ResClause.make_axiom_arity_clause (tcons,ar1)) :: (arity_clause (tcons,ars));
-
-
-fun multi_arity_clause [] expts = ([], expts)
- | multi_arity_clause ((tcon,[])::tcons_ars) expts =
- multi_arity_clause tcons_ars ((tcon,[])::expts)
- | multi_arity_clause (tcon_ar::tcons_ars) expts =
- let val result = multi_arity_clause tcons_ars expts
- in
- (((arity_clause tcon_ar) :: (fst result)),snd result)
- end;
-
-
-fun tsig_of thy = #tsig(Sign.rep_sg (sign_of thy));
-
-fun tsig_of_sg sg = #tsig(Sign.rep_sg sg);
-
+structure ResTypesSorts: RES_TYPES_SORTS =
+struct
(* Isabelle arities *)
-fun arity_clause_thy thy =
- let val tsig = tsig_of thy
- val arities = #arities (Type.rep_tsig tsig)
- val entries = Symtab.dest arities
- in
- multi_arity_clause entries []
- end;
+
+exception ARITIES of string;
+
+fun arity_clause (tcons, []) = raise ARITIES tcons
+ | arity_clause (tcons, [ar]) = [ResClause.make_axiom_arity_clause (tcons, ar)]
+ | arity_clause (tcons, ar1 :: ars) =
+ ResClause.make_axiom_arity_clause (tcons, ar1) :: arity_clause (tcons, ars);
-fun arity_clause_sig sg =
- let val tsig = #tsig(Sign.rep_sg sg)
- val arities = #arities (Type.rep_tsig tsig)
- val entries = Symtab.dest arities
- in
- multi_arity_clause entries []
- end;
-
+fun multi_arity_clause [] expts = ([], expts)
+ | multi_arity_clause ((tcon, []) :: tcons_ars) expts =
+ multi_arity_clause tcons_ars ((tcon, []) :: expts)
+ | multi_arity_clause (tcon_ar :: tcons_ars) expts =
+ let val result = multi_arity_clause tcons_ars expts
+ in ((arity_clause tcon_ar :: fst result), snd result) end;
-fun tptp_arity_clause_thy thy =
- let val (arclss,_) = arity_clause_thy thy
- in
- map (map ResClause.tptp_arity_clause) arclss
- end;
+fun arity_clause_sg sg =
+ let val arities = #arities (Type.rep_tsig (Sign.tsig_of sg))
+ in multi_arity_clause (Symtab.dest arities) [] end;
-
+fun arity_clause_thy thy = arity_clause_sg (Theory.sign_of thy);
-(**** Isabelle classrel ****)
-
-type classrelClauses = (ResClause.classrelClause list) Symtab.table;
-
+fun tptp_arity_clause_thy thy =
+ map (map ResClause.tptp_arity_clause) (#1 (arity_clause_thy thy));
-(* The new version of finding class relations from a signature *)
-fun classrel_of_sg sg = #classes (Type.rep_tsig (tsig_of_sg sg));
-
-fun classrel_clause (sub, sups) = ResClause.classrelClauses_of (sub,sups);
-
-
+(* Isabelle classes *)
-(* new version of classrel_clauses_classrel *)
-fun classrel_clauses_classrel classrel =
- let val entries = Graph.dest classrel
- in
- map classrel_clause entries
- end;
+type classrelClauses = ResClause.classrelClause list Symtab.table;
-fun classrel_clauses_sg sg =
- let val classrel = classrel_of_sg sg
- in
- classrel_clauses_classrel classrel
- end;
-
+val classrel_of_sg = #2 o #classes o Type.rep_tsig o Sign.tsig_of;
+val classrel_clause = ResClause.classrelClauses_of;
+fun classrel_clauses_classrel (C: Sorts.classes) = map classrel_clause (Graph.dest C);
+val classrel_clauses_sg = classrel_clauses_classrel o classrel_of_sg;
+val classrel_clauses_thy = classrel_clauses_sg o Theory.sign_of;
-val classrel_clauses_thy = classrel_clauses_sg o sign_of;
-
-
-fun tptp_classrel_clauses_sg sg =
- let val relclss = classrel_clauses_sg sg
- in
- map (map ResClause.tptp_classrelClause) relclss
- end;
-
-
-
+val tptp_classrel_clauses_sg =
+ map (map ResClause.tptp_classrelClause) o classrel_clauses_sg;
end;