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.
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@16158
    17
    exception FINAL of string * typ
obua@16108
    18
    exception CLASH of string * string * string
obua@16108
    19
    
obua@16108
    20
    val empty : graph
obua@16158
    21
    val declare : graph -> string * typ -> graph  (* exception DEFS *)
obua@16158
    22
    val define : graph -> string * typ -> string -> (string * typ) list -> graph 
obua@16158
    23
      (* exception DEFS, CIRCULAR, INFINITE_CHAIN, CLASH, FINAL *)
obua@16158
    24
    
obua@16158
    25
    val finalize : graph -> string * typ -> graph (* exception DEFS *)
obua@16158
    26
obua@16158
    27
    val finals : graph -> (typ list) Symtab.table
obua@16108
    28
obua@16108
    29
    (* the first argument should be the smaller graph *)
obua@16113
    30
    val merge : graph -> graph -> graph (* exception CIRCULAR, INFINITE_CHAIN, CLASH *)
obua@16108
    31
obua@16108
    32
end
obua@16108
    33
obua@16108
    34
structure Defs :> DEFS = struct
obua@16108
    35
obua@16108
    36
type tyenv = Type.tyenv
obua@16108
    37
type edgelabel = (int * typ * typ * (typ * string * string) list)
obua@16108
    38
type noderef = string
obua@16108
    39
obua@16108
    40
datatype node = Node of
obua@16108
    41
       string  (* name of constant *)
obua@16108
    42
     * typ  (* most general type of constant *)
obua@16108
    43
     * defnode Symtab.table  (* a table of defnodes, each corresponding to 1 definition of the constant for a particular type, 
obua@16108
    44
                             indexed by axiom name *)
obua@16108
    45
     * backref Symtab.table (* a table of all back references to this node, indexed by node name *)
obua@16158
    46
     * typ list (* a list of all finalized types *)
obua@16108
    47
     
obua@16108
    48
and defnode = Defnode of
obua@16108
    49
       typ  (* type of the constant in this particular definition *)
obua@16108
    50
     * ((noderef * (string option * edgelabel list) list) Symtab.table) (* The edges, grouped by nodes. *)
obua@16108
    51
obua@16108
    52
and backref = Backref of
obua@16158
    53
       noderef  (* the name of the node that has defnodes which reference a certain node A *)
obua@16108
    54
     * (unit Symtab.table) (* the names of the defnodes that DIRECTLY reference A. *)
obua@16108
    55
obua@16108
    56
fun getnode graph noderef = the (Symtab.lookup (graph, noderef))
obua@16158
    57
fun get_nodename (Node (n, _, _ ,_, _)) = n
obua@16158
    58
fun get_nodedefs (Node (_, _, defs, _, _)) = defs
obua@16158
    59
fun get_defnode (Node (_, _, defs, _, _)) defname = Symtab.lookup (defs, defname)
obua@16108
    60
fun get_defnode' graph noderef defname = Symtab.lookup (get_nodedefs (the (Symtab.lookup (graph, noderef))), defname)
obua@16158
    61
fun get_nodename (Node (n, _, _ , _, _)) = n
obua@16108
    62
obua@16158
    63
datatype graphaction = Declare of string * typ 
obua@16158
    64
		     | Define of string * typ * string * (string * typ) list
obua@16158
    65
		     | Finalize of string * typ
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@16113
    73
exception INFINITE_CHAIN of (typ * string * string) list;
obua@16108
    74
exception CLASH of string * string * string;
obua@16158
    75
exception FINAL of string * typ;
obua@16108
    76
obua@16108
    77
fun def_err s = raise (DEFS s)
obua@16108
    78
obua@16158
    79
fun declare (actions, g) (cty as (name, ty)) =
obua@16158
    80
    ((Declare cty)::actions, 
obua@16158
    81
     Symtab.update_new ((name, Node (name, Type.varifyT(Type.strip_sorts ty), Symtab.empty, Symtab.empty, [])), g))
obua@16158
    82
    handle Symtab.DUP _ => def_err "constant is already declared"
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@16158
   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@16158
   227
	val (Node (n, gty, defs, backs, finals)) = 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@16158
   234
	     else true)	
obua@16108
   235
	val _ = forall_table check_def defs		
obua@16158
   236
	fun check_final finalty = 
