# HG changeset patch
# User haftmann
# Date 1123570481 -7200
# Node ID 415e897405daf5cd7a2471daf61e1c15be463270
# Parent  b4d9b87c102efb4b1d23b22a00bc01d9774bbc5c
(added to repository)

diff -r b4d9b87c102e -r 415e897405da src/Pure/hugsclass.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/hugsclass.ML	Tue Aug 09 08:54:41 2005 +0200
@@ -0,0 +1,359 @@
+(*  Title:      Pure/hugsclass.ML
+    ID:         $Id$
+    Author:     Florian Haftmann, TU Muenchen
+
+Haskell98-like type classes, logically simulated by locales ("hugsclass")
+*)
+
+(*!!! for now, only experimental scratch code !!!*)
+
+signature HUGSCLASS =
+sig
+  val add_hugsclass: bstring -> xstring list -> Locale.element list -> theory -> theory
+(*   val add_hugsclass_i: bstring -> string list -> Locale.element list -> theory -> theory  *)
+
+  val get_locale_for_hugsclass: theory -> string -> string
+  val get_axclass_for_hugsclass: theory -> string -> class
+  val add_members_x: xstring * xstring list -> theory -> theory
+  val add_members: string * string list -> theory -> theory
+  val add_tycons_x: xstring * xstring list -> theory -> theory
+  val add_tycons: string * string list -> theory -> theory
+  val the_members: theory -> class -> string list
+  val the_tycons: theory -> class -> string list
+
+  val is_hugsclass: theory -> class -> bool
+  val get_arities: theory -> sort -> string -> sort list
+  val get_superclasses: theory -> class -> class list
+end;
+
+structure Hugsclass : HUGSCLASS =
+struct
+
+
+
+(** data kind 'Pure/classes' **)
+
+type hugsclass_info = {
+  locale_name: string,
+  axclass_name: string,
+  members: string list,
+  tycons: string list
+};
+
+structure HugsclassesData = TheoryDataFun (
+  struct
+    val name = "Pure/hugsclasses";
+    type T = hugsclass_info Symtab.table;
+    val empty = Symtab.empty;
+    val copy = I;
+    val extend = I;
+    fun merge _ = Symtab.merge (K true);
+    fun print _ tab = (Pretty.writeln o Pretty.chunks) (map Pretty.str (Symtab.keys tab));
+  end
+);
+
+val _ = Context.add_setup [HugsclassesData.init];
+val print_hugsclasses = HugsclassesData.print;
+
+fun lookup_hugsclass_info thy class = Symtab.lookup (HugsclassesData.get thy, class);
+
+fun get_hugsclass_info thy class =
+  case lookup_hugsclass_info thy class
+    of NONE => error ("undeclared hugs class " ^ quote class)
+     | SOME info => info;
+
+fun put_hugsclass_info class info thy =
+  thy
+  |> HugsclassesData.put (Symtab.update ((class, info), HugsclassesData.get thy));
+
+
+(* name mangling *)
+
+fun get_locale_for_hugsclass thy class =
+  #locale_name (get_hugsclass_info thy class)
+
+fun get_axclass_for_hugsclass thy class =
+  #axclass_name (get_hugsclass_info thy class)
+
+
+(* assign members to type classes *)
+
+local
+
+fun gen_add_members prep_class prep_member (raw_class, raw_members_new) thy =
+  let
+    val class = prep_class thy raw_class
+    val members_new = map (prep_member thy) raw_members_new
+    val {locale_name, axclass_name, members, tycons} =
+      get_hugsclass_info thy class
+  in
+    thy
+    |> put_hugsclass_info class {
+         locale_name = locale_name,
+         axclass_name = axclass_name,
+         members = members @ members_new,
+         tycons = tycons
+       }
+  end
+
+in
+
+val add_members_x = gen_add_members Sign.intern_class Sign.intern_const
+val add_members = gen_add_members (K I) (K I)
+
+end
+
+
+(* assign type constructors to type classes *)
+
+local
+
+fun gen_add_tycons prep_class prep_type (raw_class, raw_tycons_new) thy =
+  let
+    val class = prep_class thy raw_class
+    val tycons_new = map (prep_type thy) raw_tycons_new
+    val {locale_name, axclass_name, members, tycons} =
+      get_hugsclass_info thy class
+  in
+    thy
+    |> put_hugsclass_info class {
+         locale_name = locale_name,
+         axclass_name = axclass_name,
+         members = members,
+         tycons = tycons @ tycons_new
+       }
+  end;
+
+in
+
+val add_tycons_x = gen_add_tycons Sign.intern_class Sign.intern_type
+val add_tycons = gen_add_tycons (K I) (K I)
+
+end
+
+
+(* retrieve members *)
+
+val the_members = (#members oo get_hugsclass_info)
+
+
+(* retrieve type constructor associations *)
+
+val the_tycons = (#tycons oo get_hugsclass_info)
+
+
+
+(** class declaration **)
+
+local
+
+fun gen_add_hugsclass prep_class bname raw_superclss raw_locelems thy =
+  let
+    val name_class = Sign.full_name thy bname
+    val name_loc = Sign.full_name thy bname
+    val superclss = map (prep_class thy) raw_superclss
+    val _ = map (get_hugsclass_info thy) superclss
+    val defaultS = Sign.defaultS thy
+    val axsuperclss = case superclss of [] => defaultS
+                                     | _ => superclss
+    val locexpr =
+      superclss
+      |> map (get_locale_for_hugsclass thy) 
+      |> map (Locale.Locale)
+      |> Locale.Merge
+    (* fun inferT_axm pre_tm =
+      let
+        val pp = Sign.pp thy;
+        val (t, _) = Sign.infer_types pp thy (K NONE) (K NONE) [] true ([pre_tm], TFree ("a", []));
+      in t end
+    fun axiom_for members = (bname, inferT_axm
+      (ObjectLogic.assert_propT thy (list_comb (Const (name, dummyT), map (fn (mname, mtyp, _) => Const (mname, mtyp)) members)))) *)
+    fun constify thy (mname, mtyp, _) = Const (Sign.intern_const thy mname, mtyp)
+    fun axiom_for loc members thy = case Sign.const_type thy loc
+      of SOME pred_type => [((bname, 
+         (ObjectLogic.assert_propT thy
+           (list_comb (Const (loc, Type.unvarifyT pred_type), map (constify thy) members)))), [])
+        ]
+       | NONE => (writeln "--- no const_type"; [])
+    fun get_members locname thy =
+      let
+        val ctxt = ProofContext.init thy
+                   |> Locale.read_context_statement (SOME locname) [] []
+                   |> #4
+                   |> `(fn ctxt => ((writeln o commas o ProofContext.fixed_names_of) ctxt; ctxt)) |> snd
+        val ctx' = ProofContext.init thy
+                   |> Locale.read_context_statement (SOME locname) [] []
+                   |> #3
+                   |> `(fn ctxt => ((writeln o commas o ProofContext.fixed_names_of) ctxt; ctxt)) |> snd
+        val fixed = ProofContext.fixed_names_of ctxt
+        fun mk_member fixed = (fixed, (the o ProofContext.default_type ctxt) fixed, NoSyn)
+      in map mk_member fixed end;
+    fun add_constraint class (mname, mtyp, _) thy =
+      let
+        val classes = snd (#classes (Type.rep_tsig (#tsig (Sign.rep_sg thy))))
+        val tfree = case (typ_tfrees o Type.unvarifyT) mtyp
+                    of [(tfree, sort)] => if Sorts.sort_eq classes (sort, defaultS)
+                                          then tfree
+                                          else error ("sort constraint not permitted in member " ^ quote mname)
+                     | _ => error ("no or more than one type variable in declaration for member " ^ quote mname)
+        fun constrain_tfree (tfree, _) = TFree (tfree, [class])
+      in Sign.add_const_constraint_i
+        (Sign.intern_const thy mname, map_type_tfree constrain_tfree mtyp) thy
+      end;
+  in
+    thy
+    |> Locale.add_locale true bname locexpr raw_locelems
+    |> `(fn _ => writeln "(1) added locale") |> snd
+    |> `(get_members name_loc)
+       |-> (fn members =>
+       Sign.add_consts_i members
+    #> `(fn _ => writeln "(2) added members") #> snd
+    #> `(axiom_for name_loc members)
+       #-> (fn axiom =>
+       AxClass.add_axclass_i (bname, axsuperclss) axiom #> fst
+    #> `(fn _ => writeln "(3) added axclass") #> snd
+    #> fold (add_constraint name_class) members
+    #> `(fn _ => writeln "(4) constrained members") #> snd
+    #> add_members (name_class, map #1 members)
+    #> `(fn _ => writeln "(5) added class members") #> snd
+    #> put_hugsclass_info name_class {
+         locale_name = name_loc,
+         axclass_name = name_class,
+         members = [],
+         tycons = []
+       }
+    ))
+  end
+
+in
+
+val add_hugsclass = gen_add_hugsclass (Sign.intern_class);
+val add_hugsclass_i = gen_add_hugsclass (K I);
+
+end;
+
+
+
+(** technical class relations *)
+
+fun is_hugsclass thy = can (the_tycons thy)
+
+fun get_arities thy sort tycons =
+  let
+    val tsig = Type.rep_tsig (#tsig (Sign.rep_sg thy))
+    val clss_arities = (snd (#classes tsig), #arities tsig)
+  in
+    Sorts.mg_domain clss_arities tycons sort
+    |> map (filter (is_hugsclass thy))
+    (*!!! assert -> error on fail *)
+  end
+
+fun get_superclasses thy class =
+  Sorts.direct_supercls (snd (#classes (Type.rep_tsig (#tsig (Sign.rep_sg thy))))) class
+  |> filter (is_hugsclass thy)
+
+
+(** outer syntax **)
+
+local
+
+structure P = OuterParse
+and K = OuterSyntax.Keyword
+
+in
+
+val (classK, extendsK) = ("class", "extends")
+
+val classP =
+  OuterSyntax.command classK "define type class" K.thy_decl (
+    P.name
+    -- Scan.optional (P.$$$ extendsK |-- P.list1 P.xname) []
+    -- Scan.repeat P.locale_element
+    >> (fn (((name, superclss), locelems))
+        => Toplevel.theory (add_hugsclass name superclss locelems))
+  )
+
+val (instanceK, whereK) = ("inst", "where")
+
+val instanceP =
+  OuterSyntax.command instanceK "prove type arity" K.thy_goal ((
+    Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 (P.group "sort" P.xname) --| P.$$$ ")")) []
+    -- P.xname --| P.$$$ "::"
+    -- P.group "class" P.xname
+    -- Scan.optional (P.$$$ whereK |-- Scan.repeat1 P.spec_name) [])
+    >> (fn (((arity, ty), class), defs)
+        =>
+        Toplevel.theory (IsarThy.add_defs (true, defs))
+        #> (AxClass.instance_arity_proof (ty, arity, class)
+            |> (Toplevel.print oo Toplevel.theory_to_proof))
+       )
+  )
+
+val _ = OuterSyntax.add_parsers [classP, instanceP]
+
+val _ = OuterSyntax.add_keywords [extendsK]
+
+end
+
+end
+
+(*
+
+PureThy.add_thms [Thm.no_attributes (intro_name bclass, intro)]
+get_thm thy PureThy.
+
+rename intro rule
+check defs -> should contain any member
+wie syntax extrahieren?
+cases für locales
+
+isomorphism
+
+locale sg = fixes prod assumes assoc: ...
+
+consts prod :: "'a::type => 'a => 'a"
+
+axclass sg < type
+  sg: "sg prod"
+
+constraints prod :: "'a::sg => 'a => 'a"
+
+
+theory Scratch imports Main begin
+
+(* class definition *)
+
+locale sg =
+  fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<degree>" 60)
+  assumes assoc: "(x \<degree> y) \<degree> z = x \<degree> (y \<degree> z)"
+
+classes sg
+consts prod :: "'a::sg \<Rightarrow> 'a \<Rightarrow> 'a"  (infix "\<degree>\<degree>" 60)
+classrel sg < type
+axioms sg: "sg prod"
+
+interpretation sg: sg [prod] by (rule sg)
+
+
+(* abstract reasoning *)
+
+lemma (in sg)
+  bar: "x \<degree> y = x \<degree> y" ..
+
+lemma baz:
+  fixes x :: "'a::sg"
+  shows "x \<degree>\<degree> y = x \<degree>\<degree> y" ..
+
+(* class instantiation *)
+
+interpretation sg_list: sg ["op @"]
+  by (rule sg.intro) (simp only: append_assoc)
+arities list :: (type) sg
+defs (overloaded) prod_list_def: "prod == op @"
+
+interpretation sg_prod: sg ["%p q. (fst p \<degree>\<degree> fst q, snd p \<degree>\<degree> snd q)"]
+  by (rule sg.intro) (simp add: sg.assoc)
+
+arities * :: (sg, sg) sg
+
+*)