--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Oct 27 20:26:38 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Oct 27 21:02:10 2011 +0200
@@ -641,17 +641,15 @@
s |> AList.lookup (op =) (#codatatypes (Data.get (Context.Proof ctxt)))
|> Option.map snd |> these |> null |> not
| is_codatatype _ _ = false
-fun is_real_quot_type thy (Type (s, _)) =
- is_some (Quotient_Info.lookup_quotients thy s)
+fun is_real_quot_type ctxt (Type (s, _)) =
+ is_some (Quotient_Info.lookup_quotients ctxt s)
| is_real_quot_type _ _ = false
fun is_quot_type ctxt T =
- let val thy = Proof_Context.theory_of ctxt in
- is_real_quot_type thy T andalso not (is_codatatype ctxt T)
- end
+ is_real_quot_type ctxt T andalso not (is_codatatype ctxt T)
fun is_pure_typedef ctxt (T as Type (s, _)) =
let val thy = Proof_Context.theory_of ctxt in
is_typedef ctxt s andalso
- not (is_real_datatype thy s orelse is_real_quot_type thy T orelse
+ not (is_real_datatype thy s orelse is_real_quot_type ctxt T orelse
is_codatatype ctxt T orelse is_record_type T orelse
is_integer_like_type T)
end
@@ -682,7 +680,7 @@
fun is_datatype ctxt stds (T as Type (s, _)) =
let val thy = Proof_Context.theory_of ctxt in
(is_typedef ctxt s orelse is_codatatype ctxt T orelse
- T = @{typ ind} orelse is_real_quot_type thy T) andalso
+ T = @{typ ind} orelse is_real_quot_type ctxt T) andalso
not (is_basic_datatype thy stds s)
end
| is_datatype _ _ _ = false
@@ -737,8 +735,11 @@
SOME {Abs_name, ...} => (Abs_name, Type (@{type_name fun}, [T2, T1]))
| NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
| mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
-fun rep_type_for_quot_type thy (T as Type (s, _)) =
- let val {qtyp, rtyp, ...} = the (Quotient_Info.lookup_quotients thy s) in
+fun rep_type_for_quot_type ctxt (T as Type (s, _)) =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val {qtyp, rtyp, ...} = the (Quotient_Info.lookup_quotients ctxt s)
+ in
instantiate_type thy qtyp T rtyp
end
| rep_type_for_quot_type _ T =
@@ -912,8 +913,8 @@
val T' = (Record.get_extT_fields thy T
|> apsnd single |> uncurry append |> map snd) ---> T
in [(s', T')] end
- else if is_real_quot_type thy T then
- [(@{const_name Quot}, rep_type_for_quot_type thy T --> T)]
+ else if is_real_quot_type ctxt T then
+ [(@{const_name Quot}, rep_type_for_quot_type ctxt T --> T)]
else case typedef_info ctxt s of
SOME {abs_type, rep_type, Abs_name, ...} =>
[(Abs_name,
@@ -1760,7 +1761,7 @@
val rep_T = domain_type (range_type T)
val (rep_fun, _) = quot_rep_of depth Ts abs_T rep_T []
val (equiv_rel, _) =
- equiv_relation_for_quot_type thy abs_T
+ equiv_relation_for_quot_type ctxt abs_T
in
(Abs (Name.uu, abs_T, equiv_rel $ (rep_fun $ Bound 0)),
ts)
@@ -1912,10 +1913,9 @@
end
fun optimized_quot_type_axioms ctxt stds abs_z =
let
- val thy = Proof_Context.theory_of ctxt
val abs_T = Type abs_z
- val rep_T = rep_type_for_quot_type thy abs_T
- val (equiv_rel, partial) = equiv_relation_for_quot_type thy abs_T
+ val rep_T = rep_type_for_quot_type ctxt abs_T
+ val (equiv_rel, partial) = equiv_relation_for_quot_type ctxt abs_T
val a_var = Var (("a", 0), abs_T)
val x_var = Var (("x", 0), rep_T)
val y_var = Var (("y", 0), rep_T)
--- a/src/HOL/Tools/Quotient/quotient_info.ML Thu Oct 27 20:26:38 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Thu Oct 27 21:02:10 2011 +0200
@@ -7,23 +7,19 @@
signature QUOTIENT_INFO =
sig
type quotmaps = {mapfun: string, relmap: string}
- val lookup_quotmaps: theory -> string -> quotmaps option
- val update_quotmaps_global: string -> quotmaps -> theory -> theory
- val update_quotmaps: string -> quotmaps -> Proof.context -> Proof.context
+ val lookup_quotmaps: Proof.context -> string -> quotmaps option
val print_quotmaps: Proof.context -> unit
type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
val transform_quotients: morphism -> quotients -> quotients
- val lookup_quotients: theory -> string -> quotients option
- val update_quotients_global: string -> quotients -> theory -> theory
+ val lookup_quotients: Proof.context -> string -> quotients option
val update_quotients: string -> quotients -> Context.generic -> Context.generic
val dest_quotients: Proof.context -> quotients list
val print_quotients: Proof.context -> unit
type quotconsts = {qconst: term, rconst: term, def: thm}
val transform_quotconsts: morphism -> quotconsts -> quotconsts
- val lookup_quotconsts: theory -> term -> quotconsts option
- val update_quotconsts_global: string -> quotconsts -> theory -> theory
+ val lookup_quotconsts: Proof.context -> term -> quotconsts option
val update_quotconsts: string -> quotconsts -> Context.generic -> Context.generic
val dest_quotconsts: Proof.context -> quotconsts list
val print_quotconsts: Proof.context -> unit
@@ -50,7 +46,7 @@
(* info about map- and rel-functions for a type *)
type quotmaps = {mapfun: string, relmap: string}
-structure Quotmaps = Theory_Data
+structure Quotmaps = Generic_Data
(
type T = quotmaps Symtab.table
val empty = Symtab.empty
@@ -58,29 +54,23 @@
fun merge data = Symtab.merge (K true) data
)
-val lookup_quotmaps = Symtab.lookup o Quotmaps.get
-
-fun update_quotmaps_global k minfo = Quotmaps.map (Symtab.update (k, minfo))
-fun update_quotmaps k minfo = Proof_Context.background_theory (update_quotmaps_global k minfo) (* FIXME !? *)
+val lookup_quotmaps = Symtab.lookup o Quotmaps.get o Context.Proof
-fun maps_attribute_aux s minfo = Thm.declaration_attribute
- (fn _ => Context.mapping (update_quotmaps_global s minfo) (update_quotmaps s minfo))
-
-(* attribute to be used in declare statements *)
-fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) =
+fun quotmaps_attribute (ctxt, (tystr, (mapstr, relstr))) =
let
- val thy = Proof_Context.theory_of ctxt
- val tyname = Sign.intern_type thy tystr (* FIXME pass proper internal names *)
+ val thy = Proof_Context.theory_of ctxt (* FIXME proper local context *)
+ val tyname = Sign.intern_type thy tystr (* FIXME pass proper internal names via syntax *)
val mapname = Sign.intern_const thy mapstr
val relname = Sign.intern_const thy relstr
fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt; ())
val _ = List.app sanity_check [mapname, relname]
+ val minfo = {mapfun = mapname, relmap = relname}
in
- maps_attribute_aux tyname {mapfun = mapname, relmap = relname}
+ Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo)))
end
-val maps_attr_parser =
+val quotmaps_attr_parser =
Args.context -- Scan.lift
((Args.name --| Parse.$$$ "=") --
(Parse.$$$ "(" |-- Args.name --| Parse.$$$ "," --
@@ -95,9 +85,7 @@
"map:", mapfun,
"relation map:", relmap]))
in
- Quotmaps.get (Proof_Context.theory_of ctxt)
- |> Symtab.dest
- |> map (prt_map)
+ map prt_map (Symtab.dest (Quotmaps.get (Context.Proof ctxt)))
|> Pretty.big_list "maps for type constructors:"
|> Pretty.writeln
end
@@ -106,7 +94,7 @@
(* info about quotient types *)
type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
-structure Quotients = Theory_Data
+structure Quotients = Generic_Data
(
type T = quotients Symtab.table
val empty = Symtab.empty
@@ -120,13 +108,12 @@
equiv_rel = Morphism.term phi equiv_rel,
equiv_thm = Morphism.thm phi equiv_thm}
-val lookup_quotients = Symtab.lookup o Quotients.get
+val lookup_quotients = Symtab.lookup o Quotients.get o Context.Proof
-fun update_quotients_global str qinfo = Quotients.map (Symtab.update (str, qinfo))
-fun update_quotients str qinfo = Context.mapping (update_quotients_global str qinfo) I (* FIXME !? *)
+fun update_quotients str qinfo = Quotients.map (Symtab.update (str, qinfo))
-fun dest_quotients lthy = (* FIXME slightly expensive way to retrieve data *)
- map snd (Symtab.dest (Quotients.get (Proof_Context.theory_of lthy))) (* FIXME !? *)
+fun dest_quotients ctxt = (* FIXME slightly expensive way to retrieve data *)
+ map snd (Symtab.dest (Quotients.get (Context.Proof ctxt)))
fun print_quotients ctxt =
let
@@ -141,9 +128,7 @@
Pretty.str "equiv. thm:",
Syntax.pretty_term ctxt (prop_of equiv_thm)])
in
- Quotients.get (Proof_Context.theory_of ctxt)
- |> Symtab.dest
- |> map (prt_quot o snd)
+ map (prt_quot o snd) (Symtab.dest (Quotients.get (Context.Proof ctxt)))
|> Pretty.big_list "quotients:"
|> Pretty.writeln
end
@@ -157,7 +142,7 @@
(* We need to be able to lookup instances of lifted constants,
for example given "nat fset" we need to find "'a fset";
but overloaded constants share the same name *)
-structure Quotconsts = Theory_Data
+structure Quotconsts = Generic_Data
(
type T = quotconsts list Symtab.table
val empty = Symtab.empty
@@ -170,23 +155,21 @@
rconst = Morphism.term phi rconst,
def = Morphism.thm phi def}
-fun update_quotconsts_global name qcinfo = Quotconsts.map (Symtab.cons_list (name, qcinfo))
-fun update_quotconsts name qcinfo = Context.mapping (update_quotconsts_global name qcinfo) I (* FIXME !? *)
+fun update_quotconsts name qcinfo = Quotconsts.map (Symtab.cons_list (name, qcinfo))
+
+fun dest_quotconsts ctxt =
+ flat (map snd (Symtab.dest (Quotconsts.get (Context.Proof ctxt))))
-fun dest_quotconsts lthy =
- flat (map snd (Symtab.dest (Quotconsts.get (Proof_Context.theory_of lthy)))) (* FIXME !? *)
+fun lookup_quotconsts ctxt t =
+ let
+ val thy = Proof_Context.theory_of ctxt
-fun lookup_quotconsts thy t =
- let
val (name, qty) = dest_Const t
fun matches (x: quotconsts) =
- let
- val (name', qty') = dest_Const (#qconst x);
- in
- name = name' andalso Sign.typ_instance thy (qty, qty')
- end
+ let val (name', qty') = dest_Const (#qconst x);
+ in name = name' andalso Sign.typ_instance thy (qty, qty') end
in
- (case Symtab.lookup (Quotconsts.get thy) name of
+ (case Symtab.lookup (Quotconsts.get (Context.Proof ctxt)) name of
NONE => NONE
| SOME l => find_first matches l)
end
@@ -201,11 +184,7 @@
Pretty.str "as",
Syntax.pretty_term ctxt (prop_of def)])
in
- Quotconsts.get (Proof_Context.theory_of ctxt)
- |> Symtab.dest
- |> map snd
- |> flat
- |> map prt_qconst
+ map prt_qconst (maps snd (Symtab.dest (Quotconsts.get (Context.Proof ctxt))))
|> Pretty.big_list "quotient constants:"
|> Pretty.writeln
end
@@ -263,7 +242,7 @@
(* theory setup *)
val setup =
- Attrib.setup @{binding map} (maps_attr_parser >> maps_attribute)
+ Attrib.setup @{binding map} (quotmaps_attr_parser >> quotmaps_attribute)
"declaration of map information" #>
Equiv_Rules.setup #>
Rsp_Rules.setup #>
@@ -286,5 +265,4 @@
Outer_Syntax.improper_command "print_quotconsts" "print quotient constants" Keyword.diag
(Scan.succeed (Toplevel.keep (print_quotconsts o Toplevel.context_of)))
-
end;
--- a/src/HOL/Tools/Quotient/quotient_term.ML Thu Oct 27 20:26:38 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Thu Oct 27 21:02:10 2011 +0200
@@ -63,7 +63,7 @@
| RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1
fun get_mapfun ctxt s =
- (case Quotient_Info.lookup_quotmaps (Proof_Context.theory_of ctxt) s of
+ (case Quotient_Info.lookup_quotmaps ctxt s of
SOME map_data => Const (#mapfun map_data, dummyT)
| NONE => raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found."))
@@ -96,9 +96,9 @@
a quotient definition
*)
fun get_rty_qty ctxt s =
- case Quotient_Info.lookup_quotients (Proof_Context.theory_of ctxt) s of
+ (case Quotient_Info.lookup_quotients ctxt s of
SOME qdata => (#rtyp qdata, #qtyp qdata)
- | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.");
+ | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found."))
(* takes two type-environments and looks
up in both of them the variable v, which
@@ -271,7 +271,7 @@
Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2
fun get_relmap ctxt s =
- (case Quotient_Info.lookup_quotmaps (Proof_Context.theory_of ctxt) s of
+ (case Quotient_Info.lookup_quotmaps ctxt s of
SOME map_data => Const (#relmap map_data, dummyT)
| NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")"))
@@ -290,7 +290,7 @@
end
fun get_equiv_rel ctxt s =
- (case Quotient_Info.lookup_quotients (Proof_Context.theory_of ctxt) s of
+ (case Quotient_Info.lookup_quotients ctxt s of
SOME qdata => #equiv_rel qdata
| NONE => raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")"))
@@ -418,17 +418,18 @@
(* Checks that two types match, for example:
rty -> rty matches qty -> qty *)
-fun matches_typ thy rT qT =
+fun matches_typ ctxt rT qT =
if rT = qT then true
else
(case (rT, qT) of
(Type (rs, rtys), Type (qs, qtys)) =>
if rs = qs then
if length rtys <> length qtys then false
- else forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys)
+ else forall (fn x => x = true) (map2 (matches_typ ctxt) rtys qtys)
else
- (case Quotient_Info.lookup_quotients thy qs of
- SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
+ (case Quotient_Info.lookup_quotients ctxt qs of
+ SOME quotinfo =>
+ Sign.typ_instance (Proof_Context.theory_of ctxt) (rT, #rtyp quotinfo)
| NONE => false)
| _ => false)
@@ -441,7 +442,7 @@
special treatment of bound variables
*)
fun regularize_trm ctxt (rtrm, qtrm) =
- case (rtrm, qtrm) of
+ (case (rtrm, qtrm) of
(Abs (x, ty, t), Abs (_, ty', t')) =>
let
val subtrm = Abs(x, ty, regularize_trm ctxt (t, t'))
@@ -449,6 +450,7 @@
if ty = ty' then subtrm
else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm
end
+
| (Const (@{const_name Babs}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) =>
let
val subtrm = regularize_trm ctxt (t, t')
@@ -547,14 +549,14 @@
| (_, Const _) =>
let
val thy = Proof_Context.theory_of ctxt
- fun same_const (Const (s, T)) (Const (s', T')) = (s = s') andalso matches_typ thy T T'
+ fun same_const (Const (s, T)) (Const (s', T')) = s = s' andalso matches_typ ctxt T T'
| same_const _ _ = false
in
if same_const rtrm qtrm then rtrm
else
let
val rtrm' =
- (case Quotient_Info.lookup_quotconsts thy qtrm of
+ (case Quotient_Info.lookup_quotconsts ctxt qtrm of
SOME qconst_info => #rconst qconst_info
| NONE => term_mismatch "regularize (constant not found)" ctxt rtrm qtrm)
in
@@ -584,7 +586,7 @@
val qtrm_str = Syntax.string_of_term ctxt qtrm
in
raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))
- end
+ end)
fun regularize_trm_chk ctxt (rtrm, qtrm) =
regularize_trm ctxt (rtrm, qtrm)
@@ -705,9 +707,9 @@
fun matches [] = rty'
| matches ((rty, qty)::tail) =
- case try (Sign.typ_match thy (rty, rty')) Vartab.empty of
+ (case try (Sign.typ_match thy (rty, rty')) Vartab.empty of
NONE => matches tail
- | SOME inst => Envir.subst_type inst qty
+ | SOME inst => Envir.subst_type inst qty)
in
matches ty_subst
end
@@ -726,9 +728,9 @@
fun matches [] = Const (a, subst_typ ctxt ty_subst ty)
| matches ((rconst, qconst)::tail) =
- case try (Pattern.match thy (rconst, rtrm)) (Vartab.empty, Vartab.empty) of
+ (case try (Pattern.match thy (rconst, rtrm)) (Vartab.empty, Vartab.empty) of
NONE => matches tail
- | SOME inst => Envir.subst_term inst qconst
+ | SOME inst => Envir.subst_term inst qconst)
in
matches trm_subst
end
--- a/src/HOL/Tools/Quotient/quotient_typ.ML Thu Oct 27 20:26:38 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML Thu Oct 27 21:02:10 2011 +0200
@@ -219,13 +219,11 @@
(* check for existence of map functions *)
fun map_check ctxt (_, (rty, _, _)) =
let
- val thy = Proof_Context.theory_of ctxt
-
fun map_check_aux rty warns =
- case rty of
+ (case rty of
Type (_, []) => warns
- | Type (s, _) => if is_some (Quotient_Info.lookup_quotmaps thy s) then warns else s :: warns
- | _ => warns
+ | Type (s, _) => if is_some (Quotient_Info.lookup_quotmaps ctxt s) then warns else s :: warns
+ | _ => warns)
val warns = map_check_aux rty []
in
@@ -310,4 +308,4 @@
"quotient type definitions (require equivalence proofs)"
Keyword.thy_goal (quotspec_parser >> quotient_type_cmd)
-end; (* structure *)
+end;