gistfile1.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module NewRange where

data SRangeType ty where
  SAnyNumber :: SRangeType 'AnyNumber
  SNoVal :: SRangeType 'NoVal
  SNonZeroPos :: SRangeType 'NonZeroPos
  SRangeFromTo :: SRangeType 'RangeFromTo
  STyple :: SRangeType a -> SRangeType b -> SRangeType ('Tuple a b)
  SPositive :: SRangeType 'Positive
  SNullable :: SRangeType ty -> SRangeType ('Nullable ty)

-- Allows homogenous lists of ranges.
-- Pattern matching on SRangeType allows type-level range-safe connects.
data SomeRange = forall ty. SomeRange (SRangeType ty)

-- Example homogenous list of ranges
inputs :: [SomeRange]
inputs =
  [ SomeRange SNoVal,
    SomeRange SNonZeroPos
  ]

data Range (typ :: RangeType)
  = Range Int Int
  | TupleleRange (Int, Int) (Int, Int)

data RangeType where
  AnyNumber :: RangeType
  NoVal :: RangeType
  Positive :: RangeType
  NonZeroPos :: RangeType
  Nullable :: RangeType -> RangeType
  RangeFromTo :: RangeType
  Tuple :: RangeType -> RangeType -> RangeType

type family And a b where
  And 'True 'True = 'True
  And _ _ = 'False

type family RangeSubset a b where
  RangeSubset ('Tuple a1 b1) ('Tuple a2 b2) =
    And (RangeSubset a1 a2) (RangeSubset b1 b2)
  RangeSubset 'RangeFromTo 'RangeFromTo = 'True
  RangeSubset 'NoVal 'NoVal = 'True
  RangeSubset _ 'NoVal = 'False
  RangeSubset 'NoVal _ = 'True
  RangeSubset 'Positive 'Positive = 'True
  RangeSubset 'NonZeroPos 'Positive = 'True
  RangeSubset 'NonZeroPos 'NonZeroPos = 'True
  RangeSubset ('Nullable _) ('Nullable _) = 'True
  RangeSubset ('Nullable _) _ = 'False
  RangeSubset a ('Nullable b) = RangeSubset a b
  RangeSubset a 'AnyNumber = 'True
  RangeSubset a b = 'False

valueSubset :: RangeSubset a b ~ 'True => Range a -> Range b -> Bool
valueSubset (Range _fromA _toA) (Range _fromB _toB) = undefined
valueSubset _ _ = True

positive :: Range 'Positive
positive = undefined

nonZero :: Range 'NonZeroPos
nonZero = undefined

nullPositive :: Range ('Nullable 'Positive)
nullPositive = undefined

range :: Int -> Int -> Range 'RangeFromTo
range a b = Range a b

nullRange :: Int -> Int -> Range ('Nullable 'RangeFromTo)
nullRange a b = Range a b

tupleRange :: (Int, Int) -> (Int, Int) -> Range ('Tuple 'RangeFromTo 'RangeFromTo)
tupleRange a b = TupleleRange a b

type DefName = String

type PinName = String

type BoundID = Int

data Ref def where
  Ref :: (HasDefName def) => def -> BoundID -> Ref def

class HasDefName a where
  getDefName :: a -> String

type ConnRef = (DefName, PinName, BoundID)

type Conn = (ConnRef, ConnRef)

type State = (Int, [Conn])

data Pin def (range :: RangeType) = Pin String

initState :: State
initState = (0, [])

mkInstance :: HasDefName def => State -> def -> (Ref def, State)
mkInstance (idCounter, conns) def =
  ( ref,
    (idCounter + 1, conns)
  )
  where
    ref = Ref def idCounter

connect ::
  (HasDefName defA, HasDefName defB, RangeSubset rangeA rangeB ~ 'True) =>
  State ->
  (Ref defA, Pin defA rangeA) ->
  (Ref defB, Pin defB rangeB) ->
  (Ref defB, State)
connect state (Ref fromDef fromId, Pin fromPin) (toRef@(Ref toDef toId), Pin toPin) =
  ( toRef,
    addConn
      (getDefName fromDef, fromPin, fromId)
      (getDefName toDef, toPin, toId)
      state
  )

addConn :: ConnRef -> ConnRef -> State -> State
addConn from to (counter, conns) =
  (counter, conn : conns)
  where
    conn :: Conn
    conn = (from, to)

_typeCheckRanges :: a
_typeCheckRanges = undefined
  where
    _ = valueSubset positive positive
    _ = valueSubset (nullRange 100 200) (nullRange 100 300)
    _ = valueSubset nonZero positive
    _ = valueSubset positive nullPositive
    _ = valueSubset (range 123 456) (range 99 88)
    a = undefined :: Range ('Tuple 'RangeFromTo 'NoVal)
    b = undefined :: Range ('Tuple 'RangeFromTo 'Positive)
    _x = valueSubset a b