src/Pure/defs.ML
author wenzelm
Fri, 07 Oct 2005 23:29:00 +0200
changeset 17789 ccba4e900023
parent 17712 46c2091e5187
child 17803 e235a57651a1
permissions -rw-r--r--
removed obsolete comment;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
     1
(*  Title:      Pure/defs.ML
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
     2
    ID:         $Id$
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
     3
    Author:     Makarius
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
     4
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
     5
Global well-formedness checks for constant definitions.  Dependencies
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
     6
are only tracked for non-overloaded definitions!
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
     7
*)
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
     8
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
     9
signature DEFS =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    10
sig
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    11
  type T
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    12
  val monomorphic: T -> string -> bool
17712
46c2091e5187 make signature constraint actually work;
wenzelm
parents: 17711
diff changeset
    13
  val define: (string -> typ) -> string -> string * typ -> (string * typ) list -> T -> T
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    14
  val empty: T
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    15
  val merge: Pretty.pp -> T * T -> T
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    16
end
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    17
17711
c16cbe73798c activate signature constraints;
wenzelm
parents: 17707
diff changeset
    18
structure Defs: DEFS =
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    19
struct
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    20
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    21
(** datatype T **)
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    22
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    23
datatype T = Defs of
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    24
 {consts: typ Graph.T,                                 (*constant declarations and dependencies*)
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    25
  specified: (string * typ) Inttab.table Symtab.table, (*specification name and const type*)
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    26
  monomorphic: unit Symtab.table};                     (*constants having monomorphic specs*)
16384
90c51c932154 internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents: 16361
diff changeset
    27
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    28
fun rep_defs (Defs args) = args;
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    29
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    30
fun make_defs (consts, specified, monomorphic) =
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    31
  Defs {consts = consts, specified = specified, monomorphic = monomorphic};
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    32
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    33
fun map_defs f (Defs {consts, specified, monomorphic}) =
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    34
  make_defs (f (consts, specified, monomorphic));
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    35
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    36
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    37
(* specified consts *)
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    38
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    39
fun disjoint_types T U =
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    40
  (Type.raw_unify (T, Logic.incr_tvar (maxidx_of_typ T + 1) U) Vartab.empty; false)
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    41
    handle Type.TUNIFY => true;
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
    42
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    43
fun check_specified c specified =
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    44
  specified |> Inttab.forall (fn (i, (a, T)) =>
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    45
    specified |> Inttab.forall (fn (j, (b, U)) =>
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    46
      i = j orelse disjoint_types T U orelse
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    47
        error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    48
          " for constant " ^ quote c)));
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    49
16982
4600e74aeb0d chain_history: turned into runtime flag;
wenzelm
parents: 16936
diff changeset
    50
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    51
(* monomorphic constants *)
16982
4600e74aeb0d chain_history: turned into runtime flag;
wenzelm
parents: 16936
diff changeset
    52
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    53
val monomorphic = Symtab.defined o #monomorphic o rep_defs;
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    54
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    55
fun update_monomorphic specified c =
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    56
  let
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    57
    val specs = the_default Inttab.empty (Symtab.lookup specified c);
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    58
    fun is_monoT (Type (_, Ts)) = forall is_monoT Ts
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    59
      | is_monoT _ = false;
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    60
    val is_mono =
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    61
      Inttab.is_empty specs orelse
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    62
        Inttab.min_key specs = Inttab.max_key specs andalso
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    63
        is_monoT (snd (the (Inttab.lookup specs (the (Inttab.min_key specs)))));
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    64
  in if is_mono then Symtab.update (c, ()) else Symtab.remove (K true) (c, ()) end;
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    65
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    66
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    67
(* define consts *)
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    68
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    69
fun err_cyclic cycles =
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    70
  error ("Cyclic dependency of constants:\n" ^
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    71
    cat_lines (map (space_implode " -> " o map quote o rev) cycles));
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    72
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    73
fun define const_type name lhs rhs = map_defs (fn (consts, specified, monomorphic) =>
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    74
  let
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    75
    fun declare (a, _) = Graph.default_node (a, const_type a);
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    76
    fun add_deps (a, bs) G = Graph.add_deps_acyclic (a, bs) G
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    77
      handle Graph.CYCLES cycles => err_cyclic cycles;
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    78
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    79
    val (c, T) = lhs;
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    80
    val no_overloading = Type.raw_instance (const_type c, T);
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    81
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    82
    val consts' =
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    83
      consts |> declare lhs |> fold declare rhs
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    84
      |> K no_overloading ? add_deps (c, map #1 rhs);
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    85
    val specified' =
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    86
      specified |> Symtab.default (c, Inttab.empty)
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    87
      |> Symtab.map_entry c (Inttab.update (serial (), (name, T)) #> tap (check_specified c));
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    88
    val monomorphic' = monomorphic |> update_monomorphic specified' c;
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    89
  in (consts', specified', monomorphic') end);
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    90
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    91
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    92
(* empty and merge *)
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    93
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    94
val empty = make_defs (Graph.empty, Symtab.empty, Symtab.empty);
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    95
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    96
fun merge pp
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    97
   (Defs {consts = consts1, specified = specified1, monomorphic},
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    98
    Defs {consts = consts2, specified = specified2, ...}) =
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    99
  let
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
   100
    val consts' = (consts1, consts2) |> Graph.merge_acyclic (K true)
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
   101
      handle Graph.CYCLES cycles => err_cyclic cycles;
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
   102
    val specified' = (specified1, specified2)
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
   103
      |> Symtab.join (fn c => Inttab.merge (K true) #> tap (check_specified c) #> SOME);
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
   104
    val monomorphic' = monomorphic
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
   105
      |> Symtab.fold (update_monomorphic specified' o #1) specified';
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
   106
  in make_defs (consts', specified', monomorphic') end;
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   107
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   108
end;