Infinite chains in definitions are now detected, too.
authorobua
Mon May 30 16:32:47 2005 +0200 (2005-05-30)
changeset 16113692fe6595755
parent 16112 27585e65028b
child 16114 8d453f906e43
Infinite chains in definitions are now detected, too.
src/Pure/defs.ML
src/Pure/theory.ML
     1.1 --- a/src/Pure/defs.ML	Mon May 30 10:25:46 2005 +0200
     1.2 +++ b/src/Pure/defs.ML	Mon May 30 16:32:47 2005 +0200
     1.3 @@ -13,14 +13,15 @@
     1.4  
     1.5      exception DEFS of string
     1.6      exception CIRCULAR of (typ * string * string) list
     1.7 +    exception INFINITE_CHAIN of (typ * string * string) list 
     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, CLASH *)
    1.13 +    val define : graph -> string -> typ -> string -> (string * typ) list -> graph (* exception DEFS, CIRCULAR, INFINITE_CHAIN, CLASH *)
    1.14  
    1.15      (* the first argument should be the smaller graph *)
    1.16 -    val merge : graph -> graph -> graph (* exception CIRCULAR, CLASH *)
    1.17 +    val merge : graph -> graph -> graph (* exception CIRCULAR, INFINITE_CHAIN, CLASH *)
    1.18  
    1.19  end
    1.20  
    1.21 @@ -70,6 +71,7 @@
    1.22  
    1.23  exception DEFS of string;
    1.24  exception CIRCULAR of (typ * string * string) list;
    1.25 +exception INFINITE_CHAIN of (typ * string * string) list;
    1.26  exception CLASH of string * string * string;
    1.27  
    1.28  fun def_err s = raise (DEFS s)
    1.29 @@ -390,7 +392,13 @@
    1.30  				    val _ = 
    1.31  					if noderef = mainref andalso defname = axname then
    1.32  					    (case unify alpha' ty' of
    1.33 -						 NONE => ()
    1.34 +						 NONE => 
    1.35 +						   if (is_instance_r ty' alpha') then
    1.36 +						       raise (INFINITE_CHAIN (
    1.37 +							      (alpha', mainref, axname)::
    1.38 +							      (subst_history s_beta history)@
    1.39 +							      [(ty', mainref, axname)]))
    1.40 +						   else ()
    1.41  					       | SOME s => raise (CIRCULAR (
    1.42  								  (subst s alpha', mainref, axname)::
    1.43  								  (subst_history s (subst_history s_beta history))@
     2.1 --- a/src/Pure/theory.ML	Mon May 30 10:25:46 2005 +0200
     2.2 +++ b/src/Pure/theory.ML	Mon May 30 16:32:47 2005 +0200
     2.3 @@ -396,14 +396,18 @@
     2.4  
     2.5  fun pretty_const sg (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.quote (Sign.pretty_typ sg (#1 (Type.freeze_thaw_type ty)))];
     2.6  
     2.7 -fun cycle_msg sg namess = Pretty.string_of (Pretty.block (((Pretty.str "cyclic dependency found: ") :: Pretty.fbrk :: (
     2.8 -  let      
     2.9 -      fun f last (ty, constname, defname) =  
    2.10 -	  (pretty_const sg (constname, ty)) @ (if last then [] else [Pretty.str (" depends via "^ quote defname^ " on ")])
    2.11 +fun cycle_msg sg (infinite, namess) = 
    2.12 +  let val header = if not (infinite) then "cyclic dependency found: " else "infinite chain found: "
    2.13 +  in
    2.14 +      Pretty.string_of (Pretty.block (((Pretty.str header) :: Pretty.fbrk :: (
    2.15 +        let      
    2.16 +	    fun f last (ty, constname, defname) =  
    2.17 +		(pretty_const sg (constname, ty)) @ (if last then [] else [Pretty.str (" depends via "^ quote defname^ " on ")])
    2.18            	
    2.19 -  in
    2.20 -      foldr (fn (x,r) => (f (r=[]) x)@[Pretty.fbrk]@r) [] namess
    2.21 -  end))))
    2.22 +	in
    2.23 +	    foldr (fn (x,r) => (f (r=[]) x)@[Pretty.fbrk]@r) [] namess
    2.24 +	end))))
    2.25 +  end
    2.26  
    2.27  fun check_defn sg overloaded final_consts ((deps, axms), def as (name, tm)) =
    2.28    let
    2.29 @@ -455,7 +459,8 @@
    2.30  	 let 
    2.31  	     val deps' = Defs.define deps c ty name body
    2.32  		 handle Defs.DEFS s => err_in_defn sg name ("DEFS: "^s) 
    2.33 -		      | Defs.CIRCULAR s => err_in_defn sg name (cycle_msg sg s)
    2.34 +		      | Defs.CIRCULAR s => err_in_defn sg name (cycle_msg sg (false, s))
    2.35 +                      | Defs.INFINITE_CHAIN s => err_in_defn sg name (cycle_msg sg (true, s)) 
    2.36                        | Defs.CLASH (_, def1, def2) => err_in_defn sg name (
    2.37  			  "clashing definitions "^ quote def1 ^" and "^ quote def2)
    2.38  	 in
    2.39 @@ -565,7 +570,8 @@
    2.40  
    2.41      val depss = map (#const_deps o rep_theory) thys;
    2.42      val deps' = foldl (uncurry Defs.merge) (hd depss) (tl depss)
    2.43 -      handle Defs.CIRCULAR namess => error (cycle_msg sign' namess);
    2.44 +      handle Defs.CIRCULAR namess => error (cycle_msg sign' (false, namess))
    2.45 +	   | Defs.INFINITE_CHAIN namess => error (cycle_msg sign' (true, namess))
    2.46  
    2.47      val final_constss = map (#final_consts o rep_theory) thys;
    2.48      val final_consts' =