src/Pure/consts.ML
author wenzelm
Sun Oct 25 13:18:35 2009 +0100 (2009-10-25 ago)
changeset 33158 6e3dc0ba2b06
parent 33097 9d501e11084a
child 33173 b8ca12f6681a
permissions -rw-r--r--
conceal consts via name space, not tags;
wenzelm@18060
     1
(*  Title:      Pure/consts.ML
wenzelm@18060
     2
    Author:     Makarius
wenzelm@18060
     3
wenzelm@18935
     4
Polymorphic constants: declarations, abbreviations, additional type
wenzelm@18935
     5
constraints.
wenzelm@18060
     6
*)
wenzelm@18060
     7
wenzelm@18060
     8
signature CONSTS =
wenzelm@18060
     9
sig
wenzelm@18060
    10
  type T
wenzelm@30424
    11
  val eq_consts: T * T -> bool
wenzelm@30566
    12
  val retrieve_abbrevs: T -> string list -> term -> (term * term) list
wenzelm@18935
    13
  val dest: T ->
wenzelm@33095
    14
   {constants: (typ * term option) Name_Space.table,
wenzelm@33095
    15
    constraints: typ Name_Space.table}
wenzelm@25048
    16
  val the_type: T -> string -> typ                             (*exception TYPE*)
wenzelm@25048
    17
  val the_abbreviation: T -> string -> typ * term              (*exception TYPE*)
wenzelm@25048
    18
  val type_scheme: T -> string -> typ                          (*exception TYPE*)
wenzelm@28017
    19
  val the_tags: T -> string -> Properties.T                    (*exception TYPE*)
wenzelm@25048
    20
  val is_monomorphic: T -> string -> bool                      (*exception TYPE*)
wenzelm@25048
    21
  val the_constraint: T -> string -> typ                       (*exception TYPE*)
wenzelm@33095
    22
  val space_of: T -> Name_Space.T
wenzelm@33158
    23
  val is_concealed: T -> string -> bool
wenzelm@19364
    24
  val intern: T -> xstring -> string
wenzelm@19364
    25
  val extern: T -> string -> xstring
wenzelm@19364
    26
  val extern_early: T -> string -> xstring
wenzelm@19657
    27
  val syntax: T -> string * mixfix -> string * typ * mixfix
wenzelm@21181
    28
  val syntax_name: T -> string -> string
wenzelm@18965
    29
  val read_const: T -> string -> term
wenzelm@24673
    30
  val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
wenzelm@18146
    31
  val typargs: T -> string * typ -> typ list
wenzelm@18163
    32
  val instance: T -> string * typ list -> typ
wenzelm@33096
    33
  val declare: bool -> Name_Space.naming -> Properties.T -> binding * typ -> T -> T
wenzelm@19098
    34
  val constrain: string * typ option -> T -> T
wenzelm@33095
    35
  val abbreviate: Pretty.pp -> Type.tsig -> Name_Space.naming -> string -> Properties.T ->
haftmann@29581
    36
    binding * term -> T -> (term * term) * T
wenzelm@25048
    37
  val revert_abbrev: string -> string -> T -> T
wenzelm@18060
    38
  val hide: bool -> string -> T -> T
wenzelm@18060
    39
  val empty: T
wenzelm@18060
    40
  val merge: T * T -> T
wenzelm@19364
    41
end;
wenzelm@18060
    42
wenzelm@18060
    43
structure Consts: CONSTS =
wenzelm@18060
    44
struct
wenzelm@18060
    45
wenzelm@19364
    46
(** consts type **)
wenzelm@19364
    47
wenzelm@19364
    48
(* datatype T *)
wenzelm@18060
    49
wenzelm@28017
    50
type decl = {T: typ, typargs: int list list, tags: Properties.T, authentic: bool};
wenzelm@24909
    51
type abbrev = {rhs: term, normal_rhs: term, force_expand: bool};
wenzelm@18935
    52
wenzelm@18060
    53
datatype T = Consts of
wenzelm@33095
    54
 {decls: (decl * abbrev option) Name_Space.table,
wenzelm@19364
    55
  constraints: typ Symtab.table,
wenzelm@30566
    56
  rev_abbrevs: (term * term) Item_Net.T Symtab.table};
wenzelm@18060
    57
wenzelm@30424
    58
