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