1.1 --- a/libisabelle-protocol/LICENSE Sat Feb 06 17:20:08 2016 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,22 +0,0 @@
1.4 -The MIT License (MIT)
1.5 -
1.6 -Copyright (c) 2015 Lars Hupel
1.7 -
1.8 -Permission is hereby granted, free of charge, to any person obtaining a copy
1.9 -of this software and associated documentation files (the "Software"), to deal
1.10 -in the Software without restriction, including without limitation the rights
1.11 -to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
1.12 -copies of the Software, and to permit persons to whom the Software is
1.13 -furnished to do so, subject to the following conditions:
1.14 -
1.15 -The above copyright notice and this permission notice shall be included in all
1.16 -copies or substantial portions of the Software.
1.17 -
1.18 -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
1.19 -IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
1.20 -FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
1.21 -AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
1.22 -LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
1.23 -OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
1.24 -SOFTWARE.
1.25 -
2.1 --- a/libisabelle-protocol/README.md Sat Feb 06 17:20:08 2016 +0100
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,2 +0,0 @@
2.4 -# libisabelle-protocol
2.5 -Isabelle backend for the libisabelle protocol
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/libisabelle-protocol/ROOT Wed Apr 06 16:56:47 2016 +0200
3.3 @@ -0,0 +1,12 @@
3.4 +session Protocol = Classy +
3.5 + theories
3.6 + "protocol/Protocol"
3.7 + "protocol/Codec_Test"
3.8 + "operations/Basic"
3.9 +
3.10 +session "HOL-Protocol" = "HOL-Classy" +
3.11 + theories
3.12 + "protocol/Protocol"
3.13 + "protocol/Codec_Test"
3.14 + "operations/Basic"
3.15 + "operations/HOL_Operations"
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/libisabelle-protocol/ROOTS Wed Apr 06 16:56:47 2016 +0200
4.3 @@ -0,0 +1,1 @@
4.4 +lib/classy
5.1 --- a/libisabelle-protocol/common/Codec_Test.thy Sat Feb 06 17:20:08 2016 +0100
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,36 +0,0 @@
5.4 -theory Codec_Test
5.5 -imports Common "~~/src/Tools/Spec_Check/Spec_Check"
5.6 -begin
5.7 -
5.8 -ML\<open>
5.9 -fun check_for str =
5.10 - let
5.11 - val prop =
5.12 - "ALL x. (let val c = (" ^ str ^ ") in Codec.decode c (Codec.encode c x) = Codec.Success x end)"
5.13 - in check_property prop end
5.14 -
5.15 -fun gen_unit r =
5.16 - ((), r)
5.17 -\<close>
5.18 -
5.19 -ML_command\<open>
5.20 - check_for "Codec.unit";
5.21 - check_for "Codec.int";
5.22 - check_for "Codec.bool";
5.23 - check_for "Codec.string";
5.24 - check_for "Codec.tuple Codec.int Codec.int";
5.25 - check_for "Codec.tuple Codec.string Codec.unit";
5.26 - check_for "Codec.list Codec.unit";
5.27 - check_for "Codec.list Codec.int";
5.28 - check_for "Codec.list Codec.string";
5.29 - check_for "Codec.list (Codec.list Codec.string)";
5.30 - check_for "Codec.list (Codec.tuple Codec.int Codec.int)";
5.31 - check_for "Codec.tuple Codec.int (Codec.list Codec.int)";
5.32 - check_for "Codec.option Codec.int";
5.33 - check_for "Codec.option (Codec.list Codec.int)";
5.34 - check_for "Codec.list (Codec.option (Codec.int))";
5.35 - check_for "Codec.term";
5.36 - check_for "Codec.typ";
5.37 -\<close>
5.38 -
5.39 -end
6.1 --- a/libisabelle-protocol/common/Common.thy Sat Feb 06 17:20:08 2016 +0100
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,8 +0,0 @@
6.4 -theory Common
6.5 -imports Pure
6.6 -begin
6.7 -
6.8 -ML_file "codec.ML"
6.9 -ML_file "protocol.ML"
6.10 -
6.11 -end
6.12 \ No newline at end of file
7.1 --- a/libisabelle-protocol/common/codec.ML Sat Feb 06 17:20:08 2016 +0100
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,242 +0,0 @@
7.4 -signature CODEC = sig
7.5 - datatype 'a result = Success of 'a | Failure of string * XML.body
7.6 - datatype ('a, 'b) either = Left of 'a | Right of 'b
7.7 - type 'a codec
7.8 -
7.9 - val the_success: 'a result -> 'a
7.10 -
7.11 - val map_result: ('a -> 'b) -> 'a result -> 'b result
7.12 - val bind_result: ('a -> 'b result) -> 'a result -> 'b result
7.13 - val sequence_results: 'a result list -> 'a list result
7.14 - val traverse_results: ('a -> 'b result) -> 'a list -> 'b list result
7.15 -
7.16 - val transform: ('a -> 'b) -> ('b -> 'a) -> 'a codec -> 'b codec
7.17 - val encode: 'a codec -> 'a -> XML.tree
7.18 - val decode: 'a codec -> XML.tree -> 'a result
7.19 -
7.20 - val basic: {encode: 'a -> XML.tree, decode: XML.tree -> 'a result} -> 'a codec
7.21 -
7.22 - val variant: ('a -> (int * XML.tree)) -> (int -> (XML.tree -> 'a result) option) -> string -> 'a codec
7.23 - val tagged: string -> 'a codec -> 'a codec
7.24 -
7.25 - val unit: unit codec
7.26 - val bool: bool codec
7.27 - val string: string codec
7.28 - val int: int codec
7.29 - val list: 'a codec -> 'a list codec
7.30 - val tuple: 'a codec -> 'b codec -> ('a * 'b) codec
7.31 - val triple: 'a codec -> 'b codec -> 'c codec -> ('a * 'b * 'c) codec
7.32 - val either: 'a codec -> 'b codec -> ('a, 'b) either codec
7.33 - val option: 'a codec -> 'a option codec
7.34 - val tree: XML.tree codec
7.35 -
7.36 - val sort: sort codec
7.37 - val typ: typ codec
7.38 - val term: term codec
7.39 -
7.40 - exception GENERIC of string
7.41 - val exn: exn codec
7.42 - val exn_result: 'a codec -> 'a Exn.result codec
7.43 -
7.44 - val id: XML.tree codec (* internal *)
7.45 -end
7.46 -
7.47 -structure Codec: CODEC = struct
7.48 -
7.49 -datatype 'a result = Success of 'a | Failure of string * XML.body
7.50 -datatype ('a, 'b) either = Left of 'a | Right of 'b
7.51 -
7.52 -fun map_result f (Success a) = Success (f a)
7.53 - | map_result _ (Failure (msg, body)) = Failure (msg, body)
7.54 -
7.55 -fun bind_result f (Success a) = f a
7.56 - | bind_result _ (Failure (msg, body)) = Failure (msg, body)
7.57 -
7.58 -fun traverse_results _ [] = Success []
7.59 - | traverse_results f (x :: xs) =
7.60 - case f x of
7.61 - Success y => map_result (fn ys => y :: ys) (traverse_results f xs)
7.62 - | Failure (msg, body) => Failure (msg, body)
7.63 -
7.64 -fun sequence_results xs = traverse_results I xs
7.65 -
7.66 -fun the_success (Success a) = a
7.67 - | the_success _ = raise Fail "unexpected failure"
7.68 -
7.69 -fun add_tag tag idx body =
7.70 - let
7.71 - val attrs = case idx of SOME i => [("idx", XML.Encode.int_atom i)] | _ => []
7.72 - in XML.Elem (("tag", ("type", tag) :: attrs), body) end
7.73 -
7.74 -fun expect_tag tag tree =
7.75 - case tree of
7.76 - XML.Elem (("tag", [("type", tag')]), body) =>
7.77 - if tag = tag' then
7.78 - Success body
7.79 - else
7.80 - Failure ("tag mismatch: expected " ^ tag ^ ", got " ^ tag', [tree])
7.81 - | _ =>
7.82 - Failure ("tag " ^ tag ^ " expected", [tree])
7.83 -
7.84 -fun expect_tag' tag tree =
7.85 - case tree of
7.86 - XML.Elem (("tag", [("type", tag'), ("idx", i)]), body) =>
7.87 - if tag = tag' then
7.88 - Success (XML.Decode.int_atom i, body)
7.89 - handle XML.XML_ATOM err => Failure (err, [tree])
7.90 - else
7.91 - Failure ("tag mismatch: expected " ^ tag ^ ", got " ^ tag', [tree])
7.92 - | _ =>
7.93 - Failure ("indexed tag " ^ tag ^ " expected", [tree])
7.94 -
7.95 -
7.96 -abstype 'a codec = Codec of {encode: 'a -> XML.tree, decode: XML.tree -> 'a result} with
7.97 -
7.98 -val basic = Codec
7.99 -
7.100 -fun encode (Codec {encode, ...}) = encode
7.101 -fun decode (Codec {decode, ...}) = decode
7.102 -
7.103 -fun transform f g (Codec {encode, decode}) = Codec
7.104 - {encode = g #> encode,
7.105 - decode = decode #> map_result f}
7.106 -
7.107 -fun list a = Codec
7.108 - {encode = map (encode a) #> add_tag "list" NONE,
7.109 - decode = expect_tag "list" #> bind_result (traverse_results (decode a))}
7.110 -
7.111 -fun tuple a b = Codec
7.112 - {encode = (fn (x, y) => add_tag "tuple" NONE [encode a x, encode b y]),
7.113 - decode = expect_tag "tuple" #> bind_result (fn body =>
7.114 - case body of
7.115 - [x, y] => decode a x |> bind_result (fn x' => decode b y |> map_result (pair x'))
7.116 - | _ => Failure ("invalid structure", body))}
7.117 -
7.118 -fun variant enc dec tag = Codec
7.119 - {encode = (fn a => let val (idx, tree) = enc a in add_tag tag (SOME idx) [tree] end),
7.120 - decode = (fn tree => expect_tag' tag tree |> bind_result (fn (idx, body) =>
7.121 - case (body, dec idx) of
7.122 - ([tree'], SOME res) => res tree'
7.123 - | (_, SOME _) => Failure ("invalid structure", [tree])
7.124 - | (_, NONE) => Failure ("invalid index " ^ Markup.print_int idx, [tree])))}
7.125 -
7.126 -fun tagged tag a = Codec
7.127 - {encode = encode a #> single #> add_tag tag NONE,
7.128 - decode = expect_tag tag #> bind_result (fn body =>
7.129 - case body of
7.130 - [tree] => decode a tree
7.131 - | _ => Failure ("invalid structure", body))}
7.132 -
7.133 -val unit = Codec
7.134 - {encode = K (add_tag "unit" NONE []),
7.135 - decode = expect_tag "unit" #> bind_result (fn body =>
7.136 - case body of
7.137 - [] => Success ()
7.138 - | _ => Failure ("expected nothing", body))}
7.139 -
7.140 -fun text to from = Codec
7.141 - {encode = XML.Text o to,
7.142 - decode =
7.143 - (fn tree as XML.Text content =>
7.144 - (case from content of
7.145 - NONE => Failure ("decoding failed", [tree]) |
7.146 - SOME a => Success a)
7.147 - | tree => Failure ("expected text tree", [tree]))}
7.148 -
7.149 -val id = Codec {encode = I, decode = Success}
7.150 -
7.151 -end
7.152 -
7.153 -val int = tagged "int" (text Markup.print_int (Exn.get_res o Exn.capture Markup.parse_int))
7.154 -val bool = tagged "bool" (text Markup.print_bool (Exn.get_res o Exn.capture Markup.parse_bool))
7.155 -val string = tagged "string" (text I SOME)
7.156 -
7.157 -val tree = tagged "XML.tree" id
7.158 -
7.159 -fun option a =
7.160 - let
7.161 - fun enc (SOME x) = (0, encode a x)
7.162 - | enc NONE = (1, encode unit ())
7.163 - fun dec 0 = SOME (decode a #> map_result SOME)
7.164 - | dec 1 = SOME (decode unit #> map_result (K NONE))
7.165 - | dec _ = NONE
7.166 - in variant enc dec "option" end
7.167 -
7.168 -val content_of =
7.169 - XML.content_of o YXML.parse_body
7.170 -
7.171 -(* slightly fishy codec, doesn't preserve exception type *)
7.172 -exception GENERIC of string
7.173 -val exn = tagged "exn" (text (fn exn => (content_of (@{make_string} exn))) (SOME o GENERIC))
7.174 -
7.175 -fun exn_result a =
7.176 - let
7.177 - fun enc (Exn.Res t) = (0, encode a t)
7.178 - | enc (Exn.Exn e) = (1, encode exn e)
7.179 - fun dec 0 = SOME (decode a #> map_result Exn.Res)
7.180 - | dec 1 = SOME (decode exn #> map_result Exn.Exn)
7.181 - | dec _ = NONE
7.182 - in variant enc dec "Exn.result" end
7.183 -
7.184 -fun triple a b c =
7.185 - tuple a (tuple b c)
7.186 - |> transform (fn (a, (b, c)) => (a, b, c)) (fn (a, b, c) => (a, (b, c)))
7.187 -
7.188 -fun either a b =
7.189 - let
7.190 - fun enc (Left l) = (0, encode a l)
7.191 - | enc (Right r) = (1, encode b r)
7.192 - fun dec 0 = SOME (decode a #> map_result Left)
7.193 - | dec 1 = SOME (decode b #> map_result Right)
7.194 - | dec _ = NONE
7.195 - in variant enc dec "either" end
7.196 -
7.197 -val sort: sort codec = list string
7.198 -val indexname: indexname codec = tuple string int
7.199 -
7.200 -fun typ () =
7.201 - let
7.202 - fun typ_type () = tuple string (list (typ ()))
7.203 - val typ_tfree = tuple string sort
7.204 - val typ_tvar = tuple indexname sort
7.205 -
7.206 - fun enc (Type arg) = (0, encode (typ_type ()) arg)
7.207 - | enc (TFree arg) = (1, encode typ_tfree arg)
7.208 - | enc (TVar arg) = (2, encode typ_tvar arg)
7.209 - fun dec 0 = SOME (decode (typ_type ()) #> map_result Type)
7.210 - | dec 1 = SOME (decode typ_tfree #> map_result TFree)
7.211 - | dec 2 = SOME (decode typ_tvar #> map_result TVar)
7.212 - | dec _ = NONE
7.213 - in variant enc dec "Pure.typ" end
7.214 -
7.215 -val typ = typ ()
7.216 -
7.217 -fun term () =
7.218 - let
7.219 - val term_const = tuple string typ
7.220 - val term_free = tuple string typ
7.221 - val term_var = tuple indexname typ
7.222 - val term_bound = int
7.223 - fun term_abs () = triple string typ (term ())
7.224 - fun term_app () = tuple (term ()) (term ())
7.225 -
7.226 - fun enc (Const arg) = (0, encode term_const arg)
7.227 - | enc (Free arg) = (1, encode term_free arg)
7.228 - | enc (Var arg) = (2, encode term_var arg)
7.229 - | enc (Bound arg) = (3, encode term_bound arg)
7.230 - | enc (Abs arg) = (4, encode (term_abs ()) arg)
7.231 - | enc (op $ arg) = (5, encode (term_app ()) arg)
7.232 - fun dec 0 = SOME (decode term_const #> map_result Const)
7.233 - | dec 1 = SOME (decode term_free #> map_result Free)
7.234 - | dec 2 = SOME (decode term_var #> map_result Var)
7.235 - | dec 3 = SOME (decode term_bound #> map_result Bound)
7.236 - | dec 4 = SOME (decode (term_abs ()) #> map_result Abs)
7.237 - | dec 5 = SOME (decode (term_app ()) #> map_result op $)
7.238 - | dec _ = NONE
7.239 - in variant enc dec "Pure.term" end
7.240 -
7.241 -val term = term ()
7.242 -
7.243 -end
7.244 -
7.245 -type 'a codec = 'a Codec.codec
8.1 --- a/libisabelle-protocol/common/protocol.ML Sat Feb 06 17:20:08 2016 +0100
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,119 +0,0 @@
8.4 -signature PROTOCOL = sig
8.5 - type name = string
8.6 - type ('i, 'o) operation =
8.7 - {from_lib : 'i codec,
8.8 - to_lib : 'o codec,
8.9 - action : 'i -> 'o}
8.10 -
8.11 - type flags = {sequential: bool, bracket: bool, auto: bool (* ignored *)}
8.12 -
8.13 - val default_flags : flags
8.14 - val join_flags : flags -> flags -> flags
8.15 - val print_flags : flags -> string
8.16 -
8.17 - val add_operation : name -> ('i, 'o) operation -> flags -> unit
8.18 - val get_operation : name -> int -> XML.tree -> XML.tree
8.19 -end
8.20 -
8.21 -structure Protocol: PROTOCOL = struct
8.22 -
8.23 -type name = string
8.24 -type ('i, 'o) operation =
8.25 - {from_lib : 'i codec,
8.26 - to_lib : 'o codec,
8.27 - action : 'i -> 'o}
8.28 -
8.29 -type flags = {sequential: bool, bracket: bool, auto: bool}
8.30 -
8.31 -val default_flags = {sequential = false, bracket = false, auto = false}
8.32 -
8.33 -fun join_flags
8.34 - {sequential = seq1, bracket = br1, auto = a1}
8.35 - {sequential = seq2, bracket = br2, auto = a2} =
8.36 - {sequential = seq1 orelse seq2, bracket = br1 orelse br2, auto = a1 orelse a2}
8.37 -
8.38 -fun print_flags {sequential, bracket, auto} =
8.39 - "({sequential=" ^ Markup.print_bool sequential ^ "," ^
8.40 - "bracket=" ^ Markup.print_bool bracket ^ "," ^
8.41 - "auto=" ^ Markup.print_bool auto ^ "})"
8.42 -
8.43 -type raw_operation = int -> XML.tree -> XML.tree
8.44 -
8.45 -exception GENERIC of string
8.46 -
8.47 -val operations =
8.48 - Synchronized.var "libisabelle.operations" (Symtab.empty: raw_operation Symtab.table)
8.49 -
8.50 -val requests =
8.51 - Synchronized.var "libisabelle.requests" (Inttab.empty: (unit -> unit) Inttab.table)
8.52 -
8.53 -fun sequentialize name f =
8.54 - let
8.55 - val var = Synchronized.var ("libisabelle." ^ name) ()
8.56 - in
8.57 - fn x => Synchronized.change_result var (fn _ => (f x, ()))
8.58 - end
8.59 -
8.60 -fun bracketize f id x =
8.61 - let
8.62 - val start = [(Markup.functionN, "libisabelle_start"), ("id", Markup.print_int id)]
8.63 - val stop = [(Markup.functionN, "libisabelle_stop"), ("id", Markup.print_int id)]
8.64 - val _ = Output.protocol_message start []
8.65 - val res = f id x
8.66 - val _ = Output.protocol_message stop []
8.67 - in res end
8.68 -
8.69 -fun add_operation name {from_lib, to_lib, action} {sequential, bracket, ...} =
8.70 - let
8.71 - fun raw _ tree =
8.72 - case Codec.decode from_lib tree of
8.73 - Codec.Success i => Codec.encode to_lib (action i)
8.74 - | Codec.Failure (msg, _) => raise Fail ("decoding input failed for operation " ^ name ^ ": " ^ msg)
8.75 - val raw' = raw
8.76 - |> (if bracket then bracketize else I)
8.77 - |> (if sequential then sequentialize name else I)
8.78 - in
8.79 - Synchronized.change operations (Symtab.update (name, raw'))
8.80 - end
8.81 -
8.82 -fun get_operation name =
8.83 - case Symtab.lookup (Synchronized.value operations) name of
8.84 - SOME operation => operation
8.85 - | NONE => fn _ => raise Fail "libisabelle: unknown command"
8.86 -
8.87 -val _ = Isabelle_Process.protocol_command "libisabelle"
8.88 - (fn id :: name :: [arg] =>
8.89 - let
8.90 - val id = Markup.parse_int id
8.91 - val response = [(Markup.functionN, "libisabelle_response"), ("id", Markup.print_int id)]
8.92 - val args = YXML.parse arg
8.93 - fun exec f =
8.94 - let
8.95 - val future = Future.fork (fn () =>
8.96 - let
8.97 - val res = Exn.interruptible_capture (f id) args
8.98 - val yxml = YXML.string_of (Codec.encode (Codec.exn_result Codec.id) res)
8.99 - in
8.100 - Output.protocol_message response [yxml]
8.101 - end)
8.102 - in
8.103 - Synchronized.change requests (Inttab.update_new (id, fn () => Future.cancel future))
8.104 - end
8.105 - in
8.106 - exec (get_operation name)
8.107 - end)
8.108 -
8.109 -val _ = Isabelle_Process.protocol_command "libisabelle_cancel"
8.110 - (fn ids =>
8.111 - let
8.112 - fun remove id tab = (Inttab.lookup tab id, Inttab.delete_safe id tab)
8.113 - val _ =
8.114 - map Markup.parse_int ids
8.115 - |> fold_map remove
8.116 - |> Synchronized.change_result requests
8.117 - |> map (fn NONE => () | SOME f => f ())
8.118 - in
8.119 - ()
8.120 - end)
8.121 -
8.122 -end
8.123 \ No newline at end of file
9.1 --- a/libisabelle-protocol/isabelle/2015/Codec_Class.thy Sat Feb 06 17:20:08 2016 +0100
9.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
9.3 @@ -1,21 +0,0 @@
9.4 -theory Codec_Class
9.5 -imports "../../common/Common" "lib/classy/Classy"
9.6 -begin
9.7 -
9.8 -ML.class codec = \<open>'a codec\<close>
9.9 -
9.10 -ML.instance \<open>Codec.unit\<close> :: codec
9.11 -ML.instance \<open>Codec.bool\<close> :: codec
9.12 -ML.instance \<open>Codec.string\<close> :: codec
9.13 -ML.instance \<open>Codec.int\<close> :: codec
9.14 -ML.instance \<open>Codec.list\<close> :: codec
9.15 -ML.instance \<open>Codec.tuple\<close> :: codec
9.16 -ML.instance \<open>Codec.option\<close> :: codec
9.17 -ML.instance \<open>Codec.either\<close> :: codec
9.18 -ML.instance \<open>Codec.triple\<close> :: codec
9.19 -ML.instance \<open>Codec.sort\<close> :: codec
9.20 -ML.instance \<open>Codec.typ\<close> :: codec
9.21 -ML.instance \<open>Codec.term\<close> :: codec
9.22 -ML.instance \<open>Codec.tree\<close> :: codec
9.23 -
9.24 -end
9.25 \ No newline at end of file
10.1 --- a/libisabelle-protocol/isabelle/2015/Protocol.thy Sat Feb 06 17:20:08 2016 +0100
10.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
10.3 @@ -1,759 +0,0 @@
10.4 -theory Protocol
10.5 -imports Codec_Class
10.6 - "~~/src/Tools/isac/Knowledge/Build_Thydata"
10.7 -keywords "operation_setup" :: thy_decl % "ML"
10.8 -begin
10.9 -
10.10 -ML\<open>
10.11 -val _ =
10.12 - let
10.13 - open Protocol
10.14 - fun operation_setup_cmd name source (flags as {auto, ...}) ctxt =
10.15 - let
10.16 - fun eval enclose =
10.17 - ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of source)
10.18 - (ML_Lex.read ("Protocol.add_operation " ^ ML_Syntax.print_string name ^ "(") @
10.19 - enclose (ML_Lex.read_source false source) @
10.20 - ML_Lex.read ")" @
10.21 - ML_Lex.read (print_flags flags))
10.22 - in
10.23 - if auto then
10.24 - let
10.25 - val ML_Types.Fun (arg, res) = ML_Types.ml_type_of ctxt (Input.source_content source)
10.26 - val arg_codec = Classy.resolve @{ML.class codec} arg (Context.Proof ctxt)
10.27 - val res_codec = Classy.resolve @{ML.class codec} res (Context.Proof ctxt)
10.28 - fun enclose toks =
10.29 - ML_Lex.read "{from_lib=" @ ML_Lex.read arg_codec @ ML_Lex.read "," @
10.30 - ML_Lex.read "to_lib=" @ ML_Lex.read res_codec @ ML_Lex.read "," @
10.31 - ML_Lex.read "action=" @ toks @ ML_Lex.read "}"
10.32 - in
10.33 - eval enclose
10.34 - end
10.35 - else
10.36 - eval I
10.37 - end
10.38 - val parse_flag =
10.39 - (Parse.reserved "sequential" || Parse.reserved "bracket" || Parse.reserved "auto") >>
10.40 - (fn flag => join_flags
10.41 - {sequential = flag = "sequential",
10.42 - bracket = flag = "bracket",
10.43 - auto = flag = "auto"})
10.44 - val parse_flags =
10.45 - Parse.list parse_flag >> (fn fs => fold (curry op o) fs I)
10.46 - val parse_cmd =
10.47 - Scan.optional (Args.parens parse_flags) I --
10.48 - Parse.name --
10.49 - Parse.!!! (@{keyword "="} |-- Parse.ML_source)
10.50 - in
10.51 - Outer_Syntax.command @{command_keyword "operation_setup"} "define protocol operation in ML"
10.52 - (parse_cmd >> (fn ((flags, name), txt) =>
10.53 - Toplevel.keep (Toplevel.context_of #> operation_setup_cmd name txt (flags default_flags))))
10.54 - end
10.55 -\<close>
10.56 -
10.57 -section \<open>Operation setup for Math_Engine : MATH_ENGINE\<close>
10.58 -
10.59 -(* val appendFormula : calcID -> cterm' -> XML.tree *)
10.60 -operation_setup (sequential, bracket, auto) append_form =
10.61 - \<open>fn intree =>
10.62 - (let
10.63 - val (calcid, cterm') = case intree of
10.64 - XML.Elem (("APPENDFORMULA", []), [
10.65 - XML.Elem (("CALCID", []), [XML.Text ci]),
10.66 - form]) => (ci |> int_of_str', form |> xml_to_formula |> term2str)
10.67 - | x => raise ERROR ("append_form: WRONG intree = " ^ xmlstr 0 x)
10.68 - val result = Math_Engine.appendFormula calcid cterm'
10.69 - in result end)
10.70 - handle ERROR msg => appendformulaERROR2xml 4711 msg\<close>
10.71 -
10.72 -(* val autoCalculate : calcID -> auto -> XML.tree *)
10.73 -operation_setup autocalculate = \<open>
10.74 - {from_lib = Codec.tree,
10.75 - to_lib = Codec.tree,
10.76 - action = (fn intree =>
10.77 - (let
10.78 - val (ci, a) = case intree of
10.79 - XML.Elem (("AUTOCALC", []), [
10.80 - XML.Elem (("CALCID", []), [XML.Text ci]), a]) => (ci, a)
10.81 - | tree => raise ERROR ("autocalculate: WRONG intree = " ^ xmlstr 0 tree)
10.82 - val SOME calcid = int_of_str ci
10.83 - val auto = xml_to_auto a
10.84 - val result = Math_Engine.autoCalculate calcid auto
10.85 - in result end)
10.86 - handle ERROR msg => autocalculateERROR2xml 4711 msg)}\<close>
10.87 -
10.88 -(* val applyTactic : calcID -> pos' -> tac -> XML.tree *)
10.89 -operation_setup apply_tac = \<open>
10.90 - {from_lib = Codec.tree,
10.91 - to_lib = Codec.tree,
10.92 - action = (fn intree =>
10.93 - (let
10.94 - val (ci, pos, tac) = case intree of
10.95 - XML.Elem (("AUTOCALC", []), [
10.96 - XML.Elem (("CALCID", []), [XML.Text ci]),
10.97 - pos, tac]) => (str2int ci, xml_to_pos pos, xml_to_tac tac)
10.98 - | tree => raise ERROR ("apply_tac: WRONG intree = " ^ xmlstr 0 tree)
10.99 - val result = Math_Engine.applyTactic ci pos tac
10.100 - in result end)
10.101 - handle ERROR msg => autocalculateERROR2xml 4711 msg)}\<close>
10.102 -
10.103 -(* val CalcTree : fmz list -> XML.tree *)
10.104 -operation_setup calctree = \<open>
10.105 - {from_lib = Codec.tree,
10.106 - to_lib = Codec.tree,
10.107 - action = (fn intree =>
10.108 - (let
10.109 - val fmz = case intree of
10.110 - tree as XML.Elem (("FORMALIZATION", []), vars) => xml_to_fmz tree
10.111 - | tree => raise ERROR ("calctree: WRONG intree = " ^ xmlstr 0 tree)
10.112 - val result = Math_Engine.CalcTree fmz
10.113 - in result end)
10.114 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.115 -
10.116 -(* val checkContext : calcID -> pos' -> guh -> XML.tree *)
10.117 -operation_setup check_ctxt = \<open>
10.118 - {from_lib = Codec.tree,
10.119 - to_lib = Codec.tree,
10.120 - action = (fn intree =>
10.121 - (let
10.122 - val (ci, pos, guh) = case intree of
10.123 - XML.Elem (("CONTEXTTHY", []), [
10.124 - XML.Elem (("CALCID", []), [XML.Text ci]),
10.125 - pos as XML.Elem (("POSITION", []), _),
10.126 - XML.Elem (("GUH", []), [XML.Text guh])])
10.127 - => (str2int ci, xml_to_pos pos, guh)
10.128 - | tree => raise ERROR ("check_ctxt: WRONG intree = " ^ xmlstr 0 tree)
10.129 - val result = Math_Engine.checkContext ci pos guh
10.130 - in result end)
10.131 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.132 -
10.133 -(* val DEconstrCalcTree : calcID -> XML.tree *)
10.134 -operation_setup deconstrcalctree = \<open>
10.135 - {from_lib = Codec.int,
10.136 - to_lib = Codec.tree,
10.137 - action = (fn calcid =>
10.138 - let
10.139 - val result = Math_Engine.DEconstrCalcTree calcid
10.140 - in result end)}\<close>
10.141 -
10.142 -(* val fetchApplicableTactics : calcID -> int -> pos' -> XML.tree *)
10.143 -operation_setup fetch_applicable_tacs = \<open>
10.144 - {from_lib = Codec.tree,
10.145 - to_lib = Codec.tree,
10.146 - action = (fn intree =>
10.147 - (let
10.148 - val (ci, i, pos) = case intree of
10.149 - XML.Elem (("APPLICABLETACTICS", []), [
10.150 - XML.Elem (("CALCID", []), [XML.Text ci]),
10.151 - XML.Elem (("INT", []), [XML.Text i]),
10.152 - pos as XML.Elem (("POSITION", []), _)])
10.153 - => (str2int ci, str2int i, xml_to_pos pos)
10.154 - | tree => raise ERROR ("fetch_applicable_tacs: WRONG intree = " ^ xmlstr 0 tree)
10.155 - val result = Math_Engine.fetchApplicableTactics ci i pos
10.156 - in result end)
10.157 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.158 -
10.159 -(* val fetchProposedTactic : calcID -> XML.tree *)
10.160 -operation_setup fetch_proposed_tac = \<open>
10.161 - {from_lib = Codec.tree,
10.162 - to_lib = Codec.tree,
10.163 - action = (fn intree =>
10.164 - (let
10.165 - val (ci) = case intree of
10.166 - XML.Elem (("NEXTTAC", []), [
10.167 - XML.Elem (("CALCID", []), [XML.Text ci])]) => (str2int ci)
10.168 - | tree => raise ERROR ("fetch_proposed_tac: WRONG intree = " ^ xmlstr 0 tree)
10.169 - val result = Math_Engine.fetchProposedTactic ci
10.170 - in result end)
10.171 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.172 -
10.173 -(* val findFillpatterns : calcID -> errpatID -> XML.tree *)
10.174 -operation_setup find_fill_patts = \<open>
10.175 - {from_lib = Codec.tree,
10.176 - to_lib = Codec.tree,
10.177 - action = (fn intree =>
10.178 - (let
10.179 - val (ci, err_pat_id) = case intree of
10.180 - XML.Elem (("FINDFILLPATTERNS", []), [
10.181 - XML.Elem (("CALCID", []), [XML.Text ci]),
10.182 - XML.Elem (("STRING", []), [XML.Text err_pat_id])])
10.183 - => (str2int ci, err_pat_id)
10.184 - | tree => raise ERROR ("find_fill_patts: WRONG intree = " ^ xmlstr 0 tree)
10.185 - val result = Math_Engine.findFillpatterns ci err_pat_id
10.186 - in result end)
10.187 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.188 -
10.189 -(* val getAccumulatedAsms : calcID -> pos' -> XML.tree *)
10.190 -operation_setup get_accumulated_asms = \<open>
10.191 - {from_lib = Codec.tree,
10.192 - to_lib = Codec.tree,
10.193 - action = (fn intree =>
10.194 - (let
10.195 - val (ci, pos) = case intree of
10.196 - XML.Elem (("GETASSUMPTIONS", []), [
10.197 - XML.Elem (("CALCID", []), [XML.Text ci]),
10.198 - pos as XML.Elem (("POSITION", []), _)])
10.199 - => (str2int ci, xml_to_pos pos)
10.200 - | tree => raise ERROR ("autocalculate: WRONG intree = " ^ xmlstr 0 tree)
10.201 - val result = Math_Engine.getAccumulatedAsms ci pos
10.202 - in result end)
10.203 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.204 -
10.205 -(* val getActiveFormula : calcID -> XML.tree *)
10.206 -operation_setup get_active_form = \<open>
10.207 - {from_lib = Codec.tree,
10.208 - to_lib = Codec.tree,
10.209 - action = (fn intree =>
10.210 - (let
10.211 - val (ci) = case intree of
10.212 - XML.Elem (("CALCITERATOR", []), [
10.213 - XML.Elem (("CALCID", []), [XML.Text ci])])
10.214 - => (str2int ci)
10.215 - | tree => raise ERROR ("get_active_form: WRONG intree = " ^ xmlstr 0 tree)
10.216 - val result = Math_Engine.getActiveFormula ci
10.217 - in result end)
10.218 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.219 -
10.220 -(* val getAssumptions : calcID -> pos' -> XML.tree *)
10.221 -operation_setup get_asms = \<open>
10.222 - {from_lib = Codec.tree,
10.223 - to_lib = Codec.tree,
10.224 - action = (fn intree =>
10.225 - (let
10.226 - val (ci, pos) = case intree of
10.227 - XML.Elem (("APPLICABLETACTICS", []), [
10.228 - XML.Elem (("CALCID", []), [XML.Text ci]),
10.229 - pos as XML.Elem (("POSITION", []), _)])
10.230 - => (str2int ci, xml_to_pos pos)
10.231 - | tree => raise ERROR ("get_asms: WRONG intree = " ^ xmlstr 0 tree)
10.232 - val result = Math_Engine.getAssumptions ci pos
10.233 - in result end)
10.234 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.235 -
10.236 -(* val getFormulaeFromTo : calcID -> pos' -> pos' -> int -> bool -> XML.tree *)
10.237 -operation_setup getformulaefromto = \<open>
10.238 - {from_lib = Codec.tree,
10.239 - to_lib = Codec.tree,
10.240 - action = (fn intree =>
10.241 - (let
10.242 - val (calcid, from, to, level, rules) = case intree of
10.243 - XML.Elem (("GETFORMULAEFROMTO", []), [
10.244 - XML.Elem (("CALCID", []), [XML.Text calcid]),
10.245 - from as XML.Elem (("POSITION", []), [
10.246 - XML.Elem (("INTLIST", []), _),
10.247 - XML.Elem (("POS", []), [XML.Text _])]),
10.248 - to as XML.Elem (("POSITION", []), [
10.249 - XML.Elem (("INTLIST", []), _),
10.250 - XML.Elem (("POS", []), [XML.Text _])]),
10.251 - XML.Elem (("INT", []), [XML.Text level]),
10.252 - XML.Elem (("BOOL", []), [XML.Text rules])])
10.253 - => (str2int calcid, xml_to_pos from, xml_to_pos to, str2int level, string_to_bool rules)
10.254 - | tree => raise ERROR ("getformulaefromto: WRONG intree = " ^ xmlstr 0 tree)
10.255 - val result = Math_Engine.getFormulaeFromTo calcid from to level rules
10.256 - in result end)
10.257 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.258 -
10.259 -(* val getTactic : calcID -> pos' -> XML.tree *)
10.260 -operation_setup get_tac = \<open>
10.261 - {from_lib = Codec.tree,
10.262 - to_lib = Codec.tree,
10.263 - action = (fn intree =>
10.264 - (let
10.265 - val (ci, pos) = case intree of
10.266 - XML.Elem (("GETTACTIC", []), [
10.267 - XML.Elem (("CALCID", []), [XML.Text ci]),
10.268 - pos as XML.Elem (("POSITION", []), _)])
10.269 - => (str2int ci, xml_to_pos pos)
10.270 - | tree => raise ERROR ("get_tac: WRONG intree = " ^ xmlstr 0 tree)
10.271 - val result = Math_Engine.getTactic ci pos
10.272 - in result end)
10.273 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.274 -
10.275 -(* val initContext : calcID -> ketype -> pos' -> XML.tree *)
10.276 -operation_setup init_ctxt = \<open>
10.277 - {from_lib = Codec.tree,
10.278 - to_lib = Codec.tree,
10.279 - action = (fn intree =>
10.280 - ((let
10.281 - val (ci, ketype, pos) = case intree of
10.282 - XML.Elem (("INITCONTEXT", []), [
10.283 - XML.Elem (("CALCID", []), [XML.Text ci]),
10.284 - ketype as XML.Elem (("KETYPE", []), _),
10.285 - pos as XML.Elem (("POSITION", []), _)])
10.286 - => (str2int ci, xml_to_ketype ketype, xml_to_pos pos)
10.287 - | tree => raise ERROR ("init_ctxt: WRONG intree = " ^ xmlstr 0 tree)
10.288 - val result = Math_Engine.initContext ci ketype pos
10.289 - in result end)
10.290 - handle ERROR msg => sysERROR2xml 4711 msg)
10.291 - handle _ => sysERROR2xml 4711 "Protocol.operation_setup init_ctxt UNKNOWN exn")}\<close>
10.292 -
10.293 -(* val inputFillFormula: calcID -> string -> XML.tree *)
10.294 -operation_setup input_fill_form = \<open>
10.295 - {from_lib = Codec.tree,
10.296 - to_lib = Codec.tree,
10.297 - action = (fn intree =>
10.298 - (let
10.299 - val (ci, str) = case intree of
10.300 - XML.Elem (("AUTOCALC", []), [
10.301 - XML.Elem (("CALCID", []), [XML.Text ci]),
10.302 - XML.Elem (("STRING", []), [XML.Text str])])
10.303 - => (str2int ci, str)
10.304 - | tree => raise ERROR ("input_fill_form: WRONG intree = " ^ xmlstr 0 tree)
10.305 - val result = Math_Engine.inputFillFormula ci str
10.306 - in result end)
10.307 - handle ERROR msg => message2xml 4711 msg)}\<close>
10.308 -
10.309 -(* val interSteps : calcID -> pos' -> XML.tree *)
10.310 -operation_setup inter_steps = \<open>
10.311 - {from_lib = Codec.tree,
10.312 - to_lib = Codec.tree,
10.313 - action = (fn intree =>
10.314 - (let
10.315 - val (ci, pos) = case intree of
10.316 - XML.Elem (("INTERSTEPS", []), [
10.317 - XML.Elem (("CALCID", []), [XML.Text ci]),
10.318 - pos as XML.Elem (("POSITION", []), _)])
10.319 - => (str2int ci, xml_to_pos pos)
10.320 - | tree => raise ERROR ("inter_steps: WRONG intree = " ^ xmlstr 0 tree)
10.321 - val result = Math_Engine.interSteps ci pos
10.322 - in result end)
10.323 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.324 -
10.325 -(* val Iterator : calcID -> XML.tree *)
10.326 -operation_setup iterator = \<open>
10.327 - {from_lib = Codec.int,
10.328 - to_lib = Codec.tree,
10.329 - action = (fn calcid =>
10.330 - let
10.331 - val result = Math_Engine.Iterator calcid
10.332 - in result end)}\<close>
10.333 -
10.334 -(* val IteratorTEST : calcID -> iterID *)
10.335 -
10.336 -(* val modelProblem : calcID -> XML.tree *)
10.337 -operation_setup model_pbl = \<open>
10.338 - {from_lib = Codec.tree,
10.339 - to_lib = Codec.tree,
10.340 - action = (fn intree =>
10.341 - (let
10.342 - val (ci) = case intree of
10.343 - XML.Elem (("MODIFYCALCHEAD", []), [
10.344 - XML.Elem (("CALCID", []), [XML.Text ci])])
10.345 - => (str2int ci)
10.346 - | tree => raise ERROR ("model_pbl: WRONG intree = " ^ xmlstr 0 tree)
10.347 - val result = Math_Engine.modelProblem ci
10.348 - in result end)
10.349 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.350 -
10.351 -(* val modifyCalcHead : calcID -> icalhd -> XML.tree *)
10.352 -operation_setup modify_calchead = \<open>
10.353 - {from_lib = Codec.tree,
10.354 - to_lib = Codec.tree,
10.355 - action = (fn intree =>
10.356 - (let
10.357 - val (ci, icalhd) = case intree of
10.358 - XML.Elem (("MODIFYCALCHEAD", []), [
10.359 - XML.Elem (("CALCID", []), [XML.Text ci]),
10.360 - icalhd])
10.361 - => (str2int ci, xml_to_icalhd icalhd)
10.362 - | tree => raise ERROR ("modify_calchead: WRONG intree = " ^ xmlstr 0 tree)
10.363 - val result = Math_Engine.modifyCalcHead ci icalhd
10.364 - in result end)
10.365 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.366 -
10.367 -(* val moveActiveCalcHead : calcID -> XML.tree *)
10.368 -operation_setup move_active_calchead = \<open>
10.369 - {from_lib = Codec.tree,
10.370 - to_lib = Codec.tree,
10.371 - action = (fn intree =>
10.372 - (let
10.373 - val (ci) = case intree of
10.374 - XML.Elem (("CALCITERATOR", []), [
10.375 - XML.Elem (("CALCID", []), [XML.Text ci])])
10.376 - => (str2int ci)
10.377 - | tree => raise ERROR ("move_active_calchead: WRONG intree = " ^ xmlstr 0 tree)
10.378 - val result = Math_Engine.moveActiveCalcHead ci
10.379 - in result end)
10.380 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.381 -
10.382 -(* val moveActiveDown : calcID -> XML.tree *)
10.383 -operation_setup move_active_down = \<open>
10.384 - {from_lib = Codec.tree,
10.385 - to_lib = Codec.tree,
10.386 - action = (fn intree =>
10.387 - (let
10.388 - val (ci) = case intree of
10.389 - XML.Elem (("CALCITERATOR", []), [
10.390 - XML.Elem (("CALCID", []), [XML.Text ci])])
10.391 - => (str2int ci)
10.392 - | tree => raise ERROR ("move_active_down: WRONG intree = " ^ xmlstr 0 tree)
10.393 - val result = Math_Engine.moveActiveDown ci
10.394 - in result end)
10.395 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.396 -
10.397 -(* val moveActiveFormula : calcID -> pos' -> XML.tree *)
10.398 -operation_setup move_active_form = \<open>
10.399 - {from_lib = Codec.tree,
10.400 - to_lib = Codec.tree,
10.401 - action = (fn intree =>
10.402 - (let
10.403 - val (ci, pos) = case intree of
10.404 - XML.Elem (("CALCITERATOR", []), [
10.405 - XML.Elem (("CALCID", []), [XML.Text ci]),
10.406 - pos as XML.Elem (("POSITION", []), _)])
10.407 - => (str2int ci, xml_to_pos pos)
10.408 - | tree => raise ERROR ("move_active_form: WRONG intree = " ^ xmlstr 0 tree)
10.409 - val result = Math_Engine.moveActiveFormula ci pos
10.410 - in result end)
10.411 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.412 -
10.413 -(* val moveActiveLevelDown : calcID -> XML.tree *)
10.414 -operation_setup move_active_levdown = \<open>
10.415 - {from_lib = Codec.tree,
10.416 - to_lib = Codec.tree,
10.417 - action = (fn intree =>
10.418 - (let
10.419 - val (ci) = case intree of
10.420 - XML.Elem (("CALCITERATOR", []), [
10.421 - XML.Elem (("CALCID", []), [XML.Text ci])])
10.422 - => (str2int ci)
10.423 - | tree => raise ERROR ("move_active_levdown: WRONG intree = " ^ xmlstr 0 tree)
10.424 - val result = Math_Engine.moveActiveLevelDown ci
10.425 - in result end)
10.426 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.427 -
10.428 -(* val moveActiveLevelUp : calcID -> XML.tree *)
10.429 -operation_setup move_active_levup = \<open>
10.430 - {from_lib = Codec.tree,
10.431 - to_lib = Codec.tree,
10.432 - action = (fn intree =>
10.433 - (let
10.434 - val (ci) = case intree of
10.435 - XML.Elem (("CALCITERATOR", []), [
10.436 - XML.Elem (("CALCID", []), [XML.Text ci])])
10.437 - => (str2int ci)
10.438 - | tree => raise ERROR ("move_active_levup: WRONG intree = " ^ xmlstr 0 tree)
10.439 - val result = Math_Engine.moveActiveLevelUp ci
10.440 - in result end)
10.441 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.442 -
10.443 -(* val moveActiveRoot : calcID -> XML.tree *)
10.444 -operation_setup moveactiveroot = \<open>
10.445 - {from_lib = Codec.int,
10.446 - to_lib = Codec.tree,
10.447 - action = (fn calcid =>
10.448 - let
10.449 - val result = Math_Engine.moveActiveRoot calcid
10.450 - in result end)}\<close>
10.451 -
10.452 -(* val moveActiveRootTEST : calcID -> XML.tree *)
10.453 -
10.454 -(* val moveActiveUp : calcID -> XML.tree *)
10.455 -operation_setup move_active_up = \<open>
10.456 - {from_lib = Codec.tree,
10.457 - to_lib = Codec.tree,
10.458 - action = (fn intree =>
10.459 - (let
10.460 - val (ci) = case intree of
10.461 - XML.Elem (("CALCITERATOR", []), [
10.462 - XML.Elem (("CALCID", []), [XML.Text ci])])
10.463 - => (str2int ci)
10.464 - | tree => raise ERROR ("move_active_up: WRONG intree = " ^ xmlstr 0 tree)
10.465 - val result = Math_Engine.moveActiveUp ci
10.466 - in result end)
10.467 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.468 -
10.469 -(* val moveCalcHead : calcID -> pos' -> XML.tree *)
10.470 -operation_setup move_calchead = \<open>
10.471 - {from_lib = Codec.tree,
10.472 - to_lib = Codec.tree,
10.473 - action = (fn intree =>
10.474 - (let
10.475 - val (ci, pos) = case intree of
10.476 - XML.Elem (("CALCITERATOR", []), [
10.477 - XML.Elem (("CALCID", []), [XML.Text ci]),
10.478 - pos as XML.Elem (("POSITION", []), _)])
10.479 - => (str2int ci, xml_to_pos pos)
10.480 - | tree => raise ERROR ("move_active_calchead: WRONG intree = " ^ xmlstr 0 tree)
10.481 - val result = Math_Engine.moveCalcHead ci pos
10.482 - in result end)
10.483 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.484 -
10.485 -(* val moveDown : calcID -> pos' -> XML.tree *)
10.486 -operation_setup move_down = \<open>
10.487 - {from_lib = Codec.tree,
10.488 - to_lib = Codec.tree,
10.489 - action = (fn intree =>
10.490 - (let
10.491 - val (ci, pos) = case intree of
10.492 - XML.Elem (("CALCITERATOR", []), [
10.493 - XML.Elem (("CALCID", []), [XML.Text ci]),
10.494 - pos as XML.Elem (("POSITION", []), _)])
10.495 - => (str2int ci, xml_to_pos pos)
10.496 - | tree => raise ERROR ("move_down: WRONG intree = " ^ xmlstr 0 tree)
10.497 - val result = Math_Engine.moveDown ci pos
10.498 - in result end)
10.499 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.500 -
10.501 -(* val moveLevelDown : calcID -> pos' -> XML.tree *)
10.502 -operation_setup move_levdn = \<open>
10.503 - {from_lib = Codec.tree,
10.504 - to_lib = Codec.tree,
10.505 - action = (fn intree =>
10.506 - (let
10.507 - val (ci, pos) = case intree of
10.508 - XML.Elem (("CALCITERATOR", []), [
10.509 - XML.Elem (("CALCID", []), [XML.Text ci]),
10.510 - pos as XML.Elem (("POSITION", []), _)])
10.511 - => (str2int ci, xml_to_pos pos)
10.512 - | tree => raise ERROR ("move_levdn: WRONG intree = " ^ xmlstr 0 tree)
10.513 - val result = Math_Engine.moveLevelDown ci pos
10.514 - in result end)
10.515 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.516 -
10.517 -(* val moveLevelUp : calcID -> pos' -> XML.tree *)
10.518 -operation_setup move_levup = \<open>
10.519 - {from_lib = Codec.tree,
10.520 - to_lib = Codec.tree,
10.521 - action = (fn intree =>
10.522 - (let
10.523 - val (ci, pos) = case intree of
10.524 - XML.Elem (("CALCITERATOR", []), [
10.525 - XML.Elem (("CALCID", []), [XML.Text ci]),
10.526 - pos as XML.Elem (("POSITION", []), _)])
10.527 - => (str2int ci, xml_to_pos pos)
10.528 - | tree => raise ERROR ("move_levup: WRONG intree = " ^ xmlstr 0 tree)
10.529 - val result = Math_Engine.moveLevelUp ci pos
10.530 - in result end)
10.531 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.532 -
10.533 -(* val moveRoot : calcID -> XML.tree *)
10.534 -operation_setup move_root = \<open>
10.535 - {from_lib = Codec.tree,
10.536 - to_lib = Codec.tree,
10.537 - action = (fn intree =>
10.538 - (let
10.539 - val (ci) = case intree of
10.540 - XML.Elem (("CALCITERATOR", []), [
10.541 - XML.Elem (("CALCID", []), [XML.Text ci])])
10.542 - => (str2int ci)
10.543 - | tree => raise ERROR ("move_root: WRONG intree = " ^ xmlstr 0 tree)
10.544 - val result = Math_Engine.moveRoot ci
10.545 - in result end)
10.546 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.547 -
10.548 -(* val moveUp : calcID -> pos' -> XML.tree *)
10.549 -operation_setup move_up = \<open>
10.550 - {from_lib = Codec.tree,
10.551 - to_lib = Codec.tree,
10.552 - action = (fn intree =>
10.553 - (let
10.554 - val (ci, pos) = case intree of
10.555 - XML.Elem (("CALCITERATOR", []), [
10.556 - XML.Elem (("CALCID", []), [XML.Text ci]),
10.557 - pos as XML.Elem (("POSITION", []), _)])
10.558 - => (str2int ci, xml_to_pos pos)
10.559 - | tree => raise ERROR ("move_up: WRONG intree = " ^ xmlstr 0 tree)
10.560 - val result = Math_Engine.moveUp ci pos
10.561 - in result end)
10.562 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.563 -
10.564 -(* val refFormula : calcID -> pos' -> XML.tree *)
10.565 -operation_setup refformula = \<open>
10.566 - {from_lib = Codec.tree,
10.567 - to_lib = Codec.tree,
10.568 - action = (fn intree =>
10.569 - (let
10.570 - val (ci, p) = case intree of
10.571 - XML.Elem (("REFFORMULA", []), [
10.572 - XML.Elem (("CALCID", []), [XML.Text ci]), p])
10.573 - => (ci, p)
10.574 - | tree => raise ERROR ("refformula: WRONG intree = " ^ xmlstr 0 tree)
10.575 - val SOME calcid = int_of_str ci
10.576 - val pos = xml_to_pos p
10.577 - val result = Math_Engine.refFormula calcid pos
10.578 - in result end)
10.579 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.580 -
10.581 -(* val refineProblem : calcID -> pos' -> guh -> XML.tree *)
10.582 -operation_setup refine_pbl = \<open>
10.583 - {from_lib = Codec.tree,
10.584 - to_lib = Codec.tree,
10.585 - action = (fn intree =>
10.586 - (let
10.587 - val (ci, pos, guh) = case intree of
10.588 - XML.Elem (("CONTEXTPBL", []), [
10.589 - XML.Elem (("CALCID", []), [XML.Text ci]),
10.590 - pos as XML.Elem (("POSITION", []), _),
10.591 - XML.Elem (("GUH", []), [XML.Text guh])])
10.592 - => (str2int ci, xml_to_pos pos, guh)
10.593 - | tree => raise ERROR ("refine_pbl: WRONG intree = " ^ xmlstr 0 tree)
10.594 - val result = Math_Engine.refineProblem ci pos guh
10.595 - in result end)
10.596 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.597 -
10.598 -(* val replaceFormula : calcID -> cterm' -> XML.tree *)
10.599 -operation_setup replace_form = \<open>
10.600 - {from_lib = Codec.tree,
10.601 - to_lib = Codec.tree,
10.602 - action = (fn intree =>
10.603 - (let
10.604 - val (calcid, cterm') = case intree of
10.605 - XML.Elem (("REPLACEFORMULA", []), [
10.606 - XML.Elem (("CALCID", []), [XML.Text ci]), form])
10.607 - => (ci |> int_of_str', form |> xml_to_formula |> term2str)
10.608 - | tree => raise ERROR ("replace_form: WRONG intree = " ^ xmlstr 0 tree)
10.609 - val result = Math_Engine.replaceFormula calcid cterm'
10.610 - in result end)
10.611 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.612 -
10.613 -(* val requestFillformula : calcID -> errpatID * fillpatID -> XML.tree NOT IMPL. IN isac-java *)
10.614 -operation_setup request_fill_form = \<open>
10.615 - {from_lib = Codec.tree,
10.616 - to_lib = Codec.tree,
10.617 - action = (fn intree =>
10.618 - (let
10.619 - val (ci, errpat_id, fillpat_id) = case intree of
10.620 - XML.Elem (("AUTOCALC", []), [
10.621 - XML.Elem (("CALCID", []), [XML.Text ci]),
10.622 - XML.Elem (("ERRPATTID", []), [XML.Text errpat_id]),
10.623 - XML.Elem (("FILLPATTID", []), [XML.Text fillpat_id])])
10.624 - => (str2int ci, errpat_id, fillpat_id)
10.625 - | tree => raise ERROR ("request_fill_form: WRONG intree = " ^ xmlstr 0 tree)
10.626 - val result = Math_Engine.requestFillformula ci (errpat_id, fillpat_id)
10.627 - in result end)
10.628 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.629 -
10.630 -(* val resetCalcHead : calcID -> XML.tree *)
10.631 -operation_setup reset_calchead = \<open>
10.632 - {from_lib = Codec.tree,
10.633 - to_lib = Codec.tree,
10.634 - action = (fn intree =>
10.635 - (let
10.636 - val (ci) = case intree of
10.637 - XML.Elem (("MODIFYCALCHEAD", []), [
10.638 - XML.Elem (("CALCID", []), [XML.Text ci])])
10.639 - => (str2int ci)
10.640 - | tree => raise ERROR ("reset_calchead: WRONG intree = " ^ xmlstr 0 tree)
10.641 - val result = Math_Engine.resetCalcHead ci
10.642 - in result end)
10.643 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.644 -
10.645 -(* val setContext : calcID -> pos' -> guh -> XML.tree *)
10.646 -operation_setup set_ctxt = \<open>
10.647 - {from_lib = Codec.tree,
10.648 - to_lib = Codec.tree,
10.649 - action = (fn intree =>
10.650 - (let
10.651 - val (ci, pos, guh) = case intree of
10.652 - XML.Elem (("CONTEXT", []), [
10.653 - XML.Elem (("CALCID", []), [XML.Text ci]),
10.654 - pos as XML.Elem (("POSITION", []), _),
10.655 - XML.Elem (("GUH", []), [XML.Text guh])])
10.656 - => (str2int ci, xml_to_pos pos, guh)
10.657 - | tree => raise ERROR ("set_ctxt: WRONG intree = " ^ xmlstr 0 tree)
10.658 - val result = Math_Engine.setContext ci pos guh
10.659 - in result end)
10.660 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.661 -
10.662 -(*//===vvv TODO ================================================================\\\\\\\\\\\\\\\\*)
10.663 -
10.664 -(* val setMethod : calcID -> metID -> XML.tree *)
10.665 -operation_setup set_met = \<open>
10.666 - {from_lib = Codec.tree,
10.667 - to_lib = Codec.tree,
10.668 - action = (fn intree =>
10.669 - (let
10.670 - val (ci, met_id) = case intree of
10.671 - XML.Elem (("MODIFYCALCHEAD", []), [
10.672 - XML.Elem (("CALCID", []), [XML.Text ci]),
10.673 - XML.Elem (("METHODID", []), [met_id])])
10.674 - => (str2int ci, xml_to_strs met_id)
10.675 - | tree => raise ERROR ("set_met: WRONG intree = " ^ xmlstr 0 tree)
10.676 - val result = Math_Engine.setMethod ci met_id
10.677 - in result end)
10.678 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.679 -
10.680 -(* val setNextTactic : calcID -> tac -> XML.tree *)
10.681 -operation_setup set_next_tac = \<open>
10.682 - {from_lib = Codec.tree,
10.683 - to_lib = Codec.tree,
10.684 - action = (fn intree =>
10.685 - (let
10.686 - val (ci, tac) = case intree of
10.687 - XML.Elem (("SETNEXTTACTIC", []), [
10.688 - XML.Elem (("CALCID", []), [XML.Text ci]),
10.689 - tac])
10.690 - => (str2int ci, xml_to_tac tac)
10.691 - | tree => raise ERROR ("set_next_tac: WRONG intree = " ^ xmlstr 0 tree)
10.692 - val result = Math_Engine.setNextTactic ci tac
10.693 - in result end)
10.694 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.695 -
10.696 -(*\\===^^^ TODO ================================================================///////////////*)
10.697 -
10.698 -(* val setProblem : calcID -> pblID -> XML.tree *)
10.699 -operation_setup set_pbl = \<open>
10.700 - {from_lib = Codec.tree,
10.701 - to_lib = Codec.tree,
10.702 - action = (fn intree =>
10.703 - (let
10.704 - val (ci, pbl_id) = case intree of
10.705 - XML.Elem (("MODIFYCALCHEAD", []), [
10.706 - XML.Elem (("CALCID", []), [XML.Text ci]),
10.707 - XML.Elem (("PROBLEMID", []), [pbl_id])])
10.708 - => (str2int ci, xml_to_strs pbl_id)
10.709 - | tree => raise ERROR ("set_pbl: WRONG intree = " ^ xmlstr 0 tree)
10.710 - val result = Math_Engine.setProblem ci pbl_id
10.711 - in result end)
10.712 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.713 -
10.714 -(* val setTheory : calcID -> thyID -> XML.tree *)
10.715 -operation_setup set_thy = \<open>
10.716 - {from_lib = Codec.tree,
10.717 - to_lib = Codec.tree,
10.718 - action = (fn intree =>
10.719 - (let
10.720 - val (ci, thy_id) = case intree of
10.721 - XML.Elem (("MODIFYCALCHEAD", []), [
10.722 - XML.Elem (("CALCID", []), [XML.Text ci]),
10.723 - XML.Elem (("THEORYID", []), [XML.Text thy_id])])
10.724 - => (str2int ci, thy_id)
10.725 - | tree => raise ERROR ("set_thy: WRONG intree = " ^ xmlstr 0 tree)
10.726 - val result = Math_Engine.setTheory ci thy_id
10.727 - in result end)
10.728 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.729 -
10.730 -
10.731 -operation_setup make_int = \<open>
10.732 - {from_lib = Codec.unit,
10.733 - to_lib = Codec.term,
10.734 - action = (fn _ => HOLogic.mk_number @{typ int} 3)}
10.735 -\<close>
10.736 -
10.737 -operation_setup test_term_transfer = \<open>
10.738 - {from_lib = Codec.tree,
10.739 - to_lib = Codec.tree,
10.740 - action = (fn intree =>
10.741 - (let
10.742 - val t = case intree of
10.743 - XML.Elem (("MATHML", []), [
10.744 - XML.Elem (("ISA", []), [XML.Text _]),
10.745 - XML.Elem (("TERM", []), [xt])])
10.746 - => xt |> Codec.decode Codec.term |> Codec.the_success
10.747 - | tree => raise ERROR ("test_term_transfer: WRONG intree = " ^ xmlstr 0 tree)
10.748 - val test_out = HOLogic.mk_eq (t, Const ("processed_by_Isabelle_Isac", type_of t))
10.749 - in xml_of_term_NEW test_out end)
10.750 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.751 -
10.752 -operation_setup test_term_one_way = \<open>
10.753 - {from_lib = Codec.string,
10.754 - to_lib = Codec.tree,
10.755 - action = (fn instr =>
10.756 - (let
10.757 - val t = instr |> parse @{theory} |> the |> Thm.term_of
10.758 - val test_out = HOLogic.mk_eq (t, Const ("processed_by_Isabelle_Isac", type_of t))
10.759 - in xml_of_term_NEW test_out end)
10.760 - handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
10.761 -
10.762 -end
11.1 --- a/libisabelle-protocol/isabelle/2015/lib/classy/Classy.thy Sat Feb 06 17:20:08 2016 +0100
11.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
11.3 @@ -1,22 +0,0 @@
11.4 -theory Classy
11.5 -imports Pure
11.6 -keywords
11.7 - "ML.class" :: thy_decl % "ML" and
11.8 - "ML.instance" :: thy_decl % "ML" and
11.9 - "ML.print_classes" :: diag
11.10 -begin
11.11 -
11.12 -ML_file "ml_types.ML"
11.13 -ML_file "classy.ML"
11.14 -
11.15 -setup \<open>Classy.setup\<close>
11.16 -
11.17 -ML_file "pretty_class.ML"
11.18 -
11.19 -ML.class pretty = \<open>'a pretty_class\<close>
11.20 -
11.21 -ML.instance \<open>Pretty_Class.string\<close> :: pretty
11.22 -ML.instance \<open>Pretty_Class.pretty\<close> :: pretty
11.23 -ML.instance \<open>Pretty_Class.list\<close> :: pretty
11.24 -
11.25 -end
11.26 \ No newline at end of file
12.1 --- a/libisabelle-protocol/isabelle/2015/lib/classy/Examples.thy Sat Feb 06 17:20:08 2016 +0100
12.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
12.3 @@ -1,18 +0,0 @@
12.4 -theory Examples
12.5 -imports Classy
12.6 -begin
12.7 -
12.8 -ML.print_classes
12.9 -
12.10 -ML\<open>format @{ML.resolve \<open>string list\<close> :: pretty} ["a", "b"] |> Pretty.writeln\<close> (* okay *)
12.11 -
12.12 -context begin
12.13 -
12.14 - (* conflicting instance *)
12.15 - ML.instance \<open>Pretty_Class.string\<close> :: pretty
12.16 -
12.17 - ML\<open>@{ML.resolve \<open>string\<close> :: pretty}\<close> (* error *)
12.18 -
12.19 -end
12.20 -
12.21 -end
12.22 \ No newline at end of file
13.1 --- a/libisabelle-protocol/isabelle/2015/lib/classy/LICENSE Sat Feb 06 17:20:08 2016 +0100
13.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
13.3 @@ -1,22 +0,0 @@
13.4 -The MIT License (MIT)
13.5 -
13.6 -Copyright (c) 2015 Lars Hupel
13.7 -
13.8 -Permission is hereby granted, free of charge, to any person obtaining a copy
13.9 -of this software and associated documentation files (the "Software"), to deal
13.10 -in the Software without restriction, including without limitation the rights
13.11 -to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
13.12 -copies of the Software, and to permit persons to whom the Software is
13.13 -furnished to do so, subject to the following conditions:
13.14 -
13.15 -The above copyright notice and this permission notice shall be included in all
13.16 -copies or substantial portions of the Software.
13.17 -
13.18 -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
13.19 -IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
13.20 -FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
13.21 -AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
13.22 -LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
13.23 -OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
13.24 -SOFTWARE.
13.25 -
14.1 --- a/libisabelle-protocol/isabelle/2015/lib/classy/README.md Sat Feb 06 17:20:08 2016 +0100
14.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
14.3 @@ -1,2 +0,0 @@
14.4 -# classy
14.5 -Type classes for Isabelle/ML
15.1 --- a/libisabelle-protocol/isabelle/2015/lib/classy/Test.thy Sat Feb 06 17:20:08 2016 +0100
15.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
15.3 @@ -1,50 +0,0 @@
15.4 -theory Test
15.5 -imports Classy
15.6 -begin
15.7 -
15.8 -section \<open>Parsing and printing types\<close>
15.9 -
15.10 -ML\<open>
15.11 -fun check t =
15.12 - let
15.13 - val t' = ML_Types.read_ml_type t |> ML_Types.pretty |> Pretty.string_of |> YXML.content_of
15.14 - in
15.15 - if t <> t' then
15.16 - error t'
15.17 - else
15.18 - ()
15.19 - end
15.20 -\<close>
15.21 -
15.22 -ML\<open>check "'a"\<close>
15.23 -ML\<open>check "'a * 'b"\<close>
15.24 -ML\<open>check "'a * 'b * 'c"\<close>
15.25 -ML\<open>check "('a * 'b) * 'c"\<close>
15.26 -ML\<open>check "'a * ('b * 'c)"\<close>
15.27 -ML\<open>check "'a * 'b -> 'c"\<close>
15.28 -ML\<open>check "'a * 'b -> 'a * 'b"\<close>
15.29 -ML\<open>check "('a -> 'b) * ('a -> 'b)"\<close>
15.30 -ML\<open>check "('a, 'b) foo"\<close>
15.31 -ML\<open>check "'a foo"\<close>
15.32 -ML\<open>check "unit foo"\<close>
15.33 -ML\<open>check "unit * 'a"\<close>
15.34 -ML\<open>check "'a foo * 'b foo bar"\<close>
15.35 -ML\<open>check "('a, unit) foo"\<close>
15.36 -ML\<open>check "('a * 'b) foo"\<close>
15.37 -ML\<open>check "('a -> 'b) foo"\<close>
15.38 -ML\<open>check "('a -> 'b, 'c) foo"\<close>
15.39 -ML\<open>check "('a -> 'b, 'c * 'd) foo"\<close>
15.40 -ML\<open>check "'a foo bar baz"\<close>
15.41 -ML\<open>check "('a foo, 'b) bar Long.ident.baz"\<close>
15.42 -ML\<open>check "{a: int}"\<close>
15.43 -ML\<open>check "{a: int, b: float}"\<close>
15.44 -ML\<open>check "{a: int, b: 'a -> 'b}"\<close>
15.45 -
15.46 -section \<open>Instance resolution\<close>
15.47 -
15.48 -ML\<open>@{ML.resolve \<open>string\<close> :: pretty}\<close>
15.49 -ML\<open>@{ML.resolve \<open>string list\<close> :: pretty}\<close>
15.50 -ML\<open>@{ML.resolve \<open>string list list\<close> :: pretty}\<close>
15.51 -ML\<open>@{ML.resolve \<open>Pretty.T\<close> :: pretty}\<close>
15.52 -
15.53 -end
15.54 \ No newline at end of file
16.1 --- a/libisabelle-protocol/isabelle/2015/lib/classy/classy.ML Sat Feb 06 17:20:08 2016 +0100
16.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
16.3 @@ -1,173 +0,0 @@
16.4 -signature CLASSY = sig
16.5 - val register_class: binding -> ML_Types.ml_type -> local_theory -> local_theory
16.6 - val register_class_cmd: binding -> string -> local_theory -> local_theory
16.7 -
16.8 - val register_instance_cmd: xstring * Position.T -> binding -> Input.source -> local_theory -> local_theory
16.9 -
16.10 - val check_class: Context.generic -> string * Position.T -> string
16.11 - val print_classes: Context.generic -> unit
16.12 -
16.13 - val resolve: string -> ML_Types.ml_type -> Context.generic -> string
16.14 -
16.15 - val setup: theory -> theory
16.16 -end
16.17 -
16.18 -structure Classy: CLASSY = struct
16.19 -
16.20 -type class_table = (ml_type * (ml_type * string) Name_Space.table) Name_Space.table
16.21 -
16.22 -exception DUP
16.23 -
16.24 -structure Classes = Generic_Data
16.25 -(
16.26 - type T = class_table
16.27 - val empty = Name_Space.empty_table "ML class"
16.28 - val merge = Name_Space.join_tables (fn _ => raise DUP) (* FIXME consistency check *)
16.29 - val extend = I
16.30 -)
16.31 -
16.32 -fun list_comb (term: string) (args: string list) =
16.33 - space_implode " " (enclose "(" ")" term :: map (enclose "(" ")") args)
16.34 -
16.35 -fun product [] = [[]]
16.36 - | product (xs :: xss) =
16.37 - maps (fn xs' => map (fn x => x :: xs') xs) (product xss)
16.38 -
16.39 -
16.40 -fun solve entries problem =
16.41 - let
16.42 - fun find (typ, term) =
16.43 - let
16.44 - val (args, candidate) = ML_Types.strip_fun typ
16.45 - in
16.46 - case ML_Types.match candidate problem [] of
16.47 - SOME env =>
16.48 - map (ML_Types.subst env) args
16.49 - |> map (solve entries)
16.50 - |> product
16.51 - |> map (list_comb term)
16.52 - | NONE => []
16.53 - end
16.54 - in
16.55 - maps find entries
16.56 - end
16.57 -
16.58 -fun resolve class typ context =
16.59 - let
16.60 - val classes = Classes.get context
16.61 - val (constructor, table) = Name_Space.get classes class
16.62 - val ML_Types.Con (name, [ML_Types.Var _]) = constructor
16.63 - val entries = map snd (Name_Space.extern_table true (Context.proof_of context) table)
16.64 - val problem = ML_Types.Con (name, [typ])
16.65 - val solutions = solve entries problem
16.66 - in
16.67 - case solutions of
16.68 - [] => error "no solutions"
16.69 - | [solution] => enclose "(" ")" solution
16.70 - | _ => error "too many solutions"
16.71 - end
16.72 -
16.73 -fun check_class context raw_binding =
16.74 - fst (Name_Space.check context (Classes.get context) raw_binding)
16.75 -
16.76 -val antiquote_setup =
16.77 - ML_Antiquotation.inline (Binding.qualify true "ML" @{binding class})
16.78 - (Scan.state -- Scan.lift (Parse.position Args.name) >>
16.79 - (fn (context, binding) => quote (check_class context binding))) #>
16.80 - ML_Antiquotation.inline (Binding.qualify true "ML" @{binding resolve})
16.81 - (Scan.state -- Scan.lift (Parse.ML_source --| @{keyword "::"} -- Parse.position Args.name) >>
16.82 - (fn (context, (source, binding)) =>
16.83 - resolve (check_class context binding) (ML_Types.read_ml_type (Input.source_content source)) context))
16.84 -
16.85 -fun pretty_classes context =
16.86 - let
16.87 - val table = Classes.get context
16.88 - val ctxt = Context.proof_of context
16.89 - val space = Name_Space.space_of_table table
16.90 - val entries = Name_Space.extern_table true ctxt table
16.91 -
16.92 - fun pretty_class ((class, _), (typ, sub_table)) =
16.93 - let
16.94 - val header = Pretty.block [Name_Space.pretty ctxt space class, Pretty.str ":", Pretty.brk 1, ML_Types.pretty typ]
16.95 -
16.96 - val sub_space = Name_Space.space_of_table sub_table
16.97 - val sub_entries = Name_Space.extern_table true ctxt sub_table
16.98 -
16.99 - fun pretty_instance ((instance, _), (typ, _)) =
16.100 - Pretty.item [Name_Space.pretty ctxt sub_space instance, Pretty.str ":", Pretty.brk 1, ML_Types.pretty typ]
16.101 -
16.102 - val instances = map pretty_instance sub_entries
16.103 - in
16.104 - Pretty.item (Pretty.fbreaks (header :: instances))
16.105 - end
16.106 - in
16.107 - Pretty.big_list "Classes" (map pretty_class entries)
16.108 - end
16.109 -
16.110 -val print_classes =
16.111 - Pretty.writeln o pretty_classes
16.112 -
16.113 -fun register_class binding typ =
16.114 - let
16.115 - val name =
16.116 - (case typ of
16.117 - ML_Types.Con (name, [ML_Types.Var _]) => name
16.118 - | _ => error "Malformed type")
16.119 - fun decl _ context =
16.120 - let
16.121 - val classes = Classes.get context
16.122 - val table = Name_Space.empty_table ("ML instances for " ^ name)
16.123 - val (_, classes') = Name_Space.define context true (binding, (typ, table)) classes
16.124 - in
16.125 - Classes.put classes' context
16.126 - end
16.127 - in
16.128 - Local_Theory.declaration {syntax = false, pervasive = false} decl
16.129 - end
16.130 -
16.131 -fun register_class_cmd binding typ =
16.132 - register_class binding (ML_Types.read_ml_type typ)
16.133 -
16.134 -fun register_instance_cmd raw_binding binding source lthy =
16.135 - let
16.136 - val typ = ML_Types.ml_type_of lthy (Input.source_content source)
16.137 - (* doesn't have any effect except for markup *)
16.138 - val _ = ML_Context.eval_source_in (SOME lthy) ML_Compiler.flags source
16.139 -
16.140 - (* FIXME check correct type *)
16.141 -
16.142 - fun decl _ context =
16.143 - let
16.144 - val classes = Classes.get context
16.145 - val (key, _) = Name_Space.check context classes raw_binding
16.146 - val upd = Name_Space.define context true (binding, (typ, Input.source_content source)) #> snd
16.147 - val classes' = Name_Space.map_table_entry key (apsnd upd) classes
16.148 - in Classes.put classes' context end
16.149 - in
16.150 - Local_Theory.declaration {syntax = false, pervasive = false} decl lthy
16.151 - end
16.152 -
16.153 -val _ =
16.154 - Outer_Syntax.local_theory @{command_keyword "ML.class"} "register new type class"
16.155 - (Parse.binding --| @{keyword "="} -- Parse.cartouche
16.156 - >> (fn (binding, typ) => register_class_cmd binding typ))
16.157 -
16.158 -val _ =
16.159 - let
16.160 - val opt_binding =
16.161 - Parse.binding --| @{keyword "="} ||
16.162 - Parse.position (Scan.succeed ()) >>
16.163 - (fn ((), pos) => Binding.make ("instance" ^ Markup.print_int (serial ()), pos))
16.164 - in
16.165 - Outer_Syntax.local_theory @{command_keyword "ML.instance"} "register new type class instance"
16.166 - (opt_binding -- (Parse.ML_source --| @{keyword "::"} -- Parse.position Args.name)
16.167 - >> (fn (binding, (source, name)) => register_instance_cmd name binding source))
16.168 - end
16.169 -
16.170 -val _ =
16.171 - Outer_Syntax.command @{command_keyword "ML.print_classes"} "print all registered classes"
16.172 - (Scan.succeed (Toplevel.keep (print_classes o Toplevel.generic_theory_of)))
16.173 -
16.174 -val setup = antiquote_setup
16.175 -
16.176 -end
16.177 \ No newline at end of file
17.1 --- a/libisabelle-protocol/isabelle/2015/lib/classy/ml_types.ML Sat Feb 06 17:20:08 2016 +0100
17.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
17.3 @@ -1,215 +0,0 @@
17.4 -signature ML_TYPES = sig
17.5 - datatype ml_type =
17.6 - Var of string |
17.7 - Con of string * ml_type list |
17.8 - Tuple of ml_type list |
17.9 - Fun of ml_type * ml_type |
17.10 - Record of (string * ml_type) list
17.11 -
17.12 - val unit: ml_type
17.13 - val canonicalize: ml_type -> ml_type
17.14 -
17.15 - val read_ml_type: string -> ml_type
17.16 - val ml_type_of: Proof.context -> string -> ml_type
17.17 -
17.18 - val pretty: ml_type -> Pretty.T
17.19 -
17.20 - type env = (string * ml_type) list
17.21 - val subst: env -> ml_type -> ml_type
17.22 - val match: ml_type -> ml_type -> env -> env option
17.23 -
17.24 - val strip_fun: ml_type -> ml_type list * ml_type
17.25 -end
17.26 -
17.27 -structure ML_Types: ML_TYPES = struct
17.28 -
17.29 -datatype ml_type =
17.30 - Var of string |
17.31 - Con of string * ml_type list |
17.32 - Tuple of ml_type list |
17.33 - Fun of ml_type * ml_type |
17.34 - Record of (string * ml_type) list
17.35 -
17.36 -val unit = Con ("unit", [])
17.37 -
17.38 -type env = (string * ml_type) list
17.39 -
17.40 -fun subst env (Con (name, ts)) = Con (name, map (subst env) ts)
17.41 - | subst env (Var name) = the_default (Var name) (AList.lookup op = env name)
17.42 - | subst env (Tuple ts) = Tuple (map (subst env) ts)
17.43 - | subst env (Fun (x, y)) = Fun (subst env x, subst env y)
17.44 - | subst env (Record fs) = Record (map (apsnd (subst env)) fs)
17.45 -
17.46 -fun match (Var name) t env =
17.47 - (case AList.lookup op = env name of
17.48 - NONE => SOME ((name, t) :: env)
17.49 - | SOME t' => if t = t' then SOME env else NONE)
17.50 - | match (Fun (x1, y1)) (Fun (x2, y2)) env =
17.51 - Option.mapPartial (match y1 y2) (match x1 x2 env)
17.52 - | match (Con (name1, ts1)) (Con (name2, ts2)) env =
17.53 - if name1 = name2 then match_list ts1 ts2 env else NONE
17.54 - | match (Tuple ts1) (Tuple ts2) env = match_list ts1 ts2 env
17.55 - | match (Record fs1) (Record fs2) env =
17.56 - if map fst fs1 = map fst fs2 then
17.57 - match_list (map snd fs1) (map snd fs2) env
17.58 - else
17.59 - NONE
17.60 - | match _ _ _ = NONE
17.61 -and match_list [] [] env = SOME env
17.62 - | match_list (t :: ts) (u :: us) env =Option.mapPartial (match t u) (match_list ts us env)
17.63 - | match_list _ _ _ = NONE
17.64 -
17.65 -fun strip_fun (Fun (x, y)) = let val (args, res) = strip_fun y in (x :: args, res) end
17.66 - | strip_fun t = ([], t)
17.67 -
17.68 -fun canonicalize (Var name) = Var name
17.69 - | canonicalize (Con (name, ts)) = Con (name, map canonicalize ts)
17.70 - | canonicalize (Tuple []) = unit
17.71 - | canonicalize (Tuple [t]) = canonicalize t
17.72 - | canonicalize (Tuple ts) = Tuple (map canonicalize ts)
17.73 - | canonicalize (Fun (t, u)) = Fun (canonicalize t, canonicalize u)
17.74 - | canonicalize (Record []) = unit
17.75 - | canonicalize (Record es) = Record (sort_wrt fst (map (apsnd canonicalize) es))
17.76 -
17.77 -val pretty =
17.78 - let
17.79 - datatype shape = SVar | SCon | STuple | SFun_Left | SRoot
17.80 -
17.81 - fun prec SVar _ = error "impossible"
17.82 - | prec SRoot _ = true
17.83 - | prec _ (Var _) = true
17.84 - | prec _ (Record _) = true
17.85 - | prec STuple (Con _) = true
17.86 - | prec STuple _ = false
17.87 - | prec SFun_Left (Con _) = true
17.88 - | prec SFun_Left (Tuple _) = true
17.89 - | prec SFun_Left (Fun _) = false
17.90 - | prec SCon (Con _) = true
17.91 - | prec SCon _ = false
17.92 -
17.93 - fun par n t p = if prec n t then p else Pretty.block [Pretty.str "(", p, Pretty.str ")"]
17.94 -
17.95 - fun aux s t =
17.96 - (case t of
17.97 - Var id => [Pretty.str id]
17.98 - | Tuple ts => Pretty.separate " *" (map (aux STuple) ts)
17.99 - | Fun (arg, res) =>
17.100 - [aux SFun_Left arg, Pretty.brk 1, Pretty.str "->", Pretty.brk 1, aux SRoot res]
17.101 - | Con (id, [t]) =>
17.102 - [aux SCon t, Pretty.brk 1, Pretty.str id]
17.103 - | Con (id, []) =>
17.104 - [Pretty.str id]
17.105 - | Con (id, ts) =>
17.106 - [Pretty.block (Pretty.str "(" :: Pretty.separate "," (map (aux SRoot) ts) @ [Pretty.str ")"]), Pretty.brk 1, Pretty.str id]
17.107 - | Record es =>
17.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 "}"])
17.109 - |> Pretty.block |> par s t
17.110 - in
17.111 - aux SRoot o canonicalize
17.112 - end
17.113 -
17.114 -type token = ML_Lex.token_kind * string
17.115 -
17.116 -type 'a parser = token list -> 'a * token list
17.117 -
17.118 -fun kind k: string parser = Scan.one (equal k o fst) >> snd
17.119 -fun tok t: unit parser = Scan.one (equal t) >> K ()
17.120 -fun keyword k: unit parser = tok (ML_Lex.Keyword, k)
17.121 -val open_parenthesis: unit parser = keyword "("
17.122 -val closed_parenthesis: unit parser = keyword ")"
17.123 -val open_brace: unit parser = keyword "{"
17.124 -val closed_brace: unit parser = keyword "}"
17.125 -val colon: unit parser = keyword ":"
17.126 -val comma: unit parser = keyword ","
17.127 -val arrow: unit parser = keyword "->"
17.128 -val asterisk: unit parser = tok (ML_Lex.Ident, "*")
17.129 -
17.130 -val ident: string parser =
17.131 - kind ML_Lex.Long_Ident ||
17.132 - Scan.one (fn (k, c) => k = ML_Lex.Ident andalso c <> "*") >> snd
17.133 -
17.134 -fun intersep p sep =
17.135 - (p ::: Scan.repeat (sep |-- p)) || Scan.succeed []
17.136 -
17.137 -val typ =
17.138 - let
17.139 - (* code partly lifted from Spec_Check *)
17.140 - fun make_con [] = raise Empty
17.141 - | make_con [c] = c
17.142 - | make_con (Con (s, _) :: cl) = Con (s, [make_con cl]);
17.143 -
17.144 - fun typ s = (func || tuple || typ_single) s
17.145 - and typ_arg s = (tuple || typ_single) s
17.146 - and typ_single s = (con || typ_basic) s
17.147 - and typ_basic s =
17.148 - (var
17.149 - || open_brace |-- record --| closed_brace
17.150 - || open_parenthesis |-- typ --| closed_parenthesis) s
17.151 - and list s = (open_parenthesis |-- typ -- Scan.repeat1 (comma |-- typ) --| closed_parenthesis >> op ::) s
17.152 - and var s = (kind ML_Lex.Type_Var >> Var) s
17.153 - and con s = ((con_nest
17.154 - || typ_basic -- con_nest >> (fn (b, Con (t, _) :: tl) => Con (t, [b]) :: tl)
17.155 - || list -- con_nest >> (fn (l, Con (t, _) :: tl) => Con (t, l) :: tl))
17.156 - >> (make_con o rev)) s
17.157 - and con_nest s = Scan.unless var (Scan.repeat1 (ident >> (Con o rpair []))) s
17.158 - and func s = (typ_arg --| arrow -- typ >> Fun) s
17.159 - and record s = (intersep (kind ML_Lex.Ident -- (colon |-- typ)) comma >> Record) s
17.160 - and tuple s = (typ_single -- Scan.repeat1 (asterisk |-- typ_single)
17.161 - >> (fn (t, tl) => Tuple (t :: tl))) s
17.162 - in typ end
17.163 -
17.164 -fun read_binding s =
17.165 - let
17.166 - val colon = (ML_Lex.Keyword, ":")
17.167 - val semicolon = (ML_Lex.Keyword, ";")
17.168 - fun unpack_tok tok = (ML_Lex.kind_of tok, ML_Lex.content_of tok)
17.169 - val toks = filter (not o equal ML_Lex.Space o fst) (map unpack_tok (ML_Lex.tokenize s))
17.170 - val junk = (Scan.many (not o equal colon) -- tok colon) >> K ()
17.171 - val stopper = Scan.stopper (K semicolon) (equal semicolon)
17.172 - val all = junk |-- Scan.finite stopper typ
17.173 - val (typ, rest) = all toks
17.174 - in
17.175 - if null rest then
17.176 - typ
17.177 - else
17.178 - error "Could not fully parse type"
17.179 - end
17.180 -
17.181 -fun read_ml_type s =
17.182 - let
17.183 - (* FIXME deduplicate *)
17.184 - val semicolon = (ML_Lex.Keyword, ";")
17.185 - fun unpack_tok tok = (ML_Lex.kind_of tok, ML_Lex.content_of tok)
17.186 - val toks = filter (not o equal ML_Lex.Space o fst) (map unpack_tok (ML_Lex.tokenize s))
17.187 - val stopper = Scan.stopper (K semicolon) (equal semicolon)
17.188 - val all = Scan.finite stopper typ
17.189 - val (typ, rest) = all toks
17.190 - in
17.191 - if null rest then
17.192 - typ
17.193 - else
17.194 - error "Could not fully parse type"
17.195 - end
17.196 -
17.197 -fun ml_type_of ctxt s =
17.198 - let
17.199 - (* code partly lifted from Spec_Check *)
17.200 - val return = Unsynchronized.ref NONE
17.201 - val s = "(fn () => (" ^ s ^ "))"
17.202 - val use_context: use_context =
17.203 - {tune_source = #tune_source ML_Env.local_context,
17.204 - name_space = #name_space ML_Env.local_context,
17.205 - str_of_pos = #str_of_pos ML_Env.local_context,
17.206 - print = fn r => return := SOME r,
17.207 - error = #error ML_Env.local_context}
17.208 - val _ =
17.209 - Context.setmp_thread_data (SOME (Context.Proof ctxt))
17.210 - (fn () => Secure.use_text use_context (0, "generated code") true s) ()
17.211 - val (Fun (Con ("unit", []), typ)) = read_binding (the (! return))
17.212 - in
17.213 - typ
17.214 - end
17.215 -
17.216 -end
17.217 -
17.218 -type ml_type = ML_Types.ml_type
18.1 --- a/libisabelle-protocol/isabelle/2015/lib/classy/pretty_class.ML Sat Feb 06 17:20:08 2016 +0100
18.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
18.3 @@ -1,12 +0,0 @@
18.4 -datatype 'a pretty_class = Pretty of ('a -> Pretty.T)
18.5 -
18.6 -fun format (Pretty f) = f
18.7 -
18.8 -structure Pretty_Class = struct
18.9 -
18.10 -val string: string pretty_class = Pretty Pretty.str
18.11 -val pretty: Pretty.T pretty_class = Pretty I
18.12 -fun list (Pretty f): 'a list pretty_class =
18.13 - Pretty (fn xs => Pretty.block (Pretty.str "[" :: Pretty.separate "," (map f xs) @ [Pretty.str "]"]))
18.14 -
18.15 -end
18.16 \ No newline at end of file
19.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
19.2 +++ b/libisabelle-protocol/lib/classy/.git Wed Apr 06 16:56:47 2016 +0200
19.3 @@ -0,0 +1,1 @@
19.4 +gitdir: ../../../../../../.git/modules/libisabelle/src/main/isabelle/lib/classy
20.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
20.2 +++ b/libisabelle-protocol/lib/classy/.gitignore Wed Apr 06 16:56:47 2016 +0200
20.3 @@ -0,0 +1,1 @@
20.4 +Scratch.thy
21.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
21.2 +++ b/libisabelle-protocol/lib/classy/.gitmodules Wed Apr 06 16:56:47 2016 +0200
21.3 @@ -0,0 +1,3 @@
21.4 +[submodule "lib/multi-isabelle"]
21.5 + path = lib/multi-isabelle
21.6 + url = https://github.com/larsrh/multi-isabelle.git
22.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
22.2 +++ b/libisabelle-protocol/lib/classy/Classy.thy Wed Apr 06 16:56:47 2016 +0200
22.3 @@ -0,0 +1,32 @@
22.4 +theory Classy
22.5 +imports Pure "lib/multi-isabelle/Multi_Isabelle"
22.6 +keywords
22.7 + "ML.class" :: thy_decl % "ML" and
22.8 + "ML.instance" :: thy_decl % "ML" and
22.9 + "ML.print_classes" :: diag
22.10 +begin
22.11 +
22.12 +ML_cond ("2015") \<open>
22.13 + val sort_by = sort_wrt
22.14 + fun secure_use_text context {line, file, verbose, debug} txt =
22.15 + Secure.use_text context (line, file) verbose txt
22.16 +\<close>
22.17 +
22.18 +ML_cond ("2016") \<open>
22.19 + val secure_use_text = Secure.use_text
22.20 +\<close>
22.21 +
22.22 +ML_file "ml_types.ML"
22.23 +ML_file "classy.ML"
22.24 +
22.25 +setup \<open>Classy.setup\<close>
22.26 +
22.27 +ML_file "pretty_class.ML"
22.28 +
22.29 +ML.class pretty = \<open>'a pretty_class\<close>
22.30 +
22.31 +ML.instance \<open>Pretty_Class.string\<close> :: pretty
22.32 +ML.instance \<open>Pretty_Class.pretty\<close> :: pretty
22.33 +ML.instance \<open>Pretty_Class.list\<close> :: pretty
22.34 +
22.35 +end
22.36 \ No newline at end of file
23.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
23.2 +++ b/libisabelle-protocol/lib/classy/Examples.thy Wed Apr 06 16:56:47 2016 +0200
23.3 @@ -0,0 +1,18 @@
23.4 +theory Examples
23.5 +imports Classy
23.6 +begin
23.7 +
23.8 +ML.print_classes
23.9 +
23.10 +ML\<open>format @{ML.resolve \<open>string list\<close> :: pretty} ["a", "b"] |> Pretty.writeln\<close> (* okay *)
23.11 +
23.12 +context begin
23.13 +
23.14 + (* conflicting instance *)
23.15 + ML.instance \<open>Pretty_Class.string\<close> :: pretty
23.16 +
23.17 + ML\<open>@{ML.resolve \<open>string\<close> :: pretty}\<close> (* error *)
23.18 +
23.19 +end
23.20 +
23.21 +end
23.22 \ No newline at end of file
24.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
24.2 +++ b/libisabelle-protocol/lib/classy/LICENSE Wed Apr 06 16:56:47 2016 +0200
24.3 @@ -0,0 +1,22 @@
24.4 +The MIT License (MIT)
24.5 +
24.6 +Copyright (c) 2015 Lars Hupel
24.7 +
24.8 +Permission is hereby granted, free of charge, to any person obtaining a copy
24.9 +of this software and associated documentation files (the "Software"), to deal
24.10 +in the Software without restriction, including without limitation the rights
24.11 +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
24.12 +copies of the Software, and to permit persons to whom the Software is
24.13 +furnished to do so, subject to the following conditions:
24.14 +
24.15 +The above copyright notice and this permission notice shall be included in all
24.16 +copies or substantial portions of the Software.
24.17 +
24.18 +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
24.19 +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
24.20 +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
24.21 +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
24.22 +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
24.23 +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
24.24 +SOFTWARE.
24.25 +
25.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
25.2 +++ b/libisabelle-protocol/lib/classy/README.md Wed Apr 06 16:56:47 2016 +0200
25.3 @@ -0,0 +1,2 @@
25.4 +# classy
25.5 +Type classes for Isabelle/ML
26.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
26.2 +++ b/libisabelle-protocol/lib/classy/ROOT Wed Apr 06 16:56:47 2016 +0200
26.3 @@ -0,0 +1,9 @@
26.4 +session Classy = Pure +
26.5 + theories
26.6 + Classy
26.7 + Test
26.8 +
26.9 +session "HOL-Classy" = HOL +
26.10 + theories
26.11 + Classy
26.12 + Test
27.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
27.2 +++ b/libisabelle-protocol/lib/classy/Test.thy Wed Apr 06 16:56:47 2016 +0200
27.3 @@ -0,0 +1,50 @@
27.4 +theory Test
27.5 +imports Classy
27.6 +begin
27.7 +
27.8 +section \<open>Parsing and printing types\<close>
27.9 +
27.10 +ML\<open>
27.11 +fun check t =
27.12 + let
27.13 + val t' = ML_Types.read_ml_type t |> ML_Types.pretty |> Pretty.string_of |> YXML.content_of
27.14 + in
27.15 + if t <> t' then
27.16 + error t'
27.17 + else
27.18 + ()
27.19 + end
27.20 +\<close>
27.21 +
27.22 +ML\<open>check "'a"\<close>
27.23 +ML\<open>check "'a * 'b"\<close>
27.24 +ML\<open>check "'a * 'b * 'c"\<close>
27.25 +ML\<open>check "('a * 'b) * 'c"\<close>
27.26 +ML\<open>check "'a * ('b * 'c)"\<close>
27.27 +ML\<open>check "'a * 'b -> 'c"\<close>
27.28 +ML\<open>check "'a * 'b -> 'a * 'b"\<close>
27.29 +ML\<open>check "('a -> 'b) * ('a -> 'b)"\<close>
27.30 +ML\<open>check "('a, 'b) foo"\<close>
27.31 +ML\<open>check "'a foo"\<close>
27.32 +ML\<open>check "unit foo"\<close>
27.33 +ML\<open>check "unit * 'a"\<close>
27.34 +ML\<open>check "'a foo * 'b foo bar"\<close>
27.35 +ML\<open>check "('a, unit) foo"\<close>
27.36 +ML\<open>check "('a * 'b) foo"\<close>
27.37 +ML\<open>check "('a -> 'b) foo"\<close>
27.38 +ML\<open>check "('a -> 'b, 'c) foo"\<close>
27.39 +ML\<open>check "('a -> 'b, 'c * 'd) foo"\<close>
27.40 +ML\<open>check "'a foo bar baz"\<close>
27.41 +ML\<open>check "('a foo, 'b) bar Long.ident.baz"\<close>
27.42 +ML\<open>check "{a: int}"\<close>
27.43 +ML\<open>check "{a: int, b: float}"\<close>
27.44 +ML\<open>check "{a: int, b: 'a -> 'b}"\<close>
27.45 +
27.46 +section \<open>Instance resolution\<close>
27.47 +
27.48 +ML\<open>@{ML.resolve \<open>string\<close> :: pretty}\<close>
27.49 +ML\<open>@{ML.resolve \<open>string list\<close> :: pretty}\<close>
27.50 +ML\<open>@{ML.resolve \<open>string list list\<close> :: pretty}\<close>
27.51 +ML\<open>@{ML.resolve \<open>Pretty.T\<close> :: pretty}\<close>
27.52 +
27.53 +end
27.54 \ No newline at end of file
28.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
28.2 +++ b/libisabelle-protocol/lib/classy/classy.ML Wed Apr 06 16:56:47 2016 +0200
28.3 @@ -0,0 +1,173 @@
28.4 +signature CLASSY = sig
28.5 + val register_class: binding -> ML_Types.ml_type -> local_theory -> local_theory
28.6 + val register_class_cmd: binding -> string -> local_theory -> local_theory
28.7 +
28.8 + val register_instance_cmd: xstring * Position.T -> binding -> Input.source -> local_theory -> local_theory
28.9 +
28.10 + val check_class: Context.generic -> string * Position.T -> string
28.11 + val print_classes: Context.generic -> unit
28.12 +
28.13 + val resolve: string -> ML_Types.ml_type -> Context.generic -> string
28.14 +
28.15 + val setup: theory -> theory
28.16 +end
28.17 +
28.18 +structure Classy: CLASSY = struct
28.19 +
28.20 +type class_table = (ml_type * (ml_type * string) Name_Space.table) Name_Space.table
28.21 +
28.22 +exception DUP
28.23 +
28.24 +structure Classes = Generic_Data
28.25 +(
28.26 + type T = class_table
28.27 + val empty = Name_Space.empty_table "ML class"
28.28 + val merge = Name_Space.join_tables (fn _ => raise DUP) (* FIXME consistency check *)
28.29 + val extend = I
28.30 +)
28.31 +
28.32 +fun list_comb (term: string) (args: string list) =
28.33 + space_implode " " (enclose "(" ")" term :: map (enclose "(" ")") args)
28.34 +
28.35 +fun product [] = [[]]
28.36 + | product (xs :: xss) =
28.37 + maps (fn xs' => map (fn x => x :: xs') xs) (product xss)
28.38 +
28.39 +
28.40 +fun solve entries problem =
28.41 + let
28.42 + fun find (typ, term) =
28.43 + let
28.44 + val (args, candidate) = ML_Types.strip_fun typ
28.45 + in
28.46 + case ML_Types.match candidate problem [] of
28.47 + SOME env =>
28.48 + map (ML_Types.subst env) args
28.49 + |> map (solve entries)
28.50 + |> product
28.51 + |> map (list_comb term)
28.52 + | NONE => []
28.53 + end
28.54 + in
28.55 + maps find entries
28.56 + end
28.57 +
28.58 +fun resolve class typ context =
28.59 + let
28.60 + val classes = Classes.get context
28.61 + val (constructor, table) = Name_Space.get classes class
28.62 + val ML_Types.Con (name, [ML_Types.Var _]) = constructor
28.63 + val entries = map snd (Name_Space.extern_table true (Context.proof_of context) table)
28.64 + val problem = ML_Types.Con (name, [typ])
28.65 + val solutions = solve entries problem
28.66 + in
28.67 + case solutions of
28.68 + [] => error "no solutions"
28.69 + | [solution] => enclose "(" ")" solution
28.70 + | _ => error "too many solutions"
28.71 + end
28.72 +
28.73 +fun check_class context raw_binding =
28.74 + fst (Name_Space.check context (Classes.get context) raw_binding)
28.75 +
28.76 +val antiquote_setup =
28.77 + ML_Antiquotation.inline (Binding.qualify true "ML" @{binding class})
28.78 + (Scan.state -- Scan.lift (Parse.position Args.name) >>
28.79 + (fn (context, binding) => quote (check_class context binding))) #>
28.80 + ML_Antiquotation.inline (Binding.qualify true "ML" @{binding resolve})
28.81 + (Scan.state -- Scan.lift (Parse.ML_source --| @{keyword "::"} -- Parse.position Args.name) >>
28.82 + (fn (context, (source, binding)) =>
28.83 + resolve (check_class context binding) (ML_Types.read_ml_type (Input.source_content source)) context))
28.84 +
28.85 +fun pretty_classes context =
28.86 + let
28.87 + val table = Classes.get context
28.88 + val ctxt = Context.proof_of context
28.89 + val space = Name_Space.space_of_table table
28.90 + val entries = Name_Space.extern_table true ctxt table
28.91 +
28.92 + fun pretty_class ((class, _), (typ, sub_table)) =
28.93 + let
28.94 + val header = Pretty.block [Name_Space.pretty ctxt space class, Pretty.str ":", Pretty.brk 1, ML_Types.pretty typ]
28.95 +
28.96 + val sub_space = Name_Space.space_of_table sub_table
28.97 + val sub_entries = Name_Space.extern_table true ctxt sub_table
28.98 +
28.99 + fun pretty_instance ((instance, _), (typ, _)) =
28.100 + Pretty.item [Name_Space.pretty ctxt sub_space instance, Pretty.str ":", Pretty.brk 1, ML_Types.pretty typ]
28.101 +
28.102 + val instances = map pretty_instance sub_entries
28.103 + in
28.104 + Pretty.item (Pretty.fbreaks (header :: instances))
28.105 + end
28.106 + in
28.107 + Pretty.big_list "Classes" (map pretty_class entries)
28.108 + end
28.109 +
28.110 +val print_classes =
28.111 + Pretty.writeln o pretty_classes
28.112 +
28.113 +fun register_class binding typ =
28.114 + let
28.115 + val name =
28.116 + (case typ of
28.117 + ML_Types.Con (name, [ML_Types.Var _]) => name
28.118 + | _ => error "Malformed type")
28.119 + fun decl _ context =
28.120 + let
28.121 + val classes = Classes.get context
28.122 + val table = Name_Space.empty_table ("ML instances for " ^ name)
28.123 + val (_, classes') = Name_Space.define context true (binding, (typ, table)) classes
28.124 + in
28.125 + Classes.put classes' context
28.126 + end
28.127 + in
28.128 + Local_Theory.declaration {syntax = false, pervasive = false} decl
28.129 + end
28.130 +
28.131 +fun register_class_cmd binding typ =
28.132 + register_class binding (ML_Types.read_ml_type typ)
28.133 +
28.134 +fun register_instance_cmd raw_binding binding source lthy =
28.135 + let
28.136 + val typ = ML_Types.ml_type_of lthy (Input.source_content source)
28.137 + (* doesn't have any effect except for markup *)
28.138 + val _ = ML_Context.eval_source_in (SOME lthy) ML_Compiler.flags source
28.139 +
28.140 + (* FIXME check correct type *)
28.141 +
28.142 + fun decl _ context =
28.143 + let
28.144 + val classes = Classes.get context
28.145 + val (key, _) = Name_Space.check context classes raw_binding
28.146 + val upd = Name_Space.define context true (binding, (typ, Input.source_content source)) #> snd
28.147 + val classes' = Name_Space.map_table_entry key (apsnd upd) classes
28.148 + in Classes.put classes' context end
28.149 + in
28.150 + Local_Theory.declaration {syntax = false, pervasive = false} decl lthy
28.151 + end
28.152 +
28.153 +val _ =
28.154 + Outer_Syntax.local_theory @{command_keyword "ML.class"} "register new type class"
28.155 + (Parse.binding --| @{keyword "="} -- Parse.cartouche
28.156 + >> (fn (binding, typ) => register_class_cmd binding typ))
28.157 +
28.158 +val _ =
28.159 + let
28.160 + val opt_binding =
28.161 + Parse.binding --| @{keyword "="} ||
28.162 + Parse.position (Scan.succeed ()) >>
28.163 + (fn ((), pos) => Binding.make ("instance" ^ Markup.print_int (serial ()), pos))
28.164 + in
28.165 + Outer_Syntax.local_theory @{command_keyword "ML.instance"} "register new type class instance"
28.166 + (opt_binding -- (Parse.ML_source --| @{keyword "::"} -- Parse.position Args.name)
28.167 + >> (fn (binding, (source, name)) => register_instance_cmd name binding source))
28.168 + end
28.169 +
28.170 +val _ =
28.171 + Outer_Syntax.command @{command_keyword "ML.print_classes"} "print all registered classes"
28.172 + (Scan.succeed (Toplevel.keep (print_classes o Toplevel.generic_theory_of)))
28.173 +
28.174 +val setup = antiquote_setup
28.175 +
28.176 +end
28.177 \ No newline at end of file
29.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
29.2 +++ b/libisabelle-protocol/lib/classy/lib/multi-isabelle/.git Wed Apr 06 16:56:47 2016 +0200
29.3 @@ -0,0 +1,1 @@
29.4 +gitdir: /home/lars/proj/libisabelle/.git/modules/libisabelle/src/main/isabelle/lib/classy/modules/lib/multi-isabelle
30.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
30.2 +++ b/libisabelle-protocol/lib/classy/lib/multi-isabelle/LICENSE Wed Apr 06 16:56:47 2016 +0200
30.3 @@ -0,0 +1,21 @@
30.4 +The MIT License (MIT)
30.5 +
30.6 +Copyright (c) 2016 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.
31.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
31.2 +++ b/libisabelle-protocol/lib/classy/lib/multi-isabelle/Multi_Isabelle.thy Wed Apr 06 16:56:47 2016 +0200
31.3 @@ -0,0 +1,9 @@
31.4 +theory Multi_Isabelle
31.5 +imports Pure
31.6 +keywords
31.7 + "ML_cond" :: thy_decl % "ML"
31.8 +begin
31.9 +
31.10 +ML_file "ml_cond.ML"
31.11 +
31.12 +end
31.13 \ No newline at end of file
32.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
32.2 +++ b/libisabelle-protocol/lib/classy/lib/multi-isabelle/README.md Wed Apr 06 16:56:47 2016 +0200
32.3 @@ -0,0 +1,2 @@
32.4 +# multi-isabelle
32.5 +Conditional Isabelle/ML execution depending on Isabelle version
33.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
33.2 +++ b/libisabelle-protocol/lib/classy/lib/multi-isabelle/ml_cond.ML Wed Apr 06 16:56:47 2016 +0200
33.3 @@ -0,0 +1,28 @@
33.4 +signature ML_COND = sig
33.5 + val isabelle_version: string
33.6 +
33.7 + val cond_exec: Input.source -> string list -> generic_theory -> generic_theory
33.8 +end
33.9 +
33.10 +structure ML_Cond: ML_COND = struct
33.11 +
33.12 +val isabelle_version = getenv_strict "ISABELLE_VERSION"
33.13 +
33.14 +val _ = writeln ("Initializing ML_COND with ISABELLE_VERSION=" ^ isabelle_version)
33.15 +
33.16 +fun cond_exec source versions =
33.17 + member op = versions isabelle_version ?
33.18 + ML_Context.exec (fn () =>
33.19 + ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source) #>
33.20 + Local_Theory.propagate_ml_env
33.21 +
33.22 +val _ =
33.23 + let
33.24 + val parse_versions = Args.parens (Parse.list Parse.string)
33.25 + in
33.26 + Outer_Syntax.command @{command_keyword ML_cond} "ML text within theory or local theory (conditional)"
33.27 + (parse_versions -- Parse.ML_source >> (fn (versions, source) =>
33.28 + Toplevel.generic_theory (cond_exec source versions)))
33.29 + end
33.30 +
33.31 +end
33.32 \ No newline at end of file
34.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
34.2 +++ b/libisabelle-protocol/lib/classy/ml_types.ML Wed Apr 06 16:56:47 2016 +0200
34.3 @@ -0,0 +1,220 @@
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_by 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 flags =
34.209 + {file = "generated code",
34.210 + line = 0,
34.211 + debug = false,
34.212 + verbose = true}
34.213 + val _ =
34.214 + Context.setmp_thread_data (SOME (Context.Proof ctxt))
34.215 + (fn () => secure_use_text use_context flags s) ()
34.216 + val (Fun (Con ("unit", []), typ)) = read_binding (the (! return))
34.217 + in
34.218 + typ
34.219 + end
34.220 +
34.221 +end
34.222 +
34.223 +type ml_type = ML_Types.ml_type
35.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
35.2 +++ b/libisabelle-protocol/lib/classy/pretty_class.ML Wed Apr 06 16:56:47 2016 +0200
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 --- a/libisabelle-protocol/operations/Basic.thy Sat Feb 06 17:20:08 2016 +0100
36.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
36.3 @@ -1,46 +0,0 @@
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 --- a/libisabelle-protocol/operations/HOL_Operations.thy Sat Feb 06 17:20:08 2016 +0100
37.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
37.3 @@ -1,16 +0,0 @@
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 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
38.2 +++ b/libisabelle-protocol/protocol/Codec_Class.thy Wed Apr 06 16:56:47 2016 +0200
38.3 @@ -0,0 +1,21 @@
38.4 +theory Codec_Class
38.5 +imports Common "../lib/classy/Classy"
38.6 +begin
38.7 +
38.8 +ML.class codec = \<open>'a codec\<close>
38.9 +
38.10 +ML.instance \<open>Codec.unit\<close> :: codec
38.11 +ML.instance \<open>Codec.bool\<close> :: codec
38.12 +ML.instance \<open>Codec.string\<close> :: codec
38.13 +ML.instance \<open>Codec.int\<close> :: codec
38.14 +ML.instance \<open>Codec.list\<close> :: codec
38.15 +ML.instance \<open>Codec.tuple\<close> :: codec
38.16 +ML.instance \<open>Codec.option\<close> :: codec
38.17 +ML.instance \<open>Codec.either\<close> :: codec
38.18 +ML.instance \<open>Codec.triple\<close> :: codec
38.19 +ML.instance \<open>Codec.sort\<close> :: codec
38.20 +ML.instance \<open>Codec.typ\<close> :: codec
38.21 +ML.instance \<open>Codec.term\<close> :: codec
38.22 +ML.instance \<open>Codec.tree\<close> :: codec
38.23 +
38.24 +end
39.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
39.2 +++ b/libisabelle-protocol/protocol/Codec_Test.thy Wed Apr 06 16:56:47 2016 +0200
39.3 @@ -0,0 +1,36 @@
39.4 +theory Codec_Test
39.5 +imports Common "~~/src/Tools/Spec_Check/Spec_Check"
39.6 +begin
39.7 +
39.8 +ML\<open>
39.9 +fun check_for str =
39.10 + let
39.11 + val prop =
39.12 + "ALL x. (let val c = (" ^ str ^ ") in Codec.decode c (Codec.encode c x) = Codec.Success x end)"
39.13 + in check_property prop end
39.14 +
39.15 +fun gen_unit r =
39.16 + ((), r)
39.17 +\<close>
39.18 +
39.19 +ML_command\<open>
39.20 + check_for "Codec.unit";
39.21 + check_for "Codec.int";
39.22 + check_for "Codec.bool";
39.23 + check_for "Codec.string";
39.24 + check_for "Codec.tuple Codec.int Codec.int";
39.25 + check_for "Codec.tuple Codec.string Codec.unit";
39.26 + check_for "Codec.list Codec.unit";
39.27 + check_for "Codec.list Codec.int";
39.28 + check_for "Codec.list Codec.string";
39.29 + check_for "Codec.list (Codec.list Codec.string)";
39.30 + check_for "Codec.list (Codec.tuple Codec.int Codec.int)";
39.31 + check_for "Codec.tuple Codec.int (Codec.list Codec.int)";
39.32 + check_for "Codec.option Codec.int";
39.33 + check_for "Codec.option (Codec.list Codec.int)";
39.34 + check_for "Codec.list (Codec.option (Codec.int))";
39.35 + check_for "Codec.term";
39.36 + check_for "Codec.typ";
39.37 +\<close>
39.38 +
39.39 +end
40.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
40.2 +++ b/libisabelle-protocol/protocol/Common.thy Wed Apr 06 16:56:47 2016 +0200
40.3 @@ -0,0 +1,8 @@
40.4 +theory Common
40.5 +imports Pure
40.6 +begin
40.7 +
40.8 +ML_file "codec.ML"
40.9 +ML_file "protocol.ML"
40.10 +
40.11 +end
40.12 \ No newline at end of file
41.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
41.2 +++ b/libisabelle-protocol/protocol/Protocol.thy Wed Apr 06 16:56:47 2016 +0200
41.3 @@ -0,0 +1,53 @@
41.4 +theory Protocol
41.5 +imports Codec_Class
41.6 +keywords "operation_setup" :: thy_decl % "ML"
41.7 +begin
41.8 +
41.9 +ML\<open>
41.10 +val _ =
41.11 + let
41.12 + open Protocol
41.13 + fun operation_setup_cmd name source (flags as {auto, ...}) ctxt =
41.14 + let
41.15 + fun eval enclose =
41.16 + ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of source)
41.17 + (ML_Lex.read ("Protocol.add_operation " ^ ML_Syntax.print_string name ^ "(") @
41.18 + enclose (ML_Lex.read_source false source) @
41.19 + ML_Lex.read ")" @
41.20 + ML_Lex.read (print_flags flags))
41.21 + in
41.22 + if auto then
41.23 + let
41.24 + val ML_Types.Fun (arg, res) = ML_Types.ml_type_of ctxt (Input.source_content source)
41.25 + val arg_codec = Classy.resolve @{ML.class codec} arg (Context.Proof ctxt)
41.26 + val res_codec = Classy.resolve @{ML.class codec} res (Context.Proof ctxt)
41.27 + fun enclose toks =
41.28 + ML_Lex.read "{from_lib=" @ ML_Lex.read arg_codec @ ML_Lex.read "," @
41.29 + ML_Lex.read "to_lib=" @ ML_Lex.read res_codec @ ML_Lex.read "," @
41.30 + ML_Lex.read "action=" @ toks @ ML_Lex.read "}"
41.31 + in
41.32 + eval enclose
41.33 + end
41.34 + else
41.35 + eval I
41.36 + end
41.37 + val parse_flag =
41.38 + (Parse.reserved "sequential" || Parse.reserved "bracket" || Parse.reserved "auto") >>
41.39 + (fn flag => join_flags
41.40 + {sequential = flag = "sequential",
41.41 + bracket = flag = "bracket",
41.42 + auto = flag = "auto"})
41.43 + val parse_flags =
41.44 + Parse.list parse_flag >> (fn fs => fold (curry op o) fs I)
41.45 + val parse_cmd =
41.46 + Scan.optional (Args.parens parse_flags) I --
41.47 + Parse.name --
41.48 + Parse.!!! (@{keyword "="} |-- Parse.ML_source)
41.49 + in
41.50 + Outer_Syntax.command @{command_keyword "operation_setup"} "define protocol operation in ML"
41.51 + (parse_cmd >> (fn ((flags, name), txt) =>
41.52 + Toplevel.keep (Toplevel.context_of #> operation_setup_cmd name txt (flags default_flags))))
41.53 + end
41.54 +\<close>
41.55 +
41.56 +end
42.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
42.2 +++ b/libisabelle-protocol/protocol/codec.ML Wed Apr 06 16:56:47 2016 +0200
42.3 @@ -0,0 +1,242 @@
42.4 +signature CODEC = sig
42.5 + datatype 'a result = Success of 'a | Failure of string * XML.body
42.6 + datatype ('a, 'b) either = Left of 'a | Right of 'b
42.7 + type 'a codec
42.8 +
42.9 + val the_success: 'a result -> 'a
42.10 +
42.11 + val map_result: ('a -> 'b) -> 'a result -> 'b result
42.12 + val bind_result: ('a -> 'b result) -> 'a result -> 'b result
42.13 + val sequence_results: 'a result list -> 'a list result
42.14 + val traverse_results: ('a -> 'b result) -> 'a list -> 'b list result
42.15 +
42.16 + val transform: ('a -> 'b) -> ('b -> 'a) -> 'a codec -> 'b codec
42.17 + val encode: 'a codec -> 'a -> XML.tree
42.18 + val decode: 'a codec -> XML.tree -> 'a result
42.19 +
42.20 + val basic: {encode: 'a -> XML.tree, decode: XML.tree -> 'a result} -> 'a codec
42.21 +
42.22 + val variant: ('a -> (int * XML.tree)) -> (int -> (XML.tree -> 'a result) option) -> string -> 'a codec
42.23 + val tagged: string -> 'a codec -> 'a codec
42.24 +
42.25 + val unit: unit codec
42.26 + val bool: bool codec
42.27 + val string: string codec
42.28 + val int: int codec
42.29 + val list: 'a codec -> 'a list codec
42.30 + val tuple: 'a codec -> 'b codec -> ('a * 'b) codec
42.31 + val triple: 'a codec -> 'b codec -> 'c codec -> ('a * 'b * 'c) codec
42.32 + val either: 'a codec -> 'b codec -> ('a, 'b) either codec
42.33 + val option: 'a codec -> 'a option codec
42.34 + val tree: XML.tree codec
42.35 +
42.36 + val sort: sort codec
42.37 + val typ: typ codec
42.38 + val term: term codec
42.39 +
42.40 + exception GENERIC of string
42.41 + val exn: exn codec
42.42 + val exn_result: 'a codec -> 'a Exn.result codec
42.43 +
42.44 + val id: XML.tree codec (* internal *)
42.45 +end
42.46 +
42.47 +structure Codec: CODEC = struct
42.48 +
42.49 +datatype 'a result = Success of 'a | Failure of string * XML.body
42.50 +datatype ('a, 'b) either = Left of 'a | Right of 'b
42.51 +
42.52 +fun map_result f (Success a) = Success (f a)
42.53 + | map_result _ (Failure (msg, body)) = Failure (msg, body)
42.54 +
42.55 +fun bind_result f (Success a) = f a
42.56 + | bind_result _ (Failure (msg, body)) = Failure (msg, body)
42.57 +
42.58 +fun traverse_results _ [] = Success []
42.59 + | traverse_results f (x :: xs) =
42.60 + case f x of
42.61 + Success y => map_result (fn ys => y :: ys) (traverse_results f xs)
42.62 + | Failure (msg, body) => Failure (msg, body)
42.63 +
42.64 +fun sequence_results xs = traverse_results I xs
42.65 +
42.66 +fun the_success (Success a) = a
42.67 + | the_success _ = raise Fail "unexpected failure"
42.68 +
42.69 +fun add_tag tag idx body =
42.70 + let
42.71 + val attrs = case idx of SOME i => [("idx", XML.Encode.int_atom i)] | _ => []
42.72 + in XML.Elem (("tag", ("type", tag) :: attrs), body) end
42.73 +
42.74 +fun expect_tag tag tree =
42.75 + case tree of
42.76 + XML.Elem (("tag", [("type", tag')]), body) =>
42.77 + if tag = tag' then
42.78 + Success body
42.79 + else
42.80 + Failure ("tag mismatch: expected " ^ tag ^ ", got " ^ tag', [tree])
42.81 + | _ =>
42.82 + Failure ("tag " ^ tag ^ " expected", [tree])
42.83 +
42.84 +fun expect_tag' tag tree =
42.85 + case tree of
42.86 + XML.Elem (("tag", [("type", tag'), ("idx", i)]), body) =>
42.87 + if tag = tag' then
42.88 + Success (XML.Decode.int_atom i, body)
42.89 + handle XML.XML_ATOM err => Failure (err, [tree])
42.90 + else
42.91 + Failure ("tag mismatch: expected " ^ tag ^ ", got " ^ tag', [tree])
42.92 + | _ =>
42.93 + Failure ("indexed tag " ^ tag ^ " expected", [tree])
42.94 +
42.95 +
42.96 +abstype 'a codec = Codec of {encode: 'a -> XML.tree, decode: XML.tree -> 'a result} with
42.97 +
42.98 +val basic = Codec
42.99 +
42.100 +fun encode (Codec {encode, ...}) = encode
42.101 +fun decode (Codec {decode, ...}) = decode
42.102 +
42.103 +fun transform f g (Codec {encode, decode}) = Codec
42.104 + {encode = g #> encode,
42.105 + decode = decode #> map_result f}
42.106 +
42.107 +fun list a = Codec
42.108 + {encode = map (encode a) #> add_tag "list" NONE,
42.109 + decode = expect_tag "list" #> bind_result (traverse_results (decode a))}
42.110 +
42.111 +fun tuple a b = Codec
42.112 + {encode = (fn (x, y) => add_tag "tuple" NONE [encode a x, encode b y]),
42.113 + decode = expect_tag "tuple" #> bind_result (fn body =>
42.114 + case body of
42.115 + [x, y] => decode a x |> bind_result (fn x' => decode b y |> map_result (pair x'))
42.116 + | _ => Failure ("invalid structure", body))}
42.117 +
42.118 +fun variant enc dec tag = Codec
42.119 + {encode = (fn a => let val (idx, tree) = enc a in add_tag tag (SOME idx) [tree] end),
42.120 + decode = (fn tree => expect_tag' tag tree |> bind_result (fn (idx, body) =>
42.121 + case (body, dec idx) of
42.122 + ([tree'], SOME res) => res tree'
42.123 + | (_, SOME _) => Failure ("invalid structure", [tree])
42.124 + | (_, NONE) => Failure ("invalid index " ^ Markup.print_int idx, [tree])))}
42.125 +
42.126 +fun tagged tag a = Codec
42.127 + {encode = encode a #> single #> add_tag tag NONE,
42.128 + decode = expect_tag tag #> bind_result (fn body =>
42.129 + case body of
42.130 + [tree] => decode a tree
42.131 + | _ => Failure ("invalid structure", body))}
42.132 +
42.133 +val unit = Codec
42.134 + {encode = K (add_tag "unit" NONE []),
42.135 + decode = expect_tag "unit" #> bind_result (fn body =>
42.136 + case body of
42.137 + [] => Success ()
42.138 + | _ => Failure ("expected nothing", body))}
42.139 +
42.140 +fun text to from = Codec
42.141 + {encode = XML.Text o to,
42.142 + decode =
42.143 + (fn tree as XML.Text content =>
42.144 + (case from content of
42.145 + NONE => Failure ("decoding failed", [tree]) |
42.146 + SOME a => Success a)
42.147 + | tree => Failure ("expected text tree", [tree]))}
42.148 +
42.149 +val id = Codec {encode = I, decode = Success}
42.150 +
42.151 +end
42.152 +
42.153 +val int = tagged "int" (text Markup.print_int (Exn.get_res o Exn.capture Markup.parse_int))
42.154 +val bool = tagged "bool" (text Markup.print_bool (Exn.get_res o Exn.capture Markup.parse_bool))
42.155 +val string = tagged "string" (text I SOME)
42.156 +
42.157 +val tree = tagged "XML.tree" id
42.158 +
42.159 +fun option a =
42.160 + let
42.161 + fun enc (SOME x) = (0, encode a x)
42.162 + | enc NONE = (1, encode unit ())
42.163 + fun dec 0 = SOME (decode a #> map_result SOME)
42.164 + | dec 1 = SOME (decode unit #> map_result (K NONE))
42.165 + | dec _ = NONE
42.166 + in variant enc dec "option" end
42.167 +
42.168 +val content_of =
42.169 + XML.content_of o YXML.parse_body
42.170 +
42.171 +(* slightly fishy codec, doesn't preserve exception type *)
42.172 +exception GENERIC of string
42.173 +val exn = tagged "exn" (text (fn exn => (content_of (@{make_string} exn))) (SOME o GENERIC))
42.174 +
42.175 +fun exn_result a =
42.176 + let
42.177 + fun enc (Exn.Res t) = (0, encode a t)
42.178 + | enc (Exn.Exn e) = (1, encode exn e)
42.179 + fun dec 0 = SOME (decode a #> map_result Exn.Res)
42.180 + | dec 1 = SOME (decode exn #> map_result Exn.Exn)
42.181 + | dec _ = NONE
42.182 + in variant enc dec "Exn.result" end
42.183 +
42.184 +fun triple a b c =
42.185 + tuple a (tuple b c)
42.186 + |> transform (fn (a, (b, c)) => (a, b, c)) (fn (a, b, c) => (a, (b, c)))
42.187 +
42.188 +fun either a b =
42.189 + let
42.190 + fun enc (Left l) = (0, encode a l)
42.191 + | enc (Right r) = (1, encode b r)
42.192 + fun dec 0 = SOME (decode a #> map_result Left)
42.193 + | dec 1 = SOME (decode b #> map_result Right)
42.194 + | dec _ = NONE
42.195 + in variant enc dec "either" end
42.196 +
42.197 +val sort: sort codec = list string
42.198 +val indexname: indexname codec = tuple string int
42.199 +
42.200 +fun typ () =
42.201 + let
42.202 + fun typ_type () = tuple string (list (typ ()))
42.203 + val typ_tfree = tuple string sort
42.204 + val typ_tvar = tuple indexname sort
42.205 +
42.206 + fun enc (Type arg) = (0, encode (typ_type ()) arg)
42.207 + | enc (TFree arg) = (1, encode typ_tfree arg)
42.208 + | enc (TVar arg) = (2, encode typ_tvar arg)
42.209 + fun dec 0 = SOME (decode (typ_type ()) #> map_result Type)
42.210 + | dec 1 = SOME (decode typ_tfree #> map_result TFree)
42.211 + | dec 2 = SOME (decode typ_tvar #> map_result TVar)
42.212 + | dec _ = NONE
42.213 + in variant enc dec "Pure.typ" end
42.214 +
42.215 +val typ = typ ()
42.216 +
42.217 +fun term () =
42.218 + let
42.219 + val term_const = tuple string typ
42.220 + val term_free = tuple string typ
42.221 + val term_var = tuple indexname typ
42.222 + val term_bound = int
42.223 + fun term_abs () = triple string typ (term ())
42.224 + fun term_app () = tuple (term ()) (term ())
42.225 +
42.226 + fun enc (Const arg) = (0, encode term_const arg)
42.227 + | enc (Free arg) = (1, encode term_free arg)
42.228 + | enc (Var arg) = (2, encode term_var arg)
42.229 + | enc (Bound arg) = (3, encode term_bound arg)
42.230 + | enc (Abs arg) = (4, encode (term_abs ()) arg)
42.231 + | enc (op $ arg) = (5, encode (term_app ()) arg)
42.232 + fun dec 0 = SOME (decode term_const #> map_result Const)
42.233 + | dec 1 = SOME (decode term_free #> map_result Free)
42.234 + | dec 2 = SOME (decode term_var #> map_result Var)
42.235 + | dec 3 = SOME (decode term_bound #> map_result Bound)
42.236 + | dec 4 = SOME (decode (term_abs ()) #> map_result Abs)
42.237 + | dec 5 = SOME (decode (term_app ()) #> map_result op $)
42.238 + | dec _ = NONE
42.239 + in variant enc dec "Pure.term" end
42.240 +
42.241 +val term = term ()
42.242 +
42.243 +end
42.244 +
42.245 +type 'a codec = 'a Codec.codec
43.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
43.2 +++ b/libisabelle-protocol/protocol/protocol.ML Wed Apr 06 16:56:47 2016 +0200
43.3 @@ -0,0 +1,119 @@
43.4 +signature PROTOCOL = sig
43.5 + type name = string
43.6 + type ('i, 'o) operation =
43.7 + {from_lib : 'i codec,
43.8 + to_lib : 'o codec,
43.9 + action : 'i -> 'o}
43.10 +
43.11 + type flags = {sequential: bool, bracket: bool, auto: bool (* ignored *)}
43.12 +
43.13 + val default_flags : flags
43.14 + val join_flags : flags -> flags -> flags
43.15 + val print_flags : flags -> string
43.16 +
43.17 + val add_operation : name -> ('i, 'o) operation -> flags -> unit
43.18 + val get_operation : name -> int -> XML.tree -> XML.tree
43.19 +end
43.20 +
43.21 +structure Protocol: PROTOCOL = struct
43.22 +
43.23 +type name = string
43.24 +type ('i, 'o) operation =
43.25 + {from_lib : 'i codec,
43.26 + to_lib : 'o codec,
43.27 + action : 'i -> 'o}
43.28 +
43.29 +type flags = {sequential: bool, bracket: bool, auto: bool}
43.30 +
43.31 +val default_flags = {sequential = false, bracket = false, auto = false}
43.32 +
43.33 +fun join_flags
43.34 + {sequential = seq1, bracket = br1, auto = a1}
43.35 + {sequential = seq2, bracket = br2, auto = a2} =
43.36 + {sequential = seq1 orelse seq2, bracket = br1 orelse br2, auto = a1 orelse a2}
43.37 +
43.38 +fun print_flags {sequential, bracket, auto} =
43.39 + "({sequential=" ^ Markup.print_bool sequential ^ "," ^
43.40 + "bracket=" ^ Markup.print_bool bracket ^ "," ^
43.41 + "auto=" ^ Markup.print_bool auto ^ "})"
43.42 +
43.43 +type raw_operation = int -> XML.tree -> XML.tree
43.44 +
43.45 +exception GENERIC of string
43.46 +
43.47 +val operations =
43.48 + Synchronized.var "libisabelle.operations" (Symtab.empty: raw_operation Symtab.table)
43.49 +
43.50 +val requests =
43.51 + Synchronized.var "libisabelle.requests" (Inttab.empty: (unit -> unit) Inttab.table)
43.52 +
43.53 +fun sequentialize name f =
43.54 + let
43.55 + val var = Synchronized.var ("libisabelle." ^ name) ()
43.56 + in
43.57 + fn x => Synchronized.change_result var (fn _ => (f x, ()))
43.58 + end
43.59 +
43.60 +fun bracketize f id x =
43.61 + let
43.62 + val start = [(Markup.functionN, "libisabelle_start"), ("id", Markup.print_int id)]
43.63 + val stop = [(Markup.functionN, "libisabelle_stop"), ("id", Markup.print_int id)]
43.64 + val _ = Output.protocol_message start []
43.65 + val res = f id x
43.66 + val _ = Output.protocol_message stop []
43.67 + in res end
43.68 +
43.69 +fun add_operation name {from_lib, to_lib, action} {sequential, bracket, ...} =
43.70 + let
43.71 + fun raw _ tree =
43.72 + case Codec.decode from_lib tree of
43.73 + Codec.Success i => Codec.encode to_lib (action i)
43.74 + | Codec.Failure (msg, _) => raise Fail ("decoding input failed for operation " ^ name ^ ": " ^ msg)
43.75 + val raw' = raw
43.76 + |> (if bracket then bracketize else I)
43.77 + |> (if sequential then sequentialize name else I)
43.78 + in
43.79 + Synchronized.change operations (Symtab.update (name, raw'))
43.80 + end
43.81 +
43.82 +fun get_operation name =
43.83 + case Symtab.lookup (Synchronized.value operations) name of
43.84 + SOME operation => operation
43.85 + | NONE => fn _ => raise Fail "libisabelle: unknown command"
43.86 +
43.87 +val _ = Isabelle_Process.protocol_command "libisabelle"
43.88 + (fn id :: name :: [arg] =>
43.89 + let
43.90 + val id = Markup.parse_int id
43.91 + val response = [(Markup.functionN, "libisabelle_response"), ("id", Markup.print_int id)]
43.92 + val args = YXML.parse arg
43.93 + fun exec f =
43.94 + let
43.95 + val future = Future.fork (fn () =>
43.96 + let
43.97 + val res = Exn.interruptible_capture (f id) args
43.98 + val yxml = YXML.string_of (Codec.encode (Codec.exn_result Codec.id) res)
43.99 + in
43.100 + Output.protocol_message response [yxml]
43.101 + end)
43.102 + in
43.103 + Synchronized.change requests (Inttab.update_new (id, fn () => Future.cancel future))
43.104 + end
43.105 + in
43.106 + exec (get_operation name)
43.107 + end)
43.108 +
43.109 +val _ = Isabelle_Process.protocol_command "libisabelle_cancel"
43.110 + (fn ids =>
43.111 + let
43.112 + fun remove id tab = (Inttab.lookup tab id, Inttab.delete_safe id tab)
43.113 + val _ =
43.114 + map Markup.parse_int ids
43.115 + |> fold_map remove
43.116 + |> Synchronized.change_result requests
43.117 + |> map (fn NONE => () | SOME f => f ())
43.118 + in
43.119 + ()
43.120 + end)
43.121 +
43.122 +end
43.123 \ No newline at end of file
44.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
44.2 +++ b/src/Tools/isac/Isac_Protocol.thy Wed Apr 06 16:56:47 2016 +0200
44.3 @@ -0,0 +1,708 @@
44.4 +theory Isac_Protocol
44.5 +imports "~~/libisabelle-protocol/protocol/Protocol" "~~/src/Tools/isac/Knowledge/Build_Thydata"
44.6 +begin
44.7 +
44.8 +(* val appendFormula : calcID -> cterm' -> XML.tree *)
44.9 +operation_setup (sequential, bracket, auto) append_form =
44.10 + \<open>fn intree =>
44.11 + (let
44.12 + val (calcid, cterm') = case intree of
44.13 + XML.Elem (("APPENDFORMULA", []), [
44.14 + XML.Elem (("CALCID", []), [XML.Text ci]),
44.15 + form]) => (ci |> int_of_str', form |> xml_to_formula |> term2str)
44.16 + | x => raise ERROR ("append_form: WRONG intree = " ^ xmlstr 0 x)
44.17 + val result = Math_Engine.appendFormula calcid cterm'
44.18 + in result end)
44.19 + handle ERROR msg => appendformulaERROR2xml 4711 msg\<close>
44.20 +
44.21 +(* val autoCalculate : calcID -> auto -> XML.tree *)
44.22 +operation_setup autocalculate = \<open>
44.23 + {from_lib = Codec.tree,
44.24 + to_lib = Codec.tree,
44.25 + action = (fn intree =>
44.26 + (let
44.27 + val (ci, a) = case intree of
44.28 + XML.Elem (("AUTOCALC", []), [
44.29 + XML.Elem (("CALCID", []), [XML.Text ci]), a]) => (ci, a)
44.30 + | tree => raise ERROR ("autocalculate: WRONG intree = " ^ xmlstr 0 tree)
44.31 + val SOME calcid = int_of_str ci
44.32 + val auto = xml_to_auto a
44.33 + val result = Math_Engine.autoCalculate calcid auto
44.34 + in result end)
44.35 + handle ERROR msg => autocalculateERROR2xml 4711 msg)}\<close>
44.36 +
44.37 +(* val applyTactic : calcID -> pos' -> tac -> XML.tree *)
44.38 +operation_setup apply_tac = \<open>
44.39 + {from_lib = Codec.tree,
44.40 + to_lib = Codec.tree,
44.41 + action = (fn intree =>
44.42 + (let
44.43 + val (ci, pos, tac) = case intree of
44.44 + XML.Elem (("AUTOCALC", []), [
44.45 + XML.Elem (("CALCID", []), [XML.Text ci]),
44.46 + pos, tac]) => (str2int ci, xml_to_pos pos, xml_to_tac tac)
44.47 + | tree => raise ERROR ("apply_tac: WRONG intree = " ^ xmlstr 0 tree)
44.48 + val result = Math_Engine.applyTactic ci pos tac
44.49 + in result end)
44.50 + handle ERROR msg => autocalculateERROR2xml 4711 msg)}\<close>
44.51 +
44.52 +(* val CalcTree : fmz list -> XML.tree *)
44.53 +operation_setup calctree = \<open>
44.54 + {from_lib = Codec.tree,
44.55 + to_lib = Codec.tree,
44.56 + action = (fn intree =>
44.57 + (let
44.58 + val fmz = case intree of
44.59 + tree as XML.Elem (("FORMALIZATION", []), vars) => xml_to_fmz tree
44.60 + | tree => raise ERROR ("calctree: WRONG intree = " ^ xmlstr 0 tree)
44.61 + val result = Math_Engine.CalcTree fmz
44.62 + in result end)
44.63 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.64 +
44.65 +(* val checkContext : calcID -> pos' -> guh -> XML.tree *)
44.66 +operation_setup check_ctxt = \<open>
44.67 + {from_lib = Codec.tree,
44.68 + to_lib = Codec.tree,
44.69 + action = (fn intree =>
44.70 + (let
44.71 + val (ci, pos, guh) = case intree of
44.72 + XML.Elem (("CONTEXTTHY", []), [
44.73 + XML.Elem (("CALCID", []), [XML.Text ci]),
44.74 + pos as XML.Elem (("POSITION", []), _),
44.75 + XML.Elem (("GUH", []), [XML.Text guh])])
44.76 + => (str2int ci, xml_to_pos pos, guh)
44.77 + | tree => raise ERROR ("check_ctxt: WRONG intree = " ^ xmlstr 0 tree)
44.78 + val result = Math_Engine.checkContext ci pos guh
44.79 + in result end)
44.80 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.81 +
44.82 +(* val DEconstrCalcTree : calcID -> XML.tree *)
44.83 +operation_setup deconstrcalctree = \<open>
44.84 + {from_lib = Codec.int,
44.85 + to_lib = Codec.tree,
44.86 + action = (fn calcid =>
44.87 + let
44.88 + val result = Math_Engine.DEconstrCalcTree calcid
44.89 + in result end)}\<close>
44.90 +
44.91 +(* val fetchApplicableTactics : calcID -> int -> pos' -> XML.tree *)
44.92 +operation_setup fetch_applicable_tacs = \<open>
44.93 + {from_lib = Codec.tree,
44.94 + to_lib = Codec.tree,
44.95 + action = (fn intree =>
44.96 + (let
44.97 + val (ci, i, pos) = case intree of
44.98 + XML.Elem (("APPLICABLETACTICS", []), [
44.99 + XML.Elem (("CALCID", []), [XML.Text ci]),
44.100 + XML.Elem (("INT", []), [XML.Text i]),
44.101 + pos as XML.Elem (("POSITION", []), _)])
44.102 + => (str2int ci, str2int i, xml_to_pos pos)
44.103 + | tree => raise ERROR ("fetch_applicable_tacs: WRONG intree = " ^ xmlstr 0 tree)
44.104 + val result = Math_Engine.fetchApplicableTactics ci i pos
44.105 + in result end)
44.106 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.107 +
44.108 +(* val fetchProposedTactic : calcID -> XML.tree *)
44.109 +operation_setup fetch_proposed_tac = \<open>
44.110 + {from_lib = Codec.tree,
44.111 + to_lib = Codec.tree,
44.112 + action = (fn intree =>
44.113 + (let
44.114 + val (ci) = case intree of
44.115 + XML.Elem (("NEXTTAC", []), [
44.116 + XML.Elem (("CALCID", []), [XML.Text ci])]) => (str2int ci)
44.117 + | tree => raise ERROR ("fetch_proposed_tac: WRONG intree = " ^ xmlstr 0 tree)
44.118 + val result = Math_Engine.fetchProposedTactic ci
44.119 + in result end)
44.120 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.121 +
44.122 +(* val findFillpatterns : calcID -> errpatID -> XML.tree *)
44.123 +operation_setup find_fill_patts = \<open>
44.124 + {from_lib = Codec.tree,
44.125 + to_lib = Codec.tree,
44.126 + action = (fn intree =>
44.127 + (let
44.128 + val (ci, err_pat_id) = case intree of
44.129 + XML.Elem (("FINDFILLPATTERNS", []), [
44.130 + XML.Elem (("CALCID", []), [XML.Text ci]),
44.131 + XML.Elem (("STRING", []), [XML.Text err_pat_id])])
44.132 + => (str2int ci, err_pat_id)
44.133 + | tree => raise ERROR ("find_fill_patts: WRONG intree = " ^ xmlstr 0 tree)
44.134 + val result = Math_Engine.findFillpatterns ci err_pat_id
44.135 + in result end)
44.136 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.137 +
44.138 +(* val getAccumulatedAsms : calcID -> pos' -> XML.tree *)
44.139 +operation_setup get_accumulated_asms = \<open>
44.140 + {from_lib = Codec.tree,
44.141 + to_lib = Codec.tree,
44.142 + action = (fn intree =>
44.143 + (let
44.144 + val (ci, pos) = case intree of
44.145 + XML.Elem (("GETASSUMPTIONS", []), [
44.146 + XML.Elem (("CALCID", []), [XML.Text ci]),
44.147 + pos as XML.Elem (("POSITION", []), _)])
44.148 + => (str2int ci, xml_to_pos pos)
44.149 + | tree => raise ERROR ("autocalculate: WRONG intree = " ^ xmlstr 0 tree)
44.150 + val result = Math_Engine.getAccumulatedAsms ci pos
44.151 + in result end)
44.152 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.153 +
44.154 +(* val getActiveFormula : calcID -> XML.tree *)
44.155 +operation_setup get_active_form = \<open>
44.156 + {from_lib = Codec.tree,
44.157 + to_lib = Codec.tree,
44.158 + action = (fn intree =>
44.159 + (let
44.160 + val (ci) = case intree of
44.161 + XML.Elem (("CALCITERATOR", []), [
44.162 + XML.Elem (("CALCID", []), [XML.Text ci])])
44.163 + => (str2int ci)
44.164 + | tree => raise ERROR ("get_active_form: WRONG intree = " ^ xmlstr 0 tree)
44.165 + val result = Math_Engine.getActiveFormula ci
44.166 + in result end)
44.167 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.168 +
44.169 +(* val getAssumptions : calcID -> pos' -> XML.tree *)
44.170 +operation_setup get_asms = \<open>
44.171 + {from_lib = Codec.tree,
44.172 + to_lib = Codec.tree,
44.173 + action = (fn intree =>
44.174 + (let
44.175 + val (ci, pos) = case intree of
44.176 + XML.Elem (("APPLICABLETACTICS", []), [
44.177 + XML.Elem (("CALCID", []), [XML.Text ci]),
44.178 + pos as XML.Elem (("POSITION", []), _)])
44.179 + => (str2int ci, xml_to_pos pos)
44.180 + | tree => raise ERROR ("get_asms: WRONG intree = " ^ xmlstr 0 tree)
44.181 + val result = Math_Engine.getAssumptions ci pos
44.182 + in result end)
44.183 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.184 +
44.185 +(* val getFormulaeFromTo : calcID -> pos' -> pos' -> int -> bool -> XML.tree *)
44.186 +operation_setup getformulaefromto = \<open>
44.187 + {from_lib = Codec.tree,
44.188 + to_lib = Codec.tree,
44.189 + action = (fn intree =>
44.190 + (let
44.191 + val (calcid, from, to, level, rules) = case intree of
44.192 + XML.Elem (("GETFORMULAEFROMTO", []), [
44.193 + XML.Elem (("CALCID", []), [XML.Text calcid]),
44.194 + from as XML.Elem (("POSITION", []), [
44.195 + XML.Elem (("INTLIST", []), _),
44.196 + XML.Elem (("POS", []), [XML.Text _])]),
44.197 + to as XML.Elem (("POSITION", []), [
44.198 + XML.Elem (("INTLIST", []), _),
44.199 + XML.Elem (("POS", []), [XML.Text _])]),
44.200 + XML.Elem (("INT", []), [XML.Text level]),
44.201 + XML.Elem (("BOOL", []), [XML.Text rules])])
44.202 + => (str2int calcid, xml_to_pos from, xml_to_pos to, str2int level, string_to_bool rules)
44.203 + | tree => raise ERROR ("getformulaefromto: WRONG intree = " ^ xmlstr 0 tree)
44.204 + val result = Math_Engine.getFormulaeFromTo calcid from to level rules
44.205 + in result end)
44.206 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.207 +
44.208 +(* val getTactic : calcID -> pos' -> XML.tree *)
44.209 +operation_setup get_tac = \<open>
44.210 + {from_lib = Codec.tree,
44.211 + to_lib = Codec.tree,
44.212 + action = (fn intree =>
44.213 + (let
44.214 + val (ci, pos) = case intree of
44.215 + XML.Elem (("GETTACTIC", []), [
44.216 + XML.Elem (("CALCID", []), [XML.Text ci]),
44.217 + pos as XML.Elem (("POSITION", []), _)])
44.218 + => (str2int ci, xml_to_pos pos)
44.219 + | tree => raise ERROR ("get_tac: WRONG intree = " ^ xmlstr 0 tree)
44.220 + val result = Math_Engine.getTactic ci pos
44.221 + in result end)
44.222 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.223 +
44.224 +(* val initContext : calcID -> ketype -> pos' -> XML.tree *)
44.225 +operation_setup init_ctxt = \<open>
44.226 + {from_lib = Codec.tree,
44.227 + to_lib = Codec.tree,
44.228 + action = (fn intree =>
44.229 + ((let
44.230 + val (ci, ketype, pos) = case intree of
44.231 + XML.Elem (("INITCONTEXT", []), [
44.232 + XML.Elem (("CALCID", []), [XML.Text ci]),
44.233 + ketype as XML.Elem (("KETYPE", []), _),
44.234 + pos as XML.Elem (("POSITION", []), _)])
44.235 + => (str2int ci, xml_to_ketype ketype, xml_to_pos pos)
44.236 + | tree => raise ERROR ("init_ctxt: WRONG intree = " ^ xmlstr 0 tree)
44.237 + val result = Math_Engine.initContext ci ketype pos
44.238 + in result end)
44.239 + handle ERROR msg => sysERROR2xml 4711 msg)
44.240 + handle _ => sysERROR2xml 4711 "Protocol.operation_setup init_ctxt UNKNOWN exn")}\<close>
44.241 +
44.242 +(* val inputFillFormula: calcID -> string -> XML.tree *)
44.243 +operation_setup input_fill_form = \<open>
44.244 + {from_lib = Codec.tree,
44.245 + to_lib = Codec.tree,
44.246 + action = (fn intree =>
44.247 + (let
44.248 + val (ci, str) = case intree of
44.249 + XML.Elem (("AUTOCALC", []), [
44.250 + XML.Elem (("CALCID", []), [XML.Text ci]),
44.251 + XML.Elem (("STRING", []), [XML.Text str])])
44.252 + => (str2int ci, str)
44.253 + | tree => raise ERROR ("input_fill_form: WRONG intree = " ^ xmlstr 0 tree)
44.254 + val result = Math_Engine.inputFillFormula ci str
44.255 + in result end)
44.256 + handle ERROR msg => message2xml 4711 msg)}\<close>
44.257 +
44.258 +(* val interSteps : calcID -> pos' -> XML.tree *)
44.259 +operation_setup inter_steps = \<open>
44.260 + {from_lib = Codec.tree,
44.261 + to_lib = Codec.tree,
44.262 + action = (fn intree =>
44.263 + (let
44.264 + val (ci, pos) = case intree of
44.265 + XML.Elem (("INTERSTEPS", []), [
44.266 + XML.Elem (("CALCID", []), [XML.Text ci]),
44.267 + pos as XML.Elem (("POSITION", []), _)])
44.268 + => (str2int ci, xml_to_pos pos)
44.269 + | tree => raise ERROR ("inter_steps: WRONG intree = " ^ xmlstr 0 tree)
44.270 + val result = Math_Engine.interSteps ci pos
44.271 + in result end)
44.272 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.273 +
44.274 +(* val Iterator : calcID -> XML.tree *)
44.275 +operation_setup iterator = \<open>
44.276 + {from_lib = Codec.int,
44.277 + to_lib = Codec.tree,
44.278 + action = (fn calcid =>
44.279 + let
44.280 + val result = Math_Engine.Iterator calcid
44.281 + in result end)}\<close>
44.282 +
44.283 +(* val IteratorTEST : calcID -> iterID *)
44.284 +
44.285 +(* val modelProblem : calcID -> XML.tree *)
44.286 +operation_setup model_pbl = \<open>
44.287 + {from_lib = Codec.tree,
44.288 + to_lib = Codec.tree,
44.289 + action = (fn intree =>
44.290 + (let
44.291 + val (ci) = case intree of
44.292 + XML.Elem (("MODIFYCALCHEAD", []), [
44.293 + XML.Elem (("CALCID", []), [XML.Text ci])])
44.294 + => (str2int ci)
44.295 + | tree => raise ERROR ("model_pbl: WRONG intree = " ^ xmlstr 0 tree)
44.296 + val result = Math_Engine.modelProblem ci
44.297 + in result end)
44.298 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.299 +
44.300 +(* val modifyCalcHead : calcID -> icalhd -> XML.tree *)
44.301 +operation_setup modify_calchead = \<open>
44.302 + {from_lib = Codec.tree,
44.303 + to_lib = Codec.tree,
44.304 + action = (fn intree =>
44.305 + (let
44.306 + val (ci, icalhd) = case intree of
44.307 + XML.Elem (("MODIFYCALCHEAD", []), [
44.308 + XML.Elem (("CALCID", []), [XML.Text ci]),
44.309 + icalhd])
44.310 + => (str2int ci, xml_to_icalhd icalhd)
44.311 + | tree => raise ERROR ("modify_calchead: WRONG intree = " ^ xmlstr 0 tree)
44.312 + val result = Math_Engine.modifyCalcHead ci icalhd
44.313 + in result end)
44.314 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.315 +
44.316 +(* val moveActiveCalcHead : calcID -> XML.tree *)
44.317 +operation_setup move_active_calchead = \<open>
44.318 + {from_lib = Codec.tree,
44.319 + to_lib = Codec.tree,
44.320 + action = (fn intree =>
44.321 + (let
44.322 + val (ci) = case intree of
44.323 + XML.Elem (("CALCITERATOR", []), [
44.324 + XML.Elem (("CALCID", []), [XML.Text ci])])
44.325 + => (str2int ci)
44.326 + | tree => raise ERROR ("move_active_calchead: WRONG intree = " ^ xmlstr 0 tree)
44.327 + val result = Math_Engine.moveActiveCalcHead ci
44.328 + in result end)
44.329 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.330 +
44.331 +(* val moveActiveDown : calcID -> XML.tree *)
44.332 +operation_setup move_active_down = \<open>
44.333 + {from_lib = Codec.tree,
44.334 + to_lib = Codec.tree,
44.335 + action = (fn intree =>
44.336 + (let
44.337 + val (ci) = case intree of
44.338 + XML.Elem (("CALCITERATOR", []), [
44.339 + XML.Elem (("CALCID", []), [XML.Text ci])])
44.340 + => (str2int ci)
44.341 + | tree => raise ERROR ("move_active_down: WRONG intree = " ^ xmlstr 0 tree)
44.342 + val result = Math_Engine.moveActiveDown ci
44.343 + in result end)
44.344 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.345 +
44.346 +(* val moveActiveFormula : calcID -> pos' -> XML.tree *)
44.347 +operation_setup move_active_form = \<open>
44.348 + {from_lib = Codec.tree,
44.349 + to_lib = Codec.tree,
44.350 + action = (fn intree =>
44.351 + (let
44.352 + val (ci, pos) = case intree of
44.353 + XML.Elem (("CALCITERATOR", []), [
44.354 + XML.Elem (("CALCID", []), [XML.Text ci]),
44.355 + pos as XML.Elem (("POSITION", []), _)])
44.356 + => (str2int ci, xml_to_pos pos)
44.357 + | tree => raise ERROR ("move_active_form: WRONG intree = " ^ xmlstr 0 tree)
44.358 + val result = Math_Engine.moveActiveFormula ci pos
44.359 + in result end)
44.360 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.361 +
44.362 +(* val moveActiveLevelDown : calcID -> XML.tree *)
44.363 +operation_setup move_active_levdown = \<open>
44.364 + {from_lib = Codec.tree,
44.365 + to_lib = Codec.tree,
44.366 + action = (fn intree =>
44.367 + (let
44.368 + val (ci) = case intree of
44.369 + XML.Elem (("CALCITERATOR", []), [
44.370 + XML.Elem (("CALCID", []), [XML.Text ci])])
44.371 + => (str2int ci)
44.372 + | tree => raise ERROR ("move_active_levdown: WRONG intree = " ^ xmlstr 0 tree)
44.373 + val result = Math_Engine.moveActiveLevelDown ci
44.374 + in result end)
44.375 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.376 +
44.377 +(* val moveActiveLevelUp : calcID -> XML.tree *)
44.378 +operation_setup move_active_levup = \<open>
44.379 + {from_lib = Codec.tree,
44.380 + to_lib = Codec.tree,
44.381 + action = (fn intree =>
44.382 + (let
44.383 + val (ci) = case intree of
44.384 + XML.Elem (("CALCITERATOR", []), [
44.385 + XML.Elem (("CALCID", []), [XML.Text ci])])
44.386 + => (str2int ci)
44.387 + | tree => raise ERROR ("move_active_levup: WRONG intree = " ^ xmlstr 0 tree)
44.388 + val result = Math_Engine.moveActiveLevelUp ci
44.389 + in result end)
44.390 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.391 +
44.392 +(* val moveActiveRoot : calcID -> XML.tree *)
44.393 +operation_setup moveactiveroot = \<open>
44.394 + {from_lib = Codec.int,
44.395 + to_lib = Codec.tree,
44.396 + action = (fn calcid =>
44.397 + let
44.398 + val result = Math_Engine.moveActiveRoot calcid
44.399 + in result end)}\<close>
44.400 +
44.401 +(* val moveActiveRootTEST : calcID -> XML.tree *)
44.402 +
44.403 +(* val moveActiveUp : calcID -> XML.tree *)
44.404 +operation_setup move_active_up = \<open>
44.405 + {from_lib = Codec.tree,
44.406 + to_lib = Codec.tree,
44.407 + action = (fn intree =>
44.408 + (let
44.409 + val (ci) = case intree of
44.410 + XML.Elem (("CALCITERATOR", []), [
44.411 + XML.Elem (("CALCID", []), [XML.Text ci])])
44.412 + => (str2int ci)
44.413 + | tree => raise ERROR ("move_active_up: WRONG intree = " ^ xmlstr 0 tree)
44.414 + val result = Math_Engine.moveActiveUp ci
44.415 + in result end)
44.416 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.417 +
44.418 +(* val moveCalcHead : calcID -> pos' -> XML.tree *)
44.419 +operation_setup move_calchead = \<open>
44.420 + {from_lib = Codec.tree,
44.421 + to_lib = Codec.tree,
44.422 + action = (fn intree =>
44.423 + (let
44.424 + val (ci, pos) = case intree of
44.425 + XML.Elem (("CALCITERATOR", []), [
44.426 + XML.Elem (("CALCID", []), [XML.Text ci]),
44.427 + pos as XML.Elem (("POSITION", []), _)])
44.428 + => (str2int ci, xml_to_pos pos)
44.429 + | tree => raise ERROR ("move_active_calchead: WRONG intree = " ^ xmlstr 0 tree)
44.430 + val result = Math_Engine.moveCalcHead ci pos
44.431 + in result end)
44.432 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.433 +
44.434 +(* val moveDown : calcID -> pos' -> XML.tree *)
44.435 +operation_setup move_down = \<open>
44.436 + {from_lib = Codec.tree,
44.437 + to_lib = Codec.tree,
44.438 + action = (fn intree =>
44.439 + (let
44.440 + val (ci, pos) = case intree of
44.441 + XML.Elem (("CALCITERATOR", []), [
44.442 + XML.Elem (("CALCID", []), [XML.Text ci]),
44.443 + pos as XML.Elem (("POSITION", []), _)])
44.444 + => (str2int ci, xml_to_pos pos)
44.445 + | tree => raise ERROR ("move_down: WRONG intree = " ^ xmlstr 0 tree)
44.446 + val result = Math_Engine.moveDown ci pos
44.447 + in result end)
44.448 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.449 +
44.450 +(* val moveLevelDown : calcID -> pos' -> XML.tree *)
44.451 +operation_setup move_levdn = \<open>
44.452 + {from_lib = Codec.tree,
44.453 + to_lib = Codec.tree,
44.454 + action = (fn intree =>
44.455 + (let
44.456 + val (ci, pos) = case intree of
44.457 + XML.Elem (("CALCITERATOR", []), [
44.458 + XML.Elem (("CALCID", []), [XML.Text ci]),
44.459 + pos as XML.Elem (("POSITION", []), _)])
44.460 + => (str2int ci, xml_to_pos pos)
44.461 + | tree => raise ERROR ("move_levdn: WRONG intree = " ^ xmlstr 0 tree)
44.462 + val result = Math_Engine.moveLevelDown ci pos
44.463 + in result end)
44.464 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.465 +
44.466 +(* val moveLevelUp : calcID -> pos' -> XML.tree *)
44.467 +operation_setup move_levup = \<open>
44.468 + {from_lib = Codec.tree,
44.469 + to_lib = Codec.tree,
44.470 + action = (fn intree =>
44.471 + (let
44.472 + val (ci, pos) = case intree of
44.473 + XML.Elem (("CALCITERATOR", []), [
44.474 + XML.Elem (("CALCID", []), [XML.Text ci]),
44.475 + pos as XML.Elem (("POSITION", []), _)])
44.476 + => (str2int ci, xml_to_pos pos)
44.477 + | tree => raise ERROR ("move_levup: WRONG intree = " ^ xmlstr 0 tree)
44.478 + val result = Math_Engine.moveLevelUp ci pos
44.479 + in result end)
44.480 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.481 +
44.482 +(* val moveRoot : calcID -> XML.tree *)
44.483 +operation_setup move_root = \<open>
44.484 + {from_lib = Codec.tree,
44.485 + to_lib = Codec.tree,
44.486 + action = (fn intree =>
44.487 + (let
44.488 + val (ci) = case intree of
44.489 + XML.Elem (("CALCITERATOR", []), [
44.490 + XML.Elem (("CALCID", []), [XML.Text ci])])
44.491 + => (str2int ci)
44.492 + | tree => raise ERROR ("move_root: WRONG intree = " ^ xmlstr 0 tree)
44.493 + val result = Math_Engine.moveRoot ci
44.494 + in result end)
44.495 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.496 +
44.497 +(* val moveUp : calcID -> pos' -> XML.tree *)
44.498 +operation_setup move_up = \<open>
44.499 + {from_lib = Codec.tree,
44.500 + to_lib = Codec.tree,
44.501 + action = (fn intree =>
44.502 + (let
44.503 + val (ci, pos) = case intree of
44.504 + XML.Elem (("CALCITERATOR", []), [
44.505 + XML.Elem (("CALCID", []), [XML.Text ci]),
44.506 + pos as XML.Elem (("POSITION", []), _)])
44.507 + => (str2int ci, xml_to_pos pos)
44.508 + | tree => raise ERROR ("move_up: WRONG intree = " ^ xmlstr 0 tree)
44.509 + val result = Math_Engine.moveUp ci pos
44.510 + in result end)
44.511 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.512 +
44.513 +(* val refFormula : calcID -> pos' -> XML.tree *)
44.514 +operation_setup refformula = \<open>
44.515 + {from_lib = Codec.tree,
44.516 + to_lib = Codec.tree,
44.517 + action = (fn intree =>
44.518 + (let
44.519 + val (ci, p) = case intree of
44.520 + XML.Elem (("REFFORMULA", []), [
44.521 + XML.Elem (("CALCID", []), [XML.Text ci]), p])
44.522 + => (ci, p)
44.523 + | tree => raise ERROR ("refformula: WRONG intree = " ^ xmlstr 0 tree)
44.524 + val SOME calcid = int_of_str ci
44.525 + val pos = xml_to_pos p
44.526 + val result = Math_Engine.refFormula calcid pos
44.527 + in result end)
44.528 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.529 +
44.530 +(* val refineProblem : calcID -> pos' -> guh -> XML.tree *)
44.531 +operation_setup refine_pbl = \<open>
44.532 + {from_lib = Codec.tree,
44.533 + to_lib = Codec.tree,
44.534 + action = (fn intree =>
44.535 + (let
44.536 + val (ci, pos, guh) = case intree of
44.537 + XML.Elem (("CONTEXTPBL", []), [
44.538 + XML.Elem (("CALCID", []), [XML.Text ci]),
44.539 + pos as XML.Elem (("POSITION", []), _),
44.540 + XML.Elem (("GUH", []), [XML.Text guh])])
44.541 + => (str2int ci, xml_to_pos pos, guh)
44.542 + | tree => raise ERROR ("refine_pbl: WRONG intree = " ^ xmlstr 0 tree)
44.543 + val result = Math_Engine.refineProblem ci pos guh
44.544 + in result end)
44.545 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.546 +
44.547 +(* val replaceFormula : calcID -> cterm' -> XML.tree *)
44.548 +operation_setup replace_form = \<open>
44.549 + {from_lib = Codec.tree,
44.550 + to_lib = Codec.tree,
44.551 + action = (fn intree =>
44.552 + (let
44.553 + val (calcid, cterm') = case intree of
44.554 + XML.Elem (("REPLACEFORMULA", []), [
44.555 + XML.Elem (("CALCID", []), [XML.Text ci]), form])
44.556 + => (ci |> int_of_str', form |> xml_to_formula |> term2str)
44.557 + | tree => raise ERROR ("replace_form: WRONG intree = " ^ xmlstr 0 tree)
44.558 + val result = Math_Engine.replaceFormula calcid cterm'
44.559 + in result end)
44.560 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.561 +
44.562 +(* val requestFillformula : calcID -> errpatID * fillpatID -> XML.tree NOT IMPL. IN isac-java *)
44.563 +operation_setup request_fill_form = \<open>
44.564 + {from_lib = Codec.tree,
44.565 + to_lib = Codec.tree,
44.566 + action = (fn intree =>
44.567 + (let
44.568 + val (ci, errpat_id, fillpat_id) = case intree of
44.569 + XML.Elem (("AUTOCALC", []), [
44.570 + XML.Elem (("CALCID", []), [XML.Text ci]),
44.571 + XML.Elem (("ERRPATTID", []), [XML.Text errpat_id]),
44.572 + XML.Elem (("FILLPATTID", []), [XML.Text fillpat_id])])
44.573 + => (str2int ci, errpat_id, fillpat_id)
44.574 + | tree => raise ERROR ("request_fill_form: WRONG intree = " ^ xmlstr 0 tree)
44.575 + val result = Math_Engine.requestFillformula ci (errpat_id, fillpat_id)
44.576 + in result end)
44.577 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.578 +
44.579 +(* val resetCalcHead : calcID -> XML.tree *)
44.580 +operation_setup reset_calchead = \<open>
44.581 + {from_lib = Codec.tree,
44.582 + to_lib = Codec.tree,
44.583 + action = (fn intree =>
44.584 + (let
44.585 + val (ci) = case intree of
44.586 + XML.Elem (("MODIFYCALCHEAD", []), [
44.587 + XML.Elem (("CALCID", []), [XML.Text ci])])
44.588 + => (str2int ci)
44.589 + | tree => raise ERROR ("reset_calchead: WRONG intree = " ^ xmlstr 0 tree)
44.590 + val result = Math_Engine.resetCalcHead ci
44.591 + in result end)
44.592 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.593 +
44.594 +(* val setContext : calcID -> pos' -> guh -> XML.tree *)
44.595 +operation_setup set_ctxt = \<open>
44.596 + {from_lib = Codec.tree,
44.597 + to_lib = Codec.tree,
44.598 + action = (fn intree =>
44.599 + (let
44.600 + val (ci, pos, guh) = case intree of
44.601 + XML.Elem (("CONTEXT", []), [
44.602 + XML.Elem (("CALCID", []), [XML.Text ci]),
44.603 + pos as XML.Elem (("POSITION", []), _),
44.604 + XML.Elem (("GUH", []), [XML.Text guh])])
44.605 + => (str2int ci, xml_to_pos pos, guh)
44.606 + | tree => raise ERROR ("set_ctxt: WRONG intree = " ^ xmlstr 0 tree)
44.607 + val result = Math_Engine.setContext ci pos guh
44.608 + in result end)
44.609 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.610 +
44.611 +(*//===vvv TODO ================================================================\\\\\\\\\\\\\\\\*)
44.612 +
44.613 +(* val setMethod : calcID -> metID -> XML.tree *)
44.614 +operation_setup set_met = \<open>
44.615 + {from_lib = Codec.tree,
44.616 + to_lib = Codec.tree,
44.617 + action = (fn intree =>
44.618 + (let
44.619 + val (ci, met_id) = case intree of
44.620 + XML.Elem (("MODIFYCALCHEAD", []), [
44.621 + XML.Elem (("CALCID", []), [XML.Text ci]),
44.622 + XML.Elem (("METHODID", []), [met_id])])
44.623 + => (str2int ci, xml_to_strs met_id)
44.624 + | tree => raise ERROR ("set_met: WRONG intree = " ^ xmlstr 0 tree)
44.625 + val result = Math_Engine.setMethod ci met_id
44.626 + in result end)
44.627 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.628 +
44.629 +(* val setNextTactic : calcID -> tac -> XML.tree *)
44.630 +operation_setup set_next_tac = \<open>
44.631 + {from_lib = Codec.tree,
44.632 + to_lib = Codec.tree,
44.633 + action = (fn intree =>
44.634 + (let
44.635 + val (ci, tac) = case intree of
44.636 + XML.Elem (("SETNEXTTACTIC", []), [
44.637 + XML.Elem (("CALCID", []), [XML.Text ci]),
44.638 + tac])
44.639 + => (str2int ci, xml_to_tac tac)
44.640 + | tree => raise ERROR ("set_next_tac: WRONG intree = " ^ xmlstr 0 tree)
44.641 + val result = Math_Engine.setNextTactic ci tac
44.642 + in result end)
44.643 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.644 +
44.645 +(*\\===^^^ TODO ================================================================///////////////*)
44.646 +
44.647 +(* val setProblem : calcID -> pblID -> XML.tree *)
44.648 +operation_setup set_pbl = \<open>
44.649 + {from_lib = Codec.tree,
44.650 + to_lib = Codec.tree,
44.651 + action = (fn intree =>
44.652 + (let
44.653 + val (ci, pbl_id) = case intree of
44.654 + XML.Elem (("MODIFYCALCHEAD", []), [
44.655 + XML.Elem (("CALCID", []), [XML.Text ci]),
44.656 + XML.Elem (("PROBLEMID", []), [pbl_id])])
44.657 + => (str2int ci, xml_to_strs pbl_id)
44.658 + | tree => raise ERROR ("set_pbl: WRONG intree = " ^ xmlstr 0 tree)
44.659 + val result = Math_Engine.setProblem ci pbl_id
44.660 + in result end)
44.661 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.662 +
44.663 +(* val setTheory : calcID -> thyID -> XML.tree *)
44.664 +operation_setup set_thy = \<open>
44.665 + {from_lib = Codec.tree,
44.666 + to_lib = Codec.tree,
44.667 + action = (fn intree =>
44.668 + (let
44.669 + val (ci, thy_id) = case intree of
44.670 + XML.Elem (("MODIFYCALCHEAD", []), [
44.671 + XML.Elem (("CALCID", []), [XML.Text ci]),
44.672 + XML.Elem (("THEORYID", []), [XML.Text thy_id])])
44.673 + => (str2int ci, thy_id)
44.674 + | tree => raise ERROR ("set_thy: WRONG intree = " ^ xmlstr 0 tree)
44.675 + val result = Math_Engine.setTheory ci thy_id
44.676 + in result end)
44.677 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.678 +
44.679 +
44.680 +operation_setup make_int = \<open>
44.681 + {from_lib = Codec.unit,
44.682 + to_lib = Codec.term,
44.683 + action = (fn _ => HOLogic.mk_number @{typ int} 3)}
44.684 +\<close>
44.685 +
44.686 +operation_setup test_term_transfer = \<open>
44.687 + {from_lib = Codec.tree,
44.688 + to_lib = Codec.tree,
44.689 + action = (fn intree =>
44.690 + (let
44.691 + val t = case intree of
44.692 + XML.Elem (("MATHML", []), [
44.693 + XML.Elem (("ISA", []), [XML.Text _]),
44.694 + XML.Elem (("TERM", []), [xt])])
44.695 + => xt |> Codec.decode Codec.term |> Codec.the_success
44.696 + | tree => raise ERROR ("test_term_transfer: WRONG intree = " ^ xmlstr 0 tree)
44.697 + val test_out = HOLogic.mk_eq (t, Const ("processed_by_Isabelle_Isac", type_of t))
44.698 + in xml_of_term_NEW test_out end)
44.699 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.700 +
44.701 +operation_setup test_term_one_way = \<open>
44.702 + {from_lib = Codec.string,
44.703 + to_lib = Codec.tree,
44.704 + action = (fn instr =>
44.705 + (let
44.706 + val t = instr |> parse @{theory} |> the |> Thm.term_of
44.707 + val test_out = HOLogic.mk_eq (t, Const ("processed_by_Isabelle_Isac", type_of t))
44.708 + in xml_of_term_NEW test_out end)
44.709 + handle ERROR msg => sysERROR2xml 4711 msg)}\<close>
44.710 +
44.711 +end
44.712 \ No newline at end of file
45.1 --- a/src/Tools/isac/ROOT Sat Feb 06 17:20:08 2016 +0100
45.2 +++ b/src/Tools/isac/ROOT Wed Apr 06 16:56:47 2016 +0200
45.3 @@ -35,4 +35,5 @@
45.4 For installation see http://www.ist.tugraz.at/isac
45.5 *}
45.6 options [document = false (*, browser_info = true*)]
45.7 - theories Build_Isac "~~/libisabelle-protocol/isabelle/2015/Protocol" "~~/libisabelle-protocol/operations/Basic"
45.8 + theories Isac_Protocol
45.9 + "~~/libisabelle-protocol/protocol/Protocol" "~~/libisabelle-protocol/operations/Basic"
46.1 --- a/src/Tools/isac/xmlsrc/xmlsrc.thy Sat Feb 06 17:20:08 2016 +0100
46.2 +++ b/src/Tools/isac/xmlsrc/xmlsrc.thy Wed Apr 06 16:56:47 2016 +0200
46.3 @@ -4,7 +4,7 @@
46.4 *)
46.5
46.6 theory xmlsrc
46.7 -imports "~~/libisabelle-protocol/isabelle/2015/Codec_Class" "~~/src/Tools/isac/Interpret/Interpret"
46.8 +imports "~~/libisabelle-protocol/protocol/Codec_Class" "~~/src/Tools/isac/Interpret/Interpret"
46.9
46.10 begin
46.11
46.12 @@ -21,4 +21,4 @@
46.13 *} ML {*
46.14 *}
46.15
46.16 -end
46.17 \ No newline at end of file
46.18 +end