src/Pure/defs.ML
author obua
Tue May 31 19:32:41 2005 +0200 (2005-05-31)
changeset 16158 2c3565b74b7a
parent 16113 692fe6595755
child 16177 1af9f5c69745
permissions -rw-r--r--
Removed final_consts from theory data. Now const_deps deals with final
constants.
     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 constant for a particular type, 
    44                              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 forall_table P tab = Symtab.foldl (fn (true, e) => P e | (b, _) => b) (true, tab);
   165 
   166 fun label_ord NONE NONE = EQUAL
   167   | label_ord NONE (SOME _) = LESS
   168   | label_ord (SOME _) NONE = GREATER
   169   | label_ord (SOME l1) (SOME l2) = string_ord (l1,l2)
   170 
   171 fun compare_edges (e1 as (maxidx1, u1, v1, history1)) (e2 as (maxidx2, u2, v2, history2)) =
   172     let
   173 	val t1 = u1 --> v1
   174 	val t2 = u2 --> v2
   175     in
   176 	if (is_instance_r t1 t2) then
   177 	    (if is_instance_r t2 t1 then
   178 		 SOME (int_ord (length history2, length history1))
   179 	     else
   180 		 SOME LESS)
   181 	else if (is_instance_r t2 t1) then
   182 	    SOME GREATER
   183 	else
   184 	    NONE
   185     end
   186 
   187 fun merge_edges_1 (x, []) = []
   188   | merge_edges_1 (x, (y::ys)) = 
   189     (case compare_edges x y of
   190 	 SOME LESS => (y::ys)
   191        | SOME EQUAL => (y::ys)
   192        | SOME GREATER => merge_edges_1 (x, ys)
   193        | NONE => y::(merge_edges_1 (x, ys)))
   194 
   195 fun merge_edges xs ys = foldl merge_edges_1 xs ys
   196 
   197 fun pack_edges xs = merge_edges [] xs
   198 
   199 fun merge_labelled_edges [] es = es
   200   | merge_labelled_edges es [] = es
   201   | merge_labelled_edges ((l1,e1)::es1) ((l2,e2)::es2) = 
   202     (case label_ord l1 l2 of
   203 	 LESS => (l1, e1)::(merge_labelled_edges es1 ((l2, e2)::es2))
   204        | GREATER => (l2, e2)::(merge_labelled_edges ((l1, e1)::es1) es2)
   205        | EQUAL => (l1, merge_edges e1 e2)::(merge_labelled_edges es1 es2))
   206 
   207 fun defnode_edges_foldl f a defnode =
   208     let
   209 	val (Defnode (ty, def_edges)) = defnode
   210 	fun g (b, (_, (n, labelled_edges))) =
   211 	    foldl (fn ((s, edges), b') => 
   212 		      (foldl (fn (e, b'') => f ty n s e b'') b' edges))
   213 		  b
   214 		  labelled_edges		  		     
   215     in
   216 	Symtab.foldl g (a, def_edges)
   217     end	
   218 
   219 fun define (actions, graph) (name, ty) axname body =
   220     let
   221 	val ty = checkT ty
   222 	val body = map (fn (n,t) => (n, checkT t)) body		 
   223 	val mainref = name
   224 	val mainnode  = (case Symtab.lookup (graph, mainref) of 
   225 			     NONE => def_err ("constant "^(quote mainref)^" is not declared")
   226 			   | SOME n => n)
   227 	val (Node (n, gty, defs, backs, finals)) = mainnode
   228 	val _ = (if is_instance_r ty gty then () else def_err "type of constant does not match declared type")
   229 	fun check_def (s, Defnode (ty', _)) = 
   230 	    (if can_be_unified_r ty ty' then 
   231 		 raise (CLASH (mainref, axname, s))
   232 	     else if s = axname then
   233 	         def_err "name of axiom is already used for another definition of this constant"
   234 	     else true)	
   235 	val _ = forall_table check_def defs		
   236 	fun check_final finalty = 
   237 	    (if can_be_unified_r finalty ty then
   238 		 raise (FINAL (mainref, finalty))
   239 	     else
   240 		 true)
   241 	val _ = forall check_final finals
   242 	
   243 	(* now we know that the only thing that can prevent acceptance of the definition is a cyclic dependency *)
   244 
   245 	(* body contains the constants that this constant definition depends on. For each element of body,
   246            the function make_edges_to calculates a group of edges that connect this constant with 
   247            the constant that is denoted by the element of the body *)
   248 	fun make_edges_to (bodyn, bodyty) =
   249 	    let
   250 		val bnode = 
   251 		    (case Symtab.lookup (graph, bodyn) of 
   252 			 NONE => def_err "body of constant definition references undeclared constant"
   253 		       | SOME x => x)
   254 		val (Node (_, general_btyp, bdefs, bbacks, bfinals)) = bnode
   255 	    in
   256 		case unify_r 0 bodyty general_btyp of
   257 		    NONE => NONE
   258 		  | SOME (maxidx, sigma1, sigma2) => 
   259 		    SOME (
   260 		    let
   261 			(* For each definition of the constant in the body, 
   262 			   check if the definition unifies with the type of the constant in the body. *)	                
   263 	              fun make_edges ((swallowed, l),(def_name, Defnode (def_ty, _))) =
   264 			  if swallowed then
   265 			      (swallowed, l)
   266 			  else 
   267 			      (case unify_r 0 bodyty def_ty of
   268 				   NONE => (swallowed, l)
   269 				 | SOME (maxidx, sigma1, sigma2) => 
   270 				   (is_instance_r bodyty def_ty,
   271 				    merge_labelled_edges l [(SOME def_name,[(maxidx, subst sigma1 ty, subst sigma2 def_ty, [])])]))
   272           	      val (swallowed, edges) = Symtab.foldl make_edges ((false, []), bdefs)
   273 		    in
   274 			if swallowed orelse (exists (is_instance_r bodyty) bfinals) then 
   275 			    (bodyn, edges)
   276 			else 
   277 			    (bodyn, [(NONE, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])])]@edges)
   278 		    end)
   279 	    end 
   280 
   281 	fun update_edges (b as (bodyn, bodyty), edges) =
   282 	    (case make_edges_to b of
   283 		 NONE => edges
   284 	       | SOME m =>
   285 		 (case Symtab.lookup (edges, bodyn) of
   286 		      NONE => Symtab.update ((bodyn, m), edges)
   287 		    | SOME (_, es') => 
   288 		      let 
   289 			  val (_, es) = m
   290 			  val es = merge_labelled_edges es es'
   291 		      in
   292 			  Symtab.update ((bodyn, (bodyn, es)), edges)
   293 		      end
   294 		 )
   295 	    )
   296 
   297 	val edges = foldl update_edges Symtab.empty body
   298 
   299 	fun insert_edge edges (nodename, (defname_opt, edge)) = 
   300 	    let
   301 		val newlink = [(defname_opt, [edge])]
   302 	    in
   303 		case Symtab.lookup (edges, nodename) of
   304 		    NONE => Symtab.update ((nodename, (nodename, newlink)), edges)		    
   305 		  | SOME (_, links) => 
   306 		    let
   307 			val links' = merge_labelled_edges links newlink
   308 		    in
   309 			Symtab.update ((nodename, (nodename, links')), edges)
   310 		    end
   311 	    end				    
   312 
   313         (* We constructed all direct edges that this defnode has. 
   314            Now we have to construct the transitive hull by going a single step further. *)
   315 
   316         val thisDefnode = Defnode (ty, edges)
   317 
   318 	fun make_trans_edges _ noderef defname_opt (max1, alpha1, beta1, history1) edges = 
   319 	    case defname_opt of 
   320 		NONE => edges
   321 	      | SOME defname => 		
   322 		let
   323 		    val defnode = the (get_defnode' graph noderef defname)
   324 		    fun make_trans_edge _ noderef2 defname_opt2 (max2, alpha2, beta2, history2) edges =
   325 			case unify_r (Int.max (max1, max2)) beta1 alpha2 of
   326 			    NONE => edges
   327 			  | SOME (max, sleft, sright) =>
   328 			    insert_edge edges (noderef2, 
   329 					       (defname_opt2, 							  
   330 						(max, subst sleft alpha1, subst sright beta2, 
   331 						 (subst_history sleft history1)@
   332 						 ((subst sleft beta1, noderef, defname)::
   333 						  (subst_history sright history2)))))
   334 		in
   335 		    defnode_edges_foldl make_trans_edge edges defnode
   336 		end
   337 
   338 	val edges = defnode_edges_foldl make_trans_edges edges thisDefnode
   339 
   340 	val thisDefnode = Defnode (ty, edges)
   341 
   342 	(* We also have to add the backreferences that this new defnode induces. *)
   343 	    
   344 	fun hasNONElink ((NONE, _)::_) = true
   345 	  | hasNONElink _ = false
   346 	
   347 	fun install_backref graph noderef pointingnoderef pointingdefname = 
   348 	    let
   349 		val (Node (pname, _, _, _, _)) = getnode graph pointingnoderef
   350 		val (Node (name, ty, defs, backs, finals)) = getnode graph noderef
   351 	    in
   352 		case Symtab.lookup (backs, pname) of
   353 		    NONE => 
   354 		    let 
   355 			val defnames = Symtab.update ((pointingdefname, ()), Symtab.empty)
   356 			val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs)
   357 		    in
   358 			Symtab.update ((name, Node (name, ty, defs, backs, finals)), graph) 			
   359 		    end
   360 		  | SOME (Backref (pointingnoderef, defnames)) =>
   361 		    let
   362 			val defnames = Symtab.update_new ((pointingdefname, ()), defnames)
   363 			val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs)
   364 		    in
   365 			Symtab.update ((name, Node (name, ty, defs, backs, finals)), graph)
   366 		    end
   367 		    handle Symtab.DUP _ => graph
   368 	    end
   369 
   370 	fun install_backrefs (graph, (_, (noderef, labelled_edges))) =
   371 	    if hasNONElink labelled_edges then
   372 		install_backref graph noderef mainref axname
   373 	    else 
   374 		graph
   375 
   376         val graph = Symtab.foldl install_backrefs (graph, edges)
   377 
   378         val (Node (_, _, _, backs, _)) = getnode graph mainref
   379 	val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update_new 
   380           ((axname, thisDefnode), defs), backs, finals)), graph)
   381 		    
   382 	(* Now we have to check all backreferences to this node and inform them about the new defnode. 
   383 	   In this section we also check for circularity. *)
   384         fun update_backrefs ((backs, newedges), (nodename, Backref (noderef, defnames))) =	    
   385 	    let
   386 		val node = getnode graph noderef
   387 		fun update_defs ((defnames, newedges),(defname, _)) =
   388 		    let
   389 			val (Defnode (_, defnode_edges)) = the (get_defnode node defname)
   390 			val (_, labelled_edges) = the (Symtab.lookup (defnode_edges, n))
   391 						      
   392 			(* the type of thisDefnode is ty *)
   393 			fun update (e as (max, alpha, beta, history), (none_edges, this_edges)) = 
   394 			    case unify_r max beta ty of
   395 				NONE => (e::none_edges, this_edges)
   396 			      | SOME (max', s_beta, s_ty) =>
   397 				let
   398 				    val alpha' = subst s_beta alpha
   399 				    val ty' = subst s_ty ty				      
   400 				    val _ = 
   401 					if noderef = mainref andalso defname = axname then
   402 					    (case unify alpha' ty' of
   403 						 NONE => 
   404 						   if (is_instance_r ty' alpha') then
   405 						       raise (INFINITE_CHAIN (
   406 							      (alpha', mainref, axname)::
   407 							      (subst_history s_beta history)@
   408 							      [(ty', mainref, axname)]))
   409 						   else ()
   410 					       | SOME s => raise (CIRCULAR (
   411 								  (subst s alpha', mainref, axname)::
   412 								  (subst_history s (subst_history s_beta history))@
   413 								  [(subst s ty', mainref, axname)])))
   414 					else ()
   415 				    val edge = (max', alpha', ty', subst_history s_beta history)
   416 				in
   417 				    if is_instance_r beta ty then 
   418 					(none_edges, edge::this_edges)
   419 				    else
   420 					(e::none_edges, edge::this_edges)
   421 				end					    			   			    
   422 		    in
   423 			case labelled_edges of 
   424 			    ((NONE, edges)::_) => 
   425 			    let
   426 				val (none_edges, this_edges) = foldl update ([], []) edges
   427 				val defnames = if none_edges = [] then defnames else Symtab.update_new ((defname, ()), defnames) 
   428 			    in
   429 				(defnames, (defname, none_edges, this_edges)::newedges)
   430 			    end			    
   431 			  | _ => sys_error "define: update_defs, internal error, corrupt backrefs"
   432 		    end
   433 		    
   434 		val (defnames, newedges') = Symtab.foldl update_defs ((Symtab.empty, []), defnames)
   435 	    in
   436 		if Symtab.is_empty defnames then 
   437 		    (backs, (noderef, newedges')::newedges)
   438 		else
   439 		    let
   440 			val backs = Symtab.update_new ((nodename, Backref (noderef, defnames)), backs)
   441 		    in
   442 			(backs, newedges)
   443 		    end
   444 	    end
   445 	    
   446 
   447 	val (backs, newedges) = Symtab.foldl update_backrefs ((Symtab.empty, []), backs)
   448 						 
   449 	(* If a Circular exception is thrown then we never reach this point. *)
   450         (* Ok, the definition is consistent, let's update this node. *)
   451 	val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update 
   452 	  ((axname, thisDefnode), defs), backs, finals)), graph)
   453 
   454         (* Furthermore, update all the other nodes that backreference this node. *)
   455         fun final_update_backrefs graph noderef defname none_edges this_edges =
   456 	    let
   457 		val node = getnode graph noderef
   458 		val (Node (nodename, nodety, defs, backs, finals)) = node
   459 		val (Defnode (defnode_ty, defnode_edges)) = the (get_defnode node defname)
   460 		val (_, defnode_links) = the (Symtab.lookup (defnode_edges, n))
   461 
   462 		fun update edges none_edges this_edges =
   463 		    let 
   464 			val u = merge_labelled_edges edges [(SOME axname, pack_edges this_edges)]
   465 		    in
   466 			if none_edges = [] then
   467 			    u
   468 			else
   469 			    (NONE, pack_edges none_edges)::u
   470 		    end
   471 		    
   472 		val defnode_links' = 
   473 		    case defnode_links of 
   474 			((NONE, _) :: edges) => update edges none_edges this_edges
   475 		      | edges => update edges none_edges this_edges
   476 		val defnode_edges' = Symtab.update ((n, (mainref, defnode_links')), defnode_edges)
   477 		val defs' = Symtab.update ((defname, Defnode (defnode_ty, defnode_edges')), defs)
   478 	    in
   479 		Symtab.update ((nodename, Node (nodename, nodety, defs', backs, finals)), graph)
   480 	    end
   481 
   482 	val graph = foldl (fn ((noderef, newedges),graph) => foldl (fn ((defname, none_edges, this_edges), graph) =>
   483            final_update_backrefs graph noderef defname none_edges this_edges) graph newedges) graph newedges		    
   484 
   485     in	    
   486 	((Define (name, ty, axname, body))::actions, graph)	   
   487     end 
   488 
   489     fun finalize' ((c, ty), graph) = 
   490       case Symtab.lookup (graph, c) of 
   491 	  NONE => def_err ("finalize: constant "^(quote c)^" is not declared")
   492 	| SOME (Node (noderef, nodety, defs, backs, finals)) =>
   493 	  let 
   494 	      val nodety = checkT nodety 
   495 	  in
   496 	      if (not (is_instance_r ty nodety)) then
   497 		  def_err ("finalize: only type instances of the declared constant "^(quote c)^" can be finalized")
   498 	      else if exists (is_instance_r ty) finals then
   499 		  graph
   500 	      else 
   501 	      let
   502 	          val finals = ty :: finals
   503 		  val graph = Symtab.update ((noderef, Node(noderef, nodety, defs, backs, finals)), graph)
   504 		  fun update_backref ((graph, backs), (backrefname, Backref (_, backdefnames))) =
   505 		  let
   506 		      fun update_backdef ((graph, defnames), (backdefname, _)) = 
   507 	              let 
   508 			  val (backnode as Node (_, backty, backdefs, backbacks, backfinals)) = getnode graph backrefname
   509 			  val (Defnode (def_ty, all_edges)) = the (get_defnode backnode backdefname)						      
   510 			  val (defnames', all_edges') = 
   511 			      case Symtab.lookup (all_edges, noderef) of
   512 				  NONE => sys_error "finalize: corrupt backref"
   513 				| SOME (_, (NONE, edges)::rest) =>
   514 				  let
   515 				      val edges' = List.filter (fn (_, _, beta, _) => not (is_instance_r beta ty)) edges
   516 				  in
   517 				      if edges' = [] then 
   518 					  (defnames, Symtab.update ((noderef, (noderef, rest)), all_edges))
   519 				      else
   520 					  (Symtab.update ((backdefname, ()), defnames), 
   521 					   Symtab.update ((noderef, (noderef, (NONE, edges')::rest)), all_edges))
   522 				  end
   523 			  val defnode' = Defnode (def_ty, all_edges')
   524 			  val backnode' = Node (backrefname, backty, Symtab.update ((backdefname, defnode'), backdefs), 
   525 					   backbacks, backfinals)
   526 		      in
   527 			  (Symtab.update ((backrefname, backnode'), graph), defnames')			  			  
   528 		      end
   529 	  
   530 		      val (graph', defnames') = Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames)
   531 		  in
   532 		      (graph', if Symtab.is_empty defnames' then backs 
   533 			       else Symtab.update ((backrefname, Backref (backrefname, defnames')), backs))
   534 		  end
   535 		  val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs)
   536 		  val Node (_, _, defs, _, _) = getnode graph' noderef
   537 	      in
   538 		  Symtab.update ((noderef, Node (noderef, nodety, defs, backs', finals)), graph')
   539 	      end
   540 	  end
   541 	   
   542     fun finalize (history, graph) c_ty = ((Finalize c_ty)::history, finalize' (c_ty, graph))
   543     
   544     fun merge' (Declare cty, g) = (declare g cty handle _ => g)
   545       | merge' (Define (name, ty, axname, body), g as (_, graph)) = 
   546 	(case Symtab.lookup (graph, name) of
   547 	     NONE => define g (name, ty) axname body
   548 	   | SOME (Node (_, _, defs, _, _)) => 
   549 	     (case Symtab.lookup (defs, axname) of
   550 		  NONE => define g (name, ty) axname body
   551 		| SOME _ => g))
   552       | merge' (Finalize finals, g) = (finalize g finals handle _ => g)
   553 	
   554     fun merge (actions, _) g = foldr merge' g actions
   555 
   556     fun finals (history, graph) = 
   557 	Symtab.foldl 
   558 	    (fn (finals, (_, Node(name, _, _, _, ftys))) => Symtab.update_new ((name, ftys), finals))  
   559 	    (Symtab.empty, graph)
   560 
   561 end;
   562 		
   563 
   564 
   565 (*fun tvar name = TVar ((name, 0), [])
   566 
   567 val bool = Type ("bool", [])
   568 val int = Type ("int", [])
   569 val alpha = tvar "'a"
   570 val beta = tvar "'b"
   571 val gamma = tvar "'c"
   572 fun pair a b = Type ("pair", [a,b])
   573 
   574 val _ = print "make empty"
   575 val g = Defs.empty 
   576 
   577 val _ = print "declare"
   578 val g = Defs.declare g "M" (alpha --> bool)
   579 val g = Defs.declare g "N" (beta --> bool)
   580 
   581 val _ = print "define"
   582 val g = Defs.define g "N" (alpha --> bool) "defN" [("M", alpha --> bool)]
   583 val g = Defs.define g "M" (alpha --> bool) "defM" [("N", int --> alpha)]
   584 
   585 val g = Defs.declare g "0" alpha
   586 val g = Defs.define g "0" (pair alpha beta) "zp" [("0", alpha), ("0", beta)]*)
   587 
   588