src/Pure/defs.ML
changeset 16177 1af9f5c69745
parent 16158 2c3565b74b7a
child 16198 cfd070a2cc4d
     1.1 --- a/src/Pure/defs.ML	Wed Jun 01 19:40:26 2005 +0200
     1.2 +++ b/src/Pure/defs.ML	Wed Jun 01 21:25:35 2005 +0200
     1.3 @@ -161,8 +161,6 @@
     1.4    | checkT (TVar ((a, i), _)) = def_err "type is not clean"
     1.5    | checkT (TFree (a, _)) = TVar ((a, 0), [])
     1.6  
     1.7 -fun forall_table P tab = Symtab.foldl (fn (true, e) => P e | (b, _) => b) (true, tab);
     1.8 -
     1.9  fun label_ord NONE NONE = EQUAL
    1.10    | label_ord NONE (SOME _) = LESS
    1.11    | label_ord (SOME _) NONE = GREATER
    1.12 @@ -231,14 +229,14 @@
    1.13  		 raise (CLASH (mainref, axname, s))
    1.14  	     else if s = axname then
    1.15  	         def_err "name of axiom is already used for another definition of this constant"
    1.16 -	     else true)	
    1.17 -	val _ = forall_table check_def defs		
    1.18 -	fun check_final finalty = 
    1.19 +	     else false)	
    1.20 +	val _ = Symtab.exists check_def defs
    1.21 +(*	fun check_final finalty = 
    1.22  	    (if can_be_unified_r finalty ty then
    1.23  		 raise (FINAL (mainref, finalty))
    1.24  	     else
    1.25  		 true)
    1.26 -	val _ = forall check_final finals
    1.27 +	val _ = forall check_final finals*)
    1.28  	
    1.29  	(* now we know that the only thing that can prevent acceptance of the definition is a cyclic dependency *)
    1.30  
    1.31 @@ -271,7 +269,7 @@
    1.32  				    merge_labelled_edges l [(SOME def_name,[(maxidx, subst sigma1 ty, subst sigma2 def_ty, [])])]))
    1.33            	      val (swallowed, edges) = Symtab.foldl make_edges ((false, []), bdefs)
    1.34  		    in
    1.35 -			if swallowed orelse (exists (is_instance_r bodyty) bfinals) then 
    1.36 +			if swallowed (*orelse (exists (is_instance_r bodyty) bfinals)*) then 
    1.37  			    (bodyn, edges)
    1.38  			else 
    1.39  			    (bodyn, [(NONE, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])])]@edges)
    1.40 @@ -488,20 +486,30 @@
    1.41  
    1.42      fun finalize' ((c, ty), graph) = 
    1.43        case Symtab.lookup (graph, c) of 
    1.44 -	  NONE => def_err ("finalize: constant "^(quote c)^" is not declared")
    1.45 +	  NONE => def_err ("cannot finalize constant "^(quote c)^"; it is not declared")
    1.46  	| SOME (Node (noderef, nodety, defs, backs, finals)) =>
    1.47  	  let 
    1.48 -	      val nodety = checkT nodety 
    1.49 -	  in
    1.50 -	      if (not (is_instance_r ty nodety)) then
    1.51 -		  def_err ("finalize: only type instances of the declared constant "^(quote c)^" can be finalized")
    1.52 -	      else if exists (is_instance_r ty) finals then
    1.53 +	      val ty = checkT ty
    1.54 +	      val _ = if (not (is_instance_r ty nodety)) then
    1.55 +			  def_err ("only type instances of the declared constant "^(quote c)^" can be finalized")
    1.56 +		      else ()
    1.57 +	      val _ = Symtab.exists (fn (def_name, Defnode (def_ty, _)) =>  
    1.58 +					if can_be_unified_r ty def_ty then 
    1.59 +					    def_err ("cannot finalize constant "^(quote c)^"; clash with definition "^(quote def_name))
    1.60 +					else 
    1.61 +					    false)
    1.62 +				    defs
    1.63 +	  in				    
    1.64 +	      if exists (is_instance_r ty) finals then
    1.65  		  graph
    1.66  	      else 
    1.67  	      let
    1.68  	          val finals = ty :: finals
    1.69  		  val graph = Symtab.update ((noderef, Node(noderef, nodety, defs, backs, finals)), graph)
    1.70 -		  fun update_backref ((graph, backs), (backrefname, Backref (_, backdefnames))) =
    1.71 +	      in
    1.72 +		  graph
    1.73 +	      end
    1.74 +(*		  fun update_backref ((graph, backs), (backrefname, Backref (_, backdefnames))) =
    1.75  		  let
    1.76  		      fun update_backdef ((graph, defnames), (backdefname, _)) = 
    1.77  	              let 
    1.78 @@ -536,10 +544,11 @@
    1.79  		  val Node (_, _, defs, _, _) = getnode graph' noderef
    1.80  	      in
    1.81  		  Symtab.update ((noderef, Node (noderef, nodety, defs, backs', finals)), graph')
    1.82 -	      end
    1.83 +	      end*)
    1.84  	  end
    1.85  	   
    1.86 -    fun finalize (history, graph) c_ty = ((Finalize c_ty)::history, finalize' (c_ty, graph))
    1.87 +    fun finalize (history, graph) c_ty = (history, graph)
    1.88 +	(*((Finalize c_ty)::history, finalize' (c_ty, graph))*)
    1.89      
    1.90      fun merge' (Declare cty, g) = (declare g cty handle _ => g)
    1.91        | merge' (Define (name, ty, axname, body), g as (_, graph)) = 
    1.92 @@ -551,6 +560,9 @@
    1.93  		| SOME _ => g))
    1.94        | merge' (Finalize finals, g) = (finalize g finals handle _ => g)
    1.95  	
    1.96 +    fun myrev [] ys = ys
    1.97 +      | myrev (x::xs) ys = myrev xs (x::ys)
    1.98 +
    1.99      fun merge (actions, _) g = foldr merge' g actions
   1.100  
   1.101      fun finals (history, graph) =