Quelle  Test.thy

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