1383 ML {* |
1383 ML {* |
1384 (* replaces a term for the bound variable, *) |
1384 (* replaces a term for the bound variable, *) |
1385 (* possible capture *) |
1385 (* possible capture *) |
1386 fun replace_bnd0 (trm, Abs (x, T, t)) = |
1386 fun replace_bnd0 (trm, Abs (x, T, t)) = |
1387 Abs (x, T, subst_bound (trm, 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) |
1388 *} |
1392 *} |
1389 |
1393 |
1390 |
1394 |
1391 ML {* |
1395 ML {* |
1392 (* bound variables need to be treated properly, *) |
1396 (* bound variables need to be treated properly, *) |
1393 (* as the type of subterms need to be calculated *) |
1397 (* as the type of subterms need to be calculated *) |
1394 |
|
1395 fun is_lifted_const h gh = is_Const h andalso is_Const gh andalso not (h = gh) |
|
1396 |
1398 |
1397 fun inj_REPABS lthy (rtrm, qtrm) = |
1399 fun inj_REPABS lthy (rtrm, qtrm) = |
1398 let |
1400 let |
1399 val rty = fastype_of rtrm |
1401 val rty = fastype_of rtrm |
1400 val qty = fastype_of qtrm |
1402 val qty = fastype_of qtrm |
1411 val (y, s) = Term.dest_abs (x, T, t) |
1413 val (y, s) = Term.dest_abs (x, T, t) |
1412 val (_, s') = Term.dest_abs (x', T', t') |
1414 val (_, s') = Term.dest_abs (x', T', t') |
1413 val yvar = Free (y, T) |
1415 val yvar = Free (y, T) |
1414 val res = lambda yvar (inj_REPABS lthy (s, s')) |
1416 val res = lambda yvar (inj_REPABS lthy (s, s')) |
1415 in |
1417 in |
1416 if rty = qty |
1418 if rty = qty then |
1417 then res |
1419 res |
1418 else if T = T' |
1420 else if T = T' then |
1419 then mk_repabs lthy (rty, qty) res |
1421 mk_repabs lthy (rty, qty) res |
1420 else mk_repabs lthy (rty, qty) (replace_bnd0 (mk_repabs lthy (T, T') (Bound 0), res)) |
1422 else mk_repabs lthy (rty, qty) (replace_bnd0 (mk_repabs lthy (T, T') (Bound 0), res)) |
1421 end |
1423 end |
1422 | _ => |
1424 | _ => |
1423 let |
1425 let |
1424 val (rhead, rargs) = strip_comb rtrm |
1426 val (rhead, rargs) = strip_comb rtrm |
1425 val (qhead, qargs) = strip_comb qtrm |
1427 val (qhead, qargs) = strip_comb qtrm |
1426 (* TODO: val rhead' = inj_REPABS lthy (rhead, qhead) *) |
1428 (* TODO: val rhead' = inj_REPABS lthy (rhead, qhead) *) |
1427 val rhead' = rhead; |
1429 val rhead' = rhead; |
1428 val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs); |
1430 val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs); |
1429 val result = list_comb (rhead', rargs'); |
1431 val result = list_comb (rhead', rargs'); |
1430 in |
1432 in |
1431 if rty = qty then result else |
1433 if rty = qty then |
1432 if (is_lifted_const rhead qhead) then mk_repabs lthy (rty, qty) result else |
1434 result |
1433 if ((Term.is_Free rhead) andalso (length rargs' > 0)) then mk_repabs lthy (rty, qty) result else |
1435 else if (is_lifted_const rhead qhead) then |
1434 if rargs' = [] then rhead' else result |
1436 mk_repabs lthy (rty, qty) result |
|
1437 else if ((Term.is_Free rhead) andalso (length rargs' > 0)) then |
|
1438 mk_repabs lthy (rty, qty) result |
|
1439 else if rargs' = [] then |
|
1440 rhead' |
|
1441 else result |
1435 end |
1442 end |
1436 end |
1443 end |
1437 *} |
1444 *} |
1438 |
1445 |
1439 ML {* |
1446 ML {* |