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 |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
structure AntiquoteSetup: sig end =
|
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 |
|
112
|
6 |
(* functions for generating appropriate expressions *)
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
fun ml_val_open (ys, xs) txt =
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
8 |
let fun ml_val_open_aux ys txt =
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
"fn " ^ (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ " => (" ^ txt ^ ")";
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
10 |
in
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
11 |
(case xs of
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
12 |
[] => ml_val_open_aux ys txt
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
| _ => ml_val_open_aux ys ("let open " ^ (space_implode " " xs) ^ " in " ^ txt ^ " end"))
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
14 |
end;
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
15 |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
16 |
fun ml_val txt = ml_val_open ([],[]) txt;
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
17 |
|
112
|
18 |
fun ml_pat (lhs, pat) =
|
51
|
19 |
let
|
|
20 |
val pat' = implode (map (fn "\\<dots>" => "_" | s => s) (Symbol.explode pat))
|
112
|
21 |
in "val " ^ pat' ^ " = " ^ lhs end;
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
22 |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
23 |
fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end";
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
24 |
fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option";
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
25 |
|
112
|
26 |
(* eval function *)
|
171
|
27 |
fun eval_fn ctxt exp =
|
|
28 |
ML_Context.eval_in (SOME ctxt) false Position.none exp
|
57
|
29 |
|
112
|
30 |
(* string functions *)
|
103
|
31 |
fun string_explode str txt =
|
|
32 |
map (fn s => str ^ s) (space_explode "\n" txt)
|
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 |
val transform_cmts_str =
|
|
35 |
Source.of_string
|
|
36 |
#> ML_Lex.source
|
|
37 |
#> Source.exhaust
|
|
38 |
#> Chunks.transform_cmts
|
|
39 |
#> implode
|
|
40 |
#> string_explode "";
|
|
41 |
|
|
42 |
(* output function *)
|
171
|
43 |
fun output_fn txt = Chunks.output (map Pretty.str txt)
|
112
|
44 |
|
|
45 |
(* checks and prints open expressions *)
|
171
|
46 |
fun output_ml {context = ctxt, ...} (txt, ovars) =
|
|
47 |
(eval_fn ctxt (ml_val_open ovars txt);
|
|
48 |
output_fn (transform_cmts_str txt))
|
112
|
49 |
|
171
|
50 |
val parser_ml = Scan.lift (Args.name --
|
|
51 |
(Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
|
|
52 |
Scan.optional (Args.$$$ "in" |-- OuterParse.!!! (Scan.repeat1 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
|
53 |
|
112
|
54 |
(* checks and prints types and structures *)
|
171
|
55 |
fun output_exp ml {context = ctxt, ...} txt =
|
|
56 |
(eval_fn ctxt (ml txt);
|
|
57 |
output_fn (string_explode "" txt))
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
58 |
|
112
|
59 |
(* checks and expression agains a result pattern *)
|
171
|
60 |
fun output_response {context = ctxt, ...} (lhs, pat) =
|
|
61 |
(eval_fn ctxt (ml_pat (lhs, pat));
|
|
62 |
output_fn ((string_explode "" lhs) @ (string_explode "> " pat)))
|
|
63 |
|
|
64 |
(* checks the expressions, but does not check it against a result pattern *)
|
|
65 |
fun output_response_fake {context = ctxt, ...} (lhs, pat) =
|
|
66 |
(eval_fn ctxt (ml_val lhs);
|
|
67 |
output_fn ((string_explode "" lhs) @ (string_explode "> " pat)))
|
112
|
68 |
|
|
69 |
(* checks the expressions, but does not check it against a result pattern *)
|
171
|
70 |
fun ouput_response_fake_both _ (lhs, pat) =
|
|
71 |
output_fn ((string_explode "" lhs) @ (string_explode "> " pat))
|
|
72 |
|
|
73 |
val single_arg = Scan.lift (Args.name)
|
|
74 |
val two_args = Scan.lift (Args.name -- Args.name)
|
112
|
75 |
|
171
|
76 |
val _ = ThyOutput.antiquotation "ML" parser_ml output_ml
|
|
77 |
val _ = ThyOutput.antiquotation "ML_type" single_arg (output_exp ml_type)
|
|
78 |
val _ = ThyOutput.antiquotation "ML_struct" single_arg (output_exp ml_struct)
|
|
79 |
val _ = ThyOutput.antiquotation "ML_response" two_args output_response
|
|
80 |
val _ = ThyOutput.antiquotation "ML_response_fake" two_args output_response_fake
|
|
81 |
val _ = ThyOutput.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both
|
54
|
82 |
|
182
|
83 |
fun href_link txt =
|
|
84 |
let
|
|
85 |
val raw = Symbol.encode_raw
|
|
86 |
val path = "http://isabelle.in.tum.de/repos/isabelle/raw-file/tip/src/"
|
|
87 |
in
|
|
88 |
(raw "\\href{") ^ (raw path) ^ (raw txt) ^ (raw "}{") ^ txt ^ (raw "}")
|
|
89 |
end
|
|
90 |
|
112
|
91 |
(* checks whether a file exists in the Isabelle distribution *)
|
171
|
92 |
fun check_file_exists _ txt =
|
|
93 |
(if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt))
|
182
|
94 |
then output_fn [href_link txt]
|
171
|
95 |
else error ("Source file " ^ (quote txt) ^ " does not exist."))
|
|
96 |
|
|
97 |
val _ = ThyOutput.antiquotation "ML_file" single_arg check_file_exists
|
|
98 |
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
99 |
|
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
|
100 |
(* 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
|
101 |
(* that is closer to the actual output *)
|
171
|
102 |
fun output_goals {state = node, ...} _ =
|
|
103 |
let
|
98
0a5c95f4d70c
calculated the exact number of goals in the subgoal antiquotation
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
104 |
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
|
105 |
| subgoals 1 = "goal (1 subgoal):"
|
171
|
106 |
| subgoals n = "goal (" ^ string_of_int n ^ " subgoals):"
|
|
107 |
|
|
108 |
fun proof_state state =
|
|
109 |
(case try Toplevel.proof_of state of
|
|
110 |
SOME prf => prf
|
|
111 |
| _ => error "No proof state")
|
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
|
112 |
|
98
0a5c95f4d70c
calculated the exact number of goals in the subgoal antiquotation
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
113 |
val state = proof_state node;
|
209
|
114 |
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
|
115 |
|
0a5c95f4d70c
calculated the exact number of goals in the subgoal antiquotation
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
116 |
val {prop, ...} = rep_thm (Proof.get_goal state |> snd |> snd);
|
0a5c95f4d70c
calculated the exact number of goals in the subgoal antiquotation
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
117 |
val (As, B) = Logic.strip_horn prop;
|
171
|
118 |
val output = (case (length As) of
|
209
|
119 |
0 => [goals]
|
|
120 |
| 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
|
121 |
in
|
171
|
122 |
ThyOutput.output 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
|
123 |
end
|
165
|
124 |
|
171
|
125 |
val _ = ThyOutput.antiquotation "subgoals" (Scan.succeed ()) output_goals
|
209
|
126 |
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
127 |
end;
|