Re: [isabelle] Behaviour of Variable.variant_fixes



Reviving this old thread, because Dmitriy and Ondrej were asking me
about the workaround I found, so I figured I should post it publicly.

Anyway, it turns out that if the definition of a datatype is carried out
in a local theory created using Local_Theory.init, the variable names
are preserved.

ML{*
  fun init ctxt = ctxt
    |> Local_Theory.init (Sign.naming_of @{theory})
       {define = Generic_Target.define Generic_Target.theory_foundation,
        notes = Generic_Target.notes Generic_Target.theory_notes,
        abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
        declaration = K Generic_Target.theory_declaration,
        subscription = Generic_Target.theory_registration,
        pretty = K [],
        exit = Local_Theory.target_of #> Sign.change_end_local}

  val ctxt = @{theory}
    |> Sign.change_begin
    |> Proof_Context.init_global

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

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

  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 ctxt = Local_Theory.exit lthy

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

The only difference to the previous code is that all other operations
apart from datatype definition happens in a regular proof context, not
in a local theory, and that a local theory is created and exited on the
spot when a datatype is to be defined.



On 22.08.2014 11:29, Lars Hupel wrote:
> 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.