author | paulson |
Tue, 20 Sep 2005 18:43:39 +0200 | |
changeset 17525 | ae5bb6001afb |
parent 16803 | 014090d1e64b |
permissions | -rw-r--r-- |
16367 | 1 |
(* Author: Jia Meng, Cambridge University Computer Laboratory |
15347 | 2 |
ID: $Id$ |
3 |
Copyright 2004 University of Cambridge |
|
4 |
||
16367 | 5 |
Transformation of Isabelle arities and class relations into clauses |
6 |
(defined in the structure Clause). |
|
15347 | 7 |
*) |
8 |
||
9 |
signature RES_TYPES_SORTS = |
|
10 |
sig |
|
16367 | 11 |
exception ARITIES of string |
12 |
val arity_clause: string * (string * string list list) list -> ResClause.arityClause list |
|
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
16803
diff
changeset
|
13 |
val arity_clause_thy: theory -> ResClause.arityClause list |
16367 | 14 |
type classrelClauses |
15 |
val classrel_clause: string * string list -> ResClause.classrelClause list |
|
16 |
val classrel_clauses_classrel: Sorts.classes -> ResClause.classrelClause list list |
|
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
16803
diff
changeset
|
17 |
val classrel_clauses_thy: theory -> ResClause.classrelClause list |
15347 | 18 |
end; |
19 |
||
16367 | 20 |
structure ResTypesSorts: RES_TYPES_SORTS = |
21 |
struct |
|
15347 | 22 |
|
23 |
(* Isabelle arities *) |
|
16367 | 24 |
|
25 |
exception ARITIES of string; |
|
26 |
||
27 |
fun arity_clause (tcons, []) = raise ARITIES tcons |
|
28 |
| arity_clause (tcons, [ar]) = [ResClause.make_axiom_arity_clause (tcons, ar)] |
|
29 |
| arity_clause (tcons, ar1 :: ars) = |
|
30 |
ResClause.make_axiom_arity_clause (tcons, ar1) :: arity_clause (tcons, ars); |
|
15347 | 31 |
|
16367 | 32 |
fun multi_arity_clause [] expts = ([], expts) |
33 |
| multi_arity_clause ((tcon, []) :: tcons_ars) expts = |
|
34 |
multi_arity_clause tcons_ars ((tcon, []) :: expts) |
|
35 |
| multi_arity_clause (tcon_ar :: tcons_ars) expts = |
|
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
16803
diff
changeset
|
36 |
let val (cls,ary) = multi_arity_clause tcons_ars expts |
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
16803
diff
changeset
|
37 |
in ((arity_clause tcon_ar @ cls), ary) end; |
15347 | 38 |
|
16803 | 39 |
fun arity_clause_thy thy = |
40 |
let val arities = #arities (Type.rep_tsig (Sign.tsig_of thy)) |
|
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
16803
diff
changeset
|
41 |
in #1 (multi_arity_clause (Symtab.dest arities) []) end; |
15347 | 42 |
|
43 |
||
16367 | 44 |
(* Isabelle classes *) |
15347 | 45 |
|
16367 | 46 |
type classrelClauses = ResClause.classrelClause list Symtab.table; |
15347 | 47 |
|
16803 | 48 |
val classrel_of = #2 o #classes o Type.rep_tsig o Sign.tsig_of; |
16367 | 49 |
val classrel_clause = ResClause.classrelClauses_of; |
50 |
fun classrel_clauses_classrel (C: Sorts.classes) = map classrel_clause (Graph.dest C); |
|
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
16803
diff
changeset
|
51 |
val classrel_clauses_thy = List.concat o classrel_clauses_classrel o classrel_of; |
15347 | 52 |
|
53 |
end; |