--- a/QuotMain.thy Wed Nov 04 09:52:31 2009 +0100
+++ b/QuotMain.thy Wed Nov 04 10:31:20 2009 +0100
@@ -143,12 +143,6 @@
(* the auxiliary data for the quotient types *)
use "quotient_info.ML"
-ML {*
-fun error_msg pre post msg =
- msg |> quote
- |> enclose (pre ^ " ") (" " ^ post)
- |> error
-*}
declare [[map list = (map, LIST_REL)]]
declare [[map * = (prod_fun, prod_rel)]]
@@ -175,13 +169,9 @@
section {* lifting of constants *}
ML {*
-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 (op =) qenv qty) of
+ (case (AList.lookup (op=) qenv qty) of
SOME rty => SOME (qty, rty)
| NONE => NONE)
*}
@@ -210,7 +200,7 @@
in
(case (maps_lookup (ProofContext.theory_of lthy) s) of
SOME info => (list_comb (Const (#mapfun info, ftys ---> (oty --> nty)), fs), (oty, nty))
- | NONE => raise ERROR ("no map association for type " ^ s))
+ | NONE => error ("no map association for type " ^ s))
end
fun get_fun_fun fs_tys =
@@ -237,7 +227,7 @@
fun mk_identity ty = Abs ("", ty, Bound 0)
in
- if (AList.defined (op =) qenv ty)
+ if (AList.defined (op=) qenv ty)
then (get_const flag (the (lookup_qenv qenv ty)))
else (case ty of
TFree _ => (mk_identity ty, (ty, ty))
@@ -250,64 +240,26 @@
end
*}
-text {* produces the definition for a lifted constant *}
-
ML {*
-fun get_const_def nconst otrm qenv lthy =
+fun make_def nconst_bname rhs qty mx qenv lthy =
let
- val ty = fastype_of nconst
- val (arg_tys, res_ty) = strip_type ty
+ val (arg_tys, res_ty) = strip_type qty
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)
- |> Syntax.check_term lthy
-in
- fns $ otrm
-end
-*}
-
-
-ML {*
-fun exchange_ty qenv ty =
- case (lookup_snd (op =) qenv ty) of
- SOME qty => qty
- | NONE =>
- (case ty of
- Type (s, tys) => Type (s, map (exchange_ty qenv) tys)
- | _ => ty
- )
-*}
+ fun mk_fun_map t s =
+ Const (@{const_name "fun_map"}, dummyT) $ t $ s
-ML {*
-fun ppair lthy (ty1, ty2) =
- "(" ^ (Syntax.string_of_typ lthy ty1) ^ "," ^ (Syntax.string_of_typ lthy ty2) ^ ")"
-*}
-
-ML {*
-fun print_env qenv lthy =
- map (ppair lthy) qenv
- |> commas
- |> tracing
-*}
-
-ML {*
-fun make_const_def nconst_bname otrm mx qenv lthy =
-let
- 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 otrm qenv lthy
+ val absrep_fn = fold_rev mk_fun_map rep_fns abs_fn
+ |> Syntax.check_term lthy
in
- define (nconst_bname, mx, def_trm) lthy
+ define (nconst_bname, mx, absrep_fn $ rhs) lthy
end
*}
ML {*
-(* difference of two types *)
+(* returns all subterms where two types differ *)
fun diff (T, S) Ds =
case (T, S) of
(TVar v, TVar u) => if v = u then Ds else (T, S)::Ds
@@ -321,42 +273,73 @@
*}
ML {*
-fun quotdef_cmd ((bind, qty, mx), (attr, prop)) lthy =
-let
- val (_, rhs) = Logic.dest_equals prop
- val rty = fastype_of rhs
- val qenv = distinct (op=) (diff (qty, rty) [])
+fun error_msg lthy (qty, rty) =
+let
+ val qtystr = quote (Syntax.string_of_typ lthy qty)
+ val rtystr = quote (Syntax.string_of_typ lthy rty)
in
- make_const_def bind rhs mx qenv lthy
+ error (implode ["Quotient type ", qtystr, " does not match with ", rtystr])
+end
+
+
+fun sanity_chk lthy qenv =
+let
+ val qenv' = Quotient_Info.mk_qenv lthy
+ val thy = ProofContext.theory_of lthy
+
+ fun is_inst thy (qty, rty) (qty', rty') =
+ if Sign.typ_instance thy (qty, qty')
+ then let
+ val inst = Sign.typ_match thy (qty', qty) Vartab.empty
+ in
+ rty = Envir.subst_type inst rty'
+ end
+ else false
+
+ fun chk_inst (qty, rty) =
+ if exists (is_inst thy (qty, rty)) qenv' then true
+ else error_msg lthy (qty, rty)
+in
+ forall chk_inst qenv
end
*}
ML {*
-val constdecl =
- OuterParse.binding --
- (OuterParse.$$$ "::" |-- OuterParse.!!!
- (OuterParse.typ -- OuterParse.opt_mixfix' --| OuterParse.where_))
- >> OuterParse.triple2;
+fun quotdef ((bind, qty, mx), (attr, prop)) lthy =
+let
+ val (_, prop') = PrimitiveDefs.dest_def lthy (K true) (K false) (K false) prop
+ val (_, rhs) = PrimitiveDefs.abs_def prop'
+
+ val rty = fastype_of rhs
+ val qenv = distinct (op=) (diff (qty, rty) [])
+
+in
+ sanity_chk lthy qenv;
+ make_def bind rhs qty mx qenv lthy
+end
*}
ML {*
-val quotdef_parser =
- (constdecl -- (SpecParse.opt_thm_name ":" -- OuterParse.prop))
+val quotdef_parser =
+ (OuterParse.binding --
+ (OuterParse.$$$ "::" |-- OuterParse.!!! (OuterParse.typ --
+ OuterParse.opt_mixfix' --| OuterParse.where_)) >> OuterParse.triple2) --
+ (SpecParse.opt_thm_name ":" -- OuterParse.prop)
*}
ML {*
-fun quotdef ((bind, qtystr, mx), (attr, propstr)) lthy =
+fun quotdef_cmd ((bind, qtystr, mx), (attr, propstr)) lthy =
let
val qty = (Syntax.check_typ lthy o Syntax.parse_typ lthy) qtystr
val prop = (Syntax.check_prop lthy o Syntax.parse_prop lthy) propstr
in
- quotdef_cmd ((bind, qty, mx), (attr, prop)) lthy |> snd
+ quotdef ((bind, qty, mx), (attr, prop)) lthy |> snd
end
*}
ML {*
val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"
- OuterKeyword.thy_decl (quotdef_parser >> quotdef)
+ OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)
*}
section {* ATOMIZE *}
@@ -595,7 +578,7 @@
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
+ make_def nconst_bname otrm qty mx [(qty, rty)] lthy
*}
text {* Does the same as 'subst' in a given prop or theorem *}