src/Pure/logic.ML
changeset 19406 410b9d9bf9a1
parent 19391 4812d28c90a6
child 19425 e0d7d9373faf
     1.1 --- a/src/Pure/logic.ML	Tue Apr 11 16:00:01 2006 +0200
     1.2 +++ b/src/Pure/logic.ML	Tue Apr 11 16:00:02 2006 +0200
     1.3 @@ -34,6 +34,10 @@
     1.4    val class_of_const: string -> class
     1.5    val mk_inclass: typ * class -> term
     1.6    val dest_inclass: term -> typ * class
     1.7 +  val mk_classrel: class * class -> term
     1.8 +  val dest_classrel: term -> class * class
     1.9 +  val mk_arities: string * sort list * sort -> term list
    1.10 +  val dest_arity: term -> string * sort list * class
    1.11    val dest_def: Pretty.pp -> (term -> bool) -> (string -> bool) -> (string -> bool) ->
    1.12      term -> (term * term) * term
    1.13    val abs_def: term -> term * term
    1.14 @@ -178,23 +182,59 @@
    1.15    | dest_type t = raise TERM ("dest_type", [t]);
    1.16  
    1.17  
    1.18 -(** class constraints **)
    1.19 +
    1.20 +(** type classes **)
    1.21 +
    1.22 +(* const names *)
    1.23  
    1.24  val classN = "_class";
    1.25  
    1.26  val const_of_class = suffix classN;
    1.27 +
    1.28  fun class_of_const c = unsuffix classN c
    1.29    handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []);
    1.30  
    1.31 +
    1.32 +(* class constraints *)
    1.33 +
    1.34  fun mk_inclass (ty, c) =
    1.35    Const (const_of_class c, Term.itselfT ty --> propT) $ mk_type ty;
    1.36  
    1.37 -fun dest_inclass (t as Const (c_class, _) $ ty) =
    1.38 -      ((dest_type ty, class_of_const c_class)
    1.39 -        handle TERM _ => raise TERM ("dest_inclass", [t]))
    1.40 +fun dest_inclass (t as Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class)
    1.41    | dest_inclass t = raise TERM ("dest_inclass", [t]);
    1.42  
    1.43  
    1.44 +(* class relations *)
    1.45 +
    1.46 +fun mk_classrel (c1, c2) = mk_inclass (Term.aT [c1], c2);
    1.47 +
    1.48 +fun dest_classrel tm =
    1.49 +  (case dest_inclass tm of
    1.50 +    (TVar (_, [c1]), c2) => (c1, c2)
    1.51 +  | _ => raise TERM ("dest_classrel", [tm]));
    1.52 +
    1.53 +
    1.54 +(* type arities *)
    1.55 +
    1.56 +fun mk_arities (t, Ss, S) =
    1.57 +  let val T = Type (t, ListPair.map TFree (Term.invent_names [] "'a" (length Ss), Ss))
    1.58 +  in map (fn c => mk_inclass (T, c)) S end;
    1.59 +
    1.60 +fun dest_arity tm =
    1.61 +  let
    1.62 +    fun err () = raise TERM ("dest_arity", [tm]);
    1.63 +
    1.64 +    val (ty, c) = dest_inclass tm;
    1.65 +    val (t, tvars) =
    1.66 +      (case ty of
    1.67 +        Type (t, tys) => (t, map dest_TVar tys handle TYPE _ => err ())
    1.68 +      | _ => err ());
    1.69 +    val Ss =
    1.70 +      if has_duplicates (eq_fst (op =)) tvars then err ()
    1.71 +      else map snd tvars;
    1.72 +  in (t, Ss, c) end;
    1.73 +
    1.74 +
    1.75  
    1.76  (** definitions **)
    1.77  
    1.78 @@ -268,6 +308,7 @@
    1.79  fun mk_defpair lhs_rhs = mk_cond_defpair [] lhs_rhs;
    1.80  
    1.81  
    1.82 +
    1.83  (** protected propositions **)
    1.84  
    1.85  val protectC = Const ("prop", propT --> propT);