# HG changeset patch
# User obua
# Date 1117653935 -7200
# Node ID 1af9f5c69745ee84bdd14af8395fcdae7c008d0c
# Parent  ef83d8e097baebfac0678cea8bd9bf7df18a55da
Preliminary version of defs.ML that does not check final consts.

diff -r ef83d8e097ba -r 1af9f5c69745 src/Pure/defs.ML
--- a/src/Pure/defs.ML	Wed Jun 01 19:40:26 2005 +0200
+++ b/src/Pure/defs.ML	Wed Jun 01 21:25:35 2005 +0200
@@ -161,8 +161,6 @@
   | checkT (TVar ((a, i), _)) = def_err "type is not clean"
   | checkT (TFree (a, _)) = TVar ((a, 0), [])
 
-fun forall_table P tab = Symtab.foldl (fn (true, e) => P e | (b, _) => b) (true, tab);
-
 fun label_ord NONE NONE = EQUAL
   | label_ord NONE (SOME _) = LESS
   | label_ord (SOME _) NONE = GREATER
@@ -231,14 +229,14 @@
 		 raise (CLASH (mainref, axname, s))
 	     else if s = axname then
 	         def_err "name of axiom is already used for another definition of this constant"
-	     else true)	
-	val _ = forall_table check_def defs		
-	fun check_final finalty = 
+	     else false)	
+	val _ = Symtab.exists check_def defs
+(*	fun check_final finalty = 
 	    (if can_be_unified_r finalty ty then
 		 raise (FINAL (mainref, finalty))
 	     else
 		 true)
-	val _ = forall check_final finals
+	val _ = forall check_final finals*)
 	
 	(* now we know that the only thing that can prevent acceptance of the definition is a cyclic dependency *)
 
@@ -271,7 +269,7 @@
 				    merge_labelled_edges l [(SOME def_name,[(maxidx, subst sigma1 ty, subst sigma2 def_ty, [])])]))
           	      val (swallowed, edges) = Symtab.foldl make_edges ((false, []), bdefs)
 		    in
-			if swallowed orelse (exists (is_instance_r bodyty) bfinals) then 
+			if swallowed (*orelse (exists (is_instance_r bodyty) bfinals)*) then 
 			    (bodyn, edges)
 			else 
 			    (bodyn, [(NONE, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])])]@edges)
@@ -488,20 +486,30 @@
 
     fun finalize' ((c, ty), graph) = 
       case Symtab.lookup (graph, c) of 
-	  NONE => def_err ("finalize: constant "^(quote c)^" is not declared")
+	  NONE => def_err ("cannot finalize constant "^(quote c)^"; it is not declared")
 	| SOME (Node (noderef, nodety, defs, backs, finals)) =>
 	  let 
-	      val nodety = checkT nodety 
-	  in
-	      if (not (is_instance_r ty nodety)) then
-		  def_err ("finalize: only type instances of the declared constant "^(quote c)^" can be finalized")
-	      else if exists (is_instance_r ty) finals then
+	      val ty = checkT ty
+	      val _ = if (not (is_instance_r ty nodety)) then
+			  def_err ("only type instances of the declared constant "^(quote c)^" can be finalized")
+		      else ()
+	      val _ = Symtab.exists (fn (def_name, Defnode (def_ty, _)) =>  
+					if can_be_unified_r ty def_ty then 
+					    def_err ("cannot finalize constant "^(quote c)^"; clash with definition "^(quote def_name))
+					else 
+					    false)
+				    defs
+	  in				    
+	      if exists (is_instance_r ty) finals then
 		  graph
 	      else 
 	      let
 	          val finals = ty :: finals
 		  val graph = Symtab.update ((noderef, Node(noderef, nodety, defs, backs, finals)), graph)
-		  fun update_backref ((graph, backs), (backrefname, Backref (_, backdefnames))) =
+	      in
+		  graph
+	      end
+(*		  fun update_backref ((graph, backs), (backrefname, Backref (_, backdefnames))) =
 		  let
 		      fun update_backdef ((graph, defnames), (backdefname, _)) = 
 	              let 
@@ -536,10 +544,11 @@
 		  val Node (_, _, defs, _, _) = getnode graph' noderef
 	      in
 		  Symtab.update ((noderef, Node (noderef, nodety, defs, backs', finals)), graph')
-	      end
+	      end*)
 	  end
 	   
-    fun finalize (history, graph) c_ty = ((Finalize c_ty)::history, finalize' (c_ty, graph))
+    fun finalize (history, graph) c_ty = (history, graph)
+	(*((Finalize c_ty)::history, finalize' (c_ty, graph))*)
     
     fun merge' (Declare cty, g) = (declare g cty handle _ => g)
       | merge' (Define (name, ty, axname, body), g as (_, graph)) = 
@@ -551,6 +560,9 @@
 		| SOME _ => g))
       | merge' (Finalize finals, g) = (finalize g finals handle _ => g)
 	
+    fun myrev [] ys = ys
+      | myrev (x::xs) ys = myrev xs (x::ys)
+
     fun merge (actions, _) g = foldr merge' g actions
 
     fun finals (history, graph) =