fun eq_consts
wenzelm@30424
    59
   (Consts {decls = decls1, constraints = constraints1, rev_abbrevs = rev_abbrevs1},
wenzelm@30424
    60
    Consts {decls = decls2, constraints = constraints2, rev_abbrevs = rev_abbrevs2}) =
wenzelm@30424
    61
  pointer_eq (decls1, decls2) andalso
wenzelm@30424
    62
  pointer_eq (constraints1, constraints2) andalso
wenzelm@30424
    63
  pointer_eq (rev_abbrevs1, rev_abbrevs2);
wenzelm@30424
    64
wenzelm@24673
    65
fun make_consts (decls, constraints, rev_abbrevs) =
wenzelm@30284
    66
  Consts {decls = decls, constraints = constraints, rev_abbrevs = rev_abbrevs};
wenzelm@18060
    67
wenzelm@30284
    68
fun map_consts f (Consts {decls, constraints, rev_abbrevs}) =
wenzelm@24673
    69
  make_consts (f (decls, constraints, rev_abbrevs));
wenzelm@19364
    70
wenzelm@30566
    71
wenzelm@30566
    72
(* reverted abbrevs *)
wenzelm@30566
    73
wenzelm@30566
    74
val empty_abbrevs = Item_Net.init (fn ((t, u), (t', u')) => t aconv t' andalso u aconv u') #1;
wenzelm@30566
    75
wenzelm@30566
    76
fun insert_abbrevs mode abbrs =
wenzelm@30568
    77
  Symtab.map_default (mode, empty_abbrevs) (Item_Net.insert abbrs);
wenzelm@30566
    78
wenzelm@30566
    79
fun retrieve_abbrevs (Consts {rev_abbrevs, ...}) modes =
wenzelm@30566
    80
  let val nets = map_filter (Symtab.lookup rev_abbrevs) modes
wenzelm@30566
    81
  in fn t => maps (fn net => Item_Net.retrieve net t) nets end;
wenzelm@19364
    82
wenzelm@18965
    83
wenzelm@19364
    84
(* dest consts *)
wenzelm@19364
    85
wenzelm@30284
    86
