Re: [isabelle] HOLogic.dest_string



Matthias Berg wrote:
> 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;

Dear Matthias,

type "term" is not type "term" -- the same structure is used for
different purposes.

Usually, "term" is used to represent abstract lambda terms inside the
system.  For these, the operations in Logic, HOLogic etc. are designed.
 But "term" are also (mis)used to reprent a certain stage during
parsing/printing.  It seems to be the "term"s your code receives stem
from that -- can you provide more context?

Cheers
	Florian
begin:vcard
fn:Florian Haftmann
n:Haftmann;Florian
org;quoted-printable;quoted-printable:Technische Universit=C3=A4t M=C3=BCnchen ;Institut f=C3=BCr Informatik, Lehrstuhl Software and Systems Engineering
adr;quoted-printable;quoted-printable:;;Boltzmannstra=C3=9Fe 3;M=C3=BCnchen;Bayern;85748;Deutschland
email;internet:florian.haftmann at informatik.tu-muenchen.de
title:M. Sc.
tel;work:(++49 89) 289 - 17300
note;quoted-printable:PGP available: =
	=0D=0A=
	http://www4.informatik.tu-muenchen.de/~haftmann/pgp/florian_haftmann_at_i=
	nformatik_tu_muenchen_de.pgp=0D=0A=
	
x-mozilla-html:FALSE
url:http://isabelle.in.tum.de/~haftmann
version:2.1
end:vcard

Attachment: signature.asc
Description: OpenPGP digital signature



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