175 (* possible capture *) |
175 (* possible capture *) |
176 fun replace_bnd0 (trm, Abs (x, T, t)) = |
176 fun replace_bnd0 (trm, Abs (x, T, t)) = |
177 Abs (x, T, subst_bound (trm, t)) |
177 Abs (x, T, subst_bound (trm, t)) |
178 *} |
178 *} |
179 |
179 |
|
180 |
180 ML {* |
181 ML {* |
181 (* bound variables need to be treated properly, *) |
182 (* bound variables need to be treated properly, *) |
182 (* as the type of subterms need to be calculated *) |
183 (* as the type of subterms need to be calculated *) |
|
184 |
|
185 fun is_lifted_const h gh = is_Const h andalso is_Const gh andalso not (h = gh) |
183 |
186 |
184 fun inj_REPABS lthy (rtrm, qtrm) = |
187 fun inj_REPABS lthy (rtrm, qtrm) = |
185 let |
188 let |
186 val rty = fastype_of rtrm |
189 val rty = fastype_of rtrm |
187 val qty = fastype_of qtrm |
190 val qty = fastype_of qtrm |
204 then res |
207 then res |
205 else if T = T' |
208 else if T = T' |
206 then mk_repabs lthy (rty, qty) res |
209 then mk_repabs lthy (rty, qty) res |
207 else mk_repabs lthy (rty, qty) (replace_bnd0 (mk_repabs lthy (T, T') (Bound 0), res)) |
210 else mk_repabs lthy (rty, qty) (replace_bnd0 (mk_repabs lthy (T, T') (Bound 0), res)) |
208 end |
211 end |
209 (* TODO: check what happens if head is a constant *) |
212 | _ => |
210 | (_ $ _, _ $ _) => |
|
211 let |
213 let |
212 val (rhead, rargs) = strip_comb rtrm |
214 val (rhead, rargs) = strip_comb rtrm |
213 val (qhead, qargs) = strip_comb qtrm |
215 val (qhead, qargs) = strip_comb qtrm |
214 val rhead' = inj_REPABS lthy (rhead, qhead) |
216 (* TODO: val rhead' = inj_REPABS lthy (rhead, qhead) *) |
215 val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs) |
217 val rhead' = rhead; |
216 val result = list_comb (rhead', rargs') |
218 val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs); |
|
219 val result = list_comb (rhead', rargs'); |
217 in |
220 in |
218 if rty = qty |
221 if rty = qty then result else |
219 then result |
222 if (is_lifted_const rhead qhead) then mk_repabs lthy (rty, qty) result else |
220 else mk_repabs lthy (rty, qty) result |
223 if ((Term.is_Free rhead) andalso (length rargs' > 0)) then mk_repabs lthy (rty, qty) result else |
|
224 if rargs' = [] then rhead' else result |
221 end |
225 end |
222 (* TODO: maybe leave result without mk_repabs when head is a constant *) |
|
223 (* TODO: that we do not know how to lift *) |
|
224 | (Const (s, T), Const (s', T')) => |
|
225 if T = T' |
|
226 then rtrm |
|
227 else mk_repabs lthy (T, T') rtrm |
|
228 | _ => rtrm |
|
229 end |
226 end |
230 *} |
227 *} |
231 |
228 |
232 ML {* |
229 ML {* |
233 fun mk_inj_REPABS_goal lthy (rtrm, qtrm) = |
230 fun mk_inj_REPABS_goal lthy (rtrm, qtrm) = |