src/Pure/axclass.ML
changeset 404 dd3d3d6467db
child 423 a42892e72854
--- /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;
+