1) Fixed bug in Defs.merge_edges_1.
authorobua
Tue Jun 07 06:39:39 2005 +0200 (2005-06-07)
changeset 16308636a1a84977a
parent 16307 cb0f9e96d456
child 16309 39c793a9b382
1) Fixed bug in Defs.merge_edges_1.
2) Major optimization of Defs.define: do not store dependencies between constants that
cannot introduce cycles anyway. In that way, the cycle test adds almost no overhead to
theories that define their constants in HOL-light / HOL4 style.
3) Cleaned up Defs.graph, no superfluous name tags are stored anymore.
src/Pure/defs.ML
     1.1 --- a/src/Pure/defs.ML	Mon Jun 06 21:21:19 2005 +0200
     1.2 +++ b/src/Pure/defs.ML	Tue Jun 07 06:39:39 2005 +0200
     1.3 @@ -2,9 +2,10 @@
     1.4      ID:         $Id$
     1.5      Author:     Steven Obua, TU Muenchen
     1.6  
     1.7 -    Checks if definitions preserve consistency of logic by enforcing that there are no cyclic definitions.
     1.8 -    The algorithm is described in 
     1.9 -    "Cycle-free Overloading in Isabelle", Steven Obua, technical report, to be written :-)
    1.10 +    Checks if definitions preserve consistency of logic by enforcing 
    1.11 +    that there are no cyclic definitions. The algorithm is described in 
    1.12 +    "An Algorithm for Determining Definitional Cycles in Higher-Order Logic with Overloading", 
    1.13 +    Steven Obua, technical report, to be written :-)
    1.14  *)
    1.15  
    1.16  signature DEFS = sig
    1.17 @@ -20,53 +21,65 @@
    1.18    val empty : graph
    1.19    val declare : graph -> string * typ -> graph  (* exception DEFS *)
    1.20    val define : graph -> string * typ -> string -> (string * typ) list -> graph 
    1.21 -    (* exception DEFS, CIRCULAR, INFINITE_CHAIN, CLASH, FINAL *)
    1.22 -                                                                         
    1.23 +    (* exception DEFS, CIRCULAR, INFINITE_CHAIN, CLASH, FINAL *)   
    1.24 +                                                                     
    1.25    val finalize : graph -> string * typ -> graph (* exception DEFS *)
    1.26  
    1.27    val finals : graph -> (typ list) Symtab.table
    1.28  
    1.29 -  (* the first argument should be the smaller graph *)
    1.30    val merge : graph -> graph -> graph (* exception CIRCULAR, INFINITE_CHAIN, CLASH *)
    1.31  
    1.32 +  (* If set to true then the exceptions CIRCULAR and INFINITE_CHAIN return the full
    1.33 +     chain of definitions that lead to the exception. In the beginning, chain_history 
    1.34 +     is initialized with the Isabelle environment variable DEFS_CHAIN_HISTORY. *)
    1.35 +  val set_chain_history : bool -> unit
    1.36 +  val chain_history : unit -> bool
    1.37 +
    1.38  end
    1.39  
    1.40  structure Defs :> DEFS = struct
    1.41  
    1.42  type tyenv = Type.tyenv
    1.43  type edgelabel = (int * typ * typ * (typ * string * string) list)
    1.44 -type noderef = string
    1.45  
    1.46  datatype node = Node of
    1.47 -         string  (* name of constant *)
    1.48 -         * typ  (* most general type of constant *)
    1.49 -         * defnode Symtab.table  (* a table of defnodes, each corresponding to 1 definition of the 
    1.50 -             constant for a particular type, indexed by axiom name *)
    1.51 -         * backref Symtab.table (* a table of all back references to this node, indexed by node name *)
    1.52 +         typ  (* most general type of constant *)
    1.53 +         * defnode Symtab.table  
    1.54 +             (* a table of defnodes, each corresponding to 1 definition of the 
    1.55 +                constant for a particular type, indexed by axiom name *)
    1.56 +         * (unit Symtab.table) Symtab.table 
    1.57 +             (* a table of all back referencing defnodes to this node, 
    1.58 +                indexed by node name of the defnodes *)
    1.59           * typ list (* a list of all finalized types *)
    1.60       
    1.61       and defnode = Defnode of
    1.62           typ  (* type of the constant in this particular definition *)
    1.63 -         * ((noderef * (string option * edgelabel list) list) Symtab.table) (* The edges, grouped by nodes. *)
    1.64 -
    1.65 -and backref = Backref of
    1.66 -    noderef  (* the name of the node that has defnodes which reference a certain node A *)
    1.67 -    * (unit Symtab.table) (* the names of the defnodes that DIRECTLY reference A. *)
    1.68 +         * (edgelabel list) Symtab.table (* The edges, grouped by nodes. *)
    1.69  
    1.70  fun getnode graph noderef = the (Symtab.lookup (graph, noderef))
    1.71 -fun get_nodename (Node (n, _, _ ,_, _)) = n
    1.72 -fun get_nodedefs (Node (_, _, defs, _, _)) = defs
    1.73 -fun get_defnode (Node (_, _, defs, _, _)) defname = Symtab.lookup (defs, defname)
    1.74 -fun get_defnode' graph noderef defname = Symtab.lookup (get_nodedefs (the (Symtab.lookup (graph, noderef))), defname)
    1.75 -fun get_nodename (Node (n, _, _ , _, _)) = n
    1.76 +fun get_nodedefs (Node (_, defs, _, _)) = defs
    1.77 +fun get_defnode (Node (_, defs, _, _)) defname = Symtab.lookup (defs, defname)
    1.78 +fun get_defnode' graph noderef defname = 
    1.79 +    Symtab.lookup (get_nodedefs (the (Symtab.lookup (graph, noderef))), defname)
    1.80  
    1.81 -datatype graphaction = Declare of string * typ 
    1.82 +datatype graphaction = Declare of string * typ
    1.83  		     | Define of string * typ * string * (string * typ) list
    1.84  		     | Finalize of string * typ
    1.85  
    1.86 -type graph = (graphaction list) * (node Symtab.table)
    1.87 +type graph = int * (graphaction list) * (node Symtab.table)
    1.88               
    1.89 -val empty = ([], Symtab.empty)
    1.90 +val CHAIN_HISTORY = 
    1.91 +    let
    1.92 +      fun f c = if Char.isSpace c then "" else String.str (Char.toUpper c) 
    1.93 +      val env = String.translate f (getenv "DEFS_CHAIN_HISTORY")
    1.94 +    in
    1.95 +      ref (env = "ON" orelse env = "TRUE")
    1.96 +    end
    1.97 +
    1.98 +fun set_chain_history b = CHAIN_HISTORY := b
    1.99 +fun chain_history () = !CHAIN_HISTORY
   1.100 +
   1.101 +val empty = (0, [], Symtab.empty)
   1.102  
   1.103  exception DEFS of string;
   1.104  exception CIRCULAR of (typ * string * string) list;
   1.105 @@ -76,11 +89,18 @@
   1.106  
   1.107  fun def_err s = raise (DEFS s)
   1.108  
   1.109 -fun declare (actions, g) (cty as (name, ty)) =
   1.110 -    ((Declare cty)::actions, 
   1.111 -     Symtab.update_new ((name, Node (name, Type.varifyT(Type.strip_sorts ty), Symtab.empty, Symtab.empty, [])), g))
   1.112 +fun checkT (Type (a, Ts)) = Type (a, map checkT Ts)
   1.113 +  | checkT (TVar ((a, 0), _)) = TVar ((a, 0), [])
   1.114 +  | checkT (TVar ((a, i), _)) = def_err "type is not clean"
   1.115 +  | checkT (TFree (a, _)) = TVar ((a, 0), [])
   1.116 +
   1.117 +fun declare' (cost, actions, g) (cty as (name, ty)) =
   1.118 +    (cost, (Declare cty)::actions, 
   1.119 +     Symtab.update_new ((name, Node (ty, Symtab.empty, Symtab.empty, [])), g))
   1.120      handle Symtab.DUP _ => def_err "constant is already declared"
   1.121  
   1.122 +fun declare g (name, ty) = declare' g (name, checkT ty)
   1.123 +
   1.124  fun rename ty1 ty2 = incr_tvar ((maxidx_of_typ ty1)+1) ty2;  
   1.125  
   1.126  fun subst_incr_tvar inc t =
   1.127 @@ -95,16 +115,6 @@
   1.128        end	
   1.129      else
   1.130        (t, Vartab.empty)
   1.131 -
   1.132 -(* Rename tys2 so that tys2 and tys1 do not have any variables in common any more.
   1.133 -   As a result, return the renamed tys2' and the substitution that takes tys2 to tys2'. *)
   1.134 -fun subst_rename max1 ty2 =
   1.135 -    let
   1.136 -      val max2 = (maxidx_of_typ ty2)
   1.137 -      val (ty2', s) = subst_incr_tvar (max1 + 1) ty2                
   1.138 -    in
   1.139 -      (ty2', s, max1 + max2 + 1)
   1.140 -    end	       
   1.141      
   1.142  fun subst s ty = Envir.norm_type s ty
   1.143                   
   1.144 @@ -121,20 +131,21 @@
   1.145      handle Type.TUNIFY => NONE
   1.146                              
   1.147  (* 
   1.148 -   Unifies ty1 and ty2, renaming ty1 and ty2 so that they have greater indices than max and so that they
   1.149 -   are different. All indices in ty1 and ty2 are supposed to be less than or equal to max.
   1.150 -   Returns SOME (max', s1, s2), so that s1(ty1) = s2(ty2) and max' is greater or equal than all 
   1.151 -   indices in s1, s2, ty1, ty2.
   1.152 +   Unifies ty1 and ty2, renaming ty1 and ty2 so that they have greater indices than max and 
   1.153 +   so that they are different. All indices in ty1 and ty2 are supposed to be less than or 
   1.154 +   equal to max.
   1.155 +   Returns SOME (max', s1, s2), so that s1(ty1) = s2(ty2) and max' is greater or equal than 
   1.156 +   all indices in s1, s2, ty1, ty2.
   1.157  *)
   1.158  fun unify_r max ty1 ty2 = 
   1.159      let
   1.160 -      val max =  Int.max(max, 0)
   1.161 +      val max = Int.max(max, 0)
   1.162        val max1 = max (* >= maxidx_of_typ ty1 *)
   1.163        val max2 = max (* >= maxidx_of_typ ty2 *)
   1.164        val max = Int.max(max, Int.max (max1, max2))
   1.165 -      val (ty1, s1) = subst_incr_tvar (max+1) ty1
   1.166 -      val (ty2, s2) = subst_incr_tvar (max+max1+2) ty2
   1.167 -      val max = max+max1+max2+2	
   1.168 +      val (ty1, s1) = subst_incr_tvar (max + 1) ty1
   1.169 +      val (ty2, s2) = subst_incr_tvar (max + max1 + 2) ty2
   1.170 +      val max = max + max1 + max2 + 2	
   1.171        fun merge a b = Vartab.merge (fn _ => false) (a, b)
   1.172      in
   1.173        case unify ty1 ty2 of
   1.174 @@ -156,33 +167,63 @@
   1.175        NONE => false
   1.176      | _ => true
   1.177             
   1.178 -fun checkT (Type (a, Ts)) = Type (a, map checkT Ts)
   1.179 -  | checkT (TVar ((a, 0), _)) = TVar ((a, 0), [])
   1.180 -  | checkT (TVar ((a, i), _)) = def_err "type is not clean"
   1.181 -  | checkT (TFree (a, _)) = TVar ((a, 0), [])
   1.182 +structure Inttab = TableFun(type key = int val ord = int_ord);
   1.183  
   1.184 -fun label_ord NONE NONE = EQUAL
   1.185 -  | label_ord NONE (SOME _) = LESS
   1.186 -  | label_ord (SOME _) NONE = GREATER
   1.187 -  | label_ord (SOME l1) (SOME l2) = string_ord (l1,l2)
   1.188 -
   1.189 +fun normalize_edge_idx (edge as (maxidx, u1, v1, history)) =
   1.190 +    if maxidx <= 1000000 then edge else
   1.191 +    let
   1.192 +      
   1.193 +      fun idxlist idx extract_ty inject_ty (tab, max) ts = 
   1.194 +          foldr 
   1.195 +            (fn (e, ((tab, max), ts)) => 
   1.196 +                let
   1.197 +                  val ((tab, max), ty) = idx (tab, max) (extract_ty e)
   1.198 +                  val e = inject_ty (ty, e)
   1.199 +                in
   1.200 +                  ((tab, max), e::ts)
   1.201 +                end)
   1.202 +            ((tab,max), []) ts
   1.203 +          
   1.204 +      fun idx (tab,max) (TVar ((a,i),_)) = 
   1.205 +          (case Inttab.lookup (tab, i) of 
   1.206 +             SOME j => ((tab, max), TVar ((a,j),[]))
   1.207 +           | NONE => ((Inttab.update ((i, max), tab), max+1), TVar ((a,max),[])))
   1.208 +        | idx (tab,max) (Type (t, ts)) = 
   1.209 +          let 
   1.210 +            val ((tab, max), ts) = idxlist idx I fst (tab, max) ts
   1.211 +          in
   1.212 +            ((tab,max), Type (t, ts))
   1.213 +          end
   1.214 +        | idx (tab, max) ty = ((tab, max), ty)
   1.215 +      
   1.216 +      val ((tab,max), u1) = idx (Inttab.empty, 0) u1
   1.217 +      val ((tab,max), v1) = idx (tab, max) v1
   1.218 +      val ((tab,max), history) = 
   1.219 +          idxlist idx
   1.220 +            (fn (ty,_,_) => ty) 
   1.221 +            (fn (ty, (_, s1, s2)) => (ty, s1, s2)) 
   1.222 +            (tab, max) history
   1.223 +    in
   1.224 +      (max, u1, v1, history)
   1.225 +    end
   1.226 +                        
   1.227  fun compare_edges (e1 as (maxidx1, u1, v1, history1)) (e2 as (maxidx2, u2, v2, history2)) =
   1.228      let
   1.229        val t1 = u1 --> v1
   1.230 -      val t2 = u2 --> v2
   1.231 +      val t2 = incr_tvar (maxidx1+1) (u2 --> v2)
   1.232      in
   1.233 -      if (is_instance_r t1 t2) then
   1.234 -	(if is_instance_r t2 t1 then
   1.235 +      if (is_instance t1 t2) then
   1.236 +	(if is_instance t2 t1 then
   1.237  	   SOME (int_ord (length history2, length history1))
   1.238  	 else
   1.239  	   SOME LESS)
   1.240 -      else if (is_instance_r t2 t1) then
   1.241 +      else if (is_instance t2 t1) then
   1.242  	SOME GREATER
   1.243        else
   1.244  	NONE
   1.245      end
   1.246 -    
   1.247 -fun merge_edges_1 (x, []) = []
   1.248 +
   1.249 +fun merge_edges_1 (x, []) = [x]
   1.250    | merge_edges_1 (x, (y::ys)) = 
   1.251      (case compare_edges x y of
   1.252         SOME LESS => (y::ys)
   1.253 @@ -192,40 +233,16 @@
   1.254      
   1.255  fun merge_edges xs ys = foldl merge_edges_1 xs ys
   1.256  
   1.257 -fun pack_edges xs = merge_edges [] xs
   1.258 -
   1.259 -fun merge_labelled_edges [] es = es
   1.260 -  | merge_labelled_edges es [] = es
   1.261 -  | merge_labelled_edges ((l1,e1)::es1) ((l2,e2)::es2) = 
   1.262 -    (case label_ord l1 l2 of
   1.263 -       LESS => (l1, e1)::(merge_labelled_edges es1 ((l2, e2)::es2))
   1.264 -     | GREATER => (l2, e2)::(merge_labelled_edges ((l1, e1)::es1) es2)
   1.265 -     | EQUAL => (l1, merge_edges e1 e2)::(merge_labelled_edges es1 es2))
   1.266 -    
   1.267 -fun defnode_edges_foldl f a defnode =
   1.268 +fun define' (cost, actions, graph) (mainref, ty) axname body =
   1.269      let
   1.270 -      val (Defnode (ty, def_edges)) = defnode
   1.271 -      fun g (b, (_, (n, labelled_edges))) =
   1.272 -	  foldl (fn ((s, edges), b') => 
   1.273 -		    (foldl (fn (e, b'') => f ty n s e b'') b' edges))
   1.274 -		b
   1.275 -		labelled_edges		  		     
   1.276 -    in
   1.277 -      Symtab.foldl g (a, def_edges)
   1.278 -    end	
   1.279 -    
   1.280 -fun define (actions, graph) (name, ty) axname body =
   1.281 -    let
   1.282 -      val ty = checkT ty
   1.283 -      val body = map (fn (n,t) => (n, checkT t)) body		 
   1.284 -      val mainref = name
   1.285        val mainnode  = (case Symtab.lookup (graph, mainref) of 
   1.286  			 NONE => def_err ("constant "^mainref^" is not declared")
   1.287  		       | SOME n => n)
   1.288 -      val (Node (n, gty, defs, backs, finals)) = mainnode
   1.289 -      val _ = (if is_instance_r ty gty then () else def_err "type of constant does not match declared type")
   1.290 +      val (Node (gty, defs, backs, finals)) = mainnode
   1.291 +      val _ = (if is_instance_r ty gty then () 
   1.292 +               else def_err "type of constant does not match declared type")
   1.293        fun check_def (s, Defnode (ty', _)) = 
   1.294 -	  (if can_be_unified_r ty ty' then 
   1.295 +          (if can_be_unified_r ty ty' then 
   1.296  	     raise (CLASH (mainref, axname, s))
   1.297  	   else if s = axname then
   1.298  	     def_err "name of axiom is already used for another definition of this constant"
   1.299 @@ -238,160 +255,118 @@
   1.300  	     true)
   1.301        val _ = forall check_final finals
   1.302  	             
   1.303 -      (* now we know that the only thing that can prevent acceptance of the definition is a cyclic dependency *)
   1.304 +      (* now we know that the only thing that can prevent acceptance of the definition 
   1.305 +         is a cyclic dependency *)
   1.306  
   1.307 -      (* body contains the constants that this constant definition depends on. For each element of body,
   1.308 -         the function make_edges_to calculates a group of edges that connect this constant with 
   1.309 -         the constant that is denoted by the element of the body *)
   1.310 -      fun make_edges_to (bodyn, bodyty) =
   1.311 +      fun insert_edges edges (nodename, links) =
   1.312 +          (if links = [] then 
   1.313 +             edges
   1.314 +           else
   1.315 +             let
   1.316 +               val links = map normalize_edge_idx links
   1.317 +             in
   1.318 +               Symtab.update ((nodename, 
   1.319 +	                       case Symtab.lookup (edges, nodename) of
   1.320 +	                         NONE => links
   1.321 +	                       | SOME links' => merge_edges links' links),
   1.322 +                              edges)
   1.323 +             end)
   1.324 +	 
   1.325 +      fun make_edges ((bodyn, bodyty), edges) =
   1.326  	  let
   1.327  	    val bnode = 
   1.328  		(case Symtab.lookup (graph, bodyn) of 
   1.329  		   NONE => def_err "body of constant definition references undeclared constant"
   1.330  		 | SOME x => x)
   1.331 -	    val (Node (_, general_btyp, bdefs, bbacks, bfinals)) = bnode
   1.332 +	    val (Node (general_btyp, bdefs, bbacks, bfinals)) = bnode
   1.333  	  in
   1.334  	    case unify_r 0 bodyty general_btyp of
   1.335 -	      NONE => NONE
   1.336 +	      NONE => edges
   1.337  	    | SOME (maxidx, sigma1, sigma2) => 
   1.338 -	      SOME (
   1.339 -	      let
   1.340 -		(* For each definition of the constant in the body, 
   1.341 -		   check if the definition unifies with the type of the constant in the body. *)	                
   1.342 -                fun make_edges ((swallowed, l),(def_name, Defnode (def_ty, _))) =
   1.343 -		    if swallowed then
   1.344 -		      (swallowed, l)
   1.345 -		    else 
   1.346 -		      (case unify_r 0 bodyty def_ty of
   1.347 -			 NONE => (swallowed, l)
   1.348 -		       | SOME (maxidx, sigma1, sigma2) => 
   1.349 -			 (is_instance_r bodyty def_ty,
   1.350 -			  merge_labelled_edges l [(SOME def_name,[(maxidx, subst sigma1 ty, subst sigma2 def_ty, [])])]))
   1.351 -                val swallowed = exists (is_instance_r bodyty) bfinals
   1.352 -          	val (swallowed, edges) = Symtab.foldl make_edges ((swallowed, []), bdefs)
   1.353 -	      in
   1.354 -		if swallowed then 
   1.355 -		  (bodyn, edges)
   1.356 -		else 
   1.357 -		  (bodyn, [(NONE, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])])]@edges)
   1.358 -	      end)
   1.359 +              if exists (is_instance_r bodyty) bfinals then 
   1.360 +                edges
   1.361 +              else
   1.362 +	        let
   1.363 +		  fun insert_trans_edges ((step1, edges), (nodename, links)) =
   1.364 +                      let
   1.365 +                        val (maxidx1, alpha1, beta1, defname) = step1
   1.366 +                        fun connect (maxidx2, alpha2, beta2, history) = 
   1.367 +		            case unify_r (Int.max (maxidx1, maxidx2)) beta1 alpha2 of
   1.368 +		              NONE => NONE
   1.369 +		            | SOME (max, sleft, sright) =>				  
   1.370 +			      SOME (max, subst sleft alpha1, subst sright beta2, 
   1.371 +                                    if !CHAIN_HISTORY then   
   1.372 +			              ((subst sleft beta1, bodyn, defname)::
   1.373 +				       (subst_history sright history))
   1.374 +                                    else [])            
   1.375 +                        val links' = List.mapPartial connect links
   1.376 +                      in
   1.377 +                        (step1, insert_edges edges (nodename, links'))
   1.378 +                      end
   1.379 +                                                                
   1.380 +                  fun make_edges' ((swallowed, edges),
   1.381 +                                   (def_name, Defnode (def_ty, def_edges))) =
   1.382 +		      if swallowed then
   1.383 +		        (swallowed, edges)
   1.384 +		      else 
   1.385 +		        (case unify_r 0 bodyty def_ty of
   1.386 +			   NONE => (swallowed, edges)
   1.387 +		         | SOME (maxidx, sigma1, sigma2) => 
   1.388 +			   (is_instance_r bodyty def_ty,
   1.389 +                            snd (Symtab.foldl insert_trans_edges 
   1.390 +                              (((maxidx, subst sigma1 ty, subst sigma2 def_ty, def_name),
   1.391 +                                edges), def_edges))))
   1.392 +          	  val (swallowed, edges) = Symtab.foldl make_edges' ((false, edges), bdefs)
   1.393 +	        in
   1.394 +		  if swallowed then 
   1.395 +		    edges
   1.396 +		  else 
   1.397 +                    insert_edges edges 
   1.398 +                    (bodyn, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])])
   1.399 +	        end
   1.400  	  end 
   1.401 -          
   1.402 -      fun update_edges (b as (bodyn, bodyty), edges) =
   1.403 -	  (case make_edges_to b of
   1.404 -	     NONE => edges
   1.405 -	   | SOME m =>
   1.406 -	     (case Symtab.lookup (edges, bodyn) of
   1.407 -		NONE => Symtab.update ((bodyn, m), edges)
   1.408 -	      | SOME (_, es') => 
   1.409 -		let 
   1.410 -		  val (_, es) = m
   1.411 -		  val es = merge_labelled_edges es es'
   1.412 -		in
   1.413 -		  Symtab.update ((bodyn, (bodyn, es)), edges)
   1.414 -		end
   1.415 -	     )
   1.416 -	  )
   1.417 -          
   1.418 -      val edges = foldl update_edges Symtab.empty body
   1.419 -                  
   1.420 -      fun insert_edge edges (nodename, (defname_opt, edge)) = 
   1.421 -	  let
   1.422 -	    val newlink = [(defname_opt, [edge])]
   1.423 -	  in
   1.424 -	    case Symtab.lookup (edges, nodename) of
   1.425 -	      NONE => Symtab.update ((nodename, (nodename, newlink)), edges)		    
   1.426 -	    | SOME (_, links) => 
   1.427 -	      let
   1.428 -		val links' = merge_labelled_edges links newlink
   1.429 -	      in
   1.430 -		Symtab.update ((nodename, (nodename, links')), edges)
   1.431 -	      end
   1.432 -	  end				    
   1.433 -            
   1.434 -      (* We constructed all direct edges that this defnode has. 
   1.435 -         Now we have to construct the transitive hull by going a single step further. *)
   1.436 -          
   1.437 -      val thisDefnode = Defnode (ty, edges)
   1.438 -                        
   1.439 -      fun make_trans_edges _ noderef defname_opt (max1, alpha1, beta1, history1) edges = 
   1.440 -	  case defname_opt of 
   1.441 -	    NONE => edges
   1.442 -	  | SOME defname => 		
   1.443 -	    let
   1.444 -	      val defnode = the (get_defnode' graph noderef defname)
   1.445 -	      fun make_trans_edge _ noderef2 defname_opt2 (max2, alpha2, beta2, history2) edges =
   1.446 -		  case unify_r (Int.max (max1, max2)) beta1 alpha2 of
   1.447 -		    NONE => edges
   1.448 -		  | SOME (max, sleft, sright) =>
   1.449 -		    insert_edge edges (noderef2, 
   1.450 -				       (defname_opt2, 							  
   1.451 -					(max, subst sleft alpha1, subst sright beta2, 
   1.452 -					 (subst_history sleft history1)@
   1.453 -					 ((subst sleft beta1, noderef, defname)::
   1.454 -					  (subst_history sright history2)))))
   1.455 -	    in
   1.456 -	      defnode_edges_foldl make_trans_edge edges defnode
   1.457 -	    end
   1.458 -            
   1.459 -      val edges = defnode_edges_foldl make_trans_edges edges thisDefnode
   1.460 -                  
   1.461 -      val thisDefnode = Defnode (ty, edges)
   1.462 -
   1.463 -      (* We also have to add the backreferences that this new defnode induces. *)
   1.464 -	    
   1.465 -      fun hasNONElink ((NONE, _)::_) = true
   1.466 -	| hasNONElink _ = false
   1.467 -	                  
   1.468 -      fun install_backref graph noderef pointingnoderef pointingdefname = 
   1.469 -	  let
   1.470 -	    val (Node (pname, _, _, _, _)) = getnode graph pointingnoderef
   1.471 -	    val (Node (name, ty, defs, backs, finals)) = getnode graph noderef
   1.472 -	  in
   1.473 -	    case Symtab.lookup (backs, pname) of
   1.474 -	      NONE => 
   1.475 -	      let 
   1.476 -		val defnames = Symtab.update ((pointingdefname, ()), Symtab.empty)
   1.477 -		val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs)
   1.478 -	      in
   1.479 -		Symtab.update ((name, Node (name, ty, defs, backs, finals)), graph) 			
   1.480 -	      end
   1.481 -	    | SOME (Backref (pointingnoderef, defnames)) =>
   1.482 -	      let
   1.483 -		val defnames = Symtab.update_new ((pointingdefname, ()), defnames)
   1.484 -		val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs)
   1.485 -	      in
   1.486 -		Symtab.update ((name, Node (name, ty, defs, backs, finals)), graph)
   1.487 -	      end
   1.488 -	      handle Symtab.DUP _ => graph
   1.489 -	  end
   1.490 -          
   1.491 -      fun install_backrefs (graph, (_, (noderef, labelled_edges))) =
   1.492 -	  if hasNONElink labelled_edges then
   1.493 -	    install_backref graph noderef mainref axname
   1.494 -	  else 
   1.495 -	    graph
   1.496 +                    
   1.497 +      val edges = foldl make_edges Symtab.empty body
   1.498 +                  				               
   1.499 +      (* We also have to add the backreferences that this new defnode induces. *)  
   1.500 +      fun install_backrefs (graph, (noderef, links)) =
   1.501 +          if links <> [] then
   1.502 +            let
   1.503 +              val (Node (ty, defs, backs, finals)) = getnode graph noderef
   1.504 +              val defnames =
   1.505 +                  (case Symtab.lookup (backs, mainref) of
   1.506 +                     NONE => Symtab.empty
   1.507 +                   | SOME s => s)
   1.508 +              val defnames' = Symtab.update_new ((axname, ()), defnames)
   1.509 +              val backs' = Symtab.update ((mainref,defnames'), backs)
   1.510 +            in
   1.511 +              Symtab.update ((noderef, Node (ty, defs, backs', finals)), graph)
   1.512 +            end
   1.513 +          else
   1.514 +            graph
   1.515              
   1.516        val graph = Symtab.foldl install_backrefs (graph, edges)
   1.517                    
   1.518 -      val (Node (_, _, _, backs, _)) = getnode graph mainref
   1.519 -      val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update_new 
   1.520 +      val (Node (_, _, backs, _)) = getnode graph mainref
   1.521 +      val thisDefnode = Defnode (ty, edges)
   1.522 +      val graph = Symtab.update ((mainref, Node (gty, Symtab.update_new 
   1.523          ((axname, thisDefnode), defs), backs, finals)), graph)
   1.524  		                
   1.525 -      (* Now we have to check all backreferences to this node and inform them about the new defnode. 
   1.526 -	 In this section we also check for circularity. *)
   1.527 -      fun update_backrefs ((backs, newedges), (nodename, Backref (noderef, defnames))) =	    
   1.528 +      (* Now we have to check all backreferences to this node and inform them about 
   1.529 +         the new defnode. In this section we also check for circularity. *)
   1.530 +      fun update_backrefs ((backs, graph), (noderef, defnames)) =
   1.531  	  let
   1.532 -	    val node = getnode graph noderef
   1.533 -	    fun update_defs ((defnames, newedges),(defname, _)) =
   1.534 +	    fun update_defs ((defnames, graph),(defname, _)) =
   1.535  		let
   1.536 -		  val (Defnode (_, defnode_edges)) = the (get_defnode node defname)
   1.537 -		  val (_, labelled_edges) = the (Symtab.lookup (defnode_edges, n))
   1.538 -						
   1.539 +                  val (Node (nodety, nodedefs, nodebacks, nodefinals)) = getnode graph noderef
   1.540 +		  val (Defnode (def_ty, defnode_edges)) = 
   1.541 +                      the (Symtab.lookup (nodedefs, defname))
   1.542 +		  val edges = the (Symtab.lookup (defnode_edges, mainref))
   1.543 + 					
   1.544  	          (* the type of thisDefnode is ty *)
   1.545 -		  fun update (e as (max, alpha, beta, history), (none_edges, this_edges)) = 
   1.546 +		  fun update (e as (max, alpha, beta, history), (changed, edges)) = 
   1.547  		      case unify_r max beta ty of
   1.548 -			NONE => (e::none_edges, this_edges)
   1.549 +			NONE => (changed, e::edges)
   1.550  		      | SOME (max', s_beta, s_ty) =>
   1.551  			let
   1.552  			  val alpha' = subst s_beta alpha
   1.553 @@ -406,100 +381,92 @@
   1.554  					    (subst_history s_beta history)@
   1.555  					    [(ty', mainref, axname)]))
   1.556  				   else ()
   1.557 -				 | SOME s => raise (CIRCULAR (
   1.558 -						    (subst s alpha', mainref, axname)::
   1.559 -						    (subst_history s (subst_history s_beta history))@
   1.560 -						    [(subst s ty', mainref, axname)])))
   1.561 -			      else ()
   1.562 -			  val edge = (max', alpha', ty', subst_history s_beta history)
   1.563 +				 | SOME s => 
   1.564 +                                   raise (CIRCULAR (
   1.565 +					  (subst s alpha', mainref, axname)::
   1.566 +					  (subst_history s (subst_history s_beta history))@
   1.567 +					  [(subst s ty', mainref, axname)])))
   1.568 +			      else ()                             
   1.569  			in
   1.570 -			  if is_instance_r beta ty then 
   1.571 -			    (none_edges, edge::this_edges)
   1.572 +			  if is_instance_r beta ty then
   1.573 +			    (true, edges)
   1.574  			  else
   1.575 -			    (e::none_edges, edge::this_edges)
   1.576 -			end					    			   			    
   1.577 -		in
   1.578 -		  case labelled_edges of 
   1.579 -		    ((NONE, edges)::_) => 
   1.580 -		    let
   1.581 -		      val (none_edges, this_edges) = foldl update ([], []) edges
   1.582 -		      val defnames = if none_edges = [] then defnames else Symtab.update_new ((defname, ()), defnames) 
   1.583 -		    in
   1.584 -		      (defnames, (defname, none_edges, this_edges)::newedges)
   1.585 -		    end			    
   1.586 -		  | _ => sys_error "define: update_defs, internal error, corrupt backrefs"
   1.587 -		end
   1.588 +			    (changed, e::edges)
   1.589 +			end		    			   			       
   1.590 +                  
   1.591 +                  val (changed, edges') = foldl update (false, []) edges
   1.592 +                  val defnames' = if edges' = [] then 
   1.593 +                                    defnames 
   1.594 +                                  else 
   1.595 +                                    Symtab.update ((defname, ()), defnames)
   1.596 +                in
   1.597 +                  if changed then
   1.598 +                    let
   1.599 +                      val defnode_edges' = 
   1.600 +                          if edges' = [] then
   1.601 +                            Symtab.delete mainref defnode_edges
   1.602 +                          else
   1.603 +                            Symtab.update ((mainref, edges'), defnode_edges)
   1.604 +                      val defnode' = Defnode (def_ty, defnode_edges')
   1.605 +                      val nodedefs' = Symtab.update ((defname, defnode'), nodedefs)
   1.606 +                      val graph' = 
   1.607 +                          Symtab.update 
   1.608 +                            ((noderef, Node (nodety, nodedefs', nodebacks, nodefinals)),graph) 
   1.609 +                    in
   1.610 +                      (defnames', graph')
   1.611 +                    end
   1.612 +                  else
   1.613 +                    (defnames', graph)
   1.614 +                end
   1.615  		    
   1.616 -	    val (defnames, newedges') = Symtab.foldl update_defs ((Symtab.empty, []), defnames)
   1.617 +	    val (defnames', graph') = Symtab.foldl update_defs 
   1.618 +                                                   ((Symtab.empty, graph), defnames)
   1.619  	  in
   1.620 -	    if Symtab.is_empty defnames then 
   1.621 -	      (backs, (noderef, newedges')::newedges)
   1.622 +	    if Symtab.is_empty defnames' then 
   1.623 +	      (backs, graph')
   1.624  	    else
   1.625  	      let
   1.626 -		val backs = Symtab.update_new ((nodename, Backref (noderef, defnames)), backs)
   1.627 +		val backs' = Symtab.update_new ((noderef, defnames'), backs)
   1.628  	      in
   1.629 -		(backs, newedges)
   1.630 +		(backs', graph')
   1.631  	      end
   1.632  	  end
   1.633 -	  
   1.634 -
   1.635 -      val (backs, newedges) = Symtab.foldl update_backrefs ((Symtab.empty, []), backs)
   1.636 -						 
   1.637 +        
   1.638 +      val (backs, graph) = Symtab.foldl update_backrefs ((Symtab.empty, graph), backs)
   1.639 +                                        						 
   1.640        (* If a Circular exception is thrown then we never reach this point. *)
   1.641 -      (* Ok, the definition is consistent, let's update this node. *)
   1.642 -      val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update 
   1.643 -        ((axname, thisDefnode), defs), backs, finals)), graph)
   1.644 -
   1.645 -      (* Furthermore, update all the other nodes that backreference this node. *)
   1.646 -      fun final_update_backrefs graph noderef defname none_edges this_edges =
   1.647 -	  let
   1.648 -	    val node = getnode graph noderef
   1.649 -	    val (Node (nodename, nodety, defs, backs, finals)) = node
   1.650 -	    val (Defnode (defnode_ty, defnode_edges)) = the (get_defnode node defname)
   1.651 -	    val (_, defnode_links) = the (Symtab.lookup (defnode_edges, n))
   1.652 -                                     
   1.653 -	    fun update edges none_edges this_edges =
   1.654 -		let 
   1.655 -		  val u = merge_labelled_edges edges [(SOME axname, pack_edges this_edges)]
   1.656 -		in
   1.657 -		  if none_edges = [] then
   1.658 -		    u
   1.659 -		  else
   1.660 -		    (NONE, pack_edges none_edges)::u
   1.661 -		end
   1.662 -		
   1.663 -	    val defnode_links' = 
   1.664 -		case defnode_links of 
   1.665 -		  ((NONE, _) :: edges) => update edges none_edges this_edges
   1.666 -		| edges => update edges none_edges this_edges
   1.667 -	    val defnode_edges' = Symtab.update ((n, (mainref, defnode_links')), defnode_edges)
   1.668 -	    val defs' = Symtab.update ((defname, Defnode (defnode_ty, defnode_edges')), defs)
   1.669 -	  in
   1.670 -	    Symtab.update ((nodename, Node (nodename, nodety, defs', backs, finals)), graph)
   1.671 -	  end
   1.672 -          
   1.673 -      val graph = foldl (fn ((noderef, newedges),graph) => foldl (fn ((defname, none_edges, this_edges), graph) =>
   1.674 -        final_update_backrefs graph noderef defname none_edges this_edges) graph newedges) graph newedges		    
   1.675 -                  
   1.676 +      val (Node (gty, defs, _, finals)) = getnode graph mainref
   1.677 +      val graph = Symtab.update ((mainref, Node (gty, defs, backs, finals)), graph) 
   1.678      in	    
   1.679 -      ((Define (name, ty, axname, body))::actions, graph)	   
   1.680 +      (cost+3,(Define (mainref, ty, axname, body))::actions, graph)
   1.681      end 
   1.682      
   1.683 -fun finalize (history, graph) (c, ty) = 
   1.684 -    case Symtab.lookup (graph, c) of 
   1.685 -      NONE => def_err ("cannot finalize constant "^c^"; it is not declared")
   1.686 -    | SOME (Node (noderef, nodety, defs, backs, finals)) =>
   1.687 +fun define g (mainref, ty) axname body =
   1.688 +    let
   1.689 +      val ty = checkT ty
   1.690 +      val body = distinct (map (fn (n,t) => (n, checkT t)) body)
   1.691 +    in
   1.692 +      define' g (mainref, ty) axname body
   1.693 +    end
   1.694 +
   1.695 +fun finalize' (cost, history, graph) (noderef, ty) = 
   1.696 +    case Symtab.lookup (graph, noderef) of 
   1.697 +      NONE => def_err ("cannot finalize constant "^noderef^"; it is not declared")
   1.698 +    | SOME (Node (nodety, defs, backs, finals)) =>
   1.699        let 
   1.700 -	val ty = checkT ty
   1.701 -	val _ = if (not (is_instance_r ty nodety)) then
   1.702 -		  def_err ("only type instances of the declared constant "^c^" can be finalized")
   1.703 -		else ()
   1.704 -	val _ = Symtab.exists (fn (def_name, Defnode (def_ty, _)) =>  
   1.705 -				  if can_be_unified_r ty def_ty then 
   1.706 -				    def_err ("cannot finalize constant "^c^"; clash with definition "^def_name)
   1.707 -				  else 
   1.708 -				    false)
   1.709 -			      defs 
   1.710 +	val _ = 
   1.711 +            if (not (is_instance_r ty nodety)) then
   1.712 +	      def_err ("only type instances of the declared constant "^
   1.713 +                       noderef^" can be finalized")
   1.714 +	    else ()
   1.715 +	val _ = Symtab.exists 
   1.716 +                  (fn (def_name, Defnode (def_ty, _)) =>  
   1.717 +		      if can_be_unified_r ty def_ty then 
   1.718 +			def_err ("cannot finalize constant "^noderef^
   1.719 +                                 "; clash with definition "^def_name)
   1.720 +		      else 
   1.721 +			false)
   1.722 +		  defs 
   1.723          
   1.724          fun update_finals [] = SOME [ty]
   1.725            | update_finals (final_ty::finals) = 
   1.726 @@ -514,91 +481,119 @@
   1.727                     SOME (final_ty :: finals))                              
   1.728        in    
   1.729          case update_finals finals of
   1.730 -          NONE => (history, graph)
   1.731 +          NONE => (cost, history, graph)
   1.732          | SOME finals => 
   1.733  	  let
   1.734 -	    val graph = Symtab.update ((noderef, Node(noderef, nodety, defs, backs, finals)), graph)
   1.735 +	    val graph = Symtab.update ((noderef, Node(nodety, defs, backs, finals)), 
   1.736 +                                       graph)
   1.737  	                
   1.738 -	    fun update_backref ((graph, backs), (backrefname, Backref (_, backdefnames))) =
   1.739 +	    fun update_backref ((graph, backs), (backrefname, backdefnames)) =
   1.740  		let
   1.741  		  fun update_backdef ((graph, defnames), (backdefname, _)) = 
   1.742  	              let 
   1.743 -			val (backnode as Node (_, backty, backdefs, backbacks, backfinals)) = getnode graph backrefname
   1.744 -			val (Defnode (def_ty, all_edges)) = the (get_defnode backnode backdefname)						      
   1.745 +			val (backnode as Node (backty, backdefs, backbacks, backfinals)) = 
   1.746 +                            getnode graph backrefname
   1.747 +			val (Defnode (def_ty, all_edges)) = 
   1.748 +                            the (get_defnode backnode backdefname)
   1.749 +
   1.750  			val (defnames', all_edges') = 
   1.751  			    case Symtab.lookup (all_edges, noderef) of
   1.752  			      NONE => sys_error "finalize: corrupt backref"
   1.753 -			    | SOME (_, (NONE, edges)::rest) =>
   1.754 +			    | SOME edges =>
   1.755  			      let
   1.756 -				val edges' = List.filter (fn (_, _, beta, _) => not (is_instance_r beta ty)) edges
   1.757 +				val edges' = List.filter (fn (_, _, beta, _) => 
   1.758 +                                                             not (is_instance_r beta ty)) edges
   1.759  			      in
   1.760  				if edges' = [] then 
   1.761 -				  (defnames, Symtab.update ((noderef, (noderef, rest)), all_edges))
   1.762 +				  (defnames, Symtab.delete noderef all_edges)
   1.763  				else
   1.764  				  (Symtab.update ((backdefname, ()), defnames), 
   1.765 -				   Symtab.update ((noderef, (noderef, (NONE, edges')::rest)), all_edges))
   1.766 +				   Symtab.update ((noderef, edges'), all_edges))
   1.767  			      end
   1.768  			val defnode' = Defnode (def_ty, all_edges')
   1.769 -			val backnode' = Node (backrefname, backty, Symtab.update ((backdefname, defnode'), backdefs), 
   1.770 -					      backbacks, backfinals)
   1.771 +			val backnode' = 
   1.772 +                            Node (backty, 
   1.773 +                                  Symtab.update ((backdefname, defnode'), backdefs), 
   1.774 +				  backbacks, backfinals)
   1.775  		      in
   1.776 -			(Symtab.update ((backrefname, backnode'), graph), defnames')			  			  
   1.777 +			(Symtab.update ((backrefname, backnode'), graph), defnames') 
   1.778  		      end
   1.779  	              
   1.780 -		  val (graph', defnames') = Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames)
   1.781 +		  val (graph', defnames') = 
   1.782 +                      Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames)
   1.783  		in
   1.784  		  (graph', if Symtab.is_empty defnames' then backs 
   1.785 -			   else Symtab.update ((backrefname, Backref (backrefname, defnames')), backs))
   1.786 +			   else Symtab.update ((backrefname, defnames'), backs))
   1.787  		end
   1.788  	    val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs)
   1.789 -	    val Node (_, _, defs, _, _) = getnode graph' noderef
   1.790 +	    val Node ( _, defs, _, _) = getnode graph' noderef
   1.791 +	    val graph' = Symtab.update ((noderef, Node (nodety, defs, backs', finals)), graph')
   1.792  	  in
   1.793 -	    ((Finalize (c, ty)) :: history, Symtab.update ((noderef, Node (noderef, nodety, defs, backs', finals)), graph'))
   1.794 +	    (cost+1,(Finalize (noderef, ty)) :: history, graph')
   1.795  	  end
   1.796        end
   1.797 -      
   1.798 -fun merge' (Declare cty, g) = (declare g cty handle _ => g)
   1.799 -  | merge' (Define (name, ty, axname, body), g as (_, graph)) = 
   1.800 + 
   1.801 +fun finalize g (noderef, ty) = finalize' g (noderef, checkT ty)
   1.802 +
   1.803 +fun merge' (Declare cty, g) = (declare' g cty handle _ => g)
   1.804 +  | merge' (Define (name, ty, axname, body), g as (_,_, graph)) = 
   1.805      (case Symtab.lookup (graph, name) of
   1.806 -       NONE => define g (name, ty) axname body
   1.807 -     | SOME (Node (_, _, defs, _, _)) => 
   1.808 +       NONE => define' g (name, ty) axname body
   1.809 +     | SOME (Node (_, defs, _, _)) => 
   1.810         (case Symtab.lookup (defs, axname) of
   1.811 -	  NONE => define g (name, ty) axname body
   1.812 +	  NONE => define' g (name, ty) axname body
   1.813  	| SOME _ => g))
   1.814 -  | merge' (Finalize finals, g) = finalize g finals 
   1.815 +  | merge' (Finalize finals, g) = finalize' g finals 
   1.816                         
   1.817 -fun merge (actions, _) g = foldr merge' g actions
   1.818 +fun merge (g1 as (cost1, actions1, _)) (g2 as (cost2, actions2, _)) =
   1.819 +    if cost1 < cost2 then
   1.820 +      foldr merge' g2 actions1
   1.821 +    else
   1.822 +      foldr merge' g1 actions2
   1.823                             
   1.824 -fun finals (history, graph) = 
   1.825 +fun finals (cost, history, graph) = 
   1.826      Symtab.foldl 
   1.827 -      (fn (finals, (_, Node(name, _, _, _, ftys))) => Symtab.update_new ((name, ftys), finals))  
   1.828 +      (fn (finals, (name, Node(_, _, _, ftys))) => Symtab.update_new ((name, ftys), finals))  
   1.829        (Symtab.empty, graph)
   1.830  
   1.831  end;
   1.832  		
   1.833 -
   1.834 +(*
   1.835  
   1.836 -(*fun tvar name = TVar ((name, 0), [])
   1.837 +fun tvar name = TVar ((name, 0), [])
   1.838  
   1.839  val bool = Type ("bool", [])
   1.840  val int = Type ("int", [])
   1.841 +val lam = Type("lam", [])
   1.842  val alpha = tvar "'a"
   1.843  val beta = tvar "'b"
   1.844  val gamma = tvar "'c"
   1.845  fun pair a b = Type ("pair", [a,b])
   1.846 +fun prm a = Type ("prm", [a])
   1.847 +val name = Type ("name", [])
   1.848  
   1.849  val _ = print "make empty"
   1.850  val g = Defs.empty 
   1.851  
   1.852 -val _ = print "declare"
   1.853 -val g = Defs.declare g "M" (alpha --> bool)
   1.854 -val g = Defs.declare g "N" (beta --> bool)
   1.855 +val _ = print "declare perm"
   1.856 +val g = Defs.declare g ("perm", prm alpha --> beta --> beta)
   1.857 +
   1.858 +val _ = print "declare permF"
   1.859 +val g = Defs.declare g ("permF", prm alpha --> lam --> lam)
   1.860 +
   1.861 +val _ = print "define perm (1)"
   1.862 +val g = Defs.define g ("perm", prm alpha --> (beta --> gamma) --> (beta --> gamma)) "perm_fun" 
   1.863 +        [("perm", prm alpha --> gamma --> gamma), ("perm", prm alpha --> beta --> beta)]
   1.864  
   1.865 -val _ = print "define"
   1.866 -val g = Defs.define g "N" (alpha --> bool) "defN" [("M", alpha --> bool)]
   1.867 -val g = Defs.define g "M" (alpha --> bool) "defM" [("N", int --> alpha)]
   1.868 +val _ = print "define permF (1)"
   1.869 +val g = Defs.define g ("permF", prm alpha --> lam --> lam) "permF_app"
   1.870 +        ([("perm", prm alpha --> lam --> lam),
   1.871 +         ("perm", prm alpha --> lam --> lam),
   1.872 +         ("perm", prm alpha --> lam --> lam),
   1.873 +         ("perm", prm alpha --> name --> name)])
   1.874  
   1.875 -val g = Defs.declare g "0" alpha
   1.876 -val g = Defs.define g "0" (pair alpha beta) "zp" [("0", alpha), ("0", beta)]*)
   1.877 +val _ = print "define perm (2)"
   1.878 +val g = Defs.define g ("perm", prm alpha --> lam --> lam) "perm_lam"
   1.879 +        [("permF", (prm alpha --> lam --> lam))]
   1.880  
   1.881 -
   1.882 +*)
   1.883 \ No newline at end of file