396 val rel_ty = (fastype_of rel) handle TERM _ => raise exc |
396 val rel_ty = (fastype_of rel) handle TERM _ => raise exc |
397 val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') |
397 val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') |
398 in |
398 in |
399 if rel' = rel then rtrm else raise exc |
399 if rel' = rel then rtrm else raise exc |
400 end |
400 end |
401 | (_, Const (s, _)) => |
401 | (_, Const (s, Type(st, _))) => |
402 let |
402 let |
403 fun same_name (Const (s, _)) (Const (s', _)) = (s = s') |
403 fun same_name (Const (s, _)) (Const (s', _)) = (s = s') |
404 | same_name _ _ = false |
404 | same_name _ _ = false |
405 in |
405 in |
406 if same_name rtrm qtrm |
406 (* TODO/FIXME: This test is not enough *) |
407 then rtrm |
407 if same_name rtrm qtrm then rtrm |
408 else |
408 else |
409 let |
409 let |
410 fun exc1 s = LIFT_MATCH ("regularize (constant " ^ s ^ " not found)") |
410 val exc1 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") not found)") |
411 val exc2 = LIFT_MATCH ("regularize (constant mismatch)") |
411 val exc2 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") mismatch)") |
412 val thy = ProofContext.theory_of lthy |
412 val thy = ProofContext.theory_of lthy |
413 val rtrm' = (#rconst (qconsts_lookup thy s)) handle NotFound => raise (exc1 s) |
413 val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1 |
414 in |
414 in |
415 if matches_term (rtrm, rtrm') then rtrm else raise exc2 |
415 if matches_term (rtrm, rtrm') then rtrm else |
|
416 let |
|
417 val _ = tracing (Syntax.string_of_term @{context} rtrm); |
|
418 val _ = tracing (Syntax.string_of_term @{context} rtrm'); |
|
419 in raise exc2 end |
416 end |
420 end |
417 end |
421 end |
418 |
422 |
419 | (t1 $ t2, t1' $ t2') => |
423 | (t1 $ t2, t1' $ t2') => |
420 (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2') |
424 (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2') |
614 else mk_repabs lthy (T, T') rtrm |
618 else mk_repabs lthy (T, T') rtrm |
615 |
619 |
616 | (_, Const (@{const_name "op ="}, _)) => rtrm |
620 | (_, Const (@{const_name "op ="}, _)) => rtrm |
617 |
621 |
618 (* FIXME: check here that rtrm is the corresponding definition for the const *) |
622 (* FIXME: check here that rtrm is the corresponding definition for the const *) |
|
623 (* Hasn't it already been checked in regularize? *) |
619 | (_, Const (_, T')) => |
624 | (_, Const (_, T')) => |
620 let |
625 let |
621 val rty = fastype_of rtrm |
626 val rty = fastype_of rtrm |
622 in |
627 in |
623 if rty = T' then rtrm |
628 if rty = T' then rtrm |