src/Pure/defs.ML
author obua
Fri Jun 03 01:08:07 2005 +0200 (2005-06-03)
changeset 16198 cfd070a2cc4d
parent 16177 1af9f5c69745
child 16308 636a1a84977a
permissions -rw-r--r--
Integrates cycle detection in definitions with finalconsts
     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 that there are no cyclic definitions.
     6     The algorithm is described in 
     7     "Cycle-free Overloading in Isabelle", Steven Obua, technical report, to be written :-)
     8 *)
     9 
    10 signature DEFS = sig
    11     
    12   type graph
    13        
    14   exception DEFS of string
    15   exception CIRCULAR of (typ * string * string) list
    16   exception INFINITE_CHAIN of (typ * string * string) list 
    17   exception FINAL of string * typ
    18   exception CLASH of string * string * string
    19                      
    20   val empty : graph
    21   val declare : graph -> string * typ -> graph  (* exception DEFS *)
    22   val define : graph -> string * typ -> string -> (string * typ) list -> graph 
    23     (* exception DEFS, CIRCULAR, INFINITE_CHAIN, CLASH, FINAL *)
    24                                                                          
    25   val finalize : graph -> string * typ -> graph (* exception DEFS *)
    26 
    27   val finals : graph -> (typ list) Symtab.table
    28 
    29   (* the first argument should be the smaller graph *)
    30   val merge : graph -> graph -> graph (* exception CIRCULAR, INFINITE_CHAIN, CLASH *)
    31 
    32 end
    33 
    34 structure Defs :> DEFS = struct
    35 
    36 type tyenv = Type.tyenv
    37 type edgelabel = (int * typ * typ * (typ * string * string) list)
    38 type noderef = string
    39 
    40 datatype node = Node of
    41          string  (* name of constant *)
    42          * typ  (* most general type of constant *)
    43          * defnode Symtab.table  (* a table of defnodes, each corresponding to 1 definition of the 
    44              constant for a particular type, indexed by axiom name *)
    45          * backref Symtab.table (* a table of all back references to this node, indexed by node name *)
    46          * typ list (* a list of all finalized types *)
    47      
    48      and defnode = Defnode of
    49          typ  (* type of the constant in this particular definition *)
    50          * ((noderef * (string option * edgelabel list) list) Symtab.table) (* The edges, grouped by nodes. *)
    51 
    52 and backref = Backref of
    53     noderef  (* the name of the node that has defnodes which reference a certain node A *)
    54     * (unit Symtab.table) (* the names of the defnodes that DIRECTLY reference A. *)
    55 
    56 fun getnode graph noderef = the (Symtab.lookup (graph, noderef))
    57 fun get_nodename (Node (n, _, _ ,_, _)) = n
    58 fun get_nodedefs (Node (_, _, defs, _, _)) = defs
    59 fun get_defnode (Node (_, _, defs, _, _)) defname = Symtab.lookup (defs, defname)
    60 fun get_defnode' graph noderef defname = Symtab.lookup (get_nodedefs (the (Symtab.lookup (graph, noderef))), defname)
    61 fun get_nodename (Node (n, _, _ , _, _)) = n
    62 
    63 datatype graphaction = Declare of string * typ 
    64 		     | Define of string * typ * string * (string * typ) list
    65 		     | Finalize of string * typ
    66 
    67 type graph = (graphaction list) * (node Symtab.table)
    68              
    69 val empty = ([], Symtab.empty)
    70 
    71 exception DEFS of string;
    72 exception CIRCULAR of (typ * string * string) list;
    73 exception INFINITE_CHAIN of (typ * string * string) list;
    74 exception CLASH of string * string * string;
    75 exception FINAL of string * typ;
    76 
    77 fun def_err s = raise (DEFS s)
    78 
    79 fun declare (actions, g) (cty as (name, ty)) =
    80     ((Declare cty)::actions, 
    81      Symtab.update_new ((name, Node (name, Type.varifyT(Type.strip_sorts ty), Symtab.empty, Symtab.empty, [])), g))
    82     handle Symtab.DUP _ => def_err "constant is already declared"
    83 
    84 fun rename ty1 ty2 = incr_tvar ((maxidx_of_typ ty1)+1) ty2;  
    85 
    86 fun subst_incr_tvar inc t =
    87     if (inc > 0) then 
    88       let
    89 	val tv = typ_tvars t
    90 	val t' = incr_tvar inc t
    91 	fun update_subst (((n,i), _), s) =
    92 	    Vartab.update (((n, i), ([], TVar ((n, i+inc), []))), s)
    93       in
    94 	(t',List.foldl update_subst Vartab.empty tv)
    95       end	
    96     else
    97       (t, Vartab.empty)
    98 
    99 (* Rename tys2 so that tys2 and tys1 do not have any variables in common any more.
   100    As a result, return the renamed tys2' and the substitution that takes tys2 to tys2'. *)
   101 fun subst_rename max1 ty2 =
   102     let
   103       val max2 = (maxidx_of_typ ty2)
   104       val (ty2', s) = subst_incr_tvar (max1 + 1) ty2                
   105     in
   106       (ty2', s, max1 + max2 + 1)
   107     end	       
   108     
   109 fun subst s ty = Envir.norm_type s ty
   110                  
   111 fun subst_history s history = map (fn (ty, cn, dn) => (subst s ty, cn, dn)) history
   112                               
   113 fun is_instance instance_ty general_ty =
   114     Type.typ_instance Type.empty_tsig (instance_ty, general_ty)
   115     
   116 fun is_instance_r instance_ty general_ty =
   117     is_instance instance_ty (rename instance_ty general_ty)
   118     
   119 fun unify ty1 ty2 = 
   120     SOME (fst (Type.unify Type.empty_tsig (Vartab.empty, 0) (ty1, ty2)))
   121     handle Type.TUNIFY => NONE
   122                             
   123 (* 
   124    Unifies ty1 and ty2, renaming ty1 and ty2 so that they have greater indices than max and so that they
   125    are different. All indices in ty1 and ty2 are supposed to be less than or equal to max.
   126    Returns SOME (max', s1, s2), so that s1(ty1) = s2(ty2) and max' is greater or equal than all 
   127    indices in s1, s2, ty1, ty2.
   128 *)
   129 fun unify_r max ty1 ty2 = 
   130     let
   131       val max =  Int.max(max, 0)
   132       val max1 = max (* >= maxidx_of_typ ty1 *)
   133       val max2 = max (* >= maxidx_of_typ ty2 *)
   134       val max = Int.max(max, Int.max (max1, max2))
   135       val (ty1, s1) = subst_incr_tvar (max+1) ty1
   136       val (ty2, s2) = subst_incr_tvar (max+max1+2) ty2
   137       val max = max+max1+max2+2	
   138       fun merge a b = Vartab.merge (fn _ => false) (a, b)
   139     in
   140       case unify ty1 ty2 of
   141 	NONE => NONE
   142       | SOME s => SOME (max, merge s1 s, merge s2 s)
   143     end
   144     
   145 fun can_be_unified_r ty1 ty2 =
   146     let
   147       val ty2 = rename ty1 ty2
   148     in
   149       case unify ty1 ty2 of
   150 	NONE => false
   151       | _ => true
   152     end
   153     
   154 fun can_be_unified ty1 ty2 =
   155     case unify ty1 ty2 of
   156       NONE => false
   157     | _ => true
   158            
   159 fun checkT (Type (a, Ts)) = Type (a, map checkT Ts)
   160   | checkT (TVar ((a, 0), _)) = TVar ((a, 0), [])
   161   | checkT (TVar ((a, i), _)) = def_err "type is not clean"
   162   | checkT (TFree (a, _)) = TVar ((a, 0), [])
   163 
   164 fun label_ord NONE NONE = EQUAL
   165   | label_ord NONE (SOME _) = LESS
   166   | label_ord (SOME _) NONE = GREATER
   167   | label_ord (SOME l1) (SOME l2) = string_ord (l1,l2)
   168 
   169 fun compare_edges (e1 as (maxidx1, u1, v1, history1)) (e2 as (maxidx2, u2, v2, history2)) =
   170     let
   171       val t1 = u1 --> v1
   172       val t2 = u2 --> v2
   173     in
   174       if (is_instance_r t1 t2) then
   175 	(if is_instance_r t2 t1 then
   176 	   SOME (int_ord (length history2, length history1))
   177 	 else
   178 	   SOME LESS)
   179       else if (is_instance_r t2 t1) then
   180 	SOME GREATER
   181       else
   182 	NONE
   183     end
   184     
   185 fun merge_edges_1 (x, []) = []
   186   | merge_edges_1 (x, (y::ys)) = 
   187     (case compare_edges x y of
   188        SOME LESS => (y::ys)
   189      | SOME EQUAL => (y::ys)
   190      | SOME GREATER => merge_edges_1 (x, ys)
   191      | NONE => y::(merge_edges_1 (x, ys)))
   192     
   193 fun merge_edges xs ys = foldl merge_edges_1 xs ys
   194 
   195 fun pack_edges xs = merge_edges [] xs
   196 
   197 fun merge_labelled_edges [] es = es
   198   | merge_labelled_edges es [] = es
   199   | merge_labelled_edges ((l1,e1)::es1) ((l2,e2)::es2) = 
   200     (case label_ord l1 l2 of
   201        LESS => (l1, e1)::(merge_labelled_edges es1 ((l2, e2)::es2))
   202      | GREATER => (l2, e2)::(merge_labelled_edges ((l1, e1)::es1) es2)
   203      | EQUAL => (l1, merge_edges e1 e2)::(merge_labelled_edges es1 es2))
   204     
   205 fun defnode_edges_foldl f a defnode =
   206     let
   207       val (Defnode (ty, def_edges)) = defnode
   208       fun g (b, (_, (n, labelled_edges))) =
   209 	  foldl (fn ((s, edges), b') => 
   210 		    (foldl (fn (e, b'') => f ty n s e b'') b' edges))
   211 		b
   212 		labelled_edges		  		     
   213     in
   214       Symtab.foldl g (a, def_edges)
   215     end	
   216     
   217 fun define (actions, graph) (name, ty) axname body =
   218     let
   219       val ty = checkT ty
   220       val body = map (fn (n,t) => (n, checkT t)) body		 
   221       val mainref = name
   222       val mainnode  = (case Symtab.lookup (graph, mainref) of 
   223 			 NONE => def_err ("constant "^mainref^" is not declared")
   224 		       | SOME n => n)
   225       val (Node (n, gty, defs, backs, finals)) = mainnode
   226       val _ = (if is_instance_r ty gty then () else def_err "type of constant does not match declared type")
   227       fun check_def (s, Defnode (ty', _)) = 
   228 	  (if can_be_unified_r ty ty' then 
   229 	     raise (CLASH (mainref, axname, s))
   230 	   else if s = axname then
   231 	     def_err "name of axiom is already used for another definition of this constant"
   232 	   else false)	
   233       val _ = Symtab.exists check_def defs
   234       fun check_final finalty = 
   235 	  (if can_be_unified_r finalty ty then
   236 	     raise (FINAL (mainref, finalty))
   237 	   else
   238 	     true)
   239       val _ = forall check_final finals
   240 	             
   241       (* now we know that the only thing that can prevent acceptance of the definition is a cyclic dependency *)
   242 
   243       (* body contains the constants that this constant definition depends on. For each element of body,
   244          the function make_edges_to calculates a group of edges that connect this constant with 
   245          the constant that is denoted by the element of the body *)
   246       fun make_edges_to (bodyn, bodyty) =
   247 	  let
   248 	    val bnode = 
   249 		(case Symtab.lookup (graph, bodyn) of 
   250 		   NONE => def_err "body of constant definition references undeclared constant"
   251 		 | SOME x => x)
   252 	    val (Node (_, general_btyp, bdefs, bbacks, bfinals)) = bnode
   253 	  in
   254 	    case unify_r 0 bodyty general_btyp of
   255 	      NONE => NONE
   256 	    | SOME (maxidx, sigma1, sigma2) => 
   257 	      SOME (
   258 	      let
   259 		(* For each definition of the constant in the body, 
   260 		   check if the definition unifies with the type of the constant in the body. *)	                
   261                 fun make_edges ((swallowed, l),(def_name, Defnode (def_ty, _))) =
   262 		    if swallowed then
   263 		      (swallowed, l)
   264 		    else 
   265 		      (case unify_r 0 bodyty def_ty of
   266 			 NONE => (swallowed, l)
   267 		       | SOME (maxidx, sigma1, sigma2) => 
   268 			 (is_instance_r bodyty def_ty,
   269 			  merge_labelled_edges l [(SOME def_name,[(maxidx, subst sigma1 ty, subst sigma2 def_ty, [])])]))
   270                 val swallowed = exists (is_instance_r bodyty) bfinals
   271           	val (swallowed, edges) = Symtab.foldl make_edges ((swallowed, []), bdefs)
   272 	      in
   273 		if swallowed then 
   274 		  (bodyn, edges)
   275 		else 
   276 		  (bodyn, [(NONE, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])])]@edges)
   277 	      end)
   278 	  end 
   279           
   280       fun update_edges (b as (bodyn, bodyty), edges) =
   281 	  (case make_edges_to b of
   282 	     NONE => edges
   283 	   | SOME m =>
   284 	     (case Symtab.lookup (edges, bodyn) of
   285 		NONE => Symtab.update ((bodyn, m), edges)
   286 	      | SOME (_, es') => 
   287 		let 
   288 		  val (_, es) = m
   289 		  val es = merge_labelled_edges es es'
   290 		in
   291 		  Symtab.update ((bodyn, (bodyn, es)), edges)
   292 		end
   293 	     )
   294 	  )
   295           
   296       val edges = foldl update_edges Symtab.empty body
   297                   
   298       fun insert_edge edges (nodename, (defname_opt, edge)) = 
   299 	  let
   300 	    val newlink = [(defname_opt, [edge])]
   301 	  in
   302 	    case Symtab.lookup (edges, nodename) of
   303 	      NONE => Symtab.update ((nodename, (nodename, newlink)), edges)		    
   304 	    | SOME (_, links) => 
   305 	      let
   306 		val links' = merge_labelled_edges links newlink
   307 	      in
   308 		Symtab.update ((nodename, (nodename, links')), edges)
   309 	      end
   310 	  end				    
   311             
   312       (* We constructed all direct edges that this defnode has. 
   313          Now we have to construct the transitive hull by going a single step further. *)
   314           
   315       val thisDefnode = Defnode (ty, edges)
   316                         
   317       fun make_trans_edges _ noderef defname_opt (max1, alpha1, beta1, history1) edges = 
   318 	  case defname_opt of 
   319 	    NONE => edges
   320 	  | SOME defname => 		
   321 	    let
   322 	      val defnode = the (get_defnode' graph noderef defname)
   323 	      fun make_trans_edge _ noderef2 defname_opt2 (max2, alpha2, beta2, history2) edges =
   324 		  case unify_r (Int.max (max1, max2)) beta1 alpha2 of
   325 		    NONE => edges
   326 		  | SOME (max, sleft, sright) =>
   327 		    insert_edge edges (noderef2, 
   328 				       (defname_opt2, 							  
   329 					(max, subst sleft alpha1, subst sright beta2, 
   330 					 (subst_history sleft history1)@
   331 					 ((subst sleft beta1, noderef, defname)::
   332 					  (subst_history sright history2)))))
   333 	    in
   334 	      defnode_edges_foldl make_trans_edge edges defnode
   335 	    end
   336             
   337       val edges = defnode_edges_foldl make_trans_edges edges thisDefnode
   338                   
   339       val thisDefnode = Defnode (ty, edges)
   340 
   341       (* We also have to add the backreferences that this new defnode induces. *)
   342 	    
   343       fun hasNONElink ((NONE, _)::_) = true
   344 	| hasNONElink _ = false
   345 	                  
   346       fun install_backref graph noderef pointingnoderef pointingdefname = 
   347 	  let
   348 	    val (Node (pname, _, _, _, _)) = getnode graph pointingnoderef
   349 	    val (Node (name, ty, defs, backs, finals)) = getnode graph noderef
   350 	  in
   351 	    case Symtab.lookup (backs, pname) of
   352 	      NONE => 
   353 	      let 
   354 		val defnames = Symtab.update ((pointingdefname, ()), Symtab.empty)
   355 		val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs)
   356 	      in
   357 		Symtab.update ((name, Node (name, ty, defs, backs, finals)), graph) 			
   358 	      end
   359 	    | SOME (Backref (pointingnoderef, defnames)) =>
   360 	      let
   361 		val defnames = Symtab.update_new ((pointingdefname, ()), defnames)
   362 		val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs)
   363 	      in
   364 		Symtab.update ((name, Node (name, ty, defs, backs, finals)), graph)
   365 	      end
   366 	      handle Symtab.DUP _ => graph
   367 	  end
   368           
   369       fun install_backrefs (graph, (_, (noderef, labelled_edges))) =
   370 	  if hasNONElink labelled_edges then
   371 	    install_backref graph noderef mainref axname
   372 	  else 
   373 	    graph
   374             
   375       val graph = Symtab.foldl install_backrefs (graph, edges)
   376                   
   377       val (Node (_, _, _, backs, _)) = getnode graph mainref
   378       val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update_new 
   379         ((axname, thisDefnode), defs), backs, finals)), graph)
   380 		                
   381       (* Now we have to check all backreferences to this node and inform them about the new defnode. 
   382 	 In this section we also check for circularity. *)
   383       fun update_backrefs ((backs, newedges), (nodename, Backref (noderef, defnames))) =	    
   384 	  let
   385 	    val node = getnode graph noderef
   386 	    fun update_defs ((defnames, newedges),(defname, _)) =
   387 		let
   388 		  val (Defnode (_, defnode_edges)) = the (get_defnode node defname)
   389 		  val (_, labelled_edges) = the (Symtab.lookup (defnode_edges, n))
   390 						
   391 	          (* the type of thisDefnode is ty *)
   392 		  fun update (e as (max, alpha, beta, history), (none_edges, this_edges)) = 
   393 		      case unify_r max beta ty of
   394 			NONE => (e::none_edges, this_edges)
   395 		      | SOME (max', s_beta, s_ty) =>
   396 			let
   397 			  val alpha' = subst s_beta alpha
   398 			  val ty' = subst s_ty ty				      
   399 			  val _ = 
   400 			      if noderef = mainref andalso defname = axname then
   401 				(case unify alpha' ty' of
   402 				   NONE => 
   403 				   if (is_instance_r ty' alpha') then
   404 				     raise (INFINITE_CHAIN (
   405 					    (alpha', mainref, axname)::
   406 					    (subst_history s_beta history)@
   407 					    [(ty', mainref, axname)]))
   408 				   else ()
   409 				 | SOME s => raise (CIRCULAR (
   410 						    (subst s alpha', mainref, axname)::
   411 						    (subst_history s (subst_history s_beta history))@
   412 						    [(subst s ty', mainref, axname)])))
   413 			      else ()
   414 			  val edge = (max', alpha', ty', subst_history s_beta history)
   415 			in
   416 			  if is_instance_r beta ty then 
   417 			    (none_edges, edge::this_edges)
   418 			  else
   419 			    (e::none_edges, edge::this_edges)
   420 			end					    			   			    
   421 		in
   422 		  case labelled_edges of 
   423 		    ((NONE, edges)::_) => 
   424 		    let
   425 		      val (none_edges, this_edges) = foldl update ([], []) edges
   426 		      val defnames = if none_edges = [] then defnames else Symtab.update_new ((defname, ()), defnames) 
   427 		    in
   428 		      (defnames, (defname, none_edges, this_edges)::newedges)
   429 		    end			    
   430 		  | _ => sys_error "define: update_defs, internal error, corrupt backrefs"
   431 		end
   432 		    
   433 	    val (defnames, newedges') = Symtab.foldl update_defs ((Symtab.empty, []), defnames)
   434 	  in
   435 	    if Symtab.is_empty defnames then 
   436 	      (backs, (noderef, newedges')::newedges)
   437 	    else
   438 	      let
   439 		val backs = Symtab.update_new ((nodename, Backref (noderef, defnames)), backs)
   440 	      in
   441 		(backs, newedges)
   442 	      end
   443 	  end
   444 	  
   445 
   446       val (backs, newedges) = Symtab.foldl update_backrefs ((Symtab.empty, []), backs)
   447 						 
   448       (* If a Circular exception is thrown then we never reach this point. *)
   449       (* Ok, the definition is consistent, let's update this node. *)
   450       val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update 
   451         ((axname, thisDefnode), defs), backs, finals)), graph)
   452 
   453       (* Furthermore, update all the other nodes that backreference this node. *)
   454       fun final_update_backrefs graph noderef defname none_edges this_edges =
   455 	  let
   456 	    val node = getnode graph noderef
   457 	    val (Node (nodename, nodety, defs, backs, finals)) = node
   458 	    val (Defnode (defnode_ty, defnode_edges)) = the (get_defnode node defname)
   459 	    val (_, defnode_links) = the (Symtab.lookup (defnode_edges, n))
   460                                      
   461 	    fun update edges none_edges this_edges =
   462 		let 
   463 		  val u = merge_labelled_edges edges [(SOME axname, pack_edges this_edges)]
   464 		in
   465 		  if none_edges = [] then
   466 		    u
   467 		  else
   468 		    (NONE, pack_edges none_edges)::u
   469 		end
   470 		
   471 	    val defnode_links' = 
   472 		case defnode_links of 
   473 		  ((NONE, _) :: edges) => update edges none_edges this_edges
   474 		| edges => update edges none_edges this_edges
   475 	    val defnode_edges' = Symtab.update ((n, (mainref, defnode_links')), defnode_edges)
   476 	    val defs' = Symtab.update ((defname, Defnode (defnode_ty, defnode_edges')), defs)
   477 	  in
   478 	    Symtab.update ((nodename, Node (nodename, nodety, defs', backs, finals)), graph)
   479 	  end
   480           
   481       val graph = foldl (fn ((noderef, newedges),graph) => foldl (fn ((defname, none_edges, this_edges), graph) =>
   482         final_update_backrefs graph noderef defname none_edges this_edges) graph newedges) graph newedges		    
   483                   
   484     in	    
   485       ((Define (name, ty, axname, body))::actions, graph)	   
   486     end 
   487     
   488 fun finalize (history, graph) (c, ty) = 
   489     case Symtab.lookup (graph, c) of 
   490       NONE => def_err ("cannot finalize constant "^c^"; it is not declared")
   491     | SOME (Node (noderef, nodety, defs, backs, finals)) =>
   492       let 
   493 	val ty = checkT ty
   494 	val _ = if (not (is_instance_r ty nodety)) then
   495 		  def_err ("only type instances of the declared constant "^c^" can be finalized")
   496 		else ()
   497 	val _ = Symtab.exists (fn (def_name, Defnode (def_ty, _)) =>  
   498 				  if can_be_unified_r ty def_ty then 
   499 				    def_err ("cannot finalize constant "^c^"; clash with definition "^def_name)
   500 				  else 
   501 				    false)
   502 			      defs 
   503         
   504         fun update_finals [] = SOME [ty]
   505           | update_finals (final_ty::finals) = 
   506             (if is_instance_r ty final_ty then NONE
   507              else
   508                case update_finals finals of
   509                  NONE => NONE
   510                | (r as SOME finals) =>
   511                  if (is_instance_r final_ty ty) then
   512                    r
   513                  else
   514                    SOME (final_ty :: finals))                              
   515       in    
   516         case update_finals finals of
   517           NONE => (history, graph)
   518         | SOME finals => 
   519 	  let
   520 	    val graph = Symtab.update ((noderef, Node(noderef, nodety, defs, backs, finals)), graph)
   521 	                
   522 	    fun update_backref ((graph, backs), (backrefname, Backref (_, backdefnames))) =
   523 		let
   524 		  fun update_backdef ((graph, defnames), (backdefname, _)) = 
   525 	              let 
   526 			val (backnode as Node (_, backty, backdefs, backbacks, backfinals)) = getnode graph backrefname
   527 			val (Defnode (def_ty, all_edges)) = the (get_defnode backnode backdefname)						      
   528 			val (defnames', all_edges') = 
   529 			    case Symtab.lookup (all_edges, noderef) of
   530 			      NONE => sys_error "finalize: corrupt backref"
   531 			    | SOME (_, (NONE, edges)::rest) =>
   532 			      let
   533 				val edges' = List.filter (fn (_, _, beta, _) => not (is_instance_r beta ty)) edges
   534 			      in
   535 				if edges' = [] then 
   536 				  (defnames, Symtab.update ((noderef, (noderef, rest)), all_edges))
   537 				else
   538 				  (Symtab.update ((backdefname, ()), defnames), 
   539 				   Symtab.update ((noderef, (noderef, (NONE, edges')::rest)), all_edges))
   540 			      end
   541 			val defnode' = Defnode (def_ty, all_edges')
   542 			val backnode' = Node (backrefname, backty, Symtab.update ((backdefname, defnode'), backdefs), 
   543 					      backbacks, backfinals)
   544 		      in
   545 			(Symtab.update ((backrefname, backnode'), graph), defnames')			  			  
   546 		      end
   547 	              
   548 		  val (graph', defnames') = Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames)
   549 		in
   550 		  (graph', if Symtab.is_empty defnames' then backs 
   551 			   else Symtab.update ((backrefname, Backref (backrefname, defnames')), backs))
   552 		end
   553 	    val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs)
   554 	    val Node (_, _, defs, _, _) = getnode graph' noderef
   555 	  in
   556 	    ((Finalize (c, ty)) :: history, Symtab.update ((noderef, Node (noderef, nodety, defs, backs', finals)), graph'))
   557 	  end
   558       end
   559       
   560 fun merge' (Declare cty, g) = (declare g cty handle _ => g)
   561   | merge' (Define (name, ty, axname, body), g as (_, graph)) = 
   562     (case Symtab.lookup (graph, name) of
   563        NONE => define g (name, ty) axname body
   564      | SOME (Node (_, _, defs, _, _)) => 
   565        (case Symtab.lookup (defs, axname) of
   566 	  NONE => define g (name, ty) axname body
   567 	| SOME _ => g))
   568   | merge' (Finalize finals, g) = finalize g finals 
   569                        
   570 fun merge (actions, _) g = foldr merge' g actions
   571                            
   572 fun finals (history, graph) = 
   573     Symtab.foldl 
   574       (fn (finals, (_, Node(name, _, _, _, ftys))) => Symtab.update_new ((name, ftys), finals))  
   575       (Symtab.empty, graph)
   576 
   577 end;
   578 		
   579 
   580 
   581 (*fun tvar name = TVar ((name, 0), [])
   582 
   583 val bool = Type ("bool", [])
   584 val int = Type ("int", [])
   585 val alpha = tvar "'a"
   586 val beta = tvar "'b"
   587 val gamma = tvar "'c"
   588 fun pair a b = Type ("pair", [a,b])
   589 
   590 val _ = print "make empty"
   591 val g = Defs.empty 
   592 
   593 val _ = print "declare"
   594 val g = Defs.declare g "M" (alpha --> bool)
   595 val g = Defs.declare g "N" (beta --> bool)
   596 
   597 val _ = print "define"
   598 val g = Defs.define g "N" (alpha --> bool) "defN" [("M", alpha --> bool)]
   599 val g = Defs.define g "M" (alpha --> bool) "defM" [("N", int --> alpha)]
   600 
   601 val g = Defs.declare g "0" alpha
   602 val g = Defs.define g "0" (pair alpha beta) "zp" [("0", alpha), ("0", beta)]*)
   603 
   604