[isabelle] Behaviour of Variable.variant_fixes



Dear list,

consider this snippet:

ML{*
  val constr = (((Binding.empty, @{binding Constr}), []), NoSyn)
  val datatyp = (([], @{binding test}), NoSyn)

  val lthy = Named_Target.init "" @{theory}

  val (x, lthy) = Variable.variant_fixes ["x"] lthy

  val lthy =
    BNF_FP_Def_Sugar.co_datatypes
      BNF_Util.Least_FP BNF_LFP.construct_lfp
      ((false, false), [(((datatyp, [constr]), (Binding.empty,
Binding.empty)), [])]) lthy

  val (x', lthy) = Variable.variant_fixes ["x"] lthy
*}

The results for x and x' are somewhat unexpected to me:

  val x = ["x"]: string list
  val x' = ["x"]: string list

I expected them to be different. Indeed, they are different when I move
the BNF definition to the front, before the calls to `variant_fixes`.

In my use case, I'm translating between a foreign AST and Isabelle's
term language. This AST contains type and value definitions, but the
respective translations do not depend on each other, so they can be done
in parallel (this is an actual parallelized algorithm -- the definitions
are presented to the Isabelle system in some unordered way).

I can't even declare my newly-fixed variables immediately inside the
context, because I don't know their types in advance. (I tried doing
that in my above example nonetheless by inserting the line

  val lthy = Variable.declare_term (Free (x, @{typ int})) lthy

after the first `variant_fixes`, but that didn't change the outcome at all.)

Do I need to sequentialize my algorithm?

Cheers
Lars




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.