Last active
February 9, 2023 22:14
-
-
Save clayrat/e469e69313c7e0f9daaaeb4c16bf3be7 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# OPTIONS_GHC -cpp -XMagicHash #-} | |
{- For Hugs, use the option -F"cpp -P -traditional" -} | |
module Avl_ext where | |
import qualified Prelude | |
#ifdef __GLASGOW_HASKELL__ | |
import qualified GHC.Base | |
#if __GLASGOW_HASKELL__ >= 900 | |
import qualified GHC.Exts | |
#endif | |
#else | |
-- HUGS | |
import qualified IOExts | |
#endif | |
#ifdef __GLASGOW_HASKELL__ | |
unsafeCoerce :: a -> b | |
#if __GLASGOW_HASKELL__ >= 900 | |
unsafeCoerce = GHC.Exts.unsafeCoerce# | |
#else | |
unsafeCoerce = GHC.Base.unsafeCoerce# | |
#endif | |
#else | |
-- HUGS | |
unsafeCoerce :: a -> b | |
unsafeCoerce = IOExts.unsafeCoerce | |
#endif | |
#ifdef __GLASGOW_HASKELL__ | |
type Any = GHC.Base.Any | |
#else | |
-- HUGS | |
type Any = () | |
#endif | |
type Pred t = t -> Prelude.Bool | |
type Rel t = t -> Pred t | |
type Axiom t = t -> t -> Prelude.Bool | |
data Mixin_of t = | |
Mixin (Rel t) (Axiom t) | |
op :: (Mixin_of a1) -> Rel a1 | |
op m = | |
case m of { | |
Mixin op0 _ -> op0} | |
type Type = Mixin_of Any | |
-- singleton inductive, whose constructor was Pack | |
type Sort = Any | |
class0 :: Type -> Mixin_of Sort | |
class0 cT = | |
cT | |
eq_op :: Type -> Rel Sort | |
eq_op t = | |
op (class0 t) | |
type Mixin_of0 t = | |
(Pred t) -> Prelude.Integer -> Prelude.Maybe t | |
-- singleton inductive, whose constructor was Mixin | |
data Class_of t = | |
Class (Mixin_of t) (Mixin_of0 t) | |
base :: (Class_of a1) -> Mixin_of a1 | |
base c = | |
case c of { | |
Class base4 _ -> base4} | |
data Mixin_of1 t0 = | |
Mixin0 (Rel Sort) (Rel Sort) | |
lt :: (Mixin_of a1) -> (Mixin_of1 a1) -> Rel Sort | |
lt _ m = | |
case m of { | |
Mixin0 _ lt1 -> lt1} | |
data Class_of0 t = | |
Class0 (Class_of t) (Mixin_of1 t) | |
base0 :: (Class_of0 a1) -> Class_of a1 | |
base0 c = | |
case c of { | |
Class0 base4 _ -> base4} | |
mixin :: (Class_of0 a1) -> Mixin_of1 a1 | |
mixin c = | |
case c of { | |
Class0 _ mixin0 -> mixin0} | |
type Type0 = Class_of0 Any | |
-- singleton inductive, whose constructor was Pack | |
type Sort0 = Any | |
class1 :: () -> Type0 -> Class_of0 Sort0 | |
class1 _ cT = | |
cT | |
lt0 :: () -> Type0 -> Rel Sort0 | |
lt0 disp t = | |
lt (base (base0 (class1 disp t))) (mixin (class1 disp t)) | |
data Mixin_of2 t0 = | |
Mixin1 (Sort0 -> Sort0 -> Sort0) (Sort0 -> Sort0 -> Sort0) | |
data Class_of1 t = | |
Class1 (Class_of0 t) (Mixin_of2 t) | |
base1 :: (Class_of1 a1) -> Class_of0 a1 | |
base1 c = | |
case c of { | |
Class1 base4 _ -> base4} | |
type Class_of2 t = Class_of1 t | |
-- singleton inductive, whose constructor was Class | |
base2 :: (Class_of2 a1) -> Class_of1 a1 | |
base2 c = | |
c | |
type Class_of3 t = Class_of2 t | |
-- singleton inductive, whose constructor was Class | |
base3 :: (Class_of3 a1) -> Class_of2 a1 | |
base3 c = | |
c | |
type Type1 = Class_of3 Any | |
-- singleton inductive, whose constructor was Pack | |
type Sort1 = Any | |
class2 :: () -> Type1 -> Class_of3 Sort1 | |
class2 _ cT = | |
cT | |
eqType :: () -> Type1 -> Type | |
eqType disp cT = | |
base (base0 (base1 (base2 (base3 (class2 disp cT))))) | |
porderType :: () -> Type1 -> Type0 | |
porderType disp cT = | |
base1 (base2 (base3 (class2 disp cT))) | |
data Tree a = | |
Leaf | |
| Node (Tree a) a (Tree a) | |
leaf :: Tree a1 | |
leaf = | |
Leaf | |
is_node :: (Tree a1) -> Prelude.Bool | |
is_node t = | |
case t of { | |
Leaf -> Prelude.False; | |
Node _ _ _ -> Prelude.True} | |
cmp :: () -> Type1 -> Sort1 -> Sort1 -> Base.Ordering | |
cmp disp t x y = | |
case lt0 disp (porderType disp t) x y of { | |
Prelude.True -> Base.LT; | |
Prelude.False -> case eq_op (eqType disp t) x y of { | |
Prelude.True -> Base.EQ; | |
Prelude.False -> Base.GT}} | |
isin_a :: () -> Type1 -> (Tree ((,) Sort1 a1)) -> Sort1 -> Prelude.Bool | |
isin_a disp t t0 x = | |
case t0 of { | |
Leaf -> Prelude.False; | |
Node l p r -> | |
case p of { | |
(,) a _ -> | |
case cmp disp t x a of { | |
Base.LT -> isin_a disp t l x; | |
Base.EQ -> Prelude.True; | |
Base.GT -> isin_a disp t r x}}} | |
data Bal0 = | |
Lh | |
| Bal | |
| Rh | |
eqbal :: Bal0 -> Bal0 -> Prelude.Bool | |
eqbal b1 b2 = | |
case b1 of { | |
Lh -> case b2 of { | |
Lh -> Prelude.True; | |
_ -> Prelude.False}; | |
Bal -> case b2 of { | |
Bal -> Prelude.True; | |
_ -> Prelude.False}; | |
Rh -> case b2 of { | |
Rh -> Prelude.True; | |
_ -> Prelude.False}} | |
eqbalP :: Axiom Bal0 | |
eqbalP __top_assumption_ = | |
let { | |
_evar_0_ = \__top_assumption_0 -> | |
let {_evar_0_ = Prelude.True} in | |
let {_evar_0_0 = Prelude.False} in | |
let {_evar_0_1 = Prelude.False} in | |
case __top_assumption_0 of { | |
Lh -> _evar_0_; | |
Bal -> _evar_0_0; | |
Rh -> _evar_0_1}} | |
in | |
let { | |
_evar_0_0 = \__top_assumption_0 -> | |
let {_evar_0_0 = Prelude.False} in | |
let {_evar_0_1 = Prelude.True} in | |
let {_evar_0_2 = Prelude.False} in | |
case __top_assumption_0 of { | |
Lh -> _evar_0_0; | |
Bal -> _evar_0_1; | |
Rh -> _evar_0_2}} | |
in | |
let { | |
_evar_0_1 = \__top_assumption_0 -> | |
let {_evar_0_1 = Prelude.False} in | |
let {_evar_0_2 = Prelude.False} in | |
let {_evar_0_3 = Prelude.True} in | |
case __top_assumption_0 of { | |
Lh -> _evar_0_1; | |
Bal -> _evar_0_2; | |
Rh -> _evar_0_3}} | |
in | |
case __top_assumption_ of { | |
Lh -> _evar_0_; | |
Bal -> _evar_0_0; | |
Rh -> _evar_0_1} | |
bal_eqMixin :: Mixin_of Bal0 | |
bal_eqMixin = | |
Mixin eqbal eqbalP | |
bal_eqType :: Type | |
bal_eqType = | |
unsafeCoerce bal_eqMixin | |
type Tree_bal a = Tree ((,) a Bal0) | |
is_bal :: (Tree_bal a1) -> Prelude.Bool | |
is_bal t = | |
case t of { | |
Leaf -> Prelude.False; | |
Node _ p _ -> case p of { | |
(,) _ b -> eq_op bal_eqType (unsafeCoerce b) (unsafeCoerce Bal)}} | |
incr :: (Tree_bal a1) -> (Tree_bal a1) -> Prelude.Bool | |
incr t t' = | |
(Prelude.||) (Prelude.not (is_node t)) ((Prelude.&&) (is_bal t) (Prelude.not (is_bal t'))) | |
rot2 :: (Tree_bal a1) -> a1 -> (Tree_bal a1) -> a1 -> (Tree_bal a1) -> Tree_bal a1 | |
rot2 a x b z c = | |
case b of { | |
Leaf -> leaf; | |
Node b1 p b2 -> | |
case p of { | |
(,) y bb -> | |
let { | |
bb1 = case eq_op bal_eqType (unsafeCoerce bb) (unsafeCoerce Rh) of { | |
Prelude.True -> Lh; | |
Prelude.False -> Bal}} | |
in | |
let { | |
bb2 = case eq_op bal_eqType (unsafeCoerce bb) (unsafeCoerce Lh) of { | |
Prelude.True -> Rh; | |
Prelude.False -> Bal}} | |
in | |
Node (Node a ((,) x bb1) b1) ((,) y Bal) (Node b2 ((,) z bb2) c)}} | |
balL_b :: (Tree_bal a1) -> a1 -> Bal0 -> (Tree_bal a1) -> Tree_bal a1 | |
balL_b ab z bb c = | |
case bb of { | |
Lh -> | |
case ab of { | |
Leaf -> leaf; | |
Node a p b -> | |
case p of { | |
(,) x b0 -> | |
case b0 of { | |
Lh -> Node a ((,) x Bal) (Node b ((,) z Bal) c); | |
Bal -> Node a ((,) x Rh) (Node b ((,) z Lh) c); | |
Rh -> rot2 a x b z c}}}; | |
Bal -> Node ab ((,) z Lh) c; | |
Rh -> Node ab ((,) z Bal) c} | |
balR_b :: (Tree_bal a1) -> a1 -> Bal0 -> (Tree_bal a1) -> Tree_bal a1 | |
balR_b a x bb bc = | |
case bb of { | |
Lh -> Node a ((,) x Bal) bc; | |
Bal -> Node a ((,) x Rh) bc; | |
Rh -> | |
case bc of { | |
Leaf -> leaf; | |
Node b p c -> | |
case p of { | |
(,) z b0 -> | |
case b0 of { | |
Lh -> rot2 a x b z c; | |
Bal -> Node (Node a ((,) x Rh) b) ((,) z Lh) c; | |
Rh -> Node (Node a ((,) x Bal) b) ((,) z Bal) c}}}} | |
insert_b :: () -> Type1 -> Sort1 -> (Tree_bal Sort1) -> Tree_bal Sort1 | |
insert_b disp t x t0 = | |
case t0 of { | |
Leaf -> Node leaf ((,) x Bal) leaf; | |
Node l p r -> | |
case p of { | |
(,) a b -> | |
case cmp disp t x a of { | |
Base.LT -> | |
let {l' = insert_b disp t x l} in | |
case incr l l' of { | |
Prelude.True -> balL_b l' a b r; | |
Prelude.False -> Node l' ((,) a b) r}; | |
Base.EQ -> Node l ((,) a b) r; | |
Base.GT -> | |
let {r' = insert_b disp t x r} in | |
case incr r r' of { | |
Prelude.True -> balR_b l a b r'; | |
Prelude.False -> Node l ((,) a b) r'}}}} | |
decr :: (Tree_bal a1) -> (Tree_bal a1) -> Prelude.Bool | |
decr t t' = | |
(Prelude.&&) (is_node t) | |
((Prelude.||) (Prelude.not (is_node t')) ((Prelude.&&) (Prelude.not (is_bal t)) (is_bal t'))) | |
split_max_b :: (Tree_bal a1) -> a1 -> Bal0 -> (Tree_bal a1) -> (,) (Tree_bal a1) a1 | |
split_max_b l a ba r = | |
case r of { | |
Leaf -> (,) l a; | |
Node lr p rr -> | |
case p of { | |
(,) ar br -> | |
case split_max_b lr ar br rr of { | |
(,) r' a' -> | |
let { | |
t' = case decr r r' of { | |
Prelude.True -> balL_b l a ba r'; | |
Prelude.False -> Node l ((,) a ba) r'}} | |
in | |
(,) t' a'}}} | |
delete_b :: () -> Type1 -> Sort1 -> (Tree_bal Sort1) -> Tree_bal Sort1 | |
delete_b disp t x t0 = | |
case t0 of { | |
Leaf -> leaf; | |
Node l p r -> | |
case p of { | |
(,) a ba -> | |
case cmp disp t x a of { | |
Base.LT -> | |
let {l' = delete_b disp t x l} in | |
case decr l l' of { | |
Prelude.True -> balR_b l' a ba r; | |
Prelude.False -> Node l' ((,) a ba) r}; | |
Base.EQ -> | |
case l of { | |
Leaf -> r; | |
Node ll p0 rl -> | |
case p0 of { | |
(,) al bl -> | |
case split_max_b ll al bl rl of { | |
(,) l' a' -> | |
case decr l l' of { | |
Prelude.True -> balR_b l' a' ba r; | |
Prelude.False -> Node l' ((,) a' ba) r}}}}; | |
Base.GT -> | |
let {r' = delete_b disp t x r} in | |
case decr r r' of { | |
Prelude.True -> balL_b l a ba r'; | |
Prelude.False -> Node l ((,) a ba) r'}}}} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment