src/Pure/defs.ML
author wenzelm
Tue, 19 Jul 2005 17:21:49 +0200
changeset 16877 e92cba1d4842
parent 16838 131ca99f6abf
child 16936 93772bd33871
permissions -rw-r--r--
tuned interfaces declare, define, finalize, merge: canonical argument order, produce errors; tuned checkT';
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
     1
(*  Title:      Pure/General/defs.ML
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$
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
     3
    Author:     Steven Obua, TU Muenchen
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
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
     5
    Checks if definitions preserve consistency of logic by enforcing
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
     6
    that there are no cyclic definitions. The algorithm is described in
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
     7
    "An Algorithm for Determining Definitional Cycles in Higher-Order Logic with Overloading",
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
     8
    Steven Obua, technical report, to be written :-)
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
     9
*)
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    10
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    11
signature DEFS =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    12
sig
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    13
  type graph
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    14
  val empty: graph
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    15
  val declare: string * typ -> graph -> graph
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    16
  val define: Pretty.pp -> string * typ -> string -> (string * typ) list -> graph -> graph
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    17
  val finalize: string * typ -> graph -> graph
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    18
  val merge: Pretty.pp -> graph -> graph -> graph
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
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    20
  val finals : graph -> (typ list) Symtab.table
16158
2c3565b74b7a Removed final_consts from theory data. Now const_deps deals with final
obua
parents: 16113
diff changeset
    21
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
    22
  (* If set to true then the exceptions CIRCULAR and INFINITE_CHAIN return the full
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    23
     chain of definitions that lead to the exception. In the beginning, chain_history
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
    24
     is initialized with the Isabelle environment variable DEFS_CHAIN_HISTORY. *)
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
    25
  val set_chain_history : bool -> unit
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
    26
  val chain_history : unit -> bool
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
    27
16743
21dbff595bf6 1) all theorems in Orderings can now be given as a parameter
obua
parents: 16384
diff changeset
    28
  datatype overloadingstate = Open | Closed | Final
16826
ed53f24149f6 - fixed bug concerning the renaming of axiom names
obua
parents: 16766
diff changeset
    29
16743
21dbff595bf6 1) all theorems in Orderings can now be given as a parameter
obua
parents: 16384
diff changeset
    30
  val overloading_info : graph -> string -> (typ * (string*typ) list * overloadingstate) option
16826
ed53f24149f6 - fixed bug concerning the renaming of axiom names
obua
parents: 16766
diff changeset
    31
  val fast_overloading_info : graph -> string -> (typ * int * overloadingstate) option
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
    32
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
    33
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    34
structure Defs :> DEFS = struct
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    35
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    36
type tyenv = Type.tyenv
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    37
type edgelabel = (int * typ * typ * (typ * string * string) list)
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    38
16743
21dbff595bf6 1) all theorems in Orderings can now be given as a parameter
obua
parents: 16384
diff changeset
    39
datatype overloadingstate = Open | Closed | Final
16361
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
    40
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
    41
datatype node = Node of
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
    42
         typ  (* most general type of constant *)
16361
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
    43
         * defnode Symtab.table
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    44
             (* a table of defnodes, each corresponding to 1 definition of the
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
    45
                constant for a particular type, indexed by axiom name *)
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    46
         * (unit Symtab.table) Symtab.table
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    47
             (* a table of all back referencing defnodes to this node,
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
    48
                indexed by node name of the defnodes *)
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    49
         * typ list (* a list of all finalized types *)
16743
21dbff595bf6 1) all theorems in Orderings can now be given as a parameter
obua
parents: 16384
diff changeset
    50
         * overloadingstate
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    51
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    52
     and defnode = Defnode of
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    53
         typ  (* type of the constant in this particular definition *)
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
    54
         * (edgelabel list) Symtab.table (* The edges, grouped by nodes. *)
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
    55
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    56
fun getnode graph noderef = the (Symtab.lookup (graph, noderef))
16361
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
    57
fun get_nodedefs (Node (_, defs, _, _, _)) = defs
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
    58
fun get_defnode (Node (_, defs, _, _, _)) defname = Symtab.lookup (defs, defname)
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    59
fun get_defnode' graph noderef defname =
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
    60
    Symtab.lookup (get_nodedefs (the (Symtab.lookup (graph, noderef))), defname)
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
    61
16361
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
    62
fun table_size table = Symtab.foldl (fn (x, _) => x+1) (0, table)
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    63
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
    64
datatype graphaction = Declare of string * typ
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    65
                     | Define of string * typ * string * string * (string * typ) list
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    66
                     | Finalize of string * typ
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
    67
16384
90c51c932154 internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents: 16361
diff changeset
    68
type graph = int * (string Symtab.table) * (graphaction list) * (node Symtab.table)
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    69
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    70
val CHAIN_HISTORY =
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
    71
    let
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    72
      fun f c = if Char.isSpace c then "" else String.str (Char.toUpper c)
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
    73
      val env = String.translate f (getenv "DEFS_CHAIN_HISTORY")
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
    74
    in
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
    75
      ref (env = "ON" orelse env = "TRUE")
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
    76
    end
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
    77
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
    78
fun set_chain_history b = CHAIN_HISTORY := b
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
    79
