# HG changeset patch # User Christian Urban # Date 1261811205 -3600 # Node ID fb4bfbb1a2911bae372365662e039b6df9689fdf # Parent 3a48ffcf0f9a0f5624c18ef5aea9bc55ad4df73a commeted the absrep function diff -r 3a48ffcf0f9a -r fb4bfbb1a291 Quot/quotient_term.ML --- 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: