--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/axclass.ML Thu May 26 16:53:58 1994 +0200
@@ -0,0 +1,247 @@
+(* Title: Pure/axclass.ML
+ ID: $Id$
+ Author: Markus Wenzel, TU Muenchen
+
+User interface for axiomatic type classes.
+
+TODO:
+ arity_tac: FILTER is_arity (?), assume_tac (?) (no?)
+*)
+
+signature AX_CLASS =
+sig
+ structure Tactical: TACTICAL
+ local open Tactical Tactical.Thm in
+ val add_axclass: class * class list -> (string * string) list
+ -> theory -> theory
+ val add_axclass_i: class * class list -> (string * term) list
+ -> theory -> theory
+ val add_instance: string * sort list * class -> string list -> thm list
+ -> tactic option -> theory -> theory
+ val axclass_tac: theory -> tactic
+ end
+end;
+
+functor AxClassFun(structure Logic: LOGIC and Goals: GOALS and Tactic: TACTIC
+ sharing Goals.Tactical = Tactic.Tactical)(*: AX_CLASS *) = (* FIXME *)
+struct
+
+structure Tactical = Goals.Tactical;
+structure Thm = Tactical.Thm;
+structure Sign = Thm.Sign;
+structure Type = Sign.Type;
+
+open Logic Thm Tactical Tactic Goals;
+
+
+(* FIXME -> type.ML *)
+
+structure Type =
+struct
+ open Type;
+
+ fun str_of_sort [c] = c
+ | str_of_sort cs = parents "{" "}" (commas cs);
+
+ fun str_of_dom dom = parents "(" ")" (commas (map str_of_sort dom));
+
+ fun str_of_arity (t, [], S) = t ^ " :: " ^ str_of_sort S
+ | str_of_arity (t, SS, S) =
+ t ^ " :: " ^ str_of_dom SS ^ " " ^ str_of_sort S;
+end;
+
+
+(** add constant definitions **) (* FIXME -> drule.ML (?) *)
+
+(* FIXME fake! *)
+val add_defns = add_axioms;
+val add_defns_i = add_axioms_i;
+
+
+(** utilities **)
+
+(* type vars *)
+
+fun map_typ_frees f (Type (t, tys)) = Type (t, map (map_typ_frees f) tys)
+ | map_typ_frees f (TFree a) = f a
+ | map_typ_frees _ a = a;
+
+val map_term_tfrees = map_term_types o map_typ_frees;
+
+fun aT S = TFree ("'a", S);
+
+
+(* get axioms *)
+
+fun get_ax thy name =
+ Some (get_axiom thy name) handle THEORY _ => None;
+
+val get_axioms = mapfilter o get_ax;
+
+
+(* is_defn *)
+
+fun is_defn thm =
+ (case #prop (rep_thm thm) of
+ Const ("==", _) $ _ $ _ => true
+ | _ => false);
+
+
+
+(** add axiomatic type class **)
+
+(* errors *)
+
+fun err_not_logic c =
+ error ("Axiomatic class " ^ quote c ^ " not subclass of \"logic\"");
+
+fun err_bad_axsort ax c =
+ error ("Sort constraint in axiom " ^ quote ax ^ " not supersort of " ^ quote c);
+
+fun err_bad_tfrees ax =
+ error ("More than one type variable in axiom " ^ quote ax);
+
+
+(* ext_axclass *)
+
+fun ext_axclass prep_axm (class, super_classes) raw_axioms old_thy =
+ let
+ val axioms = map (prep_axm (sign_of old_thy)) raw_axioms;
+ val thy = add_classes [([], class, super_classes)] old_thy;
+ val sign = sign_of thy;
+
+
+ (* prepare abstract axioms *)
+
+ fun abs_axm ax =
+ if null (term_tfrees ax) then
+ mk_implies (mk_inclass (aT logicS, class), ax)
+ else
+ map_term_tfrees (K (aT [class])) ax;
+
+ val abs_axioms = map (apsnd abs_axm) axioms;
+
+
+ (* prepare introduction orule *)
+
+ val _ =
+ if Sign.subsort sign ([class], logicS) then ()
+ else err_not_logic class;
+
+ fun axm_sort (name, ax) =
+ (case term_tfrees ax of
+ [] => []
+ | [(_, S)] =>
+ if Sign.subsort sign ([class], S) then S
+ else err_bad_axsort name class
+ | _ => err_bad_tfrees name);
+
+ val axS = Sign.norm_sort sign (logicC :: flat (map axm_sort axioms));
+
+ val int_axm = close_form o map_term_tfrees (K (aT axS));
+ fun inclass c = mk_inclass (aT axS, c);
+
+ val intro_axm = list_implies
+ (map inclass super_classes @ map (int_axm o snd) axioms, inclass class);
+ in
+ add_axioms_i ((class ^ "I", intro_axm) :: abs_axioms) thy
+ end;
+
+
+(* external interfaces *)
+
+val add_axclass = ext_axclass read_axm;
+val add_axclass_i = ext_axclass cert_axm;
+
+
+
+(** add class instance **)
+
+(* arities as terms *)
+
+fun mk_arity (t, ss, c) =
+ let
+ val names = variantlist (replicate (length ss) "'a", []);
+ val tvars = map (fn a => TVar ((a, 0), logicS)) names;
+ in
+ mk_inclass (Type (t, tvars), c)
+ end;
+
+fun dest_arity tm =
+ let
+ fun err () = raise_term "dest_arity" [tm];
+
+ val (ty, c) = dest_inclass tm handle TERM _ => err ();
+ val (t, tvars) =
+ (case ty of
+ Type (t, tys) => (t, map (fn TVar x => x | _ => err ()) tys)
+ | _ => err ());
+ val ss =
+ if null (gen_duplicates eq_fst tvars)
+ then map snd tvars else err ();
+ in
+ (t, ss, c)
+ end;
+
+
+(* axclass_tac *)
+
+(*repeatedly resolve subgoals of form "(| ty : c_class |)";
+ try "cI" axioms first and use class_triv as last resort*)
+
+fun class_axms thy =
+ let
+ val classes = Sign.classes (sign_of thy);
+ val intros = map (fn c => c ^ "I") classes;
+ in
+ get_axioms thy intros @
+ map (class_triv thy) classes
+ end;
+
+fun axclass_tac thy =
+ REPEAT_FIRST (resolve_tac (class_axms thy));
+
+
+(* prove_arity *)
+
+(*(* FIXME *)
+(* FIXME state sign vs sign (!?) *)
+fun weaker_arity state =
+ all_subsort (ss, #2 (dest_arity (concl_of state)))
+ handle TERM _ => false;
+*)
+
+fun prove_arity thy (arity as (t, ss, c)) thms usr_tac =
+ let
+ val sign = sign_of thy;
+ val all_subsort = forall2 (Sign.subsort sign);
+
+ val arity_goal = cterm_of sign (mk_arity arity);
+
+ val arity_tac =
+ axclass_tac thy THEN
+ TRY (rewrite_goals_tac (filter is_defn thms)) THEN
+ TRY (REPEAT_FIRST (resolve_tac (filter_out is_defn thms))) THEN
+ (if_none usr_tac all_tac);
+
+ val arity_thm = prove_goalw_cterm [] arity_goal (K [arity_tac]);
+
+ val (t', ss', c') = dest_arity (#prop (rep_thm arity_thm))
+ handle TERM _ => error "Result is not an arity";
+ in
+ if t = t' andalso all_subsort (ss, ss') andalso c = c' then ()
+ else error ("Proved different arity: " ^ Type.str_of_arity (t', ss', [c']))
+ end
+ handle ERROR => error ("The error(s) above occurred while trying to prove: " ^
+ Type.str_of_arity (t, ss, [c]));
+
+
+(* external interface *)
+
+fun add_instance (t, ss, c) axms thms usr_tac thy =
+ (prove_arity thy (t, ss, c) (get_axioms thy axms @ thms) usr_tac;
+ add_arities [(t, ss, [c])] thy);
+
+
+end;
+