src/Pure/defs.ML
author obua
Fri Jun 03 01:08:07 2005 +0200 (2005-06-03)
changeset 16198 cfd070a2cc4d
parent 16177 1af9f5c69745
child 16308 636a1a84977a
permissions -rw-r--r--
Integrates cycle detection in definitions with finalconsts
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@16198
    12
  type graph
obua@16198
    13
       
obua@16198
    14
  exception DEFS of string
obua@16198
    15
  exception CIRCULAR of (typ * string * string) list
obua@16198
    16
  exception INFINITE_CHAIN of (typ * string * string) list 
obua@16198
    17
  exception FINAL of string * typ
obua@16198
    18
  exception CLASH of string * string * string
obua@16198
    19
                     
obua@16198
    20
  val empty : graph
obua@16198
    21
  val declare : graph -> string * typ -> graph  (* exception DEFS *)
obua@16198
    22
  val define : graph -> string * typ -> string -> (string * typ) list -> graph 
obua@16198
    23
    (* exception DEFS, CIRCULAR, INFINITE_CHAIN, CLASH, FINAL *)
obua@16198
    24
                                                                         
obua@16198
    25
  val finalize : graph -> string * typ -> graph (* exception DEFS *)
obua@16108
    26
obua@16198
    27
  val finals : graph -> (typ list) Symtab.table
obua@16158
    28
obua@16198
    29
  (* the first argument should be the smaller graph *)
obua@16198
    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@16198
    41
         string  (* name of constant *)
obua@16198
    42
         * typ  (* most general type of constant *)
obua@16198
    43
         * defnode Symtab.table  (* a table of defnodes, each corresponding to 1 definition of the 
obua@16198
    44
             constant for a particular type, indexed by axiom name *)
obua@16198
    45
         * backref Symtab.table (* a table of all back references to this node, indexed by node name *)
obua@16198
    46
         * typ list (* a list of all finalized types *)
obua@16108
    47
     
obua@16198
    48
     and defnode = Defnode of
obua@16198
    49
         typ  (* type of the constant in this particular definition *)
obua@16198
    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@16198
    53
    noderef  (* the name of the node that has defnodes which reference a certain node A *)
obua@16198
    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@16198
    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@16198
    88
      let
obua@16198
    89
	val tv = typ_tvars t
obua@16198
    90
	val t' = incr_tvar inc t
obua@16198
    91
	fun update_subst (((n,i), _), s) =
obua@16198
    92
	    Vartab.update (((n, i), ([], TVar ((n, i+inc), []))), s)
obua@16198
    93
      in
