author obua Tue Jun 07 06:39:39 2005 +0200 (2005-06-07) changeset 16308 636a1a84977a 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 file | annotate | diff | revisions
```     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.317 +             in
1.318 +               Symtab.update ((nodename,
1.319 +	                       case Symtab.lookup (edges, nodename) of
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.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.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.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
```