Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
authorobua
Sun May 29 12:39:12 2005 +0200 (2005-05-29)
changeset 16108cf468b93a02e
parent 16107 b16e3df5ad29
child 16109 e8c169d6f191
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
src/Pure/IsaMakefile
src/Pure/ROOT.ML
src/Pure/defs.ML
src/Pure/term.ML
src/Pure/theory.ML
     1.1 --- a/src/Pure/IsaMakefile	Sun May 29 05:23:28 2005 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Sun May 29 12:39:12 2005 +0200
     1.3 @@ -58,7 +58,7 @@
     1.4    goals.ML install_pp.ML library.ML logic.ML meta_simplifier.ML net.ML	\
     1.5    pattern.ML proof_general.ML proofterm.ML pure_thy.ML search.ML	\
     1.6    sign.ML simplifier.ML sorts.ML tactic.ML tctical.ML term.ML		\
     1.7 -  theory.ML theory_data.ML thm.ML type.ML type_infer.ML unify.ML
     1.8 +  defs.ML theory.ML theory_data.ML thm.ML type.ML type_infer.ML unify.ML
     1.9  	@./mk
    1.10  
    1.11  
     2.1 --- a/src/Pure/ROOT.ML	Sun May 29 05:23:28 2005 +0200
     2.2 +++ b/src/Pure/ROOT.ML	Sun May 29 12:39:12 2005 +0200
     2.3 @@ -36,6 +36,7 @@
     2.4  use "unify.ML";
     2.5  use "net.ML";
     2.6  use "logic.ML";
     2.7 +use "defs.ML";
     2.8  use "theory.ML";
     2.9  use "theory_data.ML";
    2.10  use "context.ML";
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/defs.ML	Sun May 29 12:39:12 2005 +0200
     3.3 @@ -0,0 +1,511 @@
     3.4 +(*  Title:      Pure/General/defs.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Steven Obua, TU Muenchen
     3.7 +
     3.8 +    Checks if definitions preserve consistency of logic by enforcing that there are no cyclic definitions.
     3.9 +    The algorithm is described in 
    3.10 +    "Cycle-free Overloading in Isabelle", Steven Obua, technical report, to be written :-)
    3.11 +*)
    3.12 +
    3.13 +signature DEFS = sig
    3.14 +    
    3.15 +    type graph
    3.16 +
    3.17 +    exception DEFS of string
    3.18 +    exception CIRCULAR of (typ * string * string) list
    3.19 +    exception CLASH of string * string * string
    3.20 +    
    3.21 +    val empty : graph
    3.22 +    val declare : graph -> string -> typ -> graph  (* exception DEFS *)
    3.23 +    val define : graph -> string -> typ -> string -> (string * typ) list -> graph (* exception DEFS, CIRCULAR, CLASH *)
    3.24 +
    3.25 +    (* the first argument should be the smaller graph *)
    3.26 +    val merge : graph -> graph -> graph (* exception CIRCULAR, CLASH *)
    3.27 +
    3.28 +end
    3.29 +
    3.30 +structure Defs :> DEFS = struct
    3.31 +
    3.32 +type tyenv = Type.tyenv
    3.33 +type edgelabel = (int * typ * typ * (typ * string * string) list)
    3.34 +type noderef = string
    3.35 +
    3.36 +datatype node = Node of
    3.37 +       string  (* name of constant *)
    3.38 +     * typ  (* most general type of constant *)
    3.39 +     * defnode Symtab.table  (* a table of defnodes, each corresponding to 1 definition of the constant for a particular type, 
    3.40 +                             indexed by axiom name *)
    3.41 +     * backref Symtab.table (* a table of all back references to this node, indexed by node name *)
    3.42 +     
    3.43 +and defnode = Defnode of
    3.44 +       typ  (* type of the constant in this particular definition *)
    3.45 +     * ((noderef * (string option * edgelabel list) list) Symtab.table) (* The edges, grouped by nodes. *)
    3.46 +
    3.47 +and backref = Backref of
    3.48 +       noderef  (* a reference to the node that has defnodes which reference a certain node A *)
    3.49 +     * (unit Symtab.table) (* the names of the defnodes that DIRECTLY reference A. *)
    3.50 +
    3.51 +fun getnode graph noderef = the (Symtab.lookup (graph, noderef))
    3.52 +fun get_nodename (Node (n, _, _ ,_)) = n
    3.53 +fun get_nodedefs (Node (_, _, defs, _)) = defs
    3.54 +fun get_defnode (Node (_, _, defs, _)) defname = Symtab.lookup (defs, defname)
    3.55 +fun get_defnode' graph noderef defname = Symtab.lookup (get_nodedefs (the (Symtab.lookup (graph, noderef))), defname)
    3.56 +fun get_nodename (Node (n, _, _ ,_)) = n
    3.57 +
    3.58 +
    3.59 +(*fun t2list t = rev (Symtab.foldl (fn (l, d) => d::l) ([], t))
    3.60 +fun tmap f t = map (fn (a,b) => (a, f b)) t
    3.61 +fun defnode2data (Defnode (typ, table)) = ("Defnode", typ, t2list table)
    3.62 +fun backref2data (Backref (noderef, table)) = ("Backref", noderef, map fst (t2list table))
    3.63 +fun node2data (Node (s, t, defs, backs)) = ("Node", ("nodename", s), ("nodetyp", t), 
    3.64 +					    ("defs", tmap defnode2data (t2list defs)), ("backs", tmap backref2data (t2list backs)))
    3.65 +fun graph2data g = ("Graph", tmap node2data (t2list g))
    3.66 +*)
    3.67 +
    3.68 +datatype graphaction = Declare of string * typ | Define of string * typ * string * (string * typ) list
    3.69 +
    3.70 +type graph = (graphaction list) * (node Symtab.table)
    3.71 +
    3.72 +val empty = ([], Symtab.empty)
    3.73 +
    3.74 +exception DEFS of string;
    3.75 +exception CIRCULAR of (typ * string * string) list;
    3.76 +exception CLASH of string * string * string;
    3.77 +
    3.78 +fun def_err s = raise (DEFS s)
    3.79 +
    3.80 +fun declare (actions, g) name ty =
    3.81 +    ((Declare (name, ty))::actions, 
    3.82 +     Symtab.update_new ((name, Node (name, Type.varifyT(Type.strip_sorts ty), Symtab.empty, Symtab.empty)), g))
    3.83 +    handle Symtab.DUP _ => def_err "declare: constant is already defined"
    3.84 +
    3.85 +fun rename ty1 ty2 = incr_tvar ((maxidx_of_typ ty1)+1) ty2;  
    3.86 +
    3.87 +fun subst_incr_tvar inc t =
    3.88 +    if (inc > 0) then 
    3.89 +	let
    3.90 +	    val tv = typ_tvars t
    3.91 +	    val t' = incr_tvar inc t
    3.92 +	    fun update_subst (((n,i), _), s) =
    3.93 +		Vartab.update (((n, i), ([], TVar ((n, i+inc), []))), s)
    3.94 +	in
    3.95 +	    (t',List.foldl update_subst Vartab.empty tv)
    3.96 +	end	
    3.97 +    else
    3.98 +	(t, Vartab.empty)
    3.99 +
   3.100 +(* Rename tys2 so that tys2 and tys1 do not have any variables in common any more.
   3.101 +   As a result, return the renamed tys2' and the substitution that takes tys2 to tys2'. *)
   3.102 +fun subst_rename max1 ty2 =
   3.103 +    let
   3.104 +        val max2 = (maxidx_of_typ ty2)
   3.105 +        val (ty2', s) = subst_incr_tvar (max1 + 1) ty2                
   3.106 +    in
   3.107 +	(ty2', s, max1 + max2 + 1)
   3.108 +    end	       
   3.109 +
   3.110 +fun subst s ty = Envir.norm_type s ty
   3.111 +
   3.112 +fun subst_history s history = map (fn (ty, cn, dn) => (subst s ty, cn, dn)) history
   3.113 +
   3.114 +fun is_instance instance_ty general_ty =
   3.115 +    Type.typ_instance Type.empty_tsig (instance_ty, general_ty)
   3.116 +
   3.117 +fun is_instance_r instance_ty general_ty =
   3.118 +    is_instance instance_ty (rename instance_ty general_ty)
   3.119 +
   3.120 +fun unify ty1 ty2 = 
   3.121 +    SOME (fst (Type.unify Type.empty_tsig (Vartab.empty, 0) (ty1, ty2)))
   3.122 +    handle Type.TUNIFY => NONE
   3.123 +
   3.124 +(* 
   3.125 +   Unifies ty1 and ty2, renaming ty1 and ty2 so that they have greater indices than max and so that they
   3.126 +   are different. All indices in ty1 and ty2 are supposed to be less than or equal to max.
   3.127 +   Returns SOME (max', s1, s2), so that s1(ty1) = s2(ty2) and max' is greater or equal than all 
   3.128 +   indices in s1, s2, ty1, ty2.
   3.129 +*)
   3.130 +fun unify_r max ty1 ty2 = 
   3.131 +    let
   3.132 +	val max =  Int.max(max, 0)
   3.133 +	val max1 = max (* >= maxidx_of_typ ty1 *)
   3.134 +	val max2 = max (* >= maxidx_of_typ ty2 *)
   3.135 +	val max = Int.max(max, Int.max (max1, max2))
   3.136 +        val (ty1, s1) = subst_incr_tvar (max+1) ty1
   3.137 +	val (ty2, s2) = subst_incr_tvar (max+max1+2) ty2
   3.138 +        val max = max+max1+max2+2	
   3.139 +	fun merge a b = Vartab.merge (fn _ => false) (a, b)
   3.140 +    in
   3.141 +	case unify ty1 ty2 of
   3.142 +	    NONE => NONE
   3.143 +	  | SOME s => SOME (max, merge s1 s, merge s2 s)
   3.144 +    end
   3.145 +
   3.146 +fun can_be_unified_r ty1 ty2 =
   3.147 +    let
   3.148 +	val ty2 = rename ty1 ty2
   3.149 +    in
   3.150 +	case unify ty1 ty2 of
   3.151 +	    NONE => false
   3.152 +	  | _ => true
   3.153 +    end
   3.154 +
   3.155 +fun can_be_unified ty1 ty2 =
   3.156 +    case unify ty1 ty2 of
   3.157 +	NONE => false
   3.158 +      | _ => true
   3.159 +
   3.160 +fun checkT (Type (a, Ts)) = Type (a, map checkT Ts)
   3.161 +  | checkT (TVar ((a, 0), _)) = TVar ((a, 0), [])
   3.162 +  | checkT (TVar ((a, i), _)) = def_err "type is not clean"
   3.163 +  | checkT (TFree (a, _)) = TVar ((a, 0), [])
   3.164 +
   3.165 +fun forall_table P tab = Symtab.foldl (fn (true, e) => P e | (b, _) => b) (true, tab);
   3.166 +
   3.167 +fun label_ord NONE NONE = EQUAL
   3.168 +  | label_ord NONE (SOME _) = LESS
   3.169 +  | label_ord (SOME _) NONE = GREATER
   3.170 +  | label_ord (SOME l1) (SOME l2) = string_ord (l1,l2)
   3.171 +
   3.172 +fun compare_edges (e1 as (maxidx1, u1, v1, history1)) (e2 as (maxidx2, u2, v2, history2)) =
   3.173 +    let
   3.174 +	val t1 = u1 --> v1
   3.175 +	val t2 = u2 --> v2
   3.176 +    in
   3.177 +	if (is_instance_r t1 t2) then
   3.178 +	    (if is_instance_r t2 t1 then
   3.179 +		 SOME (int_ord (length history2, length history1))
   3.180 +	     else
   3.181 +		 SOME LESS)
   3.182 +	else if (is_instance_r t2 t1) then
   3.183 +	    SOME GREATER
   3.184 +	else
   3.185 +	    NONE
   3.186 +    end
   3.187 +
   3.188 +fun merge_edges_1 (x, []) = []
   3.189 +  | merge_edges_1 (x, (y::ys)) = 
   3.190 +    (case compare_edges x y of
   3.191 +	 SOME LESS => (y::ys)
   3.192 +       | SOME EQUAL => (y::ys)
   3.193 +       | SOME GREATER => merge_edges_1 (x, ys)
   3.194 +       | NONE => y::(merge_edges_1 (x, ys)))
   3.195 +
   3.196 +fun merge_edges xs ys = foldl merge_edges_1 xs ys
   3.197 +
   3.198 +fun pack_edges xs = merge_edges [] xs
   3.199 +
   3.200 +fun merge_labelled_edges [] es = es
   3.201 +  | merge_labelled_edges es [] = es
   3.202 +  | merge_labelled_edges ((l1,e1)::es1) ((l2,e2)::es2) = 
   3.203 +    (case label_ord l1 l2 of
   3.204 +	 LESS => (l1, e1)::(merge_labelled_edges es1 ((l2, e2)::es2))
   3.205 +       | GREATER => (l2, e2)::(merge_labelled_edges ((l1, e1)::es1) es2)
   3.206 +       | EQUAL => (l1, merge_edges e1 e2)::(merge_labelled_edges es1 es2))
   3.207 +
   3.208 +fun defnode_edges_foldl f a defnode =
   3.209 +    let
   3.210 +	val (Defnode (ty, def_edges)) = defnode
   3.211 +	fun g (b, (_, (n, labelled_edges))) =
   3.212 +	    foldl (fn ((s, edges), b') => 
   3.213 +		      (foldl (fn (e, b'') => f ty n s e b'') b' edges))
   3.214 +		  b
   3.215 +		  labelled_edges		  		     
   3.216 +    in
   3.217 +	Symtab.foldl g (a, def_edges)
   3.218 +    end	
   3.219 +
   3.220 +fun define (actions, graph) name ty axname body =
   3.221 +    let
   3.222 +	val ty = checkT ty
   3.223 +	val body = map (fn (n,t) => (n, checkT t)) body		 
   3.224 +	val mainref = name
   3.225 +	val mainnode  = (case Symtab.lookup (graph, mainref) of 
   3.226 +			     NONE => def_err ("constant "^(quote mainref)^" is not declared")
   3.227 +			   | SOME n => n)
   3.228 +	val (Node (n, gty, defs, backs)) = mainnode
   3.229 +	val _ = (if is_instance_r ty gty then () else def_err "type of constant does not match declared type")
   3.230 +	fun check_def (s, Defnode (ty', _)) = 
   3.231 +	    (if can_be_unified_r ty ty' then 
   3.232 +		 raise (CLASH (mainref, axname, s))
   3.233 +	     else if s = axname then
   3.234 +	         def_err "name of axiom is already used for another definition of this constant"
   3.235 +	     else true)
   3.236 +	val _ = forall_table check_def defs		
   3.237 +	(* now we know that the only thing that can prevent acceptance of the definition is a cyclic dependency *)
   3.238 +
   3.239 +	(* body contains the constants that this constant definition depends on. For each element of body,
   3.240 +           the function make_edges_to calculates a group of edges that connect this constant with 
   3.241 +           the constant that is denoted by the element of the body *)
   3.242 +	fun make_edges_to (bodyn, bodyty) =
   3.243 +	    let
   3.244 +		val bnode = 
   3.245 +		    (case Symtab.lookup (graph, bodyn) of 
   3.246 +			 NONE => def_err "body of constant definition references undeclared constant"
   3.247 +		       | SOME x => x)
   3.248 +		val (Node (_, general_btyp, bdefs, bbacks)) = bnode
   3.249 +	    in
   3.250 +		case unify_r 0 bodyty general_btyp of
   3.251 +		    NONE => NONE
   3.252 +		  | SOME (maxidx, sigma1, sigma2) => 
   3.253 +		    SOME (
   3.254 +		    let
   3.255 +			(* For each definition of the constant in the body, 
   3.256 +			   check if the definition unifies with the type of the constant in the body. *)	                
   3.257 +	              fun make_edges ((swallowed, l),(def_name, Defnode (def_ty, _))) =
   3.258 +			  if swallowed then
   3.259 +			      (swallowed, l)
   3.260 +			  else 
   3.261 +			      (case unify_r 0 bodyty def_ty of
   3.262 +				   NONE => (swallowed, l)
   3.263 +				 | SOME (maxidx, sigma1, sigma2) => 
   3.264 +				   (is_instance bodyty def_ty,
   3.265 +				    merge_labelled_edges l [(SOME def_name,[(maxidx, subst sigma1 ty, subst sigma2 def_ty, [])])]))
   3.266 +          	      val (swallowed, edges) = Symtab.foldl make_edges ((false, []), bdefs)
   3.267 +		    in
   3.268 +			if swallowed then 
   3.269 +			    (bodyn, edges)
   3.270 +			else
   3.271 +			    (bodyn, [(NONE, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])])]@edges)
   3.272 +		    end)
   3.273 +	    end 
   3.274 +
   3.275 +	fun update_edges (b as (bodyn, bodyty), edges) =
   3.276 +	    (case make_edges_to b of
   3.277 +		 NONE => edges
   3.278 +	       | SOME m =>
   3.279 +		 (case Symtab.lookup (edges, bodyn) of
   3.280 +		      NONE => Symtab.update ((bodyn, m), edges)
   3.281 +		    | SOME (_, es') => 
   3.282 +		      let 
   3.283 +			  val (_, es) = m
   3.284 +			  val es = merge_labelled_edges es es'
   3.285 +		      in
   3.286 +			  Symtab.update ((bodyn, (bodyn, es)), edges)
   3.287 +		      end
   3.288 +		 )
   3.289 +	    )
   3.290 +
   3.291 +	val edges = foldl update_edges Symtab.empty body
   3.292 +
   3.293 +	fun insert_edge edges (nodename, (defname_opt, edge)) = 
   3.294 +	    let
   3.295 +		val newlink = [(defname_opt, [edge])]
   3.296 +	    in
   3.297 +		case Symtab.lookup (edges, nodename) of
   3.298 +		    NONE => Symtab.update ((nodename, (nodename, newlink)), edges)		    
   3.299 +		  | SOME (_, links) => 
   3.300 +		    let
   3.301 +			val links' = merge_labelled_edges links newlink
   3.302 +		    in
   3.303 +			Symtab.update ((nodename, (nodename, links')), edges)
   3.304 +		    end
   3.305 +	    end				    
   3.306 +
   3.307 +        (* We constructed all direct edges that this defnode has. 
   3.308 +           Now we have to construct the transitive hull by going a single step further. *)
   3.309 +
   3.310 +        val thisDefnode = Defnode (ty, edges)
   3.311 +
   3.312 +	fun make_trans_edges _ noderef defname_opt (max1, alpha1, beta1, history1) edges = 
   3.313 +	    case defname_opt of 
   3.314 +		NONE => edges
   3.315 +	      | SOME defname => 		
   3.316 +		let
   3.317 +		    val defnode = the (get_defnode' graph noderef defname)
   3.318 +		    fun make_trans_edge _ noderef2 defname_opt2 (max2, alpha2, beta2, history2) edges =
   3.319 +			case unify_r (Int.max (max1, max2)) beta1 alpha2 of
   3.320 +			    NONE => edges
   3.321 +			  | SOME (max, sleft, sright) =>
   3.322 +			    insert_edge edges (noderef2, 
   3.323 +					       (defname_opt2, 							  
   3.324 +						(max, subst sleft alpha1, subst sright beta2, 
   3.325 +						 (subst_history sleft history1)@
   3.326 +						 ((subst sleft beta1, noderef, defname)::
   3.327 +						  (subst_history sright history2)))))
   3.328 +		in
   3.329 +		    defnode_edges_foldl make_trans_edge edges defnode
   3.330 +		end
   3.331 +
   3.332 +	val edges = defnode_edges_foldl make_trans_edges edges thisDefnode
   3.333 +
   3.334 +	val thisDefnode = Defnode (ty, edges)
   3.335 +
   3.336 +	(* We also have to add the backreferences that this new defnode induces. *)
   3.337 +	    
   3.338 +	fun hasNONElink ((NONE, _)::_) = true
   3.339 +	  | hasNONElink _ = false
   3.340 +	
   3.341 +	fun install_backref graph noderef pointingnoderef pointingdefname = 
   3.342 +	    let
   3.343 +		val (Node (pname, _, _, _)) = getnode graph pointingnoderef
   3.344 +		val (Node (name, ty, defs, backs)) = getnode graph noderef
   3.345 +	    in
   3.346 +		case Symtab.lookup (backs, pname) of
   3.347 +		    NONE => 
   3.348 +		    let 
   3.349 +			val defnames = Symtab.update ((pointingdefname, ()), Symtab.empty)
   3.350 +			val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs)
   3.351 +		    in
   3.352 +			Symtab.update ((name, Node (name, ty, defs, backs)), graph) 			
   3.353 +		    end
   3.354 +		  | SOME (Backref (pointingnoderef, defnames)) =>
   3.355 +		    let
   3.356 +			val defnames = Symtab.update_new ((pointingdefname, ()), defnames)
   3.357 +			val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs)
   3.358 +		    in
   3.359 +			Symtab.update ((name, Node (name, ty, defs, backs)), graph)
   3.360 +		    end
   3.361 +		    handle Symtab.DUP _ => graph
   3.362 +	    end
   3.363 +
   3.364 +	fun install_backrefs (graph, (_, (noderef, labelled_edges))) =
   3.365 +	    if hasNONElink labelled_edges then
   3.366 +		install_backref graph noderef mainref axname
   3.367 +	    else 
   3.368 +		graph
   3.369 +
   3.370 +        val graph = Symtab.foldl install_backrefs (graph, edges)
   3.371 +
   3.372 +        val (Node (_, _, _, backs)) = getnode graph mainref
   3.373 +	val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update_new ((axname, thisDefnode), defs), backs)), graph)
   3.374 +		    
   3.375 +	(* Now we have to check all backreferences to this node and inform them about the new defnode. 
   3.376 +	   In this section we also check for circularity. *)
   3.377 +        fun update_backrefs ((backs, newedges), (nodename, Backref (noderef, defnames))) =	    
   3.378 +	    let
   3.379 +		val node = getnode graph noderef
   3.380 +		fun update_defs ((defnames, newedges),(defname, _)) =
   3.381 +		    let
   3.382 +			val (Defnode (_, defnode_edges)) = the (get_defnode node defname)
   3.383 +			val (_, labelled_edges) = the (Symtab.lookup (defnode_edges, n))
   3.384 +						      
   3.385 +			(* the type of thisDefnode is ty *)
   3.386 +			fun update (e as (max, alpha, beta, history), (none_edges, this_edges)) = 
   3.387 +			    case unify_r max beta ty of
   3.388 +				NONE => (e::none_edges, this_edges)
   3.389 +			      | SOME (max', s_beta, s_ty) =>
   3.390 +				let
   3.391 +				    val alpha' = subst s_beta alpha
   3.392 +				    val ty' = subst s_ty ty				      
   3.393 +				    val _ = 
   3.394 +					if noderef = mainref andalso defname = axname then
   3.395 +					    (case unify alpha' ty' of
   3.396 +						 NONE => ()
   3.397 +					       | SOME s => raise (CIRCULAR (
   3.398 +								  (subst s alpha', mainref, axname)::
   3.399 +								  (subst_history s (subst_history s_beta history))@
   3.400 +								  [(subst s ty', mainref, axname)])))
   3.401 +					else ()
   3.402 +				    val edge = (max', alpha', ty', subst_history s_beta history)
   3.403 +				in
   3.404 +				    if is_instance_r beta ty then 
   3.405 +					(none_edges, edge::this_edges)
   3.406 +				    else
   3.407 +					(e::none_edges, edge::this_edges)
   3.408 +				end					    			   			    
   3.409 +		    in
   3.410 +			case labelled_edges of 
   3.411 +			    ((NONE, edges)::_) => 
   3.412 +			    let
   3.413 +				val (none_edges, this_edges) = foldl update ([], []) edges
   3.414 +				val defnames = if none_edges = [] then defnames else Symtab.update_new ((defname, ()), defnames) 
   3.415 +			    in
   3.416 +				(defnames, (defname, none_edges, this_edges)::newedges)
   3.417 +			    end			    
   3.418 +			  | _ => def_err "update_defs, internal error, corrupt backrefs"
   3.419 +		    end
   3.420 +		    
   3.421 +		val (defnames, newedges') = Symtab.foldl update_defs ((Symtab.empty, []), defnames)
   3.422 +	    in
   3.423 +		if Symtab.is_empty defnames then 
   3.424 +		    (backs, (noderef, newedges')::newedges)
   3.425 +		else
   3.426 +		    let
   3.427 +			val backs = Symtab.update_new ((nodename, Backref (noderef, defnames)), backs)
   3.428 +		    in
   3.429 +			(backs, newedges)
   3.430 +		    end
   3.431 +	    end
   3.432 +	    
   3.433 +
   3.434 +	val (backs, newedges) = Symtab.foldl update_backrefs ((Symtab.empty, []), backs)
   3.435 +						 
   3.436 +	(* If a Circular exception is thrown then we never reach this point. *)
   3.437 +        (* Ok, the definition is consistent, let's update this node. *)
   3.438 +	val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update ((axname, thisDefnode), defs), backs)), graph)
   3.439 +
   3.440 +        (* Furthermore, update all the other nodes that backreference this node. *)
   3.441 +        fun final_update_backrefs graph noderef defname none_edges this_edges =
   3.442 +	    let
   3.443 +		val node = getnode graph noderef
   3.444 +		val (Node (nodename, nodety, defs, backs)) = node
   3.445 +		val (Defnode (defnode_ty, defnode_edges)) = the (get_defnode node defname)
   3.446 +		val (_, defnode_links) = the (Symtab.lookup (defnode_edges, n))
   3.447 +
   3.448 +		fun update edges none_edges this_edges =
   3.449 +		    let 
   3.450 +			val u = merge_labelled_edges edges [(SOME axname, pack_edges this_edges)]
   3.451 +		    in
   3.452 +			if none_edges = [] then
   3.453 +			    u
   3.454 +			else
   3.455 +			    (NONE, pack_edges none_edges)::u
   3.456 +		    end
   3.457 +		    
   3.458 +		val defnode_links' = 
   3.459 +		    case defnode_links of 
   3.460 +			((NONE, _) :: edges) => update edges none_edges this_edges
   3.461 +		      | edges => update edges none_edges this_edges
   3.462 +		val defnode_edges' = Symtab.update ((n, (mainref, defnode_links')), defnode_edges)
   3.463 +		val defs' = Symtab.update ((defname, Defnode (defnode_ty, defnode_edges')), defs)
   3.464 +	    in
   3.465 +		Symtab.update ((nodename, Node (nodename, nodety, defs', backs)), graph)
   3.466 +	    end
   3.467 +
   3.468 +	val graph = foldl (fn ((noderef, newedges),graph) => foldl (fn ((defname, none_edges, this_edges), graph) =>
   3.469 +           final_update_backrefs graph noderef defname none_edges this_edges) graph newedges) graph newedges		    
   3.470 +
   3.471 +    in	    
   3.472 +	((Define (name, ty, axname, body))::actions, graph)	   
   3.473 +    end 
   3.474 +
   3.475 +    
   3.476 +    fun merge' (Declare (name, ty), g) = (declare g name ty handle _ => g)
   3.477 +      | merge' (Define (name, ty, axname, body), g as (_, graph)) = 
   3.478 +	(case Symtab.lookup (graph, name) of
   3.479 +	     NONE => define g name ty axname body
   3.480 +	   | SOME (Node (_, _, defs, _)) => 
   3.481 +	     (case Symtab.lookup (defs, axname) of
   3.482 +		  NONE => define g name ty axname body
   3.483 +		| SOME _ => g))
   3.484 +	
   3.485 +    fun merge (actions, _) g = foldr merge' g actions
   3.486 +
   3.487 +end;
   3.488 +		
   3.489 +
   3.490 +
   3.491 +(*fun tvar name = TVar ((name, 0), [])
   3.492 +
   3.493 +val bool = Type ("bool", [])
   3.494 +val int = Type ("int", [])
   3.495 +val alpha = tvar "'a"
   3.496 +val beta = tvar "'b"
   3.497 +val gamma = tvar "'c"
   3.498 +fun pair a b = Type ("pair", [a,b])
   3.499 +
   3.500 +val _ = print "make empty"
   3.501 +val g = Defs.empty 
   3.502 +
   3.503 +val _ = print "declare"
   3.504 +val g = Defs.declare g "M" (alpha --> bool)
   3.505 +val g = Defs.declare g "N" (beta --> bool)
   3.506 +
   3.507 +val _ = print "define"
   3.508 +val g = Defs.define g "N" (alpha --> bool) "defN" [("M", alpha --> bool)]
   3.509 +val g = Defs.define g "M" (alpha --> bool) "defM" [("N", int --> alpha)]
   3.510 +
   3.511 +val g = Defs.declare g "0" alpha
   3.512 +val g = Defs.define g "0" (pair alpha beta) "zp" [("0", alpha), ("0", beta)]*)
   3.513 +
   3.514 +
     4.1 --- a/src/Pure/term.ML	Sun May 29 05:23:28 2005 +0200
     4.2 +++ b/src/Pure/term.ML	Sun May 29 12:39:12 2005 +0200
     4.3 @@ -150,6 +150,7 @@
     4.4    val add_term_classes: term * class list -> class list
     4.5    val add_term_consts: term * string list -> string list
     4.6    val term_consts: term -> string list
     4.7 +  val term_constsT: term -> (string * typ) list
     4.8    val add_term_frees: term * term list -> term list
     4.9    val term_frees: term -> term list
    4.10    val add_term_free_names: term * string list -> string list
    4.11 @@ -784,8 +785,6 @@
    4.12          else a :: invent_names used b (n - 1)
    4.13        end;
    4.14  
    4.15 -
    4.16 -
    4.17  (** Consts etc. **)
    4.18  
    4.19  fun add_typ_classes (Type (_, Ts), cs) = foldr add_typ_classes cs Ts
    4.20 @@ -803,8 +802,15 @@
    4.21    | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
    4.22    | add_term_consts (_, cs) = cs;
    4.23  
    4.24 +fun add_term_constsT (Const c, cs) = c::cs
    4.25 +  | add_term_constsT (t $ u, cs) = add_term_constsT (t, add_term_constsT (u, cs))
    4.26 +  | add_term_constsT (Abs (_, _, t), cs) = add_term_constsT (t, cs)
    4.27 +  | add_term_constsT (_, cs) = cs;
    4.28 +
    4.29  fun term_consts t = add_term_consts(t,[]);
    4.30  
    4.31 +fun term_constsT t = add_term_constsT(t,[]);
    4.32 +
    4.33  fun exists_Const P t = let
    4.34          fun ex (Const c      ) = P c
    4.35          |   ex (t $ u        ) = ex t orelse ex u
     5.1 --- a/src/Pure/theory.ML	Sun May 29 05:23:28 2005 +0200
     5.2 +++ b/src/Pure/theory.ML	Sun May 29 12:39:12 2005 +0200
     5.3 @@ -11,7 +11,7 @@
     5.4    exception THEORY of string * theory list
     5.5    val rep_theory: theory ->
     5.6      {sign: Sign.sg,
     5.7 -      const_deps: unit Graph.T,
     5.8 +      const_deps: Defs.graph,
     5.9        final_consts: typ list Symtab.table,
    5.10        axioms: term Symtab.table,
    5.11        oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table,
    5.12 @@ -121,12 +121,10 @@
    5.13  
    5.14  (** datatype theory **)
    5.15  
    5.16 -(*Note: dependencies are only tracked for non-overloaded constant definitions*)
    5.17 -
    5.18  datatype theory =
    5.19    Theory of {
    5.20      sign: Sign.sg,
    5.21 -    const_deps: unit Graph.T,
    5.22 +    const_deps: Defs.graph,
    5.23      final_consts: typ list Symtab.table,
    5.24      axioms: term Symtab.table,
    5.25      oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table,
    5.26 @@ -163,7 +161,7 @@
    5.27  
    5.28  (*partial Pure theory*)
    5.29  val pre_pure =
    5.30 -  make_theory Sign.pre_pure Graph.empty Symtab.empty Symtab.empty Symtab.empty [] [];
    5.31 +  make_theory Sign.pre_pure Defs.empty Symtab.empty Symtab.empty Symtab.empty [] [];
    5.32  
    5.33  
    5.34  
    5.35 @@ -317,7 +315,7 @@
    5.36  
    5.37  (* clash_types, clash_consts *)
    5.38  
    5.39 -(*check if types have common instance (ignoring sorts)*)
    5.40 +(*check if types have common instance (ignoring sorts)
    5.41  
    5.42  fun clash_types ty1 ty2 =
    5.43    let
    5.44 @@ -327,9 +325,9 @@
    5.45  
    5.46  fun clash_consts (c1, ty1) (c2, ty2) =
    5.47    c1 = c2 andalso clash_types ty1 ty2;
    5.48 -
    5.49 +*)
    5.50  
    5.51 -(* clash_defns *)
    5.52 +(* clash_defns 
    5.53  
    5.54  fun clash_defn c_ty (name, tm) =
    5.55    let val (c, ty') = dest_Const (head_of (fst (Logic.dest_equals (Logic.strip_imp_concl tm)))) in
    5.56 @@ -338,6 +336,7 @@
    5.57  
    5.58  fun clash_defns c_ty axms =
    5.59    distinct (List.mapPartial (clash_defn c_ty) axms);
    5.60 +*)
    5.61  
    5.62  
    5.63  (* overloading *)
    5.64 @@ -395,15 +394,22 @@
    5.65    (error_msg msg;
    5.66      error ("The error(s) above occurred in definition " ^ quote (Sign.full_name sg name)));
    5.67  
    5.68 -fun cycle_msg namess = "Cyclic dependency of constants:\n" ^
    5.69 -  cat_lines (map (space_implode " -> " o map quote o rev) namess);
    5.70 +fun pretty_const sg (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.quote (Sign.pretty_typ sg (#1 (Type.freeze_thaw_type ty)))];
    5.71  
    5.72 -fun add_deps (c, cs) deps =
    5.73 -  let fun declare (G, x) = Graph.new_node (x, ()) G handle Graph.DUP _ => G
    5.74 -  in Library.foldl declare (deps, c :: cs) |> Graph.add_deps_acyclic (c, cs) end;
    5.75 +fun cycle_msg sg namess = Pretty.string_of (Pretty.block (((Pretty.str "cyclic dependency found: ") :: Pretty.fbrk :: (
    5.76 +  let      
    5.77 +      fun f last (ty, constname, defname) =  
    5.78 +	  (pretty_const sg (constname, ty)) @ (if last then [] else [Pretty.str (" depends via "^ quote defname^ " on ")])
    5.79 +          	
    5.80 +  in
    5.81 +      foldr (fn (x,r) => (f (r=[]) x)@[Pretty.fbrk]@r) [] namess
    5.82 +  end))))
    5.83  
    5.84  fun check_defn sg overloaded final_consts ((deps, axms), def as (name, tm)) =
    5.85    let
    5.86 +    
    5.87 +    val name = Sign.full_name sg name
    5.88 +      
    5.89      fun is_final (c, ty) =
    5.90        case Symtab.lookup(final_consts,c) of
    5.91          SOME [] => true
    5.92 @@ -422,35 +428,43 @@
    5.93  
    5.94      val (c_ty as (c, ty), rhs) = dest_defn tm
    5.95        handle TERM (msg, _) => err_in_defn sg name msg;
    5.96 -    val c_decl =
    5.97 -      (case Sign.const_type sg c of SOME T => T
    5.98 -      | NONE => err_in_defn sg name ("Undeclared constant " ^ quote c));
    5.99 +
   5.100 +    fun decl deps c = 
   5.101 +	(case Sign.const_type sg c of 
   5.102 +	     SOME T => (Defs.declare deps c T handle _ => deps, T)
   5.103 +	   | NONE => err_in_defn sg name ("Undeclared constant " ^ quote c));
   5.104  
   5.105 -    val clashed = clash_defns c_ty axms;
   5.106 +    val (deps, c_decl) = decl deps c
   5.107 +
   5.108 +    val body = Term.term_constsT rhs
   5.109 +    val deps = foldl (fn ((c, _), deps) => fst (decl deps c)) deps body
   5.110 +
   5.111    in
   5.112 -    if not (null clashed) then
   5.113 -      err_in_defn sg name (Pretty.string_of (Pretty.chunks
   5.114 -        (def_txt (c_ty, " clashes with") :: map (show_defn c) clashed)))
   5.115 -    else if is_final c_ty then
   5.116 +    if is_final c_ty then
   5.117        err_in_defn sg name (Pretty.string_of (Pretty.block
   5.118          ([Pretty.str "The constant",Pretty.brk 1] @
   5.119  	 pretty_const c_ty @
   5.120  	 [Pretty.brk 1,Pretty.str "has been declared final"])))
   5.121      else
   5.122        (case overloading sg c_decl ty of
   5.123 -        NoOverloading =>
   5.124 -          (add_deps (c, Term.term_consts rhs) deps
   5.125 -              handle Graph.CYCLES namess => err_in_defn sg name (cycle_msg namess),
   5.126 -            def :: axms)
   5.127 -      | Useless =>
   5.128 +	 Useless =>
   5.129             err_in_defn sg name (Pretty.string_of (Pretty.chunks
   5.130 -             [Library.setmp show_sorts true def_txt (c_ty, ""), Pretty.str
   5.131 -                 "imposes additional sort constraints on the declared type of the constant"]))
   5.132 -      | Plain =>
   5.133 -         (if not overloaded then warning (Pretty.string_of (Pretty.chunks
   5.134 -           [def_txt (c_ty, ""), Pretty.str ("is strictly less general than the declared type (see "
   5.135 -               ^ quote (Sign.full_name sg name) ^ ")")]))
   5.136 -         else (); (deps, def :: axms)))
   5.137 +	   [Library.setmp show_sorts true def_txt (c_ty, ""), Pretty.str
   5.138 +              "imposes additional sort constraints on the declared type of the constant"]))   
   5.139 +       | ov =>
   5.140 +	 let 
   5.141 +	     val deps' = Defs.define deps c ty name body
   5.142 +		 handle Defs.DEFS s => err_in_defn sg name ("DEFS: "^s) 
   5.143 +		      | Defs.CIRCULAR s => err_in_defn sg name (cycle_msg sg s)
   5.144 +                      | Defs.CLASH (_, def1, def2) => err_in_defn sg name (
   5.145 +			  "clashing definitions "^ quote def1 ^" and "^ quote def2)
   5.146 +	 in
   5.147 +	     ((if ov = Plain andalso not overloaded then
   5.148 +		   warning (Pretty.string_of (Pretty.chunks
   5.149 +		     [def_txt (c_ty, ""), Pretty.str ("is strictly less general than the declared type (see " ^ quote name ^ ")")]))
   5.150 +	       else
   5.151 +		   ()); (deps', def::axms))
   5.152 +	 end)
   5.153    end;
   5.154  
   5.155  
   5.156 @@ -550,8 +564,8 @@
   5.157      val sign' = Sign.prep_ext_merge (map sign_of thys)
   5.158  
   5.159      val depss = map (#const_deps o rep_theory) thys;
   5.160 -    val deps' = Library.foldl (Graph.merge_acyclic (K true)) (hd depss, tl depss)
   5.161 -      handle Graph.CYCLES namess => error (cycle_msg namess);
   5.162 +    val deps' = foldl (uncurry Defs.merge) (hd depss) (tl depss)
   5.163 +      handle Defs.CIRCULAR namess => error (cycle_msg sign' namess);
   5.164  
   5.165      val final_constss = map (#final_consts o rep_theory) thys;
   5.166      val final_consts' =