fun dest (Consts {decls = (space, decls), constraints, ...}) =
wenzelm@19364
    87
 {constants = (space,
wenzelm@33092
    88
    Symtab.fold (fn (c, ({T, ...}, abbr)) =>
wenzelm@25404
    89
      Symtab.update (c, (T, Option.map #rhs abbr))) decls Symtab.empty),
wenzelm@18060
    90
  constraints = (space, constraints)};
wenzelm@18060
    91
wenzelm@18060
    92
wenzelm@18060
    93
(* lookup consts *)
wenzelm@18060
    94
wenzelm@30284
    95
fun the_const (Consts {decls = (_, tab), ...}) c =
wenzelm@19364
    96
  (case Symtab.lookup tab c of
wenzelm@33092
    97
    SOME decl => decl
wenzelm@25041
    98
  | NONE => raise TYPE ("Unknown constant: " ^ quote c, [], []));
wenzelm@18935
    99
wenzelm@25041
   100
fun the_type consts c =
wenzelm@24772
   101
  (case the_const consts c of
wenzelm@24909
   102
    ({T, ...}, NONE) => T
wenzelm@21720
   103
  | _ => raise TYPE ("Not a logical constant: " ^ quote c, [], []));
wenzelm@18060
   104
wenzelm@21720
   105
fun the_abbreviation consts c =
wenzelm@24772
   106
  (case the_const consts c of
wenzelm@25048
   107
    ({T, ...}, SOME {rhs, ...}) => (T, rhs)
wenzelm@21720
   108
  | _ => raise TYPE ("Not an abbreviated constant: " ^ quote c, [], []));
wenzelm@21720
   109
wenzelm@25041
   110
val the_decl = #1 oo the_const;
wenzelm@25041
   111
val type_scheme = #T oo the_decl;
wenzelm@25041
   112
val type_arguments = #typargs oo the_decl;
wenzelm@25041
   113
val the_tags = #tags oo the_decl;
wenzelm@25041
   114
wenzelm@21720
   115
val is_monomorphic = null oo type_arguments;
wenzelm@18935
   116
wenzelm@30284
   117
fun the_constraint (consts as Consts {constraints, ...}) c =
wenzelm@18060
   118
  (case Symtab.lookup constraints c of
wenzelm@18060
   119
    SOME T => T
wenzelm@25041
   120
  | NONE => type_scheme consts c);
wenzelm@18935
   121
wenzelm@18935
   122
wenzelm@19657
   123
(* name space and syntax *)
wenzelm@19364
   124
wenzelm@30284
   125
fun space_of (Consts {decls = (space, _), ...}) = space;
wenzelm@19364
   126
wenzelm@33158
   127
val is_concealed = Name_Space.is_concealed o space_of;
wenzelm@33158
   128
wenzelm@33095
   129
val intern = Name_Space.intern o space_of;
wenzelm@33095
   130
val extern = Name_Space.extern o space_of;
wenzelm@19364
   131
wenzelm@19364
   132
fun extern_early consts c =
wenzelm@19364
   133
  (case try (the_const consts) c of
wenzelm@24909
   134
    SOME ({authentic = true, ...}, _) => Syntax.constN ^ c
wenzelm@19576
   135
  | _ => extern consts c);
wenzelm@19364
   136
wenzelm@19657
   137
fun syntax consts (c, mx) =
wenzelm@19657
   138
  let
wenzelm@24909
   139
    val ({T, authentic, ...}, _) = the_const consts c handle TYPE (msg, _, _) => error msg;
wenzelm@30364
   140
    val c' = if authentic then Syntax.constN ^ c else Long_Name.base_name c;
wenzelm@19657
   141
  in (c', T, mx) end;
wenzelm@19657
   142
wenzelm@21181
   143
fun syntax_name consts c = #1 (syntax consts (c, NoSyn));
wenzelm@21181
   144
wenzelm@18060
   145
wenzelm@19364
   146
(* read_const *)
wenzelm@19364
   147
wenzelm@19364
   148
fun read_const consts raw_c =
wenzelm@19364
   149
  let
wenzelm@19364
   150
    val c = intern consts raw_c;
wenzelm@25041
   151
    val T = type_scheme consts c handle TYPE (msg, _, _) => error msg;
wenzelm@21205
   152
  in Const (c, T) end;
wenzelm@19364
   153
wenzelm@19364
   154
wenzelm@19364
   155
(* certify *)
wenzelm@19364
   156
wenzelm@24673
   157
fun certify pp tsig do_expand consts =
wenzelm@18965
   158
  let
wenzelm@18965
   159
    fun err msg (c, T) =
wenzelm@18965
   160
      raise TYPE (msg ^ " " ^ quote c ^ " :: " ^ Pretty.string_of_typ pp T, [], []);
wenzelm@24673
   161
    val certT = Type.cert_typ tsig;
wenzelm@18965
   162
    fun cert tm =
wenzelm@18965
   163
      let
wenzelm@18965
   164
        val (head, args) = Term.strip_comb tm;
wenzelm@21694
   165
        val args' = map cert args;
wenzelm@21694
   166
        fun comb head' = Term.list_comb (head', args');
wenzelm@18965
   167
      in
wenzelm@18965
   168
        (case head of
wenzelm@24673
   169
          Abs (x, T, t) => comb (Abs (x, certT T, cert t))
wenzelm@19364
   170
        | Const (c, T) =>
wenzelm@19364
   171
            let
wenzelm@24673
   172
              val T' = certT T;
wenzelm@24909
   173
              val ({T = U, ...}, abbr) = the_const consts c;
wenzelm@25048
   174
              fun expand u =
wenzelm@25048
   175
                Term.betapplys (Envir.expand_atom T' (U, u) handle TYPE _ =>
wenzelm@25048
   176
                  err "Illegal type for abbreviation" (c, T), args');
wenzelm@19364
   177
            in
wenzelm@19433
   178
              if not (Type.raw_instance (T', U)) then
wenzelm@19364
   179
                err "Illegal type for constant" (c, T)
wenzelm@19364
   180
              else
wenzelm@24909
   181
                (case abbr of
wenzelm@25048
   182
                  SOME {rhs, normal_rhs, force_expand} =>
wenzelm@25048
   183
                    if do_expand then expand normal_rhs
wenzelm@25048
   184
                    else if force_expand then expand rhs
wenzelm@21720
   185
                    else comb head
wenzelm@19364
   186
                | _ => comb head)
wenzelm@19364
   187
            end
wenzelm@19364
   188
        | _ => comb head)
wenzelm@18965
   189
      end;
wenzelm@18965
   190
  in cert end;
wenzelm@18965
   191
wenzelm@18965
   192
wenzelm@18060
   193
(* typargs -- view actual const type as instance of declaration *)
wenzelm@18060
   194
wenzelm@24909
   195
local
wenzelm@24909
   196
wenzelm@24909
   197
fun args_of (Type (_, Ts)) pos = args_of_list Ts 0 pos
wenzelm@24909
   198
  | args_of (TVar v) pos = insert (eq_fst op =) (v, rev pos)
wenzelm@24909
   199
  | args_of (TFree _) _ = I
wenzelm@24909
   200
and args_of_list (T :: Ts) i is = args_of T (i :: is) #> args_of_list Ts (i + 1) is
wenzelm@24909
   201
  | args_of_list [] _ _ = I;
wenzelm@24909
   202
wenzelm@19364
   203
fun subscript (Type (_, Ts)) (i :: is) = subscript (nth Ts i) is
wenzelm@19364
   204
  | subscript T [] = T
wenzelm@32784
   205
  | subscript _ _ = raise Subscript;
wenzelm@18060
   206
wenzelm@24909
   207
in
wenzelm@24909
   208
wenzelm@24909
   209
fun typargs_of T = map #2 (rev (args_of T [] []));
wenzelm@24909
   210
wenzelm@19364
   211
fun typargs consts (c, T) = map (subscript T) (type_arguments consts c);
wenzelm@18060
   212
wenzelm@24909
   213
end;
wenzelm@24909
   214
wenzelm@18163
   215
fun instance consts (c, Ts) =
wenzelm@18163
   216
  let
wenzelm@25041
   217
    val declT = type_scheme consts c;
wenzelm@18163
   218
    val vars = map Term.dest_TVar (typargs consts (c, declT));
wenzelm@24673
   219
    val inst = vars ~~ Ts handle UnequalLengths =>
wenzelm@24673
   220
      raise TYPE ("Consts.instance", Ts, [Const (c, dummyT)]);
wenzelm@31977
   221
  in declT |> Term_Subst.instantiateT inst end;
wenzelm@18163
   222
wenzelm@18060
   223
wenzelm@18060
   224
wenzelm@19364
   225
(** build consts **)
wenzelm@18060
   226
wenzelm@18935
   227
(* name space *)
wenzelm@18060
   228
wenzelm@24673
   229
fun hide fully c = map_consts (fn (decls, constraints, rev_abbrevs) =>
wenzelm@33095
   230
  (apfst (Name_Space.hide fully c) decls, constraints, rev_abbrevs));
wenzelm@18935
   231
wenzelm@18935
   232
wenzelm@18935
   233
(* declarations *)
wenzelm@18935
   234
wenzelm@33092
   235
fun declare authentic naming tags (b, declT) =
wenzelm@33092
   236
  map_consts (fn (decls, constraints, rev_abbrevs) =>
wenzelm@33092
   237
    let
wenzelm@33097
   238
      val decl = {T = declT, typargs = typargs_of declT, tags = tags, authentic = authentic};
wenzelm@33095
   239
      val (_, decls') = decls |> Name_Space.define true naming (b, (decl, NONE));
wenzelm@33092
   240
    in (decls', constraints, rev_abbrevs) end);
wenzelm@19364
   241
wenzelm@19364
   242
wenzelm@19364
   243
(* constraints *)
wenzelm@19364
   244
wenzelm@19364
   245
fun constrain (c, C) consts =
wenzelm@24673
   246
  consts |> map_consts (fn (decls, constraints, rev_abbrevs) =>
wenzelm@19364
   247
    (the_const consts c handle TYPE (msg, _, _) => error msg;
wenzelm@19364
   248
      (decls,
wenzelm@19364
   249
        constraints |> (case C of SOME T => Symtab.update (c, T) | NONE => Symtab.delete_safe c),
wenzelm@24673
   250
        rev_abbrevs)));
wenzelm@18060
   251
wenzelm@18935
   252
wenzelm@18935
   253
(* abbreviations *)
wenzelm@18935
   254
wenzelm@19027
   255
local
wenzelm@19027
   256
wenzelm@30568
   257
fun strip_abss (t as Abs (x, T, b)) =
wenzelm@30568
   258
      if Term.loose_bvar1 (b, 0) then strip_abss b |>> cons (x, T)
wenzelm@30568
   259
      else ([], t)
wenzelm@30568
   260
  | strip_abss t = ([], t);
wenzelm@19027
   261
wenzelm@21720
   262
fun rev_abbrev lhs rhs =
wenzelm@18060
   263
  let
wenzelm@30568
   264
    val (xs, body) = strip_abss (Envir.beta_eta_contract rhs);
wenzelm@30568
   265
    val vars = fold (fn (x, T) => cons (Var ((x, 0), T))) (Term.rename_wrt_term body xs) [];
wenzelm@30568
   266
  in (Term.subst_bounds (rev vars, body), Term.list_comb (lhs, vars)) end;
wenzelm@19027
   267
wenzelm@19027
   268
in
wenzelm@18965
   269
haftmann@28861
   270
fun abbreviate pp tsig naming mode tags (b, raw_rhs) consts =
wenzelm@18965
   271
  let
wenzelm@24673
   272
    val cert_term = certify pp tsig false consts;
wenzelm@24673
   273
    val expand_term = certify pp tsig true consts;
wenzelm@25116
   274
    val force_expand = mode = PrintMode.internal;
wenzelm@21720
   275
wenzelm@30286
   276
    val _ = Term.exists_subterm Term.is_Var raw_rhs andalso
wenzelm@33092
   277
      error ("Illegal schematic variables on rhs of abbreviation " ^ quote (Binding.str_of b));
wenzelm@30286
   278
wenzelm@19364
   279
    val rhs = raw_rhs
wenzelm@20548
   280
      |> Term.map_types (Type.cert_typ tsig)
wenzelm@30286
   281
      |> cert_term
wenzelm@30286
   282
      |> Term.close_schematic_term;
wenzelm@25404
   283
    val normal_rhs = expand_term rhs;
wenzelm@21794
   284
    val T = Term.fastype_of rhs;
wenzelm@33095
   285
    val lhs = Const (Name_Space.full_name naming b, T);
wenzelm@19364
   286
  in
wenzelm@24673
   287
    consts |> map_consts (fn (decls, constraints, rev_abbrevs) =>
wenzelm@19364
   288
      let
wenzelm@33097
   289
        val decl = {T = T, typargs = typargs_of T, tags = tags, authentic = true};
wenzelm@25404
   290
        val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand};
haftmann@28861
   291
        val (_, decls') = decls
wenzelm@33095
   292
          |> Name_Space.define true naming (b, (decl, SOME abbr));
wenzelm@19364
   293
        val rev_abbrevs' = rev_abbrevs
wenzelm@30566
   294
          |> insert_abbrevs mode (rev_abbrev lhs rhs);
wenzelm@24673
   295
      in (decls', constraints, rev_abbrevs') end)
wenzelm@21794
   296
    |> pair (lhs, rhs)
wenzelm@19364
   297
  end;
wenzelm@18935
   298
wenzelm@25048
   299
fun revert_abbrev mode c consts = consts |> map_consts (fn (decls, constraints, rev_abbrevs) =>
wenzelm@25048
   300
  let
wenzelm@25048
   301
    val (T, rhs) = the_abbreviation consts c;
wenzelm@25048
   302
    val rev_abbrevs' = rev_abbrevs
wenzelm@30566
   303
      |> insert_abbrevs mode (rev_abbrev (Const (c, T)) rhs);
wenzelm@25048
   304
  in (decls, constraints, rev_abbrevs') end);
wenzelm@25048
   305
wenzelm@19027
   306
end;
wenzelm@19027
   307
wenzelm@18060
   308
wenzelm@18060
   309
(* empty and merge *)
wenzelm@18060
   310
wenzelm@33096
   311
val empty = make_consts (Name_Space.empty_table "constant", Symtab.empty, Symtab.empty);
wenzelm@18060
   312
wenzelm@18060
   313
fun merge
wenzelm@30284
   314
   (Consts {decls = decls1, constraints = constraints1, rev_abbrevs = rev_abbrevs1},
wenzelm@30284
   315
    Consts {decls = decls2, constraints = constraints2, rev_abbrevs = rev_abbrevs2}) =
wenzelm@18060
   316
  let
wenzelm@33095
   317
    val decls' = Name_Space.merge_tables (decls1, decls2);
haftmann@25037
   318
    val constraints' = Symtab.join (K fst) (constraints1, constraints2);
wenzelm@30566
   319
    val rev_abbrevs' = Symtab.join (K Item_Net.merge) (rev_abbrevs1, rev_abbrevs2);
wenzelm@24673
   320
  in make_consts (decls', constraints', rev_abbrevs') end;
wenzelm@18060
   321
wenzelm@18060
   322
end;