# HG changeset patch # User haftmann # Date 1171095982 -3600 # Node ID bf5bdb7f7607d225131fda0b6bcb01d456b6d80e # Parent 1435d027e45300408be476aff47554c2ce7b7f54 added experimental class target diff -r 1435d027e453 -r bf5bdb7f7607 src/Pure/Tools/class_package.ML --- a/src/Pure/Tools/class_package.ML Sat Feb 10 09:26:20 2007 +0100 +++ b/src/Pure/Tools/class_package.ML Sat Feb 10 09:26:22 2007 +0100 @@ -7,15 +7,23 @@ signature CLASS_PACKAGE = sig + val fork_mixfix: bool -> bool -> mixfix -> mixfix * mixfix + val class: bstring -> class list -> Element.context_i Locale.element list -> theory -> string * Proof.context + val class_e: bstring -> string list -> Element.context Locale.element list -> theory -> + string * Proof.context val instance_arity: ((bstring * sort list) * sort) list - -> ((bstring * attribute list) * term) list + -> ((bstring * Attrib.src list) * term) list + -> theory -> Proof.state + val instance_arity_e: ((bstring * string list) * string) list + -> ((bstring * Attrib.src list) * string) list -> theory -> Proof.state val prove_instance_arity: tactic -> ((string * sort list) * sort) list - -> ((bstring * attribute list) * term) list + -> ((bstring * Attrib.src list) * term) list -> theory -> theory val instance_sort: class * sort -> theory -> Proof.state + val instance_sort_e: string * string -> theory -> Proof.state val prove_instance_sort: tactic -> class * sort -> theory -> theory val assume_arities_of_sort: theory -> ((string * sort list) * sort) list -> typ * sort -> bool @@ -23,10 +31,9 @@ (*'a must not keep any reference to theory*) (* experimental class target *) - val add_def: class * thm -> theory -> theory - val export_typ: theory -> class -> typ -> typ - val export_def: theory -> class -> term -> term - val export_thm: theory -> class -> thm -> thm + val class_of_locale: theory -> string -> class option + val add_def_in_class: local_theory -> string + -> (string * Syntax.mixfix) * ((string * Attrib.src list) * (term * thm)) -> theory -> theory val print_classes: theory -> unit val intro_classes_tac: thm list -> tactic @@ -36,9 +43,19 @@ structure ClassPackage : CLASS_PACKAGE = struct -(** axclasses with implicit parameter handling **) +(** auxiliary **) -(* axclass instances *) +fun fork_mixfix is_class is_loc mx = + let + val mx' = Syntax.unlocalize_mixfix mx; + val mx1 = if is_class orelse (is_loc andalso mx = mx') then NoSyn else mx'; + val mx2 = if is_loc then mx else NoSyn; + in (mx1, mx2) end; + + +(** AxClasses with implicit parameter handling **) + +(* AxClass instances *) local @@ -81,10 +98,10 @@ thy |> fold_map add_const consts |-> (fn cs => mk_axioms cs - #-> (fn axioms => AxClass.define_class_i (name, superclasses) (map fst cs) axioms + #-> (fn axioms_prop => AxClass.define_class_i (name, superclasses) (map fst cs) axioms_prop #-> (fn class => `(fn thy => AxClass.get_definition thy class) #-> (fn {intro, axioms, ...} => fold (add_constraint class) cs - #> pair (class, ((intro, axioms), cs)))))) + #> pair (class, ((intro, (map snd axioms_prop, axioms)), cs)))))) end; @@ -120,10 +137,10 @@ | _ => SOME raw_name; in (c, (insts, ((name, t), atts))) end; -fun read_def_e thy = gen_read_def thy Attrib.attribute read_axm; +fun read_def_e thy = gen_read_def thy Attrib.intern_src read_axm; fun read_def thy = gen_read_def thy (K I) (K I); -fun gen_instance_arity prep_arity prep_att read_def do_proof raw_arities raw_defs theory = +fun gen_instance_arity prep_arity read_def do_proof raw_arities raw_defs theory = let fun prep_arity' ((tyco, asorts), sort) = prep_arity theory (tyco, asorts, sort); val arities = map prep_arity' raw_arities; @@ -179,7 +196,7 @@ end; fun add_defs defs thy = thy - |> PureThy.add_defs_i true (map snd defs) + |> PureThy.add_defs_i true (map ((apsnd o map) (Attrib.attribute thy) o snd) defs) |-> (fn thms => pair (map fst defs ~~ thms)); fun after_qed cs thy = thy @@ -191,10 +208,8 @@ |-> (fn (cs, _) => do_proof (after_qed cs) arities) end; -fun instance_arity_e' do_proof = gen_instance_arity Sign.read_arity Attrib.attribute - read_def_e do_proof; -fun instance_arity' do_proof = gen_instance_arity Sign.cert_arity (K I) - read_def do_proof; +fun instance_arity_e' do_proof = gen_instance_arity Sign.read_arity read_def_e do_proof; +fun instance_arity' do_proof = gen_instance_arity Sign.cert_arity read_def do_proof; fun tactic_proof tac after_qed arities = fold (fn arity => AxClass.prove_arity arity tac) arities #> after_qed; @@ -217,22 +232,25 @@ locale: string, consts: (string * string) list (*locale parameter ~> toplevel theory constant*), + witness: Element.witness list, propnames: string list, - (*for ad-hoc instance in*) - defs: thm list + (*for ad-hoc instance_in*) + primdefs: thm list (*for experimental class target*) }; fun rep_classdata (ClassData c) = c; +fun merge_pair f1 f2 ((x1, y1), (x2, y2)) = (f1 (x1, x2), f2 (y1, y2)); + structure ClassData = TheoryDataFun ( struct val name = "Pure/classes"; - type T = class_data Graph.T; - val empty = Graph.empty; + type T = class_data Graph.T * class Symtab.table (*locale name ~> class name*); + val empty = (Graph.empty, Symtab.empty); val copy = I; val extend = I; - fun merge _ = Graph.merge (K true); + fun merge _ = merge_pair (Graph.merge (K true)) (Symtab.merge (K true)); fun print _ _ = (); end ); @@ -242,23 +260,28 @@ (* queries *) -val lookup_class_data = Option.map rep_classdata oo try o Graph.get_node o ClassData.get; -val is_class = can o Graph.get_node o ClassData.get; +val lookup_class_data = Option.map rep_classdata oo try o Graph.get_node o fst o ClassData.get; +fun class_of_locale thy = Symtab.lookup ((snd o ClassData.get) thy); + fun the_class_data thy class = case lookup_class_data thy class of NONE => error ("undeclared class " ^ quote class) | SOME data => data; -fun the_ancestry thy = Graph.all_succs (ClassData.get thy); +val ancestry = Graph.all_succs o fst o ClassData.get; -fun the_parm_map thy class = +fun param_map thy = let - val const_typs = (#params o AxClass.get_definition thy) class; - val const_names = (#consts o the_class_data thy) class; - in - map (apsnd (fn c => (c, (the o AList.lookup (op =) const_typs) c))) const_names - end; + fun params thy class = + let + val const_typs = (#params o AxClass.get_definition thy) class; + val const_names = (#consts o the_class_data thy) class; + in + (map o apsnd) (fn c => (c, (the o AList.lookup (op =) const_typs) c)) const_names + end; + in maps (params thy) o ancestry thy end; +val the_witness = #witness oo the_class_data; val the_propnames = #propnames oo the_class_data; fun print_classes thy = @@ -296,20 +319,42 @@ (* updaters *) -fun add_class_data ((class, superclasses), (locale, consts, propnames)) = - ClassData.map ( - Graph.new_node (class, ClassData { +fun add_class_data ((class, superclasses), (locale, consts, witness, propnames)) = + ClassData.map (fn (gr, tab) => ( + gr + |> Graph.new_node (class, ClassData { locale = locale, consts = consts, + witness = witness, propnames = propnames, - defs = []}) - #> fold (curry Graph.add_edge class) superclasses - ); + primdefs = []}) + |> fold (curry Graph.add_edge class) superclasses, + tab + |> Symtab.update (locale, class) + )); + +fun add_primdef (class, thm) thy = + (ClassData.map o apfst o Graph.map_node class) + (fn ClassData { locale, consts, witness, propnames, primdefs } => ClassData { locale = locale, + consts = consts, witness = witness, propnames = propnames, primdefs = thm :: primdefs }); + -fun add_def (class, thm) = - (ClassData.map o Graph.map_node class) - (fn ClassData { locale, consts, propnames, defs } => ClassData { locale = locale, - consts = consts, propnames = propnames, defs = thm :: defs }); +(* exporting terms and theorems to global toplevel *) +(*FIXME should also be used when introducing classes*) + +fun globalize thy classes = + let + val consts = param_map thy classes; + val constrain_sort = curry (Sorts.inter_sort (Sign.classes_of thy)) classes; + val subst_typ = Term.map_type_tfree (fn var as (v, sort) => + if v = AxClass.param_tyvarname then TFree (v, constrain_sort sort) else TFree var) + fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) consts v + of SOME (c, _) => Const (c, ty) + | NONE => t) + | subst_aterm t = t; + in (subst_typ, map_types subst_typ #> Term.map_aterms subst_aterm) end; + +val global_term = snd oo globalize (* tactics and methods *) @@ -374,9 +419,9 @@ (Locale.Merge o map (Locale.Locale o #locale o the_class_data theory)) sort; val const_names = (map (NameSpace.base o snd) o maps (#consts o the_class_data theory) - o the_ancestry theory) [class]; + o ancestry theory) [class]; fun get_thms thy = - the_ancestry thy sort + ancestry thy sort |> AList.make (the_propnames thy) |> map (apsnd (map (NameSpace.append (Logic.const_of_class loc_name)))) |> map_filter (fn (superclass, thm_names) => @@ -418,14 +463,15 @@ fun gen_class add_locale prep_class bname raw_supclasses raw_elems thy = let val elems = fold_rev (fn Locale.Elem e => cons e | _ => I) raw_elems []; + (*FIXME add constrains here to elements as hint for locale*) val supclasses = map (prep_class thy) raw_supclasses; val supsort = supclasses |> Sign.certify_sort thy - |> (fn [] => Sign.defaultS thy | S => S); (* FIXME Why syntax defaultS? *) + |> (fn [] => Sign.defaultS thy | S => S); (*FIXME Why syntax defaultS?*) val supexpr = Locale.Merge (map (Locale.Locale o #locale o the_class_data thy) supclasses); val supconsts = AList.make - (the o AList.lookup (op =) ((maps (the_parm_map thy) o the_ancestry thy) supclasses)) + (the o AList.lookup (op =) (param_map thy supclasses)) ((map (fst o fst) o Locale.parameters_of_expr thy) supexpr); fun check_locale thy name_locale = let @@ -444,7 +490,7 @@ fun extract_params thy name_locale = Locale.parameters_of thy name_locale |> (map o apfst o apsnd o Term.map_type_tfree) (K (TFree (AxClass.param_tyvarname, []))) - |> (map o apsnd) (TheoryTarget.fork_mixfix false true #> fst) + |> (map o apsnd) (fork_mixfix false true #> fst) |> chop (length supconsts) |> snd; fun extract_assumes name_locale params thy cs = @@ -475,11 +521,12 @@ #> `(fn thy => extract_params thy name_locale) #-> (fn params => axclass_params (bname, supsort) params (extract_assumes name_locale params) - #-> (fn (name_axclass, ((_, ax_axioms), consts)) => + #-> (fn (name_axclass, ((_, (ax_terms, ax_axioms)), consts)) => `(fn thy => extract_axiom_names thy name_locale) #-> (fn axiom_names => add_class_data ((name_axclass, supclasses), - (name_locale, map (fst o fst) params ~~ map fst consts, axiom_names)) + (name_locale, map (fst o fst) params ~~ map fst consts, + map2 Element.make_witness (map Logic.mk_conjunction_list ax_terms) ax_axioms, axiom_names)) #> prove_interpretation (Logic.const_of_class bname, []) (Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass) (map snd supconsts @ consts)) ((ALLGOALS o ProofContext.fact_tac) ax_axioms) @@ -500,7 +547,8 @@ let val class = prep_class theory raw_class; val sort = prep_sort theory raw_sort; - in if is_class theory class andalso forall (is_class theory) sort then + val is_class = is_some o lookup_class_data theory; + in if is_class class andalso forall is_class sort then theory |> instance_sort' (Locale.interpretation_in_locale o ProofContext.theory) (class, sort) else case sort @@ -520,86 +568,38 @@ (** experimental class target **) -fun export_typ thy loc = - let - val class = loc (*FIXME*); - val (v, _) = AxClass.params_of_class thy class; - in - Term.map_type_tfree (fn var as (w, sort) => - if w = v then TFree (w, Sorts.inter_sort (Sign.classes_of thy) - (sort, [class])) else TFree var) - end; - -fun export_def thy loc = +fun add_def_in_class lthy loc ((c, syn), ((name, atts), (rhs, eq))) thy = let - val class = loc (*FIXME*); - val consts = the_parm_map thy class; - val subst_typ = Term.map_type_tfree (fn var as (w, sort) => - if w = AxClass.param_tyvarname then TFree (w, Sorts.inter_sort (Sign.classes_of thy) - (sort, [class])) else TFree var) - fun subst (t as Free (v, _)) = (case AList.lookup (op =) consts v - of SOME c_ty => Const c_ty - | NONE => t) - | subst t = t; + val SOME class = class_of_locale thy loc; + val rhs' = global_term thy [class] rhs; + val (syn', _) = fork_mixfix true true syn; + val ty = Term.fastype_of rhs'; + fun add_const (c, ty, syn) = + Sign.add_consts_authentic [(c, ty, syn)] + #> pair (Sign.full_name thy c, ty); + fun add_def ((name, atts), prop) thy = + thy + |> PureThy.add_defs_i false [((name, prop), map (Attrib.attribute thy) atts)] + |>> the_single; + (*val _ = Output.info "------ DEF ------"; + val _ = Output.info c; + val _ = Output.info name; + val _ = (Output.info o Sign.string_of_term thy) rhs'; + val eq' = Morphism.thm (LocalTheory.target_morphism lthy) eq; + val _ = (Output.info o string_of_thm) eq; + val _ = (Output.info o string_of_thm) eq'; + val witness = the_witness thy class; + val _ = Output.info "------ WIT ------"; + fun print_wit (t, thm) = "(" ^ Sign.string_of_term thy t ^ ", " ^ Display.string_of_thm thm ^ ")" + val _ = (Output.info o cat_lines o map (print_wit o Element.dest_witness)) witness; + val _ = (Output.info o string_of_thm) eq'; + val eq'' = Element.satisfy_thm witness eq'; + val _ = (Output.info o string_of_thm) eq'';*) in - Term.map_aterms subst #> map_types subst_typ - end; - -fun export_thm thy loc = - let - val class = loc (*FIXME*); - val thms = (#defs o the_class_data thy) class; - in - MetaSimplifier.rewrite_rule thms + thy + (*|> add_const (c, ty, syn') + |-> (fn c => add_def ((name, atts), Logic.mk_equals (Const c, rhs'))) + |-> (fn global_def_thm => tap (fn _ => (Output.info o string_of_thm) global_def_thm))*) end; - - -(** toplevel interface **) - -local - -structure P = OuterParse -and K = OuterKeyword - -in - -val (classK, instanceK, print_classesK) = ("class", "instance", "print_classes") - -val class_subP = P.name -- Scan.repeat (P.$$$ "+" |-- P.name) >> (op ::); -val class_bodyP = P.!!! (Scan.repeat1 SpecParse.locale_element); - -val parse_arity = - (P.xname --| P.$$$ "::" -- P.!!! P.arity) - >> (fn (tyco, (asorts, sort)) => ((tyco, asorts), sort)); - -val classP = - OuterSyntax.command classK "define type class" K.thy_decl ( - P.name --| P.$$$ "=" - -- ( - class_subP --| P.$$$ "+" -- class_bodyP - || class_subP >> rpair [] - || class_bodyP >> pair []) - -- P.opt_begin - >> (fn ((bname, (supclasses, elems)), begin) => - Toplevel.begin_local_theory begin - (class_e bname supclasses elems #-> TheoryTarget.begin true))); - -val instanceP = - OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal (( - P.xname -- ((P.$$$ "\\" || P.$$$ "<") |-- P.!!! P.xname) - >> instance_sort_e - || P.and_list1 parse_arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop) - >> (fn (arities, defs) => instance_arity_e arities defs) - ) >> (Toplevel.print oo Toplevel.theory_to_proof)); - -val print_classesP = - OuterSyntax.improper_command print_classesK "print classes of this theory" K.diag - (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory - o Toplevel.keep (print_classes o Toplevel.theory_of))); - -val _ = OuterSyntax.add_parsers [classP, instanceP, print_classesP]; - -end; (*local*) - end;