src/Pure/defs.ML
author obua
Wed Jun 01 21:25:35 2005 +0200 (2005-06-01)
changeset 16177 1af9f5c69745
parent 16158 2c3565b74b7a
child 16198 cfd070a2cc4d
permissions -rw-r--r--
Preliminary version of defs.ML that does not check final consts.
     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 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 "^(quote 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, edges) = Symtab.foldl make_edges ((false, []), bdefs)
   271 		    in
   272 			if swallowed (*orelse (exists (is_instance_r bodyty) bfinals)*) then 
   273 			    (bodyn, edges)
   274 			else 
   275 			    (bodyn, [(NONE, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])])]@edges)
   276 		    end)
   277 	    end 
   278 
   279 	fun update_edges (b as (bodyn, bodyty), edges) =
   280 	    (case make_edges_to b of
   281 		 NONE => edges
   282 	       | SOME m =>
   283 		 (case Symtab.lookup (edges, bodyn) of
   284 		      NONE => Symtab.update ((bodyn, m), edges)
   285 		    | SOME (_, es') => 
   286 		      let 
   287 			  val (_, es) = m
   288 			  val es = merge_labelled_edges es es'
   289 		      in
   290 			  Symtab.update ((bodyn, (bodyn, es)), edges)
   291 		      end
   292 		 )
   293 	    )
   294 
   295 	val edges = foldl update_edges Symtab.empty body
   296 
   297 	fun insert_edge edges (nodename, (defname_opt, edge)) = 
   298 	    let
   299 		val newlink = [(defname_opt, [edge])]
   300 	    in
   301 		case Symtab.lookup (edges, nodename) of
   302 		    NONE => Symtab.update ((nodename, (nodename, newlink)), edges)		    
   303 		  | SOME (_, links) => 
   304 		    let
   305 			val links' = merge_labelled_edges links newlink
   306 		    in
   307 			Symtab.update ((nodename, (nodename, links')), edges)
   308 		    end
   309 	    end				    
   310 
   311         (* We constructed all direct edges that this defnode has. 
   312            Now we have to construct the transitive hull by going a single step further. *)
   313 
   314         val thisDefnode = Defnode (ty, edges)
   315 
   316 	fun make_trans_edges _ noderef defname_opt (max1, alpha1, beta1, history1) edges = 
   317 	    case defname_opt of 
   318 		NONE => edges
   319 	      | SOME defname => 		
   320 		let
   321 		    val defnode = the (get_defnode' graph noderef defname)
   322 		    fun make_trans_edge _ noderef2 defname_opt2 (max2, alpha2, beta2, history2) edges =
   323 			case unify_r (Int.max (max1, max2)) beta1 alpha2 of
   324 			    NONE => edges
   325 			  | SOME (max, sleft, sright) =>
   326 			    insert_edge edges (noderef2, 
   327 					       (defname_opt2, 							  
   328 						(max, subst sleft alpha1, subst sright beta2, 
   329 						 (subst_history sleft history1)@
   330 						 ((subst sleft beta1, noderef, defname)::
   331 						  (subst_history sright history2)))))
   332 		in
   333 		    defnode_edges_foldl make_trans_edge edges defnode
   334 		end
   335 
   336 	val edges = defnode_edges_foldl make_trans_edges edges thisDefnode
   337 
   338 	val thisDefnode = Defnode (ty, edges)
   339 
   340 	(* We also have to add the backreferences that this new defnode induces. *)
   341 	    
   342 	fun hasNONElink ((NONE, _)::_) = true
   343 	  | hasNONElink _ = false
   344 	
   345 	fun install_backref graph noderef pointingnoderef pointingdefname = 
   346 	    let
   347 		val (Node (pname, _, _, _, _)) = getnode graph pointingnoderef
   348 		val (Node (name, ty, defs, backs, finals)) = getnode graph noderef
   349 	    in
   350 		case Symtab.lookup (backs, pname) of
   351 		    NONE => 
   352 		    let 
   353 			val defnames = Symtab.update ((pointingdefname, ()), Symtab.empty)
   354 			val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs)
   355 		    in
   356 			Symtab.update ((name, Node (name, ty, defs, backs, finals)), graph) 			
   357 		    end
   358 		  | SOME (Backref (pointingnoderef, defnames)) =>
   359 		    let
   360 			val defnames = Symtab.update_new ((pointingdefname, ()), defnames)
   361 			val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs)
   362 		    in
   363 			Symtab.update ((name, Node (name, ty, defs, backs, finals)), graph)
   364 		    end
   365 		    handle Symtab.DUP _ => graph
   366 	    end
   367 
   368 	fun install_backrefs (graph, (_, (noderef, labelled_edges))) =
   369 	    if hasNONElink labelled_edges then
   370 		install_backref graph noderef mainref axname
   371 	    else 
   372 		graph
   373 
   374         val graph = Symtab.foldl install_backrefs (graph, edges)
   375 
   376         val (Node (_, _, _, backs, _)) = getnode graph mainref
   377 	val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update_new 
   378           ((axname, thisDefnode), defs), backs, finals)), graph)
   379 		    
   380 	(* Now we have to check all backreferences to this node and inform them about the new defnode. 
   381 	   In this section we also check for circularity. *)
   382         fun update_backrefs ((backs, newedges), (nodename, Backref (noderef, defnames))) =	    
   383 	    let
   384 		val node = getnode graph noderef
   385 		fun update_defs ((defnames, newedges),(defname, _)) =
   386 		    let
   387 			val (Defnode (_, defnode_edges)) = the (get_defnode node defname)
   388 			val (_, labelled_edges) = the (Symtab.lookup (defnode_edges, n))
   389 						      
   390 			(* the type of thisDefnode is ty *)
   391 			fun update (e as (max, alpha, beta, history), (none_edges, this_edges)) = 
   392 			    case unify_r max beta ty of
   393 				NONE => (e::none_edges, this_edges)
   394 			      | SOME (max', s_beta, s_ty) =>
   395 				let
   396 				    val alpha' = subst s_beta alpha
   397 				    val ty' = subst s_ty ty				      
   398 				    val _ = 
   399 					if noderef = mainref andalso defname = axname then
   400 					    (case unify alpha' ty' of
   401 						 NONE => 
   402 						   if (is_instance_r ty' alpha') then
   403 						       raise (INFINITE_CHAIN (
   404 							      (alpha', mainref, axname)::
   405 							      (subst_history s_beta history)@
   406 							      [(ty', mainref, axname)]))
   407 						   else ()
   408 					       | SOME s => raise (CIRCULAR (
   409 								  (subst s alpha', mainref, axname)::
   410 								  (subst_history s (subst_history s_beta history))@
   411 								  [(subst s ty', mainref, axname)])))
   412 					else ()
   413 				    val edge = (max', alpha', ty', subst_history s_beta history)
   414 				in
   415 				    if is_instance_r beta ty then 
   416 					(none_edges, edge::this_edges)
   417 				    else
   418 					(e::none_edges, edge::this_edges)
   419 				end					    			   			    
   420 		    in
   421 			case labelled_edges of 
   422 			    ((NONE, edges)::_) => 
   423 			    let
   424 				val (none_edges, this_edges) = foldl update ([], []) edges
   425 				val defnames = if none_edges = [] then defnames else Symtab.update_new ((defname, ()), defnames) 
   426 			    in
   427 				(defnames, (defname, none_edges, this_edges)::newedges)
   428 			    end			    
   429 			  | _ => sys_error "define: update_defs, internal error, corrupt backrefs"
   430 		    end
   431 		    
   432 		val (defnames, newedges') = Symtab.foldl update_defs ((Symtab.empty, []), defnames)
   433 	    in
   434 		if Symtab.is_empty defnames then 
   435 		    (backs, (noderef, newedges')::newedges)
   436 		else
   437 		    let
   438 			val backs = Symtab.update_new ((nodename, Backref (noderef, defnames)), backs)
   439 		    in
   440 			(backs, newedges)
   441 		    end
   442 	    end
   443 	    
   444 
   445 	val (backs, newedges) = Symtab.foldl update_backrefs ((Symtab.empty, []), backs)
   446 						 
   447 	(* If a Circular exception is thrown then we never reach this point. *)
   448         (* Ok, the definition is consistent, let's update this node. *)
   449 	val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update 
   450 	  ((axname, thisDefnode), defs), backs, finals)), graph)
   451 
   452         (* Furthermore, update all the other nodes that backreference this node. *)
   453         fun final_update_backrefs graph noderef defname none_edges this_edges =
   454 	    let
   455 		val node = getnode graph noderef
   456 		val (Node (nodename, nodety, defs, backs, finals)) = node
   457 		val (Defnode (defnode_ty, defnode_edges)) = the (get_defnode node defname)
   458 		val (_, defnode_links) = the (Symtab.lookup (defnode_edges, n))
   459 
   460 		fun update edges none_edges this_edges =
   461 		    let 
   462 			val u = merge_labelled_edges edges [(SOME axname, pack_edges this_edges)]
   463 		    in
   464 			if none_edges = [] then
   465 			    u
   466 			else
   467 			    (NONE, pack_edges none_edges)::u
   468 		    end
   469 		    
   470 		val defnode_links' = 
   471 		    case defnode_links of 
   472 			((NONE, _) :: edges) => update edges none_edges this_edges
   473 		      | edges => update edges none_edges this_edges
   474 		val defnode_edges' = Symtab.update ((n, (mainref, defnode_links')), defnode_edges)
   475 		val defs' = Symtab.update ((defname, Defnode (defnode_ty, defnode_edges')), defs)
   476 	    in
   477 		Symtab.update ((nodename, Node (nodename, nodety, defs', backs, finals)), graph)
   478 	    end
   479 
   480 	val graph = foldl (fn ((noderef, newedges),graph) => foldl (fn ((defname, none_edges, this_edges), graph) =>
   481            final_update_backrefs graph noderef defname none_edges this_edges) graph newedges) graph newedges		    
   482 
   483     in	    
   484 	((Define (name, ty, axname, body))::actions, graph)	   
   485     end 
   486 
   487     fun finalize' ((c, ty), graph) = 
   488       case Symtab.lookup (graph, c) of 
   489 	  NONE => def_err ("cannot finalize constant "^(quote c)^"; it is not declared")
   490 	| SOME (Node (noderef, nodety, defs, backs, finals)) =>
   491 	  let 
   492 	      val ty = checkT ty
   493 	      val _ = if (not (is_instance_r ty nodety)) then
   494 			  def_err ("only type instances of the declared constant "^(quote c)^" can be finalized")
   495 		      else ()
   496 	      val _ = Symtab.exists (fn (def_name, Defnode (def_ty, _)) =>  
   497 					if can_be_unified_r ty def_ty then 
   498 					    def_err ("cannot finalize constant "^(quote c)^"; clash with definition "^(quote def_name))
   499 					else 
   500 					    false)
   501 				    defs
   502 	  in				    
   503 	      if exists (is_instance_r ty) finals then
   504 		  graph
   505 	      else 
   506 	      let
   507 	          val finals = ty :: finals
   508 		  val graph = Symtab.update ((noderef, Node(noderef, nodety, defs, backs, finals)), graph)
   509 	      in
   510 		  graph
   511 	      end
   512 (*		  fun update_backref ((graph, backs), (backrefname, Backref (_, backdefnames))) =
   513 		  let
   514 		      fun update_backdef ((graph, defnames), (backdefname, _)) = 
   515 	              let 
   516 			  val (backnode as Node (_, backty, backdefs, backbacks, backfinals)) = getnode graph backrefname
   517 			  val (Defnode (def_ty, all_edges)) = the (get_defnode backnode backdefname)						      
   518 			  val (defnames', all_edges') = 
   519 			      case Symtab.lookup (all_edges, noderef) of
   520 				  NONE => sys_error "finalize: corrupt backref"
   521 				| SOME (_, (NONE, edges)::rest) =>
   522 				  let
   523 				      val edges' = List.filter (fn (_, _, beta, _) => not (is_instance_r beta ty)) edges
   524 				  in
   525 				      if edges' = [] then 
   526 					  (defnames, Symtab.update ((noderef, (noderef, rest)), all_edges))
   527 				      else
   528 					  (Symtab.update ((backdefname, ()), defnames), 
   529 					   Symtab.update ((noderef, (noderef, (NONE, edges')::rest)), all_edges))
   530 				  end
   531 			  val defnode' = Defnode (def_ty, all_edges')
   532 			  val backnode' = Node (backrefname, backty, Symtab.update ((backdefname, defnode'), backdefs), 
   533 					   backbacks, backfinals)
   534 		      in
   535 			  (Symtab.update ((backrefname, backnode'), graph), defnames')			  			  
   536 		      end
   537 	  
   538 		      val (graph', defnames') = Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames)
   539 		  in
   540 		      (graph', if Symtab.is_empty defnames' then backs 
   541 			       else Symtab.update ((backrefname, Backref (backrefname, defnames')), backs))
   542 		  end
   543 		  val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs)
   544 		  val Node (_, _, defs, _, _) = getnode graph' noderef
   545 	      in
   546 		  Symtab.update ((noderef, Node (noderef, nodety, defs, backs', finals)), graph')
   547 	      end*)
   548 	  end
   549 	   
   550     fun finalize (history, graph) c_ty = (history, graph)
   551 	(*((Finalize c_ty)::history, finalize' (c_ty, graph))*)
   552     
   553     fun merge' (Declare cty, g) = (declare g cty handle _ => g)
   554       | merge' (Define (name, ty, axname, body), g as (_, graph)) = 
   555 	(case Symtab.lookup (graph, name) of
   556 	     NONE => define g (name, ty) axname body
   557 	   | SOME (Node (_, _, defs, _, _)) => 
   558 	     (case Symtab.lookup (defs, axname) of
   559 		  NONE => define g (name, ty) axname body
   560 		| SOME _ => g))
   561       | merge' (Finalize finals, g) = (finalize g finals handle _ => g)
   562 	
   563     fun myrev [] ys = ys
   564       | myrev (x::xs) ys = myrev xs (x::ys)
   565 
   566     fun merge (actions, _) g = foldr merge' g actions
   567 
   568     fun finals (history, graph) = 
   569 	Symtab.foldl 
   570 	    (fn (finals, (_, Node(name, _, _, _, ftys))) => Symtab.update_new ((name, ftys), finals))  
   571 	    (Symtab.empty, graph)
   572 
   573 end;
   574 		
   575 
   576 
   577 (*fun tvar name = TVar ((name, 0), [])
   578 
   579 val bool = Type ("bool", [])
   580 val int = Type ("int", [])
   581 val alpha = tvar "'a"
   582 val beta = tvar "'b"
   583 val gamma = tvar "'c"
   584 fun pair a b = Type ("pair", [a,b])
   585 
   586 val _ = print "make empty"
   587 val g = Defs.empty 
   588 
   589 val _ = print "declare"
   590 val g = Defs.declare g "M" (alpha --> bool)
   591 val g = Defs.declare g "N" (beta --> bool)
   592 
   593 val _ = print "define"
   594 val g = Defs.define g "N" (alpha --> bool) "defN" [("M", alpha --> bool)]
   595 val g = Defs.define g "M" (alpha --> bool) "defM" [("N", int --> alpha)]
   596 
   597 val g = Defs.declare g "0" alpha
   598 val g = Defs.define g "0" (pair alpha beta) "zp" [("0", alpha), ("0", beta)]*)
   599 
   600