106
bdd82350cf22
renamed in the pdf all instances of cookbook to tutorial (in order to sound more serious)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1 |
(* Auxiliary antiquotations for the tutorial. *)
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
|
256
|
3 |
structure AntiquoteSetup =
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
struct
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
|
256
|
6 |
open OutputTutorial
|
|
7 |
|
112
|
8 |
(* functions for generating appropriate expressions *)
|
316
|
9 |
fun translate_string f str =
|
|
10 |
implode (map f (Symbol.explode str))
|
|
11 |
|
|
12 |
fun prefix_lines prfx txt =
|
|
13 |
map (fn s => prfx ^ s) (split_lines txt)
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
14 |
|
572
|
15 |
fun is_sep "\<dots>" = true
|
|
16 |
| is_sep s = Symbol.is_ascii_blank s;
|
|
17 |
|
|
18 |
fun scan_word sep =
|
|
19 |
Scan.many1 sep >> K NONE ||
|
|
20 |
Scan.many1 (fn s => not (sep s) andalso Symbol.not_eof s) >> (SOME o implode);
|
|
21 |
|
|
22 |
fun split_words sep = Symbol.scanner "Bad text" (Scan.repeat (scan_word sep) >> map_filter I);
|
|
23 |
|
|
24 |
fun explode_words sep = split_words sep o Symbol.explode;
|
|
25 |
|
|
26 |
fun match_string sep pat str =
|
|
27 |
let
|
|
28 |
fun match [] _ = true
|
|
29 |
| match (p :: ps) s =
|
|
30 |
size p <= size s andalso
|
|
31 |
(case try (unprefix p) s of
|
|
32 |
SOME s' => match ps s'
|
|
33 |
| NONE => match (p :: ps) (String.substring (s, 1, size s - 1)));
|
|
34 |
in match (explode_words sep pat) str end;
|
|
35 |
|
564
|
36 |
fun ml_with_vars' ys txt =
|
316
|
37 |
implode ["fn ", (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)), " => (", txt, ")"]
|
|
38 |
|
564
|
39 |
fun ml_with_vars ys src =
|
|
40 |
ML_Lex.read "fn " @ ML_Lex.read (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) @
|
|
41 |
ML_Lex.read " => (" @ src @ ML_Lex.read ")"
|
|
42 |
|
573
|
43 |
fun ml_with_struct (NONE) src = ML_Lex.read_source src
|
564
|
44 |
| ml_with_struct (SOME st) src =
|
573
|
45 |
ML_Lex.read ("let open " ^ st ^ " in ") @ ML_Lex.read_source src @ ML_Lex.read " end"
|
316
|
46 |
|
|
47 |
fun ml_val vs stru txt =
|
|
48 |
txt |> ml_with_struct stru
|
564
|
49 |
|> ml_with_vars vs
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
50 |
|
564
|
51 |
fun ml_pat pat lhs =
|
573
|
52 |
ML_Lex.read "val " @ ML_Lex.read_source pat @
|
564
|
53 |
ML_Lex.read " = " @
|
573
|
54 |
ML_Lex.read_source lhs
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
55 |
|
566
6103b0eadbf2
tuned parser for patterns in ML_response... antiquotations
Norbert Schirmer <norbert.schirmer@web.de>
diff
changeset
|
56 |
|
564
|
57 |
fun ml_struct src =
|
|
58 |
ML_Lex.read "functor DUMMY_FUNCTOR() = struct structure DUMMY = " @
|
573
|
59 |
ML_Lex.read_source src @
|
564
|
60 |
ML_Lex.read " end"
|
316
|
61 |
|
564
|
62 |
fun ml_type src =
|
573
|
63 |
ML_Lex.read "val _ = NONE : (" @ ML_Lex.read_source src @ ML_Lex.read ") option"
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
64 |
|
112
|
65 |
(* eval function *)
|
564
|
66 |
fun eval_fn ctxt prep exp =
|
|
67 |
ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of exp) (prep exp)
|
57
|
68 |
|
567
|
69 |
(* Evalate expression and convert result to a string *)
|
|
70 |
fun eval_response ctxt exp =
|
|
71 |
let
|
|
72 |
fun compute exp =
|
|
73 |
let
|
573
|
74 |
val input = ML_Lex.read "(let val r = " @ ML_Lex.read_source exp @
|
567
|
75 |
ML_Lex.read " in (raise ERROR (@{make_string} r); ()) end )"
|
|
76 |
val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of exp) input
|
|
77 |
in ""
|
|
78 |
end
|
|
79 |
in
|
|
80 |
(compute exp
|
|
81 |
handle ERROR s => s)
|
|
82 |
end
|
|
83 |
|
315
|
84 |
(* checks and prints a possibly open expressions, no index *)
|
|
85 |
|
564
|
86 |
fun output_ml ctxt (src, (vs, stru)) =
|
|
87 |
(eval_fn ctxt (ml_val vs stru) src;
|
573
|
88 |
output ctxt (split_lines (fst (Input.source_content src))))
|
564
|
89 |
|
|
90 |
val parser_ml = Scan.lift (Args.text_input --
|
426
|
91 |
(Scan.optional (Args.$$$ "for" |-- Parse.!!! (Scan.repeat1 Args.name)) [] --
|
|
92 |
Scan.option (Args.$$$ "in" |-- Parse.!!! Args.name)))
|
315
|
93 |
|
572
|
94 |
fun output_ml_response ignore_pat ctxt (src, opat) =
|
567
|
95 |
let
|
|
96 |
val res = eval_response ctxt src
|
572
|
97 |
val _ = writeln res
|
|
98 |
val cnt = YXML.content_of res
|
|
99 |
val pat = case opat of NONE => cnt
|
573
|
100 |
| SOME p => p |> fst o Input.source_content
|
572
|
101 |
val _ = if ignore_pat orelse Print_Mode.print_mode_active Latex.latexN orelse match_string is_sep pat cnt then ()
|
|
102 |
else error (cat_lines ["Substring:", pat, "not contained in:", cnt])
|
|
103 |
val out = if ignore_pat then cnt else pat
|
567
|
104 |
in
|
573
|
105 |
OutputTutorial.output ctxt ([fst (Input.source_content src)] @ [Library.prefix_lines "> " out])
|
567
|
106 |
end
|
|
107 |
|
316
|
108 |
(* checks and prints a single ML-item and produces an index entry *)
|
567
|
109 |
fun output_ml_ind ctxt (src, stru) =
|
|
110 |
let
|
573
|
111 |
val (txt,_) = Input.source_content src
|
567
|
112 |
in
|
|
113 |
(eval_fn ctxt (ml_val [] stru) src;
|
316
|
114 |
case (stru, Long_Name.base_name txt, Long_Name.qualifier txt) of
|
562
|
115 |
(NONE, _, "") => output_indexed ctxt {main = Code txt, minor = NoString} (split_lines txt)
|
449
|
116 |
| (NONE, bn, qn) => output_indexed ctxt {main = Code bn, minor = Struct qn} (split_lines txt)
|
|
117 |
| (SOME st, _, _) => output_indexed ctxt {main = Code txt, minor = Struct st} (split_lines txt))
|
567
|
118 |
end
|
112
|
119 |
|
567
|
120 |
val parser_ml_ind = Scan.lift (Args.text_input --
|
426
|
121 |
Scan.option (Args.$$$ "in" |-- Parse.!!! Args.name))
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
122 |
|
316
|
123 |
(* checks and prints structures *)
|
567
|
124 |
fun gen_output_struct outfn ctxt src =
|
|
125 |
let
|
573
|
126 |
val (txt, _) = Input.source_content src
|
567
|
127 |
in
|
|
128 |
(eval_fn ctxt ml_struct src;
|
316
|
129 |
outfn {main = Code txt, minor = Plain "structure"} (split_lines txt))
|
567
|
130 |
end
|
316
|
131 |
|
562
|
132 |
fun output_struct ctxt = gen_output_struct (K (output ctxt)) ctxt
|
|
133 |
fun output_struct_ind ctxt = gen_output_struct (output_indexed ctxt) ctxt
|
256
|
134 |
|
328
|
135 |
(* prints functors; no checks *)
|
567
|
136 |
fun gen_output_funct outfn src =
|
|
137 |
let
|
573
|
138 |
val (txt, _) = Input.source_content src
|
567
|
139 |
in
|
328
|
140 |
(outfn {main = Code txt, minor = Plain "functor"} (split_lines txt))
|
567
|
141 |
end
|
328
|
142 |
|
562
|
143 |
fun output_funct ctxt = gen_output_funct (K (output ctxt))
|
|
144 |
fun output_funct_ind ctxt = gen_output_funct (output_indexed ctxt)
|
328
|
145 |
|
316
|
146 |
(* checks and prints types *)
|
567
|
147 |
fun gen_output_type outfn ctxt src =
|
|
148 |
let
|
573
|
149 |
val (txt, _) = Input.source_content src
|
567
|
150 |
in
|
|
151 |
(eval_fn ctxt ml_type src;
|
316
|
152 |
outfn {main = Code txt, minor = Plain "type"} (split_lines txt))
|
567
|
153 |
end
|
316
|
154 |
|
562
|
155 |
fun output_type ctxt = gen_output_type (K (output ctxt)) ctxt
|
|
156 |
fun output_type_ind ctxt = gen_output_type (output_indexed ctxt) ctxt
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
157 |
|
566
6103b0eadbf2
tuned parser for patterns in ML_response... antiquotations
Norbert Schirmer <norbert.schirmer@web.de>
diff
changeset
|
158 |
val dots_pat = translate_string (fn "_" => "\<dots>" | s => s)
|
6103b0eadbf2
tuned parser for patterns in ML_response... antiquotations
Norbert Schirmer <norbert.schirmer@web.de>
diff
changeset
|
159 |
|
564
|
160 |
(* checks and expression against a result pattern *)
|
562
|
161 |
fun output_response ctxt (lhs, pat) =
|
564
|
162 |
(eval_fn ctxt (ml_pat pat) lhs;
|
573
|
163 |
output ctxt ((prefix_lines "" (fst (Input.source_content lhs))) @
|
|
164 |
(prefix_lines "> " (dots_pat (fst (Input.source_content pat))))))
|
171
|
165 |
|
|
166 |
(* checks the expressions, but does not check it against a result pattern *)
|
562
|
167 |
fun output_response_fake ctxt (lhs, pat) =
|
564
|
168 |
(eval_fn ctxt (ml_val [] NONE) lhs;
|
573
|
169 |
output ctxt ( (split_lines (fst (Input.source_content lhs))) @
|
|
170 |
(prefix_lines "> " (dots_pat (fst (Input.source_content pat))))))
|
112
|
171 |
|
|
172 |
(* checks the expressions, but does not check it against a result pattern *)
|
562
|
173 |
fun ouput_response_fake_both ctxt (lhs, pat) =
|
573
|
174 |
(output ctxt ((split_lines (fst (Input.source_content lhs))) @
|
|
175 |
(prefix_lines "> " (dots_pat (fst ((Input.source_content pat)))))))
|
171
|
176 |
|
567
|
177 |
val single_arg = Scan.lift (Args.text_input)
|
566
6103b0eadbf2
tuned parser for patterns in ML_response... antiquotations
Norbert Schirmer <norbert.schirmer@web.de>
diff
changeset
|
178 |
val two_args = Scan.lift (Args.text_input -- Args.text_input)
|
572
|
179 |
val maybe_two_args = Scan.lift (Args.text_input -- Scan.option Args.text_input)
|
317
d69214e47ef9
added an experimental antiquotation to replace eventually ML_response_fake
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
180 |
val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with" |-- Args.name))
|
112
|
181 |
|
471
|
182 |
val ml_setup =
|
567
|
183 |
Thy_Output.antiquotation_raw @{binding "ML"} parser_ml output_ml
|
572
|
184 |
#> Thy_Output.antiquotation_raw @{binding "ML_response"} maybe_two_args (output_ml_response false)
|
|
185 |
#> Thy_Output.antiquotation_raw @{binding "ML_response_ignore"} maybe_two_args (output_ml_response true)
|
562
|
186 |
#> Thy_Output.antiquotation_raw @{binding "ML_ind"} parser_ml_ind output_ml_ind
|
|
187 |
#> Thy_Output.antiquotation_raw @{binding "ML_type_ind"} single_arg output_type_ind
|
567
|
188 |
#> Thy_Output.antiquotation_raw @{binding "ML_structure_ind"} single_arg output_struct_ind
|
|
189 |
#> Thy_Output.antiquotation_raw @{binding "ML_functor_ind"} single_arg output_funct_ind
|
|
190 |
#> Thy_Output.antiquotation_raw @{binding "ML_matchresult"} two_args output_response
|
|
191 |
#> Thy_Output.antiquotation_raw @{binding "ML_matchresult_fake"} two_args output_response_fake
|
|
192 |
#> Thy_Output.antiquotation_raw @{binding "ML_matchresult_fake_both"} two_args ouput_response_fake_both
|
54
|
193 |
|
317
d69214e47ef9
added an experimental antiquotation to replace eventually ML_response_fake
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
194 |
(* checks whether a file exists in the Isabelle distribution *)
|
182
|
195 |
fun href_link txt =
|
|
196 |
let
|
562
|
197 |
val raw = I (* FIXME: Symbol.encode_raw *)
|
182
|
198 |
val path = "http://isabelle.in.tum.de/repos/isabelle/raw-file/tip/src/"
|
|
199 |
in
|
562
|
200 |
implode [raw "\\href{", raw path, raw txt, raw "}{", get_word txt, raw "}"]
|
182
|
201 |
end
|
|
202 |
|
567
|
203 |
fun check_file_exists _ src =
|
|
204 |
let
|
573
|
205 |
val (txt, _) = Input.source_content src
|
567
|
206 |
in
|
171
|
207 |
(if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt))
|
562
|
208 |
then Latex.string (href_link txt)
|
316
|
209 |
else error (implode ["Source file ", quote txt, " does not exist."]))
|
567
|
210 |
end
|
316
|
211 |
|
562
|
212 |
val ml_file_setup = Thy_Output.antiquotation_raw @{binding "ML_file"} single_arg check_file_exists
|
171
|
213 |
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
214 |
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
215 |
(* replaces the official subgoal antiquotation with one *)
|
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
216 |
(* that is closer to the actual output *)
|
562
|
217 |
|
303
05e6a33edef6
added an antiquotation for printing the raw proof state; polished the example about proof state
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
218 |
fun proof_state state =
|
539
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
219 |
(case try (Proof.goal o Toplevel.proof_of) state of
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
220 |
SOME {goal, ...} => goal
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
221 |
| _ => error "No proof state");
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
222 |
|
562
|
223 |
fun output_raw_goal_state ctxt _ =
|
539
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
224 |
let
|
562
|
225 |
val goals = proof_state (Toplevel.presentation_state ctxt)
|
|
226 |
val out = Syntax.string_of_term ctxt (Thm.prop_of goals)
|
539
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
227 |
in
|
562
|
228 |
output ctxt [out]
|
539
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
229 |
end
|
303
05e6a33edef6
added an antiquotation for printing the raw proof state; polished the example about proof state
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
230 |
|
471
|
231 |
val raw_goal_state_setup =
|
562
|
232 |
Thy_Output.antiquotation_raw @{binding "raw_goal_state"} (Scan.succeed ()) output_raw_goal_state
|
471
|
233 |
|
|
234 |
val setup =
|
|
235 |
ml_setup #>
|
|
236 |
ml_file_setup #>
|
|
237 |
raw_goal_state_setup
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
238 |
end;
|