Stream: Isabelle/ML

Topic: safely doing a evaluation of ml evaluation

irvin (Nov 28 2024 at 07:21):

I kinda want to do an evaluation of some stuff without keeping name bindings only keeping context data similar to how it works in ml_prf

context notes [[ML_environment="Isabelle"]] begin
ML‹val a = "1"›
notepad
begin
  ML_prf‹
val a = "2"

›

end
ML‹val _ = @{print} a› ―‹"1"›

right now its using code that does

ML ‹fun with_temp_ML_env f x =
  let
    val context = Context.the_generic_context()
    val res = f x
    val () = Context.>> (ML_Env.inherit [context])
  in res end
›

which messes up synchronized variables

irvin (Nov 28 2024 at 13:34):

irvin said:

I kinda want to do an evaluation of some stuff without keeping name bindings only keeping context data similar to how it works in ml_prf

context notes [[ML_environment="Isabelle"]] begin
ML‹val a = "1"›
notepad
begin
  ML_prf‹
val a = "2"

›

end
ML‹val _ = @{print} a› ―‹"1"›

right now its using code that does

ML ‹fun with_temp_ML_env f x =
  let
    val context = Context.the_generic_context()
    val res = f x
    val () = Context.>> (ML_Env.inherit [context])
  in res end
›

which messes up synchronized variables

Oh I found out that the code kinda is just kinda of doing where Data is the ML_env and somehow the values for synchronized variables are stored in nonce is rolled back.

ML ‹fun with_temp_ML_env f x =
  let
    val context = Context.the_generic_context()
    val res = f x
    val () = Context.>> (Data.put (Data.get [context]))
  in res end
›

irvin (Nov 30 2024 at 09:53):

theory Scratch
  imports Main
begin

ML‹val a = Synchronized.var "test" "hi"›
ML‹    val context = Context.the_generic_context()›

ML‹
val _ = Synchronized.assign a "oops"



›
ML‹    val _ = Context.>> (ML_Env.inherit [context])›

ML‹Synchronized.value a›
end

(Oh this is my issue more simply explained)
(*Im not sure how is one meant to do this properly *)

Last updated: Dec 21 2024 at 16:20 UTC