Serguey Zefirov (thesz) wrote,
Serguey Zefirov
thesz

Снова обшибка в проверяльщике типов ghc 6.10.1.

-- "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))
-}
                             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



Вот, ещё обнаружилось.

Что делать, не знаю. Явно проблемы в проверке типов ghc 6.10.1 (6.8.2 ест всё). Как обходить - непонятно. Синтаксические конструкции для ghc 6.10 и 6.8.2 совершенно разные.

Буду думать.
Tags: Хаскель, моделирование аппаратуры, ошибки
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 0 comments