src/Pure/consts.ML
author wenzelm
Mon Feb 06 20:59:02 2006 +0100 (2006-02-06 ago)
changeset 18935 f22be3d61ed5
parent 18163 9b729737bf14
child 18965 3b76383e3ab3
permissions -rw-r--r--
added abbreviations;
added certify (mostly from sign.ML);
wenzelm@18060
     1
(*  Title:      Pure/consts.ML
wenzelm@18060
     2
    ID:         $Id$
wenzelm@18060
     3
    Author:     Makarius
wenzelm@18060
     4
wenzelm@18935
     5
Polymorphic constants: declarations, abbreviations, additional type
wenzelm@18935
     6
constraints.
wenzelm@18060
     7
*)
wenzelm@18060
     8
wenzelm@18060
     9
signature CONSTS =
wenzelm@18060
    10
sig
wenzelm@18060
    11
  type T
wenzelm@18935
    12
  val dest: T ->
wenzelm@18935
    13
   {constants: (typ * term option) NameSpace.table,
wenzelm@18935
    14
    constraints: typ NameSpace.table}
wenzelm@18060
    15
  val space: T -> NameSpace.T
wenzelm@18935
    16
  val declaration: T -> string -> typ                           (*exception TYPE*)
wenzelm@18935
    17
  val monomorphic: T -> string -> bool                          (*exception TYPE*)
wenzelm@18935
    18
  val constraint: T -> string -> typ                            (*exception TYPE*)
wenzelm@18935
    19
  val expansion: Type.tsig -> T -> string * typ -> term option  (*exception TYPE*)
wenzelm@18935
    20
  val certify: Pretty.pp -> Type.tsig -> T -> term -> term      (*exception TYPE*)
wenzelm@18146
    21
  val typargs: T -> string * typ -> typ list
wenzelm@18163
    22
  val instance: T -> string * typ list -> typ
wenzelm@18060
    23
  val declare: NameSpace.naming -> bstring * typ -> T -> T
wenzelm@18935
    24
  val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string * term -> T -> T
wenzelm@18060
    25
  val constrain: string * typ -> T -> T
wenzelm@18060
    26
  val hide: bool -> string -> T -> T
wenzelm@18060
    27
  val empty: T
wenzelm@18060
    28
  val merge: T * T -> T
wenzelm@18060
    29
end
wenzelm@18060
    30
wenzelm@18060
    31
structure Consts: CONSTS =
wenzelm@18060
    32
struct
wenzelm@18060
    33
wenzelm@18060
    34
(** datatype T **)
wenzelm@18060
    35
wenzelm@18935
    36
datatype decl =
wenzelm@18935
    37
  LogicalConst of typ * int list list |
wenzelm@18935
    38
  Abbreviation of typ * term;
wenzelm@18935
    39
wenzelm@18060
    40
datatype T = Consts of
wenzelm@18935
    41
 {decls: (decl * serial) NameSpace.table,
wenzelm@18060
    42
  constraints: typ Symtab.table};
wenzelm@18060
    43
wenzelm@18935
    44
fun make_consts (decls, constraints) = Consts {decls = decls, constraints = constraints};
wenzelm@18935
    45
fun map_consts f (Consts {decls, constraints}) = make_consts (f (decls, constraints));
wenzelm@18060
    46
wenzelm@18935
    47
fun dest (Consts {decls = (space, decls), constraints}) =
wenzelm@18935
    48
 {constants = (space, Symtab.fold
wenzelm@18935
    49
    (fn (c, (LogicalConst (T, _), _)) => Symtab.update (c, (T, NONE))
wenzelm@18935
    50
      | (c, (Abbreviation (T, t), _)) => Symtab.update (c, (T, SOME t))) decls Symtab.empty),
wenzelm@18060
    51
  constraints = (space, constraints)};
wenzelm@18060
    52
wenzelm@18935
    53
fun space (Consts {decls, ...}) = #1 decls;
wenzelm@18060
    54
wenzelm@18060
    55
wenzelm@18060
    56
(* lookup consts *)
wenzelm@18060
    57
wenzelm@18935
    58
