--- a/src/Pure/Tools/class_package.ML Sun Aug 28 10:05:03 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,569 +0,0 @@
-(* 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 CLASS_PACKAGE =
-sig
-(* val add_class: (bstring * xstring list * Locale.element list) -> theory -> theory *)
-(* val add_class_i: bstring -> string list -> Locale.element list -> theory -> theory *)
-
- val get_locale_for_class: theory -> string -> string
- val get_axclass_for_class: 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_class: theory -> class -> bool
- val get_arities: theory -> sort -> string -> sort list
- val get_superclasses: theory -> class -> class list
- type sortcontext = (string * (string * sort)) list
- (* [(identifier, (varname, sort))] *)
- datatype lookup = Instance of class * string * lookup list list
- | Context of (string * int) * (int * class list)
- val derive_sortctxt: theory -> string -> typ -> sortcontext
- val derive_lookup: theory -> sortcontext -> typ * typ -> lookup list list
-end;
-
-structure ClassPackage : CLASS_PACKAGE =
-struct
-
-
-
-(** data kind 'Pure/classes' **)
-
-type class_info = {
- locale_name: string,
- axclass_name: string,
- members: string list,
- tycons: string list
-};
-
-structure ClassesData = TheoryDataFun (
- struct
- val name = "Pure/classes";
- type T = class_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 [ClassesData.init];
-val print_classes = ClassesData.print;
-
-fun lookup_class_info thy class = Symtab.lookup (ClassesData.get thy, class);
-
-fun get_class_info thy class =
- case lookup_class_info thy class
- of NONE => error ("undeclared class " ^ quote class)
- | SOME info => info;
-
-fun put_class_info class info thy =
- thy
- |> ClassesData.put (Symtab.update ((class, info), ClassesData.get thy));
-
-
-(* name mangling *)
-
-fun get_locale_for_class thy class =
- #locale_name (get_class_info thy class)
-
-fun get_axclass_for_class thy class =
- #axclass_name (get_class_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_class_info thy class
- in
- thy
- |> put_class_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 (*local*)
-
-
-(* 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_class_info thy class
- in
- thy
- |> put_class_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 (*local*)
-
-
-(* retrieve members *)
-
-val the_members = (#members oo get_class_info)
-
-
-(* retrieve type constructor associations *)
-
-val the_tycons = (#tycons oo get_class_info)
-
-
-
-(** generic & useful... !!! move this somewhere else ??? **)
-
-fun subst_clsvar thy class subst typ = map_type_tfree (fn (tvar, sort) =>
- if Sorts.sort_eq (Sign.classes_of thy) ([class], sort)
- then subst (tvar, sort)
- else TFree (tvar, sort)
- ) typ
-
-
-
-(** class declaration **)
-
-local
-
-fun gen_add_class prep_class prep_loc
- (bname, raw_superclss, raw_locales, raw_locelems) int thy =
- let
- val name_class = Sign.full_name thy bname
- val name_loc = Sign.full_name thy bname
- val name_intro = name_loc ^ ".intro" (*!!!*)
- val superclss = map (prep_class thy) raw_superclss
- val _ = map (get_class_info thy) superclss
- val defaultS = Sign.defaultS thy
- val axsuperclss = case superclss of [] => defaultS
- | _ => superclss
- val _ = writeln ("superclasses: " ^ commas axsuperclss)
- val superlocales =
- superclss
- |> map (get_locale_for_class thy)
- |> append (map (prep_loc thy) raw_locales)
- val locexpr =
- superlocales
- |> map (Locale.Locale)
- |> Locale.Merge
- fun get_loc_intro thy locname name_intro =
- let
- val ctxt = ProofContext.init thy
- |> Locale.read_context_statement (SOME locname) [] []
- |> #4
- in
- case ProofContext.assumptions_of ctxt
- of [] => NONE
- | _ => SOME (PureThy.get_thm thy (Name name_intro))
- end
- fun constify thy (mname, mtyp, _) = Const (Sign.intern_const thy mname, mtyp)
- fun axiom_for loc members thy = case Sign.const_constraint thy loc
- of SOME pred_type => if is_funtype pred_type
- then [((bname,
- (ObjectLogic.assert_propT thy
- (list_comb (Const (loc, Type.unvarifyT pred_type), map (constify thy) members)))), [])
- ]
- else []
- | NONE => []
- fun get_members thy locname =
- let
- val ctxt = ProofContext.init thy
- |> Locale.read_context_statement (SOME locname) [] []
- |> #4
- 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 remove_supercls_members thy =
- superlocales
- |> map (get_members thy)
- |> fold (fn fxs => fn rem => gen_rems (fn ((x, _, _), (y, _, _)) => x = y) (rem, fxs))
- fun get_members_only thy locname =
- get_members thy locname
- |> remove_supercls_members thy
- fun add_constraint class (mname, mtyp, _) thy =
- let
- val tfree = case (typ_tfrees o Type.unvarifyT) mtyp
- of [(tfree, sort)] => if Sorts.sort_eq (Sign.classes_of thy) (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
- (mname, map_type_tfree constrain_tfree mtyp) thy
- end
- fun setup_interpretation membernames = IsarThy.register_globally (*!!!*)
- (((bname ^ "_interp", []), Locale.Locale name_loc), membernames)
- in
- thy
- |> Locale.add_locale_context true bname locexpr raw_locelems
- |-> (fn (loccontext, elems) =>
- tap (fn _ => writeln "(1) added locale")
- #> `(fn thy => get_members_only thy name_loc)
- #-> (fn members =>
- Sign.add_consts_i members
- #> `(fn thy => map (fn (n, t, m) => (Sign.intern_const thy n, t, m)) members)
- #-> (fn intern_members =>
- tap (fn _ => writeln "(2) added members")
- #> `(fn thy => get_loc_intro thy name_loc name_intro)
- #-> (fn intro =>
- tap (fn _ => writeln "(3) axiom prep")
- #> `(axiom_for name_loc intern_members)
- #-> (fn axiom =>
-(* `(Sign.restore_naming) *)
-(* #-> (fn restore_naming => *)
-(* Sign.add_path "class" *)
- tap (fn thy => writeln ("(4) axiom: " ^
- commas (map (Sign.string_of_term thy o snd o fst) axiom)))
- #> AxClass.add_axclass_i (bname, axsuperclss) axiom #> fst
- #> tap (fn _ => writeln "(5) added axclass")
- #> (if is_some intro then PureThy.add_thms [Thm.no_attributes (bname ^ "_intro", the intro)] #> fst else I)
- #> tap (fn _ => writeln "(6) re-introduced intro")
- #> fold (add_constraint name_class) intern_members
-(* #> restore_naming *)
- #> tap (fn _ => writeln "(7) constrained members")
- #> put_class_info name_class {
- locale_name = name_loc,
- axclass_name = name_class,
- members = map #1 intern_members,
- tycons = []
- }
- #> tap (fn _ => writeln "(8) added class data/members")
- #> setup_interpretation (map (SOME o #1) intern_members) int
- )))))
- end
-
-in
-
-val add_class = gen_add_class (Sign.intern_class) (Locale.intern);
-
-end (*local*)
-
-
-
-(** instance definition **)
-
-local
-
-fun read_check_memberdefs thy class tycon arity raw_defs =
- let
- val pp = Sign.pp thy
- val thy_temp =
- thy
- |> Theory.copy
- |> Sign.add_arities_i [(tycon, arity, [class])]
- |> `(fn thy => Sorts.mg_domain (Sign.classes_arities_of thy) tycon [class])
- |> snd
- val _ = writeln "temp"
- fun read_check_memberdef ((raw_bname, raw_term), attr) members =
- let
- val _ = writeln ("reading " ^ class ^ " - " ^ tycon)
- val _ = (writeln o commas o map (Sign.string_of_sort thy_temp)) (Sorts.mg_domain (Sign.classes_arities_of thy_temp) tycon [class])
- val _ = writeln (raw_bname ^ ": " ^ raw_term)
- val term = Sign.read_prop thy_temp raw_term
- val _ = writeln "read"
- val ((const, typ_def), rhs) = Theory.dest_def pp term handle TERM (msg, _) => error msg
- val _ = if member (op =) members const
- then {}
- else error ("superfluos definition: " ^ quote const)
- val typ_decl = Sign.the_const_constraint thy_temp const
- val typ_arity = Type (tycon, map (fn sort => TFree ("", sort)) arity)
- val typ_inst = subst_clsvar thy_temp class (fn _ => typ_arity) typ_decl
- val _ = if Sign.typ_instance thy_temp (typ_inst, typ_def)
- andalso Sign.typ_instance thy_temp (typ_def, typ_inst)
- then {}
- else error ("member definition " ^ quote const
- ^ " does not have required type signature: expected "
- ^ (quote o Sign.string_of_typ thy_temp) typ_inst ^ ", got "
- ^ (quote o Sign.string_of_typ thy_temp) typ_decl)
- val bname = case raw_bname
- of "" => const ^ "_" ^ tycon
- | bname => bname
- val members' = remove (op =) const members
- val _ = (writeln o commas o map (Sign.string_of_sort thy)) (Sorts.mg_domain (Sign.classes_arities_of thy) tycon [class])
- in (((bname, term), attr), members') end
- in
- the_members thy_temp class
- |> fold_map read_check_memberdef raw_defs
- ||> (fn [] => I
- | members => error ("missing class member definitions: " ^ (commas o map quote) members))
- |> fst
- end
-
-in
-
-fun instance_arity_proof_ext (raw_ty, raw_arity, raw_class, raw_defs) int thy =
- let
- val class = Sign.intern_class thy raw_class
- val tycon = Sign.intern_type thy raw_ty
- val arity = map (Sign.read_sort thy) raw_arity
- val _ = writeln ("(1) mangled " ^ class ^ " - " ^ tycon)
- in
- thy
- |> `(fn thy => read_check_memberdefs thy class tycon arity raw_defs)
- |-> (fn defs =>
- `(fn _ => writeln ("(2) checked")) #> snd
-(*!!! attributes #> IsarThy.add_defs_i (true, defs) *)
- #> Theory.add_defs_i true (map fst defs)
- #> `(fn _ => writeln ("(3) added")) #> snd
- #> AxClass.instance_arity_proof (raw_ty, raw_arity, raw_class)
- (add_tycons (class, [tycon])) int
- )
- end
-
-end (*local*)
-
-
-
-(** code generation suppport (dictionaries) *)
-
-(* filtering non-hugs classes *)
-
-fun is_class thy = is_some o lookup_class_info thy
-
-fun filter_class thy = filter (is_class thy)
-
-fun assert_class thy class =
- if is_class thy class then class
- else error ("not a class: " ^ quote class)
-
-fun get_arities thy sort tycon =
- Sorts.mg_domain (Sign.classes_arities_of thy) tycon sort
- |> (map o map) (assert_class thy)
-
-fun get_superclasses thy class =
- Sorts.superclasses (Sign.classes_of thy) class
- |> filter_class thy
-
-
-(* sortcontext handling *)
-
-type sortcontext = (string * (string * sort)) list
-
-fun derive_sortctxt_proto thy typ =
- typ
- |> Type.unvarifyT
- |> typ_tfrees
- |> map (fn (v, s) => (v, filter_class thy s))
- |> filter (fn (_, []) => false | _ => true)
-
-fun derive_sortctxt thy sctxtparm typ =
- typ
- |> derive_sortctxt_proto thy
- |> map (pair sctxtparm)
-
-datatype lookup = Instance of class * string * lookup list list
- | Context of (string * int) * (int * class list)
-
-fun derive_lookup thy sctxt_use (raw_typ_def, raw_typ_use) =
- let
- val typ_def = Type.varifyT raw_typ_def
- val typ_use = Type.varifyT raw_typ_use
- val sanatize_sort = filter_class thy
- val match_tab = Sign.typ_match thy (typ_def, typ_use) Vartab.empty
- fun tab_lookup vname = (the o Vartab.lookup) (match_tab, (vname, 0))
- fun get_supercls_derivation (subclasses, superclass) =
- (the oo get_first) (fn subclass =>
- Sorts.class_le_path (Sign.classes_of thy) (subclass, superclass)
- ) subclasses
- fun mk_cls_deriv thy subclasses superclass =
- case get_supercls_derivation (subclasses, superclass)
- of (subclass::deriv) => (find_index_eq subclass subclasses, deriv)
- fun mk_lookup (sort_def, (Type (tycon, tyargs))) =
- let
- val arity_lookup = map2 mk_lookup
- (map sanatize_sort (Sorts.mg_domain (Sign.classes_arities_of thy) tycon sort_def), tyargs)
- in
- map (fn class => Instance (class, tycon, arity_lookup)) sort_def
- end
- | mk_lookup (sort_def, TVar ((vname, _), sort_use)) =
- let
- val vidx = find_index_eq vname (map (fst o snd) sctxt_use)
- val sctxtparm = #1 (List.nth (sctxt_use, vidx))
- in
- map (fn (class) => Context ((sctxtparm, vidx), mk_cls_deriv thy sort_use class)) sort_def
- end
- in
- derive_sortctxt_proto thy raw_typ_def
- |> map #1
- |> map tab_lookup
- |> map (apfst sanatize_sort)
- |> filter (fn ([], _) => false | _ => true)
- |> map mk_lookup
- end
-
-
-
-(** outer syntax **)
-
-local
-
-structure P = OuterParse
-and K = OuterKeyword
-
-in
-
-val (classK, extendsK, importingK) = ("Xclass", "Xextends", "Ximporting")
-
-val classP =
-(* OuterSyntax.command classK "define class" K.thy_decl ( *)
- OuterSyntax.command classK "define class" K.thy_goal (
- P.name
- -- Scan.optional (P.$$$ extendsK |-- P.list1 P.xname) []
- -- Scan.optional (P.$$$ importingK |-- P.list1 P.xname) []
- -- Scan.repeat1 P.locale_element
- >> (fn (((name, superclasses), locales), locelems)
-(* => Toplevel.theory (add_class (name, superclss, locelems))) *)
- => (Toplevel.print oo Toplevel.theory_to_proof)
- (add_class (name, superclasses, locales, locelems)))
- )
-
-val (instanceK, whereK) = ("Xinst", "Xwhere")
-
-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_opt_name) [])
- >> (fn (((arity, ty), class), defs)
- => (Toplevel.print oo Toplevel.theory_to_proof)
- (instance_arity_proof_ext (ty, arity, class, defs))
- )
- )
-
-val _ = OuterSyntax.add_parsers [classP, instanceP]
-
-val _ = OuterSyntax.add_keywords [extendsK, whereK]
-
-val classcgK = "codegen_class"
-
-fun classcg raw_class raw_members raw_tycons thy =
- let
- val class = Sign.intern_class thy raw_class
- in
- thy
- |> put_class_info class {
- locale_name = "",
- axclass_name = class,
- members = [],
- tycons = []
- }
- |> add_members_x (class, raw_members)
- |> add_tycons_x (class, raw_tycons)
- end
-
-val classcgP =
- OuterSyntax.command classcgK "codegen data for classes" K.thy_decl (
- P.xname
- -- ((P.$$$ "\\<Rightarrow>" || P.$$$ "=>") |-- (P.list1 P.name))
- -- (Scan.optional ((P.$$$ "\\<Rightarrow>" || P.$$$ "=>") |-- (P.list1 P.name)) [])
- >> (fn ((name, tycons), members) => (Toplevel.theory (classcg name members tycons)))
- )
-
-val _ = OuterSyntax.add_parsers [classcgP];
-
-end (*local*)
-
-end
-
-(*
-
-
-
-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
-
- (* 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)))) *)
-
-
-*)
-
--- a/src/Pure/Tools/iml_package.ML Sun Aug 28 10:05:03 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,107 +0,0 @@
-signature IML_PACKAGE =
-sig
-end;
-
-structure ImlPackage : IML_PACKAGE =
-struct
-
-type nsidf = string
-type idf = string
-type qidf = nsidf * idf
-type iclass = qidf
-type isort = iclass list
-type ityco = qidf
-type iconst = qidf
-type 'a vidf = string * 'a
-type tvname = isort vidf
-
-fun qidf_ord ((a, c), (b, d)) =
- (case string_ord (a, b) of EQUAL => string_ord (c, d) | ord => ord);
-
-structure Idfgraph = GraphFun(type key = qidf val ord = qidf_ord);
-
-datatype ityp =
- IType of ityco * ityp list
- | IFree of tvname * isort
-
-type vname = ityp vidf
-
-datatype iexpr =
- IConst of iconst * ityp
- | IVar of vname * ityp
- | IAbs of vname * iexpr
- | IApp of iexpr * iexpr
-
-datatype pat =
- PConst of iconst
- | PVar of vname
-
-type 'a defn = 'a * (pat list * iexpr) list
-
-datatype stmt =
- Def of ityp defn
- | Typdecl of vname list * ityp
- | Datadef of (iconst * vname list) list
- | Classdecl of string list * (string * ityp) list
- | Instdef of iclass * ityco * isort list * (string defn) list
-
-type module = stmt Idfgraph.T
-
-type universe = module Graph.T
-
-fun isort_of_sort nsp sort =
- map (pair nsp) sort
-
-(* fun ityp_of_typ nsp ty =
- * let
- * fun ityp_of_typ' (Type (tycon, tys)) = IType ((nsp, tycon), map ityp_of_typ' tys)
- * | ityp_of_typ' (TFree (varname, sort)) = IFree ((nsp, varname), isort_of_sort nsp sort)
- * in (ityp_of_typ' o unvarifyT) ty end;
- *)
-
-(* fun iexpr_of_term nsp t =
- * let
- * fun iexpr_of_term' (Const (const, ty)) = IConst ((nsp, const), ityp_of_typ nsp ty)
- * | iexpr_of_term' (Free (varname, ty)) = IVar ((nsp, varname), ityp_of_typ nsp ty)
- * | iexpr_of_term' (Free (varname, ty)) = IVar ((nsp, varname), ityp_of_typ nsp ty)
- * in (iexpr_of_term' o map_term_types (unvarifyT)) t
- *
- * datatype term =
- * Const of string * typ |
- * Free of string * typ |
- * Var of indexname * typ |
- * Bound of int |
- * Abs of string * typ * term |
- * op $ of term * term
- *
- *
- * fun iexpr_of
- *)
-
-val empty_universe = Graph.empty
-
-val empty_module = Idfgraph.empty
-
-datatype deps =
- Check
- | Nocheck
- | Dep of qidf list
-
-fun add_stmt modname idf deps stmt univ =
- let
- fun check_deps Nocheck = I
- | check_deps (Dep idfs) = Graph.add_deps_acyclic (modname, map #2 idfs)
- | check_deps _ = error "'Nocheck' not implemented yet"
- in
- univ
- |> Graph.default_node modname empty_module
- |> Graph.map_node modname (Idfgraph.new_node (idf, stmt))
- |> fold check_deps deps
- end
-
-(* WICHTIG: resolve_qidf, resolve_midf *)
-
-(* IDEAS: Transaktionspuffer, Errormessage-Stack *)
-
-end;
-