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