10 end; |
10 end; |
11 |
11 |
12 structure More_Antiquote : MORE_ANTIQUOTE = |
12 structure More_Antiquote : MORE_ANTIQUOTE = |
13 struct |
13 struct |
14 |
14 |
15 structure O = ThyOutput; |
|
16 |
|
17 (* printing typewriter lines *) |
15 (* printing typewriter lines *) |
18 |
16 |
19 fun typewriter s = |
17 fun typewriter s = |
20 let |
18 let |
21 val parse = Scan.repeat |
19 val parse = Scan.repeat |
22 (Scan.this_string "\n" |-- Scan.succeed "\\\\\n\\hspace*{0pt}" |
20 (Scan.this_string "\n" |-- Scan.succeed "\\\\\n\\hspace*{0pt}" |
23 || (Scan.this_string " " |
21 || (Scan.this_string " " |
24 || Scan.this_string "." |
22 || Scan.this_string "." |
25 || Scan.this_string "," |
23 || Scan.this_string "," |
26 || Scan.this_string ":" |
24 || Scan.this_string ":" |
27 || Scan.this_string ";" |
25 || Scan.this_string ";" |
28 || Scan.this_string "\"" |-- Scan.succeed "{\\char34}" |
26 || Scan.this_string "\"" |-- Scan.succeed "{\\char34}" |
64 #> Sign.extern_type (ProofContext.theory_of ctxt) |
62 #> Sign.extern_type (ProofContext.theory_of ctxt) |
65 #> pr_text; |
63 #> pr_text; |
66 |
64 |
67 in |
65 in |
68 |
66 |
69 val _ = O.add_commands |
67 val _ = ThyOutput.antiquotation "class" (Scan.lift Args.name) (pr_class o #context); |
70 [("class", ThyOutput.args (Scan.lift Args.name) (K pr_class)), |
68 val _ = ThyOutput.antiquotation "type" (Scan.lift Args.name) (pr_type o #context); |
71 ("type", ThyOutput.args (Scan.lift Args.name) (K pr_type))] |
|
72 |
69 |
73 end; |
70 end; |
74 |
71 |
75 |
72 |
76 (* code theorem antiquotation *) |
73 (* code theorem antiquotation *) |
94 val (_, funcgr) = Code_Wellsorted.make thy [const]; |
91 val (_, funcgr) = Code_Wellsorted.make thy [const]; |
95 fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm]; |
92 fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm]; |
96 val thms = Code_Wellsorted.eqns funcgr const |
93 val thms = Code_Wellsorted.eqns funcgr const |
97 |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE) |
94 |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE) |
98 |> map (holize o no_vars ctxt o AxClass.overload thy); |
95 |> map (holize o no_vars ctxt o AxClass.overload thy); |
99 in ThyOutput.output_list pretty_thm src ctxt thms end; |
96 in ThyOutput.output (ThyOutput.maybe_pretty_source (pretty_thm ctxt) src thms) end; |
100 |
97 |
101 in |
98 in |
102 |
99 |
103 val _ = O.add_commands |
100 val _ = ThyOutput.antiquotation "code_thms" Args.term |
104 [("code_thms", ThyOutput.args Args.term pretty_code_thm)]; |
101 (fn {source, context, ...} => pretty_code_thm source context); |
105 |
102 |
106 end; |
103 end; |
107 |
104 |
108 |
105 |
109 (* code antiquotation *) |
106 (* code antiquotation *) |
118 >> (fn tycos => fn thy => fn naming => map_filter (Code_Thingol.lookup_tyco naming o Sign.intern_type thy) tycos); |
115 >> (fn tycos => fn thy => fn naming => map_filter (Code_Thingol.lookup_tyco naming o Sign.intern_type thy) tycos); |
119 val parse_classes = Scan.lift (Args.parens (Args.$$$ "classes") |-- Scan.repeat1 Args.name) |
116 val parse_classes = Scan.lift (Args.parens (Args.$$$ "classes") |-- Scan.repeat1 Args.name) |
120 >> (fn classes => fn thy => fn naming => map_filter (Code_Thingol.lookup_class naming o Sign.intern_class thy) classes); |
117 >> (fn classes => fn thy => fn naming => map_filter (Code_Thingol.lookup_class naming o Sign.intern_class thy) classes); |
121 val parse_instances = Scan.lift (Args.parens (Args.$$$ "instances") |-- Scan.repeat1 (Args.name --| Args.$$$ "::" -- Args.name)) |
118 val parse_instances = Scan.lift (Args.parens (Args.$$$ "instances") |-- Scan.repeat1 (Args.name --| Args.$$$ "::" -- Args.name)) |
122 >> (fn insts => fn thy => fn naming => map_filter (Code_Thingol.lookup_instance naming o apsnd (Sign.intern_type thy) o apfst (Sign.intern_class thy) o swap) insts); |
119 >> (fn insts => fn thy => fn naming => map_filter (Code_Thingol.lookup_instance naming o apsnd (Sign.intern_type thy) o apfst (Sign.intern_class thy) o swap) insts); |
123 val parse_names = parse_consts || parse_types || parse_classes || parse_instances; |
120 val parse_names = parse_consts || parse_types || parse_classes || parse_instances; |
124 |
|
125 fun code_stmts src ctxt ((mk_cs, mk_stmtss), target) = |
|
126 Code_Target.code_of (ProofContext.theory_of ctxt) |
|
127 target "Example" (mk_cs (ProofContext.theory_of ctxt)) |
|
128 (fn naming => maps (fn f => f (ProofContext.theory_of ctxt) naming) mk_stmtss) |
|
129 |> typewriter; |
|
130 |
121 |
131 in |
122 in |
132 |
123 |
133 val _ = O.add_commands |
124 val _ = ThyOutput.antiquotation "code_stmts" |
134 [("code_stmts", O.args |
125 (parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name)) |
135 (parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name)) |
126 (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), target) => |
136 code_stmts)] |
127 let val thy = ProofContext.theory_of ctxt in |
137 |
128 Code_Target.code_of thy |
138 end |
129 target "Example" (mk_cs thy) |
|
130 (fn naming => maps (fn f => f thy naming) mk_stmtss) |
|
131 |> typewriter |
|
132 end); |
139 |
133 |
140 end; |
134 end; |
|
135 |
|
136 end; |