Chengsong Tan (Jul 16 2023 at 20:36): Chengsong Tan (Jul 16 2023 at 20:36):Hi,
Suppose I have defined a function id_to_nat in Isabelle on a finite datatype like this:
datatype DeviceID = Dev1 | Dev2
fun id_to_nat :: "DeviceID ⇒ nat" where
"id_to_nat Dev1 = 0"
| "id_to_nat Dev2 = 1"
value "id_to_nat"
The evaluation of id_to_nat prints out as "_", despite it being a quite simple mapping.
I want to be able to see the content of the mapping id_to_nat, somewhat like
id_to_nat :: "DeviceID => nat": [Dev1-->0], [Dev2 -->1]
In my actual project a map is preferred over two lists so using lists to represent the actual version of "id_to_nat" is impossible. Any suggestions on circumventions/workarounds?
Thanks a lot,
Chengsong
Mathias Fleury (Jul 17 2023 at 04:08):It is not clear why you would want that. Ctrl-click shows the definition… Which gives you the entire information needed
Mathias Fleury (Jul 17 2023 at 04:09):Or, if you want to see the SML Code, you need to do
export_code id_to_nat in SML
In this case you can actually do:
lemma [code]: ‹id_to_nat = (λx. case x of Dev1 ⇒ 0 | Dev2 ⇒ 1)›
by (auto intro!: ext split: DeviceID.split)
value "id_to_nat x"
Mathias Fleury said:
It is not clear why you would want that. Ctrl-click shows the definition… Which gives you the entire information needed
Imagine that mapping changes as a part of a large record state.
For that, the function is used as not a definition but a structured way of expressing some system state.
And we want to be able to inspect that state conveniently by printing it out.
For example, the actual finite-domain function record I am trying to print will result in something like this:
⦇hostcache = ⦇CLEntry.content = Some 0, block_state = Modified⦈, devclmap = _, reqs = _, snpresps = _, dthdatas = _, snoops = _, reqresps = _,
htddatas = _, program = _, counter = 2, registers = _, devtrackers = _, hosttracker = _, issuedEvents = _, eventsToIssue = _⦈
And there's no way to inspect it like you did for id_to_nat, as the maps such as devclmap is constantly changing as part of a model representing the possible next states of a (cache coherent multicore) system under a bunch of non-deterministic transition rules.
The whole point is being able to inspect the next states without having to explicitly know (and tediously write down) what they are.
I have attached the theory file related to this (bottom of file is where attempt was made).
Chengsong Tan (Jul 18 2023 at 13:33):If direct printing maps not possible, I guess all I need is a "printf" function in Isabelle to print ints and strings to the proof state output console. That way I can write a pretty printer in Isabelle myself.
Last updated: May 02 2024 at 01:06 UTC