Hi Makarius,
thanks, this is the hint I was looking for a long time now.
I will do the replacement in the BNF package, but I don't think that I
will have time for it before the approaching release.
Dmitriy
On 07.04.2015 17:47, Makarius wrote:
Just a short note on Local_Theory.open_target (for Isabelle/83071f4c8ae6)
versus old uses of Local_Theory.restore.
Local_Theory.open_target is the internal version of "context begin",
where Local_Theory.close_target is "end". The ML signature is now a
bit more concise form than before. It has already been used
successfully in Eisbach, to lay out a local situation for the internal
construction.
Here is a quick example that shows how to get polymorphic constants
out of local theory specifications, with such official context nesting:
context fixes x :: 'a
begin
declare [[show_types]]
ML_val ‹
val lthy = @{context};
val (_, lthy1) = lthy |> Local_Theory.open_target;
val ((t, (_, th)), lthy2) = lthy1
|> Local_Theory.define ((@{binding c}, NoSyn),
(Attrib.empty_binding, @{term "λy. x"}));
val lthy3 = lthy2 |> Local_Theory.close_target;
val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of
lthy3);
val th' = th |> singleton (Proof_Context.export lthy2 lthy3);
val th'' = th' |> singleton (Proof_Context.export lthy3 thy_ctxt);
writeln (Display.string_of_thm lthy2 th); (*monomorphic*)
writeln (Display.string_of_thm lthy3 th'); (*partly polymorphic*)
writeln (Display.string_of_thm thy_ctxt th''); (*fully polymorphic*)
›
Thus the brute-force Local_Theory.restore is avoided, which only works
properly at the boundary of local theory command transactions anyway.
Eliminating Local_Theory.restore is one of these continuous reform
projects that can be done now or later. Note that it would also
achieve better results for "private datatype", because
Local_Theory.restore disrupts the continuity of the naming policy.
It is up to the BNF guys to say if they intend to do something for the
Isabelle2015 release, or just leave the status quo. It is unlikely
that anybody will notice fine points of private datatype definitions
before the next release after Isabelle2015.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
