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 Haskell
  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