1378 fun mk_repabs lthy (T, T') trm = |
1378 fun mk_repabs lthy (T, T') trm = |
1379 Quotient_Def.get_fun repF lthy (T, T') |
1379 Quotient_Def.get_fun repF lthy (T, T') |
1380 $ (Quotient_Def.get_fun absF lthy (T, T') $ trm) |
1380 $ (Quotient_Def.get_fun absF lthy (T, T') $ trm) |
1381 *} |
1381 *} |
1382 |
1382 |
1383 ML {* |
1383 ML {* length *} |
1384 (* replaces a term for the bound variable, *) |
|
1385 (* possible capture *) |
|
1386 fun replace_bnd0 (trm, Abs (x, T, t)) = |
|
1387 Abs (x, T, subst_bound (trm, t)) |
|
1388 |
|
1389 (* FIXME: this should be a proper test with the qcinfo *) |
|
1390 fun is_lifted_const h gh = |
|
1391 is_Const h andalso is_Const gh andalso not (h = gh) |
|
1392 *} |
|
1393 |
|
1394 |
1384 |
1395 ML {* |
1385 ML {* |
1396 (* bound variables need to be treated properly, *) |
1386 (* bound variables need to be treated properly, *) |
1397 (* as the type of subterms need to be calculated *) |
1387 (* as the type of subterms need to be calculated *) |
|
1388 |
1398 |
1389 |
1399 fun inj_REPABS lthy (rtrm, qtrm) = |
1390 fun inj_REPABS lthy (rtrm, qtrm) = |
1400 let |
1391 let |
1401 val rty = fastype_of rtrm |
1392 val rty = fastype_of rtrm |
1402 val qty = fastype_of qtrm |
1393 val qty = fastype_of qtrm |
1411 | (Abs (x, T, t), Abs (x', T', t')) => |
1402 | (Abs (x, T, t), Abs (x', T', t')) => |
1412 let |
1403 let |
1413 val (y, s) = Term.dest_abs (x, T, t) |
1404 val (y, s) = Term.dest_abs (x, T, t) |
1414 val (_, s') = Term.dest_abs (x', T', t') |
1405 val (_, s') = Term.dest_abs (x', T', t') |
1415 val yvar = Free (y, T) |
1406 val yvar = Free (y, T) |
1416 val res = lambda yvar (inj_REPABS lthy (s, s')) |
1407 val result = lambda yvar (inj_REPABS lthy (s, s')) |
1417 in |
1408 in |
1418 if rty = qty then |
1409 if rty = qty |
1419 res |
1410 then result |
1420 else if T = T' then |
1411 else mk_repabs lthy (rty, qty) result |
1421 mk_repabs lthy (rty, qty) res |
|
1422 else mk_repabs lthy (rty, qty) (replace_bnd0 (mk_repabs lthy (T, T') (Bound 0), res)) |
|
1423 end |
1412 end |
1424 | _ => |
1413 | _ => |
|
1414 (* FIXME / TODO: this is a case that needs to be looked at *) |
|
1415 (* - variables get a rep-abs insde and outside an application *) |
|
1416 (* - constants only get a rep-abs on the outside of the application *) |
|
1417 (* - applications get a rep-abs insde and outside an application *) |
1425 let |
1418 let |
1426 val (rhead, rargs) = strip_comb rtrm |
1419 val (rhead, rargs) = strip_comb rtrm |
1427 val (qhead, qargs) = strip_comb qtrm |
1420 val (qhead, qargs) = strip_comb qtrm |
1428 (* TODO: val rhead' = inj_REPABS lthy (rhead, qhead) *) |
1421 val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs) |
1429 val rhead' = rhead; |
|
1430 val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs); |
|
1431 val result = list_comb (rhead', rargs'); |
|
1432 in |
1422 in |
1433 if rty = qty then |
1423 if rty = qty |
1434 result |
1424 then list_comb (rhead, rargs') |
1435 else if (is_lifted_const rhead qhead) then |
1425 else |
1436 mk_repabs lthy (rty, qty) result |
1426 case (rhead, qhead, length rargs') of |
1437 else if ((Term.is_Free rhead) andalso (length rargs' > 0)) then |
1427 (Const _, Const _, 0) => mk_repabs lthy (rty, qty) rhead |
1438 mk_repabs lthy (rty, qty) result |
1428 | (Free _, Free _, 0) => mk_repabs lthy (rty, qty) rhead |
1439 else if rargs' = [] then |
1429 | (Const _, Const _, _) => mk_repabs lthy (rty, qty) (list_comb (rhead, rargs')) |
1440 rhead' |
1430 | (Free (x, T), Free (x', T'), _) => |
1441 else result |
1431 mk_repabs lthy (rty, qty) (list_comb (mk_repabs lthy (T, T') rhead, rargs')) |
|
1432 | (Abs _, Abs _, _ ) => |
|
1433 mk_repabs lthy (rty, qty) (list_comb (inj_REPABS lthy (rhead, qhead), rargs')) |
|
1434 | _ => trm_lift_error lthy rtrm qtrm |
1442 end |
1435 end |
1443 end |
1436 end |
1444 *} |
1437 *} |
1445 |
1438 |
1446 ML {* |
1439 ML {* |