root/hhdl/problem.hs

-- "A problem with functional dependencies.
-- use -fcontext-stack=100 ghc switch.

{-# LANGUAGE GADTs, FunctionalDependencies, MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances, FlexibleContexts, UndecidableInstances #-}

module Problem where

import Data.Bits
import Data.Word

-------------------------------------------------------------------------------
-- Type level arithmetic.

data Zero = Zero
data Succ n = Succ n

type ZERO = Zero
type ONE = Succ ZERO
type TWO = Succ ONE
type THREE = Succ TWO
type FOUR = Succ THREE
type FIVE = Succ FOUR
type SIX = Succ FIVE
type SEVEN = Succ SIX
type EIGHT = Succ SEVEN
type NINE = Succ EIGHT
type SIZE10 = Succ NINE
type SIZE11 = Succ SIZE10
type SIZE12 = Succ SIZE11
type SIZE13 = Succ SIZE12
type SIZE15 = Succ (Succ SIZE13)
type SIZE16 = Succ SIZE15
type SIZE20 = Succ (Succ (Succ (Succ (Succ SIZE15))))
type SIZE25 = Succ (Succ (Succ (Succ (Succ SIZE20))))
type SIZE26 = Succ SIZE25
type SIZE30 = Succ (Succ (Succ (Succ (Succ SIZE25))))
type SIZE32 = Succ (Succ SIZE30)

class Nat n where fromNat :: n -> Int

instance Nat Zero where fromNat = const 0
instance Nat n => Nat (Succ n) where fromNat ~(Succ n) = 1+fromNat n

class (Nat a, Nat b, Nat c) => CPlus a b c | a b -> c, a c -> b

--instance Nat a => CPlus a Zero a
instance Nat a => CPlus Zero a a
instance (CPlus a b c) => CPlus (Succ a) b (Succ c)
--instance (CPlus a b c) => CPlus (Succ a) b (Succ c)
--instance (CPlus a b c) => CPlus a (Succ b) (Succ c)

class (Nat a, Nat b, Nat c) => CMax a b c | a b -> c
instance CMax Zero Zero Zero
instance Nat a => CMax (Succ a) Zero (Succ a)
instance Nat a => CMax Zero (Succ a) (Succ a)
instance CMax a b c => CMax (Succ a) (Succ b) (Succ c)

class (Nat a, Nat b) => CDbl a b | a -> b
instance CPlus a a b => CDbl a b

class (Nat a, Nat b) => CPow2 a b | a -> b
instance CPow2 Zero (Succ Zero)
instance (CPow2 a b, CDbl b b2) => CPow2 (Succ a) b2

-------------------------------------------------------------------------------
-- Sized integer.

data IntSz n where
        IntSz :: Nat sz => Integer -> IntSz sz

intSzSizeType :: IntSz n -> n; intSzSizeType _ = undefined
intSzSize :: Nat n => IntSz n -> Int; intSzSize n = fromNat $ intSzSizeType n

instance Nat sz => Eq (IntSz sz) where
        (IntSz a) == (IntSz b) = a == b

instance Show (IntSz n) where
        show n@(IntSz x) = show x++"{"++show (intSzSize n)++"}"

instance Nat sz => Num (IntSz sz) where
        fromInteger x = IntSz x
        (IntSz a) + (IntSz b) = IntSz $ a+b
        (IntSz a) - (IntSz b) = IntSz $ a-b
        (IntSz a) * (IntSz b) = IntSz $ a*b
        abs = error "No abs for IntSz."
        signum = error "No signum for IntSz."

-------------------------------------------------------------------------------
-- ToWires class, the main source of problems.

class Nat aSz => ToWires a aSz | a -> aSz where
        wireSizeType :: a -> aSz
        wireSizeType _ = undefined
        wireSize :: a -> Int
        wireSize x = fromNat $ wireSizeType x
        wireMul :: a -> Integer
        wireMul x = Data.Bits.shiftL 1 (wireSize x)
        wireSelSize :: a -> Int
        wireSelSize = const 0
        -- Integer should occupy no more than wireSize bits, higher ones should 0
        toWires :: a -> Integer
        -- fromWires should work with integers that have non-zero bits
        -- above wireSize index.
        fromWires :: Integer -> a
        -- enumeration.
        -- valuesCount of (Maybe a) returns 1+valuesCount (x::a)
        -- valuesCount of Either a b returns valuesCount (x::a) + valuesCount (yLLb)
        -- valuesCount of (a,b) returns valuesCoutn (x::a) * valuesCount (y::b)
        valuesCount :: a -> Integer
        -- valueIndex.
        -- get a value and return an index inside enumeration.
        valueIndex :: a -> Integer

-------------------------------------------------------------------------------
-- Instances.

instance (ToWires x a,ToWires y b, CPlus a b c) => ToWires (x,y) c where
        toWires (a,b) = Data.Bits.shiftL (toWires a) (wireSize b) .|. toWires b
        fromWires x = (a,b)
                where
                        b = fromWires x
                        a = fromWires $ Data.Bits.shiftR x (wireSize b)
        valuesCount (a,b) = valuesCount a*valuesCount b
        valueIndex (a,b) = valueIndex a*valuesCount b + valueIndex b

instance (ToWires x1 a,ToWires x2 b,ToWires x3 c,
        CPlus b c bc, CPlus a bc abc) =>
        ToWires (x1,x2,x3) abc where
        toWires (a,b,c) = toWires (a,(b,c))
        fromWires abc = (a,b,c)
                where
                        (a,(b,c)) = fromWires abc
        valuesCount (a,b,c) = valuesCount (a,(b,c))
        valueIndex (a,b,c) = valueIndex (a,(b,c))

instance (ToWires x1 a,ToWires x2 b,ToWires x3 c,ToWires x4 d,ToWires x5 e,
        CPlus d e de, CPlus c de cde, CPlus b cde bcde, CPlus a bcde abcde) =>
        ToWires (x1,x2,x3,x4,x5) abcde where
        toWires (a,b,c,d,e) = toWires (a,(b,(c,(d,e))))
        fromWires abcde = (a,b,c,d,e)
                where
                        (a,(b,(c,(d,e)))) = fromWires abcde
        valuesCount (a,b,c,d,e) = valuesCount (a,(b,(c,(d,e))))
        valueIndex (a,b,c,d,e) = valueIndex (a,(b,(c,(d,e))))

instance CPow2 FIVE size32 => ToWires Int size32 where
        toWires n = fromIntegral n .&. 0xffffffff
        fromWires x = fromIntegral x
        valuesCount = const (Data.Bits.shiftL (1::Integer) 32)
        valueIndex = fromIntegral

instance CPow2 FIVE size32 => ToWires Word32 size32 where
        toWires n = fromIntegral n .&. 0xffffffff
        fromWires x = fromIntegral x
        valuesCount = const (Data.Bits.shiftL (1::Integer) 32)
        valueIndex = fromIntegral

instance Nat size => ToWires (IntSz size) size where
        toWires x@(IntSz n) = n .&. (Data.Bits.shiftL 1 (wireSize x) - 1)
        fromWires x = fromIntegral x
        valuesCount x = Data.Bits.shiftL (1::Integer) (wireSize x)
        valueIndex x = toWires x

-------------------------------------------------------------------------------
-- Types for a problem.

-- A hack around bugs (??) in ghc 6.10.1.
data RI = RI (IntSz FIVE)
        deriving (Eq,Show)
data Imm5 = Imm5 (IntSz FIVE)
        deriving (Eq,Show)
data Imm16 = Imm16 (IntSz SIZE16)
        deriving (Eq,Show)
data Imm26 = Imm26 (IntSz SIZE26)
        deriving (Eq,Show)

instance ToWires RI FIVE where
        toWires (RI x) = toWires x
        fromWires x = RI $ fromWires x
        valuesCount = const 32
        valueIndex (RI x) = toWires x

instance ToWires Imm5 FIVE where
        toWires (Imm5 x) = toWires x
        fromWires x = Imm5 $ fromWires x
        valuesCount = const 32
        valueIndex (Imm5 x) = toWires x

instance ToWires Imm16 SIZE16 where
        toWires (Imm16 x) = toWires x
        fromWires x = Imm16 $ fromWires x
        valuesCount (Imm16 x) = valuesCount x
        valueIndex (Imm16 x) = valueIndex x

instance ToWires Imm26 SIZE26 where
        toWires (Imm26 x) = toWires x
        fromWires x = Imm26 $ fromWires x
        valuesCount (Imm26 x) = valuesCount x
        valueIndex (Imm26 x) = toWires x

instance ToWires a sz => ToWires (Maybe a) (Succ sz) where
        toWires Nothing = 0
        toWires (Just x) = shiftL (toWires x) 1 .|. 1
        fromWires = undefined
        valuesCount x = 1+valuesCount y
                where
                        ~(Just y) = x

        valueIndex Nothing = 0
        valueIndex (Just x) = 1+valueIndex x

-------------------------------------------------------------------------------
-- And a problem itself.

data Signed = Signed | Unsigned
        deriving (Eq,Show)

data MIPSCmd regv =
                Nop
        |       Trap
        -- we mark destination register with RI. It never gets fetched.
        -- we mark source registers as regv, because they can change their size
        -- at FETCH stage (became Word32).
        |       AddU    regv regv RI
        |       And     regv regv RI
        |       Div     Signed regv regv
        deriving (Eq,Show)

instance ToWires Signed (Succ Zero) where
        toWires (Signed) = Data.Bits.shiftL 0 1 .|. 0
        toWires (Unsigned) = Data.Bits.shiftL 0 1 .|. 1
        fromWires x = undefined
        valuesCount x = 1 + (1 + 0)
                where
                        ~(Signed) = x
                        ~(Unsigned) = x
        valueIndex x = case x of
                Signed -> 0 + 0
                Unsigned -> (0 + 0) + 0
                where
                        ~(Signed) = x
                        ~(Unsigned) = x

instance (ToWires regv_0 v_1, ToWires RI v_2,
        CPlus v_1 v_1 vCPlus_3, CPlus vCPlus_3 v_2 vCPlus_4,
        CPlus v_1 v_1 vCPlus_5, CPlus vCPlus_5 v_2 vCPlus_6,
        ToWires Signed v_7, CPlus v_7 v_1 vCPlus_8, CPlus vCPlus_8 v_1 vCPlus_9,
        CMax vCPlus_4 vCPlus_6 vCMax_10, CMax vCMax_10 vCPlus_9 vCMax_11)
        => ToWires (MIPSCmd regv_0) (Succ (Succ (Succ vCMax_11))) where

        toWires (Nop) = Data.Bits.shiftL 0 3 .|. 0
        toWires (Trap) = Data.Bits.shiftL 0 3 .|. 1
        toWires (AddU a_12 a_13 a_14) =
                Data.Bits.shiftL (Data.Bits.shiftL (Data.Bits.shiftL (Data.Bits.shiftL 0 (wireSize a_12) .|. toWires a_12) (wireSize a_13) .|. toWires a_13) (wireSize a_14) .|. toWires a_14) 3 .|. 2
        toWires (And a_15 a_16 a_17) =
                Data.Bits.shiftL (Data.Bits.shiftL (Data.Bits.shiftL (Data.Bits.shiftL 0 (wireSize a_15) .|. toWires a_15) (wireSize a_16) .|. toWires a_16) (wireSize a_17) .|. toWires a_17) 3 .|. 3
        toWires (Div a_18 a_19 a_20) =
                Data.Bits.shiftL (Data.Bits.shiftL (Data.Bits.shiftL (Data.Bits.shiftL 0 (wireSize a_18) .|. toWires a_18) (wireSize a_19) .|. toWires a_19) (wireSize a_20) .|. toWires a_20) 3 .|. 4
        fromWires x = undefined
        valuesCount x = 1 + (1 + ((valuesCount x_21 * (valuesCount x_22 * (valuesCount x_23 * 1))) + ((valuesCount x_24 * (valuesCount x_25 * (valuesCount x_26 * 1))) + ((valuesCount x_27 * (valuesCount x_28 * (valuesCount x_29 * 1))) + 0))))
                where
                        ~(Nop) = x
                        ~(Trap) = x
                        ~(AddU x_21 x_22 x_23) = x
                        ~(And x_24 x_25 x_26) = x
                        ~(Div x_27 x_28 x_29) = x
        valueIndex x = case x of
                Nop -> 0 + 0
                Trap -> (0 + 0) + 0
-- THE PROBLEM!!!
                AddU ax_30 ax_31 ax_32 ->
                        ((0 + 0) + 0) + valueIndex (ax_32,(ax_30, ax_31))
-- /THE PROBLEM!!!
{-
                                 And x_33 x_34 x_35 -> (((0 + 0) + 0) + valuesCount (x_32,
                                                                                     (x_30,
                                                                                      x_31))) + valueIndex (x_35,
                                                                                                            (x_33,
                                                                                                             x_34))
-}
                Div x_36 x_37 x_38 -> ((((0 + 0) + 0) + valuesCount (x_32,(x_30,x_31))) + valuesCount (x_35,(x_33,x_34))) + 
                        -- valueIndex (x_38,(x_36,x_37))
                        valueIndex x_38*valuesCount x_36*valuesCount x_37 + valueIndex x_36 * valuesCount x_37+valueIndex x_37
                             where ~(Nop) = x
                                   ~(Trap) = x
                                   ~(AddU x_30 x_31 x_32) = x
                                   ~(And x_33 x_34 x_35) = x
                                   ~(Div x_36 x_37 x_38) = x