Stream: Isabelle/ML

Topic: ✔ Construct type application with unification


view this post on Zulip Jan van Brügge (Sep 15 2021 at 12:36):

What is the proper way to construct a type application with ML that requires unification? If I just use the $ constructor I get an expected unification error:

Operator:  card_suc :: (?'a × ?'a) set  (?'a suc × ?'a suc) set
Operand:   natLeq :: (nat × nat) set

view this post on Zulip Lukas Stevens (Sep 15 2021 at 13:01):

https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/Construct.20term.20while.20instantiating.20schematic.20type.20variables

view this post on Zulip Jan van Brügge (Sep 15 2021 at 13:13):

Thanks,

Syntax.check_term ctxt (Const ("Prelim.card_suc", dummyT) $ BNF_Def.bd_of_bnf bnf))

does indeed correctly unify the free variables

view this post on Zulip Notification Bot (Sep 15 2021 at 13:13):

Jan van Brügge has marked this topic as resolved.

view this post on Zulip Dmitriy Traytel (Sep 15 2021 at 13:20):

You picked the last answer from the thread that Lukas linked. However, there was an earlier answer (starting with 'if "term" is something whose type you know ...') that suits your situation better. In fact, Syntax.check_term does a lot of things and moreover is extensible (so it could do even more things when your code is run in a different context), which makes it something one should avoid using in a definitional package whenever possible.

view this post on Zulip Jan van Brügge (Sep 15 2021 at 13:23):

The problem is the result type, it is not obvious to me how I would construct that from the type of natLeq as input, or better said: Depending on what relation type I get as input

view this post on Zulip Dmitriy Traytel (Sep 15 2021 at 13:27):

Have a look at the various mk_... functions in ~~/src/HOL/Tools/BNF/bnf_util.ML for terms and types.

view this post on Zulip Dmitriy Traytel (Sep 15 2021 at 13:29):

Actually, there is even a mk_cardSuc in ~~/src/HOL/Tools/BNF/bnf_lfp_util.ML, which should be very similar to what you need.

view this post on Zulip Jan van Brügge (Sep 15 2021 at 13:40):

got that to work too:

fun mk_sucT T = Type (\<^type_name>‹suc›, [T])
fun mk_card_suc r =
  let val T = fst (BNF_Util.dest_relT (fastype_of r));
  in Const (\<^const_name>‹card_suc›, BNF_Util.mk_relT (T, T) --> BNF_Util.mk_relT (mk_sucT T, mk_sucT T)) $ r end;

Last updated: Feb 27 2024 at 08:17 UTC