1.1 --- a/ROOTS Tue Sep 03 17:43:42 2019 +0200
1.2 +++ b/ROOTS Wed Sep 04 10:17:53 2019 +0200
1.3 @@ -10,6 +10,6 @@
1.4 src/Sequents
1.5 src/Doc
1.6 src/Tools
1.7 -#src/Tools/isac
1.8 -#libisabelle-protocol
1.9 +src/Tools/isac
1.10 +libisabelle-1.0.1-protocol
1.11 test/Tools/isac/ADDTESTS/session-get_theory/
1.12 \ No newline at end of file
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/libisabelle-1.0.1-protocol/Protocol_Main.thy Wed Sep 04 10:17:53 2019 +0200
2.3 @@ -0,0 +1,9 @@
2.4 +theory Protocol_Main
2.5 +imports
2.6 + Main
2.7 + "operations/HOL_Operations"
2.8 + Protocol.Basic
2.9 + Protocol.ML_Expr
2.10 +begin
2.11 +
2.12 +end
2.13 \ No newline at end of file
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/libisabelle-1.0.1-protocol/Protocol_Pure.thy Wed Sep 04 10:17:53 2019 +0200
3.3 @@ -0,0 +1,8 @@
3.4 +theory Protocol_Pure
3.5 +imports
3.6 + Pure
3.7 + "operations/Basic"
3.8 + "operations/ML_Expr"
3.9 +begin
3.10 +
3.11 +end
3.12 \ No newline at end of file
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/libisabelle-1.0.1-protocol/ROOT Wed Sep 04 10:17:53 2019 +0200
4.3 @@ -0,0 +1,13 @@
4.4 +session Protocol = Classy +
4.5 + theories
4.6 + "protocol/Protocol"
4.7 + "protocol/Codec_Test"
4.8 + "Protocol_Pure"
4.9 +
4.10 +session "HOL-Protocol" = "HOL-Classy" +
4.11 + sessions
4.12 + Protocol
4.13 + theories
4.14 + Protocol.Protocol
4.15 + Protocol.Codec_Test
4.16 + "Protocol_Main"
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/libisabelle-1.0.1-protocol/operations/Basic.thy Wed Sep 04 10:17:53 2019 +0200
5.3 @@ -0,0 +1,11 @@
5.4 +theory Basic
5.5 +imports "../protocol/Protocol"
5.6 +begin
5.7 +
5.8 +operation_setup (auto) ping = \<open>fn () => ()\<close>
5.9 +
5.10 +operation_setup (auto) hello = \<open>fn data => "Hello " ^ data\<close>
5.11 +
5.12 +operation_setup (sequential, bracket, auto) use_thys = \<open>List.app Thy_Info.use_thy\<close>
5.13 +
5.14 +end
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/libisabelle-1.0.1-protocol/operations/HOL_Operations.thy Wed Sep 04 10:17:53 2019 +0200
6.3 @@ -0,0 +1,24 @@
6.4 +theory HOL_Operations
6.5 +imports Main Protocol.Protocol
6.6 +begin
6.7 +
6.8 +operation_setup mk_int = \<open>
6.9 + {from_lib = Codec.int,
6.10 + to_lib = Codec.term,
6.11 + action = HOLogic.mk_number @{typ int}}\<close>
6.12 +
6.13 +operation_setup dest_int = \<open>
6.14 + {from_lib = Codec.term,
6.15 + to_lib = Codec.option Codec.int,
6.16 + action = fn t => case try HOLogic.dest_number t of
6.17 + NONE => NONE
6.18 + | SOME (typ, n) =>
6.19 + if typ = @{typ int} then
6.20 + SOME n
6.21 + else
6.22 + NONE}\<close>
6.23 +
6.24 +operation_setup (auto) mk_list = \<open>uncurry HOLogic.mk_list\<close>
6.25 +operation_setup (auto) dest_list = \<open>try HOLogic.dest_list\<close>
6.26 +
6.27 +end
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/libisabelle-1.0.1-protocol/operations/ML_Expr.thy Wed Sep 04 10:17:53 2019 +0200
7.3 @@ -0,0 +1,41 @@
7.4 +theory ML_Expr
7.5 +imports "../protocol/Protocol"
7.6 +begin
7.7 +
7.8 +ML_file "ml_expr.ML"
7.9 +ML_file "refs.ML"
7.10 +
7.11 +operation_setup eval_expr = \<open>
7.12 + {from_lib = Codec.triple Codec.string ML_Expr.codec Codec.string,
7.13 + to_lib = Codec.tree,
7.14 + action = fn (typ, prog, thy_name) =>
7.15 + let
7.16 + val thy = get_theory thy_name
7.17 + val ctxt = Proof_Context.init_global thy
7.18 + in
7.19 + ML_Expr.eval ctxt prog typ
7.20 + end}\<close>
7.21 +
7.22 +operation_setup eval_opaque_expr = \<open>
7.23 + {from_lib = Codec.triple (Codec.triple Codec.string Codec.string ML_Expr.codec) ML_Expr.codec Codec.string,
7.24 + to_lib = Codec.tuple Codec.int Codec.tree,
7.25 + action = fn ((table, repr_typ, conv), prog, thy_name) =>
7.26 + let
7.27 + val thy = get_theory thy_name
7.28 + val ctxt = Proof_Context.init_global thy
7.29 + in
7.30 + ML_Expr.eval_opaque ctxt prog {table = table, repr_typ = repr_typ, conv = conv}
7.31 + end}\<close>
7.32 +
7.33 +operation_setup check_expr = \<open>
7.34 + {from_lib = Codec.triple Codec.string ML_Expr.codec Codec.string,
7.35 + to_lib = Codec.option Codec.string,
7.36 + action = fn (typ, prog, thy_name) =>
7.37 + let
7.38 + val thy = get_theory thy_name
7.39 + val ctxt = Proof_Context.init_global thy
7.40 + in
7.41 + ML_Expr.check ctxt prog typ
7.42 + end}\<close>
7.43 +
7.44 +end
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/libisabelle-1.0.1-protocol/operations/ml_expr.ML Wed Sep 04 10:17:53 2019 +0200
8.3 @@ -0,0 +1,132 @@
8.4 +signature ML_EXPR = sig
8.5 + datatype ml_expr =
8.6 + Lit of string
8.7 + | App of ml_expr * ml_expr
8.8 + | Val of string * XML.tree
8.9 +
8.10 + val print_ml_expr: Proof.context -> ml_expr -> string
8.11 + val eval: Proof.context -> ml_expr -> string -> XML.tree
8.12 + val eval_opaque: Proof.context -> ml_expr -> {table: string, repr_typ: string, conv: ml_expr} -> serial * XML.tree
8.13 + val check: Proof.context -> ml_expr -> string -> string option
8.14 +
8.15 + val print_tree: XML.tree -> string
8.16 + val print_body: XML.body -> string
8.17 +
8.18 + (* internal *)
8.19 + val codec: ml_expr codec
8.20 + structure Eval : TYPED_EVAL
8.21 +end
8.22 +
8.23 +structure ML_Expr : ML_EXPR = struct
8.24 +
8.25 +structure Eval = Typed_Eval
8.26 +(
8.27 + type T = XML.tree
8.28 + val typ = "XML.tree"
8.29 + val name = "ML_Expr.Eval"
8.30 +)
8.31 +
8.32 +fun print_tree (XML.Elem elem) =
8.33 + let
8.34 + val str =
8.35 + ML_Syntax.print_pair
8.36 + (ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_properties)
8.37 + print_body
8.38 + elem
8.39 + in "(XML.Elem " ^ str ^ ")" end
8.40 + | print_tree (XML.Text text) =
8.41 + "(XML.Text " ^ ML_Syntax.print_string text ^ ")"
8.42 +and print_body body =
8.43 + ML_Syntax.print_list print_tree body
8.44 +
8.45 +datatype ml_expr =
8.46 + Lit of string
8.47 + | App of ml_expr * ml_expr
8.48 + | Val of string * XML.tree
8.49 +
8.50 +fun print_ml_expr _ (Lit text) =
8.51 + text
8.52 + | print_ml_expr ctxt (App (f, x)) =
8.53 + "(" ^ print_ml_expr ctxt f ^ ") (" ^ print_ml_expr ctxt x ^ ")"
8.54 + | print_ml_expr ctxt (Val (typ, value)) =
8.55 + let
8.56 + val codec = Classy.resolve @{ML.class codec} (ML_Types.read_ml_type typ) (Context.Proof ctxt)
8.57 + in "(Codec.the_decode " ^ codec ^ " " ^ print_tree value ^ ")" end
8.58 +
8.59 +fun check ctxt prog raw_typ =
8.60 + case try ML_Types.read_ml_type raw_typ of
8.61 + NONE => SOME ("failed to parse result type " ^ raw_typ)
8.62 + | SOME typ =>
8.63 + let
8.64 + val context = Context.Proof ctxt
8.65 + val codec = can (Classy.resolve @{ML.class codec} typ) context
8.66 +
8.67 + fun check_vals (Lit _) = NONE
8.68 + | check_vals (App (f, x)) = merge_options (check_vals f, check_vals x)
8.69 + | check_vals (Val (raw_typ, _)) =
8.70 + case try ML_Types.read_ml_type raw_typ of
8.71 + NONE => SOME ("failed to parse value type " ^ raw_typ)
8.72 + | SOME _ =>
8.73 + if can (Classy.resolve @{ML.class codec} typ) context then
8.74 + NONE
8.75 + else
8.76 + SOME ("could not resolve codec for value type " ^ raw_typ)
8.77 + in
8.78 + if not codec then
8.79 + SOME ("could not resolve codec for result type " ^ raw_typ)
8.80 + else
8.81 + case check_vals prog of
8.82 + SOME err => SOME err
8.83 + | NONE =>
8.84 + case Exn.capture (ML_Types.ml_type_of ctxt) (print_ml_expr ctxt prog) of
8.85 + Exn.Res typ' =>
8.86 + if typ = typ' then
8.87 + NONE
8.88 + else
8.89 + SOME ("expected result type " ^ raw_typ ^ " but got something else")
8.90 + | Exn.Exn exn =>
8.91 + SOME ("compilation error: " ^ @{make_string} exn)
8.92 + end
8.93 +
8.94 +fun eval ctxt prog typ =
8.95 + let
8.96 + val codec = Classy.resolve @{ML.class codec} (ML_Types.read_ml_type typ) (Context.Proof ctxt)
8.97 + val prog = "(Codec.encode " ^ codec ^ " (" ^ print_ml_expr ctxt prog ^ "))"
8.98 + in
8.99 + Eval.eval (Input.string prog) ctxt
8.100 + end
8.101 +
8.102 +fun eval_opaque ctxt prog {table, repr_typ, conv} =
8.103 + let
8.104 + val codec = Classy.resolve @{ML.class codec} (ML_Types.read_ml_type repr_typ) (Context.Proof ctxt)
8.105 + val id = serial ()
8.106 + val var = "eval_opaque_result"
8.107 + val inner_prog = "(" ^ print_ml_expr ctxt prog ^ ")"
8.108 + val store_prog = table ^ ".write " ^ ML_Syntax.print_int id ^ " " ^ var
8.109 + val res_prog = "Codec.encode " ^ codec ^ " ((" ^ print_ml_expr ctxt conv ^ ") " ^ var ^ ")"
8.110 + val prog =
8.111 + "(let " ^
8.112 + "val " ^ var ^ " = " ^ inner_prog ^
8.113 + " in " ^
8.114 + "(" ^ store_prog ^ " ; " ^ res_prog ^ ") " ^
8.115 + "end)"
8.116 + in
8.117 + (id, Eval.eval (Input.string prog) ctxt)
8.118 + end
8.119 +
8.120 +fun codec () =
8.121 + let
8.122 + val ml_expr_lit = Codec.string
8.123 + fun ml_expr_app () = Codec.tuple (codec ()) (codec ())
8.124 + val ml_expr_val = Codec.tuple Codec.string Codec.tree
8.125 +
8.126 + fun enc _ = error "impossible"
8.127 + fun dec 0 = SOME (Codec.decode ml_expr_lit #> Codec.map_result Lit)
8.128 + | dec 1 = SOME (Codec.decode (ml_expr_app ()) #> Codec.map_result App)
8.129 + | dec 2 = SOME (Codec.decode ml_expr_val #> Codec.map_result Val)
8.130 + | dec _ = NONE
8.131 + in Codec.variant enc dec "ML_Expr.ml_expr" end
8.132 +
8.133 +val codec = codec ()
8.134 +
8.135 +end
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/libisabelle-1.0.1-protocol/operations/refs.ML Wed Sep 04 10:17:53 2019 +0200
9.3 @@ -0,0 +1,7 @@
9.4 +structure Refs = struct
9.5 + structure Thy = Ref_Table(type t = theory; val name = "Refs.Thy")
9.6 + structure Ctxt = Ref_Table(type t = Proof.context; val name = "Refs.Ctxt")
9.7 + structure State = Ref_Table(type t = Proof.state; val name = "Refs.State")
9.8 + structure Thm = Ref_Table(type t = thm; val name = "Refs.Thm")
9.9 + structure Cterm = Ref_Table(type t = cterm; val name = "Refs.Cterm")
9.10 +end
9.11 \ No newline at end of file
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/libisabelle-1.0.1-protocol/protocol/Codec_Class.thy Wed Sep 04 10:17:53 2019 +0200
10.3 @@ -0,0 +1,21 @@
10.4 +theory Codec_Class
10.5 +imports Common "Classy.Classy"
10.6 +begin
10.7 +
10.8 +ML.class codec = \<open>'a codec\<close>
10.9 +
10.10 +ML.instance \<open>Codec.unit\<close> :: codec
10.11 +ML.instance \<open>Codec.bool\<close> :: codec
10.12 +ML.instance \<open>Codec.string\<close> :: codec
10.13 +ML.instance \<open>Codec.int\<close> :: codec
10.14 +ML.instance \<open>Codec.list\<close> :: codec
10.15 +ML.instance \<open>Codec.tuple\<close> :: codec
10.16 +ML.instance \<open>Codec.option\<close> :: codec
10.17 +ML.instance \<open>Codec.either\<close> :: codec
10.18 +ML.instance \<open>Codec.triple\<close> :: codec
10.19 +ML.instance \<open>Codec.sort\<close> :: codec
10.20 +ML.instance \<open>Codec.typ\<close> :: codec
10.21 +ML.instance \<open>Codec.term\<close> :: codec
10.22 +ML.instance \<open>Codec.tree\<close> :: codec
10.23 +
10.24 +end
11.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/libisabelle-1.0.1-protocol/protocol/Codec_Test.thy Wed Sep 04 10:17:53 2019 +0200
11.3 @@ -0,0 +1,41 @@
11.4 +theory Codec_Test
11.5 +imports Common "~~/src/Tools/Spec_Check/Spec_Check"
11.6 +begin
11.7 +
11.8 +ML\<open>
11.9 +fun check_for str =
11.10 + let
11.11 + val prop1 =
11.12 + "ALL x. (let val c = (" ^ str ^ ") in Codec.decode c (Codec.encode c x) = Codec.Success x end)"
11.13 + val prop2 =
11.14 + "ALL x. (let val c = (" ^ str ^ ") in Codec.decode c (YXML.parse (YXML.string_of (Codec.encode c x))) = Codec.Success x end)"
11.15 + in
11.16 + check_property prop1;
11.17 + check_property prop2
11.18 + end
11.19 +
11.20 +fun gen_unit r =
11.21 + ((), r)
11.22 +\<close>
11.23 +
11.24 +ML_command\<open>
11.25 + check_for "Codec.unit";
11.26 + check_for "Codec.int";
11.27 + check_for "Codec.bool";
11.28 + check_for "Codec.string";
11.29 + check_for "Codec.tuple Codec.int Codec.int";
11.30 + check_for "Codec.tuple Codec.string Codec.unit";
11.31 + check_for "Codec.list Codec.unit";
11.32 + check_for "Codec.list Codec.int";
11.33 + check_for "Codec.list Codec.string";
11.34 + check_for "Codec.list (Codec.list Codec.string)";
11.35 + check_for "Codec.list (Codec.tuple Codec.int Codec.int)";
11.36 + check_for "Codec.tuple Codec.int (Codec.list Codec.int)";
11.37 + check_for "Codec.option Codec.int";
11.38 + check_for "Codec.option (Codec.list Codec.int)";
11.39 + check_for "Codec.list (Codec.option (Codec.int))";
11.40 + check_for "Codec.term";
11.41 + check_for "Codec.typ";
11.42 +\<close>
11.43 +
11.44 +end
12.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
12.2 +++ b/libisabelle-1.0.1-protocol/protocol/Common.thy Wed Sep 04 10:17:53 2019 +0200
12.3 @@ -0,0 +1,80 @@
12.4 +theory Common
12.5 +imports Pure
12.6 +begin
12.7 +
12.8 +ML\<open>
12.9 + val print_int = Value.print_int
12.10 + val parse_int = Value.parse_int
12.11 + val print_bool = Value.print_bool
12.12 + val parse_bool = Value.parse_bool
12.13 + fun get_theory name =
12.14 + let
12.15 + val all = Thy_Info.get_names ()
12.16 + val qualified = find_first (fn name' => name = Long_Name.base_name name') all
12.17 + in Thy_Info.get_theory (the qualified) end
12.18 +\<close>
12.19 +
12.20 +ML\<open>
12.21 +local
12.22 + (* code copied and adapted from Isabelle/Pure *)
12.23 +
12.24 + fun encode "<" = "<"
12.25 + | encode ">" = ">"
12.26 + | encode "&" = "&"
12.27 + | encode "'" = "'"
12.28 + | encode "\"" = """
12.29 + | encode s =
12.30 + let val c = ord s in
12.31 + if c < 32 then "&#" ^ string_of_int c ^ ";"
12.32 + else if c < 127 then s
12.33 + else "&#" ^ string_of_int c ^ ";"
12.34 + end
12.35 +
12.36 + fun decode "lt" = "<"
12.37 + | decode "gt" = ">"
12.38 + | decode "amp" = "&"
12.39 + | decode "apos" = "'"
12.40 + | decode "quot" = "\""
12.41 + | decode s = chr (parse_int (unprefix "#" s))
12.42 +
12.43 + fun entity_char c = c <> ";"
12.44 + val parse_name = Scan.many entity_char
12.45 +
12.46 + val special = $$ "&" |-- (parse_name >> implode >> decode) --| $$ ";"
12.47 + val regular = Scan.one Symbol.not_eof
12.48 + val parse_chars = Scan.repeat (special || regular) >> implode
12.49 + val parse_string = Scan.read Symbol.stopper parse_chars o raw_explode
12.50 +in
12.51 + val encode_string = translate_string encode
12.52 + val decode_string = the o parse_string
12.53 +end
12.54 +\<close>
12.55 +
12.56 +ML_file "typed_eval.ML"
12.57 +ML_file "codec.ML"
12.58 +ML_file "ref_table.ML"
12.59 +ML_file "protocol.ML"
12.60 +
12.61 +syntax "_cartouche_xml" :: "cartouche_position \<Rightarrow> 'a" ("XML _")
12.62 +
12.63 +parse_translation\<open>
12.64 +let
12.65 + fun translation args =
12.66 + let
12.67 + fun err () = raise TERM ("Common._cartouche_xml", args)
12.68 + fun input s pos = Symbol_Pos.implode (Symbol_Pos.cartouche_content (Symbol_Pos.explode (s, pos)))
12.69 + val eval = Codec.the_decode Codec.term o XML.parse
12.70 + in
12.71 + case args of
12.72 + [(c as Const (@{syntax_const "_constrain"}, _)) $ Free (s, _) $ p] =>
12.73 + (case Term_Position.decode_position p of
12.74 + SOME (pos, _) => c $ eval (input s pos) $ p
12.75 + | NONE => err ())
12.76 + | _ => err ()
12.77 + end
12.78 +in
12.79 + [(@{syntax_const "_cartouche_xml"}, K translation)]
12.80 +end
12.81 +\<close>
12.82 +
12.83 +end
13.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
13.2 +++ b/libisabelle-1.0.1-protocol/protocol/Protocol.thy Wed Sep 04 10:17:53 2019 +0200
13.3 @@ -0,0 +1,54 @@
13.4 +theory Protocol
13.5 +imports Codec_Class
13.6 +keywords "operation_setup" :: thy_decl % "ML"
13.7 +begin
13.8 +
13.9 +ML\<open>
13.10 +val _ =
13.11 + let
13.12 + open Libisabelle_Protocol
13.13 + fun operation_setup_cmd name source (flags as {auto, ...}) ctxt =
13.14 + let
13.15 + fun eval enclose =
13.16 + ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of source)
13.17 + (ML_Lex.read ("Libisabelle_Protocol.add_operation " ^ ML_Syntax.print_string name ^ "(") @
13.18 + enclose (ML_Lex.read_source false source) @
13.19 + ML_Lex.read ")" @
13.20 + ML_Lex.read (print_flags flags))
13.21 + in
13.22 + if auto then
13.23 + let
13.24 + (* FIXME breaks antiquotations *)
13.25 + val ML_Types.Fun (arg, res) = ML_Types.ml_type_of ctxt (Input.source_content source)
13.26 + val arg_codec = Classy.resolve @{ML.class codec} arg (Context.Proof ctxt)
13.27 + val res_codec = Classy.resolve @{ML.class codec} res (Context.Proof ctxt)
13.28 + fun enclose toks =
13.29 + ML_Lex.read "{from_lib=" @ ML_Lex.read arg_codec @ ML_Lex.read "," @
13.30 + ML_Lex.read "to_lib=" @ ML_Lex.read res_codec @ ML_Lex.read "," @
13.31 + ML_Lex.read "action=" @ toks @ ML_Lex.read "}"
13.32 + in
13.33 + eval enclose
13.34 + end
13.35 + else
13.36 + eval I
13.37 + end
13.38 + val parse_flag =
13.39 + (Parse.reserved "sequential" || Parse.reserved "bracket" || Parse.reserved "auto") >>
13.40 + (fn flag => join_flags
13.41 + {sequential = flag = "sequential",
13.42 + bracket = flag = "bracket",
13.43 + auto = flag = "auto"})
13.44 + val parse_flags =
13.45 + Parse.list parse_flag >> (fn fs => fold (curry op o) fs I)
13.46 + val parse_cmd =
13.47 + Scan.optional (Args.parens parse_flags) I --
13.48 + Parse.name --
13.49 + Parse.!!! (@{keyword "="} |-- Parse.ML_source)
13.50 + in
13.51 + Outer_Syntax.command @{command_keyword "operation_setup"} "define protocol operation in ML"
13.52 + (parse_cmd >> (fn ((flags, name), txt) =>
13.53 + Toplevel.keep (Toplevel.context_of #> operation_setup_cmd name txt (flags default_flags))))
13.54 + end
13.55 +\<close>
13.56 +
13.57 +end
14.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
14.2 +++ b/libisabelle-1.0.1-protocol/protocol/codec.ML Wed Sep 04 10:17:53 2019 +0200
14.3 @@ -0,0 +1,248 @@
14.4 +signature CODEC = sig
14.5 + datatype 'a result = Success of 'a | Failure of string * XML.body
14.6 + datatype ('a, 'b) either = Left of 'a | Right of 'b
14.7 + type 'a codec
14.8 +
14.9 + val the_success: 'a result -> 'a
14.10 +
14.11 + val map_result: ('a -> 'b) -> 'a result -> 'b result
14.12 + val bind_result: ('a -> 'b result) -> 'a result -> 'b result
14.13 + val sequence_results: 'a result list -> 'a list result
14.14 + val traverse_results: ('a -> 'b result) -> 'a list -> 'b list result
14.15 +
14.16 + val transform: ('a -> 'b) -> ('b -> 'a) -> 'a codec -> 'b codec
14.17 + val encode: 'a codec -> 'a -> XML.tree
14.18 + val decode: 'a codec -> XML.tree -> 'a result
14.19 + val the_decode: 'a codec -> XML.tree -> 'a
14.20 +
14.21 + val basic: {encode: 'a -> XML.tree, decode: XML.tree -> 'a result} -> 'a codec
14.22 +
14.23 + val variant: ('a -> (int * XML.tree)) -> (int -> (XML.tree -> 'a result) option) -> string -> 'a codec
14.24 + val tagged: string -> 'a codec -> 'a codec
14.25 +
14.26 + val unit: unit codec
14.27 + val bool: bool codec
14.28 + val string: string codec
14.29 + val int: int codec
14.30 + val list: 'a codec -> 'a list codec
14.31 + val tuple: 'a codec -> 'b codec -> ('a * 'b) codec
14.32 + val triple: 'a codec -> 'b codec -> 'c codec -> ('a * 'b * 'c) codec
14.33 + val either: 'a codec -> 'b codec -> ('a, 'b) either codec
14.34 + val option: 'a codec -> 'a option codec
14.35 + val tree: XML.tree codec
14.36 +
14.37 + val sort: sort codec
14.38 + val typ: typ codec
14.39 + val term: term codec
14.40 +
14.41 + exception GENERIC of string
14.42 + val exn: exn codec
14.43 + val exn_result: 'a codec -> 'a Exn.result codec
14.44 +
14.45 + (* internal *)
14.46 + val id: XML.tree codec
14.47 +end
14.48 +
14.49 +structure Codec: CODEC = struct
14.50 +
14.51 +datatype 'a result = Success of 'a | Failure of string * XML.body
14.52 +datatype ('a, 'b) either = Left of 'a | Right of 'b
14.53 +
14.54 +fun map_result f (Success a) = Success (f a)
14.55 + | map_result _ (Failure (msg, body)) = Failure (msg, body)
14.56 +
14.57 +fun bind_result f (Success a) = f a
14.58 + | bind_result _ (Failure (msg, body)) = Failure (msg, body)
14.59 +
14.60 +fun traverse_results _ [] = Success []
14.61 + | traverse_results f (x :: xs) =
14.62 + case f x of
14.63 + Success y => map_result (fn ys => y :: ys) (traverse_results f xs)
14.64 + | Failure (msg, body) => Failure (msg, body)
14.65 +
14.66 +fun sequence_results xs = traverse_results I xs
14.67 +
14.68 +fun the_success (Success a) = a
14.69 + | the_success _ = raise Fail "unexpected failure"
14.70 +
14.71 +fun add_tag tag idx body =
14.72 + let
14.73 + val attrs = case idx of SOME i => [("idx", XML.Encode.int_atom i)] | _ => []
14.74 + in XML.Elem (("tag", ("type", tag) :: attrs), body) end
14.75 +
14.76 +fun expect_tag tag tree =
14.77 + case tree of
14.78 + XML.Elem (("tag", [("type", tag')]), body) =>
14.79 + if tag = tag' then
14.80 + Success body
14.81 + else
14.82 + Failure ("tag mismatch: expected " ^ tag ^ ", got " ^ tag', [tree])
14.83 + | _ =>
14.84 + Failure ("tag " ^ tag ^ " expected", [tree])
14.85 +
14.86 +fun expect_tag' tag tree =
14.87 + case tree of
14.88 + XML.Elem (("tag", [("type", tag'), ("idx", i)]), body) =>
14.89 + if tag = tag' then
14.90 + Success (XML.Decode.int_atom i, body)
14.91 + handle XML.XML_ATOM err => Failure (err, [tree])
14.92 + else
14.93 + Failure ("tag mismatch: expected " ^ tag ^ ", got " ^ tag', [tree])
14.94 + | _ =>
14.95 + Failure ("indexed tag " ^ tag ^ " expected", [tree])
14.96 +
14.97 +
14.98 +abstype 'a codec = Codec of {encode: 'a -> XML.tree, decode: XML.tree -> 'a result} with
14.99 +
14.100 +val basic = Codec
14.101 +
14.102 +fun encode (Codec {encode, ...}) = encode
14.103 +fun decode (Codec {decode, ...}) = decode
14.104 +
14.105 +fun transform f g (Codec {encode, decode}) = Codec
14.106 + {encode = g #> encode,
14.107 + decode = decode #> map_result f}
14.108 +
14.109 +fun list a = Codec
14.110 + {encode = map (encode a) #> add_tag "list" NONE,
14.111 + decode = expect_tag "list" #> bind_result (traverse_results (decode a))}
14.112 +
14.113 +fun tuple a b = Codec
14.114 + {encode = (fn (x, y) => add_tag "tuple" NONE [encode a x, encode b y]),
14.115 + decode = expect_tag "tuple" #> bind_result (fn body =>
14.116 + case body of
14.117 + [x, y] => decode a x |> bind_result (fn x' => decode b y |> map_result (pair x'))
14.118 + | _ => Failure ("invalid structure", body))}
14.119 +
14.120 +fun variant enc dec tag = Codec
14.121 + {encode = (fn a => let val (idx, tree) = enc a in add_tag tag (SOME idx) [tree] end),
14.122 + decode = (fn tree => expect_tag' tag tree |> bind_result (fn (idx, body) =>
14.123 + case (body, dec idx) of
14.124 + ([tree'], SOME res) => res tree'
14.125 + | (_, SOME _) => Failure ("invalid structure", [tree])
14.126 + | (_, NONE) => Failure ("invalid index " ^ print_int idx, [tree])))}
14.127 +
14.128 +fun tagged tag a = Codec
14.129 + {encode = encode a #> single #> add_tag tag NONE,
14.130 + decode = expect_tag tag #> bind_result (fn body =>
14.131 + case body of
14.132 + [tree] => decode a tree
14.133 + | _ => Failure ("invalid structure", body))}
14.134 +
14.135 +val unit = Codec
14.136 + {encode = K (add_tag "unit" NONE []),
14.137 + decode = expect_tag "unit" #> bind_result (fn body =>
14.138 + case body of
14.139 + [] => Success ()
14.140 + | _ => Failure ("expected nothing", body))}
14.141 +
14.142 +fun text to from = Codec
14.143 + {encode = fn s => XML.Elem (("text", [("content", encode_string (to s))]), []),
14.144 + decode =
14.145 + (fn tree as XML.Elem (("text", [("content", s)]), []) =>
14.146 + (case from (decode_string s) of
14.147 + NONE => Failure ("decoding failed", [tree]) |
14.148 + SOME a => Success a)
14.149 + | tree => Failure ("expected text tree", [tree]))}
14.150 +
14.151 +val id = Codec {encode = I, decode = Success}
14.152 +
14.153 +end
14.154 +
14.155 +fun the_decode c = the_success o decode c
14.156 +
14.157 +val int = tagged "int" (text print_int (Exn.get_res o Exn.capture parse_int))
14.158 +val bool = tagged "bool" (text print_bool (Exn.get_res o Exn.capture parse_bool))
14.159 +val string = tagged "string" (text I SOME)
14.160 +
14.161 +val tree = tagged "XML.tree" id
14.162 +
14.163 +fun option a =
14.164 + let
14.165 + fun enc (SOME x) = (0, encode a x)
14.166 + | enc NONE = (1, encode unit ())
14.167 + fun dec 0 = SOME (decode a #> map_result SOME)
14.168 + | dec 1 = SOME (decode unit #> map_result (K NONE))
14.169 + | dec _ = NONE
14.170 + in variant enc dec "option" end
14.171 +
14.172 +val content_of =
14.173 + XML.content_of o YXML.parse_body
14.174 +
14.175 +(* slightly fishy codec, doesn't preserve exception type *)
14.176 +exception GENERIC of string
14.177 +
14.178 +fun string_of_exn (ERROR msg) = "ERROR " ^ content_of msg
14.179 + | string_of_exn exn = content_of (@{make_string} exn)
14.180 +
14.181 +val exn = tagged "exn" (text string_of_exn (SOME o GENERIC))
14.182 +
14.183 +fun exn_result a =
14.184 + let
14.185 + fun enc (Exn.Res t) = (0, encode a t)
14.186 + | enc (Exn.Exn e) = (1, encode exn e)
14.187 + fun dec _ = NONE
14.188 + in variant enc dec "Exn.result" end
14.189 +
14.190 +fun triple a b c =
14.191 + tuple a (tuple b c)
14.192 + |> transform (fn (a, (b, c)) => (a, b, c)) (fn (a, b, c) => (a, (b, c)))
14.193 +
14.194 +fun either a b =
14.195 + let
14.196 + fun enc (Left l) = (0, encode a l)
14.197 + | enc (Right r) = (1, encode b r)
14.198 + fun dec 0 = SOME (decode a #> map_result Left)
14.199 + | dec 1 = SOME (decode b #> map_result Right)
14.200 + | dec _ = NONE
14.201 + in variant enc dec "either" end
14.202 +
14.203 +val sort: sort codec = list string
14.204 +val indexname: indexname codec = tuple string int
14.205 +
14.206 +fun typ () =
14.207 + let
14.208 + fun typ_type () = tuple string (list (typ ()))
14.209 + val typ_tfree = tuple string sort
14.210 + val typ_tvar = tuple indexname sort
14.211 +
14.212 + fun enc (Type arg) = (0, encode (typ_type ()) arg)
14.213 + | enc (TFree arg) = (1, encode typ_tfree arg)
14.214 + | enc (TVar arg) = (2, encode typ_tvar arg)
14.215 + fun dec 0 = SOME (decode (typ_type ()) #> map_result Type)
14.216 + | dec 1 = SOME (decode typ_tfree #> map_result TFree)
14.217 + | dec 2 = SOME (decode typ_tvar #> map_result TVar)
14.218 + | dec _ = NONE
14.219 + in variant enc dec "typ" end
14.220 +
14.221 +val typ = typ ()
14.222 +
14.223 +fun term () =
14.224 + let
14.225 + val term_const = tuple string typ
14.226 + val term_free = tuple string typ
14.227 + val term_var = tuple indexname typ
14.228 + val term_bound = int
14.229 + fun term_abs () = triple string typ (term ())
14.230 + fun term_app () = tuple (term ()) (term ())
14.231 +
14.232 + fun enc (Const arg) = (0, encode term_const arg)
14.233 + | enc (Free arg) = (1, encode term_free arg)
14.234 + | enc (Var arg) = (2, encode term_var arg)
14.235 + | enc (Bound arg) = (3, encode term_bound arg)
14.236 + | enc (Abs arg) = (4, encode (term_abs ()) arg)
14.237 + | enc (op $ arg) = (5, encode (term_app ()) arg)
14.238 + fun dec 0 = SOME (decode term_const #> map_result Const)
14.239 + | dec 1 = SOME (decode term_free #> map_result Free)
14.240 + | dec 2 = SOME (decode term_var #> map_result Var)
14.241 + | dec 3 = SOME (decode term_bound #> map_result Bound)
14.242 + | dec 4 = SOME (decode (term_abs ()) #> map_result Abs)
14.243 + | dec 5 = SOME (decode (term_app ()) #> map_result op $)
14.244 + | dec _ = NONE
14.245 + in variant enc dec "term" end
14.246 +
14.247 +val term = term ()
14.248 +
14.249 +end
14.250 +
14.251 +type 'a codec = 'a Codec.codec
14.252 \ No newline at end of file
15.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
15.2 +++ b/libisabelle-1.0.1-protocol/protocol/protocol.ML Wed Sep 04 10:17:53 2019 +0200
15.3 @@ -0,0 +1,119 @@
15.4 +signature LIBISABELLE_PROTOCOL = sig
15.5 + type name = string
15.6 + type ('i, 'o) operation =
15.7 + {from_lib : 'i codec,
15.8 + to_lib : 'o codec,
15.9 + action : 'i -> 'o}
15.10 +
15.11 + type flags = {sequential: bool, bracket: bool, auto: bool (* ignored *)}
15.12 +
15.13 + val default_flags : flags
15.14 + val join_flags : flags -> flags -> flags
15.15 + val print_flags : flags -> string
15.16 +
15.17 + val add_operation : name -> ('i, 'o) operation -> flags -> unit
15.18 + val get_operation : name -> int -> XML.tree -> XML.tree
15.19 +end
15.20 +
15.21 +structure Libisabelle_Protocol: LIBISABELLE_PROTOCOL = struct
15.22 +
15.23 +type name = string
15.24 +type ('i, 'o) operation =
15.25 + {from_lib : 'i codec,
15.26 + to_lib : 'o codec,
15.27 + action : 'i -> 'o}
15.28 +
15.29 +type flags = {sequential: bool, bracket: bool, auto: bool}
15.30 +
15.31 +val default_flags = {sequential = false, bracket = false, auto = false}
15.32 +
15.33 +fun join_flags
15.34 + {sequential = seq1, bracket = br1, auto = a1}
15.35 + {sequential = seq2, bracket = br2, auto = a2} =
15.36 + {sequential = seq1 orelse seq2, bracket = br1 orelse br2, auto = a1 orelse a2}
15.37 +
15.38 +fun print_flags {sequential, bracket, auto} =
15.39 + "({sequential=" ^ print_bool sequential ^ "," ^
15.40 + "bracket=" ^ print_bool bracket ^ "," ^
15.41 + "auto=" ^ print_bool auto ^ "})"
15.42 +
15.43 +type raw_operation = int -> XML.tree -> XML.tree
15.44 +
15.45 +exception GENERIC of string
15.46 +
15.47 +val operations =
15.48 + Synchronized.var "libisabelle.operations" (Symtab.empty: raw_operation Symtab.table)
15.49 +
15.50 +val requests =
15.51 + Synchronized.var "libisabelle.requests" (Inttab.empty: (unit -> unit) Inttab.table)
15.52 +
15.53 +fun sequentialize name f =
15.54 + let
15.55 + val var = Synchronized.var ("libisabelle." ^ name) ()
15.56 + in
15.57 + fn x => Synchronized.change_result var (fn _ => (f x, ()))
15.58 + end
15.59 +
15.60 +fun bracketize f id x =
15.61 + let
15.62 + val start = [(Markup.functionN, "libisabelle_start"), ("id", print_int id)]
15.63 + val stop = [(Markup.functionN, "libisabelle_stop"), ("id", print_int id)]
15.64 + val _ = Output.protocol_message start []
15.65 + val res = f id x
15.66 + val _ = Output.protocol_message stop []
15.67 + in res end
15.68 +
15.69 +fun add_operation name {from_lib, to_lib, action} {sequential, bracket, ...} =
15.70 + let
15.71 + fun raw _ tree =
15.72 + case Codec.decode from_lib tree of
15.73 + Codec.Success i => Codec.encode to_lib (action i)
15.74 + | Codec.Failure (msg, _) => raise Fail ("decoding input failed for operation " ^ name ^ ": " ^ msg)
15.75 + val raw' = raw
15.76 + |> (if bracket then bracketize else I)
15.77 + |> (if sequential then sequentialize name else I)
15.78 + in
15.79 + Synchronized.change operations (Symtab.update (name, raw'))
15.80 + end
15.81 +
15.82 +fun get_operation name =
15.83 + case Symtab.lookup (Synchronized.value operations) name of
15.84 + SOME operation => operation
15.85 + | NONE => fn _ => error "libisabelle: unknown command"
15.86 +
15.87 +val _ = Isabelle_Process.protocol_command "libisabelle"
15.88 + (fn id :: name :: [arg] =>
15.89 + let
15.90 + val id = parse_int id
15.91 + val response = [(Markup.functionN, "libisabelle_response"), ("id", print_int id)]
15.92 + val args = YXML.parse arg
15.93 + fun exec f =
15.94 + let
15.95 + val future = Future.fork (fn () =>
15.96 + let
15.97 + val res = Exn.interruptible_capture (fn () => f id args) ()
15.98 + val yxml = YXML.string_of (Codec.encode (Codec.exn_result Codec.id) res)
15.99 + in
15.100 + Output.protocol_message response [yxml]
15.101 + end)
15.102 + in
15.103 + Synchronized.change requests (Inttab.update_new (id, fn () => Future.cancel future))
15.104 + end
15.105 + in
15.106 + exec (get_operation name)
15.107 + end)
15.108 +
15.109 +val _ = Isabelle_Process.protocol_command "libisabelle_cancel"
15.110 + (fn ids =>
15.111 + let
15.112 + fun remove id tab = (Inttab.lookup tab id, Inttab.delete_safe id tab)
15.113 + val _ =
15.114 + map parse_int ids
15.115 + |> fold_map remove
15.116 + |> Synchronized.change_result requests
15.117 + |> map (fn NONE => () | SOME f => f ())
15.118 + in
15.119 + ()
15.120 + end)
15.121 +
15.122 +end
16.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
16.2 +++ b/libisabelle-1.0.1-protocol/protocol/ref_table.ML Wed Sep 04 10:17:53 2019 +0200
16.3 @@ -0,0 +1,31 @@
16.4 +signature REF_TABLE = sig
16.5 + type t
16.6 + val read: serial -> t
16.7 + val write: serial -> t -> unit
16.8 + val delete: serial -> unit
16.9 +
16.10 + (* internal *)
16.11 + val peek: unit -> t Inttab.table
16.12 +end
16.13 +
16.14 +signature REF_TABLE_ARGS = sig
16.15 + type t
16.16 + val name: string
16.17 +end
16.18 +
16.19 +functor Ref_Table(Args : REF_TABLE_ARGS) : REF_TABLE where type t = Args.t = struct
16.20 +
16.21 +type t = Args.t
16.22 +
16.23 +type table = t Inttab.table
16.24 +val empty_table : table = Inttab.empty
16.25 +
16.26 +val table = Synchronized.var ("Ref_Table." ^ Args.name) empty_table
16.27 +
16.28 +fun read ser = the (Inttab.lookup (Synchronized.value table) ser)
16.29 +fun write ser t = Synchronized.change table (Inttab.update (ser, t))
16.30 +val delete = Synchronized.change table o Inttab.delete
16.31 +
16.32 +fun peek () = Synchronized.value table
16.33 +
16.34 +end
17.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
17.2 +++ b/libisabelle-1.0.1-protocol/protocol/typed_eval.ML Wed Sep 04 10:17:53 2019 +0200
17.3 @@ -0,0 +1,38 @@
17.4 +signature TYPED_EVAL = sig
17.5 + type T
17.6 + val eval: Input.source -> Proof.context -> T
17.7 +
17.8 + val fulfill: T -> Context.generic -> Context.generic (* internal *)
17.9 +end
17.10 +
17.11 +signature TYPED_EVAL_ARGS = sig
17.12 + type T
17.13 + val typ: string
17.14 + val name: string
17.15 +end
17.16 +
17.17 +functor Typed_Eval(Args : TYPED_EVAL_ARGS) : TYPED_EVAL = struct
17.18 +
17.19 +structure Data = Generic_Data
17.20 +(
17.21 + type T = Args.T option
17.22 + val empty = NONE
17.23 + val extend = I
17.24 + fun merge (NONE, NONE) = NONE
17.25 + | merge _ = error "Typed_Eval.Data.merge: can't merge"
17.26 +)
17.27 +
17.28 +type T = Args.T
17.29 +
17.30 +val fulfill = Data.map o K o SOME
17.31 +
17.32 +fun eval source ctxt =
17.33 + ML_Context.expression (Input.range_of source)
17.34 + "typed_eval_result" Args.typ
17.35 + (Args.name ^ ".fulfill typed_eval_result")
17.36 + (ML_Lex.read_source false source)
17.37 + (Context.Proof ctxt)
17.38 + |> Data.get
17.39 + |> the
17.40 +
17.41 +end
17.42 \ No newline at end of file
18.1 --- a/src/Tools/isac/MathEngine/MathEngine.thy Tue Sep 03 17:43:42 2019 +0200
18.2 +++ b/src/Tools/isac/MathEngine/MathEngine.thy Wed Sep 04 10:17:53 2019 +0200
18.3 @@ -4,7 +4,8 @@
18.4 *)
18.5
18.6 theory MathEngine
18.7 -imports "~~/src/Tools/isac/Interpret/Interpret"
18.8 + imports "~~/src/Tools/isac/Interpret/Interpret"
18.9 +
18.10 begin
18.11 ML_file solve.sml
18.12 ML_file "mathengine-stateless.sml"
19.1 --- a/src/Tools/isac/ROOT Tue Sep 03 17:43:42 2019 +0200
19.2 +++ b/src/Tools/isac/ROOT Wed Sep 04 10:17:53 2019 +0200
19.3 @@ -15,14 +15,14 @@
19.4
19.5 (* run "./bin/isabelle build -v -b Isac" *)
19.6 session Isac in "~~/src/Tools/isac" = HOL +
19.7 - description {*
19.8 + description \<open>
19.9 Isac core, prototype of a math-engine and knowledge
19.10 for a TP-based educational mathematics assistant.
19.11
19.12 - The java front-end is under development at TU Graz and at FH Hagenberg,
19.13 + The java front-end is under development at FH Hagenberg,
19.14 the Isabelle/ML math-engine and Isabelle knowledge at RISC Linz.
19.15 See http://www.ist.tugraz.at/isac/.
19.16 - *}
19.17 + \<close>
19.18 options [document = false (*, browser_info = true*)]
19.19 sessions
19.20 Protocol (* Codec.encode etc required in mathml.sml only *)
19.21 @@ -34,15 +34,15 @@
19.22 or just "./bin/isabelle jedit -l libisabelle_Isac & "
19.23 *)
19.24 session libisabelle_Isac in "~~/src/Tools/isac" = HOL +
19.25 - description {*
19.26 + description \<open>
19.27 Isac core, prototype of a math-engine and knowledge for engineering math
19.28 + libisabelle by Lars Hupel as interface to the java front-end:
19.29 https://github.com/larsrh/libisabelle
19.30
19.31 - The java front-end is under development at TU Graz and at FH Hagenberg,
19.32 + The java front-end is under development at at FH Hagenberg,
19.33 the Isabelle/ML math-engine and Isabelle knowledge at RISC Linz.
19.34 See http://www.ist.tugraz.at/isac/.
19.35 - *}
19.36 + \<close>
19.37 options [document = false (*, browser_info = true*)]
19.38 sessions
19.39 Isac