src/Tools/Metis/src/NameArity.sml
author blanchet
Thu, 16 Sep 2010 07:30:15 +0200
changeset 39444 beabb8443ee4
parent 39443 e330437cd22a
child 39501 aaa7078fff55
permissions -rw-r--r--
MIT license -> BSD License
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     1
(* ========================================================================= *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     2
(* NAME/ARITY PAIRS                                                          *)
39444
beabb8443ee4 MIT license -> BSD License
blanchet
parents: 39443
diff changeset
     3
(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License            *)
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     4
(* ========================================================================= *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     5
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     6
structure NameArity :> NameArity =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     7
struct
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     8
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     9
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    10
(* A type of name/arity pairs.                                               *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    11
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    12
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    13
type nameArity = Name.name * int;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    14
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    15
fun name ((n,_) : nameArity) = n;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    16
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    17
fun arity ((_,i) : nameArity) = i;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    18
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    19
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    20
(* Testing for different arities.                                            *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    21
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    22
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    23
fun nary i n_i = arity n_i = i;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    24
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    25
val nullary = nary 0
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    26
and unary = nary 1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    27
and binary = nary 2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    28
and ternary = nary 3;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    29
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    30
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    31
(* A total ordering.                                                         *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    32
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    33
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    34
fun compare ((n1,i1),(n2,i2)) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    35
    case Name.compare (n1,n2) of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    36
      LESS => LESS
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    37
    | EQUAL => Int.compare (i1,i2)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    38
    | GREATER => GREATER;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    39
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    40
fun equal (n1,i1) (n2,i2) = i1 = i2 andalso Name.equal n1 n2;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    41
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    42
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    43
(* Parsing and pretty printing.                                              *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    44
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    45
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    46
fun pp (n,i) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    47
    Print.blockProgram Print.Inconsistent 0
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    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
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    50
       Print.ppInt i];
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    51
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    52
end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    53
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    54
structure NameArityOrdered =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    55
struct type t = NameArity.nameArity val compare = NameArity.compare end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    56
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    57
structure NameArityMap =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    58
struct
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    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
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    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
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    72
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    73
end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    74
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    75
structure NameAritySet =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    76
struct
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    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
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    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
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    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
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    91
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    92
end