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