1415 *} |
1415 *} |
1416 |
1416 |
1417 no_notation |
1417 no_notation |
1418 list_eq (infix "\<approx>" 50) |
1418 list_eq (infix "\<approx>" 50) |
1419 |
1419 |
|
1420 ML {* |
|
1421 open Quotient_Info; |
|
1422 |
|
1423 exception LIFT_MATCH of string |
|
1424 |
|
1425 |
|
1426 |
|
1427 (*** Aggregate Rep/Abs Function ***) |
|
1428 |
|
1429 |
|
1430 (* The flag RepF is for types in negative position; AbsF is for types |
|
1431 in positive position. Because of this, function types need to be |
|
1432 treated specially, since there the polarity changes. |
|
1433 *) |
|
1434 |
|
1435 datatype flag = AbsF | RepF |
|
1436 |
|
1437 fun negF AbsF = RepF |
|
1438 | negF RepF = AbsF |
|
1439 |
|
1440 fun is_identity (Const (@{const_name "id"}, _)) = true |
|
1441 | is_identity _ = false |
|
1442 |
|
1443 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) |
|
1444 |
|
1445 fun mk_fun_compose flag (trm1, trm2) = |
|
1446 case flag of |
|
1447 AbsF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 |
|
1448 | RepF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 |
|
1449 |
|
1450 fun get_mapfun ctxt s = |
|
1451 let |
|
1452 val thy = ProofContext.theory_of ctxt |
|
1453 val exn = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.") |
|
1454 val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn |
|
1455 in |
|
1456 Const (mapfun, dummyT) |
1420 end |
1457 end |
|
1458 |
|
1459 (* makes a Free out of a TVar *) |
|
1460 fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT) |
|
1461 |
|
1462 (* produces an aggregate map function for the |
|
1463 rty-part of a quotient definition; abstracts |
|
1464 over all variables listed in vs (these variables |
|
1465 correspond to the type variables in rty) |
|
1466 |
|
1467 for example for: (?'a list * ?'b) |
|
1468 it produces: %a b. prod_map (map a) b |
|
1469 *) |
|
1470 fun mk_mapfun ctxt vs rty = |
|
1471 let |
|
1472 val vs' = map (mk_Free) vs |
|
1473 |
|
1474 fun mk_mapfun_aux rty = |
|
1475 case rty of |
|
1476 TVar _ => mk_Free rty |
|
1477 | Type (_, []) => mk_identity rty |
|
1478 | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys) |
|
1479 | _ => raise LIFT_MATCH "mk_mapfun (default)" |
|
1480 in |
|
1481 fold_rev Term.lambda vs' (mk_mapfun_aux rty) |
|
1482 end |
|
1483 |
|
1484 (* looks up the (varified) rty and qty for |
|
1485 a quotient definition |
|
1486 *) |
|
1487 fun get_rty_qty ctxt s = |
|
1488 let |
|
1489 val thy = ProofContext.theory_of ctxt |
|
1490 val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.") |
|
1491 val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn |
|
1492 in |
|
1493 (#rtyp qdata, #qtyp qdata) |
|
1494 end |
|
1495 |
|
1496 (* takes two type-environments and looks |
|
1497 up in both of them the variable v, which |
|
1498 must be listed in the environment |
|
1499 *) |
|
1500 fun double_lookup rtyenv qtyenv v = |
|
1501 let |
|
1502 val v' = fst (dest_TVar v) |
|
1503 in |
|
1504 (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v'))) |
|
1505 end |
|
1506 |
|
1507 (* matches a type pattern with a type *) |
|
1508 fun match ctxt err ty_pat ty = |
|
1509 let |
|
1510 val thy = ProofContext.theory_of ctxt |
|
1511 in |
|
1512 Sign.typ_match thy (ty_pat, ty) Vartab.empty |
|
1513 handle MATCH_TYPE => err ctxt ty_pat ty |
|
1514 end |
|
1515 |
|
1516 (* produces the rep or abs constant for a qty *) |
|
1517 fun absrep_const flag ctxt qty_str = |
|
1518 let |
|
1519 val qty_name = Long_Name.base_name qty_str |
|
1520 val qualifier = Long_Name.qualifier qty_str |
|
1521 in |
|
1522 case flag of |
|
1523 AbsF => Const (Long_Name.qualify qualifier ("abs_" ^ qty_name), dummyT) |
|
1524 | RepF => Const (Long_Name.qualify qualifier ("rep_" ^ qty_name), dummyT) |
|
1525 end |
|
1526 |
|
1527 (* Lets Nitpick represent elements of quotient types as elements of the raw type *) |
|
1528 fun absrep_const_chk flag ctxt qty_str = |
|
1529 Syntax.check_term ctxt (absrep_const flag ctxt qty_str) |
|
1530 |
|
1531 fun absrep_match_err ctxt ty_pat ty = |
|
1532 let |
|
1533 val ty_pat_str = Syntax.string_of_typ ctxt ty_pat |
|
1534 val ty_str = Syntax.string_of_typ ctxt ty |
|
1535 in |
|
1536 raise LIFT_MATCH (space_implode " " |
|
1537 ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) |
|
1538 end |
|
1539 |
|
1540 |
|
1541 (** generation of an aggregate absrep function **) |
|
1542 |
|
1543 (* - In case of equal types we just return the identity. |
|
1544 |
|
1545 - In case of TFrees we also return the identity. |
|
1546 |
|
1547 - In case of function types we recurse taking |
|
1548 the polarity change into account. |
|
1549 |
|
1550 - If the type constructors are equal, we recurse for the |
|
1551 arguments and build the appropriate map function. |
|
1552 |
|
1553 - If the type constructors are unequal, there must be an |
|
1554 instance of quotient types: |
|
1555 |
|
1556 - we first look up the corresponding rty_pat and qty_pat |
|
1557 from the quotient definition; the arguments of qty_pat |
|
1558 must be some distinct TVars |
|
1559 - we then match the rty_pat with rty and qty_pat with qty; |
|
1560 if matching fails the types do not correspond -> error |
|
1561 - the matching produces two environments; we look up the |
|
1562 assignments for the qty_pat variables and recurse on the |
|
1563 assignments |
|
1564 - we prefix the aggregate map function for the rty_pat, |
|
1565 which is an abstraction over all type variables |
|
1566 - finally we compose the result with the appropriate |
|
1567 absrep function in case at least one argument produced |
|
1568 a non-identity function / |
|
1569 otherwise we just return the appropriate absrep |
|
1570 function |
|
1571 |
|
1572 The composition is necessary for types like |
|
1573 |
|
1574 ('a list) list / ('a foo) foo |
|
1575 |
|
1576 The matching is necessary for types like |
|
1577 |
|
1578 ('a * 'a) list / 'a bar |
|
1579 |
|
1580 The test is necessary in order to eliminate superfluous |
|
1581 identity maps. |
|
1582 *) |
|
1583 |
|
1584 fun absrep_fun flag ctxt (rty, qty) = |
|
1585 if rty = qty |
|
1586 then mk_identity rty |
|
1587 else |
|
1588 case (rty, qty) of |
|
1589 (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => |
|
1590 let |
|
1591 val arg1 = absrep_fun (negF flag) ctxt (ty1, ty1') |
|
1592 val arg2 = absrep_fun flag ctxt (ty2, ty2') |
|
1593 in |
|
1594 list_comb (get_mapfun ctxt "fun", [arg1, arg2]) |
|
1595 end |
|
1596 | (Type (s, tys), Type (s', tys')) => |
|
1597 if s = s' |
|
1598 then |
|
1599 let |
|
1600 val args = map (absrep_fun flag ctxt) (tys ~~ tys') |
|
1601 in |
|
1602 list_comb (get_mapfun ctxt s, args) |
|
1603 end |
|
1604 else |
|
1605 let |
|
1606 val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' |
|
1607 val rtyenv = match ctxt absrep_match_err rty_pat rty |
|
1608 val qtyenv = match ctxt absrep_match_err qty_pat qty |
|
1609 val args_aux = map (double_lookup rtyenv qtyenv) vs |
|
1610 val args = map (absrep_fun flag ctxt) args_aux |
|
1611 val map_fun = mk_mapfun ctxt vs rty_pat |
|
1612 val result = list_comb (map_fun, args) |
|
1613 in |
|
1614 (*if forall is_identity args |
|
1615 then absrep_const flag ctxt s' |
|
1616 else*) mk_fun_compose flag (absrep_const flag ctxt s', result) |
|
1617 end |
|
1618 | (TFree x, TFree x') => |
|
1619 if x = x' |
|
1620 then mk_identity rty |
|
1621 else raise (LIFT_MATCH "absrep_fun (frees)") |
|
1622 | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)") |
|
1623 | _ => raise (LIFT_MATCH "absrep_fun (default)") |
|
1624 |
|
1625 |
|
1626 *} |
|
1627 |
|
1628 ML {* |
|
1629 absrep_fun AbsF @{context} (@{typ "('a list) list \<Rightarrow> 'a list"}, @{typ "('a fset) fset \<Rightarrow> 'a fset"}) |
|
1630 |> Syntax.string_of_term @{context} |
|
1631 |> writeln |
|
1632 *} |
|
1633 |
|
1634 lemma "(\<lambda> (c::'s \<Rightarrow> bool). \<exists>(x::'s). c = rel x) = {c. \<exists>x. c = rel x}" |
|
1635 apply(auto simp add: mem_def) |
|
1636 done |
|
1637 |
|
1638 |
|
1639 end |