{-# LANGUAGE EmptyDataDecls, RankNTypes, ScopedTypeVariables #-}

module Bounded_List(Blist(..), list_of_blist, equal_blist, bnth, blength)
  where {

import Prelude ((==), (/=), (<), (<=), (>=), (>), (+), (-), (*), (/), (**),
  (>>=), (>>), (=<<), (&&), (||), (^), (^^), (.), ($), ($!), (++), (!!), Eq,
  error, id, return, not, fst, snd, map, filter, concat, concatMap, reverse,
  zip, null, takeWhile, dropWhile, all, any, Integer, negate, abs, divMod,
  String, Bool(True, False), Maybe(Nothing, Just));
import qualified Prelude;
import qualified Rational;
import qualified Set;
import qualified List;
import qualified Arith;
import qualified HOL;
import qualified Finite_Set;

data Blist a b = Bmake (HOL.Itself b) [a] deriving (Prelude.Read, Prelude.Show);

list_of_blist :: forall a b. (Finite_Set.Finite b, Eq b) => Blist a b -> [a];
list_of_blist (Bmake HOL.Type xs) =
  List.take ((Finite_Set.card :: Set.Set b -> Arith.Nat) Set.top_set) xs;

equal_blist ::
  forall a b.
    (Eq a, Finite_Set.Finite b, Eq b) => Blist a b -> Blist a b -> Bool;
equal_blist m1 m2 = list_of_blist m1 == list_of_blist m2;

instance (Eq a, Finite_Set.Finite b, Eq b) => Eq (Blist a b) where {
  a == b = equal_blist a b;
};

bnth :: forall a b. (Finite_Set.Finite b, Eq b) => Blist a b -> Arith.Nat -> a;
bnth xa = List.nth (list_of_blist xa);

blength :: forall a b. (Finite_Set.Finite b, Eq b) => Blist a b -> Arith.Nat;
blength xa = List.size_list (list_of_blist xa);

}