--- a/Quot/quotient_info.ML Wed Dec 23 22:42:30 2009 +0100
+++ b/Quot/quotient_info.ML Wed Dec 23 23:22:02 2009 +0100
@@ -2,15 +2,15 @@
sig
exception NotFound
- type maps_info = {mapfun: string, relfun: string}
- val maps_lookup: theory -> string -> maps_info (* raises NotFound *)
+ type maps_info = {mapfun: string, relmap: string}
+ val maps_lookup: theory -> string -> maps_info (* raises NotFound *)
val maps_update_thy: string -> maps_info -> theory -> theory
val maps_update: string -> maps_info -> Proof.context -> Proof.context
val print_mapsinfo: Proof.context -> unit
- type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
- val quotdata_lookup_thy: theory -> string -> quotient_info option
- val quotdata_lookup: Proof.context -> string -> quotient_info option
+ type quotient_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
+ val quotdata_lookup_thy: theory -> string -> quotient_info (* raises NotFound *)
+ val quotdata_lookup: Proof.context -> string -> quotient_info (* raises NotFound *)
val quotdata_update_thy: string -> (typ * typ * term * thm) -> theory -> theory
val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context
val quotdata_dest: theory -> quotient_info list
@@ -18,7 +18,7 @@
type qconsts_info = {qconst: term, rconst: term, def: thm}
val qconsts_transfer: morphism -> qconsts_info -> qconsts_info
- val qconsts_lookup: theory -> term -> qconsts_info (* raises NotFound *)
+ val qconsts_lookup: theory -> term -> qconsts_info (* raises NotFound *)
val qconsts_update_thy: string -> qconsts_info -> theory -> theory
val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic
val qconsts_dest: theory -> qconsts_info list
@@ -43,7 +43,7 @@
(*******************)
(* info about map- and rel-functions for a type *)
-type maps_info = {mapfun: string, relfun: string}
+type maps_info = {mapfun: string, relmap: string}
structure MapsData = Theory_Data
(type T = maps_info Symtab.table
@@ -73,7 +73,7 @@
fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt)
val _ = map sanity_check [mapname, relname]
in
- maps_attribute_aux tyname {mapfun = mapname, relfun = relname}
+ maps_attribute_aux tyname {mapfun = mapname, relmap = relname}
end
val maps_attr_parser =
@@ -88,12 +88,12 @@
fun print_mapsinfo ctxt =
let
- fun prt_map (ty_name, {mapfun, relfun}) =
+ fun prt_map (ty_name, {mapfun, relmap}) =
Pretty.block (Library.separate (Pretty.brk 2)
(map Pretty.str
["type:", ty_name,
- "map fun:", mapfun,
- "relation map:", relfun]))
+ "map:", mapfun,
+ "relation map:", relmap]))
in
MapsData.get (ProofContext.theory_of ctxt)
|> Symtab.dest
@@ -104,7 +104,7 @@
(* info about quotient types *)
-type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
+type quotient_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
structure QuotData = Theory_Data
(type T = quotient_info Symtab.table
@@ -112,13 +112,19 @@
val extend = I
val merge = Symtab.merge (K true))
-fun quotdata_lookup_thy thy str =
- Symtab.lookup (QuotData.get thy) (Sign.intern_type thy str)
+fun quotdata_lookup_thy thy s =
+ case Symtab.lookup (QuotData.get thy) (Sign.intern_type thy s) of
+ SOME qinfo => qinfo
+ | NONE => raise NotFound
val quotdata_lookup = quotdata_lookup_thy o ProofContext.theory_of
-fun quotdata_update_thy qty_name (qty, rty, rel, equiv_thm) =
- QuotData.map (Symtab.update (qty_name, {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm}))
+fun quotdata_update_thy qty_name (qty, rty, equiv_rel, equiv_thm) =
+let
+ val qinfo = {qtyp = qty, rtyp = rty, equiv_rel = equiv_rel, equiv_thm = equiv_thm}
+in
+ QuotData.map (Symtab.update (qty_name, qinfo))
+end
fun quotdata_update qty_name (qty, rty, rel, equiv_thm) =
ProofContext.theory (quotdata_update_thy qty_name (qty, rty, rel, equiv_thm))
@@ -128,14 +134,14 @@
fun print_quotinfo ctxt =
let
- fun prt_quot {qtyp, rtyp, rel, equiv_thm} =
+ fun prt_quot {qtyp, rtyp, equiv_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,
+ Syntax.pretty_term ctxt equiv_rel,
Pretty.str "equiv. thm:",
Syntax.pretty_term ctxt (prop_of equiv_thm)])
in
--- a/Quot/quotient_term.ML Wed Dec 23 22:42:30 2009 +0100
+++ b/Quot/quotient_term.ML Wed Dec 23 23:22:02 2009 +0100
@@ -45,9 +45,9 @@
let
val thy = ProofContext.theory_of ctxt
val exc = LIFT_MATCH (space_implode " " ["absrep_fun: no map for type", quote ty_str, "."])
- val info = maps_lookup thy ty_str handle NotFound => raise exc
+ val mapfun = #mapfun (maps_lookup thy ty_str) handle NotFound => raise exc
in
- Const (#mapfun info, dummyT)
+ Const (mapfun, dummyT)
end
fun get_absrep_const flag ctxt _ qty =
@@ -145,23 +145,24 @@
if s = s'
then
let
- val exc = LIFT_MATCH ("mk_resp_arg (no map function found for type " ^ s)
- val map_info = maps_lookup thy s handle NotFound => raise exc
+ val exc = LIFT_MATCH ("mk_resp_arg (no map function found for type " ^ s ^ ")")
+ val relmap = #relmap (maps_lookup thy s) handle NotFound => raise exc
val args = map (mk_resp_arg ctxt) (tys ~~ tys')
in
- list_comb (Const (#relfun map_info, dummyT), args)
+ list_comb (Const (relmap, dummyT), args)
end
else
- let
- val SOME qinfo = quotdata_lookup_thy thy s'
+ let
+ val exc = LIFT_MATCH ("mk_resp_arg (no quotient found for type " ^ s ^ ")")
+ val equiv_rel = #equiv_rel (quotdata_lookup_thy thy s') handle NotFound => raise exc
(* FIXME: check in this case that the rty and qty *)
(* FIXME: correspond to each other *)
(* we need to instantiate the TVars in the relation *)
val thy = ProofContext.theory_of ctxt
- val forced_rel = force_typ thy (#rel qinfo) (rty --> rty --> @{typ bool})
+ val forced_equiv_rel = force_typ thy equiv_rel (rty --> rty --> @{typ bool})
in
- forced_rel
+ forced_equiv_rel
end
| _ => HOLogic.eq_const rty
(* FIXME: check that the types correspond to each other? *)