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

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

                          "\"foo (**test**) bar (**test**)\""}

*}

end