src/Pure/consts.ML
author wenzelm
Thu Nov 10 20:57:16 2005 +0100 (2005-11-10 ago)
changeset 18146 47463b1825c6
parent 18117 61a430a67d7c
child 18163 9b729737bf14
permissions -rw-r--r--
uncurried Consts.typargs;
wenzelm@18060
     1
(*  Title:      Pure/consts.ML
wenzelm@18060
     2
    ID:         $Id$
wenzelm@18060
     3
    Author:     Makarius
wenzelm@18060
     4
wenzelm@18060
     5
Polymorphic constants.
wenzelm@18060
     6
*)
wenzelm@18060
     7
wenzelm@18060
     8
signature CONSTS =
wenzelm@18060
     9
sig
wenzelm@18060
    10
  type T
wenzelm@18060
    11
  val dest: T -> {declarations: typ NameSpace.table, constraints: typ NameSpace.table}
wenzelm@18060
    12
  val space: T -> NameSpace.T
wenzelm@18060
    13
  val declaration: T -> string -> typ  (*exception TYPE*)
wenzelm@18060
    14
  val constraint: T -> string -> typ    (*exception TYPE*)
wenzelm@18060
    15
  val monomorphic: T -> string -> bool
wenzelm@18146
    16
  val typargs: T -> string * typ -> typ list
wenzelm@18060
    17
  val declare: NameSpace.naming -> bstring * typ -> T -> T
wenzelm@18060
    18
  val constrain: string * typ -> T -> T
wenzelm@18060
    19
  val hide: bool -> string -> T -> T
wenzelm@18060
    20
  val empty: T
wenzelm@18060
    21
  val merge: T * T -> T
wenzelm@18060
    22
end
wenzelm@18060
    23
wenzelm@18060
    24
structure Consts: CONSTS =
wenzelm@18060
    25
struct
wenzelm@18060
    26
wenzelm@18060
    27
wenzelm@18060
    28
(** datatype T **)
wenzelm@18060
    29
wenzelm@18060
    30
datatype T = Consts of
wenzelm@18117
    31
 {declarations: ((typ * int list list) * serial) NameSpace.table,
wenzelm@18060
    32
  constraints: typ Symtab.table};
wenzelm@18060
    33
wenzelm@18060
    34
fun make_consts (declarations, constraints) =
wenzelm@18060
    35
  Consts {declarations = declarations, constraints = constraints};
wenzelm@18060
    36
wenzelm@18060
    37
fun map_consts f (Consts {declarations, constraints}) =
wenzelm@18060
    38
  make_consts (f (declarations, constraints));
wenzelm@18060
    39
wenzelm@18060
    40
fun dest (Consts {declarations = (space, decls), constraints}) =
wenzelm@18060
    41
 {declarations = (space, Symtab.map (#1 o #1) decls),
wenzelm@18060
    42
  constraints = (space, constraints)};
wenzelm@18060
    43
wenzelm@18060
    44
fun space (Consts {declarations = (space, _), ...}) = space;
wenzelm@18060
    45
wenzelm@18060
    46
wenzelm@18060
    47
(* lookup consts *)
wenzelm@18060
    48
wenzelm@18060
    49
fun the_const (Consts {declarations = (_, decls), ...}) c =
wenzelm@18060
    50
  (case Symtab.lookup decls c of SOME (decl, _) => decl
wenzelm@18060
    51
  | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], []));
wenzelm@18060
    52
wenzelm@18060
    53
fun declaration consts c = #1 (the_const consts c);
wenzelm@18060
    54
wenzelm@18060
    55
fun constraint (consts as Consts {constraints, ...}) c =
wenzelm@18060
    56
  (case Symtab.lookup constraints c of
wenzelm@18060
    57
    SOME T => T
wenzelm@18060
    58
  | NONE => declaration consts c);
wenzelm@18060
    59
wenzelm@18060
    60
