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