Email Gateway (Aug 19 2022 at 15:32): Email Gateway (Aug 19 2022 at 15:32):From: Lars Hupel <hupel@in.tum.de>
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
Email Gateway (Aug 19 2022 at 15:34):From: Lars Hupel <hupel@in.tum.de>
One more thing: this doesn't happen for other kinds of operations, e.g.
Function.add_function. Executing
val fun_config = Function_Common.FunctionConfig
{sequential=true, default=NONE, domintros=false, partials=false}
fun pat_completeness_auto ctxt =
Pat_Completeness.pat_completeness_tac ctxt 1 THEN auto_tac ctxt
val (_, lthy) = Function.add_function
[(@{binding foo}, NONE, NoSyn)]
([(Attrib.empty_binding, @{term "Trueprop (foo (Suc r) = r)"})])
fun_config pat_completeness_auto lthy
between two calls of variant_fixes doesn't exhibit this behaviour
(i.e. fixed variables are preserved). That makes me wonder whether it is
some oddity in BNF, or for type definitions in general.
Email Gateway (Aug 19 2022 at 16:40):From: Lars Hupel <hupel@in.tum.de>
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.
Last updated: Apr 26 2024 at 20:16 UTC