obua@16158
   237
	    (if can_be_unified_r finalty ty then
obua@16158
   238
		 raise (FINAL (mainref, finalty))
obua@16158
   239
	     else
obua@16158
   240
		 true)
obua@16158
   241
	val _ = forall check_final finals
obua@16158
   242
	
obua@16108
   243
	(* now we know that the only thing that can prevent acceptance of the definition is a cyclic dependency *)
obua@16108
   244
obua@16108
   245
	(* body contains the constants that this constant definition depends on. For each element of body,
obua@16108
   246
           the function make_edges_to calculates a group of edges that connect this constant with 
obua@16108
   247
           the constant that is denoted by the element of the body *)
obua@16108
   248
	fun make_edges_to (bodyn, bodyty) =
obua@16108
   249
	    let
obua@16108
   250
		val bnode = 
obua@16108
   251
		    (case Symtab.lookup (graph, bodyn) of 
obua@16108
   252
			 NONE => def_err "body of constant definition references undeclared constant"
obua@16108
   253
		       | SOME x => x)
obua@16158
   254
		val (Node (_, general_btyp, bdefs, bbacks, bfinals)) = bnode
obua@16108
   255
	    in
obua@16108
   256
		case unify_r 0 bodyty general_btyp of
obua@16108
   257
		    NONE => NONE
obua@16108
   258
		  | SOME (maxidx, sigma1, sigma2) => 
obua@16108
   259
		    SOME (
obua@16108
   260
		    let
obua@16108
   261
			(* For each definition of the constant in the body, 
obua@16108
   262
			   check if the definition unifies with the type of the constant in the body. *)	                
obua@16108
   263
	              fun make_edges ((swallowed, l),(def_name, Defnode (def_ty, _))) =
obua@16108
   264
			  if swallowed then
obua@16108
   265
			      (swallowed, l)
obua@16108
   266
			  else 
obua@16108
   267
			      (case unify_r 0 bodyty def_ty of
obua@16108
   268
				   NONE => (swallowed, l)
obua@16108
   269
				 | SOME (maxidx, sigma1, sigma2) => 
obua@16158
   270
				   (is_instance_r bodyty def_ty,
obua@16108
   271
				    merge_labelled_edges l [(SOME def_name,[(maxidx, subst sigma1 ty, subst sigma2 def_ty, [])])]))
obua@16108
   272
          	      val (swallowed, edges) = Symtab.foldl make_edges ((false, []), bdefs)
obua@16108
   273
		    in
obua@16158
   274
			if swallowed orelse (exists (is_instance_r bodyty) bfinals) then 
obua@16108
   275
			    (bodyn, edges)
obua@16158
   276
			else 
obua@16108
   277
			    (bodyn, [(NONE, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])])]@edges)
obua@16108
   278
		    end)
obua@16108
   279
	    end 
obua@16108
   280
obua@16108
   281
	fun update_edges (b as (bodyn, bodyty), edges) =
