theory Solutions+
−
imports Base+
−
begin+
−
+
−
chapter {* Solutions to Most Exercises *}+
−
+
−
text {* \solution{fun:revsum} *}+
−
+
−
ML{*fun rev_sum t =+
−
let+
−
 fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u+
−
   | dest_sum u = [u]+
−
 in+
−
   foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t)+
−
 end *}+
−
+
−
text {* \solution{fun:makesum} *}+
−
+
−
ML{*fun make_sum t1 t2 =+
−
    HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *}+
−
+
−
text {* \solution{ex:scancmts} *}+
−
+
−
ML{*val any = Scan.one (Symbol.not_eof);+
−
+
−
val scan_cmt =+
−
  let+
−
    val begin_cmt = Scan.this_string "(*" +
−
    val end_cmt = Scan.this_string "*)"+
−
  in+
−
   begin_cmt |-- Scan.repeat (Scan.unless end_cmt any) --| end_cmt +
−
    >> (enclose "(**" "**)" o implode)+
−
  end+
−
+
−
val scan_all =+
−
  Scan.finite Symbol.stopper (Scan.repeat (scan_cmt || any)) +
−
    >> implode #> fst *}+
−
+
−
text {*+
−
  By using @{text "#> fst"} in the last line, the function +
−
  @{ML scan_all} retruns a string, instead of the pair a parser would+
−
  normally return. For example:+
−
+
−
  @{ML_response [display,gray]+
−
"let+
−
   val input1 = (explode \"foo bar\")+
−
   val input2 = (explode \"foo (*test*) bar (*test*)\")+
−
 in+
−
   (scan_all input1, scan_all input2)+
−
 end"+
−
"(\"foo bar\",\"foo (**test**) bar (**test**)\")"}+
−
*}+
−
+
−
end+
−