1.1 --- a/ROOTS Thu Jan 21 17:29:33 2016 +0100
1.2 +++ b/ROOTS Fri Jan 22 15:53:13 2016 +0100
1.3 @@ -12,6 +12,3 @@
1.4 src/Tools
1.5 src/Tools/isac
1.6 test/Tools/isac/ADDTESTS/session-get_theory/
1.7 -libisabelle-protocol/isabelle-2015/lib/classy
1.8 -libisabelle-protocol/isabelle-2015
1.9 -libisabelle-protocol/isabelle-common
1.10 \ No newline at end of file
2.1 --- a/libisabelle-protocol/README.md Thu Jan 21 17:29:33 2016 +0100
2.2 +++ b/libisabelle-protocol/README.md Fri Jan 22 15:53:13 2016 +0100
2.3 @@ -1,7 +1,2 @@
2.4 # libisabelle-protocol
2.5 Isabelle backend for the libisabelle protocol
2.6 -
2.7 -# WN151217
2.8 -cloned from
2.9 -https://github.com/larsrh/libisabelle-protocol/commit/c33db5fef8af6548c494705e55e6b56e976a10a9
2.10 -and copied here without .git* and without isabelle-2014
2.11 \ No newline at end of file
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/libisabelle-protocol/common/Codec_Test.thy Fri Jan 22 15:53:13 2016 +0100
3.3 @@ -0,0 +1,36 @@
3.4 +theory Codec_Test
3.5 +imports Common "~~/src/Tools/Spec_Check/Spec_Check"
3.6 +begin
3.7 +
3.8 +ML\<open>
3.9 +fun check_for str =
3.10 + let
3.11 + val prop =
3.12 + "ALL x. (let val c = (" ^ str ^ ") in Codec.decode c (Codec.encode c x) = Codec.Success x end)"
3.13 + in check_property prop end
3.14 +
3.15 +fun gen_unit r =
3.16 + ((), r)
3.17 +\<close>
3.18 +
3.19 +ML_command\<open>
3.20 + check_for "Codec.unit";
3.21 + check_for "Codec.int";
3.22 + check_for "Codec.bool";
3.23 + check_for "Codec.string";
3.24 + check_for "Codec.tuple Codec.int Codec.int";
3.25 + check_for "Codec.tuple Codec.string Codec.unit";
3.26 + check_for "Codec.list Codec.unit";
3.27 + check_for "Codec.list Codec.int";
3.28 + check_for "Codec.list Codec.string";
3.29 + check_for "Codec.list (Codec.list Codec.string)";
3.30 + check_for "Codec.list (Codec.tuple Codec.int Codec.int)";
3.31 + check_for "Codec.tuple Codec.int (Codec.list Codec.int)";
3.32 + check_for "Codec.option Codec.int";
3.33 + check_for "Codec.option (Codec.list Codec.int)";
3.34 + check_for "Codec.list (Codec.option (Codec.int))";
3.35 + check_for "Codec.term";
3.36 + check_for "Codec.typ";
3.37 +\<close>
3.38 +
3.39 +end
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/libisabelle-protocol/common/Common.thy Fri Jan 22 15:53:13 2016 +0100
4.3 @@ -0,0 +1,8 @@
4.4 +theory Common
4.5 +imports Pure
4.6 +begin
4.7 +
4.8 +ML_file "codec.ML"
4.9 +ML_file "protocol.ML"
4.10 +
4.11 +end
4.12 \ No newline at end of file
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/libisabelle-protocol/common/codec.ML Fri Jan 22 15:53:13 2016 +0100
5.3 @@ -0,0 +1,242 @@
5.4 +signature CODEC = sig
5.5 + datatype 'a result = Success of 'a | Failure of string * XML.body
5.6 + datatype ('a, 'b) either = Left of 'a | Right of 'b
5.7 + type 'a codec
5.8 +
5.9 + val the_success: 'a result -> 'a
5.10 +
5.11 + val map_result: ('a -> 'b) -> 'a result -> 'b result
5.12 + val bind_result: ('a -> 'b result) -> 'a result -> 'b result
5.13 + val sequence_results: 'a result list -> 'a list result
5.14 + val traverse_results: ('a -> 'b result) -> 'a list -> 'b list result
5.15 +
5.16 + val transform: ('a -> 'b) -> ('b -> 'a) -> 'a codec -> 'b codec
5.17 + val encode: 'a codec -> 'a -> XML.tree
5.18 + val decode: 'a codec -> XML.tree -> 'a result
5.19 +
5.20 + val basic: {encode: 'a -> XML.tree, decode: XML.tree -> 'a result} -> 'a codec
5.21 +
5.22 + val variant: ('a -> (int * XML.tree)) -> (int -> (XML.tree -> 'a result) option) -> string -> 'a codec
5.23 + val tagged: string -> 'a codec -> 'a codec
5.24 +
5.25 + val unit: unit codec
5.26 + val bool: bool codec
5.27 + val string: string codec
5.28 + val int: int codec
5.29 + val list: 'a codec -> 'a list codec
5.30 + val tuple: 'a codec -> 'b codec -> ('a * 'b) codec
5.31 + val triple: 'a codec -> 'b codec -> 'c codec -> ('a * 'b * 'c) codec
5.32 + val either: 'a codec -> 'b codec -> ('a, 'b) either codec
5.33 + val option: 'a codec -> 'a option codec
5.34 + val tree: XML.tree codec
5.35 +
5.36 + val sort: sort codec
5.37 + val typ: typ codec
5.38 + val term: term codec
5.39 +
5.40 + exception GENERIC of string
5.41 + val exn: exn codec
5.42 + val exn_result: 'a codec -> 'a Exn.result codec
5.43 +
5.44 + val id: XML.tree codec (* internal *)
5.45 +end
5.46 +
5.47 +structure Codec: CODEC = struct
5.48 +
5.49 +datatype 'a result = Success of 'a | Failure of string * XML.body
5.50 +datatype ('a, 'b) either = Left of 'a | Right of 'b
5.51 +
5.52 +fun map_result f (Success a) = Success (f a)
5.53 + | map_result _ (Failure (msg, body)) = Failure (msg, body)
5.54 +
5.55 +fun bind_result f (Success a) = f a
5.56 + | bind_result _ (Failure (msg, body)) = Failure (msg, body)
5.57 +
5.58 +fun traverse_results _ [] = Success []
5.59 + | traverse_results f (x :: xs) =
5.60 + case f x of
5.61 + Success y => map_result (fn ys => y :: ys) (traverse_results f xs)
5.62 + | Failure (msg, body) => Failure (msg, body)
5.63 +
5.64 +fun sequence_results xs = traverse_results I xs
5.65 +
5.66 +fun the_success (Success a) = a
5.67 + | the_success _ = raise Fail "unexpected failure"
5.68 +
5.69 +fun add_tag tag idx body =
5.70 + let
5.71 + val attrs = case idx of SOME i => [("idx", XML.Encode.int_atom i)] | _ => []
5.72 + in XML.Elem (("tag", ("type", tag) :: attrs), body) end
5.73 +
5.74 +fun expect_tag tag tree =
5.75 + case tree of
5.76 + XML.Elem (("tag", [("type", tag')]), body) =>
5.77 + if tag = tag' then
5.78 + Success body
5.79 + else
5.80 + Failure ("tag mismatch: expected " ^ tag ^ ", got " ^ tag', [tree])
5.81 + | _ =>
5.82 + Failure ("tag " ^ tag ^ " expected", [tree])
5.83 +
5.84 +fun expect_tag' tag tree =
5.85 + case tree of
5.86 + XML.Elem (("tag", [("type", tag'), ("idx", i)]), body) =>
5.87 + if tag = tag' then
5.88 + Success (XML.Decode.int_atom i, body)
5.89 + handle XML.XML_ATOM err => Failure (err, [tree])
5.90 + else
5.91 + Failure ("tag mismatch: expected " ^ tag ^ ", got " ^ tag', [tree])
5.92 + | _ =>
5.93 + Failure ("indexed tag " ^ tag ^ " expected", [tree])
5.94 +
5.95 +
5.96 +abstype 'a codec = Codec of {encode: 'a -> XML.tree, decode: XML.tree -> 'a result} with
5.97 +
5.98 +val basic = Codec
5.99 +
5.100 +fun encode (Codec {encode, ...}) = encode
5.101 +fun decode (Codec {decode, ...}) = decode
5.102 +
5.103 +fun transform f g (Codec {encode, decode}) = Codec
5.104 + {encode = g #> encode,
5.105 + decode = decode #> map_result f}
5.106 +
5.107 +fun list a = Codec
5.108 + {encode = map (encode a) #> add_tag "list" NONE,
5.109 + decode = expect_tag "list" #> bind_result (traverse_results (decode a))}
5.110 +
5.111 +fun tuple a b = Codec
5.112 + {encode = (fn (x, y) => add_tag "tuple" NONE [encode a x, encode b y]),
5.113 + decode = expect_tag "tuple" #> bind_result (fn body =>
5.114 + case body of
5.115 + [x, y] => decode a x |> bind_result (fn x' => decode b y |> map_result (pair x'))
5.116 + | _ => Failure ("invalid structure", body))}
5.117 +
5.118 +fun variant enc dec tag = Codec
5.119 + {encode = (fn a => let val (idx, tree) = enc a in add_tag tag (SOME idx) [tree] end),
5.120 + decode = (fn tree => expect_tag' tag tree |> bind_result (fn (idx, body) =>
5.121 + case (body, dec idx) of
5.122 + ([tree'], SOME res) => res tree'
5.123 + | (_, SOME _) => Failure ("invalid structure", [tree])
5.124 + | (_, NONE) => Failure ("invalid index " ^ Markup.print_int idx, [tree])))}
5.125 +
5.126 +fun tagged tag a = Codec
5.127 + {encode = encode a #> single #> add_tag tag NONE,
5.128 + decode = expect_tag tag #> bind_result (fn body =>
5.129 + case body of
5.130 + [tree] => decode a tree
5.131 + | _ => Failure ("invalid structure", body))}
5.132 +
5.133 +val unit = Codec
5.134 + {encode = K (add_tag "unit" NONE []),
5.135 + decode = expect_tag "unit" #> bind_result (fn body =>
5.136 + case body of
5.137 + [] => Success ()
5.138 + | _ => Failure ("expected nothing", body))}
5.139 +
5.140 +fun text to from = Codec
5.141 + {encode = XML.Text o to,
5.142 + decode =
5.143 + (fn tree as XML.Text content =>
5.144 + (case from content of
5.145 + NONE => Failure ("decoding failed", [tree]) |
5.146 + SOME a => Success a)
5.147 + | tree => Failure ("expected text tree", [tree]))}
5.148 +
5.149 +val id = Codec {encode = I, decode = Success}
5.150 +
5.151 +end
5.152 +
5.153 +val int = tagged "int" (text Markup.print_int (Exn.get_res o Exn.capture Markup.parse_int))
5.154 +val bool = tagged "bool" (text Markup.print_bool (Exn.get_res o Exn.capture Markup.parse_bool))
5.155 +val string = tagged "string" (text I SOME)
5.156 +
5.157 +val tree = tagged "XML.tree" id
5.158 +
5.159 +fun option a =
5.160 + let
5.161 + fun enc (SOME x) = (0, encode a x)
5.162 + | enc NONE = (1, encode unit ())
5.163 + fun dec 0 = SOME (decode a #> map_result SOME)
5.164 + | dec 1 = SOME (decode unit #> map_result (K NONE))
5.165 + | dec _ = NONE
5.166 + in variant enc dec "option" end
5.167 +
5.168 +val content_of =
5.169 + XML.content_of o YXML.parse_body
5.170 +
5.171 +(* slightly fishy codec, doesn't preserve exception type *)
5.172 +exception GENERIC of string
5.173 +val exn = tagged "exn" (text (fn exn => (content_of (@{make_string} exn))) (SOME o GENERIC))
5.174 +
5.175 +fun exn_result a =
5.176 + let
5.177 + fun enc (Exn.Res t) = (0, encode a t)
5.178 + | enc (Exn.Exn e) = (1, encode exn e)
5.179 + fun dec 0 = SOME (decode a #> map_result Exn.Res)
5.180 + | dec 1 = SOME (decode exn #> map_result Exn.Exn)
5.181 + | dec _ = NONE
5.182 + in variant enc dec "Exn.result" end
5.183 +
5.184 +fun triple a b c =
5.185 + tuple a (tuple b c)
5.186 + |> transform (fn (a, (b, c)) => (a, b, c)) (fn (a, b, c) => (a, (b, c)))
5.187 +
5.188 +fun either a b =
5.189 + let
5.190 + fun enc (Left l) = (0, encode a l)
5.191 + | enc (Right r) = (1, encode b r)
5.192 + fun dec 0 = SOME (decode a #> map_result Left)
5.193 + | dec 1 = SOME (decode b #> map_result Right)
5.194 + | dec _ = NONE
5.195 + in variant enc dec "either" end
5.196 +
5.197 +val sort: sort codec = list string
5.198 +val indexname: indexname codec = tuple string int
5.199 +
5.200 +fun typ () =
5.201 + let
5.202 + fun typ_type () = tuple string (list (typ ()))
5.203 + val typ_tfree = tuple string sort
5.204 + val typ_tvar = tuple indexname sort
5.205 +
5.206 + fun enc (Type arg) = (0, encode (typ_type ()) arg)
5.207 + | enc (TFree arg) = (1, encode typ_tfree arg)
5.208 + | enc (TVar arg) = (2, encode typ_tvar arg)
5.209 + fun dec 0 = SOME (decode (typ_type ()) #> map_result Type)
5.210 + | dec 1 = SOME (decode typ_tfree #> map_result TFree)
5.211 + | dec 2 = SOME (decode typ_tvar #> map_result TVar)
5.212 + | dec _ = NONE
5.213 + in variant enc dec "Pure.typ" end
5.214 +
5.215 +val typ = typ ()
5.216 +
5.217 +fun term () =
5.218 + let
5.219 + val term_const = tuple string typ
5.220 + val term_free = tuple string typ
5.221 + val term_var = tuple indexname typ
5.222 + val term_bound = int
5.223 + fun term_abs () = triple string typ (term ())
5.224 + fun term_app () = tuple (term ()) (term ())
5.225 +
5.226 + fun enc (Const arg) = (0, encode term_const arg)
5.227 + | enc (Free arg) = (1, encode term_free arg)
5.228 + | enc (Var arg) = (2, encode term_var arg)
5.229 + | enc (Bound arg) = (3, encode term_bound arg)
5.230 + | enc (Abs arg) = (4, encode (term_abs ()) arg)
5.231 + | enc (op $ arg) = (5, encode (term_app ()) arg)
5.232 + fun dec 0 = SOME (decode term_const #> map_result Const)
5.233 + | dec 1 = SOME (decode term_free #> map_result Free)
5.234 + | dec 2 = SOME (decode term_var #> map_result Var)
5.235 + | dec 3 = SOME (decode term_bound #> map_result Bound)
5.236 + | dec 4 = SOME (decode (term_abs ()) #> map_result Abs)
5.237 + | dec 5 = SOME (decode (term_app ()) #> map_result op $)
5.238 + | dec _ = NONE
5.239 + in variant enc dec "Pure.term" end
5.240 +
5.241 +val term = term ()
5.242 +
5.243 +end
5.244 +
5.245 +type 'a codec = 'a Codec.codec
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/libisabelle-protocol/common/protocol.ML Fri Jan 22 15:53:13 2016 +0100
6.3 @@ -0,0 +1,119 @@
6.4 +signature PROTOCOL = sig
6.5 + type name = string
6.6 + type ('i, 'o) operation =
6.7 + {from_lib : 'i codec,
6.8 + to_lib : 'o codec,
6.9 + action : 'i -> 'o}
6.10 +
6.11 + type flags = {sequential: bool, bracket: bool, auto: bool (* ignored *)}
6.12 +
6.13 + val default_flags : flags
6.14 + val join_flags : flags -> flags -> flags
6.15 + val print_flags : flags -> string
6.16 +
6.17 + val add_operation : name -> ('i, 'o) operation -> flags -> unit
6.18 + val get_operation : name -> int -> XML.tree -> XML.tree
6.19 +end
6.20 +
6.21 +structure Protocol: PROTOCOL = struct
6.22 +
6.23 +type name = string
6.24 +type ('i, 'o) operation =
6.25 + {from_lib : 'i codec,
6.26 + to_lib : 'o codec,
6.27 + action : 'i -> 'o}
6.28 +
6.29 +type flags = {sequential: bool, bracket: bool, auto: bool}
6.30 +
6.31 +val default_flags = {sequential = false, bracket = false, auto = false}
6.32 +
6.33 +fun join_flags
6.34 + {sequential = seq1, bracket = br1, auto = a1}
6.35 + {sequential = seq2, bracket = br2, auto = a2} =
6.36 + {sequential = seq1 orelse seq2, bracket = br1 orelse br2, auto = a1 orelse a2}
6.37 +
6.38 +fun print_flags {sequential, bracket, auto} =
6.39 + "({sequential=" ^ Markup.print_bool sequential ^ "," ^
6.40 + "bracket=" ^ Markup.print_bool bracket ^ "," ^
6.41 + "auto=" ^ Markup.print_bool auto ^ "})"
6.42 +
6.43 +type raw_operation = int -> XML.tree -> XML.tree
6.44 +
6.45 +exception GENERIC of string
6.46 +
6.47 +val operations =
6.48 + Synchronized.var "libisabelle.operations" (Symtab.empty: raw_operation Symtab.table)
6.49 +
6.50 +val requests =
6.51 + Synchronized.var "libisabelle.requests" (Inttab.empty: (unit -> unit) Inttab.table)
6.52 +
6.53 +fun sequentialize name f =
6.54 + let
6.55 + val var = Synchronized.var ("libisabelle." ^ name) ()
6.56 + in
6.57 + fn x => Synchronized.change_result var (fn _ => (f x, ()))
6.58 + end
6.59 +
6.60 +fun bracketize f id x =
6.61 + let
6.62 + val start = [(Markup.functionN, "libisabelle_start"), ("id", Markup.print_int id)]
6.63 + val stop = [(Markup.functionN, "libisabelle_stop"), ("id", Markup.print_int id)]
6.64 + val _ = Output.protocol_message start []
6.65 + val res = f id x
6.66 + val _ = Output.protocol_message stop []
6.67 + in res end
6.68 +
6.69 +fun add_operation name {from_lib, to_lib, action} {sequential, bracket, ...} =
6.70 + let
6.71 + fun raw _ tree =
6.72 + case Codec.decode from_lib tree of
6.73 + Codec.Success i => Codec.encode to_lib (action i)
6.74 + | Codec.Failure (msg, _) => raise Fail ("decoding input failed for operation " ^ name ^ ": " ^ msg)
6.75 + val raw' = raw
6.76 + |> (if bracket then bracketize else I)
6.77 + |> (if sequential then sequentialize name else I)
6.78 + in
6.79 + Synchronized.change operations (Symtab.update (name, raw'))
6.80 + end
6.81 +
6.82 +fun get_operation name =
6.83 + case Symtab.lookup (Synchronized.value operations) name of
6.84 + SOME operation => operation
6.85 + | NONE => fn _ => raise Fail "libisabelle: unknown command"
6.86 +
6.87 +val _ = Isabelle_Process.protocol_command "libisabelle"
6.88 + (fn id :: name :: [arg] =>
6.89 + let
6.90 + val id = Markup.parse_int id
6.91 + val response = [(Markup.functionN, "libisabelle_response"), ("id", Markup.print_int id)]
6.92 + val args = YXML.parse arg
6.93 + fun exec f =
6.94 + let
6.95 + val future = Future.fork (fn () =>
6.96 + let
6.97 + val res = Exn.interruptible_capture (f id) args
6.98 + val yxml = YXML.string_of (Codec.encode (Codec.exn_result Codec.id) res)
6.99 + in
6.100 + Output.protocol_message response [yxml]
6.101 + end)
6.102 + in
6.103 + Synchronized.change requests (Inttab.update_new (id, fn () => Future.cancel future))
6.104 + end
6.105 + in
6.106 + exec (get_operation name)
6.107 + end)
6.108 +
6.109 +val _ = Isabelle_Process.protocol_command "libisabelle_cancel"
6.110 + (fn ids =>
6.111 + let
6.112 + fun remove id tab = (Inttab.lookup tab id, Inttab.delete_safe id tab)
6.113 + val _ =
6.114 + map Markup.parse_int ids
6.115 + |> fold_map remove
6.116 + |> Synchronized.change_result requests
6.117 + |> map (fn NONE => () | SOME f => f ())
6.118 + in
6.119 + ()
6.120 + end)
6.121 +
6.122 +end
6.123 \ No newline at end of file
7.1 --- a/libisabelle-protocol/isabelle-2015/Codec_Class.thy Thu Jan 21 17:29:33 2016 +0100
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,21 +0,0 @@
7.4 -theory Codec_Class
7.5 -imports "../isabelle-common/Codec" "lib/classy/Classy"
7.6 -begin
7.7 -
7.8 -ML.class codec = \<open>'a codec\<close>
7.9 -
7.10 -ML.instance \<open>Codec.unit\<close> :: codec
7.11 -ML.instance \<open>Codec.bool\<close> :: codec
7.12 -ML.instance \<open>Codec.string\<close> :: codec
7.13 -ML.instance \<open>Codec.int\<close> :: codec
7.14 -ML.instance \<open>Codec.list\<close> :: codec
7.15 -ML.instance \<open>Codec.tuple\<close> :: codec
7.16 -ML.instance \<open>Codec.option\<close> :: codec
7.17 -ML.instance \<open>Codec.either\<close> :: codec
7.18 -ML.instance \<open>Codec.triple\<close> :: codec
7.19 -ML.instance \<open>Codec.sort\<close> :: codec
7.20 -ML.instance \<open>Codec.typ\<close> :: codec
7.21 -ML.instance \<open>Codec.term\<close> :: codec
7.22 -ML.instance \<open>Codec.tree\<close> :: codec
7.23 -
7.24 -end
7.25 \ No newline at end of file
8.1 --- a/libisabelle-protocol/isabelle-2015/Protocol.thy Thu Jan 21 17:29:33 2016 +0100
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,736 +0,0 @@
8.4 -theory Protocol
8.5 -imports Codec_Class
8.6 - "~~/src/Tools/isac/Knowledge/Build_Thydata"
8.7 -keywords "operation_setup" :: thy_decl % "ML"
8.8 -begin
8.9 -
8.10 -ML_file "../isabelle-common/protocol.ML"
8.11 -
8.12 -section \<open>Original from libisabelle-protocol\<close>
8.13 -ML\<open>
8.14 -val _ =
8.15 - let
8.16 - open Protocol
8.17 - fun operation_setup_cmd name source (flags as {auto, ...}) ctxt =
8.18 - let
8.19 - fun eval enclose =
8.20 - ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of source)
8.21 - (ML_Lex.read ("Protocol.add_operation " ^ ML_Syntax.print_string name ^ "(") @
8.22 - enclose (ML_Lex.read_source false source) @
8.23 - ML_Lex.read ")" @
8.24 - ML_Lex.read (print_flags flags))
8.25 - in
8.26 - if auto then
8.27 - let
8.28 - val ML_Types.Fun (arg, res) = ML_Types.ml_type_of ctxt (Input.source_content source)
8.29 - val arg_codec = Classy.resolve @{ML.class codec} arg (Context.Proof ctxt)
8.30 - val res_codec = Classy.resolve @{ML.class codec} res (Context.Proof ctxt)
8.31 - fun enclose toks =
8.32 - ML_Lex.read "{from_lib=" @ ML_Lex.read arg_codec @ ML_Lex.read "," @
8.33 - ML_Lex.read "to_lib=" @ ML_Lex.read res_codec @ ML_Lex.read "," @
8.34 - ML_Lex.read "action=" @ toks @ ML_Lex.read "}"
8.35 - in
8.36 - eval enclose
8.37 - end
8.38 - else
8.39 - eval I
8.40 - end
8.41 - val parse_flag =
8.42 - (Parse.reserved "sequential" || Parse.reserved "bracket" || Parse.reserved "auto") >>
8.43 - (fn flag => join_flags
8.44 - {sequential = flag = "sequential",
8.45 - bracket = flag = "bracket",
8.46 - auto = flag = "auto"})
8.47 - val parse_flags =
8.48 - Parse.list parse_flag >> (fn fs => fold (curry op o) fs I)
8.49 - val parse_cmd =
8.50 - Scan.optional (Args.parens parse_flags) I --
8.51 - Parse.name --
8.52 - Parse.!!! (@{keyword "="} |-- Parse.ML_source)
8.53 - in
8.54 - Outer_Syntax.command @{command_keyword "operation_setup"} "define protocol operation in ML"
8.55 - (parse_cmd >> (fn ((flags, name), txt) =>
8.56 - Toplevel.keep (Toplevel.context_of #> operation_setup_cmd name txt (flags default_flags))))
8.57 - end
8.58 -\<close>
8.59 -
8.60 -operation_setup (auto) hello =
8.61 - \<open>fn data => "Hello " ^ data\<close>
8.62 -
8.63 -operation_setup (sequential, bracket, auto) use_thys =
8.64 - \<open>Thy_Info.use_thys o map (rpair Position.none)\<close>
8.65 -
8.66 -section \<open>Operation setup for Math_Engine : MATH_ENGINE\<close>
8.67 -
8.68 -(* val appendFormula : calcID -> cterm' -> XML.tree *)
8.69 -operation_setup (sequential, bracket, auto) append_form =
8.70 - \<open>fn intree =>
8.71 - (let
8.72 - val (calcid, cterm') = case intree of
8.73 - XML.Elem (("APPENDFORMULA", []), [
8.74 - XML.Elem (("CALCID", []), [XML.Text ci]),
8.75 - form]) => (ci |> int_of_str', form |> xml_to_formula |> term2str)
8.76 - | x => raise ERROR ("append_form: WRONG intree = " ^ xmlstr 0 x)
8.77 - val result = Math_Engine.appendFormula calcid cterm'
8.78 - in result end)
8.79 - handle ERROR msg => appendformulaERROR2xml 4711 msg\<close>
8.80 -
8.81 -(* val autoCalculate : calcID -> auto -> XML.tree *)
8.82 -operation_setup autocalculate = \<open>
8.83 - {from_lib = Codec.tree,
8.84 - to_lib = Codec.tree,
8.85 - action = (fn intree =>
8.86 - (let
8.87 - val (ci, a) = case intree of
8.88 - XML.Elem (("AUTOCALC", []), [
8.89 - XML.Elem (("CALCID", []), [XML.Text ci]), a]) => (ci, a)
8.90 - | tree => raise ERROR ("autocalculate: WRONG intree = " ^ xmlstr 0 tree)
8.91 - val SOME calcid = int_of_str ci
8.92 - val auto = xml_to_auto a
8.93 - val result = Math_Engine.autoCalculate calcid auto
8.94 - in result end)
8.95 - handle ERROR msg => autocalculateERROR2xml 4711 msg)}\<close>
8.96 -
8.97 -(* val applyTactic : calcID -> pos' -> tac -> XML.tree *)
8.98 -operation_setup apply_tac = \<open>
8.99 - {from_lib = Codec.tree,
8.100 - to_lib = Codec.tree,
8.101 - action = (fn intree =>
8.102 - (let
8.103 - val (ci, pos, tac) = case intree of
8.104 - XML.Elem (("AUTOCALC", []), [
8.105 - XML.Elem (("CALCID", []), [XML.Text ci]),
8.106 - pos, tac]) => (str2int ci, xml_to_pos pos, xml_to_tac tac)
8.107 - | tree => raise ERROR ("apply_tac: WRONG intree = " ^ xmlstr 0 tree)
8.108 - val result = Math_Engine.applyTactic ci pos tac
8.109 - in result end)
8.110 - handle ERROR msg => autocalculateERROR2xml 4711 msg)}\<close>
8.111 -
8.112 -(* val CalcTree : fmz list -> XML.tree *)
8.113 -operation_setup calctree = \<open>
8.114 - {from_lib = Codec.tree,
8.115 - to_lib = Codec.tree,
8.116 - action = (fn intree =>
8.117 - (let
8.118 - val fmz = case intree of
8.119 - tree as XML.Elem (("FORMALIZATION", []), vars) => xml_to_fmz tree
8.120 - | tree => raise ERROR ("calctree: WRONG intree = " ^ xmlstr 0 tree)
8.121 - val result = Math_Engine.CalcTree fmz
8.122 - in result end)
8.123 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.124 -
8.125 -(* val checkContext : calcID -> pos' -> guh -> XML.tree *)
8.126 -operation_setup check_ctxt = \<open>
8.127 - {from_lib = Codec.tree,
8.128 - to_lib = Codec.tree,
8.129 - action = (fn intree =>
8.130 - (let
8.131 - val (ci, pos, guh) = case intree of
8.132 - XML.Elem (("CONTEXTTHY", []), [
8.133 - XML.Elem (("CALCID", []), [XML.Text ci]),
8.134 - pos as XML.Elem (("POSITION", []), _),
8.135 - XML.Elem (("GUH", []), [XML.Text guh])])
8.136 - => (str2int ci, xml_to_pos pos, guh)
8.137 - | tree => raise ERROR ("check_ctxt: WRONG intree = " ^ xmlstr 0 tree)
8.138 - val result = Math_Engine.checkContext ci pos guh
8.139 - in result end)
8.140 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.141 -
8.142 -(* val DEconstrCalcTree : calcID -> XML.tree *)
8.143 -operation_setup deconstrcalctree = \<open>
8.144 - {from_lib = Codec.int,
8.145 - to_lib = Codec.tree,
8.146 - action = (fn calcid =>
8.147 - let
8.148 - val result = Math_Engine.DEconstrCalcTree calcid
8.149 - in result end)}\<close>
8.150 -
8.151 -(* val fetchApplicableTactics : calcID -> int -> pos' -> XML.tree *)
8.152 -operation_setup fetch_applicable_tacs = \<open>
8.153 - {from_lib = Codec.tree,
8.154 - to_lib = Codec.tree,
8.155 - action = (fn intree =>
8.156 - (let
8.157 - val (ci, i, pos) = case intree of
8.158 - XML.Elem (("APPLICABLETACTICS", []), [
8.159 - XML.Elem (("CALCID", []), [XML.Text ci]),
8.160 - XML.Elem (("INT", []), [XML.Text i]),
8.161 - pos as XML.Elem (("POSITION", []), _)])
8.162 - => (str2int ci, str2int i, xml_to_pos pos)
8.163 - | tree => raise ERROR ("fetch_applicable_tacs: WRONG intree = " ^ xmlstr 0 tree)
8.164 - val result = Math_Engine.fetchApplicableTactics ci i pos
8.165 - in result end)
8.166 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.167 -
8.168 -(* val fetchProposedTactic : calcID -> XML.tree *)
8.169 -operation_setup fetch_proposed_tac = \<open>
8.170 - {from_lib = Codec.tree,
8.171 - to_lib = Codec.tree,
8.172 - action = (fn intree =>
8.173 - (let
8.174 - val (ci) = case intree of
8.175 - XML.Elem (("NEXTTAC", []), [
8.176 - XML.Elem (("CALCID", []), [XML.Text ci])]) => (str2int ci)
8.177 - | tree => raise ERROR ("fetch_proposed_tac: WRONG intree = " ^ xmlstr 0 tree)
8.178 - val result = Math_Engine.fetchProposedTactic ci
8.179 - in result end)
8.180 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.181 -
8.182 -(* val findFillpatterns : calcID -> errpatID -> XML.tree *)
8.183 -operation_setup find_fill_patts = \<open>
8.184 - {from_lib = Codec.tree,
8.185 - to_lib = Codec.tree,
8.186 - action = (fn intree =>
8.187 - (let
8.188 - val (ci, err_pat_id) = case intree of
8.189 - XML.Elem (("FINDFILLPATTERNS", []), [
8.190 - XML.Elem (("CALCID", []), [XML.Text ci]),
8.191 - XML.Elem (("STRING", []), [XML.Text err_pat_id])])
8.192 - => (str2int ci, err_pat_id)
8.193 - | tree => raise ERROR ("find_fill_patts: WRONG intree = " ^ xmlstr 0 tree)
8.194 - val result = Math_Engine.findFillpatterns ci err_pat_id
8.195 - in result end)
8.196 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.197 -
8.198 -(* val getAccumulatedAsms : calcID -> pos' -> XML.tree *)
8.199 -operation_setup get_accumulated_asms = \<open>
8.200 - {from_lib = Codec.tree,
8.201 - to_lib = Codec.tree,
8.202 - action = (fn intree =>
8.203 - (let
8.204 - val (ci, pos) = case intree of
8.205 - XML.Elem (("GETASSUMPTIONS", []), [
8.206 - XML.Elem (("CALCID", []), [XML.Text ci]),
8.207 - pos as XML.Elem (("POSITION", []), _)])
8.208 - => (str2int ci, xml_to_pos pos)
8.209 - | tree => raise ERROR ("autocalculate: WRONG intree = " ^ xmlstr 0 tree)
8.210 - val result = Math_Engine.getAccumulatedAsms ci pos
8.211 - in result end)
8.212 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.213 -
8.214 -(* val getActiveFormula : calcID -> XML.tree *)
8.215 -operation_setup get_active_form = \<open>
8.216 - {from_lib = Codec.tree,
8.217 - to_lib = Codec.tree,
8.218 - action = (fn intree =>
8.219 - (let
8.220 - val (ci) = case intree of
8.221 - XML.Elem (("CALCITERATOR", []), [
8.222 - XML.Elem (("CALCID", []), [XML.Text ci])])
8.223 - => (str2int ci)
8.224 - | tree => raise ERROR ("get_active_form: WRONG intree = " ^ xmlstr 0 tree)
8.225 - val result = Math_Engine.getActiveFormula ci
8.226 - in result end)
8.227 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.228 -
8.229 -(* val getAssumptions : calcID -> pos' -> XML.tree *)
8.230 -operation_setup get_asms = \<open>
8.231 - {from_lib = Codec.tree,
8.232 - to_lib = Codec.tree,
8.233 - action = (fn intree =>
8.234 - (let
8.235 - val (ci, pos) = case intree of
8.236 - XML.Elem (("APPLICABLETACTICS", []), [
8.237 - XML.Elem (("CALCID", []), [XML.Text ci]),
8.238 - pos as XML.Elem (("POSITION", []), _)])
8.239 - => (str2int ci, xml_to_pos pos)
8.240 - | tree => raise ERROR ("get_asms: WRONG intree = " ^ xmlstr 0 tree)
8.241 - val result = Math_Engine.getAssumptions ci pos
8.242 - in result end)
8.243 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.244 -
8.245 -(* val getFormulaeFromTo : calcID -> pos' -> pos' -> int -> bool -> XML.tree *)
8.246 -operation_setup getformulaefromto = \<open>
8.247 - {from_lib = Codec.tree,
8.248 - to_lib = Codec.tree,
8.249 - action = (fn intree =>
8.250 - (let
8.251 - val (calcid, from, to, level, rules) = case intree of
8.252 - XML.Elem (("GETFORMULAEFROMTO", []), [
8.253 - XML.Elem (("CALCID", []), [XML.Text calcid]),
8.254 - from as XML.Elem (("POSITION", []), [
8.255 - XML.Elem (("INTLIST", []), _),
8.256 - XML.Elem (("POS", []), [XML.Text _])]),
8.257 - to as XML.Elem (("POSITION", []), [
8.258 - XML.Elem (("INTLIST", []), _),
8.259 - XML.Elem (("POS", []), [XML.Text _])]),
8.260 - XML.Elem (("INT", []), [XML.Text level]),
8.261 - XML.Elem (("BOOL", []), [XML.Text rules])])
8.262 - => (str2int calcid, xml_to_pos from, xml_to_pos to, str2int level, string_to_bool rules)
8.263 - | tree => raise ERROR ("getformulaefromto: WRONG intree = " ^ xmlstr 0 tree)
8.264 - val result = Math_Engine.getFormulaeFromTo calcid from to level rules
8.265 - in result end)
8.266 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.267 -
8.268 -(* val getTactic : calcID -> pos' -> XML.tree *)
8.269 -operation_setup get_tac = \<open>
8.270 - {from_lib = Codec.tree,
8.271 - to_lib = Codec.tree,
8.272 - action = (fn intree =>
8.273 - (let
8.274 - val (ci, pos) = case intree of
8.275 - XML.Elem (("GETTACTIC", []), [
8.276 - XML.Elem (("CALCID", []), [XML.Text ci]),
8.277 - pos as XML.Elem (("POSITION", []), _)])
8.278 - => (str2int ci, xml_to_pos pos)
8.279 - | tree => raise ERROR ("get_tac: WRONG intree = " ^ xmlstr 0 tree)
8.280 - val result = Math_Engine.getTactic ci pos
8.281 - in result end)
8.282 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.283 -
8.284 -(* val initContext : calcID -> ketype -> pos' -> XML.tree *)
8.285 -operation_setup init_ctxt = \<open>
8.286 - {from_lib = Codec.tree,
8.287 - to_lib = Codec.tree,
8.288 - action = (fn intree =>
8.289 - ((let
8.290 - val (ci, ketype, pos) = case intree of
8.291 - XML.Elem (("INITCONTEXT", []), [
8.292 - XML.Elem (("CALCID", []), [XML.Text ci]),
8.293 - ketype as XML.Elem (("KETYPE", []), _),
8.294 - pos as XML.Elem (("POSITION", []), _)])
8.295 - => (str2int ci, xml_to_ketype ketype, xml_to_pos pos)
8.296 - | tree => raise ERROR ("init_ctxt: WRONG intree = " ^ xmlstr 0 tree)
8.297 - val result = Math_Engine.initContext ci ketype pos
8.298 - in result end)
8.299 - handle ERROR msg => sysERROR2xml 4711 msg)
8.300 - handle _ => sysERROR2xml 4711 "Protocol.operation_setup init_ctxt UNKNOWN exn")}\<close>
8.301 -
8.302 -(* val inputFillFormula: calcID -> string -> XML.tree *)
8.303 -operation_setup input_fill_form = \<open>
8.304 - {from_lib = Codec.tree,
8.305 - to_lib = Codec.tree,
8.306 - action = (fn intree =>
8.307 - (let
8.308 - val (ci, str) = case intree of
8.309 - XML.Elem (("AUTOCALC", []), [
8.310 - XML.Elem (("CALCID", []), [XML.Text ci]),
8.311 - XML.Elem (("STRING", []), [XML.Text str])])
8.312 - => (str2int ci, str)
8.313 - | tree => raise ERROR ("input_fill_form: WRONG intree = " ^ xmlstr 0 tree)
8.314 - val result = Math_Engine.inputFillFormula ci str
8.315 - in result end)
8.316 - handle ERROR msg => message2xml 4711 msg)}\<close>
8.317 -
8.318 -(* val interSteps : calcID -> pos' -> XML.tree *)
8.319 -operation_setup inter_steps = \<open>
8.320 - {from_lib = Codec.tree,
8.321 - to_lib = Codec.tree,
8.322 - action = (fn intree =>
8.323 - (let
8.324 - val (ci, pos) = case intree of
8.325 - XML.Elem (("INTERSTEPS", []), [
8.326 - XML.Elem (("CALCID", []), [XML.Text ci]),
8.327 - pos as XML.Elem (("POSITION", []), _)])
8.328 - => (str2int ci, xml_to_pos pos)
8.329 - | tree => raise ERROR ("inter_steps: WRONG intree = " ^ xmlstr 0 tree)
8.330 - val result = Math_Engine.interSteps ci pos
8.331 - in result end)
8.332 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.333 -
8.334 -(* val Iterator : calcID -> XML.tree *)
8.335 -operation_setup iterator = \<open>
8.336 - {from_lib = Codec.int,
8.337 - to_lib = Codec.tree,
8.338 - action = (fn calcid =>
8.339 - let
8.340 - val result = Math_Engine.Iterator calcid
8.341 - in result end)}\<close>
8.342 -
8.343 -(* val IteratorTEST : calcID -> iterID *)
8.344 -
8.345 -(* val modelProblem : calcID -> XML.tree *)
8.346 -operation_setup model_pbl = \<open>
8.347 - {from_lib = Codec.tree,
8.348 - to_lib = Codec.tree,
8.349 - action = (fn intree =>
8.350 - (let
8.351 - val (ci) = case intree of
8.352 - XML.Elem (("MODIFYCALCHEAD", []), [
8.353 - XML.Elem (("CALCID", []), [XML.Text ci])])
8.354 - => (str2int ci)
8.355 - | tree => raise ERROR ("model_pbl: WRONG intree = " ^ xmlstr 0 tree)
8.356 - val result = Math_Engine.modelProblem ci
8.357 - in result end)
8.358 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.359 -
8.360 -(* val modifyCalcHead : calcID -> icalhd -> XML.tree *)
8.361 -operation_setup modify_calchead = \<open>
8.362 - {from_lib = Codec.tree,
8.363 - to_lib = Codec.tree,
8.364 - action = (fn intree =>
8.365 - (let
8.366 - val (ci, icalhd) = case intree of
8.367 - XML.Elem (("MODIFYCALCHEAD", []), [
8.368 - XML.Elem (("CALCID", []), [XML.Text ci]),
8.369 - icalhd])
8.370 - => (str2int ci, xml_to_icalhd icalhd)
8.371 - | tree => raise ERROR ("modify_calchead: WRONG intree = " ^ xmlstr 0 tree)
8.372 - val result = Math_Engine.modifyCalcHead ci icalhd
8.373 - in result end)
8.374 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.375 -
8.376 -(* val moveActiveCalcHead : calcID -> XML.tree *)
8.377 -operation_setup move_active_calchead = \<open>
8.378 - {from_lib = Codec.tree,
8.379 - to_lib = Codec.tree,
8.380 - action = (fn intree =>
8.381 - (let
8.382 - val (ci) = case intree of
8.383 - XML.Elem (("CALCITERATOR", []), [
8.384 - XML.Elem (("CALCID", []), [XML.Text ci])])
8.385 - => (str2int ci)
8.386 - | tree => raise ERROR ("move_active_calchead: WRONG intree = " ^ xmlstr 0 tree)
8.387 - val result = Math_Engine.moveActiveCalcHead ci
8.388 - in result end)
8.389 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.390 -
8.391 -(* val moveActiveDown : calcID -> XML.tree *)
8.392 -operation_setup move_active_down = \<open>
8.393 - {from_lib = Codec.tree,
8.394 - to_lib = Codec.tree,
8.395 - action = (fn intree =>
8.396 - (let
8.397 - val (ci) = case intree of
8.398 - XML.Elem (("CALCITERATOR", []), [
8.399 - XML.Elem (("CALCID", []), [XML.Text ci])])
8.400 - => (str2int ci)
8.401 - | tree => raise ERROR ("move_active_down: WRONG intree = " ^ xmlstr 0 tree)
8.402 - val result = Math_Engine.moveActiveDown ci
8.403 - in result end)
8.404 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.405 -
8.406 -(* val moveActiveFormula : calcID -> pos' -> XML.tree *)
8.407 -operation_setup move_active_form = \<open>
8.408 - {from_lib = Codec.tree,
8.409 - to_lib = Codec.tree,
8.410 - action = (fn intree =>
8.411 - (let
8.412 - val (ci, pos) = case intree of
8.413 - XML.Elem (("CALCITERATOR", []), [
8.414 - XML.Elem (("CALCID", []), [XML.Text ci]),
8.415 - pos as XML.Elem (("POSITION", []), _)])
8.416 - => (str2int ci, xml_to_pos pos)
8.417 - | tree => raise ERROR ("move_active_form: WRONG intree = " ^ xmlstr 0 tree)
8.418 - val result = Math_Engine.moveActiveFormula ci pos
8.419 - in result end)
8.420 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.421 -
8.422 -(* val moveActiveLevelDown : calcID -> XML.tree *)
8.423 -operation_setup move_active_levdown = \<open>
8.424 - {from_lib = Codec.tree,
8.425 - to_lib = Codec.tree,
8.426 - action = (fn intree =>
8.427 - (let
8.428 - val (ci) = case intree of
8.429 - XML.Elem (("CALCITERATOR", []), [
8.430 - XML.Elem (("CALCID", []), [XML.Text ci])])
8.431 - => (str2int ci)
8.432 - | tree => raise ERROR ("move_active_levdown: WRONG intree = " ^ xmlstr 0 tree)
8.433 - val result = Math_Engine.moveActiveLevelDown ci
8.434 - in result end)
8.435 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.436 -
8.437 -(* val moveActiveLevelUp : calcID -> XML.tree *)
8.438 -operation_setup move_active_levup = \<open>
8.439 - {from_lib = Codec.tree,
8.440 - to_lib = Codec.tree,
8.441 - action = (fn intree =>
8.442 - (let
8.443 - val (ci) = case intree of
8.444 - XML.Elem (("CALCITERATOR", []), [
8.445 - XML.Elem (("CALCID", []), [XML.Text ci])])
8.446 - => (str2int ci)
8.447 - | tree => raise ERROR ("move_active_levup: WRONG intree = " ^ xmlstr 0 tree)
8.448 - val result = Math_Engine.moveActiveLevelUp ci
8.449 - in result end)
8.450 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.451 -
8.452 -(* val moveActiveRoot : calcID -> XML.tree *)
8.453 -operation_setup moveactiveroot = \<open>
8.454 - {from_lib = Codec.int,
8.455 - to_lib = Codec.tree,
8.456 - action = (fn calcid =>
8.457 - let
8.458 - val result = Math_Engine.moveActiveRoot calcid
8.459 - in result end)}\<close>
8.460 -
8.461 -(* val moveActiveRootTEST : calcID -> XML.tree *)
8.462 -
8.463 -(* val moveActiveUp : calcID -> XML.tree *)
8.464 -operation_setup move_active_up = \<open>
8.465 - {from_lib = Codec.tree,
8.466 - to_lib = Codec.tree,
8.467 - action = (fn intree =>
8.468 - (let
8.469 - val (ci) = case intree of
8.470 - XML.Elem (("CALCITERATOR", []), [
8.471 - XML.Elem (("CALCID", []), [XML.Text ci])])
8.472 - => (str2int ci)
8.473 - | tree => raise ERROR ("move_active_up: WRONG intree = " ^ xmlstr 0 tree)
8.474 - val result = Math_Engine.moveActiveUp ci
8.475 - in result end)
8.476 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.477 -
8.478 -(* val moveCalcHead : calcID -> pos' -> XML.tree *)
8.479 -operation_setup move_calchead = \<open>
8.480 - {from_lib = Codec.tree,
8.481 - to_lib = Codec.tree,
8.482 - action = (fn intree =>
8.483 - (let
8.484 - val (ci, pos) = case intree of
8.485 - XML.Elem (("CALCITERATOR", []), [
8.486 - XML.Elem (("CALCID", []), [XML.Text ci]),
8.487 - pos as XML.Elem (("POSITION", []), _)])
8.488 - => (str2int ci, xml_to_pos pos)
8.489 - | tree => raise ERROR ("move_active_calchead: WRONG intree = " ^ xmlstr 0 tree)
8.490 - val result = Math_Engine.moveCalcHead ci pos
8.491 - in result end)
8.492 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.493 -
8.494 -(* val moveDown : calcID -> pos' -> XML.tree *)
8.495 -operation_setup move_down = \<open>
8.496 - {from_lib = Codec.tree,
8.497 - to_lib = Codec.tree,
8.498 - action = (fn intree =>
8.499 - (let
8.500 - val (ci, pos) = case intree of
8.501 - XML.Elem (("CALCITERATOR", []), [
8.502 - XML.Elem (("CALCID", []), [XML.Text ci]),
8.503 - pos as XML.Elem (("POSITION", []), _)])
8.504 - => (str2int ci, xml_to_pos pos)
8.505 - | tree => raise ERROR ("move_down: WRONG intree = " ^ xmlstr 0 tree)
8.506 - val result = Math_Engine.moveDown ci pos
8.507 - in result end)
8.508 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.509 -
8.510 -(* val moveLevelDown : calcID -> pos' -> XML.tree *)
8.511 -operation_setup move_levdn = \<open>
8.512 - {from_lib = Codec.tree,
8.513 - to_lib = Codec.tree,
8.514 - action = (fn intree =>
8.515 - (let
8.516 - val (ci, pos) = case intree of
8.517 - XML.Elem (("CALCITERATOR", []), [
8.518 - XML.Elem (("CALCID", []), [XML.Text ci]),
8.519 - pos as XML.Elem (("POSITION", []), _)])
8.520 - => (str2int ci, xml_to_pos pos)
8.521 - | tree => raise ERROR ("move_levdn: WRONG intree = " ^ xmlstr 0 tree)
8.522 - val result = Math_Engine.moveLevelDown ci pos
8.523 - in result end)
8.524 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.525 -
8.526 -(* val moveLevelUp : calcID -> pos' -> XML.tree *)
8.527 -operation_setup move_levup = \<open>
8.528 - {from_lib = Codec.tree,
8.529 - to_lib = Codec.tree,
8.530 - action = (fn intree =>
8.531 - (let
8.532 - val (ci, pos) = case intree of
8.533 - XML.Elem (("CALCITERATOR", []), [
8.534 - XML.Elem (("CALCID", []), [XML.Text ci]),
8.535 - pos as XML.Elem (("POSITION", []), _)])
8.536 - => (str2int ci, xml_to_pos pos)
8.537 - | tree => raise ERROR ("move_levup: WRONG intree = " ^ xmlstr 0 tree)
8.538 - val result = Math_Engine.moveLevelUp ci pos
8.539 - in result end)
8.540 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.541 -
8.542 -(* val moveRoot : calcID -> XML.tree *)
8.543 -operation_setup move_root = \<open>
8.544 - {from_lib = Codec.tree,
8.545 - to_lib = Codec.tree,
8.546 - action = (fn intree =>
8.547 - (let
8.548 - val (ci) = case intree of
8.549 - XML.Elem (("CALCITERATOR", []), [
8.550 - XML.Elem (("CALCID", []), [XML.Text ci])])
8.551 - => (str2int ci)
8.552 - | tree => raise ERROR ("move_root: WRONG intree = " ^ xmlstr 0 tree)
8.553 - val result = Math_Engine.moveRoot ci
8.554 - in result end)
8.555 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.556 -
8.557 -(* val moveUp : calcID -> pos' -> XML.tree *)
8.558 -operation_setup move_up = \<open>
8.559 - {from_lib = Codec.tree,
8.560 - to_lib = Codec.tree,
8.561 - action = (fn intree =>
8.562 - (let
8.563 - val (ci, pos) = case intree of
8.564 - XML.Elem (("CALCITERATOR", []), [
8.565 - XML.Elem (("CALCID", []), [XML.Text ci]),
8.566 - pos as XML.Elem (("POSITION", []), _)])
8.567 - => (str2int ci, xml_to_pos pos)
8.568 - | tree => raise ERROR ("move_up: WRONG intree = " ^ xmlstr 0 tree)
8.569 - val result = Math_Engine.moveUp ci pos
8.570 - in result end)
8.571 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.572 -
8.573 -(* val refFormula : calcID -> pos' -> XML.tree *)
8.574 -operation_setup refformula = \<open>
8.575 - {from_lib = Codec.tree,
8.576 - to_lib = Codec.tree,
8.577 - action = (fn intree =>
8.578 - (let
8.579 - val (ci, p) = case intree of
8.580 - XML.Elem (("REFFORMULA", []), [
8.581 - XML.Elem (("CALCID", []), [XML.Text ci]), p])
8.582 - => (ci, p)
8.583 - | tree => raise ERROR ("refformula: WRONG intree = " ^ xmlstr 0 tree)
8.584 - val SOME calcid = int_of_str ci
8.585 - val pos = xml_to_pos p
8.586 - val result = Math_Engine.refFormula calcid pos
8.587 - in result end)
8.588 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.589 -
8.590 -(* val refineProblem : calcID -> pos' -> guh -> XML.tree *)
8.591 -operation_setup refine_pbl = \<open>
8.592 - {from_lib = Codec.tree,
8.593 - to_lib = Codec.tree,
8.594 - action = (fn intree =>
8.595 - (let
8.596 - val (ci, pos, guh) = case intree of
8.597 - XML.Elem (("CONTEXTPBL", []), [
8.598 - XML.Elem (("CALCID", []), [XML.Text ci]),
8.599 - pos as XML.Elem (("POSITION", []), _),
8.600 - XML.Elem (("GUH", []), [XML.Text guh])])
8.601 - => (str2int ci, xml_to_pos pos, guh)
8.602 - | tree => raise ERROR ("refine_pbl: WRONG intree = " ^ xmlstr 0 tree)
8.603 - val result = Math_Engine.refineProblem ci pos guh
8.604 - in result end)
8.605 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.606 -
8.607 -(* val replaceFormula : calcID -> cterm' -> XML.tree *)
8.608 -operation_setup replace_form = \<open>
8.609 - {from_lib = Codec.tree,
8.610 - to_lib = Codec.tree,
8.611 - action = (fn intree =>
8.612 - (let
8.613 - val (calcid, cterm') = case intree of
8.614 - XML.Elem (("REPLACEFORMULA", []), [
8.615 - XML.Elem (("CALCID", []), [XML.Text ci]), form])
8.616 - => (ci |> int_of_str', form |> xml_to_formula |> term2str)
8.617 - | tree => raise ERROR ("replace_form: WRONG intree = " ^ xmlstr 0 tree)
8.618 - val result = Math_Engine.replaceFormula calcid cterm'
8.619 - in result end)
8.620 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.621 -
8.622 -(* val requestFillformula : calcID -> errpatID * fillpatID -> XML.tree NOT IMPL. IN isac-java *)
8.623 -operation_setup request_fill_form = \<open>
8.624 - {from_lib = Codec.tree,
8.625 - to_lib = Codec.tree,
8.626 - action = (fn intree =>
8.627 - (let
8.628 - val (ci, errpat_id, fillpat_id) = case intree of
8.629 - XML.Elem (("AUTOCALC", []), [
8.630 - XML.Elem (("CALCID", []), [XML.Text ci]),
8.631 - XML.Elem (("ERRPATTID", []), [XML.Text errpat_id]),
8.632 - XML.Elem (("FILLPATTID", []), [XML.Text fillpat_id])])
8.633 - => (str2int ci, errpat_id, fillpat_id)
8.634 - | tree => raise ERROR ("request_fill_form: WRONG intree = " ^ xmlstr 0 tree)
8.635 - val result = Math_Engine.requestFillformula ci (errpat_id, fillpat_id)
8.636 - in result end)
8.637 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.638 -
8.639 -(* val resetCalcHead : calcID -> XML.tree *)
8.640 -operation_setup reset_calchead = \<open>
8.641 - {from_lib = Codec.tree,
8.642 - to_lib = Codec.tree,
8.643 - action = (fn intree =>
8.644 - (let
8.645 - val (ci) = case intree of
8.646 - XML.Elem (("MODIFYCALCHEAD", []), [
8.647 - XML.Elem (("CALCID", []), [XML.Text ci])])
8.648 - => (str2int ci)
8.649 - | tree => raise ERROR ("reset_calchead: WRONG intree = " ^ xmlstr 0 tree)
8.650 - val result = Math_Engine.resetCalcHead ci
8.651 - in result end)
8.652 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.653 -
8.654 -(* val setContext : calcID -> pos' -> guh -> XML.tree *)
8.655 -operation_setup set_ctxt = \<open>
8.656 - {from_lib = Codec.tree,
8.657 - to_lib = Codec.tree,
8.658 - action = (fn intree =>
8.659 - (let
8.660 - val (ci, pos, guh) = case intree of
8.661 - XML.Elem (("CONTEXT", []), [
8.662 - XML.Elem (("CALCID", []), [XML.Text ci]),
8.663 - pos as XML.Elem (("POSITION", []), _),
8.664 - XML.Elem (("GUH", []), [XML.Text guh])])
8.665 - => (str2int ci, xml_to_pos pos, guh)
8.666 - | tree => raise ERROR ("set_ctxt: WRONG intree = " ^ xmlstr 0 tree)
8.667 - val result = Math_Engine.setContext ci pos guh
8.668 - in result end)
8.669 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.670 -
8.671 -(*//===vvv TODO ================================================================\\\\\\\\\\\\\\\\*)
8.672 -
8.673 -(* val setMethod : calcID -> metID -> XML.tree *)
8.674 -operation_setup set_met = \<open>
8.675 - {from_lib = Codec.tree,
8.676 - to_lib = Codec.tree,
8.677 - action = (fn intree =>
8.678 - (let
8.679 - val (ci, met_id) = case intree of
8.680 - XML.Elem (("MODIFYCALCHEAD", []), [
8.681 - XML.Elem (("CALCID", []), [XML.Text ci]),
8.682 - XML.Elem (("METHODID", []), [met_id])])
8.683 - => (str2int ci, xml_to_strs met_id)
8.684 - | tree => raise ERROR ("set_met: WRONG intree = " ^ xmlstr 0 tree)
8.685 - val result = Math_Engine.setMethod ci met_id
8.686 - in result end)
8.687 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.688 -
8.689 -(* val setNextTactic : calcID -> tac -> XML.tree *)
8.690 -operation_setup set_next_tac = \<open>
8.691 - {from_lib = Codec.tree,
8.692 - to_lib = Codec.tree,
8.693 - action = (fn intree =>
8.694 - (let
8.695 - val (ci, tac) = case intree of
8.696 - XML.Elem (("SETNEXTTACTIC", []), [
8.697 - XML.Elem (("CALCID", []), [XML.Text ci]),
8.698 - tac])
8.699 - => (str2int ci, xml_to_tac tac)
8.700 - | tree => raise ERROR ("set_next_tac: WRONG intree = " ^ xmlstr 0 tree)
8.701 - val result = Math_Engine.setNextTactic ci tac
8.702 - in result end)
8.703 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.704 -
8.705 -(*\\===^^^ TODO ================================================================///////////////*)
8.706 -
8.707 -(* val setProblem : calcID -> pblID -> XML.tree *)
8.708 -operation_setup set_pbl = \<open>
8.709 - {from_lib = Codec.tree,
8.710 - to_lib = Codec.tree,
8.711 - action = (fn intree =>
8.712 - (let
8.713 - val (ci, pbl_id) = case intree of
8.714 - XML.Elem (("MODIFYCALCHEAD", []), [
8.715 - XML.Elem (("CALCID", []), [XML.Text ci]),
8.716 - XML.Elem (("PROBLEMID", []), [pbl_id])])
8.717 - => (str2int ci, xml_to_strs pbl_id)
8.718 - | tree => raise ERROR ("set_pbl: WRONG intree = " ^ xmlstr 0 tree)
8.719 - val result = Math_Engine.setProblem ci pbl_id
8.720 - in result end)
8.721 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.722 -
8.723 -(* val setTheory : calcID -> thyID -> XML.tree *)
8.724 -operation_setup set_thy = \<open>
8.725 - {from_lib = Codec.tree,
8.726 - to_lib = Codec.tree,
8.727 - action = (fn intree =>
8.728 - (let
8.729 - val (ci, thy_id) = case intree of
8.730 - XML.Elem (("MODIFYCALCHEAD", []), [
8.731 - XML.Elem (("CALCID", []), [XML.Text ci]),
8.732 - XML.Elem (("THEORYID", []), [XML.Text thy_id])])
8.733 - => (str2int ci, thy_id)
8.734 - | tree => raise ERROR ("set_thy: WRONG intree = " ^ xmlstr 0 tree)
8.735 - val result = Math_Engine.setTheory ci thy_id
8.736 - in result end)
8.737 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
8.738 -
8.739 -end
9.1 --- a/libisabelle-protocol/isabelle-2015/ROOT Thu Jan 21 17:29:33 2016 +0100
9.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
9.3 @@ -1,7 +0,0 @@
9.4 -session Protocol2015 = Codec +
9.5 - theories
9.6 - Protocol
9.7 -
9.8 -session "HOL-Protocol2015" = "HOL-Codec" +
9.9 - theories
9.10 - Protocol
10.1 --- a/libisabelle-protocol/isabelle-2015/lib/classy/.git Thu Jan 21 17:29:33 2016 +0100
10.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
10.3 @@ -1,1 +0,0 @@
10.4 -gitdir: ../../../.git/modules/isabelle-2015/lib/classy
11.1 --- a/libisabelle-protocol/isabelle-2015/lib/classy/.gitignore Thu Jan 21 17:29:33 2016 +0100
11.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
11.3 @@ -1,1 +0,0 @@
11.4 -Scratch.thy
12.1 --- a/libisabelle-protocol/isabelle-2015/lib/classy/Classy.thy Thu Jan 21 17:29:33 2016 +0100
12.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
12.3 @@ -1,22 +0,0 @@
12.4 -theory Classy
12.5 -imports Pure
12.6 -keywords
12.7 - "ML.class" :: thy_decl % "ML" and
12.8 - "ML.instance" :: thy_decl % "ML" and
12.9 - "ML.print_classes" :: diag
12.10 -begin
12.11 -
12.12 -ML_file "ml_types.ML"
12.13 -ML_file "classy.ML"
12.14 -
12.15 -setup \<open>Classy.setup\<close>
12.16 -
12.17 -ML_file "pretty_class.ML"
12.18 -
12.19 -ML.class pretty = \<open>'a pretty_class\<close>
12.20 -
12.21 -ML.instance \<open>Pretty_Class.string\<close> :: pretty
12.22 -ML.instance \<open>Pretty_Class.pretty\<close> :: pretty
12.23 -ML.instance \<open>Pretty_Class.list\<close> :: pretty
12.24 -
12.25 -end
12.26 \ No newline at end of file
13.1 --- a/libisabelle-protocol/isabelle-2015/lib/classy/Examples.thy Thu Jan 21 17:29:33 2016 +0100
13.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
13.3 @@ -1,18 +0,0 @@
13.4 -theory Examples
13.5 -imports Classy
13.6 -begin
13.7 -
13.8 -ML.print_classes
13.9 -
13.10 -ML\<open>format @{ML.resolve \<open>string list\<close> :: pretty} ["a", "b"] |> Pretty.writeln\<close> (* okay *)
13.11 -
13.12 -context begin
13.13 -
13.14 - (* conflicting instance *)
13.15 - ML.instance \<open>Pretty_Class.string\<close> :: pretty
13.16 -
13.17 - ML\<open>@{ML.resolve \<open>string\<close> :: pretty}\<close> (* error *)
13.18 -
13.19 -end
13.20 -
13.21 -end
13.22 \ No newline at end of file
14.1 --- a/libisabelle-protocol/isabelle-2015/lib/classy/LICENSE Thu Jan 21 17:29:33 2016 +0100
14.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
14.3 @@ -1,22 +0,0 @@
14.4 -The MIT License (MIT)
14.5 -
14.6 -Copyright (c) 2015 Lars Hupel
14.7 -
14.8 -Permission is hereby granted, free of charge, to any person obtaining a copy
14.9 -of this software and associated documentation files (the "Software"), to deal
14.10 -in the Software without restriction, including without limitation the rights
14.11 -to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
14.12 -copies of the Software, and to permit persons to whom the Software is
14.13 -furnished to do so, subject to the following conditions:
14.14 -
14.15 -The above copyright notice and this permission notice shall be included in all
14.16 -copies or substantial portions of the Software.
14.17 -
14.18 -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
14.19 -IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
14.20 -FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
14.21 -AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
14.22 -LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
14.23 -OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
14.24 -SOFTWARE.
14.25 -
15.1 --- a/libisabelle-protocol/isabelle-2015/lib/classy/README.md Thu Jan 21 17:29:33 2016 +0100
15.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
15.3 @@ -1,2 +0,0 @@
15.4 -# classy
15.5 -Type classes for Isabelle/ML
16.1 --- a/libisabelle-protocol/isabelle-2015/lib/classy/ROOT Thu Jan 21 17:29:33 2016 +0100
16.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
16.3 @@ -1,4 +0,0 @@
16.4 -session Classy = Pure +
16.5 - theories
16.6 - Classy
16.7 - Test
16.8 \ No newline at end of file
17.1 --- a/libisabelle-protocol/isabelle-2015/lib/classy/Test.thy Thu Jan 21 17:29:33 2016 +0100
17.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
17.3 @@ -1,50 +0,0 @@
17.4 -theory Test
17.5 -imports Classy
17.6 -begin
17.7 -
17.8 -section \<open>Parsing and printing types\<close>
17.9 -
17.10 -ML\<open>
17.11 -fun check t =
17.12 - let
17.13 - val t' = ML_Types.read_ml_type t |> ML_Types.pretty |> Pretty.string_of |> YXML.content_of
17.14 - in
17.15 - if t <> t' then
17.16 - error t'
17.17 - else
17.18 - ()
17.19 - end
17.20 -\<close>
17.21 -
17.22 -ML\<open>check "'a"\<close>
17.23 -ML\<open>check "'a * 'b"\<close>
17.24 -ML\<open>check "'a * 'b * 'c"\<close>
17.25 -ML\<open>check "('a * 'b) * 'c"\<close>
17.26 -ML\<open>check "'a * ('b * 'c)"\<close>
17.27 -ML\<open>check "'a * 'b -> 'c"\<close>
17.28 -ML\<open>check "'a * 'b -> 'a * 'b"\<close>
17.29 -ML\<open>check "('a -> 'b) * ('a -> 'b)"\<close>
17.30 -ML\<open>check "('a, 'b) foo"\<close>
17.31 -ML\<open>check "'a foo"\<close>
17.32 -ML\<open>check "unit foo"\<close>
17.33 -ML\<open>check "unit * 'a"\<close>
17.34 -ML\<open>check "'a foo * 'b foo bar"\<close>
17.35 -ML\<open>check "('a, unit) foo"\<close>
17.36 -ML\<open>check "('a * 'b) foo"\<close>
17.37 -ML\<open>check "('a -> 'b) foo"\<close>
17.38 -ML\<open>check "('a -> 'b, 'c) foo"\<close>
17.39 -ML\<open>check "('a -> 'b, 'c * 'd) foo"\<close>
17.40 -ML\<open>check "'a foo bar baz"\<close>
17.41 -ML\<open>check "('a foo, 'b) bar Long.ident.baz"\<close>
17.42 -ML\<open>check "{a: int}"\<close>
17.43 -ML\<open>check "{a: int, b: float}"\<close>
17.44 -ML\<open>check "{a: int, b: 'a -> 'b}"\<close>
17.45 -
17.46 -section \<open>Instance resolution\<close>
17.47 -
17.48 -ML\<open>@{ML.resolve \<open>string\<close> :: pretty}\<close>
17.49 -ML\<open>@{ML.resolve \<open>string list\<close> :: pretty}\<close>
17.50 -ML\<open>@{ML.resolve \<open>string list list\<close> :: pretty}\<close>
17.51 -ML\<open>@{ML.resolve \<open>Pretty.T\<close> :: pretty}\<close>
17.52 -
17.53 -end
17.54 \ No newline at end of file
18.1 --- a/libisabelle-protocol/isabelle-2015/lib/classy/classy.ML Thu Jan 21 17:29:33 2016 +0100
18.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
18.3 @@ -1,173 +0,0 @@
18.4 -signature CLASSY = sig
18.5 - val register_class: binding -> ML_Types.ml_type -> local_theory -> local_theory
18.6 - val register_class_cmd: binding -> string -> local_theory -> local_theory
18.7 -
18.8 - val register_instance_cmd: xstring * Position.T -> binding -> Input.source -> local_theory -> local_theory
18.9 -
18.10 - val check_class: Context.generic -> string * Position.T -> string
18.11 - val print_classes: Context.generic -> unit
18.12 -
18.13 - val resolve: string -> ML_Types.ml_type -> Context.generic -> string
18.14 -
18.15 - val setup: theory -> theory
18.16 -end
18.17 -
18.18 -structure Classy: CLASSY = struct
18.19 -
18.20 -type class_table = (ml_type * (ml_type * string) Name_Space.table) Name_Space.table
18.21 -
18.22 -exception DUP
18.23 -
18.24 -structure Classes = Generic_Data
18.25 -(
18.26 - type T = class_table
18.27 - val empty = Name_Space.empty_table "ML class"
18.28 - val merge = Name_Space.join_tables (fn _ => raise DUP) (* FIXME consistency check *)
18.29 - val extend = I
18.30 -)
18.31 -
18.32 -fun list_comb (term: string) (args: string list) =
18.33 - space_implode " " (enclose "(" ")" term :: map (enclose "(" ")") args)
18.34 -
18.35 -fun product [] = [[]]
18.36 - | product (xs :: xss) =
18.37 - maps (fn xs' => map (fn x => x :: xs') xs) (product xss)
18.38 -
18.39 -
18.40 -fun solve entries problem =
18.41 - let
18.42 - fun find (typ, term) =
18.43 - let
18.44 - val (args, candidate) = ML_Types.strip_fun typ
18.45 - in
18.46 - case ML_Types.match candidate problem [] of
18.47 - SOME env =>
18.48 - map (ML_Types.subst env) args
18.49 - |> map (solve entries)
18.50 - |> product
18.51 - |> map (list_comb term)
18.52 - | NONE => []
18.53 - end
18.54 - in
18.55 - maps find entries
18.56 - end
18.57 -
18.58 -fun resolve class typ context =
18.59 - let
18.60 - val classes = Classes.get context
18.61 - val (constructor, table) = Name_Space.get classes class
18.62 - val ML_Types.Con (name, [ML_Types.Var _]) = constructor
18.63 - val entries = map snd (Name_Space.extern_table true (Context.proof_of context) table)
18.64 - val problem = ML_Types.Con (name, [typ])
18.65 - val solutions = solve entries problem
18.66 - in
18.67 - case solutions of
18.68 - [] => error "no solutions"
18.69 - | [solution] => enclose "(" ")" solution
18.70 - | _ => error "too many solutions"
18.71 - end
18.72 -
18.73 -fun check_class context raw_binding =
18.74 - fst (Name_Space.check context (Classes.get context) raw_binding)
18.75 -
18.76 -val antiquote_setup =
18.77 - ML_Antiquotation.inline (Binding.qualify true "ML" @{binding class})
18.78 - (Scan.state -- Scan.lift (Parse.position Args.name) >>
18.79 - (fn (context, binding) => quote (check_class context binding))) #>
18.80 - ML_Antiquotation.inline (Binding.qualify true "ML" @{binding resolve})
18.81 - (Scan.state -- Scan.lift (Parse.ML_source --| @{keyword "::"} -- Parse.position Args.name) >>
18.82 - (fn (context, (source, binding)) =>
18.83 - resolve (check_class context binding) (ML_Types.read_ml_type (Input.source_content source)) context))
18.84 -
18.85 -fun pretty_classes context =
18.86 - let
18.87 - val table = Classes.get context
18.88 - val ctxt = Context.proof_of context
18.89 - val space = Name_Space.space_of_table table
18.90 - val entries = Name_Space.extern_table true ctxt table
18.91 -
18.92 - fun pretty_class ((class, _), (typ, sub_table)) =
18.93 - let
18.94 - val header = Pretty.block [Name_Space.pretty ctxt space class, Pretty.str ":", Pretty.brk 1, ML_Types.pretty typ]
18.95 -
18.96 - val sub_space = Name_Space.space_of_table sub_table
18.97 - val sub_entries = Name_Space.extern_table true ctxt sub_table
18.98 -
18.99 - fun pretty_instance ((instance, _), (typ, _)) =
18.100 - Pretty.item [Name_Space.pretty ctxt sub_space instance, Pretty.str ":", Pretty.brk 1, ML_Types.pretty typ]
18.101 -
18.102 - val instances = map pretty_instance sub_entries
18.103 - in
18.104 - Pretty.item (Pretty.fbreaks (header :: instances))
18.105 - end
18.106 - in
18.107 - Pretty.big_list "Classes" (map pretty_class entries)
18.108 - end
18.109 -
18.110 -val print_classes =
18.111 - Pretty.writeln o pretty_classes
18.112 -
18.113 -fun register_class binding typ =
18.114 - let
18.115 - val name =
18.116 - (case typ of
18.117 - ML_Types.Con (name, [ML_Types.Var _]) => name
18.118 - | _ => error "Malformed type")
18.119 - fun decl _ context =
18.120 - let
18.121 - val classes = Classes.get context
18.122 - val table = Name_Space.empty_table ("ML instances for " ^ name)
18.123 - val (_, classes') = Name_Space.define context true (binding, (typ, table)) classes
18.124 - in
18.125 - Classes.put classes' context
18.126 - end
18.127 - in
18.128 - Local_Theory.declaration {syntax = false, pervasive = false} decl
18.129 - end
18.130 -
18.131 -fun register_class_cmd binding typ =
18.132 - register_class binding (ML_Types.read_ml_type typ)
18.133 -
18.134 -fun register_instance_cmd raw_binding binding source lthy =
18.135 - let
18.136 - val typ = ML_Types.ml_type_of lthy (Input.source_content source)
18.137 - (* doesn't have any effect except for markup *)
18.138 - val _ = ML_Context.eval_source_in (SOME lthy) ML_Compiler.flags source
18.139 -
18.140 - (* FIXME check correct type *)
18.141 -
18.142 - fun decl _ context =
18.143 - let
18.144 - val classes = Classes.get context
18.145 - val (key, _) = Name_Space.check context classes raw_binding
18.146 - val upd = Name_Space.define context true (binding, (typ, Input.source_content source)) #> snd
18.147 - val classes' = Name_Space.map_table_entry key (apsnd upd) classes
18.148 - in Classes.put classes' context end
18.149 - in
18.150 - Local_Theory.declaration {syntax = false, pervasive = false} decl lthy
18.151 - end
18.152 -
18.153 -val _ =
18.154 - Outer_Syntax.local_theory @{command_keyword "ML.class"} "register new type class"
18.155 - (Parse.binding --| @{keyword "="} -- Parse.cartouche
18.156 - >> (fn (binding, typ) => register_class_cmd binding typ))
18.157 -
18.158 -val _ =
18.159 - let
18.160 - val opt_binding =
18.161 - Parse.binding --| @{keyword "="} ||
18.162 - Parse.position (Scan.succeed ()) >>
18.163 - (fn ((), pos) => Binding.make ("instance" ^ Markup.print_int (serial ()), pos))
18.164 - in
18.165 - Outer_Syntax.local_theory @{command_keyword "ML.instance"} "register new type class instance"
18.166 - (opt_binding -- (Parse.ML_source --| @{keyword "::"} -- Parse.position Args.name)
18.167 - >> (fn (binding, (source, name)) => register_instance_cmd name binding source))
18.168 - end
18.169 -
18.170 -val _ =
18.171 - Outer_Syntax.command @{command_keyword "ML.print_classes"} "print all registered classes"
18.172 - (Scan.succeed (Toplevel.keep (print_classes o Toplevel.generic_theory_of)))
18.173 -
18.174 -val setup = antiquote_setup
18.175 -
18.176 -end
18.177 \ No newline at end of file
19.1 --- a/libisabelle-protocol/isabelle-2015/lib/classy/ml_types.ML Thu Jan 21 17:29:33 2016 +0100
19.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
19.3 @@ -1,215 +0,0 @@
19.4 -signature ML_TYPES = sig
19.5 - datatype ml_type =
19.6 - Var of string |
19.7 - Con of string * ml_type list |
19.8 - Tuple of ml_type list |
19.9 - Fun of ml_type * ml_type |
19.10 - Record of (string * ml_type) list
19.11 -
19.12 - val unit: ml_type
19.13 - val canonicalize: ml_type -> ml_type
19.14 -
19.15 - val read_ml_type: string -> ml_type
19.16 - val ml_type_of: Proof.context -> string -> ml_type
19.17 -
19.18 - val pretty: ml_type -> Pretty.T
19.19 -
19.20 - type env = (string * ml_type) list
19.21 - val subst: env -> ml_type -> ml_type
19.22 - val match: ml_type -> ml_type -> env -> env option
19.23 -
19.24 - val strip_fun: ml_type -> ml_type list * ml_type
19.25 -end
19.26 -
19.27 -structure ML_Types: ML_TYPES = struct
19.28 -
19.29 -datatype ml_type =
19.30 - Var of string |
19.31 - Con of string * ml_type list |
19.32 - Tuple of ml_type list |
19.33 - Fun of ml_type * ml_type |
19.34 - Record of (string * ml_type) list
19.35 -
19.36 -val unit = Con ("unit", [])
19.37 -
19.38 -type env = (string * ml_type) list
19.39 -
19.40 -fun subst env (Con (name, ts)) = Con (name, map (subst env) ts)
19.41 - | subst env (Var name) = the_default (Var name) (AList.lookup op = env name)
19.42 - | subst env (Tuple ts) = Tuple (map (subst env) ts)
19.43 - | subst env (Fun (x, y)) = Fun (subst env x, subst env y)
19.44 - | subst env (Record fs) = Record (map (apsnd (subst env)) fs)
19.45 -
19.46 -fun match (Var name) t env =
19.47 - (case AList.lookup op = env name of
19.48 - NONE => SOME ((name, t) :: env)
19.49 - | SOME t' => if t = t' then SOME env else NONE)
19.50 - | match (Fun (x1, y1)) (Fun (x2, y2)) env =
19.51 - Option.mapPartial (match y1 y2) (match x1 x2 env)
19.52 - | match (Con (name1, ts1)) (Con (name2, ts2)) env =
19.53 - if name1 = name2 then match_list ts1 ts2 env else NONE
19.54 - | match (Tuple ts1) (Tuple ts2) env = match_list ts1 ts2 env
19.55 - | match (Record fs1) (Record fs2) env =
19.56 - if map fst fs1 = map fst fs2 then
19.57 - match_list (map snd fs1) (map snd fs2) env
19.58 - else
19.59 - NONE
19.60 - | match _ _ _ = NONE
19.61 -and match_list [] [] env = SOME env
19.62 - | match_list (t :: ts) (u :: us) env =Option.mapPartial (match t u) (match_list ts us env)
19.63 - | match_list _ _ _ = NONE
19.64 -
19.65 -fun strip_fun (Fun (x, y)) = let val (args, res) = strip_fun y in (x :: args, res) end
19.66 - | strip_fun t = ([], t)
19.67 -
19.68 -fun canonicalize (Var name) = Var name
19.69 - | canonicalize (Con (name, ts)) = Con (name, map canonicalize ts)
19.70 - | canonicalize (Tuple []) = unit
19.71 - | canonicalize (Tuple [t]) = canonicalize t
19.72 - | canonicalize (Tuple ts) = Tuple (map canonicalize ts)
19.73 - | canonicalize (Fun (t, u)) = Fun (canonicalize t, canonicalize u)
19.74 - | canonicalize (Record []) = unit
19.75 - | canonicalize (Record es) = Record (sort_wrt fst (map (apsnd canonicalize) es))
19.76 -
19.77 -val pretty =
19.78 - let
19.79 - datatype shape = SVar | SCon | STuple | SFun_Left | SRoot
19.80 -
19.81 - fun prec SVar _ = error "impossible"
19.82 - | prec SRoot _ = true
19.83 - | prec _ (Var _) = true
19.84 - | prec _ (Record _) = true
19.85 - | prec STuple (Con _) = true
19.86 - | prec STuple _ = false
19.87 - | prec SFun_Left (Con _) = true
19.88 - | prec SFun_Left (Tuple _) = true
19.89 - | prec SFun_Left (Fun _) = false
19.90 - | prec SCon (Con _) = true
19.91 - | prec SCon _ = false
19.92 -
19.93 - fun par n t p = if prec n t then p else Pretty.block [Pretty.str "(", p, Pretty.str ")"]
19.94 -
19.95 - fun aux s t =
19.96 - (case t of
19.97 - Var id => [Pretty.str id]
19.98 - | Tuple ts => Pretty.separate " *" (map (aux STuple) ts)
19.99 - | Fun (arg, res) =>
19.100 - [aux SFun_Left arg, Pretty.brk 1, Pretty.str "->", Pretty.brk 1, aux SRoot res]
19.101 - | Con (id, [t]) =>
19.102 - [aux SCon t, Pretty.brk 1, Pretty.str id]
19.103 - | Con (id, []) =>
19.104 - [Pretty.str id]
19.105 - | Con (id, ts) =>
19.106 - [Pretty.block (Pretty.str "(" :: Pretty.separate "," (map (aux SRoot) ts) @ [Pretty.str ")"]), Pretty.brk 1, Pretty.str id]
19.107 - | Record es =>
19.108 - Pretty.str "{" :: Pretty.separate "," (map (fn (name, t) => Pretty.block [Pretty.str name, Pretty.str ":", Pretty.brk 1, aux SRoot t]) es) @ [Pretty.str "}"])
19.109 - |> Pretty.block |> par s t
19.110 - in
19.111 - aux SRoot o canonicalize
19.112 - end
19.113 -
19.114 -type token = ML_Lex.token_kind * string
19.115 -
19.116 -type 'a parser = token list -> 'a * token list
19.117 -
19.118 -fun kind k: string parser = Scan.one (equal k o fst) >> snd
19.119 -fun tok t: unit parser = Scan.one (equal t) >> K ()
19.120 -fun keyword k: unit parser = tok (ML_Lex.Keyword, k)
19.121 -val open_parenthesis: unit parser = keyword "("
19.122 -val closed_parenthesis: unit parser = keyword ")"
19.123 -val open_brace: unit parser = keyword "{"
19.124 -val closed_brace: unit parser = keyword "}"
19.125 -val colon: unit parser = keyword ":"
19.126 -val comma: unit parser = keyword ","
19.127 -val arrow: unit parser = keyword "->"
19.128 -val asterisk: unit parser = tok (ML_Lex.Ident, "*")
19.129 -
19.130 -val ident: string parser =
19.131 - kind ML_Lex.Long_Ident ||
19.132 - Scan.one (fn (k, c) => k = ML_Lex.Ident andalso c <> "*") >> snd
19.133 -
19.134 -fun intersep p sep =
19.135 - (p ::: Scan.repeat (sep |-- p)) || Scan.succeed []
19.136 -
19.137 -val typ =
19.138 - let
19.139 - (* code partly lifted from Spec_Check *)
19.140 - fun make_con [] = raise Empty
19.141 - | make_con [c] = c
19.142 - | make_con (Con (s, _) :: cl) = Con (s, [make_con cl]);
19.143 -
19.144 - fun typ s = (func || tuple || typ_single) s
19.145 - and typ_arg s = (tuple || typ_single) s
19.146 - and typ_single s = (con || typ_basic) s
19.147 - and typ_basic s =
19.148 - (var
19.149 - || open_brace |-- record --| closed_brace
19.150 - || open_parenthesis |-- typ --| closed_parenthesis) s
19.151 - and list s = (open_parenthesis |-- typ -- Scan.repeat1 (comma |-- typ) --| closed_parenthesis >> op ::) s
19.152 - and var s = (kind ML_Lex.Type_Var >> Var) s
19.153 - and con s = ((con_nest
19.154 - || typ_basic -- con_nest >> (fn (b, Con (t, _) :: tl) => Con (t, [b]) :: tl)
19.155 - || list -- con_nest >> (fn (l, Con (t, _) :: tl) => Con (t, l) :: tl))
19.156 - >> (make_con o rev)) s
19.157 - and con_nest s = Scan.unless var (Scan.repeat1 (ident >> (Con o rpair []))) s
19.158 - and func s = (typ_arg --| arrow -- typ >> Fun) s
19.159 - and record s = (intersep (kind ML_Lex.Ident -- (colon |-- typ)) comma >> Record) s
19.160 - and tuple s = (typ_single -- Scan.repeat1 (asterisk |-- typ_single)
19.161 - >> (fn (t, tl) => Tuple (t :: tl))) s
19.162 - in typ end
19.163 -
19.164 -fun read_binding s =
19.165 - let
19.166 - val colon = (ML_Lex.Keyword, ":")
19.167 - val semicolon = (ML_Lex.Keyword, ";")
19.168 - fun unpack_tok tok = (ML_Lex.kind_of tok, ML_Lex.content_of tok)
19.169 - val toks = filter (not o equal ML_Lex.Space o fst) (map unpack_tok (ML_Lex.tokenize s))
19.170 - val junk = (Scan.many (not o equal colon) -- tok colon) >> K ()
19.171 - val stopper = Scan.stopper (K semicolon) (equal semicolon)
19.172 - val all = junk |-- Scan.finite stopper typ
19.173 - val (typ, rest) = all toks
19.174 - in
19.175 - if null rest then
19.176 - typ
19.177 - else
19.178 - error "Could not fully parse type"
19.179 - end
19.180 -
19.181 -fun read_ml_type s =
19.182 - let
19.183 - (* FIXME deduplicate *)
19.184 - val semicolon = (ML_Lex.Keyword, ";")
19.185 - fun unpack_tok tok = (ML_Lex.kind_of tok, ML_Lex.content_of tok)
19.186 - val toks = filter (not o equal ML_Lex.Space o fst) (map unpack_tok (ML_Lex.tokenize s))
19.187 - val stopper = Scan.stopper (K semicolon) (equal semicolon)
19.188 - val all = Scan.finite stopper typ
19.189 - val (typ, rest) = all toks
19.190 - in
19.191 - if null rest then
19.192 - typ
19.193 - else
19.194 - error "Could not fully parse type"
19.195 - end
19.196 -
19.197 -fun ml_type_of ctxt s =
19.198 - let
19.199 - (* code partly lifted from Spec_Check *)
19.200 - val return = Unsynchronized.ref NONE
19.201 - val s = "(fn () => (" ^ s ^ "))"
19.202 - val use_context: use_context =
19.203 - {tune_source = #tune_source ML_Env.local_context,
19.204 - name_space = #name_space ML_Env.local_context,
19.205 - str_of_pos = #str_of_pos ML_Env.local_context,
19.206 - print = fn r => return := SOME r,
19.207 - error = #error ML_Env.local_context}
19.208 - val _ =
19.209 - Context.setmp_thread_data (SOME (Context.Proof ctxt))
19.210 - (fn () => Secure.use_text use_context (0, "generated code") true s) ()
19.211 - val (Fun (Con ("unit", []), typ)) = read_binding (the (! return))
19.212 - in
19.213 - typ
19.214 - end
19.215 -
19.216 -end
19.217 -
19.218 -type ml_type = ML_Types.ml_type
20.1 --- a/libisabelle-protocol/isabelle-2015/lib/classy/pretty_class.ML Thu Jan 21 17:29:33 2016 +0100
20.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
20.3 @@ -1,12 +0,0 @@
20.4 -datatype 'a pretty_class = Pretty of ('a -> Pretty.T)
20.5 -
20.6 -fun format (Pretty f) = f
20.7 -
20.8 -structure Pretty_Class = struct
20.9 -
20.10 -val string: string pretty_class = Pretty Pretty.str
20.11 -val pretty: Pretty.T pretty_class = Pretty I
20.12 -fun list (Pretty f): 'a list pretty_class =
20.13 - Pretty (fn xs => Pretty.block (Pretty.str "[" :: Pretty.separate "," (map f xs) @ [Pretty.str "]"]))
20.14 -
20.15 -end
20.16 \ No newline at end of file
21.1 --- a/libisabelle-protocol/isabelle-common/Codec.thy Thu Jan 21 17:29:33 2016 +0100
21.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
21.3 @@ -1,7 +0,0 @@
21.4 -theory Codec
21.5 -imports Pure
21.6 -begin
21.7 -
21.8 -ML_file "codec.ML"
21.9 -
21.10 -end
22.1 --- a/libisabelle-protocol/isabelle-common/Codec_Test.thy Thu Jan 21 17:29:33 2016 +0100
22.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
22.3 @@ -1,36 +0,0 @@
22.4 -theory Codec_Test
22.5 -imports Codec "~~/src/Tools/Spec_Check/Spec_Check"
22.6 -begin
22.7 -
22.8 -ML\<open>
22.9 -fun check_for str =
22.10 - let
22.11 - val prop =
22.12 - "ALL x. (let val c = (" ^ str ^ ") in Codec.decode c (Codec.encode c x) = Codec.Success x end)"
22.13 - in check_property prop end
22.14 -
22.15 -fun gen_unit r =
22.16 - ((), r)
22.17 -\<close>
22.18 -
22.19 -ML_command\<open>
22.20 - check_for "Codec.unit";
22.21 - check_for "Codec.int";
22.22 - check_for "Codec.bool";
22.23 - check_for "Codec.string";
22.24 - check_for "Codec.tuple Codec.int Codec.int";
22.25 - check_for "Codec.tuple Codec.string Codec.unit";
22.26 - check_for "Codec.list Codec.unit";
22.27 - check_for "Codec.list Codec.int";
22.28 - check_for "Codec.list Codec.string";
22.29 - check_for "Codec.list (Codec.list Codec.string)";
22.30 - check_for "Codec.list (Codec.tuple Codec.int Codec.int)";
22.31 - check_for "Codec.tuple Codec.int (Codec.list Codec.int)";
22.32 - check_for "Codec.option Codec.int";
22.33 - check_for "Codec.option (Codec.list Codec.int)";
22.34 - check_for "Codec.list (Codec.option (Codec.int))";
22.35 - check_for "Codec.term";
22.36 - check_for "Codec.typ";
22.37 -\<close>
22.38 -
22.39 -end
23.1 --- a/libisabelle-protocol/isabelle-common/ROOT Thu Jan 21 17:29:33 2016 +0100
23.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
23.3 @@ -1,7 +0,0 @@
23.4 -session Codec = Pure +
23.5 - theories
23.6 - Codec_Test
23.7 -
23.8 -session "HOL-Codec" = HOL +
23.9 - theories
23.10 - Codec_Test
24.1 --- a/libisabelle-protocol/isabelle-common/codec.ML Thu Jan 21 17:29:33 2016 +0100
24.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
24.3 @@ -1,242 +0,0 @@
24.4 -signature CODEC = sig
24.5 - datatype 'a result = Success of 'a | Failure of string * XML.body
24.6 - datatype ('a, 'b) either = Left of 'a | Right of 'b
24.7 - type 'a codec
24.8 -
24.9 - val the_success: 'a result -> 'a
24.10 -
24.11 - val map_result: ('a -> 'b) -> 'a result -> 'b result
24.12 - val bind_result: ('a -> 'b result) -> 'a result -> 'b result
24.13 - val sequence_results: 'a result list -> 'a list result
24.14 - val traverse_results: ('a -> 'b result) -> 'a list -> 'b list result
24.15 -
24.16 - val transform: ('a -> 'b) -> ('b -> 'a) -> 'a codec -> 'b codec
24.17 - val encode: 'a codec -> 'a -> XML.tree
24.18 - val decode: 'a codec -> XML.tree -> 'a result
24.19 -
24.20 - val basic: {encode: 'a -> XML.tree, decode: XML.tree -> 'a result} -> 'a codec
24.21 -
24.22 - val variant: ('a -> (int * XML.tree)) -> (int -> (XML.tree -> 'a result) option) -> string -> 'a codec
24.23 - val tagged: string -> 'a codec -> 'a codec
24.24 -
24.25 - val unit: unit codec
24.26 - val bool: bool codec
24.27 - val string: string codec
24.28 - val int: int codec
24.29 - val list: 'a codec -> 'a list codec
24.30 - val tuple: 'a codec -> 'b codec -> ('a * 'b) codec
24.31 - val triple: 'a codec -> 'b codec -> 'c codec -> ('a * 'b * 'c) codec
24.32 - val either: 'a codec -> 'b codec -> ('a, 'b) either codec
24.33 - val option: 'a codec -> 'a option codec
24.34 - val tree: XML.tree codec
24.35 -
24.36 - val sort: sort codec
24.37 - val typ: typ codec
24.38 - val term: term codec
24.39 -
24.40 - exception GENERIC of string
24.41 - val exn: exn codec
24.42 - val exn_result: 'a codec -> 'a Exn.result codec
24.43 -
24.44 - val id: XML.tree codec (* internal *)
24.45 -end
24.46 -
24.47 -structure Codec: CODEC = struct
24.48 -
24.49 -datatype 'a result = Success of 'a | Failure of string * XML.body
24.50 -datatype ('a, 'b) either = Left of 'a | Right of 'b
24.51 -
24.52 -fun map_result f (Success a) = Success (f a)
24.53 - | map_result _ (Failure (msg, body)) = Failure (msg, body)
24.54 -
24.55 -fun bind_result f (Success a) = f a
24.56 - | bind_result _ (Failure (msg, body)) = Failure (msg, body)
24.57 -
24.58 -fun traverse_results _ [] = Success []
24.59 - | traverse_results f (x :: xs) =
24.60 - case f x of
24.61 - Success y => map_result (fn ys => y :: ys) (traverse_results f xs)
24.62 - | Failure (msg, body) => Failure (msg, body)
24.63 -
24.64 -fun sequence_results xs = traverse_results I xs
24.65 -
24.66 -fun the_success (Success a) = a
24.67 - | the_success _ = raise Fail "unexpected failure"
24.68 -
24.69 -fun add_tag tag idx body =
24.70 - let
24.71 - val attrs = case idx of SOME i => [("idx", XML.Encode.int_atom i)] | _ => []
24.72 - in XML.Elem (("tag", ("type", tag) :: attrs), body) end
24.73 -
24.74 -fun expect_tag tag tree =
24.75 - case tree of
24.76 - XML.Elem (("tag", [("type", tag')]), body) =>
24.77 - if tag = tag' then
24.78 - Success body
24.79 - else
24.80 - Failure ("tag mismatch: expected " ^ tag ^ ", got " ^ tag', [tree])
24.81 - | _ =>
24.82 - Failure ("tag " ^ tag ^ " expected", [tree])
24.83 -
24.84 -fun expect_tag' tag tree =
24.85 - case tree of
24.86 - XML.Elem (("tag", [("type", tag'), ("idx", i)]), body) =>
24.87 - if tag = tag' then
24.88 - Success (XML.Decode.int_atom i, body)
24.89 - handle XML.XML_ATOM err => Failure (err, [tree])
24.90 - else
24.91 - Failure ("tag mismatch: expected " ^ tag ^ ", got " ^ tag', [tree])
24.92 - | _ =>
24.93 - Failure ("indexed tag " ^ tag ^ " expected", [tree])
24.94 -
24.95 -
24.96 -abstype 'a codec = Codec of {encode: 'a -> XML.tree, decode: XML.tree -> 'a result} with
24.97 -
24.98 -val basic = Codec
24.99 -
24.100 -fun encode (Codec {encode, ...}) = encode
24.101 -fun decode (Codec {decode, ...}) = decode
24.102 -
24.103 -fun transform f g (Codec {encode, decode}) = Codec
24.104 - {encode = g #> encode,
24.105 - decode = decode #> map_result f}
24.106 -
24.107 -fun list a = Codec
24.108 - {encode = map (encode a) #> add_tag "list" NONE,
24.109 - decode = expect_tag "list" #> bind_result (traverse_results (decode a))}
24.110 -
24.111 -fun tuple a b = Codec
24.112 - {encode = (fn (x, y) => add_tag "tuple" NONE [encode a x, encode b y]),
24.113 - decode = expect_tag "tuple" #> bind_result (fn body =>
24.114 - case body of
24.115 - [x, y] => decode a x |> bind_result (fn x' => decode b y |> map_result (pair x'))
24.116 - | _ => Failure ("invalid structure", body))}
24.117 -
24.118 -fun variant enc dec tag = Codec
24.119 - {encode = (fn a => let val (idx, tree) = enc a in add_tag tag (SOME idx) [tree] end),
24.120 - decode = (fn tree => expect_tag' tag tree |> bind_result (fn (idx, body) =>
24.121 - case (body, dec idx) of
24.122 - ([tree'], SOME res) => res tree'
24.123 - | (_, SOME _) => Failure ("invalid structure", [tree])
24.124 - | (_, NONE) => Failure ("invalid index " ^ Markup.print_int idx, [tree])))}
24.125 -
24.126 -fun tagged tag a = Codec
24.127 - {encode = encode a #> single #> add_tag tag NONE,
24.128 - decode = expect_tag tag #> bind_result (fn body =>
24.129 - case body of
24.130 - [tree] => decode a tree
24.131 - | _ => Failure ("invalid structure", body))}
24.132 -
24.133 -val unit = Codec
24.134 - {encode = K (add_tag "unit" NONE []),
24.135 - decode = expect_tag "unit" #> bind_result (fn body =>
24.136 - case body of
24.137 - [] => Success ()
24.138 - | _ => Failure ("expected nothing", body))}
24.139 -
24.140 -fun text to from = Codec
24.141 - {encode = XML.Text o to,
24.142 - decode =
24.143 - (fn tree as XML.Text content =>
24.144 - (case from content of
24.145 - NONE => Failure ("decoding failed", [tree]) |
24.146 - SOME a => Success a)
24.147 - | tree => Failure ("expected text tree", [tree]))}
24.148 -
24.149 -val id = Codec {encode = I, decode = Success}
24.150 -
24.151 -end
24.152 -
24.153 -val int = tagged "int" (text Markup.print_int (Exn.get_res o Exn.capture Markup.parse_int))
24.154 -val bool = tagged "bool" (text Markup.print_bool (Exn.get_res o Exn.capture Markup.parse_bool))
24.155 -val string = tagged "string" (text I SOME)
24.156 -
24.157 -val tree = tagged "XML.tree" id
24.158 -
24.159 -fun option a =
24.160 - let
24.161 - fun enc (SOME x) = (0, encode a x)
24.162 - | enc NONE = (1, encode unit ())
24.163 - fun dec 0 = SOME (decode a #> map_result SOME)
24.164 - | dec 1 = SOME (decode unit #> map_result (K NONE))
24.165 - | dec _ = NONE
24.166 - in variant enc dec "option" end
24.167 -
24.168 -val content_of =
24.169 - XML.content_of o YXML.parse_body
24.170 -
24.171 -(* slightly fishy codec, doesn't preserve exception type *)
24.172 -exception GENERIC of string
24.173 -val exn = tagged "exn" (text (fn exn => (content_of (@{make_string} exn))) (SOME o GENERIC))
24.174 -
24.175 -fun exn_result a =
24.176 - let
24.177 - fun enc (Exn.Res t) = (0, encode a t)
24.178 - | enc (Exn.Exn e) = (1, encode exn e)
24.179 - fun dec 0 = SOME (decode a #> map_result Exn.Res)
24.180 - | dec 1 = SOME (decode exn #> map_result Exn.Exn)
24.181 - | dec _ = NONE
24.182 - in variant enc dec "Exn.result" end
24.183 -
24.184 -fun triple a b c =
24.185 - tuple a (tuple b c)
24.186 - |> transform (fn (a, (b, c)) => (a, b, c)) (fn (a, b, c) => (a, (b, c)))
24.187 -
24.188 -fun either a b =
24.189 - let
24.190 - fun enc (Left l) = (0, encode a l)
24.191 - | enc (Right r) = (1, encode b r)
24.192 - fun dec 0 = SOME (decode a #> map_result Left)
24.193 - | dec 1 = SOME (decode b #> map_result Right)
24.194 - | dec _ = NONE
24.195 - in variant enc dec "either" end
24.196 -
24.197 -val sort: sort codec = list string
24.198 -val indexname: indexname codec = tuple string int
24.199 -
24.200 -fun typ () =
24.201 - let
24.202 - fun typ_type () = tuple string (list (typ ()))
24.203 - val typ_tfree = tuple string sort
24.204 - val typ_tvar = tuple indexname sort
24.205 -
24.206 - fun enc (Type arg) = (0, encode (typ_type ()) arg)
24.207 - | enc (TFree arg) = (1, encode typ_tfree arg)
24.208 - | enc (TVar arg) = (2, encode typ_tvar arg)
24.209 - fun dec 0 = SOME (decode (typ_type ()) #> map_result Type)
24.210 - | dec 1 = SOME (decode typ_tfree #> map_result TFree)
24.211 - | dec 2 = SOME (decode typ_tvar #> map_result TVar)
24.212 - | dec _ = NONE
24.213 - in variant enc dec "Pure.typ" end
24.214 -
24.215 -val typ = typ ()
24.216 -
24.217 -fun term () =
24.218 - let
24.219 - val term_const = tuple string typ
24.220 - val term_free = tuple string typ
24.221 - val term_var = tuple indexname typ
24.222 - val term_bound = int
24.223 - fun term_abs () = triple string typ (term ())
24.224 - fun term_app () = tuple (term ()) (term ())
24.225 -
24.226 - fun enc (Const arg) = (0, encode term_const arg)
24.227 - | enc (Free arg) = (1, encode term_free arg)
24.228 - | enc (Var arg) = (2, encode term_var arg)
24.229 - | enc (Bound arg) = (3, encode term_bound arg)
24.230 - | enc (Abs arg) = (4, encode (term_abs ()) arg)
24.231 - | enc (op $ arg) = (5, encode (term_app ()) arg)
24.232 - fun dec 0 = SOME (decode term_const #> map_result Const)
24.233 - | dec 1 = SOME (decode term_free #> map_result Free)
24.234 - | dec 2 = SOME (decode term_var #> map_result Var)
24.235 - | dec 3 = SOME (decode term_bound #> map_result Bound)
24.236 - | dec 4 = SOME (decode (term_abs ()) #> map_result Abs)
24.237 - | dec 5 = SOME (decode (term_app ()) #> map_result op $)
24.238 - | dec _ = NONE
24.239 - in variant enc dec "Pure.term" end
24.240 -
24.241 -val term = term ()
24.242 -
24.243 -end
24.244 -
24.245 -type 'a codec = 'a Codec.codec
25.1 --- a/libisabelle-protocol/isabelle-common/protocol.ML Thu Jan 21 17:29:33 2016 +0100
25.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
25.3 @@ -1,119 +0,0 @@
25.4 -signature PROTOCOL = sig
25.5 - type name = string
25.6 - type ('i, 'o) operation =
25.7 - {from_lib : 'i codec,
25.8 - to_lib : 'o codec,
25.9 - action : 'i -> 'o}
25.10 -
25.11 - type flags = {sequential: bool, bracket: bool, auto: bool (* ignored *)}
25.12 -
25.13 - val default_flags : flags
25.14 - val join_flags : flags -> flags -> flags
25.15 - val print_flags : flags -> string
25.16 -
25.17 - val add_operation : name -> ('i, 'o) operation -> flags -> unit
25.18 - val get_operation : name -> int -> XML.tree -> XML.tree
25.19 -end
25.20 -
25.21 -structure Protocol: PROTOCOL = struct
25.22 -
25.23 -type name = string
25.24 -type ('i, 'o) operation =
25.25 - {from_lib : 'i codec,
25.26 - to_lib : 'o codec,
25.27 - action : 'i -> 'o}
25.28 -
25.29 -type flags = {sequential: bool, bracket: bool, auto: bool}
25.30 -
25.31 -val default_flags = {sequential = false, bracket = false, auto = false}
25.32 -
25.33 -fun join_flags
25.34 - {sequential = seq1, bracket = br1, auto = a1}
25.35 - {sequential = seq2, bracket = br2, auto = a2} =
25.36 - {sequential = seq1 orelse seq2, bracket = br1 orelse br2, auto = a1 orelse a2}
25.37 -
25.38 -fun print_flags {sequential, bracket, auto} =
25.39 - "({sequential=" ^ Markup.print_bool sequential ^ "," ^
25.40 - "bracket=" ^ Markup.print_bool bracket ^ "," ^
25.41 - "auto=" ^ Markup.print_bool auto ^ "})"
25.42 -
25.43 -type raw_operation = int -> XML.tree -> XML.tree
25.44 -
25.45 -exception GENERIC of string
25.46 -
25.47 -val operations =
25.48 - Synchronized.var "libisabelle.operations" (Symtab.empty: raw_operation Symtab.table)
25.49 -
25.50 -val requests =
25.51 - Synchronized.var "libisabelle.requests" (Inttab.empty: (unit -> unit) Inttab.table)
25.52 -
25.53 -fun sequentialize name f =
25.54 - let
25.55 - val var = Synchronized.var ("libisabelle." ^ name) ()
25.56 - in
25.57 - fn x => Synchronized.change_result var (fn _ => (f x, ()))
25.58 - end
25.59 -
25.60 -fun bracketize f id x =
25.61 - let
25.62 - val start = [(Markup.functionN, "libisabelle_start"), ("id", Markup.print_int id)]
25.63 - val stop = [(Markup.functionN, "libisabelle_stop"), ("id", Markup.print_int id)]
25.64 - val _ = Output.protocol_message start []
25.65 - val res = f id x
25.66 - val _ = Output.protocol_message stop []
25.67 - in res end
25.68 -
25.69 -fun add_operation name {from_lib, to_lib, action} {sequential, bracket, ...} =
25.70 - let
25.71 - fun raw _ tree =
25.72 - case Codec.decode from_lib tree of
25.73 - Codec.Success i => Codec.encode to_lib (action i)
25.74 - | Codec.Failure (msg, _) => raise Fail ("decoding input failed for operation " ^ name ^ ": " ^ msg)
25.75 - val raw' = raw
25.76 - |> (if bracket then bracketize else I)
25.77 - |> (if sequential then sequentialize name else I)
25.78 - in
25.79 - Synchronized.change operations (Symtab.update (name, raw'))
25.80 - end
25.81 -
25.82 -fun get_operation name =
25.83 - case Symtab.lookup (Synchronized.value operations) name of
25.84 - SOME operation => operation
25.85 - | NONE => fn _ => raise Fail "libisabelle: unknown command"
25.86 -
25.87 -val _ = Isabelle_Process.protocol_command "libisabelle"
25.88 - (fn id :: name :: [arg] =>
25.89 - let
25.90 - val id = Markup.parse_int id
25.91 - val response = [(Markup.functionN, "libisabelle_response"), ("id", Markup.print_int id)]
25.92 - val args = YXML.parse arg
25.93 - fun exec f =
25.94 - let
25.95 - val future = Future.fork (fn () =>
25.96 - let
25.97 - val res = Exn.interruptible_capture (f id) args
25.98 - val yxml = YXML.string_of (Codec.encode (Codec.exn_result Codec.id) res)
25.99 - in
25.100 - Output.protocol_message response [yxml]
25.101 - end)
25.102 - in
25.103 - Synchronized.change requests (Inttab.update_new (id, fn () => Future.cancel future))
25.104 - end
25.105 - in
25.106 - exec (get_operation name)
25.107 - end)
25.108 -
25.109 -val _ = Isabelle_Process.protocol_command "libisabelle_cancel"
25.110 - (fn ids =>
25.111 - let
25.112 - fun remove id tab = (Inttab.lookup tab id, Inttab.delete_safe id tab)
25.113 - val _ =
25.114 - map Markup.parse_int ids
25.115 - |> fold_map remove
25.116 - |> Synchronized.change_result requests
25.117 - |> map (fn NONE => () | SOME f => f ())
25.118 - in
25.119 - ()
25.120 - end)
25.121 -
25.122 -end
25.123 \ No newline at end of file
26.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
26.2 +++ b/libisabelle-protocol/isabelle/2015/Codec_Class.thy Fri Jan 22 15:53:13 2016 +0100
26.3 @@ -0,0 +1,21 @@
26.4 +theory Codec_Class
26.5 +imports "../../common/Common" "lib/classy/Classy"
26.6 +begin
26.7 +
26.8 +ML.class codec = \<open>'a codec\<close>
26.9 +
26.10 +ML.instance \<open>Codec.unit\<close> :: codec
26.11 +ML.instance \<open>Codec.bool\<close> :: codec
26.12 +ML.instance \<open>Codec.string\<close> :: codec
26.13 +ML.instance \<open>Codec.int\<close> :: codec
26.14 +ML.instance \<open>Codec.list\<close> :: codec
26.15 +ML.instance \<open>Codec.tuple\<close> :: codec
26.16 +ML.instance \<open>Codec.option\<close> :: codec
26.17 +ML.instance \<open>Codec.either\<close> :: codec
26.18 +ML.instance \<open>Codec.triple\<close> :: codec
26.19 +ML.instance \<open>Codec.sort\<close> :: codec
26.20 +ML.instance \<open>Codec.typ\<close> :: codec
26.21 +ML.instance \<open>Codec.term\<close> :: codec
26.22 +ML.instance \<open>Codec.tree\<close> :: codec
26.23 +
26.24 +end
26.25 \ No newline at end of file
27.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
27.2 +++ b/libisabelle-protocol/isabelle/2015/Protocol.thy Fri Jan 22 15:53:13 2016 +0100
27.3 @@ -0,0 +1,727 @@
27.4 +theory Protocol
27.5 +imports Codec_Class
27.6 + "~~/src/Tools/isac/Knowledge/Build_Thydata"
27.7 +keywords "operation_setup" :: thy_decl % "ML"
27.8 +begin
27.9 +
27.10 +ML\<open>
27.11 +val _ =
27.12 + let
27.13 + open Protocol
27.14 + fun operation_setup_cmd name source (flags as {auto, ...}) ctxt =
27.15 + let
27.16 + fun eval enclose =
27.17 + ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of source)
27.18 + (ML_Lex.read ("Protocol.add_operation " ^ ML_Syntax.print_string name ^ "(") @
27.19 + enclose (ML_Lex.read_source false source) @
27.20 + ML_Lex.read ")" @
27.21 + ML_Lex.read (print_flags flags))
27.22 + in
27.23 + if auto then
27.24 + let
27.25 + val ML_Types.Fun (arg, res) = ML_Types.ml_type_of ctxt (Input.source_content source)
27.26 + val arg_codec = Classy.resolve @{ML.class codec} arg (Context.Proof ctxt)
27.27 + val res_codec = Classy.resolve @{ML.class codec} res (Context.Proof ctxt)
27.28 + fun enclose toks =
27.29 + ML_Lex.read "{from_lib=" @ ML_Lex.read arg_codec @ ML_Lex.read "," @
27.30 + ML_Lex.read "to_lib=" @ ML_Lex.read res_codec @ ML_Lex.read "," @
27.31 + ML_Lex.read "action=" @ toks @ ML_Lex.read "}"
27.32 + in
27.33 + eval enclose
27.34 + end
27.35 + else
27.36 + eval I
27.37 + end
27.38 + val parse_flag =
27.39 + (Parse.reserved "sequential" || Parse.reserved "bracket" || Parse.reserved "auto") >>
27.40 + (fn flag => join_flags
27.41 + {sequential = flag = "sequential",
27.42 + bracket = flag = "bracket",
27.43 + auto = flag = "auto"})
27.44 + val parse_flags =
27.45 + Parse.list parse_flag >> (fn fs => fold (curry op o) fs I)
27.46 + val parse_cmd =
27.47 + Scan.optional (Args.parens parse_flags) I --
27.48 + Parse.name --
27.49 + Parse.!!! (@{keyword "="} |-- Parse.ML_source)
27.50 + in
27.51 + Outer_Syntax.command @{command_keyword "operation_setup"} "define protocol operation in ML"
27.52 + (parse_cmd >> (fn ((flags, name), txt) =>
27.53 + Toplevel.keep (Toplevel.context_of #> operation_setup_cmd name txt (flags default_flags))))
27.54 + end
27.55 +\<close>
27.56 +
27.57 +section \<open>Operation setup for Math_Engine : MATH_ENGINE\<close>
27.58 +
27.59 +(* val appendFormula : calcID -> cterm' -> XML.tree *)
27.60 +operation_setup (sequential, bracket, auto) append_form =
27.61 + \<open>fn intree =>
27.62 + (let
27.63 + val (calcid, cterm') = case intree of
27.64 + XML.Elem (("APPENDFORMULA", []), [
27.65 + XML.Elem (("CALCID", []), [XML.Text ci]),
27.66 + form]) => (ci |> int_of_str', form |> xml_to_formula |> term2str)
27.67 + | x => raise ERROR ("append_form: WRONG intree = " ^ xmlstr 0 x)
27.68 + val result = Math_Engine.appendFormula calcid cterm'
27.69 + in result end)
27.70 + handle ERROR msg => appendformulaERROR2xml 4711 msg\<close>
27.71 +
27.72 +(* val autoCalculate : calcID -> auto -> XML.tree *)
27.73 +operation_setup autocalculate = \<open>
27.74 + {from_lib = Codec.tree,
27.75 + to_lib = Codec.tree,
27.76 + action = (fn intree =>
27.77 + (let
27.78 + val (ci, a) = case intree of
27.79 + XML.Elem (("AUTOCALC", []), [
27.80 + XML.Elem (("CALCID", []), [XML.Text ci]), a]) => (ci, a)
27.81 + | tree => raise ERROR ("autocalculate: WRONG intree = " ^ xmlstr 0 tree)
27.82 + val SOME calcid = int_of_str ci
27.83 + val auto = xml_to_auto a
27.84 + val result = Math_Engine.autoCalculate calcid auto
27.85 + in result end)
27.86 + handle ERROR msg => autocalculateERROR2xml 4711 msg)}\<close>
27.87 +
27.88 +(* val applyTactic : calcID -> pos' -> tac -> XML.tree *)
27.89 +operation_setup apply_tac = \<open>
27.90 + {from_lib = Codec.tree,
27.91 + to_lib = Codec.tree,
27.92 + action = (fn intree =>
27.93 + (let
27.94 + val (ci, pos, tac) = case intree of
27.95 + XML.Elem (("AUTOCALC", []), [
27.96 + XML.Elem (("CALCID", []), [XML.Text ci]),
27.97 + pos, tac]) => (str2int ci, xml_to_pos pos, xml_to_tac tac)
27.98 + | tree => raise ERROR ("apply_tac: WRONG intree = " ^ xmlstr 0 tree)
27.99 + val result = Math_Engine.applyTactic ci pos tac
27.100 + in result end)
27.101 + handle ERROR msg => autocalculateERROR2xml 4711 msg)}\<close>
27.102 +
27.103 +(* val CalcTree : fmz list -> XML.tree *)
27.104 +operation_setup calctree = \<open>
27.105 + {from_lib = Codec.tree,
27.106 + to_lib = Codec.tree,
27.107 + action = (fn intree =>
27.108 + (let
27.109 + val fmz = case intree of
27.110 + tree as XML.Elem (("FORMALIZATION", []), vars) => xml_to_fmz tree
27.111 + | tree => raise ERROR ("calctree: WRONG intree = " ^ xmlstr 0 tree)
27.112 + val result = Math_Engine.CalcTree fmz
27.113 + in result end)
27.114 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.115 +
27.116 +(* val checkContext : calcID -> pos' -> guh -> XML.tree *)
27.117 +operation_setup check_ctxt = \<open>
27.118 + {from_lib = Codec.tree,
27.119 + to_lib = Codec.tree,
27.120 + action = (fn intree =>
27.121 + (let
27.122 + val (ci, pos, guh) = case intree of
27.123 + XML.Elem (("CONTEXTTHY", []), [
27.124 + XML.Elem (("CALCID", []), [XML.Text ci]),
27.125 + pos as XML.Elem (("POSITION", []), _),
27.126 + XML.Elem (("GUH", []), [XML.Text guh])])
27.127 + => (str2int ci, xml_to_pos pos, guh)
27.128 + | tree => raise ERROR ("check_ctxt: WRONG intree = " ^ xmlstr 0 tree)
27.129 + val result = Math_Engine.checkContext ci pos guh
27.130 + in result end)
27.131 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.132 +
27.133 +(* val DEconstrCalcTree : calcID -> XML.tree *)
27.134 +operation_setup deconstrcalctree = \<open>
27.135 + {from_lib = Codec.int,
27.136 + to_lib = Codec.tree,
27.137 + action = (fn calcid =>
27.138 + let
27.139 + val result = Math_Engine.DEconstrCalcTree calcid
27.140 + in result end)}\<close>
27.141 +
27.142 +(* val fetchApplicableTactics : calcID -> int -> pos' -> XML.tree *)
27.143 +operation_setup fetch_applicable_tacs = \<open>
27.144 + {from_lib = Codec.tree,
27.145 + to_lib = Codec.tree,
27.146 + action = (fn intree =>
27.147 + (let
27.148 + val (ci, i, pos) = case intree of
27.149 + XML.Elem (("APPLICABLETACTICS", []), [
27.150 + XML.Elem (("CALCID", []), [XML.Text ci]),
27.151 + XML.Elem (("INT", []), [XML.Text i]),
27.152 + pos as XML.Elem (("POSITION", []), _)])
27.153 + => (str2int ci, str2int i, xml_to_pos pos)
27.154 + | tree => raise ERROR ("fetch_applicable_tacs: WRONG intree = " ^ xmlstr 0 tree)
27.155 + val result = Math_Engine.fetchApplicableTactics ci i pos
27.156 + in result end)
27.157 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.158 +
27.159 +(* val fetchProposedTactic : calcID -> XML.tree *)
27.160 +operation_setup fetch_proposed_tac = \<open>
27.161 + {from_lib = Codec.tree,
27.162 + to_lib = Codec.tree,
27.163 + action = (fn intree =>
27.164 + (let
27.165 + val (ci) = case intree of
27.166 + XML.Elem (("NEXTTAC", []), [
27.167 + XML.Elem (("CALCID", []), [XML.Text ci])]) => (str2int ci)
27.168 + | tree => raise ERROR ("fetch_proposed_tac: WRONG intree = " ^ xmlstr 0 tree)
27.169 + val result = Math_Engine.fetchProposedTactic ci
27.170 + in result end)
27.171 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.172 +
27.173 +(* val findFillpatterns : calcID -> errpatID -> XML.tree *)
27.174 +operation_setup find_fill_patts = \<open>
27.175 + {from_lib = Codec.tree,
27.176 + to_lib = Codec.tree,
27.177 + action = (fn intree =>
27.178 + (let
27.179 + val (ci, err_pat_id) = case intree of
27.180 + XML.Elem (("FINDFILLPATTERNS", []), [
27.181 + XML.Elem (("CALCID", []), [XML.Text ci]),
27.182 + XML.Elem (("STRING", []), [XML.Text err_pat_id])])
27.183 + => (str2int ci, err_pat_id)
27.184 + | tree => raise ERROR ("find_fill_patts: WRONG intree = " ^ xmlstr 0 tree)
27.185 + val result = Math_Engine.findFillpatterns ci err_pat_id
27.186 + in result end)
27.187 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.188 +
27.189 +(* val getAccumulatedAsms : calcID -> pos' -> XML.tree *)
27.190 +operation_setup get_accumulated_asms = \<open>
27.191 + {from_lib = Codec.tree,
27.192 + to_lib = Codec.tree,
27.193 + action = (fn intree =>
27.194 + (let
27.195 + val (ci, pos) = case intree of
27.196 + XML.Elem (("GETASSUMPTIONS", []), [
27.197 + XML.Elem (("CALCID", []), [XML.Text ci]),
27.198 + pos as XML.Elem (("POSITION", []), _)])
27.199 + => (str2int ci, xml_to_pos pos)
27.200 + | tree => raise ERROR ("autocalculate: WRONG intree = " ^ xmlstr 0 tree)
27.201 + val result = Math_Engine.getAccumulatedAsms ci pos
27.202 + in result end)
27.203 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.204 +
27.205 +(* val getActiveFormula : calcID -> XML.tree *)
27.206 +operation_setup get_active_form = \<open>
27.207 + {from_lib = Codec.tree,
27.208 + to_lib = Codec.tree,
27.209 + action = (fn intree =>
27.210 + (let
27.211 + val (ci) = case intree of
27.212 + XML.Elem (("CALCITERATOR", []), [
27.213 + XML.Elem (("CALCID", []), [XML.Text ci])])
27.214 + => (str2int ci)
27.215 + | tree => raise ERROR ("get_active_form: WRONG intree = " ^ xmlstr 0 tree)
27.216 + val result = Math_Engine.getActiveFormula ci
27.217 + in result end)
27.218 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.219 +
27.220 +(* val getAssumptions : calcID -> pos' -> XML.tree *)
27.221 +operation_setup get_asms = \<open>
27.222 + {from_lib = Codec.tree,
27.223 + to_lib = Codec.tree,
27.224 + action = (fn intree =>
27.225 + (let
27.226 + val (ci, pos) = case intree of
27.227 + XML.Elem (("APPLICABLETACTICS", []), [
27.228 + XML.Elem (("CALCID", []), [XML.Text ci]),
27.229 + pos as XML.Elem (("POSITION", []), _)])
27.230 + => (str2int ci, xml_to_pos pos)
27.231 + | tree => raise ERROR ("get_asms: WRONG intree = " ^ xmlstr 0 tree)
27.232 + val result = Math_Engine.getAssumptions ci pos
27.233 + in result end)
27.234 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.235 +
27.236 +(* val getFormulaeFromTo : calcID -> pos' -> pos' -> int -> bool -> XML.tree *)
27.237 +operation_setup getformulaefromto = \<open>
27.238 + {from_lib = Codec.tree,
27.239 + to_lib = Codec.tree,
27.240 + action = (fn intree =>
27.241 + (let
27.242 + val (calcid, from, to, level, rules) = case intree of
27.243 + XML.Elem (("GETFORMULAEFROMTO", []), [
27.244 + XML.Elem (("CALCID", []), [XML.Text calcid]),
27.245 + from as XML.Elem (("POSITION", []), [
27.246 + XML.Elem (("INTLIST", []), _),
27.247 + XML.Elem (("POS", []), [XML.Text _])]),
27.248 + to as XML.Elem (("POSITION", []), [
27.249 + XML.Elem (("INTLIST", []), _),
27.250 + XML.Elem (("POS", []), [XML.Text _])]),
27.251 + XML.Elem (("INT", []), [XML.Text level]),
27.252 + XML.Elem (("BOOL", []), [XML.Text rules])])
27.253 + => (str2int calcid, xml_to_pos from, xml_to_pos to, str2int level, string_to_bool rules)
27.254 + | tree => raise ERROR ("getformulaefromto: WRONG intree = " ^ xmlstr 0 tree)
27.255 + val result = Math_Engine.getFormulaeFromTo calcid from to level rules
27.256 + in result end)
27.257 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.258 +
27.259 +(* val getTactic : calcID -> pos' -> XML.tree *)
27.260 +operation_setup get_tac = \<open>
27.261 + {from_lib = Codec.tree,
27.262 + to_lib = Codec.tree,
27.263 + action = (fn intree =>
27.264 + (let
27.265 + val (ci, pos) = case intree of
27.266 + XML.Elem (("GETTACTIC", []), [
27.267 + XML.Elem (("CALCID", []), [XML.Text ci]),
27.268 + pos as XML.Elem (("POSITION", []), _)])
27.269 + => (str2int ci, xml_to_pos pos)
27.270 + | tree => raise ERROR ("get_tac: WRONG intree = " ^ xmlstr 0 tree)
27.271 + val result = Math_Engine.getTactic ci pos
27.272 + in result end)
27.273 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.274 +
27.275 +(* val initContext : calcID -> ketype -> pos' -> XML.tree *)
27.276 +operation_setup init_ctxt = \<open>
27.277 + {from_lib = Codec.tree,
27.278 + to_lib = Codec.tree,
27.279 + action = (fn intree =>
27.280 + ((let
27.281 + val (ci, ketype, pos) = case intree of
27.282 + XML.Elem (("INITCONTEXT", []), [
27.283 + XML.Elem (("CALCID", []), [XML.Text ci]),
27.284 + ketype as XML.Elem (("KETYPE", []), _),
27.285 + pos as XML.Elem (("POSITION", []), _)])
27.286 + => (str2int ci, xml_to_ketype ketype, xml_to_pos pos)
27.287 + | tree => raise ERROR ("init_ctxt: WRONG intree = " ^ xmlstr 0 tree)
27.288 + val result = Math_Engine.initContext ci ketype pos
27.289 + in result end)
27.290 + handle ERROR msg => sysERROR2xml 4711 msg)
27.291 + handle _ => sysERROR2xml 4711 "Protocol.operation_setup init_ctxt UNKNOWN exn")}\<close>
27.292 +
27.293 +(* val inputFillFormula: calcID -> string -> XML.tree *)
27.294 +operation_setup input_fill_form = \<open>
27.295 + {from_lib = Codec.tree,
27.296 + to_lib = Codec.tree,
27.297 + action = (fn intree =>
27.298 + (let
27.299 + val (ci, str) = case intree of
27.300 + XML.Elem (("AUTOCALC", []), [
27.301 + XML.Elem (("CALCID", []), [XML.Text ci]),
27.302 + XML.Elem (("STRING", []), [XML.Text str])])
27.303 + => (str2int ci, str)
27.304 + | tree => raise ERROR ("input_fill_form: WRONG intree = " ^ xmlstr 0 tree)
27.305 + val result = Math_Engine.inputFillFormula ci str
27.306 + in result end)
27.307 + handle ERROR msg => message2xml 4711 msg)}\<close>
27.308 +
27.309 +(* val interSteps : calcID -> pos' -> XML.tree *)
27.310 +operation_setup inter_steps = \<open>
27.311 + {from_lib = Codec.tree,
27.312 + to_lib = Codec.tree,
27.313 + action = (fn intree =>
27.314 + (let
27.315 + val (ci, pos) = case intree of
27.316 + XML.Elem (("INTERSTEPS", []), [
27.317 + XML.Elem (("CALCID", []), [XML.Text ci]),
27.318 + pos as XML.Elem (("POSITION", []), _)])
27.319 + => (str2int ci, xml_to_pos pos)
27.320 + | tree => raise ERROR ("inter_steps: WRONG intree = " ^ xmlstr 0 tree)
27.321 + val result = Math_Engine.interSteps ci pos
27.322 + in result end)
27.323 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.324 +
27.325 +(* val Iterator : calcID -> XML.tree *)
27.326 +operation_setup iterator = \<open>
27.327 + {from_lib = Codec.int,
27.328 + to_lib = Codec.tree,
27.329 + action = (fn calcid =>
27.330 + let
27.331 + val result = Math_Engine.Iterator calcid
27.332 + in result end)}\<close>
27.333 +
27.334 +(* val IteratorTEST : calcID -> iterID *)
27.335 +
27.336 +(* val modelProblem : calcID -> XML.tree *)
27.337 +operation_setup model_pbl = \<open>
27.338 + {from_lib = Codec.tree,
27.339 + to_lib = Codec.tree,
27.340 + action = (fn intree =>
27.341 + (let
27.342 + val (ci) = case intree of
27.343 + XML.Elem (("MODIFYCALCHEAD", []), [
27.344 + XML.Elem (("CALCID", []), [XML.Text ci])])
27.345 + => (str2int ci)
27.346 + | tree => raise ERROR ("model_pbl: WRONG intree = " ^ xmlstr 0 tree)
27.347 + val result = Math_Engine.modelProblem ci
27.348 + in result end)
27.349 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.350 +
27.351 +(* val modifyCalcHead : calcID -> icalhd -> XML.tree *)
27.352 +operation_setup modify_calchead = \<open>
27.353 + {from_lib = Codec.tree,
27.354 + to_lib = Codec.tree,
27.355 + action = (fn intree =>
27.356 + (let
27.357 + val (ci, icalhd) = case intree of
27.358 + XML.Elem (("MODIFYCALCHEAD", []), [
27.359 + XML.Elem (("CALCID", []), [XML.Text ci]),
27.360 + icalhd])
27.361 + => (str2int ci, xml_to_icalhd icalhd)
27.362 + | tree => raise ERROR ("modify_calchead: WRONG intree = " ^ xmlstr 0 tree)
27.363 + val result = Math_Engine.modifyCalcHead ci icalhd
27.364 + in result end)
27.365 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.366 +
27.367 +(* val moveActiveCalcHead : calcID -> XML.tree *)
27.368 +operation_setup move_active_calchead = \<open>
27.369 + {from_lib = Codec.tree,
27.370 + to_lib = Codec.tree,
27.371 + action = (fn intree =>
27.372 + (let
27.373 + val (ci) = case intree of
27.374 + XML.Elem (("CALCITERATOR", []), [
27.375 + XML.Elem (("CALCID", []), [XML.Text ci])])
27.376 + => (str2int ci)
27.377 + | tree => raise ERROR ("move_active_calchead: WRONG intree = " ^ xmlstr 0 tree)
27.378 + val result = Math_Engine.moveActiveCalcHead ci
27.379 + in result end)
27.380 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.381 +
27.382 +(* val moveActiveDown : calcID -> XML.tree *)
27.383 +operation_setup move_active_down = \<open>
27.384 + {from_lib = Codec.tree,
27.385 + to_lib = Codec.tree,
27.386 + action = (fn intree =>
27.387 + (let
27.388 + val (ci) = case intree of
27.389 + XML.Elem (("CALCITERATOR", []), [
27.390 + XML.Elem (("CALCID", []), [XML.Text ci])])
27.391 + => (str2int ci)
27.392 + | tree => raise ERROR ("move_active_down: WRONG intree = " ^ xmlstr 0 tree)
27.393 + val result = Math_Engine.moveActiveDown ci
27.394 + in result end)
27.395 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.396 +
27.397 +(* val moveActiveFormula : calcID -> pos' -> XML.tree *)
27.398 +operation_setup move_active_form = \<open>
27.399 + {from_lib = Codec.tree,
27.400 + to_lib = Codec.tree,
27.401 + action = (fn intree =>
27.402 + (let
27.403 + val (ci, pos) = case intree of
27.404 + XML.Elem (("CALCITERATOR", []), [
27.405 + XML.Elem (("CALCID", []), [XML.Text ci]),
27.406 + pos as XML.Elem (("POSITION", []), _)])
27.407 + => (str2int ci, xml_to_pos pos)
27.408 + | tree => raise ERROR ("move_active_form: WRONG intree = " ^ xmlstr 0 tree)
27.409 + val result = Math_Engine.moveActiveFormula ci pos
27.410 + in result end)
27.411 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.412 +
27.413 +(* val moveActiveLevelDown : calcID -> XML.tree *)
27.414 +operation_setup move_active_levdown = \<open>
27.415 + {from_lib = Codec.tree,
27.416 + to_lib = Codec.tree,
27.417 + action = (fn intree =>
27.418 + (let
27.419 + val (ci) = case intree of
27.420 + XML.Elem (("CALCITERATOR", []), [
27.421 + XML.Elem (("CALCID", []), [XML.Text ci])])
27.422 + => (str2int ci)
27.423 + | tree => raise ERROR ("move_active_levdown: WRONG intree = " ^ xmlstr 0 tree)
27.424 + val result = Math_Engine.moveActiveLevelDown ci
27.425 + in result end)
27.426 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.427 +
27.428 +(* val moveActiveLevelUp : calcID -> XML.tree *)
27.429 +operation_setup move_active_levup = \<open>
27.430 + {from_lib = Codec.tree,
27.431 + to_lib = Codec.tree,
27.432 + action = (fn intree =>
27.433 + (let
27.434 + val (ci) = case intree of
27.435 + XML.Elem (("CALCITERATOR", []), [
27.436 + XML.Elem (("CALCID", []), [XML.Text ci])])
27.437 + => (str2int ci)
27.438 + | tree => raise ERROR ("move_active_levup: WRONG intree = " ^ xmlstr 0 tree)
27.439 + val result = Math_Engine.moveActiveLevelUp ci
27.440 + in result end)
27.441 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.442 +
27.443 +(* val moveActiveRoot : calcID -> XML.tree *)
27.444 +operation_setup moveactiveroot = \<open>
27.445 + {from_lib = Codec.int,
27.446 + to_lib = Codec.tree,
27.447 + action = (fn calcid =>
27.448 + let
27.449 + val result = Math_Engine.moveActiveRoot calcid
27.450 + in result end)}\<close>
27.451 +
27.452 +(* val moveActiveRootTEST : calcID -> XML.tree *)
27.453 +
27.454 +(* val moveActiveUp : calcID -> XML.tree *)
27.455 +operation_setup move_active_up = \<open>
27.456 + {from_lib = Codec.tree,
27.457 + to_lib = Codec.tree,
27.458 + action = (fn intree =>
27.459 + (let
27.460 + val (ci) = case intree of
27.461 + XML.Elem (("CALCITERATOR", []), [
27.462 + XML.Elem (("CALCID", []), [XML.Text ci])])
27.463 + => (str2int ci)
27.464 + | tree => raise ERROR ("move_active_up: WRONG intree = " ^ xmlstr 0 tree)
27.465 + val result = Math_Engine.moveActiveUp ci
27.466 + in result end)
27.467 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.468 +
27.469 +(* val moveCalcHead : calcID -> pos' -> XML.tree *)
27.470 +operation_setup move_calchead = \<open>
27.471 + {from_lib = Codec.tree,
27.472 + to_lib = Codec.tree,
27.473 + action = (fn intree =>
27.474 + (let
27.475 + val (ci, pos) = case intree of
27.476 + XML.Elem (("CALCITERATOR", []), [
27.477 + XML.Elem (("CALCID", []), [XML.Text ci]),
27.478 + pos as XML.Elem (("POSITION", []), _)])
27.479 + => (str2int ci, xml_to_pos pos)
27.480 + | tree => raise ERROR ("move_active_calchead: WRONG intree = " ^ xmlstr 0 tree)
27.481 + val result = Math_Engine.moveCalcHead ci pos
27.482 + in result end)
27.483 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.484 +
27.485 +(* val moveDown : calcID -> pos' -> XML.tree *)
27.486 +operation_setup move_down = \<open>
27.487 + {from_lib = Codec.tree,
27.488 + to_lib = Codec.tree,
27.489 + action = (fn intree =>
27.490 + (let
27.491 + val (ci, pos) = case intree of
27.492 + XML.Elem (("CALCITERATOR", []), [
27.493 + XML.Elem (("CALCID", []), [XML.Text ci]),
27.494 + pos as XML.Elem (("POSITION", []), _)])
27.495 + => (str2int ci, xml_to_pos pos)
27.496 + | tree => raise ERROR ("move_down: WRONG intree = " ^ xmlstr 0 tree)
27.497 + val result = Math_Engine.moveDown ci pos
27.498 + in result end)
27.499 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.500 +
27.501 +(* val moveLevelDown : calcID -> pos' -> XML.tree *)
27.502 +operation_setup move_levdn = \<open>
27.503 + {from_lib = Codec.tree,
27.504 + to_lib = Codec.tree,
27.505 + action = (fn intree =>
27.506 + (let
27.507 + val (ci, pos) = case intree of
27.508 + XML.Elem (("CALCITERATOR", []), [
27.509 + XML.Elem (("CALCID", []), [XML.Text ci]),
27.510 + pos as XML.Elem (("POSITION", []), _)])
27.511 + => (str2int ci, xml_to_pos pos)
27.512 + | tree => raise ERROR ("move_levdn: WRONG intree = " ^ xmlstr 0 tree)
27.513 + val result = Math_Engine.moveLevelDown ci pos
27.514 + in result end)
27.515 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.516 +
27.517 +(* val moveLevelUp : calcID -> pos' -> XML.tree *)
27.518 +operation_setup move_levup = \<open>
27.519 + {from_lib = Codec.tree,
27.520 + to_lib = Codec.tree,
27.521 + action = (fn intree =>
27.522 + (let
27.523 + val (ci, pos) = case intree of
27.524 + XML.Elem (("CALCITERATOR", []), [
27.525 + XML.Elem (("CALCID", []), [XML.Text ci]),
27.526 + pos as XML.Elem (("POSITION", []), _)])
27.527 + => (str2int ci, xml_to_pos pos)
27.528 + | tree => raise ERROR ("move_levup: WRONG intree = " ^ xmlstr 0 tree)
27.529 + val result = Math_Engine.moveLevelUp ci pos
27.530 + in result end)
27.531 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.532 +
27.533 +(* val moveRoot : calcID -> XML.tree *)
27.534 +operation_setup move_root = \<open>
27.535 + {from_lib = Codec.tree,
27.536 + to_lib = Codec.tree,
27.537 + action = (fn intree =>
27.538 + (let
27.539 + val (ci) = case intree of
27.540 + XML.Elem (("CALCITERATOR", []), [
27.541 + XML.Elem (("CALCID", []), [XML.Text ci])])
27.542 + => (str2int ci)
27.543 + | tree => raise ERROR ("move_root: WRONG intree = " ^ xmlstr 0 tree)
27.544 + val result = Math_Engine.moveRoot ci
27.545 + in result end)
27.546 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.547 +
27.548 +(* val moveUp : calcID -> pos' -> XML.tree *)
27.549 +operation_setup move_up = \<open>
27.550 + {from_lib = Codec.tree,
27.551 + to_lib = Codec.tree,
27.552 + action = (fn intree =>
27.553 + (let
27.554 + val (ci, pos) = case intree of
27.555 + XML.Elem (("CALCITERATOR", []), [
27.556 + XML.Elem (("CALCID", []), [XML.Text ci]),
27.557 + pos as XML.Elem (("POSITION", []), _)])
27.558 + => (str2int ci, xml_to_pos pos)
27.559 + | tree => raise ERROR ("move_up: WRONG intree = " ^ xmlstr 0 tree)
27.560 + val result = Math_Engine.moveUp ci pos
27.561 + in result end)
27.562 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.563 +
27.564 +(* val refFormula : calcID -> pos' -> XML.tree *)
27.565 +operation_setup refformula = \<open>
27.566 + {from_lib = Codec.tree,
27.567 + to_lib = Codec.tree,
27.568 + action = (fn intree =>
27.569 + (let
27.570 + val (ci, p) = case intree of
27.571 + XML.Elem (("REFFORMULA", []), [
27.572 + XML.Elem (("CALCID", []), [XML.Text ci]), p])
27.573 + => (ci, p)
27.574 + | tree => raise ERROR ("refformula: WRONG intree = " ^ xmlstr 0 tree)
27.575 + val SOME calcid = int_of_str ci
27.576 + val pos = xml_to_pos p
27.577 + val result = Math_Engine.refFormula calcid pos
27.578 + in result end)
27.579 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.580 +
27.581 +(* val refineProblem : calcID -> pos' -> guh -> XML.tree *)
27.582 +operation_setup refine_pbl = \<open>
27.583 + {from_lib = Codec.tree,
27.584 + to_lib = Codec.tree,
27.585 + action = (fn intree =>
27.586 + (let
27.587 + val (ci, pos, guh) = case intree of
27.588 + XML.Elem (("CONTEXTPBL", []), [
27.589 + XML.Elem (("CALCID", []), [XML.Text ci]),
27.590 + pos as XML.Elem (("POSITION", []), _),
27.591 + XML.Elem (("GUH", []), [XML.Text guh])])
27.592 + => (str2int ci, xml_to_pos pos, guh)
27.593 + | tree => raise ERROR ("refine_pbl: WRONG intree = " ^ xmlstr 0 tree)
27.594 + val result = Math_Engine.refineProblem ci pos guh
27.595 + in result end)
27.596 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.597 +
27.598 +(* val replaceFormula : calcID -> cterm' -> XML.tree *)
27.599 +operation_setup replace_form = \<open>
27.600 + {from_lib = Codec.tree,
27.601 + to_lib = Codec.tree,
27.602 + action = (fn intree =>
27.603 + (let
27.604 + val (calcid, cterm') = case intree of
27.605 + XML.Elem (("REPLACEFORMULA", []), [
27.606 + XML.Elem (("CALCID", []), [XML.Text ci]), form])
27.607 + => (ci |> int_of_str', form |> xml_to_formula |> term2str)
27.608 + | tree => raise ERROR ("replace_form: WRONG intree = " ^ xmlstr 0 tree)
27.609 + val result = Math_Engine.replaceFormula calcid cterm'
27.610 + in result end)
27.611 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.612 +
27.613 +(* val requestFillformula : calcID -> errpatID * fillpatID -> XML.tree NOT IMPL. IN isac-java *)
27.614 +operation_setup request_fill_form = \<open>
27.615 + {from_lib = Codec.tree,
27.616 + to_lib = Codec.tree,
27.617 + action = (fn intree =>
27.618 + (let
27.619 + val (ci, errpat_id, fillpat_id) = case intree of
27.620 + XML.Elem (("AUTOCALC", []), [
27.621 + XML.Elem (("CALCID", []), [XML.Text ci]),
27.622 + XML.Elem (("ERRPATTID", []), [XML.Text errpat_id]),
27.623 + XML.Elem (("FILLPATTID", []), [XML.Text fillpat_id])])
27.624 + => (str2int ci, errpat_id, fillpat_id)
27.625 + | tree => raise ERROR ("request_fill_form: WRONG intree = " ^ xmlstr 0 tree)
27.626 + val result = Math_Engine.requestFillformula ci (errpat_id, fillpat_id)
27.627 + in result end)
27.628 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.629 +
27.630 +(* val resetCalcHead : calcID -> XML.tree *)
27.631 +operation_setup reset_calchead = \<open>
27.632 + {from_lib = Codec.tree,
27.633 + to_lib = Codec.tree,
27.634 + action = (fn intree =>
27.635 + (let
27.636 + val (ci) = case intree of
27.637 + XML.Elem (("MODIFYCALCHEAD", []), [
27.638 + XML.Elem (("CALCID", []), [XML.Text ci])])
27.639 + => (str2int ci)
27.640 + | tree => raise ERROR ("reset_calchead: WRONG intree = " ^ xmlstr 0 tree)
27.641 + val result = Math_Engine.resetCalcHead ci
27.642 + in result end)
27.643 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.644 +
27.645 +(* val setContext : calcID -> pos' -> guh -> XML.tree *)
27.646 +operation_setup set_ctxt = \<open>
27.647 + {from_lib = Codec.tree,
27.648 + to_lib = Codec.tree,
27.649 + action = (fn intree =>
27.650 + (let
27.651 + val (ci, pos, guh) = case intree of
27.652 + XML.Elem (("CONTEXT", []), [
27.653 + XML.Elem (("CALCID", []), [XML.Text ci]),
27.654 + pos as XML.Elem (("POSITION", []), _),
27.655 + XML.Elem (("GUH", []), [XML.Text guh])])
27.656 + => (str2int ci, xml_to_pos pos, guh)
27.657 + | tree => raise ERROR ("set_ctxt: WRONG intree = " ^ xmlstr 0 tree)
27.658 + val result = Math_Engine.setContext ci pos guh
27.659 + in result end)
27.660 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.661 +
27.662 +(*//===vvv TODO ================================================================\\\\\\\\\\\\\\\\*)
27.663 +
27.664 +(* val setMethod : calcID -> metID -> XML.tree *)
27.665 +operation_setup set_met = \<open>
27.666 + {from_lib = Codec.tree,
27.667 + to_lib = Codec.tree,
27.668 + action = (fn intree =>
27.669 + (let
27.670 + val (ci, met_id) = case intree of
27.671 + XML.Elem (("MODIFYCALCHEAD", []), [
27.672 + XML.Elem (("CALCID", []), [XML.Text ci]),
27.673 + XML.Elem (("METHODID", []), [met_id])])
27.674 + => (str2int ci, xml_to_strs met_id)
27.675 + | tree => raise ERROR ("set_met: WRONG intree = " ^ xmlstr 0 tree)
27.676 + val result = Math_Engine.setMethod ci met_id
27.677 + in result end)
27.678 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.679 +
27.680 +(* val setNextTactic : calcID -> tac -> XML.tree *)
27.681 +operation_setup set_next_tac = \<open>
27.682 + {from_lib = Codec.tree,
27.683 + to_lib = Codec.tree,
27.684 + action = (fn intree =>
27.685 + (let
27.686 + val (ci, tac) = case intree of
27.687 + XML.Elem (("SETNEXTTACTIC", []), [
27.688 + XML.Elem (("CALCID", []), [XML.Text ci]),
27.689 + tac])
27.690 + => (str2int ci, xml_to_tac tac)
27.691 + | tree => raise ERROR ("set_next_tac: WRONG intree = " ^ xmlstr 0 tree)
27.692 + val result = Math_Engine.setNextTactic ci tac
27.693 + in result end)
27.694 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.695 +
27.696 +(*\\===^^^ TODO ================================================================///////////////*)
27.697 +
27.698 +(* val setProblem : calcID -> pblID -> XML.tree *)
27.699 +operation_setup set_pbl = \<open>
27.700 + {from_lib = Codec.tree,
27.701 + to_lib = Codec.tree,
27.702 + action = (fn intree =>
27.703 + (let
27.704 + val (ci, pbl_id) = case intree of
27.705 + XML.Elem (("MODIFYCALCHEAD", []), [
27.706 + XML.Elem (("CALCID", []), [XML.Text ci]),
27.707 + XML.Elem (("PROBLEMID", []), [pbl_id])])
27.708 + => (str2int ci, xml_to_strs pbl_id)
27.709 + | tree => raise ERROR ("set_pbl: WRONG intree = " ^ xmlstr 0 tree)
27.710 + val result = Math_Engine.setProblem ci pbl_id
27.711 + in result end)
27.712 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.713 +
27.714 +(* val setTheory : calcID -> thyID -> XML.tree *)
27.715 +operation_setup set_thy = \<open>
27.716 + {from_lib = Codec.tree,
27.717 + to_lib = Codec.tree,
27.718 + action = (fn intree =>
27.719 + (let
27.720 + val (ci, thy_id) = case intree of
27.721 + XML.Elem (("MODIFYCALCHEAD", []), [
27.722 + XML.Elem (("CALCID", []), [XML.Text ci]),
27.723 + XML.Elem (("THEORYID", []), [XML.Text thy_id])])
27.724 + => (str2int ci, thy_id)
27.725 + | tree => raise ERROR ("set_thy: WRONG intree = " ^ xmlstr 0 tree)
27.726 + val result = Math_Engine.setTheory ci thy_id
27.727 + in result end)
27.728 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
27.729 +
27.730 +end
28.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
28.2 +++ b/libisabelle-protocol/isabelle/2015/lib/classy/Classy.thy Fri Jan 22 15:53:13 2016 +0100
28.3 @@ -0,0 +1,22 @@
28.4 +theory Classy
28.5 +imports Pure
28.6 +keywords
28.7 + "ML.class" :: thy_decl % "ML" and
28.8 + "ML.instance" :: thy_decl % "ML" and
28.9 + "ML.print_classes" :: diag
28.10 +begin
28.11 +
28.12 +ML_file "ml_types.ML"
28.13 +ML_file "classy.ML"
28.14 +
28.15 +setup \<open>Classy.setup\<close>
28.16 +
28.17 +ML_file "pretty_class.ML"
28.18 +
28.19 +ML.class pretty = \<open>'a pretty_class\<close>
28.20 +
28.21 +ML.instance \<open>Pretty_Class.string\<close> :: pretty
28.22 +ML.instance \<open>Pretty_Class.pretty\<close> :: pretty
28.23 +ML.instance \<open>Pretty_Class.list\<close> :: pretty
28.24 +
28.25 +end
28.26 \ No newline at end of file
29.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
29.2 +++ b/libisabelle-protocol/isabelle/2015/lib/classy/Examples.thy Fri Jan 22 15:53:13 2016 +0100
29.3 @@ -0,0 +1,18 @@
29.4 +theory Examples
29.5 +imports Classy
29.6 +begin
29.7 +
29.8 +ML.print_classes
29.9 +
29.10 +ML\<open>format @{ML.resolve \<open>string list\<close> :: pretty} ["a", "b"] |> Pretty.writeln\<close> (* okay *)
29.11 +
29.12 +context begin
29.13 +
29.14 + (* conflicting instance *)
29.15 + ML.instance \<open>Pretty_Class.string\<close> :: pretty
29.16 +
29.17 + ML\<open>@{ML.resolve \<open>string\<close> :: pretty}\<close> (* error *)
29.18 +
29.19 +end
29.20 +
29.21 +end
29.22 \ No newline at end of file
30.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
30.2 +++ b/libisabelle-protocol/isabelle/2015/lib/classy/LICENSE Fri Jan 22 15:53:13 2016 +0100
30.3 @@ -0,0 +1,22 @@
30.4 +The MIT License (MIT)
30.5 +
30.6 +Copyright (c) 2015 Lars Hupel
30.7 +
30.8 +Permission is hereby granted, free of charge, to any person obtaining a copy
30.9 +of this software and associated documentation files (the "Software"), to deal
30.10 +in the Software without restriction, including without limitation the rights
30.11 +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
30.12 +copies of the Software, and to permit persons to whom the Software is
30.13 +furnished to do so, subject to the following conditions:
30.14 +
30.15 +The above copyright notice and this permission notice shall be included in all
30.16 +copies or substantial portions of the Software.
30.17 +
30.18 +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
30.19 +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
30.20 +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
30.21 +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
30.22 +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
30.23 +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
30.24 +SOFTWARE.
30.25 +
31.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
31.2 +++ b/libisabelle-protocol/isabelle/2015/lib/classy/README.md Fri Jan 22 15:53:13 2016 +0100
31.3 @@ -0,0 +1,2 @@
31.4 +# classy
31.5 +Type classes for Isabelle/ML
32.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
32.2 +++ b/libisabelle-protocol/isabelle/2015/lib/classy/Test.thy Fri Jan 22 15:53:13 2016 +0100
32.3 @@ -0,0 +1,50 @@
32.4 +theory Test
32.5 +imports Classy
32.6 +begin
32.7 +
32.8 +section \<open>Parsing and printing types\<close>
32.9 +
32.10 +ML\<open>
32.11 +fun check t =
32.12 + let
32.13 + val t' = ML_Types.read_ml_type t |> ML_Types.pretty |> Pretty.string_of |> YXML.content_of
32.14 + in
32.15 + if t <> t' then
32.16 + error t'
32.17 + else
32.18 + ()
32.19 + end
32.20 +\<close>
32.21 +
32.22 +ML\<open>check "'a"\<close>
32.23 +ML\<open>check "'a * 'b"\<close>
32.24 +ML\<open>check "'a * 'b * 'c"\<close>
32.25 +ML\<open>check "('a * 'b) * 'c"\<close>
32.26 +ML\<open>check "'a * ('b * 'c)"\<close>
32.27 +ML\<open>check "'a * 'b -> 'c"\<close>
32.28 +ML\<open>check "'a * 'b -> 'a * 'b"\<close>
32.29 +ML\<open>check "('a -> 'b) * ('a -> 'b)"\<close>
32.30 +ML\<open>check "('a, 'b) foo"\<close>
32.31 +ML\<open>check "'a foo"\<close>
32.32 +ML\<open>check "unit foo"\<close>
32.33 +ML\<open>check "unit * 'a"\<close>
32.34 +ML\<open>check "'a foo * 'b foo bar"\<close>
32.35 +ML\<open>check "('a, unit) foo"\<close>
32.36 +ML\<open>check "('a * 'b) foo"\<close>
32.37 +ML\<open>check "('a -> 'b) foo"\<close>
32.38 +ML\<open>check "('a -> 'b, 'c) foo"\<close>
32.39 +ML\<open>check "('a -> 'b, 'c * 'd) foo"\<close>
32.40 +ML\<open>check "'a foo bar baz"\<close>
32.41 +ML\<open>check "('a foo, 'b) bar Long.ident.baz"\<close>
32.42 +ML\<open>check "{a: int}"\<close>
32.43 +ML\<open>check "{a: int, b: float}"\<close>
32.44 +ML\<open>check "{a: int, b: 'a -> 'b}"\<close>
32.45 +
32.46 +section \<open>Instance resolution\<close>
32.47 +
32.48 +ML\<open>@{ML.resolve \<open>string\<close> :: pretty}\<close>
32.49 +ML\<open>@{ML.resolve \<open>string list\<close> :: pretty}\<close>
32.50 +ML\<open>@{ML.resolve \<open>string list list\<close> :: pretty}\<close>
32.51 +ML\<open>@{ML.resolve \<open>Pretty.T\<close> :: pretty}\<close>
32.52 +
32.53 +end
32.54 \ No newline at end of file
33.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
33.2 +++ b/libisabelle-protocol/isabelle/2015/lib/classy/classy.ML Fri Jan 22 15:53:13 2016 +0100
33.3 @@ -0,0 +1,173 @@
33.4 +signature CLASSY = sig
33.5 + val register_class: binding -> ML_Types.ml_type -> local_theory -> local_theory
33.6 + val register_class_cmd: binding -> string -> local_theory -> local_theory
33.7 +
33.8 + val register_instance_cmd: xstring * Position.T -> binding -> Input.source -> local_theory -> local_theory
33.9 +
33.10 + val check_class: Context.generic -> string * Position.T -> string
33.11 + val print_classes: Context.generic -> unit
33.12 +
33.13 + val resolve: string -> ML_Types.ml_type -> Context.generic -> string
33.14 +
33.15 + val setup: theory -> theory
33.16 +end
33.17 +
33.18 +structure Classy: CLASSY = struct
33.19 +
33.20 +type class_table = (ml_type * (ml_type * string) Name_Space.table) Name_Space.table
33.21 +
33.22 +exception DUP
33.23 +
33.24 +structure Classes = Generic_Data
33.25 +(
33.26 + type T = class_table
33.27 + val empty = Name_Space.empty_table "ML class"
33.28 + val merge = Name_Space.join_tables (fn _ => raise DUP) (* FIXME consistency check *)
33.29 + val extend = I
33.30 +)
33.31 +
33.32 +fun list_comb (term: string) (args: string list) =
33.33 + space_implode " " (enclose "(" ")" term :: map (enclose "(" ")") args)
33.34 +
33.35 +fun product [] = [[]]
33.36 + | product (xs :: xss) =
33.37 + maps (fn xs' => map (fn x => x :: xs') xs) (product xss)
33.38 +
33.39 +
33.40 +fun solve entries problem =
33.41 + let
33.42 + fun find (typ, term) =
33.43 + let
33.44 + val (args, candidate) = ML_Types.strip_fun typ
33.45 + in
33.46 + case ML_Types.match candidate problem [] of
33.47 + SOME env =>
33.48 + map (ML_Types.subst env) args
33.49 + |> map (solve entries)
33.50 + |> product
33.51 + |> map (list_comb term)
33.52 + | NONE => []
33.53 + end
33.54 + in
33.55 + maps find entries
33.56 + end
33.57 +
33.58 +fun resolve class typ context =
33.59 + let
33.60 + val classes = Classes.get context
33.61 + val (constructor, table) = Name_Space.get classes class
33.62 + val ML_Types.Con (name, [ML_Types.Var _]) = constructor
33.63 + val entries = map snd (Name_Space.extern_table true (Context.proof_of context) table)
33.64 + val problem = ML_Types.Con (name, [typ])
33.65 + val solutions = solve entries problem
33.66 + in
33.67 + case solutions of
33.68 + [] => error "no solutions"
33.69 + | [solution] => enclose "(" ")" solution
33.70 + | _ => error "too many solutions"
33.71 + end
33.72 +
33.73 +fun check_class context raw_binding =
33.74 + fst (Name_Space.check context (Classes.get context) raw_binding)
33.75 +
33.76 +val antiquote_setup =
33.77 + ML_Antiquotation.inline (Binding.qualify true "ML" @{binding class})
33.78 + (Scan.state -- Scan.lift (Parse.position Args.name) >>
33.79 + (fn (context, binding) => quote (check_class context binding))) #>
33.80 + ML_Antiquotation.inline (Binding.qualify true "ML" @{binding resolve})
33.81 + (Scan.state -- Scan.lift (Parse.ML_source --| @{keyword "::"} -- Parse.position Args.name) >>
33.82 + (fn (context, (source, binding)) =>
33.83 + resolve (check_class context binding) (ML_Types.read_ml_type (Input.source_content source)) context))
33.84 +
33.85 +fun pretty_classes context =
33.86 + let
33.87 + val table = Classes.get context
33.88 + val ctxt = Context.proof_of context
33.89 + val space = Name_Space.space_of_table table
33.90 + val entries = Name_Space.extern_table true ctxt table
33.91 +
33.92 + fun pretty_class ((class, _), (typ, sub_table)) =
33.93 + let
33.94 + val header = Pretty.block [Name_Space.pretty ctxt space class, Pretty.str ":", Pretty.brk 1, ML_Types.pretty typ]
33.95 +
33.96 + val sub_space = Name_Space.space_of_table sub_table
33.97 + val sub_entries = Name_Space.extern_table true ctxt sub_table
33.98 +
33.99 + fun pretty_instance ((instance, _), (typ, _)) =
33.100 + Pretty.item [Name_Space.pretty ctxt sub_space instance, Pretty.str ":", Pretty.brk 1, ML_Types.pretty typ]
33.101 +
33.102 + val instances = map pretty_instance sub_entries
33.103 + in
33.104 + Pretty.item (Pretty.fbreaks (header :: instances))
33.105 + end
33.106 + in
33.107 + Pretty.big_list "Classes" (map pretty_class entries)
33.108 + end
33.109 +
33.110 +val print_classes =
33.111 + Pretty.writeln o pretty_classes
33.112 +
33.113 +fun register_class binding typ =
33.114 + let
33.115 + val name =
33.116 + (case typ of
33.117 + ML_Types.Con (name, [ML_Types.Var _]) => name
33.118 + | _ => error "Malformed type")
33.119 + fun decl _ context =
33.120 + let
33.121 + val classes = Classes.get context
33.122 + val table = Name_Space.empty_table ("ML instances for " ^ name)
33.123 + val (_, classes') = Name_Space.define context true (binding, (typ, table)) classes
33.124 + in
33.125 + Classes.put classes' context
33.126 + end
33.127 + in
33.128 + Local_Theory.declaration {syntax = false, pervasive = false} decl
33.129 + end
33.130 +
33.131 +fun register_class_cmd binding typ =
33.132 + register_class binding (ML_Types.read_ml_type typ)
33.133 +
33.134 +fun register_instance_cmd raw_binding binding source lthy =
33.135 + let
33.136 + val typ = ML_Types.ml_type_of lthy (Input.source_content source)
33.137 + (* doesn't have any effect except for markup *)
33.138 + val _ = ML_Context.eval_source_in (SOME lthy) ML_Compiler.flags source
33.139 +
33.140 + (* FIXME check correct type *)
33.141 +
33.142 + fun decl _ context =
33.143 + let
33.144 + val classes = Classes.get context
33.145 + val (key, _) = Name_Space.check context classes raw_binding
33.146 + val upd = Name_Space.define context true (binding, (typ, Input.source_content source)) #> snd
33.147 + val classes' = Name_Space.map_table_entry key (apsnd upd) classes
33.148 + in Classes.put classes' context end
33.149 + in
33.150 + Local_Theory.declaration {syntax = false, pervasive = false} decl lthy
33.151 + end
33.152 +
33.153 +val _ =
33.154 + Outer_Syntax.local_theory @{command_keyword "ML.class"} "register new type class"
33.155 + (Parse.binding --| @{keyword "="} -- Parse.cartouche
33.156 + >> (fn (binding, typ) => register_class_cmd binding typ))
33.157 +
33.158 +val _ =
33.159 + let
33.160 + val opt_binding =
33.161 + Parse.binding --| @{keyword "="} ||
33.162 + Parse.position (Scan.succeed ()) >>
33.163 + (fn ((), pos) => Binding.make ("instance" ^ Markup.print_int (serial ()), pos))
33.164 + in
33.165 + Outer_Syntax.local_theory @{command_keyword "ML.instance"} "register new type class instance"
33.166 + (opt_binding -- (Parse.ML_source --| @{keyword "::"} -- Parse.position Args.name)
33.167 + >> (fn (binding, (source, name)) => register_instance_cmd name binding source))
33.168 + end
33.169 +
33.170 +val _ =
33.171 + Outer_Syntax.command @{command_keyword "ML.print_classes"} "print all registered classes"
33.172 + (Scan.succeed (Toplevel.keep (print_classes o Toplevel.generic_theory_of)))
33.173 +
33.174 +val setup = antiquote_setup
33.175 +
33.176 +end
33.177 \ No newline at end of file
34.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
34.2 +++ b/libisabelle-protocol/isabelle/2015/lib/classy/ml_types.ML Fri Jan 22 15:53:13 2016 +0100
34.3 @@ -0,0 +1,215 @@
34.4 +signature ML_TYPES = sig
34.5 + datatype ml_type =
34.6 + Var of string |
34.7 + Con of string * ml_type list |
34.8 + Tuple of ml_type list |
34.9 + Fun of ml_type * ml_type |
34.10 + Record of (string * ml_type) list
34.11 +
34.12 + val unit: ml_type
34.13 + val canonicalize: ml_type -> ml_type
34.14 +
34.15 + val read_ml_type: string -> ml_type
34.16 + val ml_type_of: Proof.context -> string -> ml_type
34.17 +
34.18 + val pretty: ml_type -> Pretty.T
34.19 +
34.20 + type env = (string * ml_type) list
34.21 + val subst: env -> ml_type -> ml_type
34.22 + val match: ml_type -> ml_type -> env -> env option
34.23 +
34.24 + val strip_fun: ml_type -> ml_type list * ml_type
34.25 +end
34.26 +
34.27 +structure ML_Types: ML_TYPES = struct
34.28 +
34.29 +datatype ml_type =
34.30 + Var of string |
34.31 + Con of string * ml_type list |
34.32 + Tuple of ml_type list |
34.33 + Fun of ml_type * ml_type |
34.34 + Record of (string * ml_type) list
34.35 +
34.36 +val unit = Con ("unit", [])
34.37 +
34.38 +type env = (string * ml_type) list
34.39 +
34.40 +fun subst env (Con (name, ts)) = Con (name, map (subst env) ts)
34.41 + | subst env (Var name) = the_default (Var name) (AList.lookup op = env name)
34.42 + | subst env (Tuple ts) = Tuple (map (subst env) ts)
34.43 + | subst env (Fun (x, y)) = Fun (subst env x, subst env y)
34.44 + | subst env (Record fs) = Record (map (apsnd (subst env)) fs)
34.45 +
34.46 +fun match (Var name) t env =
34.47 + (case AList.lookup op = env name of
34.48 + NONE => SOME ((name, t) :: env)
34.49 + | SOME t' => if t = t' then SOME env else NONE)
34.50 + | match (Fun (x1, y1)) (Fun (x2, y2)) env =
34.51 + Option.mapPartial (match y1 y2) (match x1 x2 env)
34.52 + | match (Con (name1, ts1)) (Con (name2, ts2)) env =
34.53 + if name1 = name2 then match_list ts1 ts2 env else NONE
34.54 + | match (Tuple ts1) (Tuple ts2) env = match_list ts1 ts2 env
34.55 + | match (Record fs1) (Record fs2) env =
34.56 + if map fst fs1 = map fst fs2 then
34.57 + match_list (map snd fs1) (map snd fs2) env
34.58 + else
34.59 + NONE
34.60 + | match _ _ _ = NONE
34.61 +and match_list [] [] env = SOME env
34.62 + | match_list (t :: ts) (u :: us) env =Option.mapPartial (match t u) (match_list ts us env)
34.63 + | match_list _ _ _ = NONE
34.64 +
34.65 +fun strip_fun (Fun (x, y)) = let val (args, res) = strip_fun y in (x :: args, res) end
34.66 + | strip_fun t = ([], t)
34.67 +
34.68 +fun canonicalize (Var name) = Var name
34.69 + | canonicalize (Con (name, ts)) = Con (name, map canonicalize ts)
34.70 + | canonicalize (Tuple []) = unit
34.71 + | canonicalize (Tuple [t]) = canonicalize t
34.72 + | canonicalize (Tuple ts) = Tuple (map canonicalize ts)
34.73 + | canonicalize (Fun (t, u)) = Fun (canonicalize t, canonicalize u)
34.74 + | canonicalize (Record []) = unit
34.75 + | canonicalize (Record es) = Record (sort_wrt fst (map (apsnd canonicalize) es))
34.76 +
34.77 +val pretty =
34.78 + let
34.79 + datatype shape = SVar | SCon | STuple | SFun_Left | SRoot
34.80 +
34.81 + fun prec SVar _ = error "impossible"
34.82 + | prec SRoot _ = true
34.83 + | prec _ (Var _) = true
34.84 + | prec _ (Record _) = true
34.85 + | prec STuple (Con _) = true
34.86 + | prec STuple _ = false
34.87 + | prec SFun_Left (Con _) = true
34.88 + | prec SFun_Left (Tuple _) = true
34.89 + | prec SFun_Left (Fun _) = false
34.90 + | prec SCon (Con _) = true
34.91 + | prec SCon _ = false
34.92 +
34.93 + fun par n t p = if prec n t then p else Pretty.block [Pretty.str "(", p, Pretty.str ")"]
34.94 +
34.95 + fun aux s t =
34.96 + (case t of
34.97 + Var id => [Pretty.str id]
34.98 + | Tuple ts => Pretty.separate " *" (map (aux STuple) ts)
34.99 + | Fun (arg, res) =>
34.100 + [aux SFun_Left arg, Pretty.brk 1, Pretty.str "->", Pretty.brk 1, aux SRoot res]
34.101 + | Con (id, [t]) =>
34.102 + [aux SCon t, Pretty.brk 1, Pretty.str id]
34.103 + | Con (id, []) =>
34.104 + [Pretty.str id]
34.105 + | Con (id, ts) =>
34.106 + [Pretty.block (Pretty.str "(" :: Pretty.separate "," (map (aux SRoot) ts) @ [Pretty.str ")"]), Pretty.brk 1, Pretty.str id]
34.107 + | Record es =>
34.108 + Pretty.str "{" :: Pretty.separate "," (map (fn (name, t) => Pretty.block [Pretty.str name, Pretty.str ":", Pretty.brk 1, aux SRoot t]) es) @ [Pretty.str "}"])
34.109 + |> Pretty.block |> par s t
34.110 + in
34.111 + aux SRoot o canonicalize
34.112 + end
34.113 +
34.114 +type token = ML_Lex.token_kind * string
34.115 +
34.116 +type 'a parser = token list -> 'a * token list
34.117 +
34.118 +fun kind k: string parser = Scan.one (equal k o fst) >> snd
34.119 +fun tok t: unit parser = Scan.one (equal t) >> K ()
34.120 +fun keyword k: unit parser = tok (ML_Lex.Keyword, k)
34.121 +val open_parenthesis: unit parser = keyword "("
34.122 +val closed_parenthesis: unit parser = keyword ")"
34.123 +val open_brace: unit parser = keyword "{"
34.124 +val closed_brace: unit parser = keyword "}"
34.125 +val colon: unit parser = keyword ":"
34.126 +val comma: unit parser = keyword ","
34.127 +val arrow: unit parser = keyword "->"
34.128 +val asterisk: unit parser = tok (ML_Lex.Ident, "*")
34.129 +
34.130 +val ident: string parser =
34.131 + kind ML_Lex.Long_Ident ||
34.132 + Scan.one (fn (k, c) => k = ML_Lex.Ident andalso c <> "*") >> snd
34.133 +
34.134 +fun intersep p sep =
34.135 + (p ::: Scan.repeat (sep |-- p)) || Scan.succeed []
34.136 +
34.137 +val typ =
34.138 + let
34.139 + (* code partly lifted from Spec_Check *)
34.140 + fun make_con [] = raise Empty
34.141 + | make_con [c] = c
34.142 + | make_con (Con (s, _) :: cl) = Con (s, [make_con cl]);
34.143 +
34.144 + fun typ s = (func || tuple || typ_single) s
34.145 + and typ_arg s = (tuple || typ_single) s
34.146 + and typ_single s = (con || typ_basic) s
34.147 + and typ_basic s =
34.148 + (var
34.149 + || open_brace |-- record --| closed_brace
34.150 + || open_parenthesis |-- typ --| closed_parenthesis) s
34.151 + and list s = (open_parenthesis |-- typ -- Scan.repeat1 (comma |-- typ) --| closed_parenthesis >> op ::) s
34.152 + and var s = (kind ML_Lex.Type_Var >> Var) s
34.153 + and con s = ((con_nest
34.154 + || typ_basic -- con_nest >> (fn (b, Con (t, _) :: tl) => Con (t, [b]) :: tl)
34.155 + || list -- con_nest >> (fn (l, Con (t, _) :: tl) => Con (t, l) :: tl))
34.156 + >> (make_con o rev)) s
34.157 + and con_nest s = Scan.unless var (Scan.repeat1 (ident >> (Con o rpair []))) s
34.158 + and func s = (typ_arg --| arrow -- typ >> Fun) s
34.159 + and record s = (intersep (kind ML_Lex.Ident -- (colon |-- typ)) comma >> Record) s
34.160 + and tuple s = (typ_single -- Scan.repeat1 (asterisk |-- typ_single)
34.161 + >> (fn (t, tl) => Tuple (t :: tl))) s
34.162 + in typ end
34.163 +
34.164 +fun read_binding s =
34.165 + let
34.166 + val colon = (ML_Lex.Keyword, ":")
34.167 + val semicolon = (ML_Lex.Keyword, ";")
34.168 + fun unpack_tok tok = (ML_Lex.kind_of tok, ML_Lex.content_of tok)
34.169 + val toks = filter (not o equal ML_Lex.Space o fst) (map unpack_tok (ML_Lex.tokenize s))
34.170 + val junk = (Scan.many (not o equal colon) -- tok colon) >> K ()
34.171 + val stopper = Scan.stopper (K semicolon) (equal semicolon)
34.172 + val all = junk |-- Scan.finite stopper typ
34.173 + val (typ, rest) = all toks
34.174 + in
34.175 + if null rest then
34.176 + typ
34.177 + else
34.178 + error "Could not fully parse type"
34.179 + end
34.180 +
34.181 +fun read_ml_type s =
34.182 + let
34.183 + (* FIXME deduplicate *)
34.184 + val semicolon = (ML_Lex.Keyword, ";")
34.185 + fun unpack_tok tok = (ML_Lex.kind_of tok, ML_Lex.content_of tok)
34.186 + val toks = filter (not o equal ML_Lex.Space o fst) (map unpack_tok (ML_Lex.tokenize s))
34.187 + val stopper = Scan.stopper (K semicolon) (equal semicolon)
34.188 + val all = Scan.finite stopper typ
34.189 + val (typ, rest) = all toks
34.190 + in
34.191 + if null rest then
34.192 + typ
34.193 + else
34.194 + error "Could not fully parse type"
34.195 + end
34.196 +
34.197 +fun ml_type_of ctxt s =
34.198 + let
34.199 + (* code partly lifted from Spec_Check *)
34.200 + val return = Unsynchronized.ref NONE
34.201 + val s = "(fn () => (" ^ s ^ "))"
34.202 + val use_context: use_context =
34.203 + {tune_source = #tune_source ML_Env.local_context,
34.204 + name_space = #name_space ML_Env.local_context,
34.205 + str_of_pos = #str_of_pos ML_Env.local_context,
34.206 + print = fn r => return := SOME r,
34.207 + error = #error ML_Env.local_context}
34.208 + val _ =
34.209 + Context.setmp_thread_data (SOME (Context.Proof ctxt))
34.210 + (fn () => Secure.use_text use_context (0, "generated code") true s) ()
34.211 + val (Fun (Con ("unit", []), typ)) = read_binding (the (! return))
34.212 + in
34.213 + typ
34.214 + end
34.215 +
34.216 +end
34.217 +
34.218 +type ml_type = ML_Types.ml_type
35.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
35.2 +++ b/libisabelle-protocol/isabelle/2015/lib/classy/pretty_class.ML Fri Jan 22 15:53:13 2016 +0100
35.3 @@ -0,0 +1,12 @@
35.4 +datatype 'a pretty_class = Pretty of ('a -> Pretty.T)
35.5 +
35.6 +fun format (Pretty f) = f
35.7 +
35.8 +structure Pretty_Class = struct
35.9 +
35.10 +val string: string pretty_class = Pretty Pretty.str
35.11 +val pretty: Pretty.T pretty_class = Pretty I
35.12 +fun list (Pretty f): 'a list pretty_class =
35.13 + Pretty (fn xs => Pretty.block (Pretty.str "[" :: Pretty.separate "," (map f xs) @ [Pretty.str "]"]))
35.14 +
35.15 +end
35.16 \ No newline at end of file
36.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
36.2 +++ b/libisabelle-protocol/operations/Basic.thy Fri Jan 22 15:53:13 2016 +0100
36.3 @@ -0,0 +1,46 @@
36.4 +theory Basic
36.5 +imports "../isabelle/2015/Protocol"
36.6 +begin
36.7 +
36.8 +operation_setup hello = \<open>
36.9 + {from_lib = Codec.string,
36.10 + to_lib = Codec.string,
36.11 + action = (fn data => "Hello " ^ data)}\<close>
36.12 +
36.13 +operation_setup (sequential, bracket) use_thys = \<open>
36.14 + {from_lib = Codec.list Codec.string,
36.15 + to_lib = Codec.unit,
36.16 + action = Thy_Info.use_thys o map (rpair Position.none)}\<close>
36.17 +
36.18 +text \<open>
36.19 + The read_term operation performs both parsing and checking at once, because we do not want to
36.20 + send back parsed, but un-checked terms to the JVM. They may contain weird position information
36.21 + which are difficult to get rid of and confuse the codecs.
36.22 +\<close>
36.23 +
36.24 +operation_setup read_term = \<open>
36.25 + {from_lib = Codec.triple Codec.string Codec.typ Codec.string,
36.26 + to_lib = Codec.option Codec.term,
36.27 + action = (fn (raw_term, typ, thy_name) =>
36.28 + let
36.29 + val thy = Thy_Info.get_theory thy_name
36.30 + val ctxt = Proof_Context.init_global thy
36.31 + in
36.32 + try (Syntax.parse_term ctxt) raw_term
36.33 + |> Option.map (Type.constraint typ)
36.34 + |> Option.mapPartial (try (Syntax.check_term ctxt))
36.35 + end)}\<close>
36.36 +
36.37 +operation_setup check_term = \<open>
36.38 + {from_lib = Codec.triple Codec.term Codec.typ Codec.string,
36.39 + to_lib = Codec.option Codec.term,
36.40 + action = (fn (term, typ, thy_name) =>
36.41 + let
36.42 + val thy = Thy_Info.get_theory thy_name
36.43 + val ctxt = Proof_Context.init_global thy
36.44 + val term' = Type.constraint typ term
36.45 + in
36.46 + try (Syntax.check_term ctxt) term'
36.47 + end)}\<close>
36.48 +
36.49 +end
37.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
37.2 +++ b/libisabelle-protocol/operations/HOL_Operations.thy Fri Jan 22 15:53:13 2016 +0100
37.3 @@ -0,0 +1,16 @@
37.4 +theory HOL_Operations
37.5 +imports "../isabelle/2015/Protocol" Main
37.6 +begin
37.7 +
37.8 +operation_setup mk_int = \<open>
37.9 + {from_lib = Codec.int,
37.10 + to_lib = Codec.term,
37.11 + action = HOLogic.mk_number @{typ int}}\<close>
37.12 +
37.13 +operation_setup mk_list = \<open>
37.14 + {from_lib = Codec.tuple Codec.typ (Codec.list Codec.term),
37.15 + to_lib = Codec.term,
37.16 + action = uncurry HOLogic.mk_list}
37.17 +\<close>
37.18 +
37.19 +end
38.1 --- a/src/Tools/isac/ROOT Thu Jan 21 17:29:33 2016 +0100
38.2 +++ b/src/Tools/isac/ROOT Fri Jan 22 15:53:13 2016 +0100
38.3 @@ -35,4 +35,4 @@
38.4 For installation see http://www.ist.tugraz.at/isac
38.5 *}
38.6 options [document = false (*, browser_info = true*)]
38.7 - theories Build_Isac "~~/libisabelle-protocol/isabelle-2015/Protocol"
38.8 + theories Build_Isac "~~/libisabelle-protocol/isabelle/2015/Protocol" "~~/libisabelle-protocol/operations/Basic"