1.1 --- a/ROOTS Wed Aug 29 11:27:22 2018 +0200
1.2 +++ b/ROOTS Tue Sep 04 14:50:30 2018 +0200
1.3 @@ -11,4 +11,5 @@
1.4 src/Doc
1.5 src/Tools
1.6 src/Tools/isac
1.7 +libisabelle-protocol
1.8 test/Tools/isac/ADDTESTS/session-get_theory/
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/libisabelle-protocol/ROOTS Tue Sep 04 14:50:30 2018 +0200
2.3 @@ -0,0 +1,2 @@
2.4 +libisabelle
2.5 +classy
2.6 \ No newline at end of file
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/libisabelle-protocol/classy/Classy.thy Tue Sep 04 14:50:30 2018 +0200
3.3 @@ -0,0 +1,35 @@
3.4 +theory Classy
3.5 +imports Pure
3.6 +keywords
3.7 + "ML.class" :: thy_decl % "ML" and
3.8 + "ML.instance" :: thy_decl % "ML" and
3.9 + "ML.print_classes" :: diag
3.10 +begin
3.11 +
3.12 +(* FIXME unfold in ML files *)
3.13 +ML\<open>
3.14 + val secure_use_text = ML_Compiler0.ML
3.15 + val context_set_thread_data = Context.setmp_generic_context
3.16 + fun ml_env_context return : ML_Compiler0.context =
3.17 + {name_space = #name_space ML_Env.context,
3.18 + print_depth = SOME 1000000,
3.19 + here = #here ML_Env.context,
3.20 + print = fn r => return := SOME r,
3.21 + error = #error ML_Env.context}
3.22 + val print_int = Value.print_int
3.23 +\<close>
3.24 +
3.25 +ML_file "ml_types.ML"
3.26 +ML_file "classy.ML"
3.27 +
3.28 +setup \<open>Classy.setup\<close>
3.29 +
3.30 +ML_file "pretty_class.ML"
3.31 +
3.32 +ML.class pretty = \<open>'a pretty_class\<close>
3.33 +
3.34 +ML.instance \<open>Pretty_Class.string\<close> :: pretty
3.35 +ML.instance \<open>Pretty_Class.pretty\<close> :: pretty
3.36 +ML.instance \<open>Pretty_Class.list\<close> :: pretty
3.37 +
3.38 +end
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/libisabelle-protocol/classy/Examples.thy Tue Sep 04 14:50:30 2018 +0200
4.3 @@ -0,0 +1,18 @@
4.4 +theory Examples
4.5 +imports Classy
4.6 +begin
4.7 +
4.8 +ML.print_classes
4.9 +
4.10 +ML\<open>format @{ML.resolve \<open>string list\<close> :: pretty} ["a", "b"] |> Pretty.writeln\<close> (* okay *)
4.11 +
4.12 +context begin
4.13 +
4.14 + (* conflicting instance *)
4.15 + ML.instance \<open>Pretty_Class.string\<close> :: pretty
4.16 +
4.17 + ML\<open>@{ML.resolve \<open>string\<close> :: pretty}\<close> (* error *)
4.18 +
4.19 +end
4.20 +
4.21 +end
4.22 \ No newline at end of file
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/libisabelle-protocol/classy/ROOT Tue Sep 04 14:50:30 2018 +0200
5.3 @@ -0,0 +1,11 @@
5.4 +session Classy = Pure +
5.5 + theories
5.6 + Classy
5.7 + Test
5.8 +
5.9 +session "HOL-Classy" = HOL +
5.10 + sessions
5.11 + Classy
5.12 + theories
5.13 + Classy.Classy
5.14 + Classy.Test
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/libisabelle-protocol/classy/Test.thy Tue Sep 04 14:50:30 2018 +0200
6.3 @@ -0,0 +1,50 @@
6.4 +theory Test
6.5 +imports Classy
6.6 +begin
6.7 +
6.8 +section \<open>Parsing and printing types\<close>
6.9 +
6.10 +ML\<open>
6.11 +fun check t =
6.12 + let
6.13 + val t' = ML_Types.read_ml_type t |> ML_Types.pretty |> Pretty.string_of |> YXML.content_of
6.14 + in
6.15 + if t <> t' then
6.16 + error t'
6.17 + else
6.18 + ()
6.19 + end
6.20 +\<close>
6.21 +
6.22 +ML\<open>check "'a"\<close>
6.23 +ML\<open>check "'a * 'b"\<close>
6.24 +ML\<open>check "'a * 'b * 'c"\<close>
6.25 +ML\<open>check "('a * 'b) * 'c"\<close>
6.26 +ML\<open>check "'a * ('b * 'c)"\<close>
6.27 +ML\<open>check "'a * 'b -> 'c"\<close>
6.28 +ML\<open>check "'a * 'b -> 'a * 'b"\<close>
6.29 +ML\<open>check "('a -> 'b) * ('a -> 'b)"\<close>
6.30 +ML\<open>check "('a, 'b) foo"\<close>
6.31 +ML\<open>check "'a foo"\<close>
6.32 +ML\<open>check "unit foo"\<close>
6.33 +ML\<open>check "unit * 'a"\<close>
6.34 +ML\<open>check "'a foo * 'b foo bar"\<close>
6.35 +ML\<open>check "('a, unit) foo"\<close>
6.36 +ML\<open>check "('a * 'b) foo"\<close>
6.37 +ML\<open>check "('a -> 'b) foo"\<close>
6.38 +ML\<open>check "('a -> 'b, 'c) foo"\<close>
6.39 +ML\<open>check "('a -> 'b, 'c * 'd) foo"\<close>
6.40 +ML\<open>check "'a foo bar baz"\<close>
6.41 +ML\<open>check "('a foo, 'b) bar Long.ident.baz"\<close>
6.42 +ML\<open>check "{a: int}"\<close>
6.43 +ML\<open>check "{a: int, b: float}"\<close>
6.44 +ML\<open>check "{a: int, b: 'a -> 'b}"\<close>
6.45 +
6.46 +section \<open>Instance resolution\<close>
6.47 +
6.48 +ML\<open>@{ML.resolve \<open>string\<close> :: pretty}\<close>
6.49 +ML\<open>@{ML.resolve \<open>string list\<close> :: pretty}\<close>
6.50 +ML\<open>@{ML.resolve \<open>string list list\<close> :: pretty}\<close>
6.51 +ML\<open>@{ML.resolve \<open>Pretty.T\<close> :: pretty}\<close>
6.52 +
6.53 +end
6.54 \ No newline at end of file
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/libisabelle-protocol/classy/classy.ML Tue Sep 04 14:50:30 2018 +0200
7.3 @@ -0,0 +1,173 @@
7.4 +signature CLASSY = sig
7.5 + val register_class: binding -> ML_Types.ml_type -> local_theory -> local_theory
7.6 + val register_class_cmd: binding -> string -> local_theory -> local_theory
7.7 +
7.8 + val register_instance_cmd: xstring * Position.T -> binding -> Input.source -> local_theory -> local_theory
7.9 +
7.10 + val check_class: Context.generic -> string * Position.T -> string
7.11 + val print_classes: Context.generic -> unit
7.12 +
7.13 + val resolve: string -> ML_Types.ml_type -> Context.generic -> string
7.14 +
7.15 + val setup: theory -> theory
7.16 +end
7.17 +
7.18 +structure Classy: CLASSY = struct
7.19 +
7.20 +type class_table = (ml_type * (ml_type * string) Name_Space.table) Name_Space.table
7.21 +
7.22 +exception DUP
7.23 +
7.24 +structure Classes = Generic_Data
7.25 +(
7.26 + type T = class_table
7.27 + val empty = Name_Space.empty_table "ML class"
7.28 + val merge = Name_Space.join_tables (fn _ => raise DUP) (* FIXME consistency check *)
7.29 + val extend = I
7.30 +)
7.31 +
7.32 +fun list_comb (term: string) (args: string list) =
7.33 + space_implode " " (enclose "(" ")" term :: map (enclose "(" ")") args)
7.34 +
7.35 +fun product [] = [[]]
7.36 + | product (xs :: xss) =
7.37 + maps (fn xs' => map (fn x => x :: xs') xs) (product xss)
7.38 +
7.39 +
7.40 +fun solve entries problem =
7.41 + let
7.42 + fun find (typ, term) =
7.43 + let
7.44 + val (args, candidate) = ML_Types.strip_fun typ
7.45 + in
7.46 + case ML_Types.match candidate problem [] of
7.47 + SOME env =>
7.48 + map (ML_Types.subst env) args
7.49 + |> map (solve entries)
7.50 + |> product
7.51 + |> map (list_comb term)
7.52 + | NONE => []
7.53 + end
7.54 + in
7.55 + maps find entries
7.56 + end
7.57 +
7.58 +fun resolve class typ context =
7.59 + let
7.60 + val classes = Classes.get context
7.61 + val (constructor, table) = Name_Space.get classes class
7.62 + val ML_Types.Con (name, [ML_Types.Var _]) = constructor
7.63 + val entries = map snd (Name_Space.extern_table true (Context.proof_of context) table)
7.64 + val problem = ML_Types.Con (name, [typ])
7.65 + val solutions = solve entries problem
7.66 + in
7.67 + case solutions of
7.68 + [] => error "no solutions"
7.69 + | [solution] => enclose "(" ")" solution
7.70 + | _ => error "too many solutions"
7.71 + end
7.72 +
7.73 +fun check_class context raw_binding =
7.74 + fst (Name_Space.check context (Classes.get context) raw_binding)
7.75 +
7.76 +val antiquote_setup =
7.77 + ML_Antiquotation.inline (Binding.qualify true "ML" @{binding class})
7.78 + (Scan.state -- Scan.lift (Parse.position Args.name) >>
7.79 + (fn (context, binding) => quote (check_class context binding))) #>
7.80 + ML_Antiquotation.inline (Binding.qualify true "ML" @{binding resolve})
7.81 + (Scan.state -- Scan.lift (Parse.ML_source --| @{keyword "::"} -- Parse.position Args.name) >>
7.82 + (fn (context, (source, binding)) =>
7.83 + resolve (check_class context binding) (ML_Types.read_ml_type (Input.source_content source)) context))
7.84 +
7.85 +fun pretty_classes context =
7.86 + let
7.87 + val table = Classes.get context
7.88 + val ctxt = Context.proof_of context
7.89 + val space = Name_Space.space_of_table table
7.90 + val entries = Name_Space.extern_table true ctxt table
7.91 +
7.92 + fun pretty_class ((class, _), (typ, sub_table)) =
7.93 + let
7.94 + val header = Pretty.block [Name_Space.pretty ctxt space class, Pretty.str ":", Pretty.brk 1, ML_Types.pretty typ]
7.95 +
7.96 + val sub_space = Name_Space.space_of_table sub_table
7.97 + val sub_entries = Name_Space.extern_table true ctxt sub_table
7.98 +
7.99 + fun pretty_instance ((instance, _), (typ, _)) =
7.100 + Pretty.item [Name_Space.pretty ctxt sub_space instance, Pretty.str ":", Pretty.brk 1, ML_Types.pretty typ]
7.101 +
7.102 + val instances = map pretty_instance sub_entries
7.103 + in
7.104 + Pretty.item (Pretty.fbreaks (header :: instances))
7.105 + end
7.106 + in
7.107 + Pretty.big_list "Classes" (map pretty_class entries)
7.108 + end
7.109 +
7.110 +val print_classes =
7.111 + Pretty.writeln o pretty_classes
7.112 +
7.113 +fun register_class binding typ =
7.114 + let
7.115 + val name =
7.116 + (case typ of
7.117 + ML_Types.Con (name, [ML_Types.Var _]) => name
7.118 + | _ => error "Malformed type")
7.119 + fun decl _ context =
7.120 + let
7.121 + val classes = Classes.get context
7.122 + val table = Name_Space.empty_table ("ML instances for " ^ name)
7.123 + val (_, classes') = Name_Space.define context true (binding, (typ, table)) classes
7.124 + in
7.125 + Classes.put classes' context
7.126 + end
7.127 + in
7.128 + Local_Theory.declaration {syntax = false, pervasive = false} decl
7.129 + end
7.130 +
7.131 +fun register_class_cmd binding typ =
7.132 + register_class binding (ML_Types.read_ml_type typ)
7.133 +
7.134 +fun register_instance_cmd raw_binding binding source lthy =
7.135 + let
7.136 + val typ = ML_Types.ml_type_of lthy (Input.source_content source)
7.137 + (* doesn't have any effect except for markup *)
7.138 + val _ = ML_Context.eval_source_in (SOME lthy) ML_Compiler.flags source
7.139 +
7.140 + (* FIXME check correct type *)
7.141 +
7.142 + fun decl _ context =
7.143 + let
7.144 + val classes = Classes.get context
7.145 + val (key, _) = Name_Space.check context classes raw_binding
7.146 + val upd = Name_Space.define context true (binding, (typ, Input.source_content source)) #> snd
7.147 + val classes' = Name_Space.map_table_entry key (apsnd upd) classes
7.148 + in Classes.put classes' context end
7.149 + in
7.150 + Local_Theory.declaration {syntax = false, pervasive = false} decl lthy
7.151 + end
7.152 +
7.153 +val _ =
7.154 + Outer_Syntax.local_theory @{command_keyword "ML.class"} "register new type class"
7.155 + (Parse.binding --| @{keyword "="} -- Parse.cartouche
7.156 + >> (fn (binding, typ) => register_class_cmd binding typ))
7.157 +
7.158 +val _ =
7.159 + let
7.160 + val opt_binding =
7.161 + Parse.binding --| @{keyword "="} ||
7.162 + Parse.position (Scan.succeed ()) >>
7.163 + (fn ((), pos) => Binding.make ("instance" ^ print_int (serial ()), pos))
7.164 + in
7.165 + Outer_Syntax.local_theory @{command_keyword "ML.instance"} "register new type class instance"
7.166 + (opt_binding -- (Parse.ML_source --| @{keyword "::"} -- Parse.position Args.name)
7.167 + >> (fn (binding, (source, name)) => register_instance_cmd name binding source))
7.168 + end
7.169 +
7.170 +val _ =
7.171 + Outer_Syntax.command @{command_keyword "ML.print_classes"} "print all registered classes"
7.172 + (Scan.succeed (Toplevel.keep (print_classes o Toplevel.generic_theory_of)))
7.173 +
7.174 +val setup = antiquote_setup
7.175 +
7.176 +end
7.177 \ No newline at end of file
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/libisabelle-protocol/classy/ml_types.ML Tue Sep 04 14:50:30 2018 +0200
8.3 @@ -0,0 +1,215 @@
8.4 +signature ML_TYPES = sig
8.5 + datatype ml_type =
8.6 + Var of string |
8.7 + Con of string * ml_type list |
8.8 + Tuple of ml_type list |
8.9 + Fun of ml_type * ml_type |
8.10 + Record of (string * ml_type) list
8.11 +
8.12 + val unit: ml_type
8.13 + val canonicalize: ml_type -> ml_type
8.14 +
8.15 + val read_ml_type: string -> ml_type
8.16 + val ml_type_of: Proof.context -> string -> ml_type
8.17 +
8.18 + val pretty: ml_type -> Pretty.T
8.19 +
8.20 + type env = (string * ml_type) list
8.21 + val subst: env -> ml_type -> ml_type
8.22 + val match: ml_type -> ml_type -> env -> env option
8.23 +
8.24 + val strip_fun: ml_type -> ml_type list * ml_type
8.25 +end
8.26 +
8.27 +structure ML_Types: ML_TYPES = struct
8.28 +
8.29 +datatype ml_type =
8.30 + Var of string |
8.31 + Con of string * ml_type list |
8.32 + Tuple of ml_type list |
8.33 + Fun of ml_type * ml_type |
8.34 + Record of (string * ml_type) list
8.35 +
8.36 +val unit = Con ("unit", [])
8.37 +
8.38 +type env = (string * ml_type) list
8.39 +
8.40 +fun subst env (Con (name, ts)) = Con (name, map (subst env) ts)
8.41 + | subst env (Var name) = the_default (Var name) (AList.lookup op = env name)
8.42 + | subst env (Tuple ts) = Tuple (map (subst env) ts)
8.43 + | subst env (Fun (x, y)) = Fun (subst env x, subst env y)
8.44 + | subst env (Record fs) = Record (map (apsnd (subst env)) fs)
8.45 +
8.46 +fun match (Var name) t env =
8.47 + (case AList.lookup op = env name of
8.48 + NONE => SOME ((name, t) :: env)
8.49 + | SOME t' => if t = t' then SOME env else NONE)
8.50 + | match (Fun (x1, y1)) (Fun (x2, y2)) env =
8.51 + Option.mapPartial (match y1 y2) (match x1 x2 env)
8.52 + | match (Con (name1, ts1)) (Con (name2, ts2)) env =
8.53 + if name1 = name2 then match_list ts1 ts2 env else NONE
8.54 + | match (Tuple ts1) (Tuple ts2) env = match_list ts1 ts2 env
8.55 + | match (Record fs1) (Record fs2) env =
8.56 + if map fst fs1 = map fst fs2 then
8.57 + match_list (map snd fs1) (map snd fs2) env
8.58 + else
8.59 + NONE
8.60 + | match _ _ _ = NONE
8.61 +and match_list [] [] env = SOME env
8.62 + | match_list (t :: ts) (u :: us) env =Option.mapPartial (match t u) (match_list ts us env)
8.63 + | match_list _ _ _ = NONE
8.64 +
8.65 +fun strip_fun (Fun (x, y)) = let val (args, res) = strip_fun y in (x :: args, res) end
8.66 + | strip_fun t = ([], t)
8.67 +
8.68 +fun canonicalize (Var name) = Var name
8.69 + | canonicalize (Con (name, ts)) = Con (name, map canonicalize ts)
8.70 + | canonicalize (Tuple []) = unit
8.71 + | canonicalize (Tuple [t]) = canonicalize t
8.72 + | canonicalize (Tuple ts) = Tuple (map canonicalize ts)
8.73 + | canonicalize (Fun (t, u)) = Fun (canonicalize t, canonicalize u)
8.74 + | canonicalize (Record []) = unit
8.75 + | canonicalize (Record es) = Record (sort_by fst (map (apsnd canonicalize) es))
8.76 +
8.77 +val pretty =
8.78 + let
8.79 + datatype shape = SVar | SCon | STuple | SFun_Left | SRoot
8.80 +
8.81 + fun prec SVar _ = error "impossible"
8.82 + | prec SRoot _ = true
8.83 + | prec _ (Var _) = true
8.84 + | prec _ (Record _) = true
8.85 + | prec STuple (Con _) = true
8.86 + | prec STuple _ = false
8.87 + | prec SFun_Left (Con _) = true
8.88 + | prec SFun_Left (Tuple _) = true
8.89 + | prec SFun_Left (Fun _) = false
8.90 + | prec SCon (Con _) = true
8.91 + | prec SCon _ = false
8.92 +
8.93 + fun par n t p = if prec n t then p else Pretty.block [Pretty.str "(", p, Pretty.str ")"]
8.94 +
8.95 + fun aux s t =
8.96 + (case t of
8.97 + Var id => [Pretty.str id]
8.98 + | Tuple ts => Pretty.separate " *" (map (aux STuple) ts)
8.99 + | Fun (arg, res) =>
8.100 + [aux SFun_Left arg, Pretty.brk 1, Pretty.str "->", Pretty.brk 1, aux SRoot res]
8.101 + | Con (id, [t]) =>
8.102 + [aux SCon t, Pretty.brk 1, Pretty.str id]
8.103 + | Con (id, []) =>
8.104 + [Pretty.str id]
8.105 + | Con (id, ts) =>
8.106 + [Pretty.block (Pretty.str "(" :: Pretty.separate "," (map (aux SRoot) ts) @ [Pretty.str ")"]), Pretty.brk 1, Pretty.str id]
8.107 + | Record es =>
8.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 "}"])
8.109 + |> Pretty.block |> par s t
8.110 + in
8.111 + aux SRoot o canonicalize
8.112 + end
8.113 +
8.114 +type token = ML_Lex.token_kind * string
8.115 +
8.116 +type 'a parser = token list -> 'a * token list
8.117 +
8.118 +fun kind k: string parser = Scan.one (equal k o fst) >> snd
8.119 +fun tok t: unit parser = Scan.one (equal t) >> K ()
8.120 +fun keyword k: unit parser = tok (ML_Lex.Keyword, k)
8.121 +val open_parenthesis: unit parser = keyword "("
8.122 +val closed_parenthesis: unit parser = keyword ")"
8.123 +val open_brace: unit parser = keyword "{"
8.124 +val closed_brace: unit parser = keyword "}"
8.125 +val colon: unit parser = keyword ":"
8.126 +val comma: unit parser = keyword ","
8.127 +val arrow: unit parser = keyword "->"
8.128 +val asterisk: unit parser = tok (ML_Lex.Ident, "*")
8.129 +
8.130 +val ident: string parser =
8.131 + kind ML_Lex.Long_Ident ||
8.132 + Scan.one (fn (k, c) => k = ML_Lex.Ident andalso c <> "*") >> snd
8.133 +
8.134 +fun intersep p sep =
8.135 + (p ::: Scan.repeat (sep |-- p)) || Scan.succeed []
8.136 +
8.137 +val typ =
8.138 + let
8.139 + (* code partly lifted from Spec_Check *)
8.140 + fun make_con [] = raise Empty
8.141 + | make_con [c] = c
8.142 + | make_con (Con (s, _) :: cl) = Con (s, [make_con cl]);
8.143 +
8.144 + fun typ s = (func || tuple || typ_single) s
8.145 + and typ_arg s = (tuple || typ_single) s
8.146 + and typ_single s = (con || typ_basic) s
8.147 + and typ_basic s =
8.148 + (var
8.149 + || open_brace |-- record --| closed_brace
8.150 + || open_parenthesis |-- typ --| closed_parenthesis) s
8.151 + and list s = (open_parenthesis |-- typ -- Scan.repeat1 (comma |-- typ) --| closed_parenthesis >> op ::) s
8.152 + and var s = (kind ML_Lex.Type_Var >> Var) s
8.153 + and con s = ((con_nest
8.154 + || typ_basic -- con_nest >> (fn (b, Con (t, _) :: tl) => Con (t, [b]) :: tl)
8.155 + || list -- con_nest >> (fn (l, Con (t, _) :: tl) => Con (t, l) :: tl))
8.156 + >> (make_con o rev)) s
8.157 + and con_nest s = Scan.unless var (Scan.repeat1 (ident >> (Con o rpair []))) s
8.158 + and func s = (typ_arg --| arrow -- typ >> Fun) s
8.159 + and record s = (intersep (kind ML_Lex.Ident -- (colon |-- typ)) comma >> Record) s
8.160 + and tuple s = (typ_single -- Scan.repeat1 (asterisk |-- typ_single)
8.161 + >> (fn (t, tl) => Tuple (t :: tl))) s
8.162 + in typ end
8.163 +
8.164 +fun read_binding s =
8.165 + let
8.166 + val colon = (ML_Lex.Keyword, ":")
8.167 + val semicolon = (ML_Lex.Keyword, ";")
8.168 + fun unpack_tok tok = (ML_Lex.kind_of tok, ML_Lex.content_of tok)
8.169 + val toks = filter (not o equal ML_Lex.Space o fst) (map unpack_tok (ML_Lex.tokenize s))
8.170 + val junk = (Scan.many (not o equal colon) -- tok colon) >> K ()
8.171 + val stopper = Scan.stopper (K semicolon) (equal semicolon)
8.172 + val all = junk |-- Scan.finite stopper typ
8.173 + val (typ, rest) = all toks
8.174 + in
8.175 + if null rest then
8.176 + typ
8.177 + else
8.178 + error "Could not fully parse type"
8.179 + end
8.180 +
8.181 +fun read_ml_type s =
8.182 + let
8.183 + (* FIXME deduplicate *)
8.184 + val semicolon = (ML_Lex.Keyword, ";")
8.185 + fun unpack_tok tok = (ML_Lex.kind_of tok, ML_Lex.content_of tok)
8.186 + val toks = filter (not o equal ML_Lex.Space o fst) (map unpack_tok (ML_Lex.tokenize s))
8.187 + val stopper = Scan.stopper (K semicolon) (equal semicolon)
8.188 + val all = Scan.finite stopper typ
8.189 + val (typ, rest) = all toks
8.190 + in
8.191 + if null rest then
8.192 + typ
8.193 + else
8.194 + error "Could not fully parse type"
8.195 + end
8.196 +
8.197 +fun ml_type_of ctxt s =
8.198 + let
8.199 + (* code partly lifted from Spec_Check *)
8.200 + val return = Unsynchronized.ref NONE
8.201 + val s = "(fn () => (" ^ s ^ "))"
8.202 + val use_context = ml_env_context return
8.203 + val flags =
8.204 + {file = "generated code",
8.205 + line = 0,
8.206 + debug = false,
8.207 + verbose = true}
8.208 + val _ =
8.209 + context_set_thread_data (SOME (Context.Proof ctxt))
8.210 + (fn () => secure_use_text use_context flags s) ()
8.211 + val (Fun (Con ("unit", []), typ)) = read_binding (the (! return))
8.212 + in
8.213 + typ
8.214 + end
8.215 +
8.216 +end
8.217 +
8.218 +type ml_type = ML_Types.ml_type
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/libisabelle-protocol/classy/pretty_class.ML Tue Sep 04 14:50:30 2018 +0200
9.3 @@ -0,0 +1,12 @@
9.4 +datatype 'a pretty_class = Pretty of ('a -> Pretty.T)
9.5 +
9.6 +fun format (Pretty f) = f
9.7 +
9.8 +structure Pretty_Class = struct
9.9 +
9.10 +val string: string pretty_class = Pretty Pretty.str
9.11 +val pretty: Pretty.T pretty_class = Pretty I
9.12 +fun list (Pretty f): 'a list pretty_class =
9.13 + Pretty (fn xs => Pretty.block (Pretty.str "[" :: Pretty.separate "," (map f xs) @ [Pretty.str "]"]))
9.14 +
9.15 +end
9.16 \ No newline at end of file
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/libisabelle-protocol/etc/settings Tue Sep 04 14:50:30 2018 +0200
10.3 @@ -0,0 +1,1 @@
10.4 +LIBISABELLE_RESOURCES_HOME="$COMPONENT"
10.5 \ No newline at end of file
11.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/libisabelle-protocol/libisabelle/Protocol_Main.thy Tue Sep 04 14:50:30 2018 +0200
11.3 @@ -0,0 +1,9 @@
11.4 +theory Protocol_Main
11.5 +imports
11.6 + Main
11.7 + "operations/HOL_Operations"
11.8 + Protocol.Basic
11.9 + Protocol.ML_Expr
11.10 +begin
11.11 +
11.12 +end
11.13 \ No newline at end of file
12.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
12.2 +++ b/libisabelle-protocol/libisabelle/Protocol_Pure.thy Tue Sep 04 14:50:30 2018 +0200
12.3 @@ -0,0 +1,8 @@
12.4 +theory Protocol_Pure
12.5 +imports
12.6 + Pure
12.7 + "operations/Basic"
12.8 + "operations/ML_Expr"
12.9 +begin
12.10 +
12.11 +end
12.12 \ No newline at end of file
13.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
13.2 +++ b/libisabelle-protocol/libisabelle/ROOT Tue Sep 04 14:50:30 2018 +0200
13.3 @@ -0,0 +1,13 @@
13.4 +session Protocol = Classy +
13.5 + theories
13.6 + "protocol/Protocol"
13.7 + "protocol/Codec_Test"
13.8 + "Protocol_Pure"
13.9 +
13.10 +session "HOL-Protocol" = "HOL-Classy" +
13.11 + sessions
13.12 + Protocol
13.13 + theories
13.14 + Protocol.Protocol
13.15 + Protocol.Codec_Test
13.16 + "Protocol_Main"
14.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
14.2 +++ b/libisabelle-protocol/libisabelle/operations/Basic.thy Tue Sep 04 14:50:30 2018 +0200
14.3 @@ -0,0 +1,11 @@
14.4 +theory Basic
14.5 +imports "../protocol/Protocol"
14.6 +begin
14.7 +
14.8 +operation_setup (auto) ping = \<open>fn () => ()\<close>
14.9 +
14.10 +operation_setup (auto) hello = \<open>fn data => "Hello " ^ data\<close>
14.11 +
14.12 +operation_setup (sequential, bracket, auto) use_thys = \<open>List.app Thy_Info.use_thy\<close>
14.13 +
14.14 +end
15.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
15.2 +++ b/libisabelle-protocol/libisabelle/operations/HOL_Operations.thy Tue Sep 04 14:50:30 2018 +0200
15.3 @@ -0,0 +1,24 @@
15.4 +theory HOL_Operations
15.5 +imports Main Protocol.Protocol
15.6 +begin
15.7 +
15.8 +operation_setup mk_int = \<open>
15.9 + {from_lib = Codec.int,
15.10 + to_lib = Codec.term,
15.11 + action = HOLogic.mk_number @{typ int}}\<close>
15.12 +
15.13 +operation_setup dest_int = \<open>
15.14 + {from_lib = Codec.term,
15.15 + to_lib = Codec.option Codec.int,
15.16 + action = fn t => case try HOLogic.dest_number t of
15.17 + NONE => NONE
15.18 + | SOME (typ, n) =>
15.19 + if typ = @{typ int} then
15.20 + SOME n
15.21 + else
15.22 + NONE}\<close>
15.23 +
15.24 +operation_setup (auto) mk_list = \<open>uncurry HOLogic.mk_list\<close>
15.25 +operation_setup (auto) dest_list = \<open>try HOLogic.dest_list\<close>
15.26 +
15.27 +end
16.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
16.2 +++ b/libisabelle-protocol/libisabelle/operations/ML_Expr.thy Tue Sep 04 14:50:30 2018 +0200
16.3 @@ -0,0 +1,41 @@
16.4 +theory ML_Expr
16.5 +imports "../protocol/Protocol"
16.6 +begin
16.7 +
16.8 +ML_file "ml_expr.ML"
16.9 +ML_file "refs.ML"
16.10 +
16.11 +operation_setup eval_expr = \<open>
16.12 + {from_lib = Codec.triple Codec.string ML_Expr.codec Codec.string,
16.13 + to_lib = Codec.tree,
16.14 + action = fn (typ, prog, thy_name) =>
16.15 + let
16.16 + val thy = get_theory thy_name
16.17 + val ctxt = Proof_Context.init_global thy
16.18 + in
16.19 + ML_Expr.eval ctxt prog typ
16.20 + end}\<close>
16.21 +
16.22 +operation_setup eval_opaque_expr = \<open>
16.23 + {from_lib = Codec.triple (Codec.triple Codec.string Codec.string ML_Expr.codec) ML_Expr.codec Codec.string,
16.24 + to_lib = Codec.tuple Codec.int Codec.tree,
16.25 + action = fn ((table, repr_typ, conv), prog, thy_name) =>
16.26 + let
16.27 + val thy = get_theory thy_name
16.28 + val ctxt = Proof_Context.init_global thy
16.29 + in
16.30 + ML_Expr.eval_opaque ctxt prog {table = table, repr_typ = repr_typ, conv = conv}
16.31 + end}\<close>
16.32 +
16.33 +operation_setup check_expr = \<open>
16.34 + {from_lib = Codec.triple Codec.string ML_Expr.codec Codec.string,
16.35 + to_lib = Codec.option Codec.string,
16.36 + action = fn (typ, prog, thy_name) =>
16.37 + let
16.38 + val thy = get_theory thy_name
16.39 + val ctxt = Proof_Context.init_global thy
16.40 + in
16.41 + ML_Expr.check ctxt prog typ
16.42 + end}\<close>
16.43 +
16.44 +end
17.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
17.2 +++ b/libisabelle-protocol/libisabelle/operations/ml_expr.ML Tue Sep 04 14:50:30 2018 +0200
17.3 @@ -0,0 +1,132 @@
17.4 +signature ML_EXPR = sig
17.5 + datatype ml_expr =
17.6 + Lit of string
17.7 + | App of ml_expr * ml_expr
17.8 + | Val of string * XML.tree
17.9 +
17.10 + val print_ml_expr: Proof.context -> ml_expr -> string
17.11 + val eval: Proof.context -> ml_expr -> string -> XML.tree
17.12 + val eval_opaque: Proof.context -> ml_expr -> {table: string, repr_typ: string, conv: ml_expr} -> serial * XML.tree
17.13 + val check: Proof.context -> ml_expr -> string -> string option
17.14 +
17.15 + val print_tree: XML.tree -> string
17.16 + val print_body: XML.body -> string
17.17 +
17.18 + (* internal *)
17.19 + val codec: ml_expr codec
17.20 + structure Eval : TYPED_EVAL
17.21 +end
17.22 +
17.23 +structure ML_Expr : ML_EXPR = struct
17.24 +
17.25 +structure Eval = Typed_Eval
17.26 +(
17.27 + type T = XML.tree
17.28 + val typ = "XML.tree"
17.29 + val name = "ML_Expr.Eval"
17.30 +)
17.31 +
17.32 +fun print_tree (XML.Elem elem) =
17.33 + let
17.34 + val str =
17.35 + ML_Syntax.print_pair
17.36 + (ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_properties)
17.37 + print_body
17.38 + elem
17.39 + in "(XML.Elem " ^ str ^ ")" end
17.40 + | print_tree (XML.Text text) =
17.41 + "(XML.Text " ^ ML_Syntax.print_string text ^ ")"
17.42 +and print_body body =
17.43 + ML_Syntax.print_list print_tree body
17.44 +
17.45 +datatype ml_expr =
17.46 + Lit of string
17.47 + | App of ml_expr * ml_expr
17.48 + | Val of string * XML.tree
17.49 +
17.50 +fun print_ml_expr _ (Lit text) =
17.51 + text
17.52 + | print_ml_expr ctxt (App (f, x)) =
17.53 + "(" ^ print_ml_expr ctxt f ^ ") (" ^ print_ml_expr ctxt x ^ ")"
17.54 + | print_ml_expr ctxt (Val (typ, value)) =
17.55 + let
17.56 + val codec = Classy.resolve @{ML.class codec} (ML_Types.read_ml_type typ) (Context.Proof ctxt)
17.57 + in "(Codec.the_decode " ^ codec ^ " " ^ print_tree value ^ ")" end
17.58 +
17.59 +fun check ctxt prog raw_typ =
17.60 + case try ML_Types.read_ml_type raw_typ of
17.61 + NONE => SOME ("failed to parse result type " ^ raw_typ)
17.62 + | SOME typ =>
17.63 + let
17.64 + val context = Context.Proof ctxt
17.65 + val codec = can (Classy.resolve @{ML.class codec} typ) context
17.66 +
17.67 + fun check_vals (Lit _) = NONE
17.68 + | check_vals (App (f, x)) = merge_options (check_vals f, check_vals x)
17.69 + | check_vals (Val (raw_typ, _)) =
17.70 + case try ML_Types.read_ml_type raw_typ of
17.71 + NONE => SOME ("failed to parse value type " ^ raw_typ)
17.72 + | SOME _ =>
17.73 + if can (Classy.resolve @{ML.class codec} typ) context then
17.74 + NONE
17.75 + else
17.76 + SOME ("could not resolve codec for value type " ^ raw_typ)
17.77 + in
17.78 + if not codec then
17.79 + SOME ("could not resolve codec for result type " ^ raw_typ)
17.80 + else
17.81 + case check_vals prog of
17.82 + SOME err => SOME err
17.83 + | NONE =>
17.84 + case Exn.capture (ML_Types.ml_type_of ctxt) (print_ml_expr ctxt prog) of
17.85 + Exn.Res typ' =>
17.86 + if typ = typ' then
17.87 + NONE
17.88 + else
17.89 + SOME ("expected result type " ^ raw_typ ^ " but got something else")
17.90 + | Exn.Exn exn =>
17.91 + SOME ("compilation error: " ^ @{make_string} exn)
17.92 + end
17.93 +
17.94 +fun eval ctxt prog typ =
17.95 + let
17.96 + val codec = Classy.resolve @{ML.class codec} (ML_Types.read_ml_type typ) (Context.Proof ctxt)
17.97 + val prog = "(Codec.encode " ^ codec ^ " (" ^ print_ml_expr ctxt prog ^ "))"
17.98 + in
17.99 + Eval.eval (Input.string prog) ctxt
17.100 + end
17.101 +
17.102 +fun eval_opaque ctxt prog {table, repr_typ, conv} =
17.103 + let
17.104 + val codec = Classy.resolve @{ML.class codec} (ML_Types.read_ml_type repr_typ) (Context.Proof ctxt)
17.105 + val id = serial ()
17.106 + val var = "eval_opaque_result"
17.107 + val inner_prog = "(" ^ print_ml_expr ctxt prog ^ ")"
17.108 + val store_prog = table ^ ".write " ^ ML_Syntax.print_int id ^ " " ^ var
17.109 + val res_prog = "Codec.encode " ^ codec ^ " ((" ^ print_ml_expr ctxt conv ^ ") " ^ var ^ ")"
17.110 + val prog =
17.111 + "(let " ^
17.112 + "val " ^ var ^ " = " ^ inner_prog ^
17.113 + " in " ^
17.114 + "(" ^ store_prog ^ " ; " ^ res_prog ^ ") " ^
17.115 + "end)"
17.116 + in
17.117 + (id, Eval.eval (Input.string prog) ctxt)
17.118 + end
17.119 +
17.120 +fun codec () =
17.121 + let
17.122 + val ml_expr_lit = Codec.string
17.123 + fun ml_expr_app () = Codec.tuple (codec ()) (codec ())
17.124 + val ml_expr_val = Codec.tuple Codec.string Codec.tree
17.125 +
17.126 + fun enc _ = error "impossible"
17.127 + fun dec 0 = SOME (Codec.decode ml_expr_lit #> Codec.map_result Lit)
17.128 + | dec 1 = SOME (Codec.decode (ml_expr_app ()) #> Codec.map_result App)
17.129 + | dec 2 = SOME (Codec.decode ml_expr_val #> Codec.map_result Val)
17.130 + | dec _ = NONE
17.131 + in Codec.variant enc dec "ML_Expr.ml_expr" end
17.132 +
17.133 +val codec = codec ()
17.134 +
17.135 +end
18.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
18.2 +++ b/libisabelle-protocol/libisabelle/operations/refs.ML Tue Sep 04 14:50:30 2018 +0200
18.3 @@ -0,0 +1,7 @@
18.4 +structure Refs = struct
18.5 + structure Thy = Ref_Table(type t = theory; val name = "Refs.Thy")
18.6 + structure Ctxt = Ref_Table(type t = Proof.context; val name = "Refs.Ctxt")
18.7 + structure State = Ref_Table(type t = Proof.state; val name = "Refs.State")
18.8 + structure Thm = Ref_Table(type t = thm; val name = "Refs.Thm")
18.9 + structure Cterm = Ref_Table(type t = cterm; val name = "Refs.Cterm")
18.10 +end
18.11 \ No newline at end of file
19.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
19.2 +++ b/libisabelle-protocol/libisabelle/protocol/Codec_Class.thy Tue Sep 04 14:50:30 2018 +0200
19.3 @@ -0,0 +1,21 @@
19.4 +theory Codec_Class
19.5 +imports Common "Classy.Classy"
19.6 +begin
19.7 +
19.8 +ML.class codec = \<open>'a codec\<close>
19.9 +
19.10 +ML.instance \<open>Codec.unit\<close> :: codec
19.11 +ML.instance \<open>Codec.bool\<close> :: codec
19.12 +ML.instance \<open>Codec.string\<close> :: codec
19.13 +ML.instance \<open>Codec.int\<close> :: codec
19.14 +ML.instance \<open>Codec.list\<close> :: codec
19.15 +ML.instance \<open>Codec.tuple\<close> :: codec
19.16 +ML.instance \<open>Codec.option\<close> :: codec
19.17 +ML.instance \<open>Codec.either\<close> :: codec
19.18 +ML.instance \<open>Codec.triple\<close> :: codec
19.19 +ML.instance \<open>Codec.sort\<close> :: codec
19.20 +ML.instance \<open>Codec.typ\<close> :: codec
19.21 +ML.instance \<open>Codec.term\<close> :: codec
19.22 +ML.instance \<open>Codec.tree\<close> :: codec
19.23 +
19.24 +end
20.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
20.2 +++ b/libisabelle-protocol/libisabelle/protocol/Codec_Test.thy Tue Sep 04 14:50:30 2018 +0200
20.3 @@ -0,0 +1,41 @@
20.4 +theory Codec_Test
20.5 +imports Common "~~/src/Tools/Spec_Check/Spec_Check"
20.6 +begin
20.7 +
20.8 +ML\<open>
20.9 +fun check_for str =
20.10 + let
20.11 + val prop1 =
20.12 + "ALL x. (let val c = (" ^ str ^ ") in Codec.decode c (Codec.encode c x) = Codec.Success x end)"
20.13 + val prop2 =
20.14 + "ALL x. (let val c = (" ^ str ^ ") in Codec.decode c (YXML.parse (YXML.string_of (Codec.encode c x))) = Codec.Success x end)"
20.15 + in
20.16 + check_property prop1;
20.17 + check_property prop2
20.18 + end
20.19 +
20.20 +fun gen_unit r =
20.21 + ((), r)
20.22 +\<close>
20.23 +
20.24 +ML_command\<open>
20.25 + check_for "Codec.unit";
20.26 + check_for "Codec.int";
20.27 + check_for "Codec.bool";
20.28 + check_for "Codec.string";
20.29 + check_for "Codec.tuple Codec.int Codec.int";
20.30 + check_for "Codec.tuple Codec.string Codec.unit";
20.31 + check_for "Codec.list Codec.unit";
20.32 + check_for "Codec.list Codec.int";
20.33 + check_for "Codec.list Codec.string";
20.34 + check_for "Codec.list (Codec.list Codec.string)";
20.35 + check_for "Codec.list (Codec.tuple Codec.int Codec.int)";
20.36 + check_for "Codec.tuple Codec.int (Codec.list Codec.int)";
20.37 + check_for "Codec.option Codec.int";
20.38 + check_for "Codec.option (Codec.list Codec.int)";
20.39 + check_for "Codec.list (Codec.option (Codec.int))";
20.40 + check_for "Codec.term";
20.41 + check_for "Codec.typ";
20.42 +\<close>
20.43 +
20.44 +end
21.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
21.2 +++ b/libisabelle-protocol/libisabelle/protocol/Common.thy Tue Sep 04 14:50:30 2018 +0200
21.3 @@ -0,0 +1,80 @@
21.4 +theory Common
21.5 +imports Pure
21.6 +begin
21.7 +
21.8 +ML\<open>
21.9 + val print_int = Value.print_int
21.10 + val parse_int = Value.parse_int
21.11 + val print_bool = Value.print_bool
21.12 + val parse_bool = Value.parse_bool
21.13 + fun get_theory name =
21.14 + let
21.15 + val all = Thy_Info.get_names ()
21.16 + val qualified = find_first (fn name' => name = Long_Name.base_name name') all
21.17 + in Thy_Info.get_theory (the qualified) end
21.18 +\<close>
21.19 +
21.20 +ML\<open>
21.21 +local
21.22 + (* code copied and adapted from Isabelle/Pure *)
21.23 +
21.24 + fun encode "<" = "<"
21.25 + | encode ">" = ">"
21.26 + | encode "&" = "&"
21.27 + | encode "'" = "'"
21.28 + | encode "\"" = """
21.29 + | encode s =
21.30 + let val c = ord s in
21.31 + if c < 32 then "&#" ^ string_of_int c ^ ";"
21.32 + else if c < 127 then s
21.33 + else "&#" ^ string_of_int c ^ ";"
21.34 + end
21.35 +
21.36 + fun decode "lt" = "<"
21.37 + | decode "gt" = ">"
21.38 + | decode "amp" = "&"
21.39 + | decode "apos" = "'"
21.40 + | decode "quot" = "\""
21.41 + | decode s = chr (parse_int (unprefix "#" s))
21.42 +
21.43 + fun entity_char c = c <> ";"
21.44 + val parse_name = Scan.many entity_char
21.45 +
21.46 + val special = $$ "&" |-- (parse_name >> implode >> decode) --| $$ ";"
21.47 + val regular = Scan.one Symbol.not_eof
21.48 + val parse_chars = Scan.repeat (special || regular) >> implode
21.49 + val parse_string = Scan.read Symbol.stopper parse_chars o raw_explode
21.50 +in
21.51 + val encode_string = translate_string encode
21.52 + val decode_string = the o parse_string
21.53 +end
21.54 +\<close>
21.55 +
21.56 +ML_file "typed_eval.ML"
21.57 +ML_file "codec.ML"
21.58 +ML_file "ref_table.ML"
21.59 +ML_file "protocol.ML"
21.60 +
21.61 +syntax "_cartouche_xml" :: "cartouche_position \<Rightarrow> 'a" ("XML _")
21.62 +
21.63 +parse_translation\<open>
21.64 +let
21.65 + fun translation args =
21.66 + let
21.67 + fun err () = raise TERM ("Common._cartouche_xml", args)
21.68 + fun input s pos = Symbol_Pos.implode (Symbol_Pos.cartouche_content (Symbol_Pos.explode (s, pos)))
21.69 + val eval = Codec.the_decode Codec.term o XML.parse
21.70 + in
21.71 + case args of
21.72 + [(c as Const (@{syntax_const "_constrain"}, _)) $ Free (s, _) $ p] =>
21.73 + (case Term_Position.decode_position p of
21.74 + SOME (pos, _) => c $ eval (input s pos) $ p
21.75 + | NONE => err ())
21.76 + | _ => err ()
21.77 + end
21.78 +in
21.79 + [(@{syntax_const "_cartouche_xml"}, K translation)]
21.80 +end
21.81 +\<close>
21.82 +
21.83 +end
22.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
22.2 +++ b/libisabelle-protocol/libisabelle/protocol/Protocol.thy Tue Sep 04 14:50:30 2018 +0200
22.3 @@ -0,0 +1,54 @@
22.4 +theory Protocol
22.5 +imports Codec_Class
22.6 +keywords "operation_setup" :: thy_decl % "ML"
22.7 +begin
22.8 +
22.9 +ML\<open>
22.10 +val _ =
22.11 + let
22.12 + open Libisabelle_Protocol
22.13 + fun operation_setup_cmd name source (flags as {auto, ...}) ctxt =
22.14 + let
22.15 + fun eval enclose =
22.16 + ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of source)
22.17 + (ML_Lex.read ("Libisabelle_Protocol.add_operation " ^ ML_Syntax.print_string name ^ "(") @
22.18 + enclose (ML_Lex.read_source false source) @
22.19 + ML_Lex.read ")" @
22.20 + ML_Lex.read (print_flags flags))
22.21 + in
22.22 + if auto then
22.23 + let
22.24 + (* FIXME breaks antiquotations *)
22.25 + val ML_Types.Fun (arg, res) = ML_Types.ml_type_of ctxt (Input.source_content source)
22.26 + val arg_codec = Classy.resolve @{ML.class codec} arg (Context.Proof ctxt)
22.27 + val res_codec = Classy.resolve @{ML.class codec} res (Context.Proof ctxt)
22.28 + fun enclose toks =
22.29 + ML_Lex.read "{from_lib=" @ ML_Lex.read arg_codec @ ML_Lex.read "," @
22.30 + ML_Lex.read "to_lib=" @ ML_Lex.read res_codec @ ML_Lex.read "," @
22.31 + ML_Lex.read "action=" @ toks @ ML_Lex.read "}"
22.32 + in
22.33 + eval enclose
22.34 + end
22.35 + else
22.36 + eval I
22.37 + end
22.38 + val parse_flag =
22.39 + (Parse.reserved "sequential" || Parse.reserved "bracket" || Parse.reserved "auto") >>
22.40 + (fn flag => join_flags
22.41 + {sequential = flag = "sequential",
22.42 + bracket = flag = "bracket",
22.43 + auto = flag = "auto"})
22.44 + val parse_flags =
22.45 + Parse.list parse_flag >> (fn fs => fold (curry op o) fs I)
22.46 + val parse_cmd =
22.47 + Scan.optional (Args.parens parse_flags) I --
22.48 + Parse.name --
22.49 + Parse.!!! (@{keyword "="} |-- Parse.ML_source)
22.50 + in
22.51 + Outer_Syntax.command @{command_keyword "operation_setup"} "define protocol operation in ML"
22.52 + (parse_cmd >> (fn ((flags, name), txt) =>
22.53 + Toplevel.keep (Toplevel.context_of #> operation_setup_cmd name txt (flags default_flags))))
22.54 + end
22.55 +\<close>
22.56 +
22.57 +end
23.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
23.2 +++ b/libisabelle-protocol/libisabelle/protocol/codec.ML Tue Sep 04 14:50:30 2018 +0200
23.3 @@ -0,0 +1,248 @@
23.4 +signature CODEC = sig
23.5 + datatype 'a result = Success of 'a | Failure of string * XML.body
23.6 + datatype ('a, 'b) either = Left of 'a | Right of 'b
23.7 + type 'a codec
23.8 +
23.9 + val the_success: 'a result -> 'a
23.10 +
23.11 + val map_result: ('a -> 'b) -> 'a result -> 'b result
23.12 + val bind_result: ('a -> 'b result) -> 'a result -> 'b result
23.13 + val sequence_results: 'a result list -> 'a list result
23.14 + val traverse_results: ('a -> 'b result) -> 'a list -> 'b list result
23.15 +
23.16 + val transform: ('a -> 'b) -> ('b -> 'a) -> 'a codec -> 'b codec
23.17 + val encode: 'a codec -> 'a -> XML.tree
23.18 + val decode: 'a codec -> XML.tree -> 'a result
23.19 + val the_decode: 'a codec -> XML.tree -> 'a
23.20 +
23.21 + val basic: {encode: 'a -> XML.tree, decode: XML.tree -> 'a result} -> 'a codec
23.22 +
23.23 + val variant: ('a -> (int * XML.tree)) -> (int -> (XML.tree -> 'a result) option) -> string -> 'a codec
23.24 + val tagged: string -> 'a codec -> 'a codec
23.25 +
23.26 + val unit: unit codec
23.27 + val bool: bool codec
23.28 + val string: string codec
23.29 + val int: int codec
23.30 + val list: 'a codec -> 'a list codec
23.31 + val tuple: 'a codec -> 'b codec -> ('a * 'b) codec
23.32 + val triple: 'a codec -> 'b codec -> 'c codec -> ('a * 'b * 'c) codec
23.33 + val either: 'a codec -> 'b codec -> ('a, 'b) either codec
23.34 + val option: 'a codec -> 'a option codec
23.35 + val tree: XML.tree codec
23.36 +
23.37 + val sort: sort codec
23.38 + val typ: typ codec
23.39 + val term: term codec
23.40 +
23.41 + exception GENERIC of string
23.42 + val exn: exn codec
23.43 + val exn_result: 'a codec -> 'a Exn.result codec
23.44 +
23.45 + (* internal *)
23.46 + val id: XML.tree codec
23.47 +end
23.48 +
23.49 +structure Codec: CODEC = struct
23.50 +
23.51 +datatype 'a result = Success of 'a | Failure of string * XML.body
23.52 +datatype ('a, 'b) either = Left of 'a | Right of 'b
23.53 +
23.54 +fun map_result f (Success a) = Success (f a)
23.55 + | map_result _ (Failure (msg, body)) = Failure (msg, body)
23.56 +
23.57 +fun bind_result f (Success a) = f a
23.58 + | bind_result _ (Failure (msg, body)) = Failure (msg, body)
23.59 +
23.60 +fun traverse_results _ [] = Success []
23.61 + | traverse_results f (x :: xs) =
23.62 + case f x of
23.63 + Success y => map_result (fn ys => y :: ys) (traverse_results f xs)
23.64 + | Failure (msg, body) => Failure (msg, body)
23.65 +
23.66 +fun sequence_results xs = traverse_results I xs
23.67 +
23.68 +fun the_success (Success a) = a
23.69 + | the_success _ = raise Fail "unexpected failure"
23.70 +
23.71 +fun add_tag tag idx body =
23.72 + let
23.73 + val attrs = case idx of SOME i => [("idx", XML.Encode.int_atom i)] | _ => []
23.74 + in XML.Elem (("tag", ("type", tag) :: attrs), body) end
23.75 +
23.76 +fun expect_tag tag tree =
23.77 + case tree of
23.78 + XML.Elem (("tag", [("type", tag')]), body) =>
23.79 + if tag = tag' then
23.80 + Success body
23.81 + else
23.82 + Failure ("tag mismatch: expected " ^ tag ^ ", got " ^ tag', [tree])
23.83 + | _ =>
23.84 + Failure ("tag " ^ tag ^ " expected", [tree])
23.85 +
23.86 +fun expect_tag' tag tree =
23.87 + case tree of
23.88 + XML.Elem (("tag", [("type", tag'), ("idx", i)]), body) =>
23.89 + if tag = tag' then
23.90 + Success (XML.Decode.int_atom i, body)
23.91 + handle XML.XML_ATOM err => Failure (err, [tree])
23.92 + else
23.93 + Failure ("tag mismatch: expected " ^ tag ^ ", got " ^ tag', [tree])
23.94 + | _ =>
23.95 + Failure ("indexed tag " ^ tag ^ " expected", [tree])
23.96 +
23.97 +
23.98 +abstype 'a codec = Codec of {encode: 'a -> XML.tree, decode: XML.tree -> 'a result} with
23.99 +
23.100 +val basic = Codec
23.101 +
23.102 +fun encode (Codec {encode, ...}) = encode
23.103 +fun decode (Codec {decode, ...}) = decode
23.104 +
23.105 +fun transform f g (Codec {encode, decode}) = Codec
23.106 + {encode = g #> encode,
23.107 + decode = decode #> map_result f}
23.108 +
23.109 +fun list a = Codec
23.110 + {encode = map (encode a) #> add_tag "list" NONE,
23.111 + decode = expect_tag "list" #> bind_result (traverse_results (decode a))}
23.112 +
23.113 +fun tuple a b = Codec
23.114 + {encode = (fn (x, y) => add_tag "tuple" NONE [encode a x, encode b y]),
23.115 + decode = expect_tag "tuple" #> bind_result (fn body =>
23.116 + case body of
23.117 + [x, y] => decode a x |> bind_result (fn x' => decode b y |> map_result (pair x'))
23.118 + | _ => Failure ("invalid structure", body))}
23.119 +
23.120 +fun variant enc dec tag = Codec
23.121 + {encode = (fn a => let val (idx, tree) = enc a in add_tag tag (SOME idx) [tree] end),
23.122 + decode = (fn tree => expect_tag' tag tree |> bind_result (fn (idx, body) =>
23.123 + case (body, dec idx) of
23.124 + ([tree'], SOME res) => res tree'
23.125 + | (_, SOME _) => Failure ("invalid structure", [tree])
23.126 + | (_, NONE) => Failure ("invalid index " ^ print_int idx, [tree])))}
23.127 +
23.128 +fun tagged tag a = Codec
23.129 + {encode = encode a #> single #> add_tag tag NONE,
23.130 + decode = expect_tag tag #> bind_result (fn body =>
23.131 + case body of
23.132 + [tree] => decode a tree
23.133 + | _ => Failure ("invalid structure", body))}
23.134 +
23.135 +val unit = Codec
23.136 + {encode = K (add_tag "unit" NONE []),
23.137 + decode = expect_tag "unit" #> bind_result (fn body =>
23.138 + case body of
23.139 + [] => Success ()
23.140 + | _ => Failure ("expected nothing", body))}
23.141 +
23.142 +fun text to from = Codec
23.143 + {encode = fn s => XML.Elem (("text", [("content", encode_string (to s))]), []),
23.144 + decode =
23.145 + (fn tree as XML.Elem (("text", [("content", s)]), []) =>
23.146 + (case from (decode_string s) of
23.147 + NONE => Failure ("decoding failed", [tree]) |
23.148 + SOME a => Success a)
23.149 + | tree => Failure ("expected text tree", [tree]))}
23.150 +
23.151 +val id = Codec {encode = I, decode = Success}
23.152 +
23.153 +end
23.154 +
23.155 +fun the_decode c = the_success o decode c
23.156 +
23.157 +val int = tagged "int" (text print_int (Exn.get_res o Exn.capture parse_int))
23.158 +val bool = tagged "bool" (text print_bool (Exn.get_res o Exn.capture parse_bool))
23.159 +val string = tagged "string" (text I SOME)
23.160 +
23.161 +val tree = tagged "XML.tree" id
23.162 +
23.163 +fun option a =
23.164 + let
23.165 + fun enc (SOME x) = (0, encode a x)
23.166 + | enc NONE = (1, encode unit ())
23.167 + fun dec 0 = SOME (decode a #> map_result SOME)
23.168 + | dec 1 = SOME (decode unit #> map_result (K NONE))
23.169 + | dec _ = NONE
23.170 + in variant enc dec "option" end
23.171 +
23.172 +val content_of =
23.173 + XML.content_of o YXML.parse_body
23.174 +
23.175 +(* slightly fishy codec, doesn't preserve exception type *)
23.176 +exception GENERIC of string
23.177 +
23.178 +fun string_of_exn (ERROR msg) = "ERROR " ^ content_of msg
23.179 + | string_of_exn exn = content_of (@{make_string} exn)
23.180 +
23.181 +val exn = tagged "exn" (text string_of_exn (SOME o GENERIC))
23.182 +
23.183 +fun exn_result a =
23.184 + let
23.185 + fun enc (Exn.Res t) = (0, encode a t)
23.186 + | enc (Exn.Exn e) = (1, encode exn e)
23.187 + fun dec _ = NONE
23.188 + in variant enc dec "Exn.result" end
23.189 +
23.190 +fun triple a b c =
23.191 + tuple a (tuple b c)
23.192 + |> transform (fn (a, (b, c)) => (a, b, c)) (fn (a, b, c) => (a, (b, c)))
23.193 +
23.194 +fun either a b =
23.195 + let
23.196 + fun enc (Left l) = (0, encode a l)
23.197 + | enc (Right r) = (1, encode b r)
23.198 + fun dec 0 = SOME (decode a #> map_result Left)
23.199 + | dec 1 = SOME (decode b #> map_result Right)
23.200 + | dec _ = NONE
23.201 + in variant enc dec "either" end
23.202 +
23.203 +val sort: sort codec = list string
23.204 +val indexname: indexname codec = tuple string int
23.205 +
23.206 +fun typ () =
23.207 + let
23.208 + fun typ_type () = tuple string (list (typ ()))
23.209 + val typ_tfree = tuple string sort
23.210 + val typ_tvar = tuple indexname sort
23.211 +
23.212 + fun enc (Type arg) = (0, encode (typ_type ()) arg)
23.213 + | enc (TFree arg) = (1, encode typ_tfree arg)
23.214 + | enc (TVar arg) = (2, encode typ_tvar arg)
23.215 + fun dec 0 = SOME (decode (typ_type ()) #> map_result Type)
23.216 + | dec 1 = SOME (decode typ_tfree #> map_result TFree)
23.217 + | dec 2 = SOME (decode typ_tvar #> map_result TVar)
23.218 + | dec _ = NONE
23.219 + in variant enc dec "typ" end
23.220 +
23.221 +val typ = typ ()
23.222 +
23.223 +fun term () =
23.224 + let
23.225 + val term_const = tuple string typ
23.226 + val term_free = tuple string typ
23.227 + val term_var = tuple indexname typ
23.228 + val term_bound = int
23.229 + fun term_abs () = triple string typ (term ())
23.230 + fun term_app () = tuple (term ()) (term ())
23.231 +
23.232 + fun enc (Const arg) = (0, encode term_const arg)
23.233 + | enc (Free arg) = (1, encode term_free arg)
23.234 + | enc (Var arg) = (2, encode term_var arg)
23.235 + | enc (Bound arg) = (3, encode term_bound arg)
23.236 + | enc (Abs arg) = (4, encode (term_abs ()) arg)
23.237 + | enc (op $ arg) = (5, encode (term_app ()) arg)
23.238 + fun dec 0 = SOME (decode term_const #> map_result Const)
23.239 + | dec 1 = SOME (decode term_free #> map_result Free)
23.240 + | dec 2 = SOME (decode term_var #> map_result Var)
23.241 + | dec 3 = SOME (decode term_bound #> map_result Bound)
23.242 + | dec 4 = SOME (decode (term_abs ()) #> map_result Abs)
23.243 + | dec 5 = SOME (decode (term_app ()) #> map_result op $)
23.244 + | dec _ = NONE
23.245 + in variant enc dec "term" end
23.246 +
23.247 +val term = term ()
23.248 +
23.249 +end
23.250 +
23.251 +type 'a codec = 'a Codec.codec
23.252 \ No newline at end of file
24.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
24.2 +++ b/libisabelle-protocol/libisabelle/protocol/protocol.ML Tue Sep 04 14:50:30 2018 +0200
24.3 @@ -0,0 +1,119 @@
24.4 +signature LIBISABELLE_PROTOCOL = sig
24.5 + type name = string
24.6 + type ('i, 'o) operation =
24.7 + {from_lib : 'i codec,
24.8 + to_lib : 'o codec,
24.9 + action : 'i -> 'o}
24.10 +
24.11 + type flags = {sequential: bool, bracket: bool, auto: bool (* ignored *)}
24.12 +
24.13 + val default_flags : flags
24.14 + val join_flags : flags -> flags -> flags
24.15 + val print_flags : flags -> string
24.16 +
24.17 + val add_operation : name -> ('i, 'o) operation -> flags -> unit
24.18 + val get_operation : name -> int -> XML.tree -> XML.tree
24.19 +end
24.20 +
24.21 +structure Libisabelle_Protocol: LIBISABELLE_PROTOCOL = struct
24.22 +
24.23 +type name = string
24.24 +type ('i, 'o) operation =
24.25 + {from_lib : 'i codec,
24.26 + to_lib : 'o codec,
24.27 + action : 'i -> 'o}
24.28 +
24.29 +type flags = {sequential: bool, bracket: bool, auto: bool}
24.30 +
24.31 +val default_flags = {sequential = false, bracket = false, auto = false}
24.32 +
24.33 +fun join_flags
24.34 + {sequential = seq1, bracket = br1, auto = a1}
24.35 + {sequential = seq2, bracket = br2, auto = a2} =
24.36 + {sequential = seq1 orelse seq2, bracket = br1 orelse br2, auto = a1 orelse a2}
24.37 +
24.38 +fun print_flags {sequential, bracket, auto} =
24.39 + "({sequential=" ^ print_bool sequential ^ "," ^
24.40 + "bracket=" ^ print_bool bracket ^ "," ^
24.41 + "auto=" ^ print_bool auto ^ "})"
24.42 +
24.43 +type raw_operation = int -> XML.tree -> XML.tree
24.44 +
24.45 +exception GENERIC of string
24.46 +
24.47 +val operations =
24.48 + Synchronized.var "libisabelle.operations" (Symtab.empty: raw_operation Symtab.table)
24.49 +
24.50 +val requests =
24.51 + Synchronized.var "libisabelle.requests" (Inttab.empty: (unit -> unit) Inttab.table)
24.52 +
24.53 +fun sequentialize name f =
24.54 + let
24.55 + val var = Synchronized.var ("libisabelle." ^ name) ()
24.56 + in
24.57 + fn x => Synchronized.change_result var (fn _ => (f x, ()))
24.58 + end
24.59 +
24.60 +fun bracketize f id x =
24.61 + let
24.62 + val start = [(Markup.functionN, "libisabelle_start"), ("id", print_int id)]
24.63 + val stop = [(Markup.functionN, "libisabelle_stop"), ("id", print_int id)]
24.64 + val _ = Output.protocol_message start []
24.65 + val res = f id x
24.66 + val _ = Output.protocol_message stop []
24.67 + in res end
24.68 +
24.69 +fun add_operation name {from_lib, to_lib, action} {sequential, bracket, ...} =
24.70 + let
24.71 + fun raw _ tree =
24.72 + case Codec.decode from_lib tree of
24.73 + Codec.Success i => Codec.encode to_lib (action i)
24.74 + | Codec.Failure (msg, _) => raise Fail ("decoding input failed for operation " ^ name ^ ": " ^ msg)
24.75 + val raw' = raw
24.76 + |> (if bracket then bracketize else I)
24.77 + |> (if sequential then sequentialize name else I)
24.78 + in
24.79 + Synchronized.change operations (Symtab.update (name, raw'))
24.80 + end
24.81 +
24.82 +fun get_operation name =
24.83 + case Symtab.lookup (Synchronized.value operations) name of
24.84 + SOME operation => operation
24.85 + | NONE => fn _ => error "libisabelle: unknown command"
24.86 +
24.87 +val _ = Isabelle_Process.protocol_command "libisabelle"
24.88 + (fn id :: name :: [arg] =>
24.89 + let
24.90 + val id = parse_int id
24.91 + val response = [(Markup.functionN, "libisabelle_response"), ("id", print_int id)]
24.92 + val args = YXML.parse arg
24.93 + fun exec f =
24.94 + let
24.95 + val future = Future.fork (fn () =>
24.96 + let
24.97 + val res = Exn.interruptible_capture (fn () => f id args) ()
24.98 + val yxml = YXML.string_of (Codec.encode (Codec.exn_result Codec.id) res)
24.99 + in
24.100 + Output.protocol_message response [yxml]
24.101 + end)
24.102 + in
24.103 + Synchronized.change requests (Inttab.update_new (id, fn () => Future.cancel future))
24.104 + end
24.105 + in
24.106 + exec (get_operation name)
24.107 + end)
24.108 +
24.109 +val _ = Isabelle_Process.protocol_command "libisabelle_cancel"
24.110 + (fn ids =>
24.111 + let
24.112 + fun remove id tab = (Inttab.lookup tab id, Inttab.delete_safe id tab)
24.113 + val _ =
24.114 + map parse_int ids
24.115 + |> fold_map remove
24.116 + |> Synchronized.change_result requests
24.117 + |> map (fn NONE => () | SOME f => f ())
24.118 + in
24.119 + ()
24.120 + end)
24.121 +
24.122 +end
25.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
25.2 +++ b/libisabelle-protocol/libisabelle/protocol/ref_table.ML Tue Sep 04 14:50:30 2018 +0200
25.3 @@ -0,0 +1,31 @@
25.4 +signature REF_TABLE = sig
25.5 + type t
25.6 + val read: serial -> t
25.7 + val write: serial -> t -> unit
25.8 + val delete: serial -> unit
25.9 +
25.10 + (* internal *)
25.11 + val peek: unit -> t Inttab.table
25.12 +end
25.13 +
25.14 +signature REF_TABLE_ARGS = sig
25.15 + type t
25.16 + val name: string
25.17 +end
25.18 +
25.19 +functor Ref_Table(Args : REF_TABLE_ARGS) : REF_TABLE where type t = Args.t = struct
25.20 +
25.21 +type t = Args.t
25.22 +
25.23 +type table = t Inttab.table
25.24 +val empty_table : table = Inttab.empty
25.25 +
25.26 +val table = Synchronized.var ("Ref_Table." ^ Args.name) empty_table
25.27 +
25.28 +fun read ser = the (Inttab.lookup (Synchronized.value table) ser)
25.29 +fun write ser t = Synchronized.change table (Inttab.update (ser, t))
25.30 +val delete = Synchronized.change table o Inttab.delete
25.31 +
25.32 +fun peek () = Synchronized.value table
25.33 +
25.34 +end
26.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
26.2 +++ b/libisabelle-protocol/libisabelle/protocol/typed_eval.ML Tue Sep 04 14:50:30 2018 +0200
26.3 @@ -0,0 +1,38 @@
26.4 +signature TYPED_EVAL = sig
26.5 + type T
26.6 + val eval: Input.source -> Proof.context -> T
26.7 +
26.8 + val fulfill: T -> Context.generic -> Context.generic (* internal *)
26.9 +end
26.10 +
26.11 +signature TYPED_EVAL_ARGS = sig
26.12 + type T
26.13 + val typ: string
26.14 + val name: string
26.15 +end
26.16 +
26.17 +functor Typed_Eval(Args : TYPED_EVAL_ARGS) : TYPED_EVAL = struct
26.18 +
26.19 +structure Data = Generic_Data
26.20 +(
26.21 + type T = Args.T option
26.22 + val empty = NONE
26.23 + val extend = I
26.24 + fun merge (NONE, NONE) = NONE
26.25 + | merge _ = error "Typed_Eval.Data.merge: can't merge"
26.26 +)
26.27 +
26.28 +type T = Args.T
26.29 +
26.30 +val fulfill = Data.map o K o SOME
26.31 +
26.32 +fun eval source ctxt =
26.33 + ML_Context.expression (Input.range_of source)
26.34 + "typed_eval_result" Args.typ
26.35 + (Args.name ^ ".fulfill typed_eval_result")
26.36 + (ML_Lex.read_source false source)
26.37 + (Context.Proof ctxt)
26.38 + |> Data.get
26.39 + |> the
26.40 +
26.41 +end
26.42 \ No newline at end of file
27.1 --- a/src/Tools/isac/Build_Isac.thy Wed Aug 29 11:27:22 2018 +0200
27.2 +++ b/src/Tools/isac/Build_Isac.thy Tue Sep 04 14:50:30 2018 +0200
27.3 @@ -56,9 +56,9 @@
27.4 "Knowledge/Build_Thydata" (*imports Isac.thy etc*)
27.5
27.6 (* the Protocol for the connection isac-java -- Isabelle/Isac is built separately:
27.7 - libisabelle$ /usr/local/isabisac/bin/isabelle build -D . -bv
27.8 here we partly check consistency libisabelle/Isac -- Isabelle/Isac: *)
27.9 - (*"~~/libisabelle-protocol/isabelle-2015/Protocol"*)
27.10 + (*"~~/libisabelle-protocol/libisabelle/protocol/Protocol"*) Protocol.Protocol
27.11 +
27.12 begin
27.13
27.14 text {*
28.1 --- a/src/Tools/isac/Isac_Protocol.thy Wed Aug 29 11:27:22 2018 +0200
28.2 +++ b/src/Tools/isac/Isac_Protocol.thy Tue Sep 04 14:50:30 2018 +0200
28.3 @@ -1,5 +1,5 @@
28.4 theory Isac_Protocol
28.5 -imports "~~/libisabelle-protocol/libisabelle/protocol/Protocol" "~~/src/Tools/isac/Knowledge/Build_Thydata"
28.6 +imports "~~/src/Tools/isac/Knowledge/Build_Thydata" (*"~~/libisabelle-protocol/libisabelle/protocol/Protocol"*) Protocol.Protocol
28.7 begin
28.8
28.9 (* val appendFormula : calcID -> cterm' -> XML.tree *)
29.1 --- a/src/Tools/isac/ROOT Wed Aug 29 11:27:22 2018 +0200
29.2 +++ b/src/Tools/isac/ROOT Tue Sep 04 14:50:30 2018 +0200
29.3 @@ -29,7 +29,6 @@
29.4 options [document = false (*, browser_info = true*)]
29.5 theories Build_Isac
29.6
29.7 -(*//----- update Isabelle2017 -> Isabelle2018 without libisabelle, see libisabelle_DUMMY ---------
29.8 session libisabelle_Isac = HOL +
29.9 description {*
29.10 Isac core, prototype of a math-engine and knowledge for engineering math
29.11 @@ -41,6 +40,7 @@
29.12 For installation see http://www.ist.tugraz.at/isac
29.13 *}
29.14 options [document = false (*, browser_info = true*)]
29.15 - theories Isac_Protocol
29.16 - "~~/libisabelle-protocol/libisabelle/protocol/Protocol"
29.17 ------ update Isabelle2017 -> Isabelle2018 without libisabelle, see libisabelle_DUMMY ---------//*)
29.18 + sessions
29.19 + Protocol
29.20 + theories
29.21 + Isac_Protocol
30.1 --- a/src/Tools/isac/xmlsrc/mathml.sml Wed Aug 29 11:27:22 2018 +0200
30.2 +++ b/src/Tools/isac/xmlsrc/mathml.sml Tue Sep 04 14:50:30 2018 +0200
30.3 @@ -48,8 +48,7 @@
30.4 fun xmlstr i (XML.Text str) = indent i ^ str ^ "\n"
30.5 | xmlstr i (XML.Elem (("TERM", []), [xt])) =
30.6 indent i ^ "(" ^ "TERM" ^ ")" ^ "\n" ^
30.7 - (*indent (i + 1) ^ (xt |> Codec.decode Codec.term |> Codec.the_success |> Rule.term2str) ^ "\n" ^ *)
30.8 - indent (i + 1) ^ "libisabelle_DUMMY" ^ "\n" ^
30.9 + indent (i + 1) ^ (xt |> Codec.decode Codec.term |> Codec.the_success |> Rule.term2str) ^ "\n" ^
30.10 indent i ^ "(/" ^ "TERM" ^ ")" ^ "\n"
30.11 | xmlstr i (XML.Elem ((str, []), trees)) =
30.12 indent i ^ "(" ^ str ^ ")" ^ "\n" ^
30.13 @@ -99,16 +98,13 @@
30.14 (* intermediate replacements while introducing transfer of terms by libisabelle *)
30.15 fun xml_of_term_NEW (t : term) =
30.16 XML.Elem (("FORMULA", []), [
30.17 - (*XML.Elem (("ISA", []), [XML.Text ((decode o Rule.term2str) t)]),*)
30.18 - XML.Elem (("ISA", []), [XML.Text ("libisabelle_DUMMY ")]),
30.19 - (*XML.Elem (("TERM", []), [Codec.encode Codec.term t])])*)
30.20 - XML.Elem (("TERM", []), [XML.Text ("libisabelle_DUMMY")])])
30.21 + XML.Elem (("ISA", []), [XML.Text ((decode o Rule.term2str) t)]),
30.22 + XML.Elem (("TERM", []), [Codec.encode Codec.term t])])
30.23 (* unused: formulas come as strings from frontend and are parsed by Isabelle *)
30.24 fun xml_to_term_UNUSED
30.25 ((XML.Elem (("FORMULA", []), [
30.26 XML.Elem (("ISA", []), [XML.Text _]),
30.27 - (*XML.Elem (("TERM", []), [xt])]))) = xt |> Codec.decode Codec.term |> Codec.the_success*)
30.28 - XML.Elem (("TERM", []), [xt])]))) = Const ("libisabelle_DUMMY", Type ("'a", []))
30.29 + XML.Elem (("TERM", []), [xt])]))) = xt |> Codec.decode Codec.term |> Codec.the_success
30.30 | xml_to_term_UNUSED xx = raise ERROR ("xml_to_term_NEW wrong arg: " ^ xmlstr 0 xx)
30.31
30.32 (*version for TextIO*)
31.1 --- a/src/Tools/isac/xmlsrc/xmlsrc.thy Wed Aug 29 11:27:22 2018 +0200
31.2 +++ b/src/Tools/isac/xmlsrc/xmlsrc.thy Tue Sep 04 14:50:30 2018 +0200
31.3 @@ -4,8 +4,7 @@
31.4 *)
31.5
31.6 theory xmlsrc
31.7 - imports (*"~~/libisabelle-protocol/libisabelle/protocol/Codec_Class" libisabelle_DUMMY*)
31.8 - "~~/src/Tools/isac/Interpret/Interpret"
31.9 + imports "~~/src/Tools/isac/Interpret/Interpret" (*"~~/libisabelle-protocol/libisabelle/protocol/Protocol"*) Protocol.Protocol
31.10
31.11 begin
31.12