src/Tools/Metis/src/Name.sml
author blanchet
Mon, 13 Sep 2010 21:11:59 +0200
changeset 39349 2d0a4361c3ef
parent 39348 6f9c9899f99f
child 39353 7f11d833d65b
permissions -rw-r--r--
change license, with Joe Hurd's permission
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
(* NAMES                                                                     *)
39349
2d0a4361c3ef change license, with Joe Hurd's permission
blanchet
parents: 39348
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 Name :> Name =
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
open Useful;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    10
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    11
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    12
(* A type of names.                                                          *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    13
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    14
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    15
type name = string;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    16
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    17
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    18
(* A total ordering.                                                         *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    19
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    20
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    21
val compare = String.compare;
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 equal n1 n2 = n1 = n2;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    24
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    25
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    26
(* Fresh variables.                                                          *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    27
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    28
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    29
local
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    30
  val prefix  = "_";
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    31
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    32
  fun numName i = mkPrefix prefix (Int.toString i);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    33
in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    34
  fun newName () = numName (newInt ());
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    35
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    36
  fun newNames n = map numName (newInts n);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    37
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    38
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    39
fun variantPrime acceptable =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    40
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    41
      fun variant n = if acceptable n then n else variant (n ^ "'")
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    42
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    43
      variant
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    44
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    45
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    46
local
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    47
  fun isDigitOrPrime #"'" = true
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    48
    | isDigitOrPrime c = Char.isDigit c;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    49
in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    50
  fun variantNum acceptable n =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    51
      if acceptable n then n
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    52
      else
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    53
        let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    54
          val n = stripSuffix isDigitOrPrime n
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    55
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    56
          fun variant i =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    57
              let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    58
                val n_i = n ^ Int.toString i
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    59
              in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    60
                if acceptable n_i then n_i else variant (i + 1)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    61
              end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    62
        in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    63
          variant 0
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    64
        end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    65
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    66
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    67
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    68
(* Parsing and pretty printing.                                              *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    69
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    70
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    71
val pp = Print.ppString;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    72
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    73
fun toString s : string = s;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    74
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    75
fun fromString s : name = s;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    76
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    77
end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    78
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    79
structure NameOrdered =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    80
struct type t = Name.name val compare = Name.compare end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    81
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    82
structure NameMap = KeyMap (NameOrdered);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    83
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    84
structure NameSet =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    85
struct
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    86
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    87
  local
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    88
    structure S = ElementSet (NameMap);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    89
  in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    90
    open S;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    91
  end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    92
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    93
  val pp =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    94
      Print.ppMap
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    95
        toList
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    96
        (Print.ppBracket "{" "}" (Print.ppOpList "," Name.pp));
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    97
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    98
end