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