src/Pure/defs.ML
author wenzelm
Thu Jul 14 19:28:20 2005 +0200 (2005-07-14)
changeset 16838 131ca99f6abf
parent 16826 ed53f24149f6
child 16877 e92cba1d4842
permissions -rw-r--r--
use existing Inttab;
     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 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 orig_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, orig_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) orig_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 orig_axname
   538     in
   539       define' (cost, axmap, actions, graph) (mainref, ty) axname orig_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 update_axname ax orig_ax (cost, axmap, history, graph) =
   639   (cost, Symtab.update ((ax, orig_ax), axmap), history, graph)
   640 
   641 fun merge' (Declare cty, g) = declare' g cty
   642   | merge' (Define (name, ty, axname, orig_axname, body), g as (cost, axmap, history, graph)) = 
   643     (case Symtab.lookup (graph, name) of
   644        NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body
   645      | SOME (Node (_, defs, _, _, _)) => 
   646        (case Symtab.lookup (defs, axname) of
   647 	  NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body
   648 	| SOME _ => g))
   649   | merge' (Finalize finals, g) = finalize' g finals 
   650                        
   651 fun merge (g1 as (cost1, _, actions1, _)) (g2 as (cost2, _, actions2, _)) =
   652     if cost1 < cost2 then
   653       foldr merge' g2 actions1
   654     else
   655       foldr merge' g1 actions2
   656                            
   657 fun finals (_, _, history, graph) = 
   658     Symtab.foldl 
   659       (fn (finals, (name, Node(_, _, _, ftys, _))) => 
   660           Symtab.update_new ((name, ftys), finals)) 
   661       (Symtab.empty, graph)
   662 
   663 fun overloading_info (_, axmap, _, graph) c = 
   664     let
   665       fun translate (ax, Defnode (ty, _)) = (the (Symtab.lookup (axmap, ax)), ty)
   666     in
   667       case Symtab.lookup (graph, c) of
   668         NONE => NONE
   669       | SOME (Node (ty, defnodes, _, _, state)) =>
   670         SOME (ty, map translate (Symtab.dest defnodes), state)
   671     end
   672       
   673 fun fast_overloading_info (_, _, _, graph) c = 
   674     let 
   675       fun count (c, _) = c+1
   676     in
   677       case Symtab.lookup (graph, c) of
   678         NONE => NONE
   679       | SOME (Node (ty, defnodes, _, _, state)) =>
   680         SOME (ty, Symtab.foldl count (0, defnodes), state)
   681     end
   682 
   683 end;
   684 		
   685 (*
   686 
   687 fun tvar name = TVar ((name, 0), [])
   688 
   689 val bool = Type ("bool", [])
   690 val int = Type ("int", [])
   691 val lam = Type("lam", [])
   692 val alpha = tvar "'a"
   693 val beta = tvar "'b"
   694 val gamma = tvar "'c"
   695 fun pair a b = Type ("pair", [a,b])
   696 fun prm a = Type ("prm", [a])
   697 val name = Type ("name", [])
   698 
   699 val _ = print "make empty"
   700 val g = Defs.empty 
   701 
   702 val _ = print "declare perm"
   703 val g = Defs.declare g ("perm", prm alpha --> beta --> beta)
   704 
   705 val _ = print "declare permF"
   706 val g = Defs.declare g ("permF", prm alpha --> lam --> lam)
   707 
   708 val _ = print "define perm (1)"
   709 val g = Defs.define g ("perm", prm alpha --> (beta --> gamma) --> (beta --> gamma)) "perm_fun" 
   710         [("perm", prm alpha --> gamma --> gamma), ("perm", prm alpha --> beta --> beta)]
   711 
   712 val _ = print "define permF (1)"
   713 val g = Defs.define g ("permF", prm alpha --> lam --> lam) "permF_app"
   714         ([("perm", prm alpha --> lam --> lam),
   715          ("perm", prm alpha --> lam --> lam),
   716          ("perm", prm alpha --> lam --> lam),
   717          ("perm", prm alpha --> name --> name)])
   718 
   719 val _ = print "define perm (2)"
   720 val g = Defs.define g ("perm", prm alpha --> lam --> lam) "perm_lam"
   721         [("permF", (prm alpha --> lam --> lam))]
   722 
   723 *)