# HG changeset patch # User Walther Neuper # Date 1567585073 -7200 # Node ID 1aa20558eca8bd1dd56bcd82dad027b6f3068960 # Parent 62ff42cd45c713a0921176d4cec67c20591a8d08 Isabelle2018->19: cp libisabelle into Isac, partially diff -r 62ff42cd45c7 -r 1aa20558eca8 ROOTS --- a/ROOTS Tue Sep 03 17:43:42 2019 +0200 +++ b/ROOTS Wed Sep 04 10:17:53 2019 +0200 @@ -10,6 +10,6 @@ src/Sequents src/Doc src/Tools -#src/Tools/isac -#libisabelle-protocol +src/Tools/isac +libisabelle-1.0.1-protocol test/Tools/isac/ADDTESTS/session-get_theory/ \ No newline at end of file diff -r 62ff42cd45c7 -r 1aa20558eca8 libisabelle-1.0.1-protocol/Protocol_Main.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/libisabelle-1.0.1-protocol/Protocol_Main.thy Wed Sep 04 10:17:53 2019 +0200 @@ -0,0 +1,9 @@ +theory Protocol_Main +imports + Main + "operations/HOL_Operations" + Protocol.Basic + Protocol.ML_Expr +begin + +end \ No newline at end of file diff -r 62ff42cd45c7 -r 1aa20558eca8 libisabelle-1.0.1-protocol/Protocol_Pure.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/libisabelle-1.0.1-protocol/Protocol_Pure.thy Wed Sep 04 10:17:53 2019 +0200 @@ -0,0 +1,8 @@ +theory Protocol_Pure +imports + Pure + "operations/Basic" + "operations/ML_Expr" +begin + +end \ No newline at end of file diff -r 62ff42cd45c7 -r 1aa20558eca8 libisabelle-1.0.1-protocol/ROOT --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/libisabelle-1.0.1-protocol/ROOT Wed Sep 04 10:17:53 2019 +0200 @@ -0,0 +1,13 @@ +session Protocol = Classy + + theories + "protocol/Protocol" + "protocol/Codec_Test" + "Protocol_Pure" + +session "HOL-Protocol" = "HOL-Classy" + + sessions + Protocol + theories + Protocol.Protocol + Protocol.Codec_Test + "Protocol_Main" diff -r 62ff42cd45c7 -r 1aa20558eca8 libisabelle-1.0.1-protocol/operations/Basic.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/libisabelle-1.0.1-protocol/operations/Basic.thy Wed Sep 04 10:17:53 2019 +0200 @@ -0,0 +1,11 @@ +theory Basic +imports "../protocol/Protocol" +begin + +operation_setup (auto) ping = \fn () => ()\ + +operation_setup (auto) hello = \fn data => "Hello " ^ data\ + +operation_setup (sequential, bracket, auto) use_thys = \List.app Thy_Info.use_thy\ + +end diff -r 62ff42cd45c7 -r 1aa20558eca8 libisabelle-1.0.1-protocol/operations/HOL_Operations.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/libisabelle-1.0.1-protocol/operations/HOL_Operations.thy Wed Sep 04 10:17:53 2019 +0200 @@ -0,0 +1,24 @@ +theory HOL_Operations +imports Main Protocol.Protocol +begin + +operation_setup mk_int = \ + {from_lib = Codec.int, + to_lib = Codec.term, + action = HOLogic.mk_number @{typ int}}\ + +operation_setup dest_int = \ + {from_lib = Codec.term, + to_lib = Codec.option Codec.int, + action = fn t => case try HOLogic.dest_number t of + NONE => NONE + | SOME (typ, n) => + if typ = @{typ int} then + SOME n + else + NONE}\ + +operation_setup (auto) mk_list = \uncurry HOLogic.mk_list\ +operation_setup (auto) dest_list = \try HOLogic.dest_list\ + +end diff -r 62ff42cd45c7 -r 1aa20558eca8 libisabelle-1.0.1-protocol/operations/ML_Expr.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/libisabelle-1.0.1-protocol/operations/ML_Expr.thy Wed Sep 04 10:17:53 2019 +0200 @@ -0,0 +1,41 @@ +theory ML_Expr +imports "../protocol/Protocol" +begin + +ML_file "ml_expr.ML" +ML_file "refs.ML" + +operation_setup eval_expr = \ + {from_lib = Codec.triple Codec.string ML_Expr.codec Codec.string, + to_lib = Codec.tree, + action = fn (typ, prog, thy_name) => + let + val thy = get_theory thy_name + val ctxt = Proof_Context.init_global thy + in + ML_Expr.eval ctxt prog typ + end}\ + +operation_setup eval_opaque_expr = \ + {from_lib = Codec.triple (Codec.triple Codec.string Codec.string ML_Expr.codec) ML_Expr.codec Codec.string, + to_lib = Codec.tuple Codec.int Codec.tree, + action = fn ((table, repr_typ, conv), prog, thy_name) => + let + val thy = get_theory thy_name + val ctxt = Proof_Context.init_global thy + in + ML_Expr.eval_opaque ctxt prog {table = table, repr_typ = repr_typ, conv = conv} + end}\ + +operation_setup check_expr = \ + {from_lib = Codec.triple Codec.string ML_Expr.codec Codec.string, + to_lib = Codec.option Codec.string, + action = fn (typ, prog, thy_name) => + let + val thy = get_theory thy_name + val ctxt = Proof_Context.init_global thy + in + ML_Expr.check ctxt prog typ + end}\ + +end diff -r 62ff42cd45c7 -r 1aa20558eca8 libisabelle-1.0.1-protocol/operations/ml_expr.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/libisabelle-1.0.1-protocol/operations/ml_expr.ML Wed Sep 04 10:17:53 2019 +0200 @@ -0,0 +1,132 @@ +signature ML_EXPR = sig + datatype ml_expr = + Lit of string + | App of ml_expr * ml_expr + | Val of string * XML.tree + + val print_ml_expr: Proof.context -> ml_expr -> string + val eval: Proof.context -> ml_expr -> string -> XML.tree + val eval_opaque: Proof.context -> ml_expr -> {table: string, repr_typ: string, conv: ml_expr} -> serial * XML.tree + val check: Proof.context -> ml_expr -> string -> string option + + val print_tree: XML.tree -> string + val print_body: XML.body -> string + + (* internal *) + val codec: ml_expr codec + structure Eval : TYPED_EVAL +end + +structure ML_Expr : ML_EXPR = struct + +structure Eval = Typed_Eval +( + type T = XML.tree + val typ = "XML.tree" + val name = "ML_Expr.Eval" +) + +fun print_tree (XML.Elem elem) = + let + val str = + ML_Syntax.print_pair + (ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_properties) + print_body + elem + in "(XML.Elem " ^ str ^ ")" end + | print_tree (XML.Text text) = + "(XML.Text " ^ ML_Syntax.print_string text ^ ")" +and print_body body = + ML_Syntax.print_list print_tree body + +datatype ml_expr = + Lit of string + | App of ml_expr * ml_expr + | Val of string * XML.tree + +fun print_ml_expr _ (Lit text) = + text + | print_ml_expr ctxt (App (f, x)) = + "(" ^ print_ml_expr ctxt f ^ ") (" ^ print_ml_expr ctxt x ^ ")" + | print_ml_expr ctxt (Val (typ, value)) = + let + val codec = Classy.resolve @{ML.class codec} (ML_Types.read_ml_type typ) (Context.Proof ctxt) + in "(Codec.the_decode " ^ codec ^ " " ^ print_tree value ^ ")" end + +fun check ctxt prog raw_typ = + case try ML_Types.read_ml_type raw_typ of + NONE => SOME ("failed to parse result type " ^ raw_typ) + | SOME typ => + let + val context = Context.Proof ctxt + val codec = can (Classy.resolve @{ML.class codec} typ) context + + fun check_vals (Lit _) = NONE + | check_vals (App (f, x)) = merge_options (check_vals f, check_vals x) + | check_vals (Val (raw_typ, _)) = + case try ML_Types.read_ml_type raw_typ of + NONE => SOME ("failed to parse value type " ^ raw_typ) + | SOME _ => + if can (Classy.resolve @{ML.class codec} typ) context then + NONE + else + SOME ("could not resolve codec for value type " ^ raw_typ) + in + if not codec then + SOME ("could not resolve codec for result type " ^ raw_typ) + else + case check_vals prog of + SOME err => SOME err + | NONE => + case Exn.capture (ML_Types.ml_type_of ctxt) (print_ml_expr ctxt prog) of + Exn.Res typ' => + if typ = typ' then + NONE + else + SOME ("expected result type " ^ raw_typ ^ " but got something else") + | Exn.Exn exn => + SOME ("compilation error: " ^ @{make_string} exn) + end + +fun eval ctxt prog typ = + let + val codec = Classy.resolve @{ML.class codec} (ML_Types.read_ml_type typ) (Context.Proof ctxt) + val prog = "(Codec.encode " ^ codec ^ " (" ^ print_ml_expr ctxt prog ^ "))" + in + Eval.eval (Input.string prog) ctxt + end + +fun eval_opaque ctxt prog {table, repr_typ, conv} = + let + val codec = Classy.resolve @{ML.class codec} (ML_Types.read_ml_type repr_typ) (Context.Proof ctxt) + val id = serial () + val var = "eval_opaque_result" + val inner_prog = "(" ^ print_ml_expr ctxt prog ^ ")" + val store_prog = table ^ ".write " ^ ML_Syntax.print_int id ^ " " ^ var + val res_prog = "Codec.encode " ^ codec ^ " ((" ^ print_ml_expr ctxt conv ^ ") " ^ var ^ ")" + val prog = + "(let " ^ + "val " ^ var ^ " = " ^ inner_prog ^ + " in " ^ + "(" ^ store_prog ^ " ; " ^ res_prog ^ ") " ^ + "end)" + in + (id, Eval.eval (Input.string prog) ctxt) + end + +fun codec () = + let + val ml_expr_lit = Codec.string + fun ml_expr_app () = Codec.tuple (codec ()) (codec ()) + val ml_expr_val = Codec.tuple Codec.string Codec.tree + + fun enc _ = error "impossible" + fun dec 0 = SOME (Codec.decode ml_expr_lit #> Codec.map_result Lit) + | dec 1 = SOME (Codec.decode (ml_expr_app ()) #> Codec.map_result App) + | dec 2 = SOME (Codec.decode ml_expr_val #> Codec.map_result Val) + | dec _ = NONE + in Codec.variant enc dec "ML_Expr.ml_expr" end + +val codec = codec () + +end diff -r 62ff42cd45c7 -r 1aa20558eca8 libisabelle-1.0.1-protocol/operations/refs.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/libisabelle-1.0.1-protocol/operations/refs.ML Wed Sep 04 10:17:53 2019 +0200 @@ -0,0 +1,7 @@ +structure Refs = struct + structure Thy = Ref_Table(type t = theory; val name = "Refs.Thy") + structure Ctxt = Ref_Table(type t = Proof.context; val name = "Refs.Ctxt") + structure State = Ref_Table(type t = Proof.state; val name = "Refs.State") + structure Thm = Ref_Table(type t = thm; val name = "Refs.Thm") + structure Cterm = Ref_Table(type t = cterm; val name = "Refs.Cterm") +end \ No newline at end of file diff -r 62ff42cd45c7 -r 1aa20558eca8 libisabelle-1.0.1-protocol/protocol/Codec_Class.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/libisabelle-1.0.1-protocol/protocol/Codec_Class.thy Wed Sep 04 10:17:53 2019 +0200 @@ -0,0 +1,21 @@ +theory Codec_Class +imports Common "Classy.Classy" +begin + +ML.class codec = \'a codec\ + +ML.instance \Codec.unit\ :: codec +ML.instance \Codec.bool\ :: codec +ML.instance \Codec.string\ :: codec +ML.instance \Codec.int\ :: codec +ML.instance \Codec.list\ :: codec +ML.instance \Codec.tuple\ :: codec +ML.instance \Codec.option\ :: codec +ML.instance \Codec.either\ :: codec +ML.instance \Codec.triple\ :: codec +ML.instance \Codec.sort\ :: codec +ML.instance \Codec.typ\ :: codec +ML.instance \Codec.term\ :: codec +ML.instance \Codec.tree\ :: codec + +end diff -r 62ff42cd45c7 -r 1aa20558eca8 libisabelle-1.0.1-protocol/protocol/Codec_Test.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/libisabelle-1.0.1-protocol/protocol/Codec_Test.thy Wed Sep 04 10:17:53 2019 +0200 @@ -0,0 +1,41 @@ +theory Codec_Test +imports Common "~~/src/Tools/Spec_Check/Spec_Check" +begin + +ML\ +fun check_for str = + let + val prop1 = + "ALL x. (let val c = (" ^ str ^ ") in Codec.decode c (Codec.encode c x) = Codec.Success x end)" + val prop2 = + "ALL x. (let val c = (" ^ str ^ ") in Codec.decode c (YXML.parse (YXML.string_of (Codec.encode c x))) = Codec.Success x end)" + in + check_property prop1; + check_property prop2 + end + +fun gen_unit r = + ((), r) +\ + +ML_command\ + check_for "Codec.unit"; + check_for "Codec.int"; + check_for "Codec.bool"; + check_for "Codec.string"; + check_for "Codec.tuple Codec.int Codec.int"; + check_for "Codec.tuple Codec.string Codec.unit"; + check_for "Codec.list Codec.unit"; + check_for "Codec.list Codec.int"; + check_for "Codec.list Codec.string"; + check_for "Codec.list (Codec.list Codec.string)"; + check_for "Codec.list (Codec.tuple Codec.int Codec.int)"; + check_for "Codec.tuple Codec.int (Codec.list Codec.int)"; + check_for "Codec.option Codec.int"; + check_for "Codec.option (Codec.list Codec.int)"; + check_for "Codec.list (Codec.option (Codec.int))"; + check_for "Codec.term"; + check_for "Codec.typ"; +\ + +end diff -r 62ff42cd45c7 -r 1aa20558eca8 libisabelle-1.0.1-protocol/protocol/Common.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/libisabelle-1.0.1-protocol/protocol/Common.thy Wed Sep 04 10:17:53 2019 +0200 @@ -0,0 +1,80 @@ +theory Common +imports Pure +begin + +ML\ + val print_int = Value.print_int + val parse_int = Value.parse_int + val print_bool = Value.print_bool + val parse_bool = Value.parse_bool + fun get_theory name = + let + val all = Thy_Info.get_names () + val qualified = find_first (fn name' => name = Long_Name.base_name name') all + in Thy_Info.get_theory (the qualified) end +\ + +ML\ +local + (* code copied and adapted from Isabelle/Pure *) + + fun encode "<" = "<" + | encode ">" = ">" + | encode "&" = "&" + | encode "'" = "'" + | encode "\"" = """ + | encode s = + let val c = ord s in + if c < 32 then "&#" ^ string_of_int c ^ ";" + else if c < 127 then s + else "&#" ^ string_of_int c ^ ";" + end + + fun decode "lt" = "<" + | decode "gt" = ">" + | decode "amp" = "&" + | decode "apos" = "'" + | decode "quot" = "\"" + | decode s = chr (parse_int (unprefix "#" s)) + + fun entity_char c = c <> ";" + val parse_name = Scan.many entity_char + + val special = $$ "&" |-- (parse_name >> implode >> decode) --| $$ ";" + val regular = Scan.one Symbol.not_eof + val parse_chars = Scan.repeat (special || regular) >> implode + val parse_string = Scan.read Symbol.stopper parse_chars o raw_explode +in + val encode_string = translate_string encode + val decode_string = the o parse_string +end +\ + +ML_file "typed_eval.ML" +ML_file "codec.ML" +ML_file "ref_table.ML" +ML_file "protocol.ML" + +syntax "_cartouche_xml" :: "cartouche_position \ 'a" ("XML _") + +parse_translation\ +let + fun translation args = + let + fun err () = raise TERM ("Common._cartouche_xml", args) + fun input s pos = Symbol_Pos.implode (Symbol_Pos.cartouche_content (Symbol_Pos.explode (s, pos))) + val eval = Codec.the_decode Codec.term o XML.parse + in + case args of + [(c as Const (@{syntax_const "_constrain"}, _)) $ Free (s, _) $ p] => + (case Term_Position.decode_position p of + SOME (pos, _) => c $ eval (input s pos) $ p + | NONE => err ()) + | _ => err () + end +in + [(@{syntax_const "_cartouche_xml"}, K translation)] +end +\ + +end diff -r 62ff42cd45c7 -r 1aa20558eca8 libisabelle-1.0.1-protocol/protocol/Protocol.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/libisabelle-1.0.1-protocol/protocol/Protocol.thy Wed Sep 04 10:17:53 2019 +0200 @@ -0,0 +1,54 @@ +theory Protocol +imports Codec_Class +keywords "operation_setup" :: thy_decl % "ML" +begin + +ML\ +val _ = + let + open Libisabelle_Protocol + fun operation_setup_cmd name source (flags as {auto, ...}) ctxt = + let + fun eval enclose = + ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of source) + (ML_Lex.read ("Libisabelle_Protocol.add_operation " ^ ML_Syntax.print_string name ^ "(") @ + enclose (ML_Lex.read_source false source) @ + ML_Lex.read ")" @ + ML_Lex.read (print_flags flags)) + in + if auto then + let + (* FIXME breaks antiquotations *) + val ML_Types.Fun (arg, res) = ML_Types.ml_type_of ctxt (Input.source_content source) + val arg_codec = Classy.resolve @{ML.class codec} arg (Context.Proof ctxt) + val res_codec = Classy.resolve @{ML.class codec} res (Context.Proof ctxt) + fun enclose toks = + ML_Lex.read "{from_lib=" @ ML_Lex.read arg_codec @ ML_Lex.read "," @ + ML_Lex.read "to_lib=" @ ML_Lex.read res_codec @ ML_Lex.read "," @ + ML_Lex.read "action=" @ toks @ ML_Lex.read "}" + in + eval enclose + end + else + eval I + end + val parse_flag = + (Parse.reserved "sequential" || Parse.reserved "bracket" || Parse.reserved "auto") >> + (fn flag => join_flags + {sequential = flag = "sequential", + bracket = flag = "bracket", + auto = flag = "auto"}) + val parse_flags = + Parse.list parse_flag >> (fn fs => fold (curry op o) fs I) + val parse_cmd = + Scan.optional (Args.parens parse_flags) I -- + Parse.name -- + Parse.!!! (@{keyword "="} |-- Parse.ML_source) + in + Outer_Syntax.command @{command_keyword "operation_setup"} "define protocol operation in ML" + (parse_cmd >> (fn ((flags, name), txt) => + Toplevel.keep (Toplevel.context_of #> operation_setup_cmd name txt (flags default_flags)))) + end +\ + +end diff -r 62ff42cd45c7 -r 1aa20558eca8 libisabelle-1.0.1-protocol/protocol/codec.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/libisabelle-1.0.1-protocol/protocol/codec.ML Wed Sep 04 10:17:53 2019 +0200 @@ -0,0 +1,248 @@ +signature CODEC = sig + datatype 'a result = Success of 'a | Failure of string * XML.body + datatype ('a, 'b) either = Left of 'a | Right of 'b + type 'a codec + + val the_success: 'a result -> 'a + + val map_result: ('a -> 'b) -> 'a result -> 'b result + val bind_result: ('a -> 'b result) -> 'a result -> 'b result + val sequence_results: 'a result list -> 'a list result + val traverse_results: ('a -> 'b result) -> 'a list -> 'b list result + + val transform: ('a -> 'b) -> ('b -> 'a) -> 'a codec -> 'b codec + val encode: 'a codec -> 'a -> XML.tree + val decode: 'a codec -> XML.tree -> 'a result + val the_decode: 'a codec -> XML.tree -> 'a + + val basic: {encode: 'a -> XML.tree, decode: XML.tree -> 'a result} -> 'a codec + + val variant: ('a -> (int * XML.tree)) -> (int -> (XML.tree -> 'a result) option) -> string -> 'a codec + val tagged: string -> 'a codec -> 'a codec + + val unit: unit codec + val bool: bool codec + val string: string codec + val int: int codec + val list: 'a codec -> 'a list codec + val tuple: 'a codec -> 'b codec -> ('a * 'b) codec + val triple: 'a codec -> 'b codec -> 'c codec -> ('a * 'b * 'c) codec + val either: 'a codec -> 'b codec -> ('a, 'b) either codec + val option: 'a codec -> 'a option codec + val tree: XML.tree codec + + val sort: sort codec + val typ: typ codec + val term: term codec + + exception GENERIC of string + val exn: exn codec + val exn_result: 'a codec -> 'a Exn.result codec + + (* internal *) + val id: XML.tree codec +end + +structure Codec: CODEC = struct + +datatype 'a result = Success of 'a | Failure of string * XML.body +datatype ('a, 'b) either = Left of 'a | Right of 'b + +fun map_result f (Success a) = Success (f a) + | map_result _ (Failure (msg, body)) = Failure (msg, body) + +fun bind_result f (Success a) = f a + | bind_result _ (Failure (msg, body)) = Failure (msg, body) + +fun traverse_results _ [] = Success [] + | traverse_results f (x :: xs) = + case f x of + Success y => map_result (fn ys => y :: ys) (traverse_results f xs) + | Failure (msg, body) => Failure (msg, body) + +fun sequence_results xs = traverse_results I xs + +fun the_success (Success a) = a + | the_success _ = raise Fail "unexpected failure" + +fun add_tag tag idx body = + let + val attrs = case idx of SOME i => [("idx", XML.Encode.int_atom i)] | _ => [] + in XML.Elem (("tag", ("type", tag) :: attrs), body) end + +fun expect_tag tag tree = + case tree of + XML.Elem (("tag", [("type", tag')]), body) => + if tag = tag' then + Success body + else + Failure ("tag mismatch: expected " ^ tag ^ ", got " ^ tag', [tree]) + | _ => + Failure ("tag " ^ tag ^ " expected", [tree]) + +fun expect_tag' tag tree = + case tree of + XML.Elem (("tag", [("type", tag'), ("idx", i)]), body) => + if tag = tag' then + Success (XML.Decode.int_atom i, body) + handle XML.XML_ATOM err => Failure (err, [tree]) + else + Failure ("tag mismatch: expected " ^ tag ^ ", got " ^ tag', [tree]) + | _ => + Failure ("indexed tag " ^ tag ^ " expected", [tree]) + + +abstype 'a codec = Codec of {encode: 'a -> XML.tree, decode: XML.tree -> 'a result} with + +val basic = Codec + +fun encode (Codec {encode, ...}) = encode +fun decode (Codec {decode, ...}) = decode + +fun transform f g (Codec {encode, decode}) = Codec + {encode = g #> encode, + decode = decode #> map_result f} + +fun list a = Codec + {encode = map (encode a) #> add_tag "list" NONE, + decode = expect_tag "list" #> bind_result (traverse_results (decode a))} + +fun tuple a b = Codec + {encode = (fn (x, y) => add_tag "tuple" NONE [encode a x, encode b y]), + decode = expect_tag "tuple" #> bind_result (fn body => + case body of + [x, y] => decode a x |> bind_result (fn x' => decode b y |> map_result (pair x')) + | _ => Failure ("invalid structure", body))} + +fun variant enc dec tag = Codec + {encode = (fn a => let val (idx, tree) = enc a in add_tag tag (SOME idx) [tree] end), + decode = (fn tree => expect_tag' tag tree |> bind_result (fn (idx, body) => + case (body, dec idx) of + ([tree'], SOME res) => res tree' + | (_, SOME _) => Failure ("invalid structure", [tree]) + | (_, NONE) => Failure ("invalid index " ^ print_int idx, [tree])))} + +fun tagged tag a = Codec + {encode = encode a #> single #> add_tag tag NONE, + decode = expect_tag tag #> bind_result (fn body => + case body of + [tree] => decode a tree + | _ => Failure ("invalid structure", body))} + +val unit = Codec + {encode = K (add_tag "unit" NONE []), + decode = expect_tag "unit" #> bind_result (fn body => + case body of + [] => Success () + | _ => Failure ("expected nothing", body))} + +fun text to from = Codec + {encode = fn s => XML.Elem (("text", [("content", encode_string (to s))]), []), + decode = + (fn tree as XML.Elem (("text", [("content", s)]), []) => + (case from (decode_string s) of + NONE => Failure ("decoding failed", [tree]) | + SOME a => Success a) + | tree => Failure ("expected text tree", [tree]))} + +val id = Codec {encode = I, decode = Success} + +end + +fun the_decode c = the_success o decode c + +val int = tagged "int" (text print_int (Exn.get_res o Exn.capture parse_int)) +val bool = tagged "bool" (text print_bool (Exn.get_res o Exn.capture parse_bool)) +val string = tagged "string" (text I SOME) + +val tree = tagged "XML.tree" id + +fun option a = + let + fun enc (SOME x) = (0, encode a x) + | enc NONE = (1, encode unit ()) + fun dec 0 = SOME (decode a #> map_result SOME) + | dec 1 = SOME (decode unit #> map_result (K NONE)) + | dec _ = NONE + in variant enc dec "option" end + +val content_of = + XML.content_of o YXML.parse_body + +(* slightly fishy codec, doesn't preserve exception type *) +exception GENERIC of string + +fun string_of_exn (ERROR msg) = "ERROR " ^ content_of msg + | string_of_exn exn = content_of (@{make_string} exn) + +val exn = tagged "exn" (text string_of_exn (SOME o GENERIC)) + +fun exn_result a = + let + fun enc (Exn.Res t) = (0, encode a t) + | enc (Exn.Exn e) = (1, encode exn e) + fun dec _ = NONE + in variant enc dec "Exn.result" end + +fun triple a b c = + tuple a (tuple b c) + |> transform (fn (a, (b, c)) => (a, b, c)) (fn (a, b, c) => (a, (b, c))) + +fun either a b = + let + fun enc (Left l) = (0, encode a l) + | enc (Right r) = (1, encode b r) + fun dec 0 = SOME (decode a #> map_result Left) + | dec 1 = SOME (decode b #> map_result Right) + | dec _ = NONE + in variant enc dec "either" end + +val sort: sort codec = list string +val indexname: indexname codec = tuple string int + +fun typ () = + let + fun typ_type () = tuple string (list (typ ())) + val typ_tfree = tuple string sort + val typ_tvar = tuple indexname sort + + fun enc (Type arg) = (0, encode (typ_type ()) arg) + | enc (TFree arg) = (1, encode typ_tfree arg) + | enc (TVar arg) = (2, encode typ_tvar arg) + fun dec 0 = SOME (decode (typ_type ()) #> map_result Type) + | dec 1 = SOME (decode typ_tfree #> map_result TFree) + | dec 2 = SOME (decode typ_tvar #> map_result TVar) + | dec _ = NONE + in variant enc dec "typ" end + +val typ = typ () + +fun term () = + let + val term_const = tuple string typ + val term_free = tuple string typ + val term_var = tuple indexname typ + val term_bound = int + fun term_abs () = triple string typ (term ()) + fun term_app () = tuple (term ()) (term ()) + + fun enc (Const arg) = (0, encode term_const arg) + | enc (Free arg) = (1, encode term_free arg) + | enc (Var arg) = (2, encode term_var arg) + | enc (Bound arg) = (3, encode term_bound arg) + | enc (Abs arg) = (4, encode (term_abs ()) arg) + | enc (op $ arg) = (5, encode (term_app ()) arg) + fun dec 0 = SOME (decode term_const #> map_result Const) + | dec 1 = SOME (decode term_free #> map_result Free) + | dec 2 = SOME (decode term_var #> map_result Var) + | dec 3 = SOME (decode term_bound #> map_result Bound) + | dec 4 = SOME (decode (term_abs ()) #> map_result Abs) + | dec 5 = SOME (decode (term_app ()) #> map_result op $) + | dec _ = NONE + in variant enc dec "term" end + +val term = term () + +end + +type 'a codec = 'a Codec.codec \ No newline at end of file diff -r 62ff42cd45c7 -r 1aa20558eca8 libisabelle-1.0.1-protocol/protocol/protocol.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/libisabelle-1.0.1-protocol/protocol/protocol.ML Wed Sep 04 10:17:53 2019 +0200 @@ -0,0 +1,119 @@ +signature LIBISABELLE_PROTOCOL = sig + type name = string + type ('i, 'o) operation = + {from_lib : 'i codec, + to_lib : 'o codec, + action : 'i -> 'o} + + type flags = {sequential: bool, bracket: bool, auto: bool (* ignored *)} + + val default_flags : flags + val join_flags : flags -> flags -> flags + val print_flags : flags -> string + + val add_operation : name -> ('i, 'o) operation -> flags -> unit + val get_operation : name -> int -> XML.tree -> XML.tree +end + +structure Libisabelle_Protocol: LIBISABELLE_PROTOCOL = struct + +type name = string +type ('i, 'o) operation = + {from_lib : 'i codec, + to_lib : 'o codec, + action : 'i -> 'o} + +type flags = {sequential: bool, bracket: bool, auto: bool} + +val default_flags = {sequential = false, bracket = false, auto = false} + +fun join_flags + {sequential = seq1, bracket = br1, auto = a1} + {sequential = seq2, bracket = br2, auto = a2} = + {sequential = seq1 orelse seq2, bracket = br1 orelse br2, auto = a1 orelse a2} + +fun print_flags {sequential, bracket, auto} = + "({sequential=" ^ print_bool sequential ^ "," ^ + "bracket=" ^ print_bool bracket ^ "," ^ + "auto=" ^ print_bool auto ^ "})" + +type raw_operation = int -> XML.tree -> XML.tree + +exception GENERIC of string + +val operations = + Synchronized.var "libisabelle.operations" (Symtab.empty: raw_operation Symtab.table) + +val requests = + Synchronized.var "libisabelle.requests" (Inttab.empty: (unit -> unit) Inttab.table) + +fun sequentialize name f = + let + val var = Synchronized.var ("libisabelle." ^ name) () + in + fn x => Synchronized.change_result var (fn _ => (f x, ())) + end + +fun bracketize f id x = + let + val start = [(Markup.functionN, "libisabelle_start"), ("id", print_int id)] + val stop = [(Markup.functionN, "libisabelle_stop"), ("id", print_int id)] + val _ = Output.protocol_message start [] + val res = f id x + val _ = Output.protocol_message stop [] + in res end + +fun add_operation name {from_lib, to_lib, action} {sequential, bracket, ...} = + let + fun raw _ tree = + case Codec.decode from_lib tree of + Codec.Success i => Codec.encode to_lib (action i) + | Codec.Failure (msg, _) => raise Fail ("decoding input failed for operation " ^ name ^ ": " ^ msg) + val raw' = raw + |> (if bracket then bracketize else I) + |> (if sequential then sequentialize name else I) + in + Synchronized.change operations (Symtab.update (name, raw')) + end + +fun get_operation name = + case Symtab.lookup (Synchronized.value operations) name of + SOME operation => operation + | NONE => fn _ => error "libisabelle: unknown command" + +val _ = Isabelle_Process.protocol_command "libisabelle" + (fn id :: name :: [arg] => + let + val id = parse_int id + val response = [(Markup.functionN, "libisabelle_response"), ("id", print_int id)] + val args = YXML.parse arg + fun exec f = + let + val future = Future.fork (fn () => + let + val res = Exn.interruptible_capture (fn () => f id args) () + val yxml = YXML.string_of (Codec.encode (Codec.exn_result Codec.id) res) + in + Output.protocol_message response [yxml] + end) + in + Synchronized.change requests (Inttab.update_new (id, fn () => Future.cancel future)) + end + in + exec (get_operation name) + end) + +val _ = Isabelle_Process.protocol_command "libisabelle_cancel" + (fn ids => + let + fun remove id tab = (Inttab.lookup tab id, Inttab.delete_safe id tab) + val _ = + map parse_int ids + |> fold_map remove + |> Synchronized.change_result requests + |> map (fn NONE => () | SOME f => f ()) + in + () + end) + +end diff -r 62ff42cd45c7 -r 1aa20558eca8 libisabelle-1.0.1-protocol/protocol/ref_table.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/libisabelle-1.0.1-protocol/protocol/ref_table.ML Wed Sep 04 10:17:53 2019 +0200 @@ -0,0 +1,31 @@ +signature REF_TABLE = sig + type t + val read: serial -> t + val write: serial -> t -> unit + val delete: serial -> unit + + (* internal *) + val peek: unit -> t Inttab.table +end + +signature REF_TABLE_ARGS = sig + type t + val name: string +end + +functor Ref_Table(Args : REF_TABLE_ARGS) : REF_TABLE where type t = Args.t = struct + +type t = Args.t + +type table = t Inttab.table +val empty_table : table = Inttab.empty + +val table = Synchronized.var ("Ref_Table." ^ Args.name) empty_table + +fun read ser = the (Inttab.lookup (Synchronized.value table) ser) +fun write ser t = Synchronized.change table (Inttab.update (ser, t)) +val delete = Synchronized.change table o Inttab.delete + +fun peek () = Synchronized.value table + +end diff -r 62ff42cd45c7 -r 1aa20558eca8 libisabelle-1.0.1-protocol/protocol/typed_eval.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/libisabelle-1.0.1-protocol/protocol/typed_eval.ML Wed Sep 04 10:17:53 2019 +0200 @@ -0,0 +1,38 @@ +signature TYPED_EVAL = sig + type T + val eval: Input.source -> Proof.context -> T + + val fulfill: T -> Context.generic -> Context.generic (* internal *) +end + +signature TYPED_EVAL_ARGS = sig + type T + val typ: string + val name: string +end + +functor Typed_Eval(Args : TYPED_EVAL_ARGS) : TYPED_EVAL = struct + +structure Data = Generic_Data +( + type T = Args.T option + val empty = NONE + val extend = I + fun merge (NONE, NONE) = NONE + | merge _ = error "Typed_Eval.Data.merge: can't merge" +) + +type T = Args.T + +val fulfill = Data.map o K o SOME + +fun eval source ctxt = + ML_Context.expression (Input.range_of source) + "typed_eval_result" Args.typ + (Args.name ^ ".fulfill typed_eval_result") + (ML_Lex.read_source false source) + (Context.Proof ctxt) + |> Data.get + |> the + +end \ No newline at end of file diff -r 62ff42cd45c7 -r 1aa20558eca8 src/Tools/isac/MathEngine/MathEngine.thy --- a/src/Tools/isac/MathEngine/MathEngine.thy Tue Sep 03 17:43:42 2019 +0200 +++ b/src/Tools/isac/MathEngine/MathEngine.thy Wed Sep 04 10:17:53 2019 +0200 @@ -4,7 +4,8 @@ *) theory MathEngine -imports "~~/src/Tools/isac/Interpret/Interpret" + imports "~~/src/Tools/isac/Interpret/Interpret" + begin ML_file solve.sml ML_file "mathengine-stateless.sml" diff -r 62ff42cd45c7 -r 1aa20558eca8 src/Tools/isac/ROOT --- a/src/Tools/isac/ROOT Tue Sep 03 17:43:42 2019 +0200 +++ b/src/Tools/isac/ROOT Wed Sep 04 10:17:53 2019 +0200 @@ -15,14 +15,14 @@ (* run "./bin/isabelle build -v -b Isac" *) session Isac in "~~/src/Tools/isac" = HOL + - description {* + description \ Isac core, prototype of a math-engine and knowledge for a TP-based educational mathematics assistant. - The java front-end is under development at TU Graz and at FH Hagenberg, + The java front-end is under development at FH Hagenberg, the Isabelle/ML math-engine and Isabelle knowledge at RISC Linz. See http://www.ist.tugraz.at/isac/. - *} + \ options [document = false (*, browser_info = true*)] sessions Protocol (* Codec.encode etc required in mathml.sml only *) @@ -34,15 +34,15 @@ or just "./bin/isabelle jedit -l libisabelle_Isac & " *) session libisabelle_Isac in "~~/src/Tools/isac" = HOL + - description {* + description \ Isac core, prototype of a math-engine and knowledge for engineering math + libisabelle by Lars Hupel as interface to the java front-end: https://github.com/larsrh/libisabelle - The java front-end is under development at TU Graz and at FH Hagenberg, + The java front-end is under development at at FH Hagenberg, the Isabelle/ML math-engine and Isabelle knowledge at RISC Linz. See http://www.ist.tugraz.at/isac/. - *} + \ options [document = false (*, browser_info = true*)] sessions Isac