--- a/QuotMain.thy Wed Oct 28 10:29:00 2009 +0100
+++ b/QuotMain.thy Wed Oct 28 15:25:11 2009 +0100
@@ -147,32 +147,7 @@
ML {* maps_lookup @{theory} "*" *}
ML {* maps_lookup @{theory} "fun" *}
-ML {*
-fun matches ty1 ty2 =
- Type.raw_instance (ty1, Logic.varifyT ty2)
-*}
-
-
-
-ML {*
-val quot_def_parser =
- (OuterParse.$$$ "(" |-- OuterParse.$$$ "with" |--
- ((OuterParse.list1 OuterParse.typ) --| OuterParse.$$$ ")")) --
- (OuterParse.binding --
- Scan.option (OuterParse.$$$ "::" |-- OuterParse.typ) --
- OuterParse.mixfix --| OuterParse.where_ -- SpecParse.spec)
-*}
-
-ML {*
-fun test (qrtys, (((bind, typstr), mx), (attr, prop))) lthy = lthy
-*}
-
-ML {*
-val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"
- OuterKeyword.thy_decl (quot_def_parser >> test)
-*}
-
-(* FIXME: auxiliary function *)
+text {* FIXME: auxiliary function *}
ML {*
val no_vars = Thm.rule_attribute (fn context => fn th =>
let
@@ -184,7 +159,19 @@
section {* lifting of constants *}
ML {*
+(* whether ty1 is an instance of ty2 *)
+fun matches (ty1, ty2) =
+ Type.raw_instance (ty1, Logic.varifyT ty2)
+fun lookup_snd _ [] _ = NONE
+ | lookup_snd eq ((value, key)::xs) key' =
+ if eq (key', key) then SOME value
+ else lookup_snd eq xs key';
+
+fun lookup_qenv qenv qty =
+ (case (AList.lookup matches qenv qty) of
+ SOME rty => SOME (qty, rty)
+ | NONE => NONE)
*}
ML {*
@@ -198,10 +185,9 @@
fun negF absF = repF
| negF repF = absF
-fun get_fun flag rty qty lthy ty =
+fun get_fun flag qenv lthy ty =
let
- val qty_name = Long_Name.base_name (fst (dest_Type qty))
-
+
fun get_fun_aux s fs_tys =
let
val (fs, tys) = split_list fs_tys
@@ -226,22 +212,27 @@
(list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty))
end
- val thy = ProofContext.theory_of lthy
-
- fun get_const absF = (Const (Sign.full_bname thy ("ABS_" ^ qty_name), rty --> qty), (rty, qty))
- | get_const repF = (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty))
+ fun get_const flag (qty, rty) =
+ let
+ val thy = ProofContext.theory_of lthy
+ val qty_name = Long_Name.base_name (fst (dest_Type qty))
+ in
+ case flag of
+ absF => (Const (Sign.full_bname thy ("ABS_" ^ qty_name), rty --> qty), (rty, qty))
+ | repF => (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty))
+ end
fun mk_identity ty = Abs ("", ty, Bound 0)
in
- if ty = qty
- then (get_const flag)
+ if (AList.defined matches qenv ty)
+ then (get_const flag (the (lookup_qenv qenv ty)))
else (case ty of
TFree _ => (mk_identity ty, (ty, ty))
| Type (_, []) => (mk_identity ty, (ty, ty))
| Type ("fun" , [ty1, ty2]) =>
- get_fun_fun [get_fun (negF flag) rty qty lthy ty1, get_fun flag rty qty lthy ty2]
- | Type (s, tys) => get_fun_aux s (map (get_fun flag rty qty lthy) tys)
+ get_fun_fun [get_fun (negF flag) qenv lthy ty1, get_fun flag qenv lthy ty2]
+ | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys)
| _ => raise ERROR ("no type variables")
)
end
@@ -251,50 +242,104 @@
text {* produces the definition for a lifted constant *}
ML {*
-fun get_const_def nconst oconst rty qty lthy =
+fun get_const_def nconst otrm qenv lthy =
let
val ty = fastype_of nconst
val (arg_tys, res_ty) = strip_type ty
- val fresh_args = arg_tys |> map (pair "x")
- |> Variable.variant_frees lthy [nconst, oconst]
- |> map Free
-
- val rep_fns = map (fst o get_fun repF rty qty lthy) arg_tys
- val abs_fn = (fst o get_fun absF rty qty lthy) res_ty
+ val rep_fns = map (fst o get_fun repF qenv lthy) arg_tys
+ val abs_fn = (fst o get_fun absF qenv lthy) res_ty
fun mk_fun_map (t1,t2) = Const (@{const_name "fun_map"}, dummyT) $ t1 $ t2
- val fns = Library.foldr (mk_fun_map) (rep_fns, abs_fn)
+ val fns = Library.foldr mk_fun_map (rep_fns, abs_fn)
|> Syntax.check_term lthy
in
- fns $ oconst
+ fns $ otrm
end
*}
+ML {* lookup_snd *}
+
ML {*
-fun exchange_ty rty qty ty =
- if ty = rty
- then qty
- else
+fun exchange_ty qenv ty =
+ case (lookup_snd matches qenv ty) of
+ SOME qty => qty
+ | NONE =>
(case ty of
- Type (s, tys) => Type (s, map (exchange_ty rty qty) tys)
+ Type (s, tys) => Type (s, map (exchange_ty qenv) tys)
| _ => ty
)
*}
ML {*
-fun make_const_def nconst_bname oconst mx rty qty lthy =
+fun make_const_def nconst_bname otrm mx qenv lthy =
let
- val oconst_ty = fastype_of oconst
- val nconst_ty = exchange_ty rty qty oconst_ty
+ val otrm_ty = fastype_of otrm
+ val nconst_ty = exchange_ty qenv otrm_ty
val nconst = Const (Binding.name_of nconst_bname, nconst_ty)
- val def_trm = get_const_def nconst oconst rty qty lthy
+ val def_trm = get_const_def nconst otrm qenv lthy
in
define (nconst_bname, mx, def_trm) lthy
end
*}
+ML {*
+fun build_qenv lthy qtys =
+let
+ val qenv = map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) (quotdata_lookup lthy)
+
+ fun find_assoc qty =
+ case (AList.lookup matches qenv qty) of
+ SOME rty => (qty, rty)
+ | NONE => error (implode
+ ["Quotient type ",
+ quote (Syntax.string_of_typ lthy qty),
+ " does not exists"])
+in
+ map find_assoc qtys
+end
+*}
+
+ML {*
+(* taken from isar_syn.ML *)
+val constdecl =
+ OuterParse.binding --
+ (OuterParse.where_ >> K (NONE, NoSyn) ||
+ OuterParse.$$$ "::" |-- OuterParse.!!! ((OuterParse.typ >> SOME) --
+ OuterParse.opt_mixfix' --| OuterParse.where_) ||
+ Scan.ahead (OuterParse.$$$ "(") |--
+ OuterParse.!!! (OuterParse.mixfix' --| OuterParse.where_ >> pair NONE))
+*}
+
+ML {*
+val qd_parser =
+ (Args.parens (OuterParse.$$$ "for" |-- (Scan.repeat OuterParse.typ))) --
+ (constdecl -- (SpecParse.opt_thm_name ":" -- OuterParse.prop))
+*}
+
+ML {*
+fun pair lthy (ty1, ty2) =
+ "(" ^ (Syntax.string_of_typ lthy ty1) ^ "," ^ (Syntax.string_of_typ lthy ty2) ^ ")"
+*}
+
+ML {*
+fun parse_qd_spec (qtystrs, ((bind, (typstr__, mx)), (attr__, propstr))) lthy =
+let
+ val qtys = map (Syntax.check_typ lthy o Syntax.parse_typ lthy) qtystrs
+ val qenv = build_qenv lthy qtys
+ val prop = Syntax.parse_prop lthy propstr |> Syntax.check_prop lthy
+ val (lhs, rhs) = Logic.dest_equals prop
+in
+ make_const_def bind rhs mx qenv lthy |> snd
+end
+*}
+
+ML {*
+val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"
+ OuterKeyword.thy_decl (qd_parser >> parse_qd_spec)
+*}
+
section {* ATOMIZE *}
text {*
@@ -587,17 +632,36 @@
by (simp add: id_def)
ML {*
+fun old_exchange_ty rty qty ty =
+ if ty = rty
+ then qty
+ else
+ (case ty of
+ Type (s, tys) => Type (s, map (old_exchange_ty rty qty) tys)
+ | _ => ty
+ )
+*}
+
+ML {*
+fun old_get_fun flag rty qty lthy ty =
+ get_fun flag [(qty, rty)] lthy ty
+
+fun old_make_const_def nconst_bname otrm mx rty qty lthy =
+ make_const_def nconst_bname otrm mx [(qty, rty)] lthy
+*}
+
+ML {*
fun build_repabs_term lthy thm constructors rty qty =
let
fun mk_rep tm =
let
- val ty = exchange_ty rty qty (fastype_of tm)
- in fst (get_fun repF rty qty lthy ty) $ tm end
+ val ty = old_exchange_ty rty qty (fastype_of tm)
+ in fst (old_get_fun repF rty qty lthy ty) $ tm end
fun mk_abs tm =
let
- val ty = exchange_ty rty qty (fastype_of tm) in
- fst (get_fun absF rty qty lthy ty) $ tm end
+ val ty = old_exchange_ty rty qty (fastype_of tm) in
+ fst (old_get_fun absF rty qty lthy ty) $ tm end
fun is_constructor (Const (x, _)) = member (op =) constructors x
| is_constructor _ = false;