wneuper/isa: libisabelle-1.0.1-protocol/operations/ML

     1 theory ML_Expr

     2 imports "../protocol/Protocol"

     3 begin

     5 ML_file "ml_expr.ML"

     6 ML_file "refs.ML"

     8 operation_setup eval_expr = \<open>

     9   {from_lib = Codec.triple Codec.string ML_Expr.codec Codec.string,

    10    to_lib = Codec.tree,

    11    action = fn (typ, prog, thy_name) =>

    12     let

    13       val thy = get_theory thy_name

    14       val ctxt = Proof_Context.init_global thy

    15     in

    16       ML_Expr.eval ctxt prog typ

    17     end}\<close>

    19 operation_setup eval_opaque_expr = \<open>

    20   {from_lib = Codec.triple (Codec.triple Codec.string Codec.string ML_Expr.codec) ML_Expr.codec Codec.string,

    21    to_lib = Codec.tuple Codec.int Codec.tree,

    22    action = fn ((table, repr_typ, conv), prog, thy_name) =>

    23     let

    24       val thy = get_theory thy_name

    25       val ctxt = Proof_Context.init_global thy

    26     in

    27       ML_Expr.eval_opaque ctxt prog {table = table, repr_typ = repr_typ, conv = conv}

    28     end}\<close>

    30 operation_setup check_expr = \<open>

    31   {from_lib = Codec.triple Codec.string ML_Expr.codec Codec.string,

    32    to_lib = Codec.option Codec.string,

    33    action = fn (typ, prog, thy_name) =>

    34     let

    35       val thy = get_theory thy_name

    36       val ctxt = Proof_Context.init_global thy

    37     in

    38       ML_Expr.check ctxt prog typ

    39     end}\<close>

    41 end

author	Walther Neuper <walther.neuper@jku.at>
	Wed, 04 Sep 2019 10:17:53 +0200
changeset 59611	1aa20558eca8
permissions	-rw-r--r--