[isabelle-dev] Updating the current theory

[Alexander Krauss]

Hi Michael,

I think you want to use

setup {*
   ml_expression
*}

where ml_expression has type theory -> theory.

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
>