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