Stream: Beginner Questions

Topic: Executing Imperative-HOL

Mark Wassell (Apr 05 2024 at 07:06):

Is it possible to use the 'value' command on Imperative-HOL constructs? I have:

theory ImpPlay
  imports "HOL-Imperative_HOL.Imperative_HOL_ex"
begin

value "execute example Heap.empty"

end

but the value line gives:

exception Fail raised (line 211 of "generated code"): Heap_Monad.execute

Mathias Fleury (Apr 05 2024 at 10:13):

I think that execution only makes sense when exporting the code and executing it outside. The alternative is to do it with simp:

lemma "execute example Heap.empty = A"
  apply (simp add: example_def Array.make_def execute_bind_case execute_heap Array.alloc_def Let_def
      Imperative_Reverse.rev.simps execute_upd Imperative_Reverse.swap.simps execute_nth Array.length_def
      split: option.splits)

(Yes this is annoying, but the entire point of Imperative_HOL is the imperative execution that you cannot do directly)

Manuel Eberl (Apr 05 2024 at 12:41):

The following does work for example being some expression of type 'a heap:

ML_val ‹@{code example} ()›

Of course, that gives the result as an ML value and not a HOL term, but that might be enough. For non-"heapy" result types one could probably wrap the result in a Code_Evaluation.term_of and then interpret the resulting ML value as a HOL value, similar to what the value command normally does. But I'm not sure how that would work for e.g. functions that return an array or a pointer. It probably doesn't.

Manuel Eberl (Apr 05 2024 at 12:51):

Well I guess you can just convert that array to a list to print it… The following kind of works:

definition "example2 = do {
    a ← Array.of_list ([42, 2, 3, 5, 0, 1705, 8, 3, 15] :: nat list);
    xs ← Array.freeze a;
    return (Code_Evaluation.term_of xs)
  }"


ML ‹
  val _ = @{code example2} () |> Syntax.pretty_term @{context} |> Pretty.writeln
›

Output:

[nat_of_integer 42, nat_of_integer 2,
 nat_of_integer 3, nat_of_integer 5,
 nat_of_integer 0, nat_of_integer 1705,
 nat_of_integer 8, nat_of_integer 3,
 nat_of_integer 15]

Manuel Eberl (Apr 05 2024 at 12:52):

Not quite as nice at what value would give you because the code_proc rules are not applied. One could probably fix up something that does this a bit more automatically and wrap it in a value_imp command or something. Or perhaps even an alternative evaluator for the normal value command.

Manuel Eberl (Apr 05 2024 at 12:53):

Quite possibly one could even tweak the normal value command to do something like this.

Last updated: Dec 21 2024 at 16:20 UTC