# HG changeset patch # User wenzelm # Date 1320423573 -3600 # Node ID 98ec8b51af9c83b16f68cacb8fdf3dffce101e88 # Parent 2838109364f0f974990c1ffc61594fa0980603be prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230); diff -r 2838109364f0 -r 98ec8b51af9c src/HOL/Tools/Quotient/quotient_info.ML --- a/src/HOL/Tools/Quotient/quotient_info.ML Fri Nov 04 13:52:19 2011 +0100 +++ b/src/HOL/Tools/Quotient/quotient_info.ML Fri Nov 04 17:19:33 2011 +0100 @@ -8,18 +8,20 @@ sig type quotmaps = {mapfun: string, relmap: string} val lookup_quotmaps: Proof.context -> string -> quotmaps option + val lookup_quotmaps_global: theory -> 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: Proof.context -> string -> quotients option + val lookup_quotients_global: theory -> 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: Proof.context -> term -> quotconsts option + val lookup_quotconsts_global: theory -> 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 @@ -55,6 +57,7 @@ ) val lookup_quotmaps = Symtab.lookup o Quotmaps.get o Context.Proof +val lookup_quotmaps_global = Symtab.lookup o Quotmaps.get o Context.Theory (* FIXME export proper internal update operation!? *) @@ -101,6 +104,7 @@ equiv_thm = Morphism.thm phi equiv_thm} val lookup_quotients = Symtab.lookup o Quotients.get o Context.Proof +val lookup_quotients_global = Symtab.lookup o Quotients.get o Context.Theory fun update_quotients str qinfo = Quotients.map (Symtab.update (str, qinfo)) @@ -152,16 +156,14 @@ fun dest_quotconsts ctxt = flat (map snd (Symtab.dest (Quotconsts.get (Context.Proof ctxt)))) -fun lookup_quotconsts ctxt t = +fun lookup_quotconsts_global thy t = let - val thy = Proof_Context.theory_of ctxt - 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 in - (case Symtab.lookup (Quotconsts.get (Context.Proof ctxt)) name of + (case Symtab.lookup (Quotconsts.get (Context.Theory thy)) name of NONE => NONE | SOME l => find_first matches l) end diff -r 2838109364f0 -r 98ec8b51af9c src/HOL/Tools/Quotient/quotient_term.ML --- a/src/HOL/Tools/Quotient/quotient_term.ML Fri Nov 04 13:52:19 2011 +0100 +++ b/src/HOL/Tools/Quotient/quotient_term.ML Fri Nov 04 17:19:33 2011 +0100 @@ -62,8 +62,8 @@ AbsF => Const (@{const_name comp}, dummyT) $ trm1 $ trm2 | RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1 -fun get_mapfun ctxt s = - (case Quotient_Info.lookup_quotmaps ctxt s of +fun get_mapfun thy s = + (case Quotient_Info.lookup_quotmaps_global thy s of SOME map_data => Const (#mapfun map_data, dummyT) | NONE => raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")) @@ -78,7 +78,7 @@ for example for: (?'a list * ?'b) it produces: %a b. prod_map (map a) b *) -fun mk_mapfun ctxt vs rty = +fun mk_mapfun thy vs rty = let val vs' = map mk_Free vs @@ -86,7 +86,7 @@ case rty of TVar _ => mk_Free rty | Type (_, []) => mk_identity rty - | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys) + | Type (s, tys) => list_comb (get_mapfun thy s, map mk_mapfun_aux tys) | _ => raise LIFT_MATCH "mk_mapfun (default)" in fold_rev Term.lambda vs' (mk_mapfun_aux rty) @@ -95,8 +95,8 @@ (* looks up the (varified) rty and qty for a quotient definition *) -fun get_rty_qty ctxt s = - (case Quotient_Info.lookup_quotients ctxt s of +fun get_rty_qty thy s = + (case Quotient_Info.lookup_quotients_global thy s of SOME qdata => (#rtyp qdata, #qtyp qdata) | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")) @@ -189,56 +189,60 @@ *) fun absrep_fun flag ctxt (rty, qty) = - if rty = qty - then mk_identity rty - else - case (rty, qty) of - (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => - let - val arg1 = absrep_fun (negF flag) ctxt (ty1, ty1') - val arg2 = absrep_fun flag ctxt (ty2, ty2') - in - list_comb (get_mapfun ctxt "fun", [arg1, arg2]) - end -(* FIXME: use type_name antiquotation if set type becomes explicit *) - | (Type ("Set.set", [ty]), Type ("Set.set", [ty'])) => - let - val arg = absrep_fun (negF flag) ctxt (ty, ty') - in - get_mapfun ctxt "Set.set" $ arg - end - | (Type (s, tys), Type (s', tys')) => - if s = s' - then + let + val thy = Proof_Context.theory_of ctxt + in + if rty = qty + then mk_identity rty + else + case (rty, qty) of + (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => let - val args = map (absrep_fun flag ctxt) (tys ~~ tys') + val arg1 = absrep_fun (negF flag) ctxt (ty1, ty1') + val arg2 = absrep_fun flag ctxt (ty2, ty2') + in + list_comb (get_mapfun thy "fun", [arg1, arg2]) + end + (* FIXME: use type_name antiquotation if set type becomes explicit *) + | (Type ("Set.set", [ty]), Type ("Set.set", [ty'])) => + let + val arg = absrep_fun (negF flag) ctxt (ty, ty') in - list_comb (get_mapfun ctxt s, args) + get_mapfun thy "Set.set" $ arg end - else - let - val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' - val rtyenv = match ctxt absrep_match_err rty_pat rty - val qtyenv = match ctxt absrep_match_err qty_pat qty - val args_aux = map (double_lookup rtyenv qtyenv) vs - val args = map (absrep_fun flag ctxt) args_aux - in - if forall is_identity args - then absrep_const flag ctxt s' - else - let - val map_fun = mk_mapfun ctxt vs rty_pat - val result = list_comb (map_fun, args) - in - mk_fun_compose flag (absrep_const flag ctxt s', result) - end - end - | (TFree x, TFree x') => - if x = x' - then mk_identity rty - else raise (LIFT_MATCH "absrep_fun (frees)") - | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)") - | _ => raise (LIFT_MATCH "absrep_fun (default)") + | (Type (s, tys), Type (s', tys')) => + if s = s' + then + let + val args = map (absrep_fun flag ctxt) (tys ~~ tys') + in + list_comb (get_mapfun thy s, args) + end + else + let + val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty thy s' + val rtyenv = match ctxt absrep_match_err rty_pat rty + val qtyenv = match ctxt absrep_match_err qty_pat qty + val args_aux = map (double_lookup rtyenv qtyenv) vs + val args = map (absrep_fun flag ctxt) args_aux + in + if forall is_identity args + then absrep_const flag ctxt s' + else + let + val map_fun = mk_mapfun thy vs rty_pat + val result = list_comb (map_fun, args) + in + mk_fun_compose flag (absrep_const flag ctxt s', result) + end + end + | (TFree x, TFree x') => + if x = x' + then mk_identity rty + else raise (LIFT_MATCH "absrep_fun (frees)") + | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)") + | _ => raise (LIFT_MATCH "absrep_fun (default)") + end fun absrep_fun_chk flag ctxt (rty, qty) = absrep_fun flag ctxt (rty, qty) @@ -270,8 +274,8 @@ fun mk_rel_compose (trm1, trm2) = Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2 -fun get_relmap ctxt s = - (case Quotient_Info.lookup_quotmaps ctxt s of +fun get_relmap thy s = + (case Quotient_Info.lookup_quotmaps thy s of SOME map_data => Const (#relmap map_data, dummyT) | NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")) @@ -289,8 +293,8 @@ fold_rev Term.lambda vs' (mk_relmap_aux rty) end -fun get_equiv_rel ctxt s = - (case Quotient_Info.lookup_quotients ctxt s of +fun get_equiv_rel thy s = + (case Quotient_Info.lookup_quotients thy s of SOME qdata => #equiv_rel qdata | NONE => raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")) @@ -307,39 +311,43 @@ that will be the argument of Respects *) fun equiv_relation ctxt (rty, qty) = - if rty = qty - then HOLogic.eq_const rty - else - case (rty, qty) of - (Type (s, tys), Type (s', tys')) => - if s = s' - then - let - val args = map (equiv_relation ctxt) (tys ~~ tys') - in - list_comb (get_relmap ctxt s, args) - end - else - let - val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' - val rtyenv = match ctxt equiv_match_err rty_pat rty - val qtyenv = match ctxt equiv_match_err qty_pat qty - val args_aux = map (double_lookup rtyenv qtyenv) vs - val args = map (equiv_relation ctxt) args_aux - val eqv_rel = get_equiv_rel ctxt s' - val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool}) - in - if forall is_eq args - then eqv_rel' - else - let - val rel_map = mk_relmap ctxt vs rty_pat - val result = list_comb (rel_map, args) - in - mk_rel_compose (result, eqv_rel') - end - end - | _ => HOLogic.eq_const rty + let + val thy = Proof_Context.theory_of ctxt + in + if rty = qty + then HOLogic.eq_const rty + else + case (rty, qty) of + (Type (s, tys), Type (s', tys')) => + if s = s' + then + let + val args = map (equiv_relation ctxt) (tys ~~ tys') + in + list_comb (get_relmap ctxt s, args) + end + else + let + val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty thy s' + val rtyenv = match ctxt equiv_match_err rty_pat rty + val qtyenv = match ctxt equiv_match_err qty_pat qty + val args_aux = map (double_lookup rtyenv qtyenv) vs + val args = map (equiv_relation ctxt) args_aux + val eqv_rel = get_equiv_rel ctxt s' + val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool}) + in + if forall is_eq args + then eqv_rel' + else + let + val rel_map = mk_relmap ctxt vs rty_pat + val result = list_comb (rel_map, args) + in + mk_rel_compose (result, eqv_rel') + end + end + | _ => HOLogic.eq_const rty + end fun equiv_relation_chk ctxt (rty, qty) = equiv_relation ctxt (rty, qty) @@ -419,19 +427,22 @@ (* Checks that two types match, for example: rty -> rty matches qty -> qty *) 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 ctxt) rtys qtys) - else - (case Quotient_Info.lookup_quotients ctxt qs of - SOME quotinfo => - Sign.typ_instance (Proof_Context.theory_of ctxt) (rT, #rtyp quotinfo) - | NONE => false) - | _ => false) + let + val thy = Proof_Context.theory_of ctxt + in + 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 ctxt) rtys qtys) + else + (case Quotient_Info.lookup_quotients_global thy qs of + SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo) + | NONE => false) + | _ => false) + end (* produces a regularized version of rtrm @@ -556,7 +567,7 @@ else let val rtrm' = - (case Quotient_Info.lookup_quotconsts ctxt qtrm of + (case Quotient_Info.lookup_quotconsts_global thy qtrm of SOME qconst_info => #rconst qconst_info | NONE => term_mismatch "regularize (constant not found)" ctxt rtrm qtrm) in diff -r 2838109364f0 -r 98ec8b51af9c src/HOL/Tools/Quotient/quotient_typ.ML --- a/src/HOL/Tools/Quotient/quotient_typ.ML Fri Nov 04 13:52:19 2011 +0100 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML Fri Nov 04 17:19:33 2011 +0100 @@ -193,12 +193,13 @@ end (* check for existence of map functions *) -fun map_check ctxt (_, (rty, _, _)) = +fun map_check thy (_, (rty, _, _)) = let fun map_check_aux rty warns = (case rty of Type (_, []) => warns - | Type (s, _) => if is_some (Quotient_Info.lookup_quotmaps ctxt s) then warns else s :: warns + | Type (s, _) => + if is_some (Quotient_Info.lookup_quotmaps_global thy s) then warns else s :: warns | _ => warns) val warns = map_check_aux rty [] @@ -230,7 +231,7 @@ let (* sanity check *) val _ = List.app sanity_check quot_list - val _ = List.app (map_check lthy) quot_list + val _ = List.app (map_check (Proof_Context.theory_of lthy)) quot_list fun mk_goal (rty, rel, partial) = let