src/Pure/defs.ML
author wenzelm
Sat, 21 Jan 2006 23:02:14 +0100
changeset 18728 6790126ab5f6
parent 17994 6a1a49cba5b3
child 19025 596fb1eb7856
permissions -rw-r--r--
simplified type attribute;
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
17712
46c2091e5187 make signature constraint actually work;
wenzelm
parents: 17711
diff changeset
    12
  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
    13
  val empty: T
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    14
  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
    15
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
    16
17711
c16cbe73798c activate signature constraints;
wenzelm
parents: 17707
diff changeset
    17
structure Defs: DEFS =
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    18
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
    19
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    20
(** datatype T **)
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    21
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    22
datatype T = Defs of
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    23
 {consts: typ Graph.T,                                 (*constant declarations and dependencies*)
17994
6a1a49cba5b3 removed inappropriate monomorphic test;
wenzelm
parents: 17803
diff changeset
    24
  specified: (string * typ) Inttab.table Symtab.table}; (*specification name and const type*)
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    25
17994
6a1a49cba5b3 removed inappropriate monomorphic test;
wenzelm
parents: 17803
diff changeset
    26
fun make_defs (consts, specified) = Defs {consts = consts, specified = specified};
6a1a49cba5b3 removed inappropriate monomorphic test;
wenzelm
parents: 17803
diff changeset
    27
fun map_defs f (Defs {consts, specified}) = make_defs (f (consts, specified));
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    28
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
(* specified consts *)
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    31
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    32
fun disjoint_types T U =
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    33
  (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
    34
    handle Type.TUNIFY => true;
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
    35
17803
e235a57651a1 more efficient check_specified, much less invocations;
wenzelm
parents: 17712
diff changeset
    36
fun check_specified c (i, (a, T)) = Inttab.forall (fn (j, (b, U)) =>
e235a57651a1 more efficient check_specified, much less invocations;
wenzelm
parents: 17712
diff changeset
    37
  i = j orelse not (Type.could_unify (T, U)) orelse disjoint_types T U orelse
e235a57651a1 more efficient check_specified, much less invocations;
wenzelm
parents: 17712
diff changeset
    38
    error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^
e235a57651a1 more efficient check_specified, much less invocations;
wenzelm
parents: 17712
diff changeset
    39
      " for constant " ^ quote c));
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    40
16982
4600e74aeb0d chain_history: turned into runtime flag;
wenzelm
parents: 16936
diff changeset
    41
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    42
(* define consts *)
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    43
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    44
fun err_cyclic cycles =
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    45
  error ("Cyclic dependency of constants:\n" ^
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    46
    cat_lines (map (space_implode " -> " o map quote o rev) cycles));
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    47
17994
6a1a49cba5b3 removed inappropriate monomorphic test;
wenzelm
parents: 17803
diff changeset
    48
fun define const_type name lhs rhs = map_defs (fn (consts, specified) =>
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    49
  let
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    50
    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
    51
    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
    52
      handle Graph.CYCLES cycles => err_cyclic cycles;
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    53
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    54
    val (c, T) = lhs;
17803
e235a57651a1 more efficient check_specified, much less invocations;
wenzelm
parents: 17712
diff changeset
    55
    val spec = (serial (), (name, T));
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    56
    val no_overloading = Type.raw_instance (const_type c, T);
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    57
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    58
    val consts' =
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    59
      consts |> declare lhs |> fold declare rhs
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    60
      |> K no_overloading ? add_deps (c, map #1 rhs);
17803
e235a57651a1 more efficient check_specified, much less invocations;
wenzelm
parents: 17712
diff changeset
    61
    val specified' = specified
e235a57651a1 more efficient check_specified, much less invocations;
wenzelm
parents: 17712
diff changeset
    62
      |> Symtab.default (c, Inttab.empty)
e235a57651a1 more efficient check_specified, much less invocations;
wenzelm
parents: 17712
diff changeset
    63
      |> Symtab.map_entry c (fn specs =>
e235a57651a1 more efficient check_specified, much less invocations;
wenzelm
parents: 17712
diff changeset
    64
        (check_specified c spec specs; Inttab.update spec specs));
17994
6a1a49cba5b3 removed inappropriate monomorphic test;
wenzelm
parents: 17803
diff changeset
    65
  in (consts', specified') end);
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    66
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    67
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    68
(* empty and merge *)
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    69
17994
6a1a49cba5b3 removed inappropriate monomorphic test;
wenzelm
parents: 17803
diff changeset
    70
val empty = make_defs (Graph.empty, Symtab.empty);
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    71
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    72
fun merge pp
17994
6a1a49cba5b3 removed inappropriate monomorphic test;
wenzelm
parents: 17803
diff changeset
    73
   (Defs {consts = consts1, specified = specified1},
6a1a49cba5b3 removed inappropriate monomorphic test;
wenzelm
parents: 17803
diff changeset
    74
    Defs {consts = consts2, specified = specified2}) =
17707
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    75
  let
bc0270e9d27f back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents: 17670
diff changeset
    76
    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
    77
      handle Graph.CYCLES cycles => err_cyclic cycles;
17803
e235a57651a1 more efficient check_specified, much less invocations;
wenzelm
parents: 17712
diff changeset
    78
    val specified' = (specified1, specified2) |> Symtab.join (fn c => fn (orig_specs1, specs2) =>
e235a57651a1 more efficient check_specified, much less invocations;
wenzelm
parents: 17712
diff changeset
    79
      SOME (Inttab.fold (fn spec2 => fn specs1 =>
e235a57651a1 more efficient check_specified, much less invocations;
wenzelm
parents: 17712
diff changeset
    80
        (check_specified c spec2 orig_specs1; Inttab.update spec2 specs1)) specs2 orig_specs1));
17994
6a1a49cba5b3 removed inappropriate monomorphic test;
wenzelm
parents: 17803
diff changeset
    81
  in make_defs (consts', specified') end;
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    82
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
    83
end;