fun chain_history () = !CHAIN_HISTORY
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
    80
16384
90c51c932154 internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents: 16361
diff changeset
    81
val empty = (0, Symtab.empty, [], Symtab.empty)
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
    82
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
exception DEFS of string;
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    84
exception CIRCULAR of (typ * string * string) list;
16113
692fe6595755 Infinite chains in definitions are now detected, too.
obua
parents: 16108
diff changeset
    85
exception INFINITE_CHAIN of (typ * string * string) list;
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
    86
exception CLASH of string * string * string;
16158
2c3565b74b7a Removed final_consts from theory data. Now const_deps deals with final
obua
parents: 16113
diff changeset
    87
exception FINAL of string * typ;
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
    88
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    89
fun def_err s = raise (DEFS s)
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    90
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    91
fun no_forwards defs =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    92
    Symtab.foldl
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    93
    (fn (closed, (_, Defnode (_, edges))) =>
16361
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
    94
        if not closed then false else Symtab.is_empty edges)
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
    95
    (true, defs)
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
    96
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    97
fun checkT' (Type (a, Ts)) = Type (a, map checkT' Ts)
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    98
  | checkT' (TFree (a, _)) = TVar ((a, 0), [])        (* FIXME !? *)
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
    99
  | checkT' (TVar ((a, 0), _)) = TVar ((a, 0), [])
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   100
  | checkT' (T as TVar _) = raise TYPE ("Illegal schematic type variable encountered", [T], []);
