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 |
|
316
|
15 |
fun ml_with_vars ys txt =
|
|
16 |
implode ["fn ", (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)), " => (", txt, ")"]
|
|
17 |
|
|
18 |
fun ml_with_struct (NONE) txt = txt
|
|
19 |
| ml_with_struct (SOME st) txt = implode ["let open ", st, " in ", txt, " end"]
|
|
20 |
|
|
21 |
fun ml_val vs stru txt =
|
|
22 |
txt |> ml_with_struct stru
|
|
23 |
|> 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
|
24 |
|
112
|
25 |
fun ml_pat (lhs, pat) =
|
316
|
26 |
implode ["val ", translate_string (fn "\<dots>" => "_" | s => s) pat, " = ", lhs]
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
27 |
|
316
|
28 |
fun ml_struct txt =
|
|
29 |
implode ["functor DUMMY_FUNCTOR() = struct structure DUMMY = ", txt, " end"]
|
|
30 |
|
|
31 |
fun ml_type txt =
|
|
32 |
implode ["val _ = NONE : (", txt, ") option"];
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
33 |
|
112
|
34 |
(* eval function *)
|
171
|
35 |
fun eval_fn ctxt exp =
|
438
|
36 |
ML_Context.eval_text_in (SOME ctxt) false Position.none exp
|
57
|
37 |
|
315
|
38 |
(* checks and prints a possibly open expressions, no index *)
|
316
|
39 |
fun output_ml {context = ctxt, ...} (txt, (vs, stru)) =
|
|
40 |
(eval_fn ctxt (ml_val vs stru txt);
|
449
|
41 |
output ctxt (split_lines txt))
|
315
|
42 |
|
|
43 |
val parser_ml = Scan.lift (Args.name --
|
426
|
44 |
(Scan.optional (Args.$$$ "for" |-- Parse.!!! (Scan.repeat1 Args.name)) [] --
|
|
45 |
Scan.option (Args.$$$ "in" |-- Parse.!!! Args.name)))
|
315
|
46 |
|
316
|
47 |
(* checks and prints a single ML-item and produces an index entry *)
|
|
48 |
fun output_ml_ind {context = ctxt, ...} (txt, stru) =
|
|
49 |
(eval_fn ctxt (ml_val [] stru txt);
|
|
50 |
case (stru, Long_Name.base_name txt, Long_Name.qualifier txt) of
|
449
|
51 |
(NONE, bn, "") => output_indexed ctxt {main = Code txt, minor = NoString} (split_lines txt)
|
|
52 |
| (NONE, bn, qn) => output_indexed ctxt {main = Code bn, minor = Struct qn} (split_lines txt)
|
|
53 |
| (SOME st, _, _) => output_indexed ctxt {main = Code txt, minor = Struct st} (split_lines txt))
|
112
|
54 |
|
315
|
55 |
val parser_ml_ind = Scan.lift (Args.name --
|
426
|
56 |
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
|
57 |
|
316
|
58 |
(* checks and prints structures *)
|
449
|
59 |
fun gen_output_struct outfn ctxt txt =
|
316
|
60 |
(eval_fn ctxt (ml_struct txt);
|
|
61 |
outfn {main = Code txt, minor = Plain "structure"} (split_lines txt))
|
|
62 |
|
449
|
63 |
fun output_struct {context = ctxt, ...} = gen_output_struct (K (output ctxt)) ctxt
|
|
64 |
fun output_struct_ind {context = ctxt, ...} = gen_output_struct (output_indexed ctxt) ctxt
|
256
|
65 |
|
328
|
66 |
(* prints functors; no checks *)
|
449
|
67 |
fun gen_output_funct outfn txt =
|
328
|
68 |
(outfn {main = Code txt, minor = Plain "functor"} (split_lines txt))
|
|
69 |
|
449
|
70 |
fun output_funct {context = ctxt, ...} = gen_output_funct (K (output ctxt))
|
|
71 |
fun output_funct_ind {context = ctxt, ...} = gen_output_funct (output_indexed ctxt)
|
328
|
72 |
|
316
|
73 |
(* checks and prints types *)
|
449
|
74 |
fun gen_output_type outfn ctxt txt =
|
316
|
75 |
(eval_fn ctxt (ml_type txt);
|
|
76 |
outfn {main = Code txt, minor = Plain "type"} (split_lines txt))
|
|
77 |
|
449
|
78 |
fun output_type {context = ctxt, ...} = gen_output_type (K (output ctxt)) ctxt
|
|
79 |
fun output_type_ind {context = 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
|
80 |
|
112
|
81 |
(* checks and expression agains a result pattern *)
|
171
|
82 |
fun output_response {context = ctxt, ...} (lhs, pat) =
|
|
83 |
(eval_fn ctxt (ml_pat (lhs, pat));
|
356
|
84 |
write_file_ml_blk lhs (ProofContext.theory_of ctxt);
|
449
|
85 |
output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat)))
|
171
|
86 |
|
|
87 |
(* checks the expressions, but does not check it against a result pattern *)
|
|
88 |
fun output_response_fake {context = ctxt, ...} (lhs, pat) =
|
316
|
89 |
(eval_fn ctxt (ml_val [] NONE lhs);
|
356
|
90 |
write_file_ml_blk lhs (ProofContext.theory_of ctxt);
|
449
|
91 |
output ctxt ((split_lines lhs) @ (prefix_lines "> " pat)))
|
112
|
92 |
|
|
93 |
(* checks the expressions, but does not check it against a result pattern *)
|
449
|
94 |
fun ouput_response_fake_both {context = ctxt, ...} (lhs, pat) =
|
|
95 |
output ctxt ((split_lines lhs) @ (prefix_lines "> " pat))
|
171
|
96 |
|
|
97 |
val single_arg = Scan.lift (Args.name)
|
|
98 |
val two_args = Scan.lift (Args.name -- Args.name)
|
317
d69214e47ef9
added an experimental antiquotation to replace eventually ML_response_fake
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
99 |
val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with" |-- Args.name))
|
112
|
100 |
|
470
|
101 |
val _ = Thy_Output.antiquotation @{binding "ML"} parser_ml output_ml
|
|
102 |
val _ = Thy_Output.antiquotation @{binding "ML_ind"} parser_ml_ind output_ml_ind
|
|
103 |
val _ = Thy_Output.antiquotation @{binding "ML_type"} single_arg output_type
|
|
104 |
val _ = Thy_Output.antiquotation @{binding "ML_type_ind"} single_arg output_type_ind
|
|
105 |
val _ = Thy_Output.antiquotation @{binding "ML_struct"} single_arg output_struct
|
|
106 |
val _ = Thy_Output.antiquotation @{binding "ML_struct_ind"} single_arg output_struct_ind
|
|
107 |
val _ = Thy_Output.antiquotation @{binding "ML_funct"} single_arg output_funct
|
|
108 |
val _ = Thy_Output.antiquotation @{binding "ML_funct_ind"} single_arg output_funct_ind
|
|
109 |
val _ = Thy_Output.antiquotation @{binding "ML_response"} two_args output_response
|
|
110 |
val _ = Thy_Output.antiquotation @{binding "ML_response_fake"} two_args output_response_fake
|
|
111 |
val _ = Thy_Output.antiquotation @{binding "ML_response_fake_both"} two_args ouput_response_fake_both
|
54
|
112 |
|
317
d69214e47ef9
added an experimental antiquotation to replace eventually ML_response_fake
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
113 |
(* FIXME: experimental *)
|
d69214e47ef9
added an experimental antiquotation to replace eventually ML_response_fake
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
114 |
fun ml_eq (lhs, pat, eq) =
|
d69214e47ef9
added an experimental antiquotation to replace eventually ML_response_fake
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
115 |
implode ["val true = ((", eq, ") (", lhs, ",", pat, "))"]
|
d69214e47ef9
added an experimental antiquotation to replace eventually ML_response_fake
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
116 |
|
d69214e47ef9
added an experimental antiquotation to replace eventually ML_response_fake
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
117 |
fun output_response_eq {context = ctxt, ...} ((lhs, pat), eq) =
|
d69214e47ef9
added an experimental antiquotation to replace eventually ML_response_fake
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
118 |
(case eq of
|
d69214e47ef9
added an experimental antiquotation to replace eventually ML_response_fake
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
119 |
NONE => eval_fn ctxt (ml_pat (lhs, pat))
|
d69214e47ef9
added an experimental antiquotation to replace eventually ML_response_fake
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
120 |
| SOME e => eval_fn ctxt (ml_eq (lhs, pat, e));
|
449
|
121 |
output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat)))
|
317
d69214e47ef9
added an experimental antiquotation to replace eventually ML_response_fake
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
122 |
|
470
|
123 |
val _ = Thy_Output.antiquotation @{binding "ML_response_eq"} test output_response_eq
|
317
d69214e47ef9
added an experimental antiquotation to replace eventually ML_response_fake
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
124 |
|
d69214e47ef9
added an experimental antiquotation to replace eventually ML_response_fake
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
125 |
(* checks whether a file exists in the Isabelle distribution *)
|
182
|
126 |
fun href_link txt =
|
|
127 |
let
|
|
128 |
val raw = Symbol.encode_raw
|
|
129 |
val path = "http://isabelle.in.tum.de/repos/isabelle/raw-file/tip/src/"
|
|
130 |
in
|
316
|
131 |
implode [raw "\\href{", raw path, raw txt, raw "}{", txt, raw "}"]
|
182
|
132 |
end
|
|
133 |
|
449
|
134 |
fun check_file_exists {context = ctxt, ...} txt =
|
171
|
135 |
(if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt))
|
449
|
136 |
then output ctxt [href_link txt]
|
316
|
137 |
else error (implode ["Source file ", quote txt, " does not exist."]))
|
|
138 |
|
470
|
139 |
val _ = Thy_Output.antiquotation @{binding "ML_file"} single_arg check_file_exists
|
171
|
140 |
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
141 |
|
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
|
142 |
(* 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
|
143 |
(* that is closer to the actual output *)
|
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
|
144 |
fun proof_state state =
|
05e6a33edef6
added an antiquotation for printing the raw proof state; polished the example about proof state
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
145 |
(case try Toplevel.proof_of state of
|
05e6a33edef6
added an antiquotation for printing the raw proof state; polished the example about proof state
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
146 |
SOME prf => prf
|
05e6a33edef6
added an antiquotation for printing the raw proof state; polished the example about proof state
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
147 |
| _ => error "No proof state")
|
05e6a33edef6
added an antiquotation for printing the raw proof state; polished the example about proof state
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
148 |
|
449
|
149 |
fun output_goals {state = node, context = ctxt, ...} _ =
|
171
|
150 |
let
|
98
0a5c95f4d70c
calculated the exact number of goals in the subgoal antiquotation
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
151 |
fun subgoals 0 = ""
|
96
018bfa718982
(re)defined the document antiquotation @subgoal in order to be closer to what is actually printed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
152 |
| subgoals 1 = "goal (1 subgoal):"
|
171
|
153 |
| subgoals n = "goal (" ^ string_of_int n ^ " subgoals):"
|
|
154 |
|
98
0a5c95f4d70c
calculated the exact number of goals in the subgoal antiquotation
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
155 |
val state = proof_state node;
|
209
|
156 |
val goals = Pretty.chunks (Proof.pretty_goals false state);
|
98
0a5c95f4d70c
calculated the exact number of goals in the subgoal antiquotation
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
157 |
|
367
|
158 |
val {prop, ...} = (rep_thm o #goal o Proof.goal) state;
|
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
|
159 |
val (As, _) = Logic.strip_horn prop;
|
171
|
160 |
val output = (case (length As) of
|
209
|
161 |
0 => [goals]
|
|
162 |
| n => [Pretty.str (subgoals n), goals])
|
96
018bfa718982
(re)defined the document antiquotation @subgoal in order to be closer to what is actually printed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
163 |
in
|
449
|
164 |
Thy_Output.output ctxt output
|
96
018bfa718982
(re)defined the document antiquotation @subgoal in order to be closer to what is actually printed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
165 |
end
|
165
|
166 |
|
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
|
167 |
fun output_raw_goal_state {state = node, context = ctxt, ...} _ =
|
05e6a33edef6
added an antiquotation for printing the raw proof state; polished the example about proof state
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
168 |
let
|
05e6a33edef6
added an antiquotation for printing the raw proof state; polished the example about proof state
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
169 |
val state = proof_state node;
|
367
|
170 |
val goals = (#goal o Proof.goal) state;
|
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
|
171 |
|
05e6a33edef6
added an antiquotation for printing the raw proof state; polished the example about proof state
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
172 |
val output = [Pretty.str (Syntax.string_of_term ctxt (prop_of goals))]
|
05e6a33edef6
added an antiquotation for printing the raw proof state; polished the example about proof state
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
173 |
val _ = tracing (Syntax.string_of_term ctxt (prop_of goals))
|
05e6a33edef6
added an antiquotation for printing the raw proof state; polished the example about proof state
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
174 |
val _ = tracing (Pretty.string_of (Pretty.str (Syntax.string_of_term ctxt (prop_of goals))))
|
05e6a33edef6
added an antiquotation for printing the raw proof state; polished the example about proof state
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
175 |
in
|
449
|
176 |
Thy_Output.output ctxt output
|
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
|
177 |
end
|
05e6a33edef6
added an antiquotation for printing the raw proof state; polished the example about proof state
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
178 |
|
470
|
179 |
val _ = Thy_Output.antiquotation @{binding "subgoals"} (Scan.succeed ()) output_goals
|
|
180 |
val _ = Thy_Output.antiquotation @{binding "raw_goal_state"} (Scan.succeed ()) output_raw_goal_state
|
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
|
181 |
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
182 |
end;
|