# HG changeset patch # User Christian Urban # Date 1257182815 -3600 # Node ID d0581fbc096c7a3423be2a25c99148079a6355b8 # Parent a159ba20979ec535ea81a2e2b88d7657b78f629d split quotient.ML into two files diff -r a159ba20979e -r d0581fbc096c QuotMain.thy --- a/QuotMain.thy Mon Nov 02 18:16:19 2009 +0100 +++ b/QuotMain.thy Mon Nov 02 18:26:55 2009 +0100 @@ -1,6 +1,7 @@ theory QuotMain imports QuotScript QuotList Prove -uses ("quotient.ML") +uses ("quotient_info.ML") + ("quotient.ML") begin ML {* Attrib.empty_binding *} @@ -139,6 +140,7 @@ section {* type definition for the quotient type *} +use "quotient_info.ML" use "quotient.ML" declare [[map list = (map, LIST_REL)]] diff -r a159ba20979e -r d0581fbc096c quotient.ML --- a/quotient.ML Mon Nov 02 18:16:19 2009 +0100 +++ b/quotient.ML Mon Nov 02 18:26:55 2009 +0100 @@ -1,112 +1,14 @@ signature QUOTIENT = sig - type maps_info = {mapfun: string, relfun: string} - type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} val mk_quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state val mk_quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory val note: binding * thm -> local_theory -> thm * local_theory - val maps_lookup: theory -> string -> maps_info option - val maps_update_thy: string -> maps_info -> theory -> theory - val maps_update: string -> maps_info -> Proof.context -> Proof.context - val print_quotdata: Proof.context -> unit - val quotdata_lookup_thy: theory -> quotient_info list - val quotdata_lookup: Proof.context -> quotient_info list - val quotdata_update_thy: (typ * typ * term * thm) -> theory -> theory - val quotdata_update: (typ * typ * term * thm) -> Proof.context -> Proof.context end; structure Quotient: QUOTIENT = struct -(* data containers *) -(*******************) - -(* info about map- and rel-functions *) -type maps_info = {mapfun: string, relfun: string} - -structure MapsData = TheoryDataFun - (type T = maps_info Symtab.table - val empty = Symtab.empty - val copy = I - val extend = I - fun merge _ = Symtab.merge (K true)) - -val maps_lookup = Symtab.lookup o MapsData.get - - -fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) -fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo) - -fun maps_attribute_aux s minfo = Thm.declaration_attribute - (fn thm => Context.mapping (maps_update_thy s minfo) (maps_update s minfo)) - -(* attribute to be used in declare statements *) -fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) = -let - val thy = ProofContext.theory_of ctxt - val tyname = Sign.intern_type thy tystr - val mapname = Sign.intern_const thy mapstr - val relname = Sign.intern_const thy relstr -in - maps_attribute_aux tyname {mapfun = mapname, relfun = relname} -end - -val maps_attr_parser = - Args.context -- Scan.lift - ((Args.name --| OuterParse.$$$ "=") -- - (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," -- - Args.name --| OuterParse.$$$ ")")) - -val _ = Context.>> (Context.map_theory - (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) - "declaration of map information")) - - -(* info about the quotient types *) -type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} - -structure QuotData = TheoryDataFun - (type T = quotient_info list - val empty = [] - val copy = I - val extend = I - fun merge _ = (op @)) (* FIXME: is this the correct merging function for the list? *) - -val quotdata_lookup_thy = QuotData.get -val quotdata_lookup = QuotData.get o ProofContext.theory_of - -fun quotdata_update_thy (qty, rty, rel, equiv_thm) thy = - QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm}::ls) thy - -fun quotdata_update (qty, rty, rel, equiv_thm) ctxt = - ProofContext.theory (quotdata_update_thy (qty, rty, rel, equiv_thm)) ctxt - -fun print_quotdata ctxt = -let - fun prt_quot {qtyp, rtyp, rel, equiv_thm} = - Pretty.block (Library.separate (Pretty.brk 2) - [Pretty.str ("quotient type:"), - Syntax.pretty_typ ctxt qtyp, - Pretty.str ("raw type:"), - Syntax.pretty_typ ctxt rtyp, - Pretty.str ("relation:"), - Syntax.pretty_term ctxt rel, - Pretty.str ("equiv. thm:"), - Syntax.pretty_term ctxt (prop_of equiv_thm)]) -in - QuotData.get (ProofContext.theory_of ctxt) - |> map prt_quot - |> Pretty.big_list "quotients:" - |> Pretty.writeln -end - -val _ = - OuterSyntax.improper_command "print_quotients" "print out all quotients" - OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotdata o Toplevel.context_of))) - - - (* wrappers for define, note and theorem_i *) fun define (name, mx, rhs) lthy = let diff -r a159ba20979e -r d0581fbc096c quotient_info.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/quotient_info.ML Mon Nov 02 18:26:55 2009 +0100 @@ -0,0 +1,107 @@ +signature QUOTIENT_INFO = +sig + type maps_info = {mapfun: string, relfun: string} + val maps_lookup: theory -> string -> maps_info option + val maps_update_thy: string -> maps_info -> theory -> theory + val maps_update: string -> maps_info -> Proof.context -> Proof.context + + type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} + val print_quotdata: Proof.context -> unit + val quotdata_lookup_thy: theory -> quotient_info list + val quotdata_lookup: Proof.context -> quotient_info list + val quotdata_update_thy: (typ * typ * term * thm) -> theory -> theory + val quotdata_update: (typ * typ * term * thm) -> Proof.context -> Proof.context +end; + +structure Quotient_Info: QUOTIENT_INFO = +struct + +(* data containers *) +(*******************) + +(* info about map- and rel-functions *) +type maps_info = {mapfun: string, relfun: string} + +structure MapsData = TheoryDataFun + (type T = maps_info Symtab.table + val empty = Symtab.empty + val copy = I + val extend = I + fun merge _ = Symtab.merge (K true)) + +val maps_lookup = Symtab.lookup o MapsData.get + + +fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) +fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo) + +fun maps_attribute_aux s minfo = Thm.declaration_attribute + (fn thm => Context.mapping (maps_update_thy s minfo) (maps_update s minfo)) + +(* attribute to be used in declare statements *) +fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) = +let + val thy = ProofContext.theory_of ctxt + val tyname = Sign.intern_type thy tystr + val mapname = Sign.intern_const thy mapstr + val relname = Sign.intern_const thy relstr +in + maps_attribute_aux tyname {mapfun = mapname, relfun = relname} +end + +val maps_attr_parser = + Args.context -- Scan.lift + ((Args.name --| OuterParse.$$$ "=") -- + (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," -- + Args.name --| OuterParse.$$$ ")")) + +val _ = Context.>> (Context.map_theory + (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) + "declaration of map information")) + + +(* info about the quotient types *) +type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} + +structure QuotData = TheoryDataFun + (type T = quotient_info list + val empty = [] + val copy = I + val extend = I + fun merge _ = (op @)) (* FIXME: is this the correct merging function for the list? *) + +val quotdata_lookup_thy = QuotData.get +val quotdata_lookup = QuotData.get o ProofContext.theory_of + +fun quotdata_update_thy (qty, rty, rel, equiv_thm) thy = + QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm}::ls) thy + +fun quotdata_update (qty, rty, rel, equiv_thm) ctxt = + ProofContext.theory (quotdata_update_thy (qty, rty, rel, equiv_thm)) ctxt + +fun print_quotdata ctxt = +let + fun prt_quot {qtyp, rtyp, rel, equiv_thm} = + Pretty.block (Library.separate (Pretty.brk 2) + [Pretty.str ("quotient type:"), + Syntax.pretty_typ ctxt qtyp, + Pretty.str ("raw type:"), + Syntax.pretty_typ ctxt rtyp, + Pretty.str ("relation:"), + Syntax.pretty_term ctxt rel, + Pretty.str ("equiv. thm:"), + Syntax.pretty_term ctxt (prop_of equiv_thm)]) +in + QuotData.get (ProofContext.theory_of ctxt) + |> map prt_quot + |> Pretty.big_list "quotients:" + |> Pretty.writeln +end + +val _ = + OuterSyntax.improper_command "print_quotients" "print out all quotients" + OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotdata o Toplevel.context_of))) + +end; (* structure *) + +open Quotient_Info \ No newline at end of file