Email Gateway (Aug 18 2022 at 11:38): Email Gateway (Aug 18 2022 at 11:38):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Matthias Berg wrote:
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
florian.haftmann.vcf
signature.asc
Email Gateway (Aug 18 2022 at 11:39):From: Amine Chaieb <chaieb@in.tum.de>
Dear Matthias,
Indeed Const ("List.list.Cons", _) is the right implementation and not
Const ("Cons", _). If you use the interactive mode and interpret e.g.
ML{* @{term "Cons"} *} in a theory higher than List.thy, you will see
that the output is indeed the first and not the second representation
above. To convince yourself, you can try to certify a term built by just
"Cons" e.g.
ML{* cterm_of @{theory} (Const("Cons",@{typ "'a list"}))*}
and you will see that Isabelle refuses this term as valid.
Terms (datatype term) as pointed out by Florian, is very liberal and
contains many "ill-formed" terms.
Hope this helps,
Amine.
Matthias Berg wrote:
Email Gateway (Aug 18 2022 at 11:47):From: Matthias Berg <berg@cs.uni-sb.de>
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
smime.p7s
Last updated: May 03 2024 at 04:19 UTC