# HG changeset patch # User wenzelm # Date 1319742130 -7200 # Node ID 9fd6fce8a230062d462dc17cadb502400a35b2f4 # Parent 89a17197cb9842b6c96432d507812d9e318c9a78 localized quotient data; diff -r 89a17197cb98 -r 9fd6fce8a230 src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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) diff -r 89a17197cb98 -r 9fd6fce8a230 src/HOL/Tools/Quotient/quotient_info.ML --- 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; diff -r 89a17197cb98 -r 9fd6fce8a230 src/HOL/Tools/Quotient/quotient_term.ML --- 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 diff -r 89a17197cb98 -r 9fd6fce8a230 src/HOL/Tools/Quotient/quotient_typ.ML --- 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;