# HG changeset patch # User haftmann # Date 1125216516 -7200 # Node ID c5fb1fb537c060816cf157842a7fd3faf4831fc4 # Parent e50f95ccde996846d01183b18419c9b86ca96c0b (branch cleanup) diff -r e50f95ccde99 -r c5fb1fb537c0 src/Pure/Tools/class_package.ML --- 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.$$$ "\\" || P.$$$ "=>") |-- (P.list1 P.name)) - -- (Scan.optional ((P.$$$ "\\" || 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 \ 'a \ 'a" (infix "\" 60) - assumes assoc: "(x \ y) \ z = x \ (y \ z)" - -classes sg -consts prod :: "'a::sg \ 'a \ 'a" (infix "\\" 60) -classrel sg < type -axioms sg: "sg prod" - -interpretation sg: sg [prod] by (rule sg) - - -(* abstract reasoning *) - -lemma (in sg) - bar: "x \ y = x \ y" .. - -lemma baz: - fixes x :: "'a::sg" - shows "x \\ y = x \\ 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 \\ fst q, snd p \\ 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)))) *) - - -*) - diff -r e50f95ccde99 -r c5fb1fb537c0 src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Sun Aug 28 10:05:03 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -signature CODEGEN_PACKAGE = -sig -end; - -structure CodegenPackage : CODEGEN_PACKAGE = -struct - -end; diff -r e50f95ccde99 -r c5fb1fb537c0 src/Pure/Tools/iml_package.ML --- 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; -