src/Pure/defs.ML
changeset 16158 2c3565b74b7a
parent 16113 692fe6595755
child 16177 1af9f5c69745
     1.1 --- a/src/Pure/defs.ML	Tue May 31 17:52:10 2005 +0200
     1.2 +++ b/src/Pure/defs.ML	Tue May 31 19:32:41 2005 +0200
     1.3 @@ -14,11 +14,17 @@
     1.4      exception DEFS of string
     1.5      exception CIRCULAR of (typ * string * string) list
     1.6      exception INFINITE_CHAIN of (typ * string * string) list 
     1.7 +    exception FINAL of string * typ
     1.8      exception CLASH of string * string * string
     1.9      
    1.10      val empty : graph
    1.11 -    val declare : graph -> string -> typ -> graph  (* exception DEFS *)
    1.12 -    val define : graph -> string -> typ -> string -> (string * typ) list -> graph (* exception DEFS, CIRCULAR, INFINITE_CHAIN, CLASH *)
    1.13 +    val declare : graph -> string * typ -> graph  (* exception DEFS *)
    1.14 +    val define : graph -> string * typ -> string -> (string * typ) list -> graph 
    1.15 +      (* exception DEFS, CIRCULAR, INFINITE_CHAIN, CLASH, FINAL *)
    1.16 +    
    1.17 +    val finalize : graph -> string * typ -> graph (* exception DEFS *)
    1.18 +
    1.19 +    val finals : graph -> (typ list) Symtab.table
    1.20  
    1.21      (* the first argument should be the smaller graph *)
    1.22      val merge : graph -> graph -> graph (* exception CIRCULAR, INFINITE_CHAIN, CLASH *)
    1.23 @@ -37,33 +43,26 @@
    1.24       * defnode Symtab.table  (* a table of defnodes, each corresponding to 1 definition of the constant for a particular type, 
    1.25                               indexed by axiom name *)
    1.26       * backref Symtab.table (* a table of all back references to this node, indexed by node name *)
    1.27 +     * typ list (* a list of all finalized types *)
    1.28       
    1.29  and defnode = Defnode of
    1.30         typ  (* type of the constant in this particular definition *)
    1.31       * ((noderef * (string option * edgelabel list) list) Symtab.table) (* The edges, grouped by nodes. *)
    1.32  
    1.33  and backref = Backref of
    1.34 -       noderef  (* a reference to the node that has defnodes which reference a certain node A *)
    1.35 +       noderef  (* the name of the node that has defnodes which reference a certain node A *)
    1.36       * (unit Symtab.table) (* the names of the defnodes that DIRECTLY reference A. *)
    1.37  
    1.38  fun getnode graph noderef = the (Symtab.lookup (graph, noderef))
    1.39 -fun get_nodename (Node (n, _, _ ,_)) = n
    1.40 -fun get_nodedefs (Node (_, _, defs, _)) = defs
    1.41 -fun get_defnode (Node (_, _, defs, _)) defname = Symtab.lookup (defs, defname)
    1.42 +fun get_nodename (Node (n, _, _ ,_, _)) = n
    1.43 +fun get_nodedefs (Node (_, _, defs, _, _)) = defs
    1.44 +fun get_defnode (Node (_, _, defs, _, _)) defname = Symtab.lookup (defs, defname)
    1.45  fun get_defnode' graph noderef defname = Symtab.lookup (get_nodedefs (the (Symtab.lookup (graph, noderef))), defname)
    1.46 -fun get_nodename (Node (n, _, _ ,_)) = n
    1.47 -
    1.48 +fun get_nodename (Node (n, _, _ , _, _)) = n
    1.49  
    1.50 -(*fun t2list t = rev (Symtab.foldl (fn (l, d) => d::l) ([], t))
    1.51 -fun tmap f t = map (fn (a,b) => (a, f b)) t
    1.52 -fun defnode2data (Defnode (typ, table)) = ("Defnode", typ, t2list table)
    1.53 -fun backref2data (Backref (noderef, table)) = ("Backref", noderef, map fst (t2list table))
    1.54 -fun node2data (Node (s, t, defs, backs)) = ("Node", ("nodename", s), ("nodetyp", t), 
    1.55 -					    ("defs", tmap defnode2data (t2list defs)), ("backs", tmap backref2data (t2list backs)))
    1.56 -fun graph2data g = ("Graph", tmap node2data (t2list g))
    1.57 -*)
    1.58 -
    1.59 -datatype graphaction = Declare of string * typ | Define of string * typ * string * (string * typ) list
    1.60 +datatype graphaction = Declare of string * typ 
    1.61 +		     | Define of string * typ * string * (string * typ) list
    1.62 +		     | Finalize of string * typ
    1.63  
    1.64  type graph = (graphaction list) * (node Symtab.table)
    1.65  
    1.66 @@ -73,13 +72,14 @@
    1.67  exception CIRCULAR of (typ * string * string) list;
    1.68  exception INFINITE_CHAIN of (typ * string * string) list;
    1.69  exception CLASH of string * string * string;
    1.70 +exception FINAL of string * typ;
    1.71  
    1.72  fun def_err s = raise (DEFS s)
    1.73  
    1.74 -fun declare (actions, g) name ty =
    1.75 -    ((Declare (name, ty))::actions, 
    1.76 -     Symtab.update_new ((name, Node (name, Type.varifyT(Type.strip_sorts ty), Symtab.empty, Symtab.empty)), g))
    1.77 -    handle Symtab.DUP _ => def_err "declare: constant is already defined"
    1.78 +fun declare (actions, g) (cty as (name, ty)) =
    1.79 +    ((Declare cty)::actions, 
    1.80 +     Symtab.update_new ((name, Node (name, Type.varifyT(Type.strip_sorts ty), Symtab.empty, Symtab.empty, [])), g))
    1.81 +    handle Symtab.DUP _ => def_err "constant is already declared"
    1.82  
    1.83  fun rename ty1 ty2 = incr_tvar ((maxidx_of_typ ty1)+1) ty2;  
    1.84  
    1.85 @@ -216,7 +216,7 @@
    1.86  	Symtab.foldl g (a, def_edges)
    1.87      end	
    1.88  
    1.89 -fun define (actions, graph) name ty axname body =
    1.90 +fun define (actions, graph) (name, ty) axname body =
    1.91      let
    1.92  	val ty = checkT ty
    1.93  	val body = map (fn (n,t) => (n, checkT t)) body		 
    1.94 @@ -224,15 +224,22 @@
    1.95  	val mainnode  = (case Symtab.lookup (graph, mainref) of 
    1.96  			     NONE => def_err ("constant "^(quote mainref)^" is not declared")
    1.97  			   | SOME n => n)
    1.98 -	val (Node (n, gty, defs, backs)) = mainnode
    1.99 +	val (Node (n, gty, defs, backs, finals)) = mainnode
   1.100  	val _ = (if is_instance_r ty gty then () else def_err "type of constant does not match declared type")
   1.101  	fun check_def (s, Defnode (ty', _)) = 
   1.102  	    (if can_be_unified_r ty ty' then 
   1.103  		 raise (CLASH (mainref, axname, s))
   1.104  	     else if s = axname then
   1.105  	         def_err "name of axiom is already used for another definition of this constant"
   1.106 -	     else true)
   1.107 +	     else true)	
   1.108  	val _ = forall_table check_def defs		
   1.109 +	fun check_final finalty = 
   1.110 +	    (if can_be_unified_r finalty ty then
   1.111 +		 raise (FINAL (mainref, finalty))
   1.112 +	     else
   1.113 +		 true)
   1.114 +	val _ = forall check_final finals
   1.115 +	
   1.116  	(* now we know that the only thing that can prevent acceptance of the definition is a cyclic dependency *)
   1.117  
   1.118  	(* body contains the constants that this constant definition depends on. For each element of body,
   1.119 @@ -244,7 +251,7 @@
   1.120  		    (case Symtab.lookup (graph, bodyn) of 
   1.121  			 NONE => def_err "body of constant definition references undeclared constant"
   1.122  		       | SOME x => x)
   1.123 -		val (Node (_, general_btyp, bdefs, bbacks)) = bnode
   1.124 +		val (Node (_, general_btyp, bdefs, bbacks, bfinals)) = bnode
   1.125  	    in
   1.126  		case unify_r 0 bodyty general_btyp of
   1.127  		    NONE => NONE
   1.128 @@ -260,13 +267,13 @@
   1.129  			      (case unify_r 0 bodyty def_ty of
   1.130  				   NONE => (swallowed, l)
   1.131  				 | SOME (maxidx, sigma1, sigma2) => 
   1.132 -				   (is_instance bodyty def_ty,
   1.133 +				   (is_instance_r bodyty def_ty,
   1.134  				    merge_labelled_edges l [(SOME def_name,[(maxidx, subst sigma1 ty, subst sigma2 def_ty, [])])]))
   1.135            	      val (swallowed, edges) = Symtab.foldl make_edges ((false, []), bdefs)
   1.136  		    in
   1.137 -			if swallowed then 
   1.138 +			if swallowed orelse (exists (is_instance_r bodyty) bfinals) then 
   1.139  			    (bodyn, edges)
   1.140 -			else
   1.141 +			else 
   1.142  			    (bodyn, [(NONE, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])])]@edges)
   1.143  		    end)
   1.144  	    end 
   1.145 @@ -339,8 +346,8 @@
   1.146  	
   1.147  	fun install_backref graph noderef pointingnoderef pointingdefname = 
   1.148  	    let
   1.149 -		val (Node (pname, _, _, _)) = getnode graph pointingnoderef
   1.150 -		val (Node (name, ty, defs, backs)) = getnode graph noderef
   1.151 +		val (Node (pname, _, _, _, _)) = getnode graph pointingnoderef
   1.152 +		val (Node (name, ty, defs, backs, finals)) = getnode graph noderef
   1.153  	    in
   1.154  		case Symtab.lookup (backs, pname) of
   1.155  		    NONE => 
   1.156 @@ -348,14 +355,14 @@
   1.157  			val defnames = Symtab.update ((pointingdefname, ()), Symtab.empty)
   1.158  			val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs)
   1.159  		    in
   1.160 -			Symtab.update ((name, Node (name, ty, defs, backs)), graph) 			
   1.161 +			Symtab.update ((name, Node (name, ty, defs, backs, finals)), graph) 			
   1.162  		    end
   1.163  		  | SOME (Backref (pointingnoderef, defnames)) =>
   1.164  		    let
   1.165  			val defnames = Symtab.update_new ((pointingdefname, ()), defnames)
   1.166  			val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs)
   1.167  		    in
   1.168 -			Symtab.update ((name, Node (name, ty, defs, backs)), graph)
   1.169 +			Symtab.update ((name, Node (name, ty, defs, backs, finals)), graph)
   1.170  		    end
   1.171  		    handle Symtab.DUP _ => graph
   1.172  	    end
   1.173 @@ -368,8 +375,9 @@
   1.174  
   1.175          val graph = Symtab.foldl install_backrefs (graph, edges)
   1.176  
   1.177 -        val (Node (_, _, _, backs)) = getnode graph mainref
   1.178 -	val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update_new ((axname, thisDefnode), defs), backs)), graph)
   1.179 +        val (Node (_, _, _, backs, _)) = getnode graph mainref
   1.180 +	val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update_new 
   1.181 +          ((axname, thisDefnode), defs), backs, finals)), graph)
   1.182  		    
   1.183  	(* Now we have to check all backreferences to this node and inform them about the new defnode. 
   1.184  	   In this section we also check for circularity. *)
   1.185 @@ -420,7 +428,7 @@
   1.186  			    in
   1.187  				(defnames, (defname, none_edges, this_edges)::newedges)
   1.188  			    end			    
   1.189 -			  | _ => def_err "update_defs, internal error, corrupt backrefs"
   1.190 +			  | _ => sys_error "define: update_defs, internal error, corrupt backrefs"
   1.191  		    end
   1.192  		    
   1.193  		val (defnames, newedges') = Symtab.foldl update_defs ((Symtab.empty, []), defnames)
   1.194 @@ -440,13 +448,14 @@
   1.195  						 
   1.196  	(* If a Circular exception is thrown then we never reach this point. *)
   1.197          (* Ok, the definition is consistent, let's update this node. *)
   1.198 -	val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update ((axname, thisDefnode), defs), backs)), graph)
   1.199 +	val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update 
   1.200 +	  ((axname, thisDefnode), defs), backs, finals)), graph)
   1.201  
   1.202          (* Furthermore, update all the other nodes that backreference this node. *)
   1.203          fun final_update_backrefs graph noderef defname none_edges this_edges =
   1.204  	    let
   1.205  		val node = getnode graph noderef
   1.206 -		val (Node (nodename, nodety, defs, backs)) = node
   1.207 +		val (Node (nodename, nodety, defs, backs, finals)) = node
   1.208  		val (Defnode (defnode_ty, defnode_edges)) = the (get_defnode node defname)
   1.209  		val (_, defnode_links) = the (Symtab.lookup (defnode_edges, n))
   1.210  
   1.211 @@ -467,7 +476,7 @@
   1.212  		val defnode_edges' = Symtab.update ((n, (mainref, defnode_links')), defnode_edges)
   1.213  		val defs' = Symtab.update ((defname, Defnode (defnode_ty, defnode_edges')), defs)
   1.214  	    in
   1.215 -		Symtab.update ((nodename, Node (nodename, nodety, defs', backs)), graph)
   1.216 +		Symtab.update ((nodename, Node (nodename, nodety, defs', backs, finals)), graph)
   1.217  	    end
   1.218  
   1.219  	val graph = foldl (fn ((noderef, newedges),graph) => foldl (fn ((defname, none_edges, this_edges), graph) =>
   1.220 @@ -477,18 +486,78 @@
   1.221  	((Define (name, ty, axname, body))::actions, graph)	   
   1.222      end 
   1.223  
   1.224 +    fun finalize' ((c, ty), graph) = 
   1.225 +      case Symtab.lookup (graph, c) of 
   1.226 +	  NONE => def_err ("finalize: constant "^(quote c)^" is not declared")
   1.227 +	| SOME (Node (noderef, nodety, defs, backs, finals)) =>
   1.228 +	  let 
   1.229 +	      val nodety = checkT nodety 
   1.230 +	  in
   1.231 +	      if (not (is_instance_r ty nodety)) then
   1.232 +		  def_err ("finalize: only type instances of the declared constant "^(quote c)^" can be finalized")
   1.233 +	      else if exists (is_instance_r ty) finals then
   1.234 +		  graph
   1.235 +	      else 
   1.236 +	      let
   1.237 +	          val finals = ty :: finals
   1.238 +		  val graph = Symtab.update ((noderef, Node(noderef, nodety, defs, backs, finals)), graph)
   1.239 +		  fun update_backref ((graph, backs), (backrefname, Backref (_, backdefnames))) =
   1.240 +		  let
   1.241 +		      fun update_backdef ((graph, defnames), (backdefname, _)) = 
   1.242 +	              let 
   1.243 +			  val (backnode as Node (_, backty, backdefs, backbacks, backfinals)) = getnode graph backrefname
   1.244 +			  val (Defnode (def_ty, all_edges)) = the (get_defnode backnode backdefname)						      
   1.245 +			  val (defnames', all_edges') = 
   1.246 +			      case Symtab.lookup (all_edges, noderef) of
   1.247 +				  NONE => sys_error "finalize: corrupt backref"
   1.248 +				| SOME (_, (NONE, edges)::rest) =>
   1.249 +				  let
   1.250 +				      val edges' = List.filter (fn (_, _, beta, _) => not (is_instance_r beta ty)) edges
   1.251 +				  in
   1.252 +				      if edges' = [] then 
   1.253 +					  (defnames, Symtab.update ((noderef, (noderef, rest)), all_edges))
   1.254 +				      else
   1.255 +					  (Symtab.update ((backdefname, ()), defnames), 
   1.256 +					   Symtab.update ((noderef, (noderef, (NONE, edges')::rest)), all_edges))
   1.257 +				  end
   1.258 +			  val defnode' = Defnode (def_ty, all_edges')
   1.259 +			  val backnode' = Node (backrefname, backty, Symtab.update ((backdefname, defnode'), backdefs), 
   1.260 +					   backbacks, backfinals)
   1.261 +		      in
   1.262 +			  (Symtab.update ((backrefname, backnode'), graph), defnames')			  			  
   1.263 +		      end
   1.264 +	  
   1.265 +		      val (graph', defnames') = Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames)
   1.266 +		  in
   1.267 +		      (graph', if Symtab.is_empty defnames' then backs 
   1.268 +			       else Symtab.update ((backrefname, Backref (backrefname, defnames')), backs))
   1.269 +		  end
   1.270 +		  val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs)
   1.271 +		  val Node (_, _, defs, _, _) = getnode graph' noderef
   1.272 +	      in
   1.273 +		  Symtab.update ((noderef, Node (noderef, nodety, defs, backs', finals)), graph')
   1.274 +	      end
   1.275 +	  end
   1.276 +	   
   1.277 +    fun finalize (history, graph) c_ty = ((Finalize c_ty)::history, finalize' (c_ty, graph))
   1.278      
   1.279 -    fun merge' (Declare (name, ty), g) = (declare g name ty handle _ => g)
   1.280 +    fun merge' (Declare cty, g) = (declare g cty handle _ => g)
   1.281        | merge' (Define (name, ty, axname, body), g as (_, graph)) = 
   1.282  	(case Symtab.lookup (graph, name) of
   1.283 -	     NONE => define g name ty axname body
   1.284 -	   | SOME (Node (_, _, defs, _)) => 
   1.285 +	     NONE => define g (name, ty) axname body
   1.286 +	   | SOME (Node (_, _, defs, _, _)) => 
   1.287  	     (case Symtab.lookup (defs, axname) of
   1.288 -		  NONE => define g name ty axname body
   1.289 +		  NONE => define g (name, ty) axname body
   1.290  		| SOME _ => g))
   1.291 +      | merge' (Finalize finals, g) = (finalize g finals handle _ => g)
   1.292  	
   1.293      fun merge (actions, _) g = foldr merge' g actions
   1.294  
   1.295 +    fun finals (history, graph) = 
   1.296 +	Symtab.foldl 
   1.297 +	    (fn (finals, (_, Node(name, _, _, _, ftys))) => Symtab.update_new ((name, ftys), finals))  
   1.298 +	    (Symtab.empty, graph)
   1.299 +
   1.300  end;
   1.301  		
   1.302