fun err_undeclared c = raise TYPE ("Undeclared constant: " ^ quote c, [], []);
wenzelm@18935
    59
wenzelm@18935
    60
fun the_const (Consts {decls = (_, tab), ...}) c =
wenzelm@18935
    61
  (case Symtab.lookup tab c of SOME (decl, _) => decl | NONE => err_undeclared c);
wenzelm@18935
    62
wenzelm@18935
    63
fun logical_const consts c =
wenzelm@18935
    64
  (case the_const consts c of LogicalConst d => d | _ => err_undeclared c);
wenzelm@18060
    65
wenzelm@18935
    66
fun declaration consts c = #1 (logical_const consts c);
wenzelm@18935
    67
fun monomorphic consts c = null (#2 (logical_const consts c));
wenzelm@18935
    68
wenzelm@18935
    69
fun expansion tsig consts (c, T) =
wenzelm@18935
    70
  (case the_const consts c of
wenzelm@18935
    71
    Abbreviation a => SOME (Envir.expand_atom tsig T a)
wenzelm@18935
    72
  | _ => NONE);
wenzelm@18060
    73
wenzelm@18060
    74
fun constraint (consts as Consts {constraints, ...}) c =
wenzelm@18060
    75
  (case Symtab.lookup constraints c of
wenzelm@18060
    76
    SOME T => T
wenzelm@18935
    77
  | NONE => (case the_const consts c of LogicalConst (T, _) => T | Abbreviation (T, _) => T));
wenzelm@18935
    78
wenzelm@18935
    79
wenzelm@18935
    80
(* certify: check/expand consts -- without beta normalization *)
wenzelm@18935
    81
wenzelm@18935
    82
fun certify pp tsig consts tm =
wenzelm@18935
    83
  let
wenzelm@18935
    84
    fun err msg = raise TYPE (msg, [], [tm]);
wenzelm@18935
    85
    fun show_const (c, T) = quote c ^ " :: " ^ Pretty.string_of_typ pp T;
wenzelm@18060
    86
wenzelm@18935
    87
    fun cert (t as Const (c, T)) =
wenzelm@18935
    88
          (case the_const consts c of
wenzelm@18935
    89
            LogicalConst (U, _) =>
wenzelm@18935
    90
              if Type.typ_instance tsig (T, U) then t
wenzelm@18935
    91
              else err ("Illegal type for constant " ^ show_const (c, T))
wenzelm@18935
    92
          | Abbreviation (U, u) =>
wenzelm@18935
    93
              Envir.expand_atom tsig T (U, u) handle TYPE _ =>
wenzelm@18935
    94
                err ("Illegal type for abbreviation " ^ show_const (c, T)))
wenzelm@18935
    95
      | cert (t $ u) = cert t $ cert u
wenzelm@18935
    96
      | cert (Abs (x, T, t)) = Abs (x, T, cert t)
wenzelm@18935
    97
      | cert a = a;
wenzelm@18935
    98
  in cert tm end;
wenzelm@18060
    99
wenzelm@18060
   100
wenzelm@18060
   101
(* typargs -- view actual const type as instance of declaration *)
wenzelm@18060
   102
wenzelm@18060
   103
fun sub (Type (_, Ts)) (i :: is) = sub (nth Ts i) is
wenzelm@18060
   104
  | sub T [] = T
wenzelm@18060
   105
  | sub T _ = raise Subscript;
wenzelm@18060
   106
wenzelm@18935
   107
fun typargs consts (c, T) = map (sub T) (#2 (logical_const consts c));
wenzelm@18060
   108
wenzelm@18163
   109
fun instance consts (c, Ts) =
wenzelm@18163
   110
  let
wenzelm@18163
   111
    val declT = declaration consts c;
wenzelm@18163
   112
    val vars = map Term.dest_TVar (typargs consts (c, declT));
wenzelm@18163
   113
  in declT |> Term.instantiateT (vars ~~ Ts) end;
wenzelm@18163
   114
wenzelm@18060
   115
wenzelm@18060
   116
wenzelm@18935
   117
(** declare consts **)
wenzelm@18060
   118
wenzelm@18060
   119
fun err_dup_consts cs =
wenzelm@18060
   120
  error ("Duplicate declaration of constant(s) " ^ commas_quote cs);
wenzelm@18060
   121
wenzelm@18060
   122
fun err_inconsistent_constraints cs =
wenzelm@18060
   123
  error ("Inconsistent type constraints for constant(s) " ^ commas_quote cs);
wenzelm@18060
   124
wenzelm@18935
   125
fun extend_decls naming decl tab = NameSpace.extend_table naming (tab, [decl])
wenzelm@18935
   126
  handle Symtab.DUPS cs => err_dup_consts cs;
wenzelm@18060
   127
wenzelm@18935
   128
wenzelm@18935
   129
(* name space *)
wenzelm@18060
   130
wenzelm@18935
   131
fun hide fully c = map_consts (fn (decls, constraints) =>
wenzelm@18935
   132
  (apfst (NameSpace.hide fully c) decls, constraints));
wenzelm@18935
   133
wenzelm@18935
   134
wenzelm@18935
   135
(* declarations *)
wenzelm@18935
   136
wenzelm@18935
   137
fun declare naming (c, declT) = map_consts (fn (decls, constraints) =>
wenzelm@18060
   138
  let
wenzelm@18935
   139
    fun args_of (Type (_, Ts)) pos = args_of_list Ts 0 pos
wenzelm@18935
   140
      | args_of (TVar v) pos = insert (eq_fst op =) (v, rev pos)
wenzelm@18935
   141
      | args_of (TFree _) _ = I
wenzelm@18935
   142
    and args_of_list (T :: Ts) i is = args_of T (i :: is) #> args_of_list Ts (i + 1) is
wenzelm@18935
   143
      | args_of_list [] _ _ = I;
wenzelm@18935
   144
    val decl = (c, (LogicalConst (declT, map #2 (rev (args_of declT [] []))), serial ()));
wenzelm@18935
   145
  in (extend_decls naming decl decls, constraints) end);
wenzelm@18060
   146
wenzelm@18935
   147
wenzelm@18935
   148
(* abbreviations *)
wenzelm@18935
   149
wenzelm@18935
   150
fun abbreviate pp tsig naming (c, rhs) consts =
wenzelm@18935
   151
    consts |> map_consts (fn (decls, constraints) =>
wenzelm@18060
   152
  let
wenzelm@18935
   153
    val rhs' = Envir.beta_norm (certify pp tsig consts rhs);
wenzelm@18935
   154
    val decl = (c, (Abbreviation (Term.fastype_of rhs', rhs'), serial ()));
wenzelm@18935
   155
  in (extend_decls naming decl decls, constraints) end);
wenzelm@18935
   156
wenzelm@18060
   157
wenzelm@18935
   158
(* constraints *)
wenzelm@18060
   159
wenzelm@18935
   160
fun constrain (c, T) =
wenzelm@18935
   161
  map_consts (fn (decls, constraints) => (decls, Symtab.update (c, T) constraints));
wenzelm@18060
   162
wenzelm@18060
   163
wenzelm@18060
   164
(* empty and merge *)
wenzelm@18060
   165
wenzelm@18060
   166
val empty = make_consts (NameSpace.empty_table, Symtab.empty);
wenzelm@18060
   167
wenzelm@18060
   168
fun merge
wenzelm@18935
   169
  (Consts {decls = decls1, constraints = constraints1},
wenzelm@18935
   170
   Consts {decls = decls2, constraints = constraints2}) =
wenzelm@18060
   171
  let
wenzelm@18935
   172
    val decls' = NameSpace.merge_tables (eq_snd (op =)) (decls1, decls2)
wenzelm@18060
   173
      handle Symtab.DUPS cs => err_dup_consts cs;
wenzelm@18935
   174
    val constraints' = Symtab.merge (op =) (constraints1, constraints2)
wenzelm@18060
   175
      handle Symtab.DUPS cs => err_inconsistent_constraints cs;
wenzelm@18935
   176
  in make_consts (decls', constraints') end;
wenzelm@18060
   177
wenzelm@18060
   178
end;