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