obua@16198
    94
	(t',List.foldl update_subst Vartab.empty tv)
obua@16198
    95
      end	
obua@16108
    96
    else
obua@16198
    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@16198
   103
      val max2 = (maxidx_of_typ ty2)
obua@16198
   104
      val (ty2', s) = subst_incr_tvar (max1 + 1) ty2                
obua@16108
   105
    in
obua@16198
   106
      (ty2', s, max1 + max2 + 1)
obua@16108
   107
    end	       
obua@16198
   108
    
obua@16108
   109
fun subst s ty = Envir.norm_type s ty
obua@16198
   110
                 
obua@16108
   111
fun subst_history s history = map (fn (ty, cn, dn) => (subst s ty, cn, dn)) history
obua@16198
   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@16198
   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@16198
   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@16198
   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@16198
   131
      val max =  Int.max(max, 0)
obua@16198
   132
      val max1 = max (* >= maxidx_of_typ ty1 *)
obua@16198
   133
      val max2 = max (* >= maxidx_of_typ ty2 *)
obua@16198
   134
      val max = Int.max(max, Int.max (max1, max2))
obua@16198
   135
      val (ty1, s1) = subst_incr_tvar (max+1) ty1
obua@16198
   136
      val (ty2, s2) = subst_incr_tvar (max+max1+2) ty2
obua@16198
   137
      val max = max+max1+max2+2	
obua@16198
   138
      fun merge a b = Vartab.merge (fn _ => false) (a, b)
obua@16108
   139
    in
obua@16198
   140
      case unify ty1 ty2 of
obua@16198
   141
	NONE => NONE
obua@16198
   142
      | SOME s => SOME (max, merge s1 s, merge s2 s)
obua@16108
   143
    end
obua@16198
   144
    
obua@16108
   145
fun can_be_unified_r ty1 ty2 =
obua@16108
   146
    let
obua@16198
   147
      val ty2 = rename ty1 ty2
obua@16108
   148
    in
obua@16198
   149
      case unify ty1 ty2 of
obua@16198
   150
	NONE => false
obua@16198
   151
      | _ => true
obua@16108
   152
    end
obua@16198
   153
    
obua@16108
   154
fun can_be_unified ty1 ty2 =
obua@16108
   155
    case unify ty1 ty2 of
obua@16198
   156
      NONE => false
obua@16198
   157
    | _ => true
obua@16198
   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 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@16198
   171
      val t1 = u1 --> v1
obua@16198
   172
      val t2 = u2 --> v2
obua@16108
   173
    in
obua@16198
   174
      if (is_instance_r t1 t2) then
obua@16198
   175
	(if is_instance_r t2 t1 then
obua@16198
   176
	   SOME (int_ord (length history2, length history1))
obua@16198
   177
	 else
obua@16198
   178
	   SOME LESS)
obua@16198
   179
      else if (is_instance_r t2 t1) then
obua@16198
   180
	SOME GREATER
obua@16198
   181
      else
obua@16198
   182
	NONE
obua@16108
   183
    end
obua@16198
   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@16198
   188
       SOME LESS => (y::ys)
obua@16198
   189
     | SOME EQUAL => (y::ys)
obua@16198
   190
     | SOME GREATER => merge_edges_1 (x, ys)
obua@16198
   191
     | NONE => y::(merge_edges_1 (x, ys)))
obua@16198
   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@16198
   201
       LESS => (l1, e1)::(merge_labelled_edges es1 ((l2, e2)::es2))
obua@16198
   202
     | GREATER => (l2, e2)::(merge_labelled_edges ((l1, e1)::es1) es2)
obua@16198
   203
     | EQUAL => (l1, merge_edges e1 e2)::(merge_labelled_edges es1 es2))
obua@16198
   204
    
obua@16108
   205
fun defnode_edges_foldl f a defnode =
obua@16108
   206
    let
obua@16198
   207
      val (Defnode (ty, def_edges)) = defnode
obua@16198
   208
      fun g (b, (_, (n, labelled_edges))) =
obua@16198
   209
	  foldl (fn ((s, edges), b') => 
obua@16198
   210
		    (foldl (fn (e, b'') => f ty n s e b'') b' edges))
obua@16198
   211
		b
obua@16198
   212
		labelled_edges		  		     
obua@16108
   213
    in
obua@16198
   214
      Symtab.foldl g (a, def_edges)
obua@16108
   215
    end	
obua@16198
   216
    
obua@16158
   217
fun define (actions, graph) (name, ty) axname body =
obua@16108
   218
    let
obua@16198
   219
      val ty = checkT ty
obua@16198
   220
      val body = map (fn (n,t) => (n, checkT t)) body		 
obua@16198
   221
      val mainref = name
obua@16198
   222
      val mainnode  = (case Symtab.lookup (graph, mainref) of 
obua@16198
   223
			 NONE => def_err ("constant "^mainref^" is not declared")
obua@16198
   224
		       | SOME n => n)
obua@16198
   225
      val (Node (n, gty, defs, backs, finals)) = mainnode
obua@16198
   226
      val _ = (if is_instance_r ty gty then () else def_err "type of constant does not match declared type")
obua@16198
   227
      fun check_def (s, Defnode (ty', _)) = 
obua@16198
   228
	  (if can_be_unified_r ty ty' then 
obua@16198
   229
	     raise (CLASH (mainref, axname, s))
obua@16198
   230
	   else if s = axname then
obua@16198
   231
	     def_err "name of axiom is already used for another definition of this constant"
obua@16198
   232
	   else false)	
obua@16198
   233
      val _ = Symtab.exists check_def defs
obua@16198
   234
      fun check_final finalty = 
obua@16198
   235
	  (if can_be_unified_r finalty ty then
obua@16198
   236
	     raise (FINAL (mainref, finalty))
obua@16198
   237
	   else
obua@16198
   238
	     true)
obua@16198
   239
      val _ = forall check_final finals
obua@16198
   240
	             
obua@16198
   241
      (* now we know that the only thing that can prevent acceptance of the definition is a cyclic dependency *)
obua@16108
   242
obua@16198
   243
      (* body contains the constants that this constant definition depends on. For each element of body,
obua@16198
   244
         the function make_edges_to calculates a group of edges that connect this constant with 
obua@16198
   245
         the constant that is denoted by the element of the body *)
obua@16198
   246
      fun make_edges_to (bodyn, bodyty) =
obua@16198
   247
	  let
obua@16198
   248
	    val bnode = 
obua@16198
   249
		(case Symtab.lookup (graph, bodyn) of 
obua@16198
   250
		   NONE => def_err "body of constant definition references undeclared constant"
obua@16198
   251
		 | SOME x => x)
obua@16198
   252
	    val (Node (_, general_btyp, bdefs, bbacks, bfinals)) = bnode
obua@16198
   253
	  in
obua@16198
   254
	    case unify_r 0 bodyty general_btyp of
obua@16198
   255
	      NONE => NONE
obua@16198
   256
	    | SOME (maxidx, sigma1, sigma2) => 
obua@16198
   257
	      SOME (
obua@16198
   258
	      let
obua@16198
   259
		(* For each definition of the constant in the body, 
obua@16198
   260
		   check if the definition unifies with the type of the constant in the body. *)	                
obua@16198
   261
                fun make_edges ((swallowed, l),(def_name, Defnode (def_ty, _))) =
obua@16198
   262
		    if swallowed then
obua@16198
   263
		      (swallowed, l)
obua@16198
   264
		    else 
obua@16198
   265
		      (case unify_r 0 bodyty def_ty of
obua@16198
   266
			 NONE => (swallowed, l)
obua@16198
   267
		       | SOME (maxidx, sigma1, sigma2) => 
obua@16198
   268
			 (is_instance_r bodyty def_ty,
obua@16198
   269
			  merge_labelled_edges l [(SOME def_name,[(maxidx, subst sigma1 ty, subst sigma2 def_ty, [])])]))
obua@16198
   270
                val swallowed = exists (is_instance_r bodyty) bfinals
obua@16198
   271
          	val (swallowed, edges) = Symtab.foldl make_edges ((swallowed, []), bdefs)
obua@16198
   272
	      in
obua@16198
   273
		if swallowed then 
obua@16198
   274
		  (bodyn, edges)
obua@16198
   275
		else 
obua@16198
   276
		  (bodyn, [(NONE, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])])]@edges)
obua@16198
   277
	      end)
obua@16198
   278
	  end 
obua@16198
   279
          
obua@16198
   280
      fun update_edges (b as (bodyn, bodyty), edges) =
obua@16198
   281
	  (case make_edges_to b of
obua@16198
   282
	     NONE => edges
obua@16198
   283
	   | SOME m =>
obua@16198
   284
	     (case Symtab.lookup (edges, bodyn) of
obua@16198
   285
		NONE => Symtab.update ((bodyn, m), edges)
obua@16198
   286
	      | SOME (_, es') => 
obua@16198
   287
		let 
obua@16198
   288
		  val (_, es) = m
obua@16198
   289
		  val es = merge_labelled_edges es es'
obua@16198
   290
		in
obua@16198
   291
		  Symtab.update ((bodyn, (bodyn, es)), edges)
obua@16198
   292
		end
obua@16198
   293
	     )
obua@16198
   294
	  )
obua@16198
   295
          
obua@16198
   296
      val edges = foldl update_edges Symtab.empty body
obua@16198
   297
                  
obua@16198
   298
      fun insert_edge edges (nodename, (defname_opt, edge)) = 
obua@16198
   299
	  let
obua@16198
   300
	    val newlink = [(defname_opt, [edge])]
obua@16198
   301
	  in
obua@16198
   302
	    case Symtab.lookup (edges, nodename) of
obua@16198
   303
	      NONE => Symtab.update ((nodename, (nodename, newlink)), edges)		    
obua@16198
   304
	    | SOME (_, links) => 
obua@16198
   305
	      let
obua@16198
   306
		val links' = merge_labelled_edges links newlink
obua@16198
   307
	      in
obua@16198
   308
		Symtab.update ((nodename, (nodename, links')), edges)
obua@16198
   309
	      end
obua@16198
   310
	  end				    
obua@16198
   311
            
obua@16198
   312
      (* We constructed all direct edges that this defnode has. 
obua@16198
   313
         Now we have to construct the transitive hull by going a single step further. *)
obua@16198
   314
          
obua@16198
   315
      val thisDefnode = Defnode (ty, edges)
obua@16198
   316
                        
obua@16198
   317
      fun make_trans_edges _ noderef defname_opt (max1, alpha1, beta1, history1) edges = 
obua@16198
   318
	  case defname_opt of 
obua@16198
   319
	    NONE => edges
obua@16198
   320
	  | SOME defname => 		
obua@16108
   321
	    let
obua@16198
   322
	      val defnode = the (get_defnode' graph noderef defname)
obua@16198
   323
	      fun make_trans_edge _ noderef2 defname_opt2 (max2, alpha2, beta2, history2) edges =
obua@16198
   324
		  case unify_r (Int.max (max1, max2)) beta1 alpha2 of
obua@16198
   325
		    NONE => edges
obua@16198
   326
		  | SOME (max, sleft, sright) =>
obua@16198
   327
		    insert_edge edges (noderef2, 
obua@16198
   328
				       (defname_opt2, 							  
obua@16198
   329
					(max, subst sleft alpha1, subst sright beta2, 
obua@16198
   330
					 (subst_history sleft history1)@
obua@16198
   331
					 ((subst sleft beta1, noderef, defname)::
obua@16198
   332
					  (subst_history sright history2)))))
obua@16108
   333
	    in
obua@16198
   334
	      defnode_edges_foldl make_trans_edge edges defnode
obua@16198
   335
	    end
obua@16198
   336
            
obua@16198
   337
      val edges = defnode_edges_foldl make_trans_edges edges thisDefnode
obua@16198
   338
                  
obua@16198
   339
      val thisDefnode = Defnode (ty, edges)
obua@16108
   340
obua@16198
   341
      (* We also have to add the backreferences that this new defnode induces. *)
obua@16108
   342
	    
obua@16198
   343
      fun hasNONElink ((NONE, _)::_) = true
obua@16198
   344
	| hasNONElink _ = false
obua@16198
   345
	                  
obua@16198
   346
      fun install_backref graph noderef pointingnoderef pointingdefname = 
obua@16198
   347
	  let
obua@16198
   348
	    val (Node (pname, _, _, _, _)) = getnode graph pointingnoderef
obua@16198
   349
	    val (Node (name, ty, defs, backs, finals)) = getnode graph noderef
obua@16198
   350
	  in
obua@16198
   351
	    case Symtab.lookup (backs, pname) of
obua@16198
   352
	      NONE => 
obua@16198
   353
	      let 
obua@16198
   354
		val defnames = Symtab.update ((pointingdefname, ()), Symtab.empty)
obua@16198
   355
		val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs)
obua@16198
   356
	      in
obua@16198
   357
		Symtab.update ((name, Node (name, ty, defs, backs, finals)), graph) 			
obua@16198
   358
	      end
obua@16198
   359
	    | SOME (Backref (pointingnoderef, defnames)) =>
obua@16198
   360
	      let
obua@16198
   361
		val defnames = Symtab.update_new ((pointingdefname, ()), defnames)
obua@16198
   362
		val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs)
obua@16198
   363
	      in
obua@16198
   364
		Symtab.update ((name, Node (name, ty, defs, backs, finals)), graph)
obua@16198
   365
	      end
obua@16198
   366
	      handle Symtab.DUP _ => graph
obua@16198
   367
	  end
obua@16198
   368
          
obua@16198
   369
      fun install_backrefs (graph, (_, (noderef, labelled_edges))) =
obua@16198
   370
	  if hasNONElink labelled_edges then
obua@16198
   371
	    install_backref graph noderef mainref axname
obua@16198
   372
	  else 
obua@16198
   373
	    graph
obua@16198
   374
            
obua@16198
   375
      val graph = Symtab.foldl install_backrefs (graph, edges)
obua@16198
   376
                  
obua@16198
   377
      val (Node (_, _, _, backs, _)) = getnode graph mainref
obua@16198
   378
      val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update_new 
obua@16198
   379
        ((axname, thisDefnode), defs), backs, finals)), graph)
obua@16198
   380
		                
obua@16198
   381
      (* Now we have to check all backreferences to this node and inform them about the new defnode. 
obua@16198
   382
	 In this section we also check for circularity. *)
obua@16198
   383
      fun update_backrefs ((backs, newedges), (nodename, Backref (noderef, defnames))) =	    
obua@16198
   384
	  let
obua@16198
   385
	    val node = getnode graph noderef
obua@16198
   386
	    fun update_defs ((defnames, newedges),(defname, _)) =
obua@16198
   387
		let
obua@16198
   388
		  val (Defnode (_, defnode_edges)) = the (get_defnode node defname)
obua@16198
   389
		  val (_, labelled_edges) = the (Symtab.lookup (defnode_edges, n))
obua@16198
   390
						
obua@16198
   391
	          (* the type of thisDefnode is ty *)
obua@16198
   392
		  fun update (e as (max, alpha, beta, history), (none_edges, this_edges)) = 
obua@16198
   393
		      case unify_r max beta ty of
obua@16198
   394
			NONE => (e::none_edges, this_edges)
obua@16198
   395
		      | SOME (max', s_beta, s_ty) =>
obua@16198
   396
			let
obua@16198
   397
			  val alpha' = subst s_beta alpha
obua@16198
   398
			  val ty' = subst s_ty ty				      
obua@16198
   399
			  val _ = 
obua@16198
   400
			      if noderef = mainref andalso defname = axname then
obua@16198
   401
				(case unify alpha' ty' of
obua@16198
   402
				   NONE => 
obua@16198
   403
				   if (is_instance_r ty' alpha') then
obua@16198
   404
				     raise (INFINITE_CHAIN (
obua@16198
   405
					    (alpha', mainref, axname)::
obua@16198
   406
					    (subst_history s_beta history)@
obua@16198
   407
					    [(ty', mainref, axname)]))
obua@16198
   408
				   else ()
obua@16198
   409
				 | SOME s => raise (CIRCULAR (
obua@16198
   410
						    (subst s alpha', mainref, axname)::
obua@16198
   411
						    (subst_history s (subst_history s_beta history))@
obua@16198
   412
						    [(subst s ty', mainref, axname)])))
obua@16198
   413
			      else ()
obua@16198
   414
			  val edge = (max', alpha', ty', subst_history s_beta history)
obua@16198
   415
			in
obua@16198
   416
			  if is_instance_r beta ty then 
obua@16198
   417
			    (none_edges, edge::this_edges)
obua@16198
   418
			  else
obua@16198
   419
			    (e::none_edges, edge::this_edges)
obua@16198
   420
			end					    			   			    
obua@16198
   421
		in
obua@16198
   422
		  case labelled_edges of 
obua@16198
   423
		    ((NONE, edges)::_) => 
obua@16108
   424
		    let
obua@16198
   425
		      val (none_edges, this_edges) = foldl update ([], []) edges
obua@16198
   426
		      val defnames = if none_edges = [] then defnames else Symtab.update_new ((defname, ()), defnames) 
obua@16108
   427
		    in
obua@16198
   428
		      (defnames, (defname, none_edges, this_edges)::newedges)
obua@16198
   429
		    end			    
obua@16198
   430
		  | _ => sys_error "define: update_defs, internal error, corrupt backrefs"
obua@16198
   431
		end
obua@16108
   432
		    
obua@16198
   433
	    val (defnames, newedges') = Symtab.foldl update_defs ((Symtab.empty, []), defnames)
obua@16198
   434
	  in
obua@16198
   435
	    if Symtab.is_empty defnames then 
obua@16198
   436
	      (backs, (noderef, newedges')::newedges)
obua@16198
   437
	    else
obua@16198
   438
	      let
obua@16198
   439
		val backs = Symtab.update_new ((nodename, Backref (noderef, defnames)), backs)
obua@16198
   440
	      in
obua@16198
   441
		(backs, newedges)
obua@16198
   442
	      end
obua@16198
   443
	  end
obua@16198
   444
	  
obua@16108
   445
obua@16198
   446
      val (backs, newedges) = Symtab.foldl update_backrefs ((Symtab.empty, []), backs)
obua@16198
   447
						 
obua@16198
   448
      (* If a Circular exception is thrown then we never reach this point. *)
obua@16198
   449
      (* Ok, the definition is consistent, let's update this node. *)
obua@16198
   450
      val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update 
obua@16198
   451
        ((axname, thisDefnode), defs), backs, finals)), graph)
obua@16108
   452
obua@16198
   453
      (* Furthermore, update all the other nodes that backreference this node. *)
obua@16198
   454
      fun final_update_backrefs graph noderef defname none_edges this_edges =
obua@16198
   455
	  let
obua@16198
   456
	    val node = getnode graph noderef
obua@16198
   457
	    val (Node (nodename, nodety, defs, backs, finals)) = node
obua@16198
   458
	    val (Defnode (defnode_ty, defnode_edges)) = the (get_defnode node defname)
obua@16198
   459
	    val (_, defnode_links) = the (Symtab.lookup (defnode_edges, n))
obua@16198
   460
                                     
obua@16198
   461
	    fun update edges none_edges this_edges =
obua@16198
   462
		let 
obua@16198
   463
		  val u = merge_labelled_edges edges [(SOME axname, pack_edges this_edges)]
obua@16198
   464
		in
obua@16198
   465
		  if none_edges = [] then
obua@16198
   466
		    u
obua@16198
   467
		  else
obua@16198
   468
		    (NONE, pack_edges none_edges)::u
obua@16198
   469
		end
obua@16198
   470
		
obua@16198
   471
	    val defnode_links' = 
obua@16198
   472
		case defnode_links of 
obua@16198
   473
		  ((NONE, _) :: edges) => update edges none_edges this_edges
obua@16198
   474
		| edges => update edges none_edges this_edges
obua@16198
   475
	    val defnode_edges' = Symtab.update ((n, (mainref, defnode_links')), defnode_edges)
obua@16198
   476
	    val defs' = Symtab.update ((defname, Defnode (defnode_ty, defnode_edges')), defs)
obua@16198
   477
	  in
obua@16198
   478
	    Symtab.update ((nodename, Node (nodename, nodety, defs', backs, finals)), graph)
obua@16198
   479
	  end
obua@16198
   480
          
obua@16198
   481
      val graph = foldl (fn ((noderef, newedges),graph) => foldl (fn ((defname, none_edges, this_edges), graph) =>
obua@16198
   482
        final_update_backrefs graph noderef defname none_edges this_edges) graph newedges) graph newedges		    
obua@16198
   483
                  
obua@16108
   484
    in	    
obua@16198
   485
      ((Define (name, ty, axname, body))::actions, graph)	   
obua@16108
   486
    end 
obua@16198
   487
    
obua@16198
   488
fun finalize (history, graph) (c, ty) = 
obua@16198
   489
    case Symtab.lookup (graph, c) of 
obua@16198
   490
      NONE => def_err ("cannot finalize constant "^c^"; it is not declared")
obua@16198
   491
    | SOME (Node (noderef, nodety, defs, backs, finals)) =>
obua@16198
   492
      let 
obua@16198
   493
	val ty = checkT ty
obua@16198
   494
	val _ = if (not (is_instance_r ty nodety)) then
obua@16198
   495
		  def_err ("only type instances of the declared constant "^c^" can be finalized")
obua@16198
   496
		else ()
obua@16198
   497
	val _ = Symtab.exists (fn (def_name, Defnode (def_ty, _)) =>  
obua@16198
   498
				  if can_be_unified_r ty def_ty then 
obua@16198
   499
				    def_err ("cannot finalize constant "^c^"; clash with definition "^def_name)
obua@16198
   500
				  else 
obua@16198
   501
				    false)
obua@16198
   502
			      defs 
obua@16198
   503
        
obua@16198
   504
        fun update_finals [] = SOME [ty]
obua@16198
   505
          | update_finals (final_ty::finals) = 
obua@16198
   506
            (if is_instance_r ty final_ty then NONE
obua@16198
   507
             else
obua@16198
   508
               case update_finals finals of
obua@16198
   509
                 NONE => NONE
obua@16198
   510
               | (r as SOME finals) =>
obua@16198
   511
                 if (is_instance_r final_ty ty) then
obua@16198
   512
                   r
obua@16198
   513
                 else
obua@16198
   514
                   SOME (final_ty :: finals))                              
obua@16198
   515
      in    
obua@16198
   516
        case update_finals finals of
obua@16198
   517
          NONE => (history, graph)
obua@16198
   518
        | SOME finals => 
obua@16198
   519
	  let
obua@16198
   520
	    val graph = Symtab.update ((noderef, Node(noderef, nodety, defs, backs, finals)), graph)
obua@16198
   521
	                
obua@16198
   522
	    fun update_backref ((graph, backs), (backrefname, Backref (_, backdefnames))) =
obua@16198
   523
		let
obua@16198
   524
		  fun update_backdef ((graph, defnames), (backdefname, _)) = 
obua@16158
   525
	              let 
obua@16198
   526
			val (backnode as Node (_, backty, backdefs, backbacks, backfinals)) = getnode graph backrefname
obua@16198
   527
			val (Defnode (def_ty, all_edges)) = the (get_defnode backnode backdefname)						      
obua@16198
   528
			val (defnames', all_edges') = 
obua@16198
   529
			    case Symtab.lookup (all_edges, noderef) of
obua@16198
   530
			      NONE => sys_error "finalize: corrupt backref"
obua@16198
   531
			    | SOME (_, (NONE, edges)::rest) =>
obua@16198
   532
			      let
obua@16198
   533
				val edges' = List.filter (fn (_, _, beta, _) => not (is_instance_r beta ty)) edges
obua@16198
   534
			      in
obua@16198
   535
				if edges' = [] then 
obua@16198
   536
				  (defnames, Symtab.update ((noderef, (noderef, rest)), all_edges))
obua@16198
   537
				else
obua@16198
   538
				  (Symtab.update ((backdefname, ()), defnames), 
obua@16198
   539
				   Symtab.update ((noderef, (noderef, (NONE, edges')::rest)), all_edges))
obua@16198
   540
			      end
obua@16198
   541
			val defnode' = Defnode (def_ty, all_edges')
obua@16198
   542
			val backnode' = Node (backrefname, backty, Symtab.update ((backdefname, defnode'), backdefs), 
obua@16198
   543
					      backbacks, backfinals)
obua@16158
   544
		      in
obua@16198
   545
			(Symtab.update ((backrefname, backnode'), graph), defnames')			  			  
obua@16158
   546
		      end
obua@16198
   547
	              
obua@16198
   548
		  val (graph', defnames') = Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames)
obua@16198
   549
		in
obua@16198
   550
		  (graph', if Symtab.is_empty defnames' then backs 
obua@16198
   551
			   else Symtab.update ((backrefname, Backref (backrefname, defnames')), backs))
obua@16198
   552
		end
obua@16198
   553
	    val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs)
obua@16198
   554
	    val Node (_, _, defs, _, _) = getnode graph' noderef
obua@16198
   555
	  in
obua@16198
   556
	    ((Finalize (c, ty)) :: history, Symtab.update ((noderef, Node (noderef, nodety, defs, backs', finals)), graph'))
obua@16158
   557
	  end
obua@16198
   558
      end
obua@16198
   559
      
obua@16198
   560
fun merge' (Declare cty, g) = (declare g cty handle _ => g)
obua@16198
   561
  | merge' (Define (name, ty, axname, body), g as (_, graph)) = 
obua@16198
   562
    (case Symtab.lookup (graph, name) of
obua@16198
   563
       NONE => define g (name, ty) axname body
obua@16198
   564
     | SOME (Node (_, _, defs, _, _)) => 
obua@16198
   565
       (case Symtab.lookup (defs, axname) of
obua@16198
   566
	  NONE => define g (name, ty) axname body
obua@16198
   567
	| SOME _ => g))
obua@16198
   568
  | merge' (Finalize finals, g) = finalize g finals 
obua@16198
   569
                       
obua@16198
   570
fun merge (actions, _) g = foldr merge' g actions
obua@16198
   571
                           
obua@16198
   572
fun finals (history, graph) = 
obua@16198
   573
    Symtab.foldl 
obua@16198
   574
      (fn (finals, (_, Node(name, _, _, _, ftys))) => Symtab.update_new ((name, ftys), finals))  
obua@16198
   575
      (Symtab.empty, graph)
obua@16158
   576
obua@16108
   577
end;
obua@16108
   578
		
obua@16108
   579
obua@16108
   580
obua@16108
   581
(*fun tvar name = TVar ((name, 0), [])
obua@16108
   582
obua@16108
   583
val bool = Type ("bool", [])
obua@16108
   584
val int = Type ("int", [])
obua@16108
   585
val alpha = tvar "'a"
obua@16108
   586
val beta = tvar "'b"
obua@16108
   587
val gamma = tvar "'c"
obua@16108
   588
fun pair a b = Type ("pair", [a,b])
obua@16108
   589
obua@16108
   590
val _ = print "make empty"
obua@16108
   591
val g = Defs.empty 
obua@16108
   592
obua@16108
   593
val _ = print "declare"
obua@16108
   594
val g = Defs.declare g "M" (alpha --> bool)
obua@16108
   595
val g = Defs.declare g "N" (beta --> bool)
obua@16108
   596
obua@16108
   597
val _ = print "define"
obua@16108
   598
val g = Defs.define g "N" (alpha --> bool) "defN" [("M", alpha --> bool)]
obua@16108
   599
val g = Defs.define g "M" (alpha --> bool) "defM" [("N", int --> alpha)]
obua@16108
   600
obua@16108
   601
val g = Defs.declare g "0" alpha
obua@16108
   602
val g = Defs.define g "0" (pair alpha beta) "zp" [("0", alpha), ("0", beta)]*)
obua@16108
   603
obua@16108
   604