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 ***
     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;