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