Theory LLVM_Shallow
section ‹Shallow Embedding of LLVM Semantics›
theory LLVM_Shallow
imports Main
"Simple_Memory"
begin
subsection ‹Shallow Embedding of Values›
text ‹We use a type class to characterize types that can be injected into the value type.
We will instantiate this type class to obtain injections from types of shape
‹T = T×T | _ word | _ ptr›
Although, this type class can be instantiated by other types, those will not be accepted
by the code generator.
We also define a class ‹llvm_repv›, which additionally contains ‹unit›.
This is required for void functions, and if-the-else statements that produce no result.
Again, while this class might be instantiated for other types, those will be rejected
by the code generator.
›
class llvm_repv
class llvm_rep = llvm_repv +
fixes to_val :: "'a ⇒ llvm_val"
and from_val :: "llvm_val ⇒ 'a"
and struct_of :: "'a itself ⇒ llvm_struct"
and init :: 'a
assumes from_to_id[simp]: "from_val o to_val = id"
assumes to_from_id[simp]: "llvm_struct_of_val v = struct_of TYPE('a) ⟹ to_val (from_val v) = v"
assumes struct_of_matches[simp]: "llvm_struct_of_val (to_val x) = (struct_of TYPE('a))"
assumes init_zero: "to_val init = llvm_zero_initializer (struct_of TYPE('a))"
begin
lemma from_to_id'[simp]: "from_val (to_val x) = x"
using pointfree_idE[OF from_to_id] .
lemma "to_val x = to_val y ⟷ x=y"
by (metis from_to_id')
end
text ‹We use a phantom type to attach the type of the pointed to value to a pointer.
Note that we define pointers for any datatype. While it will always point to
representable datatypes, this enables easy ‹llvm_rep› instantiations for recursive structures
via pointers, such as linked list cells.
›