16384
90c51c932154 internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents: 16361
diff changeset
   101
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   102
val checkT = Term.compress_type o checkT';
16384
90c51c932154 internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents: 16361
diff changeset
   103
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   104
fun rename ty1 ty2 = Logic.incr_tvar ((maxidx_of_typ ty1)+1) ty2;
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
   105
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   106
fun subst_incr_tvar inc t =
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   107
    if (inc > 0) then
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   108
      let
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   109
        val tv = typ_tvars t
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   110
        val t' = Logic.incr_tvar inc t
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   111
        fun update_subst (((n,i), _), s) =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   112
            Vartab.update (((n, i), ([], TVar ((n, i+inc), []))), s)
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   113
      in
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   114
        (t',List.foldl update_subst Vartab.empty tv)
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   115
      end
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
   116
    else
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   117
      (t, Vartab.empty)
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   118
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
   119
fun subst s ty = Envir.norm_type s ty
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   120
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
   121
fun subst_history s history = map (fn (ty, cn, dn) => (subst s ty, cn, dn)) history
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   122
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
   123
fun is_instance instance_ty general_ty =
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   124
    Type.typ_instance Type.empty_tsig (instance_ty, general_ty)
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   125
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
   126
fun is_instance_r instance_ty general_ty =
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   127
    is_instance instance_ty (rename instance_ty general_ty)
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   128
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   129
fun unify ty1 ty2 =
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
   130
    SOME (fst (Type.unify Type.empty_tsig (Vartab.empty, 0) (ty1, ty2)))
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   131
    handle Type.TUNIFY => NONE
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   132
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   133
(*
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   134
   Unifies ty1 and ty2, renaming ty1 and ty2 so that they have greater indices than max and
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   135
   so that they are different. All indices in ty1 and ty2 are supposed to be less than or
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   136
   equal to max.
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   137
   Returns SOME (max', s1, s2), so that s1(ty1) = s2(ty2) and max' is greater or equal than
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   138
   all indices in s1, s2, ty1, ty2.
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
   139
*)
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   140
fun unify_r max ty1 ty2 =
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
   141
    let
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   142
      val max = Int.max(max, 0)
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   143
      val max1 = max (* >= maxidx_of_typ ty1 *)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   144
      val max2 = max (* >= maxidx_of_typ ty2 *)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   145
      val max = Int.max(max, Int.max (max1, max2))
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   146
      val (ty1, s1) = subst_incr_tvar (max + 1) ty1
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   147
      val (ty2, s2) = subst_incr_tvar (max + max1 + 2) ty2
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   148
      val max = max + max1 + max2 + 2
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   149
      fun merge a b = Vartab.merge (fn _ => false) (a, b)
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
   150
    in
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   151
      case unify ty1 ty2 of
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   152
        NONE => NONE
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   153
      | SOME s => SOME (max, merge s1 s, merge s2 s)
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
   154
    end
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   155
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
   156
fun can_be_unified_r ty1 ty2 =
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   157
    let
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   158
      val ty2 = rename ty1 ty2
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
   159
    in
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   160
      case unify ty1 ty2 of
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   161
        NONE => false
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   162
      | _ => true
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
   163
    end
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   164
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
   165
fun can_be_unified ty1 ty2 =
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   166
    case unify ty1 ty2 of
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   167
      NONE => false
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   168
    | _ => true
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   169
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   170
fun normalize_edge_idx (edge as (maxidx, u1, v1, history)) =
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   171
    if maxidx <= 1000000 then edge else
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   172
    let
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   173
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   174
      fun idxlist idx extract_ty inject_ty (tab, max) ts =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   175
          foldr
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   176
            (fn (e, ((tab, max), ts)) =>
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   177
                let
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   178
                  val ((tab, max), ty) = idx (tab, max) (extract_ty e)
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   179
                  val e = inject_ty (ty, e)
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   180
                in
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   181
                  ((tab, max), e::ts)
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   182
                end)
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   183
            ((tab,max), []) ts
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   184
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   185
      fun idx (tab,max) (TVar ((a,i),_)) =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   186
          (case Inttab.lookup (tab, i) of
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   187
             SOME j => ((tab, max), TVar ((a,j),[]))
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   188
           | NONE => ((Inttab.update ((i, max), tab), max+1), TVar ((a,max),[])))
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   189
        | idx (tab,max) (Type (t, ts)) =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   190
          let
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   191
            val ((tab, max), ts) = idxlist idx I fst (tab, max) ts
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   192
          in
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   193
            ((tab,max), Type (t, ts))
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   194
          end
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   195
        | idx (tab, max) ty = ((tab, max), ty)
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   196
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   197
      val ((tab,max), u1) = idx (Inttab.empty, 0) u1
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   198
      val ((tab,max), v1) = idx (tab, max) v1
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   199
      val ((tab,max), history) =
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   200
          idxlist idx
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   201
            (fn (ty,_,_) => ty)
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   202
            (fn (ty, (_, s1, s2)) => (ty, s1, s2))
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   203
            (tab, max) history
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   204
    in
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   205
      (max, u1, v1, history)
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   206
    end
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   207
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
   208
fun compare_edges (e1 as (maxidx1, u1, v1, history1)) (e2 as (maxidx2, u2, v2, history2)) =
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   209
    let
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   210
      val t1 = u1 --> v1
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   211
      val t2 = Logic.incr_tvar (maxidx1+1) (u2 --> v2)
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
   212
    in
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   213
      if (is_instance t1 t2) then
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   214
        (if is_instance t2 t1 then
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   215
           SOME (int_ord (length history2, length history1))
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   216
         else
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   217
           SOME LESS)
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   218
      else if (is_instance t2 t1) then
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   219
        SOME GREATER
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   220
      else
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   221
        NONE
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
   222
    end
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   223
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   224
fun merge_edges_1 (x, []) = [x]
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   225
  | merge_edges_1 (x, (y::ys)) =
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
   226
    (case compare_edges x y of
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   227
       SOME LESS => (y::ys)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   228
     | SOME EQUAL => (y::ys)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   229
     | SOME GREATER => merge_edges_1 (x, ys)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   230
     | NONE => y::(merge_edges_1 (x, ys)))
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   231
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
   232
fun merge_edges xs ys = foldl merge_edges_1 xs ys
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   233
16384
90c51c932154 internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents: 16361
diff changeset
   234
fun declare' (g as (cost, axmap, actions, graph)) (cty as (name, ty)) =
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   235
    (cost, axmap, (Declare cty)::actions,
16361
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   236
     Symtab.update_new ((name, Node (ty, Symtab.empty, Symtab.empty, [], Open)), graph))
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   237
    handle Symtab.DUP _ =>
16361
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   238
           let
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   239
             val (Node (gty, _, _, _, _)) = the (Symtab.lookup(graph, name))
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   240
           in
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   241
             if is_instance_r ty gty andalso is_instance_r gty ty then
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   242
               g
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   243
             else
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   244
               def_err "constant is already declared with different type"
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   245
           end
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   246
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   247
fun declare'' g (name, ty) = declare' g (name, checkT ty)
16361
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   248
16384
90c51c932154 internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents: 16361
diff changeset
   249
val axcounter = ref (IntInf.fromInt 0)
90c51c932154 internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents: 16361
diff changeset
   250
fun newaxname axmap axname =
90c51c932154 internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents: 16361
diff changeset
   251
    let
90c51c932154 internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents: 16361
diff changeset
   252
      val c = !axcounter
90c51c932154 internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents: 16361
diff changeset
   253
      val _ = axcounter := c+1
90c51c932154 internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents: 16361
diff changeset
   254
      val axname' = axname^"_"^(IntInf.toString c)
90c51c932154 internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents: 16361
diff changeset
   255
    in
90c51c932154 internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents: 16361
diff changeset
   256
      (Symtab.update ((axname', axname), axmap), axname')
90c51c932154 internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents: 16361
diff changeset
   257
    end
90c51c932154 internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents: 16361
diff changeset
   258
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   259
fun translate_ex axmap x =
16384
90c51c932154 internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents: 16361
diff changeset
   260
    let
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   261
      fun translate (ty, nodename, axname) =
16384
90c51c932154 internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents: 16361
diff changeset
   262
          (ty, nodename, the (Symtab.lookup (axmap, axname)))
90c51c932154 internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents: 16361
diff changeset
   263
    in
90c51c932154 internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents: 16361
diff changeset
   264
      case x of
90c51c932154 internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents: 16361
diff changeset
   265
        INFINITE_CHAIN chain => raise (INFINITE_CHAIN (map translate chain))
90c51c932154 internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents: 16361
diff changeset
   266
      | CIRCULAR cycle => raise (CIRCULAR (map translate cycle))
90c51c932154 internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents: 16361
diff changeset
   267
      | _ => raise x
90c51c932154 internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents: 16361
diff changeset
   268
    end
90c51c932154 internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents: 16361
diff changeset
   269
16826
ed53f24149f6 - fixed bug concerning the renaming of axiom names
obua
parents: 16766
diff changeset
   270
fun define' (cost, axmap, actions, graph) (mainref, ty) axname orig_axname body =
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
   271
    let
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   272
      val mainnode  = (case Symtab.lookup (graph, mainref) of
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   273
                         NONE => def_err ("constant "^mainref^" is not declared")
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   274
                       | SOME n => n)
16361
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   275
      val (Node (gty, defs, backs, finals, _)) = mainnode
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   276
      val _ = (if is_instance_r ty gty then ()
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   277
               else def_err "type of constant does not match declared type")
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   278
      fun check_def (s, Defnode (ty', _)) =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   279
          (if can_be_unified_r ty ty' then
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   280
             raise (CLASH (mainref, axname, s))
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   281
           else if s = axname then
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   282
             def_err "name of axiom is already used for another definition of this constant"
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   283
           else false)
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   284
      val _ = Symtab.exists check_def defs
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   285
      fun check_final finalty =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   286
          (if can_be_unified_r finalty ty then
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   287
             raise (FINAL (mainref, finalty))
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   288
           else
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   289
             true)
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   290
      val _ = forall check_final finals
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   291
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   292
      (* now we know that the only thing that can prevent acceptance of the definition
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   293
         is a cyclic dependency *)
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   294
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   295
      fun insert_edges edges (nodename, links) =
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   296
          (if links = [] then
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   297
             edges
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   298
           else
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   299
             let
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   300
               val links = map normalize_edge_idx links
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   301
             in
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   302
               Symtab.update ((nodename,
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   303
                               case Symtab.lookup (edges, nodename) of
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   304
                                 NONE => links
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   305
                               | SOME links' => merge_edges links' links),
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   306
                              edges)
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   307
             end)
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   308
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   309
      fun make_edges ((bodyn, bodyty), edges) =
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   310
          let
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   311
            val bnode =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   312
                (case Symtab.lookup (graph, bodyn) of
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   313
                   NONE => def_err "body of constant definition references undeclared constant"
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   314
                 | SOME x => x)
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   315
            val (Node (general_btyp, bdefs, bbacks, bfinals, closed)) = bnode
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   316
          in
16361
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   317
            if closed = Final then edges else
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   318
            case unify_r 0 bodyty general_btyp of
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   319
              NONE => edges
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   320
            | SOME (maxidx, sigma1, sigma2) =>
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   321
              if exists (is_instance_r bodyty) bfinals then
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   322
                edges
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   323
              else
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   324
                let
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   325
                  fun insert_trans_edges ((step1, edges), (nodename, links)) =
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   326
                      let
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   327
                        val (maxidx1, alpha1, beta1, defname) = step1
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   328
                        fun connect (maxidx2, alpha2, beta2, history) =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   329
                            case unify_r (Int.max (maxidx1, maxidx2)) beta1 alpha2 of
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   330
                              NONE => NONE
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   331
                            | SOME (max, sleft, sright) =>
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   332
                              SOME (max, subst sleft alpha1, subst sright beta2,
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   333
                                    if !CHAIN_HISTORY then
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   334
                                      ((subst sleft beta1, bodyn, defname)::
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   335
                                       (subst_history sright history))
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   336
                                    else [])
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   337
                        val links' = List.mapPartial connect links
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   338
                      in
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   339
                        (step1, insert_edges edges (nodename, links'))
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   340
                      end
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   341
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   342
                  fun make_edges' ((swallowed, edges),
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   343
                                   (def_name, Defnode (def_ty, def_edges))) =
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   344
                      if swallowed then
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   345
                        (swallowed, edges)
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   346
                      else
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   347
                        (case unify_r 0 bodyty def_ty of
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   348
                           NONE => (swallowed, edges)
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   349
                         | SOME (maxidx, sigma1, sigma2) =>
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   350
                           (is_instance_r bodyty def_ty,
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   351
                            snd (Symtab.foldl insert_trans_edges
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   352
                              (((maxidx, subst sigma1 ty, subst sigma2 def_ty, def_name),
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   353
                                edges), def_edges))))
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   354
                  val (swallowed, edges) = Symtab.foldl make_edges' ((false, edges), bdefs)
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   355
                in
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   356
                  if swallowed then
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   357
                    edges
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   358
                  else
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   359
                    insert_edges edges
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   360
                    (bodyn, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])])
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   361
                end
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   362
          end
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   363
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   364
      val edges = foldl make_edges Symtab.empty body
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   365
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   366
      (* We also have to add the backreferences that this new defnode induces. *)
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   367
      fun install_backrefs (graph, (noderef, links)) =
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   368
          if links <> [] then
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   369
            let
16361
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   370
              val (Node (ty, defs, backs, finals, closed)) = getnode graph noderef
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   371
              val _ = if closed = Final then
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   372
                        sys_error ("install_backrefs: closed node cannot be updated")
16361
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   373
                      else ()
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   374
              val defnames =
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   375
                  (case Symtab.lookup (backs, mainref) of
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   376
                     NONE => Symtab.empty
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   377
                   | SOME s => s)
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   378
              val defnames' = Symtab.update_new ((axname, ()), defnames)
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   379
              val backs' = Symtab.update ((mainref,defnames'), backs)
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   380
            in
16361
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   381
              Symtab.update ((noderef, Node (ty, defs, backs', finals, closed)), graph)
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   382
            end
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   383
          else
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   384
            graph
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   385
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   386
      val graph = Symtab.foldl install_backrefs (graph, edges)
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   387
16361
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   388
      val (Node (_, _, backs, _, closed)) = getnode graph mainref
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   389
      val closed =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   390
          if closed = Final then sys_error "define: closed node"
16361
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   391
          else if closed = Open andalso is_instance_r gty ty then Closed else closed
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   392
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   393
      val thisDefnode = Defnode (ty, edges)
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   394
      val graph = Symtab.update ((mainref, Node (gty, Symtab.update_new
16361
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   395
        ((axname, thisDefnode), defs), backs, finals, closed)), graph)
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   396
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   397
      (* Now we have to check all backreferences to this node and inform them about
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   398
         the new defnode. In this section we also check for circularity. *)
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   399
      fun update_backrefs ((backs, graph), (noderef, defnames)) =
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   400
          let
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   401
            fun update_defs ((defnames, graph),(defname, _)) =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   402
                let
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   403
                  val (Node (nodety, nodedefs, nodebacks, nodefinals, closed)) =
16361
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   404
                      getnode graph noderef
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   405
                  val _ = if closed = Final then sys_error "update_defs: closed node" else ()
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   406
                  val (Defnode (def_ty, defnode_edges)) =
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   407
                      the (Symtab.lookup (nodedefs, defname))
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   408
                  val edges = the (Symtab.lookup (defnode_edges, mainref))
16361
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   409
                  val refclosed = ref false
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   410
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   411
                  (* the type of thisDefnode is ty *)
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   412
                  fun update (e as (max, alpha, beta, history), (changed, edges)) =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   413
                      case unify_r max beta ty of
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   414
                        NONE => (changed, e::edges)
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   415
                      | SOME (max', s_beta, s_ty) =>
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   416
                        let
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   417
                          val alpha' = subst s_beta alpha
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   418
                          val ty' = subst s_ty ty
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   419
                          val _ =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   420
                              if noderef = mainref andalso defname = axname then
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   421
                                (case unify alpha' ty' of
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   422
                                   NONE =>
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   423
                                   if (is_instance_r ty' alpha') then
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   424
                                     raise (INFINITE_CHAIN (
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   425
                                            (alpha', mainref, axname)::
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   426
                                            (subst_history s_beta history)@
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   427
                                            [(ty', mainref, axname)]))
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   428
                                   else ()
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   429
                                 | SOME s =>
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   430
                                   raise (CIRCULAR (
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   431
                                          (subst s alpha', mainref, axname)::
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   432
                                          (subst_history s (subst_history s_beta history))@
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   433
                                          [(subst s ty', mainref, axname)])))
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   434
                              else ()
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   435
                        in
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   436
                          if is_instance_r beta ty then
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   437
                            (true, edges)
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   438
                          else
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   439
                            (changed, e::edges)
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   440
                        end
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   441
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   442
                  val (changed, edges') = foldl update (false, []) edges
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   443
                  val defnames' = if edges' = [] then
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   444
                                    defnames
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   445
                                  else
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   446
                                    Symtab.update ((defname, ()), defnames)
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   447
                in
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   448
                  if changed then
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   449
                    let
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   450
                      val defnode_edges' =
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   451
                          if edges' = [] then
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   452
                            Symtab.delete mainref defnode_edges
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   453
                          else
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   454
                            Symtab.update ((mainref, edges'), defnode_edges)
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   455
                      val defnode' = Defnode (def_ty, defnode_edges')
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   456
                      val nodedefs' = Symtab.update ((defname, defnode'), nodedefs)
16361
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   457
                      val closed = if closed = Closed andalso Symtab.is_empty defnode_edges'
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   458
                                      andalso no_forwards nodedefs'
16361
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   459
                                   then Final else closed
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   460
                      val graph' =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   461
                          Symtab.update
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   462
                            ((noderef,
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   463
                              Node (nodety, nodedefs', nodebacks, nodefinals, closed)),graph)
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   464
                    in
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   465
                      (defnames', graph')
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   466
                    end
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   467
                  else
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   468
                    (defnames', graph)
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   469
                end
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   470
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   471
            val (defnames', graph') = Symtab.foldl update_defs
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   472
                                                   ((Symtab.empty, graph), defnames)
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   473
          in
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   474
            if Symtab.is_empty defnames' then
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   475
              (backs, graph')
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   476
            else
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   477
              let
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   478
                val backs' = Symtab.update_new ((noderef, defnames'), backs)
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   479
              in
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   480
                (backs', graph')
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   481
              end
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   482
          end
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   483
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   484
      val (backs, graph) = Symtab.foldl update_backrefs ((Symtab.empty, graph), backs)
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   485
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   486
      (* If a Circular exception is thrown then we never reach this point. *)
16361
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   487
      val (Node (gty, defs, _, finals, closed)) = getnode graph mainref
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   488
      val closed = if closed = Closed andalso no_forwards defs then Final else closed
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   489
      val graph = Symtab.update ((mainref, Node (gty, defs, backs, finals, closed)), graph)
16826
ed53f24149f6 - fixed bug concerning the renaming of axiom names
obua
parents: 16766
diff changeset
   490
      val actions' = (Define (mainref, ty, axname, orig_axname, body))::actions
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   491
    in
16384
90c51c932154 internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents: 16361
diff changeset
   492
      (cost+3, axmap, actions', graph)
90c51c932154 internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents: 16361
diff changeset
   493
    end handle ex => translate_ex axmap ex
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   494
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   495
fun define'' (g as (cost, axmap, actions, graph)) (mainref, ty) orig_axname body =
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   496
    let
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   497
      val ty = checkT ty
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   498
      fun checkbody (n, t) =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   499
          let
16361
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   500
            val (Node (_, _, _,_, closed)) = getnode graph n
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   501
          in
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   502
            case closed of
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   503
              Final => NONE
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   504
            | _ => SOME (n, checkT t)
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   505
          end
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   506
      val body = distinct (List.mapPartial checkbody body)
16826
ed53f24149f6 - fixed bug concerning the renaming of axiom names
obua
parents: 16766
diff changeset
   507
      val (axmap, axname) = newaxname axmap orig_axname
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   508
    in
16826
ed53f24149f6 - fixed bug concerning the renaming of axiom names
obua
parents: 16766
diff changeset
   509
      define' (cost, axmap, actions, graph) (mainref, ty) axname orig_axname body
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   510
    end
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   511
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   512
fun finalize' (cost, axmap, history, graph) (noderef, ty) =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   513
    case Symtab.lookup (graph, noderef) of
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   514
      NONE => def_err ("cannot finalize constant "^noderef^"; it is not declared")
16361
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   515
    | SOME (Node (nodety, defs, backs, finals, closed)) =>
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   516
      let
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   517
        val _ =
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   518
            if (not (is_instance_r ty nodety)) then
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   519
              def_err ("only type instances of the declared constant "^
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   520
                       noderef^" can be finalized")
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   521
            else ()
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   522
        val _ = Symtab.exists
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   523
                  (fn (def_name, Defnode (def_ty, _)) =>
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   524
                      if can_be_unified_r ty def_ty then
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   525
                        def_err ("cannot finalize constant "^noderef^
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   526
                                 "; clash with definition "^def_name)
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   527
                      else
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   528
                        false)
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   529
                  defs
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   530
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   531
        fun update_finals [] = SOME [ty]
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   532
          | update_finals (final_ty::finals) =
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   533
            (if is_instance_r ty final_ty then NONE
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   534
             else
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   535
               case update_finals finals of
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   536
                 NONE => NONE
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   537
               | (r as SOME finals) =>
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   538
                 if (is_instance_r final_ty ty) then
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   539
                   r
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   540
                 else
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   541
                   SOME (final_ty :: finals))
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   542
      in
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   543
        case update_finals finals of
16384
90c51c932154 internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents: 16361
diff changeset
   544
          NONE => (cost, axmap, history, graph)
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   545
        | SOME finals =>
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   546
          let
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   547
            val closed = if closed = Open andalso is_instance_r nodety ty then
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   548
                           Closed else
16361
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   549
                         closed
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   550
            val graph = Symtab.update ((noderef, Node(nodety, defs, backs, finals, closed)),
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   551
                                       graph)
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   552
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   553
            fun update_backref ((graph, backs), (backrefname, backdefnames)) =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   554
                let
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   555
                  fun update_backdef ((graph, defnames), (backdefname, _)) =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   556
                      let
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   557
                        val (backnode as Node (backty, backdefs, backbacks,
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   558
                                               backfinals, backclosed)) =
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   559
                            getnode graph backrefname
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   560
                        val (Defnode (def_ty, all_edges)) =
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   561
                            the (get_defnode backnode backdefname)
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   562
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   563
                        val (defnames', all_edges') =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   564
                            case Symtab.lookup (all_edges, noderef) of
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   565
                              NONE => sys_error "finalize: corrupt backref"
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   566
                            | SOME edges =>
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   567
                              let
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   568
                                val edges' = List.filter (fn (_, _, beta, _) =>
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   569
                                                             not (is_instance_r beta ty)) edges
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   570
                              in
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   571
                                if edges' = [] then
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   572
                                  (defnames, Symtab.delete noderef all_edges)
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   573
                                else
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   574
                                  (Symtab.update ((backdefname, ()), defnames),
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   575
                                   Symtab.update ((noderef, edges'), all_edges))
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   576
                              end
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   577
                        val defnode' = Defnode (def_ty, all_edges')
16361
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   578
                        val backdefs' = Symtab.update ((backdefname, defnode'), backdefs)
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   579
                        val backclosed' = if backclosed = Closed andalso
16361
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   580
                                             Symtab.is_empty all_edges'
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   581
                                             andalso no_forwards backdefs'
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   582
                                          then Final else backclosed
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   583
                        val backnode' =
16361
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   584
                            Node (backty, backdefs', backbacks, backfinals, backclosed')
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   585
                      in
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   586
                        (Symtab.update ((backrefname, backnode'), graph), defnames')
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   587
                      end
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   588
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   589
                  val (graph', defnames') =
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   590
                      Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames)
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   591
                in
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   592
                  (graph', if Symtab.is_empty defnames' then backs
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   593
                           else Symtab.update ((backrefname, defnames'), backs))
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   594
                end
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   595
            val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs)
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   596
            val Node ( _, defs, _, _, closed) = getnode graph' noderef
16361
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   597
            val closed = if closed = Closed andalso no_forwards defs then Final else closed
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   598
            val graph' = Symtab.update ((noderef, Node (nodety, defs, backs',
16361
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   599
                                                        finals, closed)), graph')
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   600
            val history' = (Finalize (noderef, ty)) :: history
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   601
          in
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   602
            (cost+1, axmap, history', graph')
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   603
          end
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   604
      end
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   605
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   606
fun finalize'' g (noderef, ty) = finalize' g (noderef, checkT ty)
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   607
16826
ed53f24149f6 - fixed bug concerning the renaming of axiom names
obua
parents: 16766
diff changeset
   608
fun update_axname ax orig_ax (cost, axmap, history, graph) =
ed53f24149f6 - fixed bug concerning the renaming of axiom names
obua
parents: 16766
diff changeset
   609
  (cost, Symtab.update ((ax, orig_ax), axmap), history, graph)
ed53f24149f6 - fixed bug concerning the renaming of axiom names
obua
parents: 16766
diff changeset
   610
16361
cb31cb768a6c further optimizations of cycle test
obua
parents: 16308
diff changeset
   611
fun merge' (Declare cty, g) = declare' g cty
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   612
  | merge' (Define (name, ty, axname, orig_axname, body), g as (cost, axmap, history, graph)) =
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   613
    (case Symtab.lookup (graph, name) of
16826
ed53f24149f6 - fixed bug concerning the renaming of axiom names
obua
parents: 16766
diff changeset
   614
       NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   615
     | SOME (Node (_, defs, _, _, _)) =>
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   616
       (case Symtab.lookup (defs, axname) of
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   617
          NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   618
        | SOME _ => g))
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   619
  | merge' (Finalize finals, g) = finalize' g finals
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   620
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   621
fun merge'' (g1 as (cost1, _, actions1, _)) (g2 as (cost2, _, actions2, _)) =
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   622
    if cost1 < cost2 then
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   623
      foldr merge' g2 actions1
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   624
    else
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   625
      foldr merge' g1 actions2
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   626
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   627
fun finals (_, _, history, graph) =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   628
    Symtab.foldl
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   629
      (fn (finals, (name, Node(_, _, _, ftys, _))) =>
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   630
          Symtab.update_new ((name, ftys), finals))
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   631
      (Symtab.empty, graph)
16158
2c3565b74b7a Removed final_consts from theory data. Now const_deps deals with final
obua
parents: 16113
diff changeset
   632
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   633
fun overloading_info (_, axmap, _, graph) c =
16743
21dbff595bf6 1) all theorems in Orderings can now be given as a parameter
obua
parents: 16384
diff changeset
   634
    let
21dbff595bf6 1) all theorems in Orderings can now be given as a parameter
obua
parents: 16384
diff changeset
   635
      fun translate (ax, Defnode (ty, _)) = (the (Symtab.lookup (axmap, ax)), ty)
21dbff595bf6 1) all theorems in Orderings can now be given as a parameter
obua
parents: 16384
diff changeset
   636
    in
21dbff595bf6 1) all theorems in Orderings can now be given as a parameter
obua
parents: 16384
diff changeset
   637
      case Symtab.lookup (graph, c) of
21dbff595bf6 1) all theorems in Orderings can now be given as a parameter
obua
parents: 16384
diff changeset
   638
        NONE => NONE
21dbff595bf6 1) all theorems in Orderings can now be given as a parameter
obua
parents: 16384
diff changeset
   639
      | SOME (Node (ty, defnodes, _, _, state)) =>
21dbff595bf6 1) all theorems in Orderings can now be given as a parameter
obua
parents: 16384
diff changeset
   640
        SOME (ty, map translate (Symtab.dest defnodes), state)
21dbff595bf6 1) all theorems in Orderings can now be given as a parameter
obua
parents: 16384
diff changeset
   641
    end
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   642
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   643
fun fast_overloading_info (_, _, _, graph) c =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   644
    let
16826
ed53f24149f6 - fixed bug concerning the renaming of axiom names
obua
parents: 16766
diff changeset
   645
      fun count (c, _) = c+1
16766
ea667a5426fe Improved implementation of Defs.is_overloaded.
obua
parents: 16743
diff changeset
   646
    in
ea667a5426fe Improved implementation of Defs.is_overloaded.
obua
parents: 16743
diff changeset
   647
      case Symtab.lookup (graph, c) of
16826
ed53f24149f6 - fixed bug concerning the renaming of axiom names
obua
parents: 16766
diff changeset
   648
        NONE => NONE
ed53f24149f6 - fixed bug concerning the renaming of axiom names
obua
parents: 16766
diff changeset
   649
      | SOME (Node (ty, defnodes, _, _, state)) =>
ed53f24149f6 - fixed bug concerning the renaming of axiom names
obua
parents: 16766
diff changeset
   650
        SOME (ty, Symtab.foldl count (0, defnodes), state)
16766
ea667a5426fe Improved implementation of Defs.is_overloaded.
obua
parents: 16743
diff changeset
   651
    end
16743
21dbff595bf6 1) all theorems in Orderings can now be given as a parameter
obua
parents: 16384
diff changeset
   652
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   653
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   654
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   655
(** diagnostics **)
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   656
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   657
fun pretty_const pp (c, T) =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   658
 [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   659
  Pretty.quote (Pretty.typ pp (Type.freeze_type T))];    (* FIXME zero indexes!? *)
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   660
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   661
fun pretty_path pp path = fold_rev (fn (T, c, def) =>
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   662
  fn [] => [Pretty.block (pretty_const pp (c, T))]
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   663
   | prts => Pretty.block (pretty_const pp (c, T) @
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   664
      [Pretty.brk 1, Pretty.str ("depends via " ^ quote def ^ " on")]) :: prts) path [];
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   665
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   666
fun chain_history_msg s =    (* FIXME huh!? *)
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   667
  if chain_history () then s ^ ": "
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   668
  else s ^ " (set DEFS_CHAIN_HISTORY=ON for full history): ";
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   669
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   670
fun defs_circular pp path =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   671
  Pretty.str (chain_history_msg "Cyclic dependency of definitions") :: pretty_path pp path
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   672
  |> Pretty.chunks |> Pretty.string_of;
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   673
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   674
fun defs_infinite_chain pp path =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   675
  Pretty.str (chain_history_msg "Infinite chain of definitions") :: pretty_path pp path
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   676
  |> Pretty.chunks |> Pretty.string_of;
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   677
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   678
fun defs_clash def1 def2 = "Type clash in definitions " ^ quote def1 ^ " and " ^ quote def2;
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   679
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   680
fun defs_final pp const =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   681
  (Pretty.str "Attempt to define final constant" :: Pretty.brk 1 :: pretty_const pp const)
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   682
  |> Pretty.block |> Pretty.string_of;
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   683
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   684
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   685
(* external interfaces *)
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   686
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   687
fun declare const defs =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   688
  if_none (try (declare'' defs) const) defs;
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   689
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   690
fun define pp const name rhs defs =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   691
  define'' defs const name rhs
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   692
    handle DEFS msg => sys_error msg
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   693
      | CIRCULAR path => error (defs_circular pp path)
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   694
      | INFINITE_CHAIN path => error (defs_infinite_chain pp path)
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   695
      | CLASH (_, def1, def2) => error (defs_clash def1 def2)
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   696
      | FINAL const => error (defs_final pp const);
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   697
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   698
fun finalize const defs =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   699
  finalize'' defs const handle DEFS msg => sys_error msg;
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   700
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   701
fun merge pp defs1 defs2 =
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   702
  merge'' defs1 defs2
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   703
    handle CIRCULAR namess => error (defs_circular pp namess)
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   704
      | INFINITE_CHAIN namess => error (defs_infinite_chain pp namess);
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   705
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
   706
end;
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   707
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   708
(*
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
   709
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   710
fun tvar name = TVar ((name, 0), [])
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
   711
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   712
val bool = Type ("bool", [])
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   713
val int = Type ("int", [])
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   714
val lam = Type("lam", [])
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
   715
val alpha = tvar "'a"
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   716
val beta = tvar "'b"
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   717
val gamma = tvar "'c"
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   718
fun pair a b = Type ("pair", [a,b])
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   719
fun prm a = Type ("prm", [a])
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   720
val name = Type ("name", [])
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
   721
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   722
val _ = print "make empty"
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   723
val g = Defs.empty
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
   724
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   725
val _ = print "declare perm"
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   726
val g = Defs.declare g ("perm", prm alpha --> beta --> beta)
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   727
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   728
val _ = print "declare permF"
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   729
val g = Defs.declare g ("permF", prm alpha --> lam --> lam)
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   730
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   731
val _ = print "define perm (1)"
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   732
val g = Defs.define g ("perm", prm alpha --> (beta --> gamma) --> (beta --> gamma)) "perm_fun"
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   733
        [("perm", prm alpha --> gamma --> gamma), ("perm", prm alpha --> beta --> beta)]
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
   734
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   735
val _ = print "define permF (1)"
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   736
val g = Defs.define g ("permF", prm alpha --> lam --> lam) "permF_app"
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   737
        ([("perm", prm alpha --> lam --> lam),
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   738
         ("perm", prm alpha --> lam --> lam),
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   739
         ("perm", prm alpha --> lam --> lam),
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   740
         ("perm", prm alpha --> name --> name)])
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
   741
16308
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   742
val _ = print "define perm (2)"
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   743
val g = Defs.define g ("perm", prm alpha --> lam --> lam) "perm_lam"
636a1a84977a 1) Fixed bug in Defs.merge_edges_1.
obua
parents: 16198
diff changeset
   744
        [("permF", (prm alpha --> lam --> lam))]
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
   745
16877
e92cba1d4842 tuned interfaces declare, define, finalize, merge:
wenzelm
parents: 16838
diff changeset
   746
*)