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