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] "scan_all (explode \"foo bar\")" "\"foo bar\""}

  @{ML_response [display,gray] "scan_all (explode \"foo (*test*) bar (*test*)\")" 
                          "\"foo (**test**) bar (**test**)\""}

*}

end