obua@16108
   282
	    (case make_edges_to b of
obua@16108
   283
		 NONE => edges
obua@16108
   284
	       | SOME m =>
obua@16108
   285
		 (case Symtab.lookup (edges, bodyn) of
obua@16108
   286
		      NONE => Symtab.update ((bodyn, m), edges)
obua@16108
   287
		    | SOME (_, es') => 
obua@16108
   288
		      let 
obua@16108
   289
			  val (_, es) = m
obua@16108
   290
			  val es = merge_labelled_edges es es'
obua@16108
   291
		      in
obua@16108
   292
			  Symtab.update ((bodyn, (bodyn, es)), edges)
obua@16108
   293
		      end
obua@16108
   294
		 )
obua@16108
   295
	    )
obua@16108
   296
obua@16108
   297
	val edges = foldl update_edges Symtab.empty body
obua@16108
   298
obua@16108
   299
	fun insert_edge edges (nodename, (defname_opt, edge)) = 
obua@16108
   300
	    let
obua@16108
   301
		val newlink = [(defname_opt, [edge])]
obua@16108
   302
	    in
obua@16108
   303
		case Symtab.lookup (edges, nodename) of
obua@16108
   304
		    NONE => Symtab.update ((nodename, (nodename, newlink)), edges)		    
obua@16108
   305
		  | SOME (_, links) => 
obua@16108
   306
		    let
obua@16108
   307
			val links' = merge_labelled_edges links newlink
obua@16108
   308
		    in
obua@16108
   309
			Symtab.update ((nodename, (nodename, links')), edges)
obua@16108
   310
		    end
obua@16108
   311
	    end				    
obua@16108
   312
obua@16108
   313
        (* We constructed all direct edges that this defnode has. 
obua@16108
   314
           Now we have to construct the transitive hull by going a single step further. *)
obua@16108
   315
obua@16108
   316
        val thisDefnode = Defnode (ty, edges)
obua@16108
   317
obua@16108
   318
	fun make_trans_edges _ noderef defname_opt (max1, alpha1, beta1, history1) edges = 
obua@16108
   319
	    case defname_opt of 
obua@16108
   320
		NONE => edges
obua@16108
   321
	      | SOME defname => 		
obua@16108
   322
		let
obua@16108
   323
		    val defnode = the (get_defnode' graph noderef defname)
obua@16108
   324
		    fun make_trans_edge _ noderef2 defname_opt2 (max2, alpha2, beta2, history2) edges =
obua@16108
   325
			case unify_r (Int.max (max1, max2)) beta1 alpha2 of
obua@16108
   326
			    NONE => edges
obua@16108
   327
			  | SOME (max, sleft, sright) =>
obua@16108
   328
			    insert_edge edges (noderef2, 
obua@16108
   329
					       (defname_opt2, 							  
obua@16108
   330
						(max, subst sleft alpha1, subst sright beta2, 
obua@16108
   331
						 (subst_history sleft history1)@
obua@16108
   332
						 ((subst sleft beta1, noderef, defname)::
obua@16108
   333
						  (subst_history sright history2)))))
obua@16108
   334
		in
obua@16108
   335
		    defnode_edges_foldl make_trans_edge edges defnode
obua@16108
   336
		end
obua@16108
   337
obua@16108
   338
	val edges = defnode_edges_foldl make_trans_edges edges thisDefnode
obua@16108
   339
obua@16108
   340
	val thisDefnode = Defnode (ty, edges)
obua@16108
   341
obua@16108
   342
	(* We also have to add the backreferences that this new defnode induces. *)
obua@16108
   343
	    
obua@16108
   344
	fun hasNONElink ((NONE, _)::_) = true
obua@16108
   345
	  | hasNONElink _ = false
obua@16108
   346
	
obua@16108
   347
	fun install_backref graph noderef pointingnoderef pointingdefname = 
obua@16108
   348
	    let
obua@16158
   349
		val (Node (pname, _, _, _, _)) = getnode graph pointingnoderef
obua@16158
   350
		val (Node (name, ty, defs, backs, finals)) = getnode graph noderef
obua@16108
   351
	    in
obua@16108
   352
		case Symtab.lookup (backs, pname) of
obua@16108
   353
		    NONE => 
obua@16108
   354
		    let 
obua@16108
   355
			val defnames = Symtab.update ((pointingdefname, ()), Symtab.empty)
obua@16108
   356
			val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs)
obua@16108
   357
		    in
obua@16158
   358
			Symtab.update ((name, Node (name, ty, defs, backs, finals)), graph) 			
obua@16108
   359
		    end
obua@16108
   360
		  | SOME (Backref (pointingnoderef, defnames)) =>
obua@16108
   361
		    let
obua@16108
   362
			val defnames = Symtab.update_new ((pointingdefname, ()), defnames)
obua@16108
   363
			val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs)
obua@16108
   364
		    in
obua@16158
   365
			Symtab.update ((name, Node (name, ty, defs, backs, finals)), graph)
obua@16108
   366
		    end
obua@16108
   367
		    handle Symtab.DUP _ => graph
obua@16108
   368
	    end
obua@16108
   369
obua@16108
   370
	fun install_backrefs (graph, (_, (noderef, labelled_edges))) =
obua@16108
   371
	    if hasNONElink labelled_edges then
obua@16108
   372
		install_backref graph noderef mainref axname
obua@16108
   373
	    else 
obua@16108
   374
		graph
obua@16108
   375
obua@16108
   376
        val graph = Symtab.foldl install_backrefs (graph, edges)
obua@16108
   377
obua@16158
   378
        val (Node (_, _, _, backs, _)) = getnode graph mainref
obua@16158
   379
	val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update_new 
obua@16158
   380
          ((axname, thisDefnode), defs), backs, finals)), graph)
obua@16108
   381
		    
obua@16108
   382
	(* Now we have to check all backreferences to this node and inform them about the new defnode. 
obua@16108
   383
	   In this section we also check for circularity. *)
