author | wenzelm |
Sun, 12 Jan 2025 23:07:50 +0100 | |
changeset 81802 | 4d78ad5abeca |
parent 72004 | 913162a47d9f |
permissions | -rw-r--r-- |
39348 | 1 |
(* ========================================================================= *) |
2 |
(* NAME/ARITY PAIRS *) |
|
72004 | 3 |
(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *) |
39348 | 4 |
(* ========================================================================= *) |
5 |
||
6 |
structure NameArity :> NameArity = |
|
7 |
struct |
|
8 |
||
9 |
(* ------------------------------------------------------------------------- *) |
|
10 |
(* A type of name/arity pairs. *) |
|
11 |
(* ------------------------------------------------------------------------- *) |
|
12 |
||
13 |
type nameArity = Name.name * int; |
|
14 |
||
15 |
fun name ((n,_) : nameArity) = n; |
|
16 |
||
17 |
fun arity ((_,i) : nameArity) = i; |
|
18 |
||
19 |
(* ------------------------------------------------------------------------- *) |
|
20 |
(* Testing for different arities. *) |
|
21 |
(* ------------------------------------------------------------------------- *) |
|
22 |
||
23 |
fun nary i n_i = arity n_i = i; |
|
24 |
||
25 |
val nullary = nary 0 |
|
26 |
and unary = nary 1 |
|
27 |
and binary = nary 2 |
|
28 |
and ternary = nary 3; |
|
29 |
||
30 |
(* ------------------------------------------------------------------------- *) |
|
31 |
(* A total ordering. *) |
|
32 |
(* ------------------------------------------------------------------------- *) |
|
33 |
||
34 |
fun compare ((n1,i1),(n2,i2)) = |
|
35 |
case Name.compare (n1,n2) of |
|
36 |
LESS => LESS |
|
37 |
| EQUAL => Int.compare (i1,i2) |
|
38 |
| GREATER => GREATER; |
|
39 |
||
40 |
fun equal (n1,i1) (n2,i2) = i1 = i2 andalso Name.equal n1 n2; |
|
41 |
||
42 |
(* ------------------------------------------------------------------------- *) |
|
43 |
(* Parsing and pretty printing. *) |
|
44 |
(* ------------------------------------------------------------------------- *) |
|
45 |
||
46 |
fun pp (n,i) = |
|
45778 | 47 |
Print.inconsistentBlock 0 |
39348 | 48 |
[Name.pp n, |
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
49 |
Print.ppString "/", |
39348 | 50 |
Print.ppInt i]; |
51 |
||
52 |
end |
|
53 |
||
54 |
structure NameArityOrdered = |
|
55 |
struct type t = NameArity.nameArity val compare = NameArity.compare end |
|
56 |
||
57 |
structure NameArityMap = |
|
58 |
struct |
|
59 |
||
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
60 |
local |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
61 |
structure S = KeyMap (NameArityOrdered); |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
62 |
in |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
63 |
open S; |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
64 |
end; |
39348 | 65 |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
66 |
fun compose m1 m2 = |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
67 |
let |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
68 |
fun pk ((_,a),n) = peek m2 (n,a) |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
69 |
in |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
70 |
mapPartial pk m1 |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
71 |
end; |
39348 | 72 |
|
73 |
end |
|
74 |
||
75 |
structure NameAritySet = |
|
76 |
struct |
|
77 |
||
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
78 |
local |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
79 |
structure S = ElementSet (NameArityMap); |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
80 |
in |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
81 |
open S; |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
82 |
end; |
39348 | 83 |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
84 |
val allNullary = all NameArity.nullary; |
39348 | 85 |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
86 |
val pp = |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
87 |
Print.ppMap |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
88 |
toList |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
89 |
(Print.ppBracket "{" "}" (Print.ppOpList "," NameArity.pp)); |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
90 |
|
39348 | 91 |
|
92 |
end |