341 |
341 |
342 fun constrset_of_consts thy cs = |
342 fun constrset_of_consts thy cs = |
343 let |
343 let |
344 val _ = map (fn (c, _) => if (is_some o AxClass.class_of_param thy) c |
344 val _ = map (fn (c, _) => if (is_some o AxClass.class_of_param thy) c |
345 then error ("Is a class parameter: " ^ string_of_const thy c) else ()) cs; |
345 then error ("Is a class parameter: " ^ string_of_const thy c) else ()) cs; |
346 fun no_constr (c, ty) = error ("Not a datatype constructor: " ^ string_of_const thy c |
346 fun no_constr s (c, ty) = error ("Not a datatype constructor:\n" ^ string_of_const thy c |
347 ^ " :: " ^ string_of_typ thy ty); |
347 ^ " :: " ^ string_of_typ thy ty ^ "\n" ^ enclose "(" ")" s); |
348 fun last_typ c_ty ty = |
348 fun last_typ c_ty ty = |
349 let |
349 let |
350 val frees = OldTerm.typ_tfrees ty; |
350 val tfrees = Term.add_tfreesT ty []; |
351 val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) ty |
351 val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) ty |
352 handle TYPE _ => no_constr c_ty |
352 handle TYPE _ => no_constr "bad type" c_ty |
353 val _ = if has_duplicates (eq_fst (op =)) vs then no_constr c_ty else (); |
353 val _ = if has_duplicates (eq_fst (op =)) vs |
354 val _ = if length frees <> length vs then no_constr c_ty else (); |
354 then no_constr "duplicate type variables in datatype" c_ty else (); |
|
355 val _ = if length tfrees <> length vs |
|
356 then no_constr "type variables missing in datatype" c_ty else (); |
355 in (tyco, vs) end; |
357 in (tyco, vs) end; |
356 fun ty_sorts (c, ty) = |
358 fun ty_sorts (c, ty) = |
357 let |
359 let |
358 val ty_decl = (Logic.unvarifyT o Sign.the_const_type thy) c; |
360 val ty_decl = (Logic.unvarifyT o Sign.the_const_type thy) c; |
359 val (tyco, _) = last_typ (c, ty) ty_decl; |
361 val (tyco, _) = last_typ (c, ty) ty_decl; |