# Theory Test

```theory Test
imports "HOL-Library.Code_Target_Numeral" BinomialHeap SkewBinomialHeap
begin
text ‹
This theory is included into teh session, in order to
catch problems with code generation.
›

definition
sh_empty :: "unit ⇒ ('a,nat) SkewBinomialHeap"
where "sh_empty u ≡ SkewBinomialHeap.empty"
definition
sh_findMin :: "('a,nat) SkewBinomialHeap ⇒ _"
where "sh_findMin ≡ SkewBinomialHeap.findMin"
definition
sh_deleteMin :: "('a,nat) SkewBinomialHeap ⇒ ('a,nat) SkewBinomialHeap"
where "sh_deleteMin ≡ SkewBinomialHeap.deleteMin"
definition
sh_insert :: "_ ⇒ nat ⇒ _ ⇒ _"
where "sh_insert ≡ SkewBinomialHeap.insert"
definition
sh_meld :: "('a,nat) SkewBinomialHeap ⇒ _"
where "sh_meld ≡ SkewBinomialHeap.meld"

definition
bh_empty :: "unit ⇒ ('a,nat) BinomialHeap"
where "bh_empty u ≡ BinomialHeap.empty"
definition
bh_findMin :: "('a,nat) BinomialHeap ⇒ _"
where "bh_findMin ≡ BinomialHeap.findMin"
definition
bh_deleteMin :: "('a,nat) BinomialHeap ⇒ ('a,nat) BinomialHeap"
where "bh_deleteMin ≡ BinomialHeap.deleteMin"
definition
bh_insert :: "_ ⇒ nat ⇒ _ ⇒ _"
where "bh_insert ≡ BinomialHeap.insert"
definition
bh_meld :: "('a,nat) BinomialHeap ⇒ _"
where "bh_meld ≡ BinomialHeap.meld"

export_code
sh_empty
sh_findMin
sh_deleteMin
sh_insert
sh_meld

bh_empty
bh_findMin
bh_deleteMin
bh_insert
bh_meld
in OCaml
in SML

ML_val ‹
(* ** Binomial Heaps ** *)

val q1 = @{code bh_insert} "a" (@{code nat_of_integer} 1)
(@{code bh_insert} "b" (@{code nat_of_integer} 2) (@{code bh_empty} ()));
val q2 = @{code bh_insert} "c" (@{code nat_of_integer} 3)
(@{code bh_insert} "d" (@{code nat_of_integer} 4) (@{code bh_empty} ()));

val q = @{code bh_meld} q1 q2;
@{code bh_findMin} q;

val q = @{code bh_deleteMin} q;
@{code bh_findMin} q;

(* ** Skew Binomial Heaps ** *)
val q1 = @{code sh_insert} "a" (@{code nat_of_integer} 1)
(@{code sh_insert} "b" (@{code nat_of_integer} 2) (@{code sh_empty} ()));
val q2 = @{code sh_insert} "c" (@{code nat_of_integer} 3)
(@{code sh_insert} "d" (@{code nat_of_integer} 4) (@{code sh_empty} ()));

val q = @{code sh_meld} q1 q2;
@{code sh_findMin} q;

val q = @{code sh_deleteMin} q;
@{code sh_findMin} q;
›

end
```