1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/libisabelle-1.0.1-protocol/operations/ML_Expr.thy	Wed Sep 04 10:17:53 2019 +0200
     1.3 @@ -0,0 +1,41 @@
     1.4 +theory ML_Expr
     1.5 +imports "../protocol/Protocol"
     1.6 +begin
     1.7 +
     1.8 +ML_file "ml_expr.ML"
     1.9 +ML_file "refs.ML"
    1.10 +
    1.11 +operation_setup eval_expr = \<open>
    1.12 +  {from_lib = Codec.triple Codec.string ML_Expr.codec Codec.string,
    1.13 +   to_lib = Codec.tree,
    1.14 +   action = fn (typ, prog, thy_name) =>
    1.15 +    let
    1.16 +      val thy = get_theory thy_name
    1.17 +      val ctxt = Proof_Context.init_global thy
    1.18 +    in
    1.19 +      ML_Expr.eval ctxt prog typ
    1.20 +    end}\<close>
    1.21 +
    1.22 +operation_setup eval_opaque_expr = \<open>
    1.23 +  {from_lib = Codec.triple (Codec.triple Codec.string Codec.string ML_Expr.codec) ML_Expr.codec Codec.string,
    1.24 +   to_lib = Codec.tuple Codec.int Codec.tree,
    1.25 +   action = fn ((table, repr_typ, conv), prog, thy_name) =>
    1.26 +    let
    1.27 +      val thy = get_theory thy_name
    1.28 +      val ctxt = Proof_Context.init_global thy
    1.29 +    in
    1.30 +      ML_Expr.eval_opaque ctxt prog {table = table, repr_typ = repr_typ, conv = conv}
    1.31 +    end}\<close>
    1.32 +
    1.33 +operation_setup check_expr = \<open>
    1.34 +  {from_lib = Codec.triple Codec.string ML_Expr.codec Codec.string,
    1.35 +   to_lib = Codec.option Codec.string,
    1.36 +   action = fn (typ, prog, thy_name) =>
    1.37 +    let
    1.38 +      val thy = get_theory thy_name
    1.39 +      val ctxt = Proof_Context.init_global thy
    1.40 +    in
    1.41 +      ML_Expr.check ctxt prog typ
    1.42 +    end}\<close>
    1.43 +
    1.44 +end