better error messages for datatypes not declared Const
authorpaulson
Wed May 15 10:44:58 2002 +0200 (2002-05-15 ago)
changeset 131500c50d13d449a
parent 13149 773657d466cb
child 13151 0f1c6fa846f2
better error messages for datatypes not declared Const
src/ZF/Tools/datatype_package.ML
src/ZF/ind_syntax.ML
     1.1 --- a/src/ZF/Tools/datatype_package.ML	Wed May 15 10:42:32 2002 +0200
     1.2 +++ b/src/ZF/Tools/datatype_package.ML	Wed May 15 10:44:58 2002 +0200
     1.3 @@ -54,7 +54,13 @@
     1.4    val dummy = (*has essential ancestors?*)
     1.5      Theory.requires thy "Datatype" "(co)datatype definitions";
     1.6  
     1.7 -  val rec_names = map (#1 o dest_Const o head_of) rec_tms
     1.8 +  val rec_hds = map head_of rec_tms;
     1.9 +
    1.10 +  val dummy = assert_all is_Const rec_hds
    1.11 +          (fn t => "Datatype set not previously declared as constant: " ^
    1.12 +                   Sign.string_of_term (sign_of thy) t);
    1.13 +
    1.14 +  val rec_names = map (#1 o dest_Const) rec_hds
    1.15    val rec_base_names = map Sign.base_name rec_names
    1.16    val big_rec_base_name = space_implode "_" rec_base_names
    1.17  
     2.1 --- a/src/ZF/ind_syntax.ML	Wed May 15 10:42:32 2002 +0200
     2.2 +++ b/src/ZF/ind_syntax.ML	Wed May 15 10:44:58 2002 +0200
     2.3 @@ -121,8 +121,12 @@
     2.4    definition other than Nat.nat and the datatype sets themselves.
     2.5    FIXME: could insert all constant set expressions, e.g. nat->nat.*)
     2.6  fun data_domain co (rec_tms, con_ty_lists) = 
     2.7 -    let val rec_names = (*nat doesn't have to be added*)
     2.8 -	    "Nat.nat" :: map (#1 o dest_Const o head_of) rec_tms
     2.9 +    let val rec_hds = map head_of rec_tms
    2.10 +        val dummy = assert_all is_Const rec_hds
    2.11 +          (fn t => "Datatype set not previously declared as constant: " ^
    2.12 +                   Sign.string_of_term (sign_of IFOL.thy) t);
    2.13 +        val rec_names = (*nat doesn't have to be added*)
    2.14 +	    "Nat.nat" :: map (#1 o dest_Const) rec_hds
    2.15  	val u = if co then quniv else univ
    2.16  	fun is_OK (Const(a,T)) = not (a mem_string rec_names)
    2.17  	  | is_OK _            = false