removed add_classes/classrel/arities (superceded by AxClass.axiomatize_class/classrel/arity);
authorwenzelm
Sun Apr 30 22:50:07 2006 +0200 (2006-04-30)
changeset 1951377ff7cd602d7
parent 19512 94cd541dc8fa
child 19514 1f0218dab849
removed add_classes/classrel/arities (superceded by AxClass.axiomatize_class/classrel/arity);
added primitive_class/classrel/arity;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Sun Apr 30 22:50:06 2006 +0200
     1.2 +++ b/src/Pure/sign.ML	Sun Apr 30 22:50:07 2006 +0200
     1.3 @@ -15,8 +15,6 @@
     1.4    val add_nonterminals: bstring list -> theory -> theory
     1.5    val add_tyabbrs: (bstring * string list * string * mixfix) list -> theory -> theory
     1.6    val add_tyabbrs_i: (bstring * string list * typ * mixfix) list -> theory -> theory
     1.7 -  val add_arities: (xstring * string list * string) list -> theory -> theory
     1.8 -  val add_arities_i: (string * sort list * sort) list -> theory -> theory
     1.9    val add_syntax: (bstring * string * mixfix) list -> theory -> theory
    1.10    val add_syntax_i: (bstring * typ * mixfix) list -> theory -> theory
    1.11    val add_modesyntax: (string * bool) -> (bstring * string * mixfix) list -> theory -> theory
    1.12 @@ -29,10 +27,9 @@
    1.13    val add_abbrevs_i: string * bool -> (bstring * term * mixfix) list -> theory -> theory
    1.14    val add_const_constraint: xstring * string option -> theory -> theory
    1.15    val add_const_constraint_i: string * typ option -> theory -> theory
    1.16 -  val add_classes: (bstring * xstring list) list -> theory -> theory
    1.17 -  val add_classes_i: (bstring * class list) list -> theory -> theory
    1.18 -  val add_classrel: (xstring * xstring) list -> theory -> theory
    1.19 -  val add_classrel_i: (class * class) list -> theory -> theory
    1.20 +  val primitive_class: string * class list -> theory -> theory
    1.21 +  val primitive_classrel: class * class -> theory -> theory
    1.22 +  val primitive_arity: arity -> theory -> theory
    1.23    val add_trfuns:
    1.24      (string * (ast list -> ast)) list *
    1.25      (string * (term list -> term)) list *
    1.26 @@ -527,7 +524,7 @@
    1.27  
    1.28  fun prep_arity prep_tycon prep_sort thy (t, Ss, S) =
    1.29    let val arity = (prep_tycon thy t, map (prep_sort thy) Ss, prep_sort thy S)
    1.30 -  in Type.add_arities (pp thy) [arity] (tsig_of thy); arity end;
    1.31 +  in Type.add_arity (pp thy) arity (tsig_of thy); arity end;
    1.32  
    1.33  val read_arity = prep_arity intern_type read_sort;
    1.34  val cert_arity = prep_arity (K I) certify_sort;
    1.35 @@ -698,19 +695,6 @@
    1.36  val add_tyabbrs_i = fold (gen_add_tyabbr certify_typ_syntax);
    1.37  
    1.38  
    1.39 -(* add type arities *)
    1.40 -
    1.41 -fun gen_add_arities int_type prep_sort arities thy = thy |> map_tsig (fn tsig =>
    1.42 -  let
    1.43 -    fun prep_arity (a, Ss, S) = (int_type thy a, map (prep_sort thy) Ss, prep_sort thy S)
    1.44 -      handle ERROR msg => cat_error msg ("in arity for type " ^ quote a);
    1.45 -    val tsig' = Type.add_arities (pp thy) (map prep_arity arities) tsig;
    1.46 -  in tsig' end);
    1.47 -
    1.48 -val add_arities = gen_add_arities intern_type read_sort;
    1.49 -val add_arities_i = gen_add_arities (K I) certify_sort;
    1.50 -
    1.51 -
    1.52  (* modify syntax *)
    1.53  
    1.54  fun gen_syntax change_gram prep_typ prmode args thy =
    1.55 @@ -799,31 +783,18 @@
    1.56  val add_const_constraint_i = gen_add_constraint (K I) certify_typ;
    1.57  
    1.58  
    1.59 -(* add type classes *)
    1.60 +(* primitive classes and arities *)
    1.61  
    1.62 -fun gen_add_class int_class (bclass, raw_classes) thy =
    1.63 +fun primitive_class (bclass, classes) thy =
    1.64    thy |> map_sign (fn (naming, syn, tsig, consts) =>
    1.65      let
    1.66 -      val classes = map (int_class thy) raw_classes;
    1.67        val syn' = Syntax.extend_consts [bclass] syn;
    1.68 -      val tsig' = Type.add_classes (pp thy) naming [(bclass, classes)] tsig;
    1.69 +      val tsig' = Type.add_class (pp thy) naming (bclass, classes) tsig;
    1.70      in (naming, syn', tsig', consts) end)
    1.71    |> add_consts_i [(Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
    1.72  
    1.73 -val add_classes = fold (gen_add_class intern_class);
    1.74 -val add_classes_i = fold (gen_add_class (K I));
    1.75 -
    1.76 -
    1.77 -(* add to classrel *)
    1.78 -
    1.79 -fun gen_add_classrel int_class raw_pairs thy = thy |> map_tsig (fn tsig =>
    1.80 -  let
    1.81 -    val pairs = map (pairself (int_class thy)) raw_pairs;
    1.82 -    val tsig' = Type.add_classrel (pp thy) pairs tsig;
    1.83 -  in tsig' end);
    1.84 -
    1.85 -val add_classrel = gen_add_classrel intern_class;
    1.86 -val add_classrel_i = gen_add_classrel (K I);
    1.87 +fun primitive_classrel arg thy = thy |> map_tsig (Type.add_classrel (pp thy) arg);
    1.88 +fun primitive_arity arg thy = thy |> map_tsig (Type.add_arity (pp thy) arg);
    1.89  
    1.90  
    1.91  (* add translation functions *)