Theory Test

theory Test
imports "~~/src/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 file -
  in OCaml file -
  in SML file -

ML {*
  (* ** 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