equal
deleted
inserted
replaced
22 text {* \solution{ex:scancmts} *} |
22 text {* \solution{ex:scancmts} *} |
23 |
23 |
24 ML{*val any = Scan.one (Symbol.not_eof) |
24 ML{*val any = Scan.one (Symbol.not_eof) |
25 |
25 |
26 val scan_cmt = |
26 val scan_cmt = |
27 let |
27 let |
28 val begin_cmt = Scan.this_string "(*" |
28 val begin_cmt = Scan.this_string "(*" |
29 val end_cmt = Scan.this_string "*)" |
29 val end_cmt = Scan.this_string "*)" |
30 in |
30 in |
31 begin_cmt |-- Scan.repeat (Scan.unless end_cmt any) --| end_cmt |
31 begin_cmt |-- Scan.repeat (Scan.unless end_cmt any) --| end_cmt |
32 >> (enclose "(**" "**)" o implode) |
32 >> (enclose "(**" "**)" o implode) |
33 end |
33 end |
34 |
34 |
35 val parser = Scan.repeat (scan_cmt || any) |
35 val parser = Scan.repeat (scan_cmt || any) |
36 |
36 |
37 val scan_all = |
37 val scan_all = |
38 Scan.finite Symbol.stopper parser >> implode #> fst *} |
38 Scan.finite Symbol.stopper parser >> implode #> fst *} |
39 |
39 |
40 text {* |
40 text {* |
41 By using @{text "#> fst"} in the last line, the function |
41 By using @{text "#> fst"} in the last line, the function |
42 @{ML scan_all} retruns a string, instead of the pair a parser would |
42 @{ML scan_all} retruns a string, instead of the pair a parser would |
43 normally return. For example: |
43 normally return. For example: |
93 \end{minipage}\bigskip |
93 \end{minipage}\bigskip |
94 *}(*<*)oops(*>*) |
94 *}(*<*)oops(*>*) |
95 |
95 |
96 text {* \solution{ex:addconversion} *} |
96 text {* \solution{ex:addconversion} *} |
97 |
97 |
|
98 text {* |
|
99 The following code assumes the function @{ML dest_sum} from the previous |
|
100 exercise. |
|
101 *} |
|
102 |
|
103 |
98 ML{*fun add_simple_conv ctxt ctrm = |
104 ML{*fun add_simple_conv ctxt ctrm = |
99 let |
105 let |
100 val trm = Thm.term_of ctrm |
106 val trm = Thm.term_of ctrm |
101 in |
107 in |
102 get_sum_thm ctxt trm (dest_sum trm) |
108 get_sum_thm ctxt trm (dest_sum trm) |
120 (Conv.params_conv ~1 (fn ctxt => |
126 (Conv.params_conv ~1 (fn ctxt => |
121 (Conv.prems_conv ~1 (add_conv ctxt) then_conv |
127 (Conv.prems_conv ~1 (add_conv ctxt) then_conv |
122 Conv.concl_conv ~1 (add_conv ctxt))) ctxt) i |
128 Conv.concl_conv ~1 (add_conv ctxt))) ctxt) i |
123 end)*} |
129 end)*} |
124 |
130 |
|
131 text {* |
|
132 A test case is as follows |
|
133 *} |
|
134 |
125 lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)" |
135 lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)" |
126 apply(tactic {* add_tac 1 *})? |
136 apply(tactic {* add_tac 1 *})? |
127 txt {* |
137 txt {* |
128 where the simproc produces the goal state |
138 where the conversion produces the goal state |
129 |
139 |
130 \begin{minipage}{\textwidth} |
140 \begin{minipage}{\textwidth} |
131 @{subgoals [display]} |
141 @{subgoals [display]} |
132 \end{minipage}\bigskip |
142 \end{minipage}\bigskip |
133 *}(*<*)oops(*>*) |
143 *}(*<*)oops(*>*) |