fun monomorphic consts c = null (#2 (the_const consts c));
wenzelm@18060
    61
wenzelm@18060
    62
wenzelm@18060
    63
(* typargs -- view actual const type as instance of declaration *)
wenzelm@18060
    64
wenzelm@18060
    65
fun sub (Type (_, Ts)) (i :: is) = sub (nth Ts i) is
wenzelm@18060
    66
  | sub T [] = T
wenzelm@18060
    67
  | sub T _ = raise Subscript;
wenzelm@18060
    68
wenzelm@18146
    69
fun typargs consts (c, T) = map (sub T) (#2 (the_const consts c));
wenzelm@18060
    70
wenzelm@18060
    71
wenzelm@18060
    72
wenzelm@18060
    73
(** build consts **)
wenzelm@18060
    74
wenzelm@18060
    75
fun err_dup_consts cs =
wenzelm@18060
    76
  error ("Duplicate declaration of constant(s) " ^ commas_quote cs);
wenzelm@18060
    77
wenzelm@18060
    78
fun err_inconsistent_constraints cs =
wenzelm@18060
    79
  error ("Inconsistent type constraints for constant(s) " ^ commas_quote cs);
wenzelm@18060
    80
wenzelm@18060
    81
wenzelm@18060
    82
(* declarations etc. *)
wenzelm@18060
    83
wenzelm@18060
    84
fun args_of declT =
wenzelm@18060
    85
  let
wenzelm@18060
    86
    fun args (Type (_, Ts)) pos = args_list Ts 0 pos
wenzelm@18060
    87
      | args (TVar v) pos = insert (eq_fst op =) (v, rev pos)
wenzelm@18060
    88
      | args (TFree _) _ = I
wenzelm@18060
    89
    and args_list (T :: Ts) i is = args T (i :: is) #> args_list Ts (i + 1) is
wenzelm@18060
    90
      | args_list [] _ _ = I;
wenzelm@18117
    91
  in map #2 (rev (args declT [] [])) end;
wenzelm@18060
    92
wenzelm@18060
    93
fun declare naming (c, T) = map_consts (apfst (fn declarations =>
wenzelm@18060
    94
  let
wenzelm@18060
    95
    val decl = (c, ((T, args_of T), serial ()));
wenzelm@18060
    96
    val declarations' = NameSpace.extend_table naming (declarations, [decl])
wenzelm@18060
    97
      handle Symtab.DUPS cs => err_dup_consts cs;
wenzelm@18060
    98
  in declarations' end));
wenzelm@18060
    99
wenzelm@18060
   100
val constrain = map_consts o apsnd o Symtab.update;
wenzelm@18060
   101
wenzelm@18060
   102
fun hide fully c = map_consts (apfst (apfst (NameSpace.hide fully c)));
wenzelm@18060
   103
wenzelm@18060
   104
wenzelm@18060
   105
(* empty and merge *)
wenzelm@18060
   106
wenzelm@18060
   107
val empty = make_consts (NameSpace.empty_table, Symtab.empty);
wenzelm@18060
   108
wenzelm@18060
   109
fun merge
wenzelm@18060
   110
  (Consts {declarations = declarations1, constraints = constraints1},
wenzelm@18060
   111
   Consts {declarations = declarations2, constraints = constraints2}) =
wenzelm@18060
   112
  let
wenzelm@18060
   113
    val declarations = NameSpace.merge_tables (eq_snd (op =)) (declarations1, declarations2)
wenzelm@18060
   114
      handle Symtab.DUPS cs => err_dup_consts cs;
wenzelm@18060
   115
    val constraints = Symtab.merge (op =) (constraints1, constraints2)
wenzelm@18060
   116
      handle Symtab.DUPS cs => err_inconsistent_constraints cs;
wenzelm@18060
   117
  in make_consts (declarations, constraints) end;
wenzelm@18060
   118
wenzelm@18060
   119
end;