src/Pure/defs.ML
author obua
Mon May 30 16:32:47 2005 +0200 (2005-05-30)
changeset 16113 692fe6595755
parent 16108 cf468b93a02e
child 16158 2c3565b74b7a
permissions -rw-r--r--
Infinite chains in definitions are now detected, too.
     1 (*  Title:      Pure/General/defs.ML
     2     ID:         $Id$
     3     Author:     Steven Obua, TU Muenchen
     4 
     5     Checks if definitions preserve consistency of logic by enforcing that there are no cyclic definitions.
     6     The algorithm is described in 
     7     "Cycle-free Overloading in Isabelle", Steven Obua, technical report, to be written :-)
     8 *)
     9 
    10 signature DEFS = sig
    11     
    12     type graph
    13 
    14     exception DEFS of string
    15     exception CIRCULAR of (typ * string * string) list
    16     exception INFINITE_CHAIN of (typ * string * string) list 
    17     exception CLASH of string * string * string
    18     
    19     val empty : graph
    20     val declare : graph -> string -> typ -> graph  (* exception DEFS *)
    21     val define : graph -> string -> typ -> string -> (string * typ) list -> graph (* exception DEFS, CIRCULAR, INFINITE_CHAIN, CLASH *)
    22 
    23     (* the first argument should be the smaller graph *)
    24     val merge : graph -> graph -> graph (* exception CIRCULAR, INFINITE_CHAIN, CLASH *)
    25 
    26 end
    27 
    28 structure Defs :> DEFS = struct
    29 
    30 type tyenv = Type.tyenv
    31 type edgelabel = (int * typ * typ * (typ * string * string) list)
    32 type noderef = string
    33 
    34 datatype node = Node of
    35        string  (* name of constant *)
    36      * typ  (* most general type of constant *)
    37      * defnode Symtab.table  (* a table of defnodes, each corresponding to 1 definition of the constant for a particular type, 
    38                              indexed by axiom name *)
    39      * backref Symtab.table (* a table of all back references to this node, indexed by node name *)
    40      
    41 and defnode = Defnode of
    42        typ  (* type of the constant in this particular definition *)
    43      * ((noderef * (string option * edgelabel list) list) Symtab.table) (* The edges, grouped by nodes. *)
    44 
    45 and backref = Backref of
    46        noderef  (* a reference to the node that has defnodes which reference a certain node A *)
    47      * (unit Symtab.table) (* the names of the defnodes that DIRECTLY reference A. *)
    48 
    49 fun getnode graph noderef = the (Symtab.lookup (graph, noderef))
    50 fun get_nodename (Node (n, _, _ ,_)) = n
    51 fun get_nodedefs (Node (_, _, defs, _)) = defs
    52 fun get_defnode (Node (_, _, defs, _)) defname = Symtab.lookup (defs, defname)
    53 fun get_defnode' graph noderef defname = Symtab.lookup (get_nodedefs (the (Symtab.lookup (graph, noderef))), defname)
    54 fun get_nodename (Node (n, _, _ ,_)) = n
    55 
    56 
    57 (*fun t2list t = rev (Symtab.foldl (fn (l, d) => d::l) ([], t))
    58 fun tmap f t = map (fn (a,b) => (a, f b)) t
    59 fun defnode2data (Defnode (typ, table)) = ("Defnode", typ, t2list table)
    60 fun backref2data (Backref (noderef, table)) = ("Backref", noderef, map fst (t2list table))
    61 fun node2data (Node (s, t, defs, backs)) = ("Node", ("nodename", s), ("nodetyp", t), 
    62 					    ("defs", tmap defnode2data (t2list defs)), ("backs", tmap backref2data (t2list backs)))
    63 fun graph2data g = ("Graph", tmap node2data (t2list g))
    64 *)
    65 
    66 datatype graphaction = Declare of string * typ | Define of string * typ * string * (string * typ) list
    67 
    68 type graph = (graphaction list) * (node Symtab.table)
    69 
    70 val empty = ([], Symtab.empty)
    71 
    72 exception DEFS of string;
    73 exception CIRCULAR of (typ * string * string) list;
    74 exception INFINITE_CHAIN of (typ * string * string) list;
    75 exception CLASH of string * string * string;
    76 
    77 fun def_err s = raise (DEFS s)
    78 
    79 fun declare (actions, g) name ty =
    80     ((Declare (name, ty))::actions, 
    81      Symtab.update_new ((name, Node (name, Type.varifyT(Type.strip_sorts ty), Symtab.empty, Symtab.empty)), g))
    82     handle Symtab.DUP _ => def_err "declare: constant is already defined"
    83 
    84 fun rename ty1 ty2 = incr_tvar ((maxidx_of_typ ty1)+1) ty2;  
    85 
    86 fun subst_incr_tvar inc t =
    87     if (inc > 0) then 
    88 	let
    89 	    val tv = typ_tvars t
    90 	    val t' = incr_tvar inc t
    91 	    fun update_subst (((n,i), _), s) =
    92 		Vartab.update (((n, i), ([], TVar ((n, i+inc), []))), s)
    93 	in
    94 	    (t',List.foldl update_subst Vartab.empty tv)
    95 	end	
    96     else
    97 	(t, Vartab.empty)
    98 
    99 (* Rename tys2 so that tys2 and tys1 do not have any variables in common any more.
   100    As a result, return the renamed tys2' and the substitution that takes tys2 to tys2'. *)
   101 fun subst_rename max1 ty2 =
   102     let
   103         val max2 = (maxidx_of_typ ty2)
   104         val (ty2', s) = subst_incr_tvar (max1 + 1) ty2                
   105     in
   106 	(ty2', s, max1 + max2 + 1)
   107     end	       
   108 
   109 fun subst s ty = Envir.norm_type s ty
   110 
   111 fun subst_history s history = map (fn (ty, cn, dn) => (subst s ty, cn, dn)) history
   112 
   113 fun is_instance instance_ty general_ty =
   114     Type.typ_instance Type.empty_tsig (instance_ty, general_ty)
   115 
   116 fun is_instance_r instance_ty general_ty =
   117     is_instance instance_ty (rename instance_ty general_ty)
   118 
   119 fun unify ty1 ty2 = 
   120     SOME (fst (Type.unify Type.empty_tsig (Vartab.empty, 0) (ty1, ty2)))
   121     handle Type.TUNIFY => NONE
   122 
   123 (* 
   124    Unifies ty1 and ty2, renaming ty1 and ty2 so that they have greater indices than max and so that they
   125    are different. All indices in ty1 and ty2 are supposed to be less than or equal to max.
   126    Returns SOME (max', s1, s2), so that s1(ty1) = s2(ty2) and max' is greater or equal than all 
   127    indices in s1, s2, ty1, ty2.
   128 *)
   129 fun unify_r max ty1 ty2 = 
   130     let
   131 	val max =  Int.max(max, 0)
   132 	val max1 = max (* >= maxidx_of_typ ty1 *)
   133 	val max2 = max (* >= maxidx_of_typ ty2 *)
   134 	val max = Int.max(max, Int.max (max1, max2))
   135         val (ty1, s1) = subst_incr_tvar (max+1) ty1
   136 	val (ty2, s2) = subst_incr_tvar (max+max1+2) ty2
   137         val max = max+max1+max2+2	
   138 	fun merge a b = Vartab.merge (fn _ => false) (a, b)
   139     in
   140 	case unify ty1 ty2 of
   141 	    NONE => NONE
   142 	  | SOME s => SOME (max, merge s1 s, merge s2 s)
   143     end
   144 
   145 fun can_be_unified_r ty1 ty2 =
   146     let
   147 	val ty2 = rename ty1 ty2
   148     in
   149 	case unify ty1 ty2 of
   150 	    NONE => false
   151 	  | _ => true
   152     end
   153 
   154 fun can_be_unified ty1 ty2 =
   155     case unify ty1 ty2 of
   156 	NONE => false
   157       | _ => true
   158 
   159 fun checkT (Type (a, Ts)) = Type (a, map checkT Ts)
   160   | checkT (TVar ((a, 0), _)) = TVar ((a, 0), [])
   161   | checkT (TVar ((a, i), _)) = def_err "type is not clean"
   162   | checkT (TFree (a, _)) = TVar ((a, 0), [])
   163 
   164 fun forall_table P tab = Symtab.foldl (fn (true, e) => P e | (b, _) => b) (true, tab);
   165 
   166 fun label_ord NONE NONE = EQUAL
   167   | label_ord NONE (SOME _) = LESS
   168   | label_ord (SOME _) NONE = GREATER
   169   | label_ord (SOME l1) (SOME l2) = string_ord (l1,l2)
   170 
   171 fun compare_edges (e1 as (maxidx1, u1, v1, history1)) (e2 as (maxidx2, u2, v2, history2)) =
   172     let
   173 	val t1 = u1 --> v1
   174 	val t2 = u2 --> v2
   175     in
   176 	if (is_instance_r t1 t2) then
   177 	    (if is_instance_r t2 t1 then
   178 		 SOME (int_ord (length history2, length history1))
   179 	     else
   180 		 SOME LESS)
   181 	else if (is_instance_r t2 t1) then
   182 	    SOME GREATER
   183 	else
   184 	    NONE
   185     end
   186 
   187 fun merge_edges_1 (x, []) = []
   188   | merge_edges_1 (x, (y::ys)) = 
   189     (case compare_edges x y of
   190 	 SOME LESS => (y::ys)
   191        | SOME EQUAL => (y::ys)
   192        | SOME GREATER => merge_edges_1 (x, ys)
   193        | NONE => y::(merge_edges_1 (x, ys)))
   194 
   195 fun merge_edges xs ys = foldl merge_edges_1 xs ys
   196 
   197 fun pack_edges xs = merge_edges [] xs
   198 
   199 fun merge_labelled_edges [] es = es
   200   | merge_labelled_edges es [] = es
   201   | merge_labelled_edges ((l1,e1)::es1) ((l2,e2)::es2) = 
   202     (case label_ord l1 l2 of
   203 	 LESS => (l1, e1)::(merge_labelled_edges es1 ((l2, e2)::es2))
   204        | GREATER => (l2, e2)::(merge_labelled_edges ((l1, e1)::es1) es2)
   205        | EQUAL => (l1, merge_edges e1 e2)::(merge_labelled_edges es1 es2))
   206 
   207 fun defnode_edges_foldl f a defnode =
   208     let
   209 	val (Defnode (ty, def_edges)) = defnode
   210 	fun g (b, (_, (n, labelled_edges))) =
   211 	    foldl (fn ((s, edges), b') => 
   212 		      (foldl (fn (e, b'') => f ty n s e b'') b' edges))
   213 		  b
   214 		  labelled_edges		  		     
   215     in
   216 	Symtab.foldl g (a, def_edges)
   217     end	
   218 
   219 fun define (actions, graph) name ty axname body =
   220     let
   221 	val ty = checkT ty
   222 	val body = map (fn (n,t) => (n, checkT t)) body		 
   223 	val mainref = name
   224 	val mainnode  = (case Symtab.lookup (graph, mainref) of 
   225 			     NONE => def_err ("constant "^(quote mainref)^" is not declared")
   226 			   | SOME n => n)
   227 	val (Node (n, gty, defs, backs)) = mainnode
   228 	val _ = (if is_instance_r ty gty then () else def_err "type of constant does not match declared type")
   229 	fun check_def (s, Defnode (ty', _)) = 
   230 	    (if can_be_unified_r ty ty' then 
   231 		 raise (CLASH (mainref, axname, s))
   232 	     else if s = axname then
   233 	         def_err "name of axiom is already used for another definition of this constant"
   234 	     else true)
   235 	val _ = forall_table check_def defs		
   236 	(* now we know that the only thing that can prevent acceptance of the definition is a cyclic dependency *)
   237 
   238 	(* body contains the constants that this constant definition depends on. For each element of body,
   239            the function make_edges_to calculates a group of edges that connect this constant with 
   240            the constant that is denoted by the element of the body *)
   241 	fun make_edges_to (bodyn, bodyty) =
   242 	    let
   243 		val bnode = 
   244 		    (case Symtab.lookup (graph, bodyn) of 
   245 			 NONE => def_err "body of constant definition references undeclared constant"
   246 		       | SOME x => x)
   247 		val (Node (_, general_btyp, bdefs, bbacks)) = bnode
   248 	    in
   249 		case unify_r 0 bodyty general_btyp of
   250 		    NONE => NONE
   251 		  | SOME (maxidx, sigma1, sigma2) => 
   252 		    SOME (
   253 		    let
   254 			(* For each definition of the constant in the body, 
   255 			   check if the definition unifies with the type of the constant in the body. *)	                
   256 	              fun make_edges ((swallowed, l),(def_name, Defnode (def_ty, _))) =
   257 			  if swallowed then
   258 			      (swallowed, l)
   259 			  else 
   260 			      (case unify_r 0 bodyty def_ty of
   261 				   NONE => (swallowed, l)
   262 				 | SOME (maxidx, sigma1, sigma2) => 
   263 				   (is_instance bodyty def_ty,
   264 				    merge_labelled_edges l [(SOME def_name,[(maxidx, subst sigma1 ty, subst sigma2 def_ty, [])])]))
   265           	      val (swallowed, edges) = Symtab.foldl make_edges ((false, []), bdefs)
   266 		    in
   267 			if swallowed then 
   268 			    (bodyn, edges)
   269 			else
   270 			    (bodyn, [(NONE, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])])]@edges)
   271 		    end)
   272 	    end 
   273 
   274 	fun update_edges (b as (bodyn, bodyty), edges) =
   275 	    (case make_edges_to b of
   276 		 NONE => edges
   277 	       | SOME m =>
   278 		 (case Symtab.lookup (edges, bodyn) of
   279 		      NONE => Symtab.update ((bodyn, m), edges)
   280 		    | SOME (_, es') => 
   281 		      let 
   282 			  val (_, es) = m
   283 			  val es = merge_labelled_edges es es'
   284 		      in
   285 			  Symtab.update ((bodyn, (bodyn, es)), edges)
   286 		      end
   287 		 )
   288 	    )
   289 
   290 	val edges = foldl update_edges Symtab.empty body
   291 
   292 	fun insert_edge edges (nodename, (defname_opt, edge)) = 
   293 	    let
   294 		val newlink = [(defname_opt, [edge])]
   295 	    in
   296 		case Symtab.lookup (edges, nodename) of
   297 		    NONE => Symtab.update ((nodename, (nodename, newlink)), edges)		    
   298 		  | SOME (_, links) => 
   299 		    let
   300 			val links' = merge_labelled_edges links newlink
   301 		    in
   302 			Symtab.update ((nodename, (nodename, links')), edges)
   303 		    end
   304 	    end				    
   305 
   306         (* We constructed all direct edges that this defnode has. 
   307            Now we have to construct the transitive hull by going a single step further. *)
   308 
   309         val thisDefnode = Defnode (ty, edges)
   310 
   311 	fun make_trans_edges _ noderef defname_opt (max1, alpha1, beta1, history1) edges = 
   312 	    case defname_opt of 
   313 		NONE => edges
   314 	      | SOME defname => 		
   315 		let
   316 		    val defnode = the (get_defnode' graph noderef defname)
   317 		    fun make_trans_edge _ noderef2 defname_opt2 (max2, alpha2, beta2, history2) edges =
   318 			case unify_r (Int.max (max1, max2)) beta1 alpha2 of
   319 			    NONE => edges
   320 			  | SOME (max, sleft, sright) =>
   321 			    insert_edge edges (noderef2, 
   322 					       (defname_opt2, 							  
   323 						(max, subst sleft alpha1, subst sright beta2, 
   324 						 (subst_history sleft history1)@
   325 						 ((subst sleft beta1, noderef, defname)::
   326 						  (subst_history sright history2)))))
   327 		in
   328 		    defnode_edges_foldl make_trans_edge edges defnode
   329 		end
   330 
   331 	val edges = defnode_edges_foldl make_trans_edges edges thisDefnode
   332 
   333 	val thisDefnode = Defnode (ty, edges)
   334 
   335 	(* We also have to add the backreferences that this new defnode induces. *)
   336 	    
   337 	fun hasNONElink ((NONE, _)::_) = true
   338 	  | hasNONElink _ = false
   339 	
   340 	fun install_backref graph noderef pointingnoderef pointingdefname = 
   341 	    let
   342 		val (Node (pname, _, _, _)) = getnode graph pointingnoderef
   343 		val (Node (name, ty, defs, backs)) = getnode graph noderef
   344 	    in
   345 		case Symtab.lookup (backs, pname) of
   346 		    NONE => 
   347 		    let 
   348 			val defnames = Symtab.update ((pointingdefname, ()), Symtab.empty)
   349 			val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs)
   350 		    in
   351 			Symtab.update ((name, Node (name, ty, defs, backs)), graph) 			
   352 		    end
   353 		  | SOME (Backref (pointingnoderef, defnames)) =>
   354 		    let
   355 			val defnames = Symtab.update_new ((pointingdefname, ()), defnames)
   356 			val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs)
   357 		    in
   358 			Symtab.update ((name, Node (name, ty, defs, backs)), graph)
   359 		    end
   360 		    handle Symtab.DUP _ => graph
   361 	    end
   362 
   363 	fun install_backrefs (graph, (_, (noderef, labelled_edges))) =
   364 	    if hasNONElink labelled_edges then
   365 		install_backref graph noderef mainref axname
   366 	    else 
   367 		graph
   368 
   369         val graph = Symtab.foldl install_backrefs (graph, edges)
   370 
   371         val (Node (_, _, _, backs)) = getnode graph mainref
   372 	val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update_new ((axname, thisDefnode), defs), backs)), graph)
   373 		    
   374 	(* Now we have to check all backreferences to this node and inform them about the new defnode. 
   375 	   In this section we also check for circularity. *)
   376         fun update_backrefs ((backs, newedges), (nodename, Backref (noderef, defnames))) =	    
   377 	    let
   378 		val node = getnode graph noderef
   379 		fun update_defs ((defnames, newedges),(defname, _)) =
   380 		    let
   381 			val (Defnode (_, defnode_edges)) = the (get_defnode node defname)
   382 			val (_, labelled_edges) = the (Symtab.lookup (defnode_edges, n))
   383 						      
   384 			(* the type of thisDefnode is ty *)
   385 			fun update (e as (max, alpha, beta, history), (none_edges, this_edges)) = 
   386 			    case unify_r max beta ty of
   387 				NONE => (e::none_edges, this_edges)
   388 			      | SOME (max', s_beta, s_ty) =>
   389 				let
   390 				    val alpha' = subst s_beta alpha
   391 				    val ty' = subst s_ty ty				      
   392 				    val _ = 
   393 					if noderef = mainref andalso defname = axname then
   394 					    (case unify alpha' ty' of
   395 						 NONE => 
   396 						   if (is_instance_r ty' alpha') then
   397 						       raise (INFINITE_CHAIN (
   398 							      (alpha', mainref, axname)::
   399 							      (subst_history s_beta history)@
   400 							      [(ty', mainref, axname)]))
   401 						   else ()
   402 					       | SOME s => raise (CIRCULAR (
   403 								  (subst s alpha', mainref, axname)::
   404 								  (subst_history s (subst_history s_beta history))@
   405 								  [(subst s ty', mainref, axname)])))
   406 					else ()
   407 				    val edge = (max', alpha', ty', subst_history s_beta history)
   408 				in
   409 				    if is_instance_r beta ty then 
   410 					(none_edges, edge::this_edges)
   411 				    else
   412 					(e::none_edges, edge::this_edges)
   413 				end					    			   			    
   414 		    in
   415 			case labelled_edges of 
   416 			    ((NONE, edges)::_) => 
   417 			    let
   418 				val (none_edges, this_edges) = foldl update ([], []) edges
   419 				val defnames = if none_edges = [] then defnames else Symtab.update_new ((defname, ()), defnames) 
   420 			    in
   421 				(defnames, (defname, none_edges, this_edges)::newedges)
   422 			    end			    
   423 			  | _ => def_err "update_defs, internal error, corrupt backrefs"
   424 		    end
   425 		    
   426 		val (defnames, newedges') = Symtab.foldl update_defs ((Symtab.empty, []), defnames)
   427 	    in
   428 		if Symtab.is_empty defnames then 
   429 		    (backs, (noderef, newedges')::newedges)
   430 		else
   431 		    let
   432 			val backs = Symtab.update_new ((nodename, Backref (noderef, defnames)), backs)
   433 		    in
   434 			(backs, newedges)
   435 		    end
   436 	    end
   437 	    
   438 
   439 	val (backs, newedges) = Symtab.foldl update_backrefs ((Symtab.empty, []), backs)
   440 						 
   441 	(* If a Circular exception is thrown then we never reach this point. *)
   442         (* Ok, the definition is consistent, let's update this node. *)
   443 	val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update ((axname, thisDefnode), defs), backs)), graph)
   444 
   445         (* Furthermore, update all the other nodes that backreference this node. *)
   446         fun final_update_backrefs graph noderef defname none_edges this_edges =
   447 	    let
   448 		val node = getnode graph noderef
   449 		val (Node (nodename, nodety, defs, backs)) = node
   450 		val (Defnode (defnode_ty, defnode_edges)) = the (get_defnode node defname)
   451 		val (_, defnode_links) = the (Symtab.lookup (defnode_edges, n))
   452 
   453 		fun update edges none_edges this_edges =
   454 		    let 
   455 			val u = merge_labelled_edges edges [(SOME axname, pack_edges this_edges)]
   456 		    in
   457 			if none_edges = [] then
   458 			    u
   459 			else
   460 			    (NONE, pack_edges none_edges)::u
   461 		    end
   462 		    
   463 		val defnode_links' = 
   464 		    case defnode_links of 
   465 			((NONE, _) :: edges) => update edges none_edges this_edges
   466 		      | edges => update edges none_edges this_edges
   467 		val defnode_edges' = Symtab.update ((n, (mainref, defnode_links')), defnode_edges)
   468 		val defs' = Symtab.update ((defname, Defnode (defnode_ty, defnode_edges')), defs)
   469 	    in
   470 		Symtab.update ((nodename, Node (nodename, nodety, defs', backs)), graph)
   471 	    end
   472 
   473 	val graph = foldl (fn ((noderef, newedges),graph) => foldl (fn ((defname, none_edges, this_edges), graph) =>
   474            final_update_backrefs graph noderef defname none_edges this_edges) graph newedges) graph newedges		    
   475 
   476     in	    
   477 	((Define (name, ty, axname, body))::actions, graph)	   
   478     end 
   479 
   480     
   481     fun merge' (Declare (name, ty), g) = (declare g name ty handle _ => g)
   482       | merge' (Define (name, ty, axname, body), g as (_, graph)) = 
   483 	(case Symtab.lookup (graph, name) of
   484 	     NONE => define g name ty axname body
   485 	   | SOME (Node (_, _, defs, _)) => 
   486 	     (case Symtab.lookup (defs, axname) of
   487 		  NONE => define g name ty axname body
   488 		| SOME _ => g))
   489 	
   490     fun merge (actions, _) g = foldr merge' g actions
   491 
   492 end;
   493 		
   494 
   495 
   496 (*fun tvar name = TVar ((name, 0), [])
   497 
   498 val bool = Type ("bool", [])
   499 val int = Type ("int", [])
   500 val alpha = tvar "'a"
   501 val beta = tvar "'b"
   502 val gamma = tvar "'c"
   503 fun pair a b = Type ("pair", [a,b])
   504 
   505 val _ = print "make empty"
   506 val g = Defs.empty 
   507 
   508 val _ = print "declare"
   509 val g = Defs.declare g "M" (alpha --> bool)
   510 val g = Defs.declare g "N" (beta --> bool)
   511 
   512 val _ = print "define"
   513 val g = Defs.define g "N" (alpha --> bool) "defN" [("M", alpha --> bool)]
   514 val g = Defs.define g "M" (alpha --> bool) "defM" [("N", int --> alpha)]
   515 
   516 val g = Defs.declare g "0" alpha
   517 val g = Defs.define g "0" (pair alpha beta) "zp" [("0", alpha), ("0", beta)]*)
   518 
   519