aboutsummaryrefslogtreecommitdiff
path: root/src/AST/Types.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/AST/Types.hs')
-rw-r--r--src/AST/Types.hs205
1 files changed, 0 insertions, 205 deletions
diff --git a/src/AST/Types.hs b/src/AST/Types.hs
deleted file mode 100644
index a3b7302..0000000
--- a/src/AST/Types.hs
+++ /dev/null
@@ -1,205 +0,0 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE StandaloneKindSignatures #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE TypeData #-}
-module AST.Types where
-
-import Data.Int (Int32, Int64)
-import Data.GADT.Compare
-import Data.GADT.Show
-import Data.Kind (Type)
-import Data.Type.Equality
-
-import Data
-
-
-type data Ty
- = TNil
- | TPair Ty Ty
- | TEither Ty Ty
- | TLEither Ty Ty
- | TMaybe Ty
- | TArr Nat Ty -- ^ rank, element type
- | TScal ScalTy
- | TAccum Ty -- ^ contained type must be a monoid type
-
-type data ScalTy = TI32 | TI64 | TF32 | TF64 | TBool
-
-type STy :: Ty -> Type
-data STy t where
- STNil :: STy TNil
- STPair :: STy a -> STy b -> STy (TPair a b)
- STEither :: STy a -> STy b -> STy (TEither a b)
- STLEither :: STy a -> STy b -> STy (TLEither a b)
- STMaybe :: STy a -> STy (TMaybe a)
- STArr :: SNat n -> STy t -> STy (TArr n t)
- STScal :: SScalTy t -> STy (TScal t)
- STAccum :: SMTy t -> STy (TAccum t)
-deriving instance Show (STy t)
-
-instance GCompare STy where
- gcompare = \cases
- STNil STNil -> GEQ
- STNil _ -> GLT ; _ STNil -> GGT
- (STPair a b) (STPair a' b') -> gorderingLift2 (gcompare a a') (gcompare b b')
- STPair{} _ -> GLT ; _ STPair{} -> GGT
- (STEither a b) (STEither a' b') -> gorderingLift2 (gcompare a a') (gcompare b b')
- STEither{} _ -> GLT ; _ STEither{} -> GGT
- (STLEither a b) (STLEither a' b') -> gorderingLift2 (gcompare a a') (gcompare b b')
- STLEither{} _ -> GLT ; _ STLEither{} -> GGT
- (STMaybe a) (STMaybe a') -> gorderingLift1 (gcompare a a')
- STMaybe{} _ -> GLT ; _ STMaybe{} -> GGT
- (STArr n t) (STArr n' t') -> gorderingLift2 (gcompare n n') (gcompare t t')
- STArr{} _ -> GLT ; _ STArr{} -> GGT
- (STScal t) (STScal t') -> gorderingLift1 (gcompare t t')
- STScal{} _ -> GLT ; _ STScal{} -> GGT
- (STAccum t) (STAccum t') -> gorderingLift1 (gcompare t t')
- -- STAccum{} _ -> GLT ; _ STAccum{} -> GGT
-
-instance TestEquality STy where testEquality = geq
-instance GEq STy where geq = defaultGeq
-instance GShow STy where gshowsPrec = defaultGshowsPrec
-
--- | Monoid types
-type SMTy :: Ty -> Type
-data SMTy t where
- SMTNil :: SMTy TNil
- SMTPair :: SMTy a -> SMTy b -> SMTy (TPair a b)
- SMTLEither :: SMTy a -> SMTy b -> SMTy (TLEither a b)
- SMTMaybe :: SMTy a -> SMTy (TMaybe a)
- SMTArr :: SNat n -> SMTy t -> SMTy (TArr n t)
- SMTScal :: ScalIsNumeric t ~ True => SScalTy t -> SMTy (TScal t)
-deriving instance Show (SMTy t)
-
-instance GCompare SMTy where
- gcompare = \cases
- SMTNil SMTNil -> GEQ
- SMTNil _ -> GLT ; _ SMTNil -> GGT
- (SMTPair a b) (SMTPair a' b') -> gorderingLift2 (gcompare a a') (gcompare b b')
- SMTPair{} _ -> GLT ; _ SMTPair{} -> GGT
- (SMTLEither a b) (SMTLEither a' b') -> gorderingLift2 (gcompare a a') (gcompare b b')
- SMTLEither{} _ -> GLT ; _ SMTLEither{} -> GGT
- (SMTMaybe a) (SMTMaybe a') -> gorderingLift1 (gcompare a a')
- SMTMaybe{} _ -> GLT ; _ SMTMaybe{} -> GGT
- (SMTArr n t) (SMTArr n' t') -> gorderingLift2 (gcompare n n') (gcompare t t')
- SMTArr{} _ -> GLT ; _ SMTArr{} -> GGT
- (SMTScal t) (SMTScal t') -> gorderingLift1 (gcompare t t')
- -- SMTScal{} _ -> GLT ; _ SMTScal{} -> GGT
-
-instance TestEquality SMTy where testEquality = geq
-instance GEq SMTy where geq = defaultGeq
-instance GShow SMTy where gshowsPrec = defaultGshowsPrec
-
-fromSMTy :: SMTy t -> STy t
-fromSMTy = \case
- SMTNil -> STNil
- SMTPair t1 t2 -> STPair (fromSMTy t1) (fromSMTy t2)
- SMTLEither t1 t2 -> STLEither (fromSMTy t1) (fromSMTy t2)
- SMTMaybe t -> STMaybe (fromSMTy t)
- SMTArr n t -> STArr n (fromSMTy t)
- SMTScal sty -> STScal sty
-
-data SScalTy t where
- STI32 :: SScalTy TI32
- STI64 :: SScalTy TI64
- STF32 :: SScalTy TF32
- STF64 :: SScalTy TF64
- STBool :: SScalTy TBool
-deriving instance Show (SScalTy t)
-
-instance GCompare SScalTy where
- gcompare = \cases
- STI32 STI32 -> GEQ
- STI32 _ -> GLT ; _ STI32 -> GGT
- STI64 STI64 -> GEQ
- STI64 _ -> GLT ; _ STI64 -> GGT
- STF32 STF32 -> GEQ
- STF32 _ -> GLT ; _ STF32 -> GGT
- STF64 STF64 -> GEQ
- STF64 _ -> GLT ; _ STF64 -> GGT
- STBool STBool -> GEQ
- -- STBool _ -> GLT ; _ STBool -> GGT
-
-instance TestEquality SScalTy where testEquality = geq
-instance GEq SScalTy where geq = defaultGeq
-instance GShow SScalTy where gshowsPrec = defaultGshowsPrec
-
-scalRepIsShow :: SScalTy t -> Dict (Show (ScalRep t))
-scalRepIsShow STI32 = Dict
-scalRepIsShow STI64 = Dict
-scalRepIsShow STF32 = Dict
-scalRepIsShow STF64 = Dict
-scalRepIsShow STBool = Dict
-
-type TIx = TScal TI64
-
-tIx :: STy TIx
-tIx = STScal STI64
-
-type family ScalRep t where
- ScalRep TI32 = Int32
- ScalRep TI64 = Int64
- ScalRep TF32 = Float
- ScalRep TF64 = Double
- ScalRep TBool = Bool
-
-type family ScalIsNumeric t where
- ScalIsNumeric TI32 = True
- ScalIsNumeric TI64 = True
- ScalIsNumeric TF32 = True
- ScalIsNumeric TF64 = True
- ScalIsNumeric TBool = False
-
-type family ScalIsFloating t where
- ScalIsFloating TI32 = False
- ScalIsFloating TI64 = False
- ScalIsFloating TF32 = True
- ScalIsFloating TF64 = True
- ScalIsFloating TBool = False
-
-type family ScalIsIntegral t where
- ScalIsIntegral TI32 = True
- ScalIsIntegral TI64 = True
- ScalIsIntegral TF32 = False
- ScalIsIntegral TF64 = False
- ScalIsIntegral TBool = False
-
--- | Returns true for arrays /and/ accumulators.
-hasArrays :: STy t' -> Bool
-hasArrays STNil = False
-hasArrays (STPair a b) = hasArrays a || hasArrays b
-hasArrays (STEither a b) = hasArrays a || hasArrays b
-hasArrays (STLEither a b) = hasArrays a || hasArrays b
-hasArrays (STMaybe t) = hasArrays t
-hasArrays STArr{} = True
-hasArrays STScal{} = False
-hasArrays STAccum{} = True
-
-type family Tup env where
- Tup '[] = TNil
- Tup (t : ts) = TPair (Tup ts) t
-
-mkTup :: f TNil -> (forall a b. f a -> f b -> f (TPair a b))
- -> SList f list -> f (Tup list)
-mkTup nil _ SNil = nil
-mkTup nil pair (e `SCons` es) = pair (mkTup nil pair es) e
-
-tTup :: SList STy env -> STy (Tup env)
-tTup = mkTup STNil STPair
-
-unTup :: (forall a b. c (TPair a b) -> (c a, c b))
- -> SList f list -> c (Tup list) -> SList c list
-unTup _ SNil _ = SNil
-unTup unpack (_ `SCons` list) tup =
- let (xs, x) = unpack tup
- in x `SCons` unTup unpack list xs
-
-type family InvTup core env where
- InvTup core '[] = core
- InvTup core (t : ts) = InvTup (TPair core t) ts