1.1 --- a/ROOTS Wed Sep 04 10:17:53 2019 +0200
1.2 +++ b/ROOTS Tue Sep 10 10:47:18 2019 +0200
1.3 @@ -11,5 +11,4 @@
1.4 src/Doc
1.5 src/Tools
1.6 src/Tools/isac
1.7 -libisabelle-1.0.1-protocol
1.8 test/Tools/isac/ADDTESTS/session-get_theory/
1.9 \ No newline at end of file
2.1 --- a/libisabelle-1.0.1-protocol/Protocol_Main.thy Wed Sep 04 10:17:53 2019 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,9 +0,0 @@
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 --- a/libisabelle-1.0.1-protocol/Protocol_Pure.thy Wed Sep 04 10:17:53 2019 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,8 +0,0 @@
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 --- a/libisabelle-1.0.1-protocol/ROOT Wed Sep 04 10:17:53 2019 +0200
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,13 +0,0 @@
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 --- a/libisabelle-1.0.1-protocol/operations/Basic.thy Wed Sep 04 10:17:53 2019 +0200
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,11 +0,0 @@
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 --- a/libisabelle-1.0.1-protocol/operations/HOL_Operations.thy Wed Sep 04 10:17:53 2019 +0200
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,24 +0,0 @@
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 --- a/libisabelle-1.0.1-protocol/operations/ML_Expr.thy Wed Sep 04 10:17:53 2019 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,41 +0,0 @@
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 --- a/libisabelle-1.0.1-protocol/operations/ml_expr.ML Wed Sep 04 10:17:53 2019 +0200
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,132 +0,0 @@
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 --- a/libisabelle-1.0.1-protocol/operations/refs.ML Wed Sep 04 10:17:53 2019 +0200
9.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
9.3 @@ -1,7 +0,0 @@
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 --- a/libisabelle-1.0.1-protocol/protocol/Codec_Class.thy Wed Sep 04 10:17:53 2019 +0200
10.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
10.3 @@ -1,21 +0,0 @@
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 --- a/libisabelle-1.0.1-protocol/protocol/Codec_Test.thy Wed Sep 04 10:17:53 2019 +0200
11.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
11.3 @@ -1,41 +0,0 @@
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 --- a/libisabelle-1.0.1-protocol/protocol/Common.thy Wed Sep 04 10:17:53 2019 +0200
12.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
12.3 @@ -1,80 +0,0 @@
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 --- a/libisabelle-1.0.1-protocol/protocol/Protocol.thy Wed Sep 04 10:17:53 2019 +0200
13.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
13.3 @@ -1,54 +0,0 @@
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 --- a/libisabelle-1.0.1-protocol/protocol/codec.ML Wed Sep 04 10:17:53 2019 +0200
14.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
14.3 @@ -1,248 +0,0 @@
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 --- a/libisabelle-1.0.1-protocol/protocol/protocol.ML Wed Sep 04 10:17:53 2019 +0200
15.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
15.3 @@ -1,119 +0,0 @@
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 --- a/libisabelle-1.0.1-protocol/protocol/ref_table.ML Wed Sep 04 10:17:53 2019 +0200
16.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
16.3 @@ -1,31 +0,0 @@
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 --- a/libisabelle-1.0.1-protocol/protocol/typed_eval.ML Wed Sep 04 10:17:53 2019 +0200
17.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
17.3 @@ -1,38 +0,0 @@
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/BridgeLibisabelle/BridgeLibisabelle.thy Wed Sep 04 10:17:53 2019 +0200
18.2 +++ b/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy Tue Sep 10 10:47:18 2019 +0200
18.3 @@ -4,15 +4,15 @@
18.4 *)
18.5
18.6 theory BridgeLibisabelle
18.7 - imports "~~/src/Tools/isac/MathEngine/MathEngine" Protocol.Protocol
18.8 + imports "~~/src/Tools/isac/MathEngine/MathEngine"
18.9
18.10 begin
18.11 ML_file mathml.sml
18.12 ML_file datatypes.sml
18.13 ML_file "pbl-met-hierarchy.sml"
18.14 ML_file "thy-hierarchy.sml"
18.15 - ML_file "interface-xml.sml"
18.16 - ML_file interface.sml
18.17 +(*ML_file "interface-xml.sml" --- rm libisabelle ---*)
18.18 +(*ML_file interface.sml --- rm libisabelle ---*)
18.19 (*declare [[ML_print_depth = 999]]*)
18.20 ML \<open>
18.21 \<close> ML \<open>
19.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Wed Sep 04 10:17:53 2019 +0200
19.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Tue Sep 10 10:47:18 2019 +0200
19.3 @@ -288,6 +288,7 @@
19.4
19.5 (** general types: lists, **)
19.6
19.7 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
19.8 fun xml_of_bool b = XML.Elem (("BOOL", []), [XML.Text (bool2str b)])
19.9 fun xml_to_bool (XML.Elem (("BOOL", []), [XML.Text b])) = string_to_bool b
19.10 | xml_to_bool tree = raise ERROR ("xml_to_bool: wrong XML.tree \n" ^ xmlstr 0 tree)
19.11 @@ -338,6 +339,7 @@
19.12 | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteSubpbl"])) = Solve.CompleteSubpbl
19.13 | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteCalc"])) = Solve.CompleteCalc
19.14 | xml_to_auto tree = raise ERROR ("xml_to_auto: wrong XML.tree \n" ^ xmlstr 0 tree)
19.15 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
19.16
19.17 fun filterpbl str =
19.18 let fun filt [] = []
19.19 @@ -345,6 +347,7 @@
19.20 if str = s then (t1 $ t2) :: filt ps else filt ps
19.21 in filt end;
19.22
19.23 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
19.24 fun xml_of_itm_ (Model.Cor (dts, _)) =
19.25 XML.Elem (("ITEM", [("status", "correct")]), [xml_of_term (Model.comp_dts' dts)])
19.26 | xml_of_itm_ (Model.Syn c) =
19.27 @@ -464,12 +467,14 @@
19.28 (XML.Elem (("SUBSTITUTION", []),
19.29 xml_var_val_pairs)) = Selem.subst2sube (map xml_to_sub xml_var_val_pairs)
19.30 | xml_to_sube x = raise ERROR ("xml_to_sube wrong arg: " ^ xmlstr 0 x)
19.31 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
19.32
19.33 fun thm''2xml j (thm : thm) =
19.34 indt j ^ "<THEOREM>\n" ^
19.35 indt (j+i) ^ "<ID> " ^ Celem.thmID_of_derivation_name' thm ^ " </ID>\n"^
19.36 term2xml j (Thm.prop_of thm) ^ "\n" ^
19.37 indt j ^ "</THEOREM>\n";
19.38 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
19.39 fun xml_of_thm' (ID, form) =
19.40 XML.Elem (("THEOREM", []), [
19.41 XML.Elem (("ID", []), [XML.Text ID]),
19.42 @@ -659,6 +664,7 @@
19.43 XML.Elem (("ASMEVALUATED", []),[
19.44 XML.Elem (("ASM", []), [xml_of_term asm]),
19.45 XML.Elem (("VALUE", []), [xml_of_term vl])])
19.46 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
19.47
19.48 (*.a reference to an element in the theory hierarchy;
19.49 compare 'fun keref2xml'.*)
19.50 @@ -674,6 +680,7 @@
19.51 indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
19.52 indt j ^ "</KESTOREREF>\n"
19.53 end;
19.54 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
19.55 fun xml_of_theref thyid typ xstring =
19.56 let
19.57 val guh = Celem.theID2guh ["IsacKnowledge", thyid, typ, xstring]
19.58 @@ -784,6 +791,7 @@
19.59
19.60 (* for checking output at Frontend *)
19.61 fun cut_xml xml i = xml |> xmlstr 0 |> Symbol.explode |> curry take i |> implode
19.62 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
19.63 (*------------------------------------------------------------------
19.64 end
19.65 open datatypes;
20.1 --- a/src/Tools/isac/BridgeLibisabelle/mathml.sml Wed Sep 04 10:17:53 2019 +0200
20.2 +++ b/src/Tools/isac/BridgeLibisabelle/mathml.sml Tue Sep 10 10:47:18 2019 +0200
20.3 @@ -41,6 +41,7 @@
20.4
20.5 val indentation = 2;
20.6
20.7 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
20.8 local
20.9 fun indent i = fold (curry op ^) (replicate i ". ") ""
20.10 in
20.11 @@ -61,6 +62,7 @@
20.12 | xmlstr _ (XML.Elem ((_, (_ :: _)), _)) =
20.13 error "xmlstr: TODO review attribute \"status\" etc";
20.14 end
20.15 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
20.16
20.17 fun strs2xml strs = foldl (op ^) ("", strs);
20.18 (* writeln (strs2xml ["<XXX> xxx </XXX>\n","<YYY> yyy </YYY>\n"]);
20.19 @@ -80,6 +82,7 @@
20.20 <MATHML>
20.21 <ISA> equality e_ </ISA>
20.22 <MATHML> *)
20.23 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
20.24 fun xml_of_term t =
20.25 XML.Elem (("MATHML", []),
20.26 [XML.Elem (("ISA", []), [XML.Text ((decode o Rule.term2str) t)])])
20.27 @@ -106,6 +109,7 @@
20.28 XML.Elem (("ISA", []), [XML.Text _]),
20.29 XML.Elem (("TERM", []), [xt])]))) = xt |> Codec.decode Codec.term |> Codec.the_success
20.30 | xml_to_term_UNUSED xx = raise ERROR ("xml_to_term_NEW wrong arg: " ^ xmlstr 0 xx)
20.31 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
20.32
20.33 (*version for TextIO*)
20.34 fun terms2xml j [] = ""
20.35 @@ -120,6 +124,7 @@
20.36 indt (j+i) ^ "<MATHML>\n" ^
20.37 indt (j+2*i) ^ "<ISA> " ^ ct ^ " </ISA>\n" ^
20.38 indt (j+i) ^ "</MATHML>\n";
20.39 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
20.40 fun xml_of_cterm ct =
20.41 XML.Elem (("MATHML", []),
20.42 [XML.Elem (("ISA", []), [XML.Text ct])])
20.43 @@ -127,6 +132,7 @@
20.44 (XML.Elem (("MATHML", []),
20.45 [XML.Elem (("ISA", []), [XML.Text ct])])) = ct
20.46 | xml_to_cterm x = raise ERROR ("xml_to_cterm wrong arg: " ^ xmlstr 0 x)
20.47 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
20.48
20.49 (*version for TextIO*)
20.50 fun cterms2xml j [] = ""
21.1 --- a/src/Tools/isac/Build_Isac.thy Wed Sep 04 10:17:53 2019 +0200
21.2 +++ b/src/Tools/isac/Build_Isac.thy Tue Sep 10 10:47:18 2019 +0200
21.3 @@ -69,13 +69,10 @@
21.4 ML_file "thy-hierarchy.sml"
21.5 ML_file "interface-xml.sml"
21.6 ML_file interface.sml
21.7 -*) "BridgeLibisabelle/BridgeLibisabelle"
21.8 + "BridgeLibisabelle/BridgeLibisabelle"
21.9 +*)
21.10
21.11 - "Knowledge/Build_Thydata" (*imports Isac.thy etc*)
21.12 -
21.13 - (* the Protocol for the connection isac-java -- Isabelle/Isac is built separately:
21.14 - here we partly check consistency libisabelle/Isac -- Isabelle/Isac: *)
21.15 - Protocol.Protocol
21.16 + "Knowledge/Build_Thydata" (*imports Isac.thy etc*)
21.17
21.18 (*//-----------------------------------------------------------------------------------------\\*)
21.19 (*\\-----------------------------------------------------------------------------------------//*)
22.1 --- a/src/Tools/isac/ROOT Wed Sep 04 10:17:53 2019 +0200
22.2 +++ b/src/Tools/isac/ROOT Tue Sep 10 10:47:18 2019 +0200
22.3 @@ -24,27 +24,5 @@
22.4 See http://www.ist.tugraz.at/isac/.
22.5 \<close>
22.6 options [document = false (*, browser_info = true*)]
22.7 - sessions
22.8 - Protocol (* Codec.encode etc required in mathml.sml only *)
22.9 theories
22.10 Build_Isac
22.11 -
22.12 -(* run "./bin/isabelle build -v -b Protocol" (* generates Classy, too *)
22.13 - "./bin/isabelle build -v -b libisabelle_Isac"
22.14 -or just "./bin/isabelle jedit -l libisabelle_Isac & "
22.15 -*)
22.16 -session libisabelle_Isac in "~~/src/Tools/isac" = HOL +
22.17 - description \<open>
22.18 - Isac core, prototype of a math-engine and knowledge for engineering math
22.19 - + libisabelle by Lars Hupel as interface to the java front-end:
22.20 - https://github.com/larsrh/libisabelle
22.21 -
22.22 - The java front-end is under development at at FH Hagenberg,
22.23 - the Isabelle/ML math-engine and Isabelle knowledge at RISC Linz.
22.24 - See http://www.ist.tugraz.at/isac/.
22.25 - \<close>
22.26 - options [document = false (*, browser_info = true*)]
22.27 - sessions
22.28 - Isac
22.29 - theories
22.30 - Isac_Protocol