1 theory Basic |
|
2 imports "../isabelle/2015/Protocol" |
|
3 begin |
|
4 |
|
5 operation_setup hello = \<open> |
|
6 {from_lib = Codec.string, |
|
7 to_lib = Codec.string, |
|
8 action = (fn data => "Hello " ^ data)}\<close> |
|
9 |
|
10 operation_setup (sequential, bracket) use_thys = \<open> |
|
11 {from_lib = Codec.list Codec.string, |
|
12 to_lib = Codec.unit, |
|
13 action = Thy_Info.use_thys o map (rpair Position.none)}\<close> |
|
14 |
|
15 text \<open> |
|
16 The read_term operation performs both parsing and checking at once, because we do not want to |
|
17 send back parsed, but un-checked terms to the JVM. They may contain weird position information |
|
18 which are difficult to get rid of and confuse the codecs. |
|
19 \<close> |
|
20 |
|
21 operation_setup read_term = \<open> |
|
22 {from_lib = Codec.triple Codec.string Codec.typ Codec.string, |
|
23 to_lib = Codec.option Codec.term, |
|
24 action = (fn (raw_term, typ, thy_name) => |
|
25 let |
|
26 val thy = Thy_Info.get_theory thy_name |
|
27 val ctxt = Proof_Context.init_global thy |
|
28 in |
|
29 try (Syntax.parse_term ctxt) raw_term |
|
30 |> Option.map (Type.constraint typ) |
|
31 |> Option.mapPartial (try (Syntax.check_term ctxt)) |
|
32 end)}\<close> |
|
33 |
|
34 operation_setup check_term = \<open> |
|
35 {from_lib = Codec.triple Codec.term Codec.typ Codec.string, |
|
36 to_lib = Codec.option Codec.term, |
|
37 action = (fn (term, typ, thy_name) => |
|
38 let |
|
39 val thy = Thy_Info.get_theory thy_name |
|
40 val ctxt = Proof_Context.init_global thy |
|
41 val term' = Type.constraint typ term |
|
42 in |
|
43 try (Syntax.check_term ctxt) term' |
|
44 end)}\<close> |
|
45 |
|
46 end |
|