obua@16108
   384
        fun update_backrefs ((backs, newedges), (nodename, Backref (noderef, defnames))) =	    
obua@16108
   385
	    let
obua@16108
   386
		val node = getnode graph noderef
obua@16108
   387
		fun update_defs ((defnames, newedges),(defname, _)) =
obua@16108
   388
		    let
obua@16108
   389
			val (Defnode (_, defnode_edges)) = the (get_defnode node defname)
obua@16108
   390
			val (_, labelled_edges) = the (Symtab.lookup (defnode_edges, n))
obua@16108
   391
						      
obua@16108
   392
			(* the type of thisDefnode is ty *)
obua@16108
   393
			fun update (e as (max, alpha, beta, history), (none_edges, this_edges)) = 
obua@16108
   394
			    case unify_r max beta ty of
obua@16108
   395
				NONE => (e::none_edges, this_edges)
obua@16108
   396
			      | SOME (max', s_beta, s_ty) =>
obua@16108
   397
				let
obua@16108
   398
				    val alpha' = subst s_beta alpha
obua@16108
   399
				    val ty' = subst s_ty ty				      
obua@16108
   400
				    val _ = 
obua@16108
   401
					if noderef = mainref andalso defname = axname then
obua@16108
   402
					    (case unify alpha' ty' of
obua@16113
   403
						 NONE => 
obua@16113
   404
						   if (is_instance_r ty' alpha') then
obua@16113
   405
						       raise (INFINITE_CHAIN (
obua@16113
   406
							      (alpha', mainref, axname)::
obua@16113
   407
							      (subst_history s_beta history)@
obua@16113
   408
							      [(ty', mainref, axname)]))
obua@16113
   409
						   else ()
obua@16108
   410
					       | SOME s => raise (CIRCULAR (
obua@16108
   411
								  (subst s alpha', mainref, axname)::
obua@16108
   412
								  (subst_history s (subst_history s_beta history))@
obua@16108
   413
								  [(subst s ty', mainref, axname)])))
obua@16108
   414
					else ()
obua@16108
   415
				    val edge = (max', alpha', ty', subst_history s_beta history)
obua@16108
   416
				in
obua@16108
   417
				    if is_instance_r beta ty then 
obua@16108
   418
					(none_edges, edge::this_edges)
obua@16108
   419
				    else
obua@16108
   420
					(e::none_edges, edge::this_edges)
obua@16108
   421
				end					    			   			    
obua@16108
   422
		    in
obua@16108
   423
			case labelled_edges of 
obua@16108
   424
			    ((NONE, edges)::_) => 
obua@16108
   425
			    let
obua@16108
   426
				val (none_edges, this_edges) = foldl update ([], []) edges
obua@16108
   427
				val defnames = if none_edges = [] then defnames else Symtab.update_new ((defname, ()), defnames) 
obua@16108
   428
			    in
obua@16108
   429
				(defnames, (defname, none_edges, this_edges)::newedges)
obua@16108
   430
			    end			    
obua@16158
   431
			  | _ => sys_error "define: update_defs, internal error, corrupt backrefs"
obua@16108
   432
		    end
obua@16108
   433
		    
obua@16108
   434
		val (defnames, newedges') = Symtab.foldl update_defs ((Symtab.empty, []), defnames)
obua@16108
   435
	    in
obua@16108
   436
		if Symtab.is_empty defnames then 
obua@16108
   437
		    (backs, (noderef, newedges')::newedges)
obua@16108
   438
		else
obua@16108
   439
		    let
obua@16108
   440
			val backs = Symtab.update_new ((nodename, Backref (noderef, defnames)), backs)
obua@16108
   441
		    in
obua@16108
   442
			(backs, newedges)
obua@16108
   443
		    end
obua@16108
   444
	    end
obua@16108
   445
	    
obua@16108
   446
obua@16108
   447
	val (backs, newedges) = Symtab.foldl update_backrefs ((Symtab.empty, []), backs)
obua@16108
   448
						 
obua@16108
   449
	(* If a Circular exception is thrown then we never reach this point. *)
obua@16108
   450
        (* Ok, the definition is consistent, let's update this node. *)
obua@16158
   451
	val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update 
obua@16158
   452
	  ((axname, thisDefnode), defs), backs, finals)), graph)
obua@16108
   453
obua@16108
   454
        (* Furthermore, update all the other nodes that backreference this node. *)
obua@16108
   455
        fun final_update_backrefs graph noderef defname none_edges this_edges =
obua@16108
   456
	    let
obua@16108
   457
		val node = getnode graph noderef
obua@16158
   458
		val (Node (nodename, nodety, defs, backs, finals)) = node
obua@16108
   459
		val (Defnode (defnode_ty, defnode_edges)) = the (get_defnode node defname)
obua@16108
   460
		val (_, defnode_links) = the (Symtab.lookup (defnode_edges, n))
obua@16108
   461
obua@16108
   462
		fun update edges none_edges this_edges =
obua@16108
   463
		    let 
obua@16108
   464
			val u = merge_labelled_edges edges [(SOME axname, pack_edges this_edges)]
obua@16108
   465
		    in
obua@16108
   466
			if none_edges = [] then
obua@16108
   467
			    u
obua@16108
   468
			else
obua@16108
   469
			    (NONE, pack_edges none_edges)::u
obua@16108
   470
		    end
obua@16108
   471
		    
obua@16108
   472
		val defnode_links' = 
obua@16108
   473
		    case defnode_links of 
obua@16108
   474
			((NONE, _) :: edges) => update edges none_edges this_edges
obua@16108
   475
		      | edges => update edges none_edges this_edges
obua@16108
   476
		val defnode_edges' = Symtab.update ((n, (mainref, defnode_links')), defnode_edges)
obua@16108
   477
		val defs' = Symtab.update ((defname, Defnode (defnode_ty, defnode_edges')), defs)
obua@16108
   478
	    in
obua@16158
   479
		Symtab.update ((nodename, Node (nodename, nodety, defs', backs, finals)), graph)
obua@16108
   480
	    end
obua@16108
   481
obua@16108
   482
	val graph = foldl (fn ((noderef, newedges),graph) => foldl (fn ((defname, none_edges, this_edges), graph) =>
obua@16108
   483
           final_update_backrefs graph noderef defname none_edges this_edges) graph newedges) graph newedges		    
obua@16108
   484
obua@16108
   485
    in	    
obua@16108
   486
	((Define (name, ty, axname, body))::actions, graph)	   
obua@16108
   487
    end 
obua@16108
   488
obua@16158
   489
    fun finalize' ((c, ty), graph) = 
obua@16158
   490
      case Symtab.lookup (graph, c) of 
obua@16158
   491
	  NONE => def_err ("finalize: constant "^(quote c)^" is not declared")
obua@16158
   492
	| SOME (Node (noderef, nodety, defs, backs, finals)) =>
obua@16158
   493
	  let 
obua@16158
   494
	      val nodety = checkT nodety 
obua@16158
   495
	  in
obua@16158
   496
	      if (not (is_instance_r ty nodety)) then
obua@16158
   497
		  def_err ("finalize: only type instances of the declared constant "^(quote c)^" can be finalized")
obua@16158
   498
	      else if exists (is_instance_r ty) finals then
obua@16158
   499
		  graph
obua@16158
   500
	      else 
obua@16158
   501
	      let
obua@16158
   502
	          val finals = ty :: finals
obua@16158
   503
		  val graph = Symtab.update ((noderef, Node(noderef, nodety, defs, backs, finals)), graph)
obua@16158
   504
		  fun update_backref ((graph, backs), (backrefname, Backref (_, backdefnames))) =
obua@16158
   505
		  let
obua@16158
   506
		      fun update_backdef ((graph, defnames), (backdefname, _)) = 
obua@16158
   507
	              let 
obua@16158
   508
			  val (backnode as Node (_, backty, backdefs, backbacks, backfinals)) = getnode graph backrefname
obua@16158
   509
			  val (Defnode (def_ty, all_edges)) = the (get_defnode backnode backdefname)						      
obua@16158
   510
			  val (defnames', all_edges') = 
obua@16158
   511
			      case Symtab.lookup (all_edges, noderef) of
obua@16158
   512
				  NONE => sys_error "finalize: corrupt backref"
obua@16158
   513
				| SOME (_, (NONE, edges)::rest) =>
obua@16158
   514
				  let
obua@16158
   515
				      val edges' = List.filter (fn (_, _, beta, _) => not (is_instance_r beta ty)) edges
obua@16158
   516
				  in
obua@16158
   517
				      if edges' = [] then 
obua@16158
   518
					  (defnames, Symtab.update ((noderef, (noderef, rest)), all_edges))
obua@16158
   519
				      else
obua@16158
   520
					  (Symtab.update ((backdefname, ()), defnames), 
obua@16158
   521
					   Symtab.update ((noderef, (noderef, (NONE, edges')::rest)), all_edges))
obua@16158
   522
				  end
obua@16158
   523
			  val defnode' = Defnode (def_ty, all_edges')
obua@16158
   524
			  val backnode' = Node (backrefname, backty, Symtab.update ((backdefname, defnode'), backdefs), 
obua@16158
   525
					   backbacks, backfinals)
obua@16158
   526
		      in
obua@16158
   527
			  (Symtab.update ((backrefname, backnode'), graph), defnames')			  			  
obua@16158
   528
		      end
obua@16158
   529
	  
obua@16158
   530
		      val (graph', defnames') = Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames)
obua@16158
   531
		  in
obua@16158
   532
		      (graph', if Symtab.is_empty defnames' then backs 
obua@16158
   533
			       else Symtab.update ((backrefname, Backref (backrefname, defnames')), backs))
obua@16158
   534
		  end
obua@16158
   535
		  val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs)
obua@16158
   536
		  val Node (_, _, defs, _, _) = getnode graph' noderef
obua@16158
   537
	      in
obua@16158
   538
		  Symtab.update ((noderef, Node (noderef, nodety, defs, backs', finals)), graph')
obua@16158
   539
	      end
obua@16158
   540
	  end
obua@16158
   541
	   
obua@16158
   542
    fun finalize (history, graph) c_ty = ((Finalize c_ty)::history, finalize' (c_ty, graph))
obua@16108
   543
    
obua@16158
   544
    fun merge' (Declare cty, g) = (declare g cty handle _ => g)
obua@16108
   545
      | merge' (Define (name, ty, axname, body), g as (_, graph)) = 
obua@16108
   546
	(case Symtab.lookup (graph, name) of
obua@16158
   547
	     NONE => define g (name, ty) axname body
obua@16158
   548
	   | SOME (Node (_, _, defs, _, _)) => 
obua@16108
   549
	     (case Symtab.lookup (defs, axname) of
obua@16158
   550
		  NONE => define g (name, ty) axname body
obua@16108
   551
		| SOME _ => g))
obua@16158
   552
      | merge' (Finalize finals, g) = (finalize g finals handle _ => g)
obua@16108
   553
	
obua@16108
   554
    fun merge (actions, _) g = foldr merge' g actions
obua@16108
   555
obua@16158
   556
    fun finals (history, graph) = 
obua@16158
   557
	Symtab.foldl 
obua@16158
   558
	    (fn (finals, (_, Node(name, _, _, _, ftys))) => Symtab.update_new ((name, ftys), finals))  
obua@16158
   559
	    (Symtab.empty, graph)
obua@16158
   560
obua@16108
   561
end;
obua@16108
   562
		
obua@16108
   563
obua@16108
   564
obua@16108
   565
(*fun tvar name = TVar ((name, 0), [])
obua@16108
   566
obua@16108
   567
val bool = Type ("bool", [])
obua@16108
   568
val int = Type ("int", [])
obua@16108
   569
val alpha = tvar "'a"
obua@16108
   570
val beta = tvar "'b"
obua@16108
   571
val gamma = tvar "'c"
obua@16108
   572
fun pair a b = Type ("pair", [a,b])
obua@16108
   573
obua@16108
   574
val _ = print "make empty"
obua@16108
   575
val g = Defs.empty 
obua@16108
   576
obua@16108
   577
val _ = print "declare"
obua@16108
   578
val g = Defs.declare g "M" (alpha --> bool)
obua@16108
   579
val g = Defs.declare g "N" (beta --> bool)
obua@16108
   580
obua@16108
   581
val _ = print "define"
obua@16108
   582
val g = Defs.define g "N" (alpha --> bool) "defN" [("M", alpha --> bool)]
obua@16108
   583
val g = Defs.define g "M" (alpha --> bool) "defM" [("N", int --> alpha)]
obua@16108
   584
obua@16108
   585
val g = Defs.declare g "0" alpha
obua@16108
   586
val g = Defs.define g "0" (pair alpha beta) "zp" [("0", alpha), ("0", beta)]*)
obua@16108
   587
obua@16108
   588