equal
deleted
inserted
replaced
4 |
4 |
5 chapter {* Solutions to Most Exercises *} |
5 chapter {* Solutions to Most Exercises *} |
6 |
6 |
7 text {* \solution{fun:revsum} *} |
7 text {* \solution{fun:revsum} *} |
8 |
8 |
9 ML {* |
9 ML{*fun rev_sum t = |
10 fun rev_sum t = |
|
11 let |
10 let |
12 fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u |
11 fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u |
13 | dest_sum u = [u] |
12 | dest_sum u = [u] |
14 in |
13 in |
15 foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t) |
14 foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t) |
16 end; |
15 end *} |
17 *} |
|
18 |
16 |
19 text {* \solution{fun:makesum} *} |
17 text {* \solution{fun:makesum} *} |
20 |
18 |
21 ML {* |
19 ML{*fun make_sum t1 t2 = |
22 fun make_sum t1 t2 = |
20 HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *} |
23 HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) |
|
24 *} |
|
25 |
21 |
26 text {* \solution{ex:scancmts} *} |
22 text {* \solution{ex:scancmts} *} |
27 |
23 |
28 ML {* |
24 ML{*val any = Scan.one (Symbol.not_eof); |
29 val any = Scan.one (Symbol.not_eof); |
|
30 |
25 |
31 val scan_cmt = |
26 val scan_cmt = |
32 let |
27 let |
33 val begin_cmt = Scan.this_string "(*" |
28 val begin_cmt = Scan.this_string "(*" |
34 val end_cmt = Scan.this_string "*)" |
29 val end_cmt = Scan.this_string "*)" |
37 >> (enclose "(**" "**)" o implode) |
32 >> (enclose "(**" "**)" o implode) |
38 end |
33 end |
39 |
34 |
40 val scan_all = |
35 val scan_all = |
41 Scan.finite Symbol.stopper (Scan.repeat (scan_cmt || any)) |
36 Scan.finite Symbol.stopper (Scan.repeat (scan_cmt || any)) |
42 >> implode #> fst |
37 >> implode #> fst *} |
43 *} |
|
44 |
38 |
45 text {* |
39 text {* |
46 By using @{text "#> fst"} in the last line, the function |
40 By using @{text "#> fst"} in the last line, the function |
47 @{ML scan_all} retruns a string, instead of the pair a parser would |
41 @{ML scan_all} retruns a string, instead of the pair a parser would |
48 normally return. For example: |
42 normally return. For example: |