Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quot/quotient_info.ML
changeset 784 da75568e7f12
parent 778 54f186bb5e3e
child 786 d6407afb913c
equal deleted inserted replaced
783:06e17083e90b 784:da75568e7f12 
     1 signature QUOTIENT_INFO =
 
     1 signature QUOTIENT_INFO =
 
     2 sig
 
     2 sig
 
     3   exception NotFound
 
     3   exception NotFound
 
     4 
     4 
     5   type maps_info = {mapfun: string, relfun: string}
 
     5   type maps_info = {mapfun: string, relmap: string}
 
     6   val maps_lookup: theory -> string -> maps_info       (* raises NotFound *)
 
     6   val maps_lookup: theory -> string -> maps_info     (* raises NotFound *)
 
     7   val maps_update_thy: string -> maps_info -> theory -> theory    
     7   val maps_update_thy: string -> maps_info -> theory -> theory    
     8   val maps_update: string -> maps_info -> Proof.context -> Proof.context     
     8   val maps_update: string -> maps_info -> Proof.context -> Proof.context     
     9   val print_mapsinfo: Proof.context -> unit
 
     9   val print_mapsinfo: Proof.context -> unit
 
    10 
    10 
    11   type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
 
    11   type quotient_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
 
    12   val quotdata_lookup_thy: theory -> string -> quotient_info option
 
    12   val quotdata_lookup_thy: theory -> string -> quotient_info     (* raises NotFound *)
 
    13   val quotdata_lookup: Proof.context -> string -> quotient_info option
 
    13   val quotdata_lookup: Proof.context -> string -> quotient_info     (* raises NotFound *)
 
    14   val quotdata_update_thy: string -> (typ * typ * term * thm) -> theory -> theory
 
    14   val quotdata_update_thy: string -> (typ * typ * term * thm) -> theory -> theory
 
    15   val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context
 
    15   val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context
 
    16   val quotdata_dest: theory -> quotient_info list
 
    16   val quotdata_dest: theory -> quotient_info list
 
    17   val print_quotinfo: Proof.context -> unit
 
    17   val print_quotinfo: Proof.context -> unit
 
    18 
    18 
    19   type qconsts_info = {qconst: term, rconst: term, def: thm}
 
    19   type qconsts_info = {qconst: term, rconst: term, def: thm}
 
    20   val qconsts_transfer: morphism -> qconsts_info -> qconsts_info
 
    20   val qconsts_transfer: morphism -> qconsts_info -> qconsts_info
 
    21   val qconsts_lookup: theory -> term -> qconsts_info    (* raises NotFound *)
 
    21   val qconsts_lookup: theory -> term -> qconsts_info     (* raises NotFound *)
 
    22   val qconsts_update_thy: string -> qconsts_info -> theory -> theory
 
    22   val qconsts_update_thy: string -> qconsts_info -> theory -> theory
 
    23   val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic
 
    23   val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic
 
    24   val qconsts_dest: theory -> qconsts_info list
 
    24   val qconsts_dest: theory -> qconsts_info list
 
    25   val print_qconstinfo: Proof.context -> unit
 
    25   val print_qconstinfo: Proof.context -> unit
 
    26 
    26 
    41 (*******************)
 
    41 (*******************)
 
    42 (* data containers *)
 
    42 (* data containers *)
 
    43 (*******************)
 
    43 (*******************)
 
    44 
    44 
    45 (* info about map- and rel-functions for a type *)
 
    45 (* info about map- and rel-functions for a type *)
 
    46 type maps_info = {mapfun: string, relfun: string}
 
    46 type maps_info = {mapfun: string, relmap: string}
 
    47 
    47 
    48 structure MapsData = Theory_Data
 
    48 structure MapsData = Theory_Data
 
    49   (type T = maps_info Symtab.table
 
    49   (type T = maps_info Symtab.table
 
    50    val empty = Symtab.empty
 
    50    val empty = Symtab.empty
 
    51    val extend = I
 
    51    val extend = I
 
    71   val relname = Sign.intern_const thy relstr
 
    71   val relname = Sign.intern_const thy relstr
 
    72 
    72 
    73   fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt)
 
    73   fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt)
 
    74   val _ =  map sanity_check [mapname, relname]
 
    74   val _ =  map sanity_check [mapname, relname]
 
    75 in
 
    75 in
 
    76   maps_attribute_aux tyname {mapfun = mapname, relfun = relname}
 
    76   maps_attribute_aux tyname {mapfun = mapname, relmap = relname}
 
    77 end
 
    77 end
 
    78 
    78 
    79 val maps_attr_parser = 
    79 val maps_attr_parser = 
    80       Args.context -- Scan.lift
 
    80       Args.context -- Scan.lift
 
    81        ((Args.name --| OuterParse.$$$ "=") -- 
    81        ((Args.name --| OuterParse.$$$ "=") -- 
    86          (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) 
    86          (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) 
    87            "declaration of map information"))
 
    87            "declaration of map information"))
 
    88 
    88 
    89 fun print_mapsinfo ctxt =
 
    89 fun print_mapsinfo ctxt =
 
    90 let
 
    90 let
 
    91   fun prt_map (ty_name, {mapfun, relfun}) = 
    91   fun prt_map (ty_name, {mapfun, relmap}) = 
    92       Pretty.block (Library.separate (Pretty.brk 2)
 
    92       Pretty.block (Library.separate (Pretty.brk 2)
 
    93         (map Pretty.str 
    93         (map Pretty.str 
    94           ["type:", ty_name,
 
    94           ["type:", ty_name,
 
    95            "map fun:", mapfun,
 
    95            "map:", mapfun,
 
    96            "relation map:", relfun]))
 
    96            "relation map:", relmap]))
 
    97 in
 
    97 in
 
    98   MapsData.get (ProofContext.theory_of ctxt)
 
    98   MapsData.get (ProofContext.theory_of ctxt)
 
    99   |> Symtab.dest
 
    99   |> Symtab.dest
 
   100   |> map (prt_map)
 
   100   |> map (prt_map)
 
   101   |> Pretty.big_list "maps:" 
   101   |> Pretty.big_list "maps:" 
   102   |> Pretty.writeln
 
   102   |> Pretty.writeln
 
   103 end
 
   103 end
 
   104 
   104 
   105  
   105  
   106 (* info about quotient types *)
 
   106 (* info about quotient types *)
 
   107 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
 
   107 type quotient_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
 
   108 
   108 
   109 structure QuotData = Theory_Data
 
   109 structure QuotData = Theory_Data
 
   110   (type T = quotient_info Symtab.table
 
   110   (type T = quotient_info Symtab.table
 
   111    val empty = Symtab.empty
 
   111    val empty = Symtab.empty
 
   112    val extend = I
 
   112    val extend = I
 
   113    val merge = Symtab.merge (K true)) 
   113    val merge = Symtab.merge (K true)) 
   114 
   114 
   115 fun quotdata_lookup_thy thy str = 
   115 fun quotdata_lookup_thy thy s = 
   116     Symtab.lookup (QuotData.get thy) (Sign.intern_type thy str)
 
   116   case Symtab.lookup (QuotData.get thy) (Sign.intern_type thy s) of
 
       
   117     SOME qinfo => qinfo
 
       
   118   | NONE => raise NotFound
 
   117 
   119 
   118 val quotdata_lookup = quotdata_lookup_thy o ProofContext.theory_of
 
   120 val quotdata_lookup = quotdata_lookup_thy o ProofContext.theory_of
 
   119 
   121 
   120 fun quotdata_update_thy qty_name (qty, rty, rel, equiv_thm) =
 
   122 fun quotdata_update_thy qty_name (qty, rty, equiv_rel, equiv_thm) =
 
   121       QuotData.map (Symtab.update (qty_name, {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm}))
 
   123 let
 
       
   124   val qinfo = {qtyp = qty, rtyp = rty, equiv_rel = equiv_rel, equiv_thm = equiv_thm}
 
       
   125 in
 
       
   126   QuotData.map (Symtab.update (qty_name, qinfo))
 
       
   127 end
 
   122 
   128 
   123 fun quotdata_update qty_name (qty, rty, rel, equiv_thm) = 
   129 fun quotdata_update qty_name (qty, rty, rel, equiv_thm) = 
   124       ProofContext.theory (quotdata_update_thy qty_name (qty, rty, rel, equiv_thm))
 
   130       ProofContext.theory (quotdata_update_thy qty_name (qty, rty, rel, equiv_thm))
 
   125 
   131 
   126 fun quotdata_dest thy =
 
   132 fun quotdata_dest thy =
 
   127     map snd (Symtab.dest (QuotData.get thy))
 
   133     map snd (Symtab.dest (QuotData.get thy))
 
   128 
   134 
   129 fun print_quotinfo ctxt =
 
   135 fun print_quotinfo ctxt =
 
   130 let
 
   136 let
 
   131   fun prt_quot {qtyp, rtyp, rel, equiv_thm} = 
   137   fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} = 
   132       Pretty.block (Library.separate (Pretty.brk 2)
 
   138       Pretty.block (Library.separate (Pretty.brk 2)
 
   133           [Pretty.str "quotient type:", 
   139           [Pretty.str "quotient type:", 
   134            Syntax.pretty_typ ctxt qtyp,
 
   140            Syntax.pretty_typ ctxt qtyp,
 
   135            Pretty.str "raw type:", 
   141            Pretty.str "raw type:", 
   136            Syntax.pretty_typ ctxt rtyp,
 
   142            Syntax.pretty_typ ctxt rtyp,
 
   137            Pretty.str "relation:", 
   143            Pretty.str "relation:", 
   138            Syntax.pretty_term ctxt rel,
 
   144            Syntax.pretty_term ctxt equiv_rel,
 
   139            Pretty.str "equiv. thm:", 
   145            Pretty.str "equiv. thm:", 
   140            Syntax.pretty_term ctxt (prop_of equiv_thm)])
 
   146            Syntax.pretty_term ctxt (prop_of equiv_thm)])
 
   141 in
 
   147 in
 
   142   QuotData.get (ProofContext.theory_of ctxt)
 
   148   QuotData.get (ProofContext.theory_of ctxt)
 
   143   |> Symtab.dest
 
   149   |> Symtab.dest
nominal2