--- a/Quot/quotient_term.ML Sat Dec 26 07:15:30 2009 +0100
+++ b/Quot/quotient_term.ML Sat Dec 26 08:06:45 2009 +0100
@@ -21,13 +21,13 @@
exception LIFT_MATCH of string
-(*******************************)
-(* Aggregate Rep/Abs Functions *)
-(*******************************)
+(******************************)
+(* Aggregate Rep/Abs Function *)
+(******************************)
-(* The flag repF is for types in negative position, while absF is *)
-(* for types in positive position. Because of this, function types *)
-(* need to be treated specially, since there the polarity changes. *)
+(* The flag repF is for types in negative position; absF is for types *)
+(* in positive position. Because of this, function types need to be *)
+(* treated specially, since there the polarity changes. *)
datatype flag = absF | repF
@@ -37,6 +37,7 @@
val mk_id = Const (@{const_name "id"}, dummyT)
fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
+(* makes a Free out of a TVar *)
fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
fun mk_compose flag (trm1, trm2) =
@@ -53,6 +54,10 @@
Const (mapfun, dummyT)
end
+(* 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 *)
fun mk_mapfun ctxt vs ty =
let
val vs' = map (mk_Free) vs
@@ -67,6 +72,8 @@
fold_rev Term.lambda vs' (mk_mapfun_aux ty)
end
+(* looks up the (varified) rty and qty for *)
+(* a quotient definition *)
fun get_rty_qty ctxt s =
let
val thy = ProofContext.theory_of ctxt
@@ -76,6 +83,8 @@
(#rtyp qdata, #qtyp qdata)
end
+(* receives two type-environments and looks *)
+(* up in both of them the variable v *)
fun double_lookup rtyenv qtyenv v =
let
val v' = fst (dest_TVar v)
@@ -83,6 +92,7 @@
(snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v')))
end
+(* produces the rep or abs constants for a qty *)
fun absrep_const flag ctxt qty_str =
let
val thy = ProofContext.theory_of ctxt
@@ -93,6 +103,37 @@
| repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT)
end
+(* produces the aggregate absrep function *)
+(* *)
+(* - In case of function types and TFrees, we recurse, taking in *)
+(* the first case the polarity change into account. *)
+(* *)
+(* - If the type constructors are equal, we recurse for the *)
+(* arguments and prefix the appropriate map function *)
+(* *)
+(* - If the type constructors are unequal, there must be an *)
+(* instance of quotient types: *)
+(* - we first look up the corresponding rty_pat and qty_pat *)
+(* from the quotient definition; the arguments of qty_pat *)
+(* must be some distinct TVars *)
+(* - we then match the rty_pat with rty and qty_pat with qty; *)
+(* if matching fails the types do not match *)
+(* - the matching produces two environments, we look up the *)
+(* assignments for the qty_pat variables and recurse on the *)
+(* assignmetnts *)
+(* - we prefix the aggregate map function for the rty_pat, *)
+(* which is an abstraction over all type variables *)
+(* - finally we compse the result with the appropriate *)
+(* absrep function *)
+(* *)
+(* The composition is necessary for types like *)
+(* *)
+(* ('a list) list / ('a foo) foo *)
+(* *)
+(* The matching is necessary for types like *)
+(* *)
+(* ('a * 'a) list / 'a bar *)
+
fun absrep_fun flag ctxt (rty, qty) =
if rty = qty
then mk_identity qty
@@ -116,9 +157,12 @@
else
let
val thy = ProofContext.theory_of ctxt
+ val exc = (LIFT_MATCH "absrep_fun (Types do not match.)")
val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
- val rtyenv = Sign.typ_match thy (rty_pat, rty) Vartab.empty
- val qtyenv = Sign.typ_match thy (qty_pat, qty) Vartab.empty
+ val (rtyenv, qtyenv) =
+ (Sign.typ_match thy (rty_pat, rty) Vartab.empty,
+ Sign.typ_match thy (qty_pat, qty) Vartab.empty)
+ handle MATCH_TYPE => raise exc
val args_aux = map (double_lookup rtyenv qtyenv) vs
val args = map (absrep_fun flag ctxt) args_aux
val map_fun = mk_mapfun ctxt vs rty_pat
@@ -131,25 +175,12 @@
then mk_identity qty
else raise (LIFT_MATCH "absrep_fun (frees)")
| (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)")
- | _ =>
- let
- val rty_str = Syntax.string_of_typ ctxt rty
- val qty_str = Syntax.string_of_typ ctxt qty
- in
- raise (LIFT_MATCH ("absrep_fun (default) " ^ rty_str ^ " " ^ qty_str))
- end
+ | _ => raise (LIFT_MATCH "absrep_fun (default)")
fun absrep_fun_chk flag ctxt (rty, qty) =
-let
- val rty_str = Syntax.string_of_typ ctxt rty
- val qty_str = Syntax.string_of_typ ctxt qty
- val _ = tracing "rty / qty"
- val _ = tracing rty_str
- val _ = tracing qty_str
-in
absrep_fun flag ctxt (rty, qty)
|> Syntax.check_term ctxt
-end
+
(* Regularizing an rtrm means: