namespace NSokoban
{

    public variant SplayHeap 
    {
  | Empty
  | SplayTree { l : SplayHeap; elem : SMap; r : SplayHeap; min : option[SMap]}

  public IsEmpty () : bool
  {
      this is Empty
  }

  private Min : option [SMap]
  {
      get
      {
    match(this)
    {
        | Empty => None ()
        | SplayTree (_ , _ , _ , m) => m
    }
      }
  }

  public override ToString () : string
  {
      match(this)
      {
    | Empty => ""
    | SplayTree (a , x , b ,min) =>
        x.ToString ()  + " " + "\nLEFT\n\n" + a.ToString () + "\nRIGHT\n\n" + b.ToString () + 
        (match(min)
        {
      | None => "None\n========\n"
      | Some (m) => "Some\n" + m.ToString () + "\n========";
        })
      }
  }

  private partition (pivot : SMap, tree : SplayHeap) : SplayHeap * SplayHeap
  {
      match(tree)
      {
    | Empty => (Empty (),Empty ())
    | SplayTree ( a , x , b , _) as t =>
        if (SMap.Leq (x,pivot))
      match(b)
      {
          | Empty => (t ,Empty ())
          | SplayTree ( b1 , y , b2 ,_) =>
        if(SMap.Leq (y , pivot) )
        {
            def (small,big) = partition (pivot , b2);
            def t1 = SplayTree (a , x , b1 , 
          if(a is Empty)
              Some (x)
          else
              a.Min);
            def t2 = SplayTree ( t1 , y , small , 
                if(a is Empty)
              Some (x)
          else
              a.Min);
              
            (t2, big)
        }
        else
        {
            def (small,big) = partition (pivot , b1);
            def t1 = SplayTree (a , x , small,
          if(a is Empty)
              Some (x)
          else
              a.Min);
            def t2 = SplayTree (big , y , b2 ,
          if(big is Empty)
              Some (y)
          else
              big.Min);
            (t1 , t2)
        }        
      }
        else
      match(a)
      {
          | Empty => (t , Empty())
          | SplayTree ( a1 , y , a2 ,_) =>
        if(SMap.Leq (y , pivot) )
        {
            def (small,big) = partition (pivot, a2);
            def t1 = SplayTree (a1 , y , small,
          if(a1 is Empty)
              Some (y)
          else
              a1.Min);
            def t2 = SplayTree (big , x , b ,
          if(big is Empty)
              Some (x)
          else
              big.Min);
            (t1 , t2)
        }
        else
        {
            def (small,big) = partition (pivot, a1);    
            def t1 = SplayTree (a2 , x , b ,
          if(a2 is Empty)
              Some (x)
          else
              a2.Min);
            def t2 = SplayTree (big , y , t1,
          if(big is Empty)
              Some (x)
          else
              big.Min);
            (small , t2)
        }
      }
      }
  }

  public FindMin () : SMap
  {
      match(this)
      {
    | Empty => throw System.ArgumentException ("FindMin on empty heap");  
    | SplayTree (_ , _ , _ , Some(m)) => m
    | SplayTree (_ , _ , _ , None ()) => assert(false)
      }
  }

  public Insert (x : SMap) : SplayHeap
  {
      def (a,b) = partition(x , this);

      def t = 
      if(a is Empty)
    SplayTree(a , x , b , Some(x));
      else
    SplayTree(a , x , b , a.Min);
    
      t
  }            

  public DeleteMin () : SMap * SplayHeap 
  {

      match(this)
      {
    | Empty => throw System.ArgumentException ("DeleteMin on empty heap");  
    | SplayTree (Empty , x , b , _) =>
        (x, b)
    | SplayTree ( SplayTree (Empty , x , b , _ ) , y , c , _) => 
        def t = SplayTree ( b , y , c , 
      if(b is Empty)
          Some (y)
      else
          b.Min);

        (x,t)
    | SplayTree ( SplayTree (a , x , b , _), y ,c ,_) => 
        def (m,d) = a.DeleteMin ();        
        def t = SplayTree(d , x , 
      SplayTree(b , y , c ,
          if(b is Empty)
        Some(y)
          else
        b.Min),
      if(d is Empty)
          Some (x)
      else
          d.Min);
        
        (m,t)
      }
  }
    }
}