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