# HG changeset patch # User wenzelm # Date 769964038 -7200 # Node ID dd3d3d6467dbf9e105747d6576774b882b0ccf8a # Parent 4c66b15777534cf859c91902ebb79d498f84835a axiomatic type class 'package' for Pure (alpha version); diff -r 4c66b1577753 -r dd3d3d6467db src/Pure/axclass.ML --- /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; +