# HG changeset patch # User kuncar # Date 1323436602 -3600 # Node ID 2373d86cf2e85fd4afaa7e4891f9b44ac8390d6e # Parent 977cf00fb8d3b748a120691ca4a7eddbdc0dbbfa# Parent 16e8e4d33c426d5753459e8ec9dbf3b448b87b5e merged diff -r 16e8e4d33c42 -r 2373d86cf2e8 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Dec 09 13:42:16 2011 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Dec 09 14:16:42 2011 +0100 @@ -720,12 +720,12 @@ | is_rep_fun _ _ = false fun is_quot_abs_fun ctxt (x as (_, Type (@{type_name fun}, [_, abs_T as Type (s', _)]))) = - try (Quotient_Term.absrep_const_chk Quotient_Term.AbsF ctxt) s' + try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.AbsF) s' = SOME (Const x) andalso not (is_codatatype ctxt abs_T) | is_quot_abs_fun _ _ = false fun is_quot_rep_fun ctxt (x as (_, Type (@{type_name fun}, [abs_T as Type (s', _), _]))) = - try (Quotient_Term.absrep_const_chk Quotient_Term.RepF ctxt) s' + try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.RepF) s' = SOME (Const x) andalso not (is_codatatype ctxt abs_T) | is_quot_rep_fun _ _ = false diff -r 16e8e4d33c42 -r 2373d86cf2e8 src/HOL/Tools/Quotient/quotient_def.ML --- a/src/HOL/Tools/Quotient/quotient_def.ML Fri Dec 09 13:42:16 2011 +0100 +++ b/src/HOL/Tools/Quotient/quotient_def.ML Fri Dec 09 14:16:42 2011 +0100 @@ -64,7 +64,7 @@ else error_msg binding lhs_str | _ => raise Match) - val absrep_trm = Quotient_Term.absrep_fun Quotient_Term.AbsF lthy (fastype_of rhs, lhs_ty) $ rhs + val absrep_trm = Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (fastype_of rhs, lhs_ty) $ rhs val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm) val (_, prop') = Local_Defs.cert_def lthy prop val (_, newrhs) = Local_Defs.abs_def prop' diff -r 16e8e4d33c42 -r 2373d86cf2e8 src/HOL/Tools/Quotient/quotient_term.ML --- a/src/HOL/Tools/Quotient/quotient_term.ML Fri Dec 09 13:42:16 2011 +0100 +++ b/src/HOL/Tools/Quotient/quotient_term.ML Fri Dec 09 14:16:42 2011 +0100 @@ -11,11 +11,11 @@ datatype flag = AbsF | RepF - val absrep_fun: flag -> Proof.context -> typ * typ -> term - val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term + val absrep_fun: Proof.context -> flag -> typ * typ -> term + val absrep_fun_chk: Proof.context -> flag -> typ * typ -> term (* Allows Nitpick to represent quotient types as single elements from raw type *) - val absrep_const_chk: flag -> Proof.context -> string -> term + val absrep_const_chk: Proof.context -> flag -> string -> term val equiv_relation: Proof.context -> typ * typ -> term val equiv_relation_chk: Proof.context -> typ * typ -> term @@ -62,53 +62,30 @@ AbsF => Const (@{const_name comp}, dummyT) $ trm1 $ trm2 | RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1 -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.")) +fun get_mapfun_data ctxt s = + (case Symtab.lookup (Enriched_Type.entries ctxt) s of + SOME [map_data] => (case try dest_Const (#mapper map_data) of + SOME (c, _) => (Const (c, dummyT), #variances map_data) + | NONE => raise LIFT_MATCH ("map function for type " ^ quote s ^ " is not a constant.")) + | SOME _ => raise LIFT_MATCH ("map function for type " ^ quote s ^ " is non-singleton entry.") + | NONE => raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")) +fun defined_mapfun_data ctxt s = + Symtab.defined (Enriched_Type.entries ctxt) s + (* makes a Free out of a TVar *) fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT) -(* produces an aggregate map function for the - rty-part of a quotient definition; abstracts - over all variables listed in vs (these variables - correspond to the type variables in rty) - - for example for: (?'a list * ?'b) - it produces: %a b. prod_map (map a) b -*) -fun mk_mapfun thy vs rty = - let - val vs' = map mk_Free vs - - fun mk_mapfun_aux rty = - case rty of - TVar _ => mk_Free rty - | Type (_, []) => mk_identity rty - | 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) - end - (* looks up the (varified) rty and qty for a quotient definition *) -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.")) - -(* takes two type-environments and looks - up in both of them the variable v, which - must be listed in the environment -*) -fun double_lookup rtyenv qtyenv v = +fun get_rty_qty ctxt s = let - val v' = fst (dest_TVar v) + val thy = Proof_Context.theory_of ctxt in - (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v'))) + (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.")) end (* matches a type pattern with a type *) @@ -121,7 +98,7 @@ end (* produces the rep or abs constant for a qty *) -fun absrep_const flag ctxt qty_str = +fun absrep_const ctxt flag qty_str = let (* FIXME *) fun mk_dummyT (Const (c, _)) = Const (c, dummyT) @@ -137,8 +114,8 @@ end (* Lets Nitpick represent elements of quotient types as elements of the raw type *) -fun absrep_const_chk flag ctxt qty_str = - Syntax.check_term ctxt (absrep_const flag ctxt qty_str) +fun absrep_const_chk ctxt flag qty_str = + Syntax.check_term ctxt (absrep_const ctxt flag qty_str) fun absrep_match_err ctxt ty_pat ty = let @@ -193,52 +170,71 @@ identity maps. *) -fun absrep_fun flag ctxt (rty, qty) = +fun absrep_fun ctxt flag (rty, qty) = let - val thy = Proof_Context.theory_of ctxt + fun absrep_args tys tys' variances = + let + fun absrep_arg (types, (_, variant)) = + (case variant of + (false, false) => [] + | (true, false) => [(absrep_fun ctxt flag types)] + | (false, true) => [(absrep_fun ctxt (negF flag) types)] + | (true, true) => [(absrep_fun ctxt flag types),(absrep_fun ctxt (negF flag) types)]) + in + maps absrep_arg ((tys ~~ tys') ~~ variances) + end + fun test_identities tys rtys' s s' = + let + val args = map (absrep_fun ctxt flag) (tys ~~ rtys') + in + if forall is_identity args + then + absrep_const ctxt flag s' + else + raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.") + end in 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 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 - get_mapfun thy "Set.set" $ arg - end - | (Type (s, tys), Type (s', tys')) => + (Type (s, tys), Type (s', tys')) => if s = s' then let - val args = map (absrep_fun flag ctxt) (tys ~~ tys') + val (map_fun, variances) = get_mapfun_data ctxt s + val args = absrep_args tys tys' variances in - list_comb (get_mapfun thy s, args) + list_comb (map_fun, 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 (Type (_, rtys), qty_pat) = get_rty_qty ctxt s' 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 + val rtys' = map (Envir.subst_type qtyenv) rtys in - if forall is_identity args - then absrep_const flag ctxt s' + if not (defined_mapfun_data ctxt s) + then + (* + If we don't know a map function for the raw type, + we are not necessarilly in troubles because + it can still be the case we don't need the map + function <=> all abs/rep functions are identities. + *) + test_identities tys rtys' s s' else let - val map_fun = mk_mapfun thy vs rty_pat - val result = list_comb (map_fun, args) + val (map_fun, variances) = get_mapfun_data ctxt s + val args = absrep_args tys rtys' variances in - mk_fun_compose flag (absrep_const flag ctxt s', result) + if forall is_identity args + then absrep_const ctxt flag s' + else + let + val result = list_comb (map_fun, args) + in + mk_fun_compose flag (absrep_const ctxt flag s', result) + end end end | (TFree x, TFree x') => @@ -249,13 +245,12 @@ | _ => raise (LIFT_MATCH "absrep_fun (default)") end -fun absrep_fun_chk flag ctxt (rty, qty) = - absrep_fun flag ctxt (rty, qty) +fun absrep_fun_chk ctxt flag (rty, qty) = + absrep_fun ctxt flag (rty, qty) |> Syntax.check_term ctxt - (*** Aggregate Equivalence Relation ***) @@ -284,6 +279,17 @@ SOME map_data => Const (#relmap map_data, dummyT) | NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")) +(* takes two type-environments and looks + up in both of them the variable v, which + must be listed in the environment +*) +fun double_lookup rtyenv qtyenv v = + let + val v' = fst (dest_TVar v) + in + (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v'))) + end + fun mk_relmap ctxt vs rty = let val vs' = map (mk_Free) vs @@ -316,43 +322,40 @@ that will be the argument of Respects *) fun equiv_relation ctxt (rty, qty) = - 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 + 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 + fun equiv_relation_chk ctxt (rty, qty) = equiv_relation ctxt (rty, qty) @@ -642,7 +645,7 @@ *) fun mk_repabs ctxt (T, T') trm = - absrep_fun RepF ctxt (T, T') $ (absrep_fun AbsF ctxt (T, T') $ trm) + absrep_fun ctxt RepF (T, T') $ (absrep_fun ctxt AbsF (T, T') $ trm) fun inj_repabs_err ctxt msg rtrm qtrm = let diff -r 16e8e4d33c42 -r 2373d86cf2e8 src/HOL/Tools/Quotient/quotient_type.ML --- a/src/HOL/Tools/Quotient/quotient_type.ML Fri Dec 09 13:42:16 2011 +0100 +++ b/src/HOL/Tools/Quotient/quotient_type.ML Fri Dec 09 14:16:42 2011 +0100 @@ -197,13 +197,13 @@ end (* check for existence of map functions *) -fun map_check thy (_, (rty, _, _), _) = +fun map_check ctxt (_, (rty, _, _), _) = let fun map_check_aux rty warns = (case rty of Type (_, []) => warns | Type (s, _) => - if is_some (Quotient_Info.lookup_quotmaps_global thy s) then warns else s :: warns + if Symtab.defined (Enriched_Type.entries ctxt) s then warns else s :: warns | _ => warns) val warns = map_check_aux rty [] @@ -234,7 +234,7 @@ let (* sanity check *) val _ = List.app sanity_check quot_list - val _ = List.app (map_check (Proof_Context.theory_of lthy)) quot_list + val _ = List.app (map_check lthy) quot_list fun mk_goal (rty, rel, partial) = let