[isabelle] HOLogic.dest_string



Hi,

I just tried to use the function HOLogic.dest_string and it seems that
its pattern matching does not work. The function dest_list tries to
match terms like  (Const ("List.list.Cons", _) $ t $ u) but I think it
should be just (Const ("Cons", _) $ t $ u). The same problem occurs in
other functions as well. The following works for me:

fun dest_nibble t =
  let fun err () = raise TERM ("dest_nibble", [t]) in
    (case try (unprefix "Nibble" o fst o Term.dest_Const) t of
      NONE => err ()
    | SOME c =>
        if size c <> 1 then err ()
        else if "0" <= c andalso c <= "9" then ord c - ord "0"
        else if "A" <= c andalso c <= "F" then ord c - ord "A" + 10
        else err ())
  end;
fun dest_char (Const ("Char", _) $ t $ u) =
      dest_nibble t * 16 + dest_nibble u
  | dest_char t = raise TERM ("dest_char", [t]);
fun dest_list (Const ("Nil", _)) = []
  | dest_list (Const ("Cons", _) $ t $ u) = t :: dest_list u
  | dest_list t = raise TERM ("dest_list", [t]);
val dest_string = implode o map (chr o dest_char) o dest_list;

Sincerely,
Matthias Berg


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.