src/Pure/sign.ML
changeset 19244 1d7e51d9828b
parent 19099 100bf66d7e85
child 19250 932a50e2332f
     1.1 --- a/src/Pure/sign.ML	Sat Mar 11 16:53:20 2006 +0100
     1.2 +++ b/src/Pure/sign.ML	Sat Mar 11 16:53:23 2006 +0100
     1.3 @@ -161,8 +161,13 @@
     1.4    val cert_prop: theory -> term -> term
     1.5    val no_vars: Pretty.pp -> term -> term
     1.6    val cert_def: Pretty.pp -> term -> (string * typ) * term
     1.7 +  val read_class: theory -> xstring -> class
     1.8    val read_sort': Syntax.syntax -> Context.generic -> string -> sort
     1.9    val read_sort: theory -> string -> sort
    1.10 +  val read_classrel: theory -> xstring * xstring -> class * class
    1.11 +  val cert_classrel: theory -> class * class -> class * class
    1.12 +  val read_arity: theory -> xstring * string list * string -> arity
    1.13 +  val cert_arity: theory -> arity -> arity
    1.14    val read_typ': Syntax.syntax -> Context.generic ->
    1.15      (indexname -> sort option) -> string -> typ
    1.16    val read_typ_syntax': Syntax.syntax -> Context.generic ->
    1.17 @@ -496,7 +501,9 @@
    1.18  
    1.19  (** read and certify entities **)    (*exception ERROR*)
    1.20  
    1.21 -(* sorts *)
    1.22 +(* classes and sorts *)
    1.23 +
    1.24 +fun read_class thy c = certify_class thy (intern_class thy c);
    1.25  
    1.26  fun read_sort' syn context str =
    1.27    let
    1.28 @@ -508,6 +515,26 @@
    1.29  fun read_sort thy str = read_sort' (syn_of thy) (Context.Theory thy) str;
    1.30  
    1.31  
    1.32 +(* class relations *)
    1.33 +
    1.34 +fun prep_classrel prep thy raw_rel =
    1.35 +  let val rel = Library.pairself (prep thy) raw_rel
    1.36 +  in Type.add_classrel (pp thy) [rel] (tsig_of thy); rel end;
    1.37 +
    1.38 +val read_classrel = prep_classrel read_class;
    1.39 +val cert_classrel = prep_classrel certify_class;
    1.40 +
    1.41 +
    1.42 +(* type arities *)
    1.43 +
    1.44 +fun prep_arity prep_tycon prep_sort thy (t, Ss, S) =
    1.45 +  let val arity = (prep_tycon thy t, map (prep_sort thy) Ss, prep_sort thy S)
    1.46 +  in Type.add_arities (pp thy) [arity] (tsig_of thy); arity end;
    1.47 +
    1.48 +val read_arity = prep_arity intern_type read_sort;
    1.49 +val cert_arity = prep_arity (K I) certify_sort;
    1.50 +
    1.51 +
    1.52  (* types *)
    1.53  
    1.54  local