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