*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Behaviour of Variable.variant_fixes*From*: Lars Hupel <hupel at in.tum.de>*Date*: Mon, 17 Nov 2014 15:20:20 +0100*In-reply-to*: <53F70D6C.90907@in.tum.de>*References*: <53F70D6C.90907@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.2.0

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 > >

- Previous by Date: Re: [isabelle] Problem copying logical relation from TAPL
- Next by Date: Re: [isabelle] Problem copying logical relation from TAPL
- Previous by Thread: Re: [isabelle] Reindexing series
- Next by Thread: [isabelle] Isabelle/PIDE as IDE for Standard ML
- Cl-isabelle-users November 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list