On 27/11/10 17:12, Alexander Krauss wrote:
Hi Michael,I think you want to use setup {* ml_expression *} where ml_expression has type theory -> theory.
Thanks, Alex. Indeed, the effect I'm after is like using setup {* *}, but ultimately I'd like this effect to be produced by calling a tactic, i.e. let a tactic make updates to the current theory when invoked using 'apply (tac...)'. I'll look at the implementation of 'setup'.
Michael
Alex Michael Chan wrote:Hello, I'm trying to update the current theory at the ML-level, e.g., creating a new table in the current theory. For example, I have a function foo that does very much what Locale.register_locale does -- mainly, adding an entry into a table in the name space: ML {* val thy' = foo "x" @{theory}; Bar.get thy'; *} thy' is therefore the updated theory (containing the new table). Let Bar be structure Bar = Theory_Data (...) So Bar.get thy' returns the Name_Space-table pair, in which the table is updated. This is fine if I call "Bar.get thy'" rather than "Bar.get @{theory}" because the current theory hasn't been updated. Now, what if I want the update to be made in the current theory such that I can get the updated table using Bar.get @{theory} instead? What I have tried so far is to rebuild HOL with "datatype node = ..." and "val transaction ..." declared in signature TOPLEVEL and I transform the state using Isar.>>: ML {* val thy' = foo "x" @{theory}; val update_thy = Toplevel.transaction (fn int => (fn Toplevel.Proof (prf, (finish,_)) => Toplevel.Proof (prf, (finish, Context.Theory thy')) | Toplevel.Theory (_,c) => Toplevel.Theory (Context.Theory thy', c) )); val tr = Toplevel.name "test_tr" Toplevel.empty; update_thy tr |> Isar.>>; Bar.get @{theory}; *} Here, Bar.get @{theory} still doesn't give me the updated table. However, if I undo one step and add ML {* Bar.get @{theory} *} then do one step, I see the updated table! I must be transforming the states incorrectly -- perhaps I shouldn't use Isar.>>? Also, I have a strong feeling that I'm not supposed to rebuild HOL with those hacks in TOPLEVEL... Thanks for the help in advance. Michael_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
-- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
