Stream: General

Topic: Construct term while instantiating schematic type variables

Lukas Stevens (Aug 04 2020 at 14:46):

I have this situation:

val term = ...
val app_term = term $ t1 $ t2

term contains schematic type variables. Is there a function that constructs app_term with instantiated schematic type variables?

Lukas Stevens (Aug 04 2020 at 14:50):

The instantiation should use the types of t1 and t2 accordingly.

Manuel Eberl (Aug 04 2020 at 14:58):

Hmm, I think maybe you want type inference. Don't know all that much about it though to be honest. Maybe search for "schematic" in the Isabelle cookbook.

Manuel Eberl (Aug 04 2020 at 14:58):

(inb4 have fun with flex-flex pairs :D)

Lukas Stevens (Aug 04 2020 at 15:04):

there should'nt be any flex-flex pairs since there is only one schematic type variable that only occurs in term :fingers_crossed:

Manuel Eberl (Aug 04 2020 at 15:07):

if "term" is something whose type you know, I would just compute the type

Manuel Eberl (Aug 04 2020 at 15:08):

e.g. if "term" where addition, you should write an ML function mk_add : typ -> term that does something like mk_add T = Const (@{const_name "Groups.add"}, T --> T --> T).

Manuel Eberl (Aug 04 2020 at 15:08):

That's the way it's done in the library.

Manuel Eberl (Aug 04 2020 at 15:08):

I'd only use actual type inference with schematic variables and whatever if you absolutely have to

Manuel Eberl (Aug 04 2020 at 15:09):

Depends a bit where this "term" thing comes from, I guess.

Lukas Stevens (Aug 04 2020 at 15:09):

Ok, I'll try to do it without type inference, thanks for the hint.

Manuel Eberl (Aug 04 2020 at 15:11):

one common pattern is also to specify the type of the function as dummyT and then do a Syntax.check_term to let type inference fill in the type

Manuel Eberl (Aug 04 2020 at 15:12):

that doesn't seem to work in the presence of schematic variables though and I never really understood why

Manuel Eberl (Aug 04 2020 at 15:12):

I think you have to tag them somehow to tell type inference that it is allowed to fill them in

Lukas Stevens (Aug 04 2020 at 15:50):

Manuel Eberl said:

one common pattern is also to specify the type of the function as dummyT and then do a Syntax.check_term to let type inference fill in the type

Cool, I am using that now.

Last updated: Dec 21 2024 at 12:33 UTC