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