--- /dev/null
+module test
+
+import qualified StdEnv
+import StdEnv => qualified isEven, isOdd, class toInt(..), instance toInt Int, class toString(..)
+
+:: Zero = Zero
+:: Succ a = Succ
+:: One :== Succ Zero
+One :: One
+One = undef
+:: Two :== Succ (Succ Zero)
+Two :: Two
+Two = undef
+:: Three :== Succ (Succ (Succ Zero))
+Three :: Three
+Three = undef
+:: True = Tr
+:: False = Fs
+
+class Even a ~c
+where
+ isEven :: a -> c
+ isEven _ = undef
+class Odd a ~c
+where
+ isOdd :: a -> c
+ isOdd _ = undef
+instance Even Zero True
+instance Odd Zero False
+instance Even (Succ a) b | Odd a b
+instance Odd (Succ a) b | Even a b
+
+dec :: (Succ a) -> a
+dec _ = undef
+
+class Add a b ~c
+where
+ (:+:) infixl 6 :: a b -> c
+ (:+:) _ _ = undef
+instance Add Zero b b
+instance Add (Succ a) b (Succ c) | Add a b c
+
+class Mult a b ~c
+where
+ (:*:) infixl 7 :: a b -> c
+ (:*:) _ _ = undef
+instance Mult Zero b Zero
+instance Mult (Succ a) b d | Mult a b c & Add b c d
+
+class Pow a b ~c
+where
+ (:^:) infixr 8 :: a b -> c
+ (:^:) _ _ = undef
+instance Pow a Zero One
+instance Pow a (Succ b) d | Pow a b c & Mult a c d
+
+instance +++ {!a}
+where
+ (+++) l r =
+ { 'StdEnv'._createArray (size l+size r)
+ & [i]=l.[i], [size l+j]=r.[j]
+ \\ i<-[0..size l-1] & j <- [0..size r-1]
+ }
+
+:: Vec n a = Vec {!a}
+
+empty :: Vec Zero a
+empty = Vec {}
+
+single :: a -> Vec (Succ Zero) a
+single a = Vec {a}
+
+length :: (Vec n a) -> n
+length _ = undef
+
+nrepeat :: n a -> Vec n a | toInt n
+nrepeat _ a = repeat a
+
+repeat :: a -> Vec n a | toInt n
+repeat a = let r = Vec (createArray (toInt (length r)) a) in r
+
+append :: (Vec n a) (Vec m a) -> Vec x a | Add n m x
+append (Vec a) (Vec b) = Vec (a +++ b)
+
+<<<<<<< HEAD
+//Start = nrepeat (Three :*: Three) 'a'
+
+v1 :: Vec (Succ (Succ Zero)) Int
+v1 = append (single 1) (single 32)
+
+v2 :: Vec Three Int
+v2 = repeat 5
+
+=======
+>>>>>>> 7675818dc8fc41eaf864dc89a8c2ce62c7dae93f
+class Le a b ~c
+where
+ le :: a b -> c
+ le _ _ = undef
+instance Le Zero b True
+instance Le (Succ a) Zero False
+instance Le (Succ a) (Succ b) c | Le a b c
+
+//Because toInt from StdEnv is strict in the first argument
+class toInt a :: a -> Int
+instance toInt Int where toInt i = i
+instance toInt Zero where toInt _ = 0
+instance toInt (Succ n) | toInt n where toInt a = inc (toInt (dec a))
+
+(!!) infixl 9 :: (Vec n a) i -> a | Le (Succ i) n True & toInt i
+(!!) (Vec a) i = a.[toInt i]
+
+(=.) infixl 9 :: (Vec n a) (i, a) -> Vec n a | Le (Succ i) n True & toInt i
+(=.) (Vec a) (i, x) = Vec {{e\\e<-:a} & [toInt i]=x}
+
+:: A = A; :: B = B; :: C = C; :: D = D; :: E = E; :: F = F; :: G = G; :: H = H;
+:: I = I; :: J = J; :: K = K; :: L = L; :: M = M; :: N = N; :: O = O; :: P = P;
+:: Q = Q; :: R = R; :: S = S; :: T = T; :: U = U; :: V = V; :: W = W; :: X = X;
+<<<<<<< HEAD
+:: Y = Y; :: Z = Z; :: Spc = Spc
+:: Nl = Nl
+:: SC l r = SC
+
+:: Cons x xs = Cons
+class HConcat a b ~c
+where
+ hconcat :: a b -> c
+ hconcat _ _ = undef
+instance HConcat () a a
+instance HConcat (Cons x xs) ys (Cons x zs) | HConcat xs ys zs
+
+:: FooS :== Cons F (Cons O (Cons O ()))
+FooS :: FooS
+FooS = undef
+:: BarS :== Cons B (Cons A (Cons A ()))
+BarS :: BarS
+BarS = undef
+
+:: NilS :== ()
+NilS :: NilS
+NilS = undef
+=======
+:: Y = Y; :: Z = Z;
+:: Nul = Nul
+:: SC l r = SC
+
+Start = nrepeat (Three :*: Three) 'a'
+
+e1 :: Vec (Succ (Succ Zero)) Int
+e1 = append (single 1) (single 32)
+
+e2 :: Vec Three Int
+e2 = repeat 5
+>>>>>>> 7675818dc8fc41eaf864dc89a8c2ce62c7dae93f
+++ /dev/null
-Clean System Files
-*.prj
-*.prp
-*.exe
-*.out
-*-data
-*-www
-*-sapl
-*.bc
-*.pbc
+++ /dev/null
-# Deeply embedded generics
-
+++ /dev/null
-definition module GenType
-
-import StdGeneric
-from StdOverloaded import class ==, class toString
-
-//* Auxiliary type to help with casting values, this is gone at runtime
-:: Box b a =: Box b
-derive bimap Box
-unBox (Box b) :== b
-box b :== Box b
-reBox x :== box (unBox x)
-
-//* Deeply embedded generic type representation
-:: GType
- = GTyBasic BasicType
- | GTyRef String
- | GTyArrow GType GType
- | GTyArray ArrayType GType
- | GTyUList UListType GType
- | GTyUMaybe GType
- | GTyUnit
- | GTyEither GType GType
- | GTyPair GType GType
- | GTyCons GenericConsDescriptor GType
- | GTyField GenericFieldDescriptor GType
- | GTyObject GenericTypeDefDescriptor GType
- | GTyRecord GenericRecordDescriptor GType
-
-//* Type representation larded with the generic type information
-:: Type
- = TyBasic BasicType
- | TyRef String
- | TyArrow Type Type
- | TyArray ArrayType Type
- | TyUList UListType Type
- | TyUMaybe Type
- | TyNewType GenericTypeDefDescriptor GenericConsDescriptor Type
- | TyObject GenericTypeDefDescriptor [(GenericConsDescriptor, [Type])]
- | TyRecord GenericRecordDescriptor [(GenericFieldDescriptor, Type)]
-
-//* Basic types
-:: BasicType = BTInt | BTChar | BTReal | BTBool | BTDynamic | BTFile | BTWorld
-//* Array kinds
-:: ArrayType = AStrict | ALazy | AUnboxed | APacked
-//* Unboxed list kinds
-:: UListType = ULLazy | ULStrict
-//* Kind of a type
-:: Kind = KStar | (KArrow) infixr 1 Kind Kind
-
-instance == GType, Type, BasicType, ArrayType, UListType, GenType, Kind
-instance toString GType, Type, BasicType, ArrayType, UListType, GenType, Kind
-
-/**
- * Removes recursive types by replacing them with references
- *
- * @param gtype
- * @result the main type
- * @result the separated types grouped in strongly connected components
- */
-flattenGType :: GType -> [[GType]]
-
-//* Convert a GType to a Type
-gTypeToType :: GType -> Type
-
-//* Extract the name of the type
-typeName :: Type -> String
-
-//* Extract the genType for a type
-typeGenType :: Type -> [GenType]
-
-//* Extract the kind of the type's constructors (see `{{typeGenType}}`)
-genTypeKind :: [GenType] -> Kind
-//* @type Type -> Kind
-typeKind t :== genTypeKind (typeGenType t)
-
-//* Predicate whether the outer type is a builtin type
-class isBuiltin a :: a -> Bool
-instance isBuiltin Type, GType
-
-//* Predicate whether the outer type is a basic type
-class isBasic a :: a -> Bool
-instance isBasic Type, GType
-
-//* Replace builtin constructors with their pretty names (e.g. _!Cons with [!])
-class replaceBuiltins a :: a -> a
-instance replaceBuiltins Type, GType, GenType
-
-//* Creates a deep embedded generic representation of a type
-generic gType a :: Box GType a
-derive gType UNIT, EITHER, PAIR, CONS of gcd, FIELD of gfd, OBJECT of gtd, RECORD of grd
-derive gType Int, Bool, Real, Char, World, File
-derive gType (->)
-derive gType ?#, ?, ?^
-derive gType [], [! ], [ !], [!!], [#], [#!], {}, {!}, {#}, {32#}
-derive gType (), (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,)
+++ /dev/null
-implementation module GenType
-
-import StdEnv, StdGeneric
-import Control.Applicative
-
-import Control.Monad
-import Control.Monad.State
-import Data.GenEq
-import Control.Monad.Writer
-import Control.Monad.Trans
-import Data.Func
-import Data.Functor
-import Data.Functor.Identity
-import Data.Generics
-import Data.List
-import Data.Maybe
-from Text import class Text(concat), instance Text String
-
-derive bimap Box
-derive gEq BasicType, UListType, ArrayType, GenType
-instance == BasicType where (==) a b = a === b
-instance == UListType where (==) a b = a === b
-instance == ArrayType where (==) a b = a === b
-instance == GenType where (==) a b = a === b
-instance == GType where (==) x y = gTypeEqShallow (2<<30-1) x y
-
-/**
- * Compares two GTypes only up to a given depth
- *
- * @param depth
- * @param lhs
- * @param rhs
- * @return equality
- */
-gTypeEqShallow :: Int GType GType -> Bool
-gTypeEqShallow i _ _
- | i < 0 = True
-gTypeEqShallow _ (GTyBasic i) (GTyBasic j) = i == j
-gTypeEqShallow _ (GTyRef i) (GTyRef j) = i == j
-gTypeEqShallow _ (GTyRef i) (GTyObject j _) = i == j.gtd_name
-gTypeEqShallow _ (GTyRef i) (GTyRecord j _) = i == j.grd_name
-gTypeEqShallow _ (GTyObject j _) (GTyRef i) = i == j.gtd_name
-gTypeEqShallow _ (GTyRecord j _) (GTyRef i) = i == j.grd_name
-gTypeEqShallow i (GTyArrow l1 r1) (GTyArrow l2 r2) = gTypeEqShallow (dec i) l1 l2 && gTypeEqShallow (dec i) r1 r2
-gTypeEqShallow i (GTyArray s1 a1) (GTyArray s2 a2) = s1 == s2 && gTypeEqShallow (dec i) a1 a2
-gTypeEqShallow i (GTyUList s1 a1) (GTyUList s2 a2) = s1 == s2 && gTypeEqShallow (dec i) a1 a2
-gTypeEqShallow i (GTyUMaybe a1) (GTyUMaybe a2) = gTypeEqShallow (dec i) a1 a2
-gTypeEqShallow _ GTyUnit GTyUnit = True
-gTypeEqShallow i (GTyEither l1 r1) (GTyEither l2 r2) = gTypeEqShallow i l1 l2 && gTypeEqShallow i r1 r2
-gTypeEqShallow i (GTyPair l1 r1) (GTyPair l2 r2) = gTypeEqShallow i l1 l2 && gTypeEqShallow i r1 r2
-gTypeEqShallow i (GTyCons i1 a1) (GTyCons i2 a2) = i1.gcd_name == i2.gcd_name && gTypeEqShallow i a1 a2
-gTypeEqShallow i (GTyField i1 a1) (GTyField i2 a2)
- = i1.gfd_name == i2.gfd_name && i1.gfd_cons.grd_name == i2.gfd_cons.grd_name && gTypeEqShallow i a1 a2
-gTypeEqShallow i (GTyObject i1 a1) (GTyObject i2 a2)
- = i1.gtd_name == i2.gtd_name && gTypeEqShallow (dec i) a1 a2
-gTypeEqShallow i (GTyRecord i1 a1) (GTyRecord i2 a2)
- = i1.grd_name == i2.grd_name && gTypeEqShallow (dec i) a1 a2
-gTypeEqShallow _ _ _ = False
-
-instance == Type
-where
- (==) (TyBasic a1) (TyBasic a2) = a1 == a2
- (==) (TyRef a1) (TyRef a2) = a1 == a2
- (==) (TyArrow l1 r1) (TyArrow l2 r2) = l1 == l2 && r1 == r2
- (==) (TyArray s1 a1) (TyArray s2 a2) = s1 == s2 && a1 == a2
- (==) (TyUList s1 a1) (TyUList s2 a2) = s1 == s2 && a1 == a2
- (==) (TyUMaybe a1) (TyUMaybe a2) = a1 == a2
- (==) (TyNewType i1 j1 a1) (TyNewType i2 j2 a2)
- = i1.gtd_name == i2.gtd_name && a1 == a2
- (==) (TyObject i1 a1) (TyObject i2 a2)
- = i1.gtd_name == i2.gtd_name && length a1 == length a2
- && and [l1.gcd_name == l2.gcd_name && t1 == t2\\(l1, t1)<-a1 & (l2, t2)<-a2]
- (==) (TyRecord i1 a1) (TyRecord i2 a2)
- = i1.grd_name == i2.grd_name && length a1 == length a2
- && and [l1.gfd_name == l2.gfd_name && t1 == t2\\(l1, t1)<-a1 & (l2, t2)<-a2]
- (==) _ _ = False
-
-class print a :: a [String] -> [String]
-instance print Bool where print s c = [toString s:c]
-instance print Int where print s c = [toString s:c]
-instance print Char where print s c = [toString s:c]
-instance print String where print s c = [s:c]
-instance print BasicType
-where
- print BTInt c = ["Int":c]
- print BTChar c = ["Char":c]
- print BTReal c = ["Real":c]
- print BTBool c = ["Bool":c]
- print BTDynamic c = ["Dynamic":c]
- print BTFile c = ["File":c]
- print BTWorld c = ["World":c]
-instance print UListType
-where
- print ULStrict c = ["!":c]
- print ULLazy c = c
-instance print ArrayType
-where
- print AStrict c = ["!":c]
- print AUnboxed c = ["#":c]
- print APacked c = ["32#":c]
- print ALazy c = c
-instance print GType
-where
- print (GTyBasic s) c = print s c
- print (GTyRef s) c = [s:c]
- print (GTyArrow l r) c = ["((->)":print l [" ":print r [")":c]]]
- print (GTyArray s a) c = ["{":print s $ print a ["}":c]]
- print (GTyUList s a) c = ["[#":print s $ print s ["]":c]]
- print (GTyUMaybe a) c = ["?#":print a ["]":c]]
- print GTyUnit c = ["UNIT":c]
- print (GTyEither l r) c = ["(EITHER ":print l [" ":print r [")":c]]]
- print (GTyPair l r) c = ["(PAIR ":print l [")":c]]
- print (GTyCons i a) c = ["(CONS ", i.gcd_name, " ":print a [")":c]]
- print (GTyField i a) c = ["(FIELD ", i.gfd_name, " ":print a [")":c]]
- print (GTyObject i a) c = ["(OBJECT ", i.gtd_name, " ":print a [")":c]]
- print (GTyRecord i a) c = ["(RECORD ", i.grd_name, " ":print a [")":c]]
-instance print Type
-where
- print (TyBasic s) c = print s c
- print (TyRef s) c = [s:c]
- print (TyArrow l r) c = print l [" -> ":print r c]
- print (TyArray s a) c = ["{":print s ["}":print a c]]
- print (TyUList s a) c = ["[#":print s ["]":print a c]]
- print (TyUMaybe a) c = ["?#":print a c]
- print (TyNewType i j cons) c = pTyVars i.gtd_name i.gtd_arity
- [": ", j.gcd_name, " ":print (nttype j.gcd_type) c]
- where
- nttype (GenTypeArrow l r) = l
- print (TyRecord i fields) c = pTyVars i.grd_name i.grd_type_arity
- [" {":isperse ", " (pField (\i c->[i.gfd_name, " :: ":c]) fields i.grd_type) ["}":c]]
- print (TyObject i conses) c = pTyVars i.gtd_name i.gtd_arity
- $ [" ":isperse " | " (map pCons conses) c]
- where
- pCons :: (GenericConsDescriptor, [Type]) [String] -> [String]
- pCons (i, ts) c = n [" ":isperse " " (pField (\_->id) [(i, t)\\t<-ts] i.gcd_type) c]
- where
- n c = case i.gcd_prio of
- GenConsNoPrio = [i.gcd_name:c]
- GenConsPrio a s = ["(",i.gcd_name,") infix",case a of
- GenConsAssocRight = "r";
- GenConsAssocLeft = "l"
- _ = "", " ":print s c]
-
-pTyVars :: String Int [String] -> [String]
-pTyVars ty arity c = [":: ", ty, " ":isperse " " (map print ['a'..'a'+toChar (arity-1)]) [" =":c]]
-
-pField :: (a [String] -> [String]) [(a, Type)] GenType -> [[String] -> [String]]
-pField pre [] _ = []
-pField pre [(i, t):xs] (GenTypeArrow l r) = [pre i o print l:pField pre xs r]
-
-instance print GenType
-where
- print (GenTypeVar i) c = print (['a'..] !! i) c
- print t=:(GenTypeApp _ _) c = ["(":isperse " " (collectApps t []) [")":c]]
- where
- collectApps (GenTypeApp l r) c = collectApps l [print r:c]
- collectApps a c = [print a:c]
- print (GenTypeCons s) c = [s:c]
- print (GenTypeArrow l r) c = ["(":print l [" -> ":print r [")":c]]]
-
-instance toString GType where toString a = concat $ print a []
-instance toString Type where toString a = concat $ print a []
-instance toString BasicType where toString a = concat $ print a []
-instance toString ArrayType where toString a = concat $ print a []
-instance toString UListType where toString a = concat $ print a []
-instance toString GenType where toString a = concat $ print a []
-
-isperse :: a [[a] -> [a]] [a] -> [a]
-isperse s m c = foldr id c $ intersperse (\c->[s:c]) m
-
-gTypeToType :: GType -> Type
-gTypeToType (GTyBasic a) = TyBasic a
-gTypeToType (GTyRef a) = TyRef a
-gTypeToType (GTyArrow l r) = TyArrow (gTypeToType l) (gTypeToType r)
-gTypeToType (GTyArray s a) = TyArray s (gTypeToType a)
-gTypeToType (GTyUList s a) = TyUList s (gTypeToType a)
-gTypeToType (GTyUMaybe a) = TyUMaybe (gTypeToType a)
-gTypeToType (GTyRecord i t) = TyRecord i (gtrec t [])
-where
- gtrec :: GType [(GenericFieldDescriptor, Type)] -> [(GenericFieldDescriptor, Type)]
- gtrec (GTyField i t) c = [(i, gTypeToType t):c]
- gtrec (GTyPair l r) c = gtrec l $ gtrec r c
- gtrec _ c = c
-gTypeToType (GTyObject i=:{gtd_num_conses=0} t)
- = TyNewType i (hd i.gtd_conses) (gTypeToType t)
-gTypeToType (GTyObject i t) = TyObject i (gtobj t [])
-where
- gtobj :: GType [(GenericConsDescriptor, [Type])] -> [(GenericConsDescriptor, [Type])]
- gtobj (GTyEither l r) c = gtobj l $ gtobj r c
- gtobj (GTyCons i a) c = [(i, gtcons a []):c]
- gtobj _ c = c
-
- gtcons :: GType [Type] -> [Type]
- gtcons GTyUnit c = c
- gtcons (GTyPair l r) c = gtcons l $ gtcons r c
- gtcons t c = [gTypeToType t:c]
-
-:: FlatMonad :== State FMState GType
-:: FMState = { objects :: [String], types :: [GType], otypes :: [GType], depth :: Int }
-flattenGType :: GType -> [[GType]]
-flattenGType ot
- # {types} = execState (mkf ot) {objects=[], otypes=[], types=[], depth=10}
- = scc [(t, refs t [])\\t<-types]
-where
- refs (GTyObject _ a) c = refs a c
- refs (GTyRecord _ a) c = refs a c
- refs (GTyEither l r) c = refs l $ refs r c
- refs (GTyPair l r) c = refs l $ refs r c
- refs (GTyCons _ a) c = refs a c
- refs (GTyField _ a) c = refs a c
- refs GTyUnit c = c
- refs (GTyArrow l r) c = refs l $ refs r c
- refs (GTyArray _ a) c = refs a c
- refs (GTyUList _ a) c = refs a c
- refs (GTyUMaybe a) c = refs a c
- refs (GTyBasic _) c = c
- refs a=:(GTyRef _) c = [a:c]
-
- write :: (a GType -> GType) a GType -> FlatMonad | genericDescriptorName a
- write cons t a = getState >>= \s
- //We have seen the type but it might've had different arguments
- | isMember name s.objects
- //We have not seen this configuration
- | isEmpty [ot \\ ot<-s.otypes | gTypeEqShallow s.depth ot a]
- = modify (\x->{x & depth=dec x.depth}) *> mkf a *> pure (GTyRef name)
- //If not, just return the basictype
- = pure $ GTyRef name
- //We have not seen the type so we add, calculate and output it
- = cons t <$ modify (\x->{x & otypes=[a:x.otypes], objects=[name:x.objects]}) <*> mkf a
- >>= \ty->addIfNotThere ty >>| pure (GTyRef name)
- where
- name = genericDescriptorName t
-
- addIfNotThere :: GType -> FlatMonad
- addIfNotThere ty = getState >>= \s
- | isMember ty s.types
- = pure ty
- = modify (\s->{s & types=[ty:s.types]}) >>| pure ty
-
- mkf :: GType -> FlatMonad
- mkf (GTyObject t a) = write GTyObject t a
- mkf (GTyRecord t a) = write GTyRecord t a
- mkf (GTyEither l r) = GTyEither <$> mkf l <*> mkf r
- mkf (GTyPair l r) = GTyPair <$> mkf l <*> mkf r
- mkf (GTyCons i a) = GTyCons i <$> mkf a
- mkf (GTyField i a) = GTyField i <$> mkf a
- mkf GTyUnit = pure GTyUnit
- mkf (GTyArrow l r) = GTyArrow <$> mkf l <*> mkf r
- mkf (GTyArray s a) = GTyArray s <$> mkf a
- mkf (GTyUList s a) = GTyUList s <$> mkf a
- mkf (GTyUMaybe a) = GTyUMaybe <$> mkf a
- mkf a=:(GTyBasic _) = addIfNotThere a
- mkf a=:(GTyRef _) = pure a
-
-typeName :: Type -> String
-typeName (TyBasic a) = toString a
-typeName (TyRef a) = a
-typeName (TyArrow l r) = typeName l +++ "->" +++ typeName r
-typeName (TyArray s a) = "{" +++ toString s +++ typeName a +++ "}"
-typeName (TyUList s a) = "[#" +++ toString s +++ typeName a +++ "]"
-typeName (TyUMaybe a) = "?#" +++ typeName a
-typeName (TyNewType i _ _) = i.gtd_name
-typeName (TyObject i _) = i.gtd_name
-typeName (TyRecord i _) = i.grd_name
-
-typeGenType :: Type -> [GenType]
-typeGenType (TyBasic a) = [GenTypeCons $ toString a]
-typeGenType (TyRef a) = [GenTypeCons $ toString a]
-typeGenType (TyArrow l r) = GenTypeArrow <$> typeGenType l <*> typeGenType r
-typeGenType (TyArray s a) = GenTypeApp (GenTypeCons (toString s)) <$> typeGenType a
-typeGenType (TyUList s a) = [GenTypeCons "_#Nil":GenTypeApp (GenTypeCons (toString s)) <$> typeGenType a]
-typeGenType (TyUMaybe a) = [GenTypeCons "_#Nothing":GenTypeApp (GenTypeCons "_#Just") <$> typeGenType a]
-typeGenType (TyNewType _ i a) = [i.gcd_type]
-typeGenType (TyRecord i _) = [i.grd_type]
-typeGenType (TyObject _ fs) = [c.gcd_type\\(c, _)<-fs]
-
-genTypeKind :: [GenType] -> Kind
-genTypeKind ts = foldr (KArrow) KStar $ map snd $ sortBy ((<) `on` fst) $ foldr (\t->gt t id) [] ts
-where
- gt :: GenType (Kind -> Kind) [(Int, Kind)] -> [(Int, Kind)]
- gt (GenTypeCons _) _ ks = ks
- gt (GenTypeVar i) c ks
- # k = c KStar
- = case lookup i ks of
- Nothing = [(i, k):ks]
- Just k`
- | numArr k` > numArr k = ks
- = [(i, k):filter ((<>)i o fst) ks]
- gt (GenTypeArrow l r) _ ks = gt l id $ gt r id ks
- gt (GenTypeApp l r) c ks = gt l ((KArrow) KStar o c) $ gt r id ks
-
-numArr :: Kind -> Int
-numArr KStar = 0
-numArr (l KArrow r) = inc (numArr l + numArr r)
-
-instance == Kind
-where
- (==) KStar KStar = True
- (==) (l1 KArrow r1) (l2 KArrow r2) = l1 == l2 && r1 == r2
- (==) _ _ = False
-instance toString Kind where toString k = concat $ pr k False []
-
-
-pr :: Kind Bool [String] -> [String]
-pr KStar _ c = ["*":c]
-pr (l KArrow r) b c = [if b "(" "":pr l True ["->":pr r False [if b ")" "":c]]]
-
-instance isBuiltin String
-where
- isBuiltin s = [()\\(l, r)<-predef | l == s || r == s] =: [_:_]
-instance isBuiltin Type
-where
- isBuiltin (TyObject i a) = isBuiltin i.gtd_name
- isBuiltin (TyRecord i a) = isBuiltin i.grd_name
- isBuiltin (TyRef a) = isBuiltin a
- isBuiltin _ = True
-instance isBuiltin GType
-where
- isBuiltin (GTyObject i a) = isBuiltin i.gtd_name
- isBuiltin (GTyRecord i a) = isBuiltin i.grd_name
- isBuiltin (GTyRef a) = isBuiltin a
- isBuiltin _ = True
-
-instance isBasic Type
-where
- isBasic (TyBasic t) = True
- isBasic _ = False
-
-instance isBasic GType
-where
- isBasic (GTyBasic t) = True
- isBasic _ = False
-
-instance replaceBuiltins GenericFieldDescriptor
-where
- replaceBuiltins s = {s & gfd_name=replaceBuiltins s.gfd_name}
-instance replaceBuiltins GenericConsDescriptor
-where
- replaceBuiltins s = {s & gcd_name=replaceBuiltins s.gcd_name, gcd_type=replaceBuiltins s.gcd_type}
-instance replaceBuiltins GenericTypeDefDescriptor
-where
- replaceBuiltins s = {s & gtd_name=replaceBuiltins s.gtd_name}
-instance replaceBuiltins GenericRecordDescriptor
-where
- replaceBuiltins s = {s & grd_name=replaceBuiltins s.grd_name, grd_type=replaceBuiltins s.grd_type}
-instance replaceBuiltins String
-where
- replaceBuiltins a = fromMaybe a $ lookup a predef
-instance replaceBuiltins Type
-where
- replaceBuiltins (TyRef a) = TyRef (replaceBuiltins a)
- replaceBuiltins (TyArrow l r) = TyArrow (replaceBuiltins l) (replaceBuiltins r)
- replaceBuiltins (TyArray s a) = TyArray s (replaceBuiltins a)
- replaceBuiltins (TyUList s a) = TyUList s (replaceBuiltins a)
- replaceBuiltins (TyUMaybe a) = TyUMaybe (replaceBuiltins a)
- replaceBuiltins (TyNewType i j a) = TyNewType (replaceBuiltins i) (replaceBuiltins j) (replaceBuiltins a)
- replaceBuiltins (TyObject i cs) = TyObject (replaceBuiltins i) [(replaceBuiltins i, map replaceBuiltins fs)\\(i, fs)<-cs]
- replaceBuiltins (TyRecord j fs) = TyRecord (replaceBuiltins j) [(replaceBuiltins i, replaceBuiltins a)\\(i, a)<-fs]
- replaceBuiltins t = t
-instance replaceBuiltins GType
-where
- replaceBuiltins (GTyEither l r) = GTyEither (replaceBuiltins l) (replaceBuiltins r)
- replaceBuiltins (GTyPair l r) = GTyPair (replaceBuiltins l) (replaceBuiltins r)
- replaceBuiltins (GTyArrow l r) = GTyArrow (replaceBuiltins l) (replaceBuiltins r)
- replaceBuiltins (GTyArray s a) = GTyArray s (replaceBuiltins a)
- replaceBuiltins (GTyUList s a) = GTyUList s (replaceBuiltins a)
- replaceBuiltins (GTyUMaybe a) = GTyUMaybe (replaceBuiltins a)
- replaceBuiltins (GTyObject i a) = GTyObject (replaceBuiltins i) (replaceBuiltins a)
- replaceBuiltins (GTyRecord i a) = GTyRecord (replaceBuiltins i) (replaceBuiltins a)
- replaceBuiltins (GTyCons i a) = GTyCons (replaceBuiltins i) (replaceBuiltins a)
- replaceBuiltins (GTyField i a) = GTyField (replaceBuiltins i) (replaceBuiltins a)
- replaceBuiltins (GTyRef a) = GTyRef (replaceBuiltins a)
- replaceBuiltins a = a
-instance replaceBuiltins GenType
-where
- replaceBuiltins (GenTypeCons a) = GenTypeCons (replaceBuiltins a)
- replaceBuiltins (GenTypeApp l r) = GenTypeApp (replaceBuiltins l) (replaceBuiltins r)
- replaceBuiltins (GenTypeArrow l r) = GenTypeArrow (replaceBuiltins l) (replaceBuiltins r)
- replaceBuiltins a = a
-
-predef :: [(String, String)]
-predef =:
- [ ("_List", "[]"), ("_Cons", "(:)"), ("_Nil", "[]")
- , ("_!List", "[! ]"), ("_!Cons", "(:)"), ("_!Nil", "[! ]")
- , ("_List!", "[ !]"), ("_Cons!", "(:)"), ("_Nil!", "[ !]")
- , ("_!List!", "[!!]"), ("_!Cons!", "(:)"), ("_!Nil!", "[ !]")
- , ("_#List", "[#]"), ("_#Cons", "(:)"), ("_#Nil", "[#]")
- , ("_#List!", "[#!]"), ("_#Cons!", "(:)"), ("_#Nil!", "[#!]")
- , ("_!Maybe", "?"), ("_!Just", "?Just"), ("_!Nothing", "?None")
- , ("_Maybe", "?^"), ("_Just", "?^Just"), ("_Nothing", "?^None")
- , ("_Array", "{}"), ("_!Array", "{!}"), ("_#Array", "{#}"), ("_32#Array", "{32#}")
- , ("_Unit", "()")
- :[("_Tuple" +++ toString i, "(" +++ createArray i ',' +++")")\\i<-[2..32]]]
-
-generic type a :: Box GType a
-gType{|UNIT|} = box GTyUnit
-gType{|EITHER|} l r = box $ GTyEither (unBox l) (unBox r)
-gType{|PAIR|} l r = box $ GTyPair (unBox l) (unBox r)
-gType{|CONS of gcd|} a = box $ GTyCons gcd $ unBox a
-gType{|FIELD of gfd|} a = box $ GTyField gfd $ unBox a
-gType{|OBJECT of gtd|} a = box $ GTyObject gtd $ unBox a
-gType{|RECORD of grd|} a = box $ GTyRecord grd $ unBox a
-gType{|Int|} = box $ GTyBasic BTInt
-gType{|Bool|} = box $ GTyBasic BTBool
-gType{|Real|} = box $ GTyBasic BTReal
-gType{|Char|} = box $ GTyBasic BTChar
-gType{|World|} = box $ GTyBasic BTWorld
-//gType{|Dynamic|} = box $ GTyBasic BTDynamic
-gType{|File|} = box $ GTyBasic BTFile
-gType{|(->)|} l r = box $ GTyArrow (unBox l) (unBox r)
-gType{|[#]|} a = box $ GTyUList ULLazy $ unBox a
-gType{|[#!]|} a = box $ GTyUList ULStrict $ unBox a
-gType{|{}|} a = box $ GTyArray ALazy $ unBox a
-gType{|{!}|} a = box $ GTyArray AStrict $ unBox a
-gType{|{#}|} a = box $ GTyArray AUnboxed $ unBox a
-gType{|{32#}|} a = box $ GTyArray APacked $ unBox a
-gType{|(?#)|} a = box $ GTyUMaybe $ unBox a
-derive gType ?, ?^
-derive gType [], [! ], [ !], [!!]
-derive gType (), (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,)
+++ /dev/null
-definition module GenType.CParser
-
-from Data.Either import :: Either
-from GenType import :: Type
-
-/**
- * Generate a single parser for a type.
- * This does not terminate for a recursive type
- */
-flatParser :: Type -> Either String ([String], [String])
-
-/**
- * generate parsers for the types grouped by strongly connected components
- */
-parsers :: [[Type]] -> Either String ([String], [String])
+++ /dev/null
-implementation module GenType.CParser
-
-import Control.Applicative
-import Control.Monad
-import Control.Monad.Fail
-import Control.Monad.Reader
-import Control.Monad.State
-import Control.Monad.Trans
-import Control.Monad.Writer
-import Data.Either
-import Data.Func
-import Data.Functor
-import Data.List
-import qualified Data.Map
-from Data.Map import :: Map(..)
-import Data.Maybe
-import Data.Tuple
-import StdEnv
-import qualified Text
-from Text import class Text(concat), instance Text String
-
-import GenType
-import GenType.CType
-
-instance MonadFail (Either String) where fail s = Left s
-:: FPMonad :== WriterT [String] (ReaderT Int (Either String)) ()
-
-indent c = liftT ask >>= \i->tell [createArray i '\t':c]
-
-parsefun t c = ["parse_", safe (typeName t):c]
-
-(<.>) infixr 6
-(<.>) a b = a +++ "." +++ b
-
-(<->) infixr 6
-(<->) a b = a +++ "->" +++ b
-
-result r op s = indent [r, " ", op, " ", s, ";\n"]
-assign r s = result r "=" s
-parsename s = "parse_" +++ safe s
-tail = ["\treturn r;\n}\n"]
-parsenameimp t c def = def t [" {\n\t":ctypename t [" ", c, "\n\n"]]
-ctypename t c = [prefix t, safe (typeName t):c]
-
-flatParser :: Type -> Either String ([String], [String])
-flatParser t = tuple (parsedef [";\n"]) <$> runReaderT (execWriterT (tell (parsenameimp t "r;" \_->parsedef) >>| fpd t True "r" >>| tell tail)) 1
-where
- parsedef c = ctypename t [" ":parsefun t ["(uint8_t (*get)())":c]]
-
- fpd :: Type Bool String -> FPMonad
- fpd (TyRef s) tl r = assign r (parsename s)
- fpd (TyBasic t) tl r
- | tl = pure ()
- = case t of
- BTInt = assign r "(int64_t)get()<<54"
- >>| result r "+=" "(int64_t)get()<<48"
- >>| result r "+=" "(int64_t)get()<<40"
- >>| result r "+=" "(int64_t)get()<<32"
- >>| result r "+=" "(int64_t)get()<<24"
- >>| result r "+=" "(int64_t)get()<<16"
- >>| result r "+=" "(int64_t)get()<<8"
- >>| result r "+=" "(int64_t)get()"
- BTChar = assign r "(char)get()"
-// BTReal = assign r "double"
- BTBool = assign r "(bool)get()"
- t = fail $ "flatParse: there is no basic type for " +++ toString t
- fpd (TyArrow _ _) tl r = fail $ "flatParser: function cannot be serialized"
- fpd (TyNewType ti ci a) tl r = fpd a tl r
- fpd (TyArray _ _) tl r = fail $ "flatParser: arrays are not supported since they require dynamic memory"
- fpd (TyRecord ti fs) tl r
- = mapM_ (fmtField) [(r <.> fi.gfd_name, ty)\\(fi, ty)<-fs]
- //Enumeration
- fpd (TyObject ti fs) tl r
- | and [t =: [] \\ (_, t)<-fs]
- = assign r $ "(" +++ consName ti +++ ") get()"
- //Single constructor, single field (box)
- fpd (TyObject ti [(ci, [ty])]) tl r = fpd ty tl r
- //Single constructor
- fpd (TyObject ti [(ci, ts)]) tl r
- = mapM_ fmtField [(r <.> "f" +++ toString i, ty)\\i<-[0..] & ty<-ts]
- //Complex adt
- fpd (TyObject ti fs) tl r
- = assign (r <.> "cons") ("(" +++ consName ti +++ ") get()")
- >>| indent ["switch (", r <.> "cons){\n"]
- >>| mapM_ fmtCons fs
- >>| indent ["}\n"]
- where
- fmtCons :: (GenericConsDescriptor,[Type]) -> FPMonad
- fmtCons (ci, ts) = indent ["case ", safe ci.gcd_name, ":\n"]
- >>| mapM_ (mapWriterT (local inc) o fmtField) [(cs i, ty) \\i<-[0..] & ty<-ts]
- >>| mapWriterT (local inc) (indent ["break;\n"])
- where
- cs i = r <.> "data" <.> safe ci.gcd_name +++ if (ts=:[_]) "" (".f" +++ toString i)
- fpd t tl r = fail $ "flatParser: unsupported " +++ toString t
-
- fmtField :: (String, Type) -> FPMonad
- fmtField (name, ty) = fpd ty False name
-
-:: TPMonad :== WriterT [String] (StateT TPState (Either String)) ()
-:: TPState :== 'Data.Map'.Map String (String, Bool)
-parsers :: [[Type]] -> Either String ([String], [String])
-parsers ts = tuple (parsedefs ts) <$> evalStateT (execWriterT $ mapM_ parsergroup ts) 'Data.Map'.newMap
-where
- parsedefs :: ([[Type]] -> [String])
- parsedefs = foldr (\t c->parsedef t [";\n":c]) [] o flatten
-
- parsedef :: Type [String] -> [String]
- parsedef t c = ctypename t [" *":parsefun t ["(uint8_t (*get)()":pks (typeKind t) True [")":c]]]
- where
- pks :: Kind Bool [String] -> [String]
- pks k tl c = foldr (\(i, k) c->pd k tl i c) c $ zip2 [0..] $ typeArgs k
-
- pd :: Kind Bool Int [String] -> [String]
- pd KStar tl i c = [", void *(*", if tl ("parse_"+++toString i) "", ")(uint8_t (*)())":c]
- pd (l KArrow r) tl i c =
- [ ", void *(*", if tl ("parse_"+++toString i) "", ")(uint8_t (*)()"
- : pks l False $ pd r False (inc i) [")":c]]
-
- typeArgs :: Kind -> [Kind]
- typeArgs KStar = []
- typeArgs (l KArrow r) = [l:typeArgs r]
-
- parsergroup :: [Type] -> TPMonad
- parsergroup ts
- = liftT (modify ('Data.Map'.putList [(typeName ty, (prefix ty, True))\\ty<-ts]))
- >>| mapM_ (\t->tell (parsenameimp t (declaration t) parsedef) >>| parser t >>| tell ["\n":tail]) ts
- where
- declaration t = concat ["*r = (":ctypename t [" *)malloc(sizeof(":ctypename t ["));"]]]
-
- printTypeName :: String -> TPMonad
- printTypeName tname
- = liftT (gets (\s->maybe [safe tname, " "] (\(p, b)->[p, safe tname, if b " *" " "]) $ 'Data.Map'.get tname s))
- >>= tell
-
- parser :: Type -> TPMonad
- parser t=:(TyRef s) = tell $ parsefun t []
- parser (TyBasic t)
- = case t of
- BTInt = tell ["\t*r = (Int)get()<<54;\n"
- , "\t*r += (Int)get()<<48;\n"
- , "\t*r += (Int)get()<<40;\n"
- , "\t*r += (Int)get()<<32;\n"
- , "\t*r += (Int)get()<<24;\n"
- , "\t*r += (Int)get()<<16;\n"
- , "\t*r += (Int)get()<<8;\n"
- , "\t*r += (Int)get();\n"]
- BTChar = tell ["\t*r = (Char)get();\n"]
- BTBool = tell ["\t*r = (Bool)get();\n"]
- //BTReal = tell ["\t*r = double;\n"]
- t = fail $ "parser: there is no basic type for " +++ toString t
- parser (TyArrow _ _) = fail $ "parser: function cannot be serialized"
- parser (TyNewType ti ci a) = parser a
- parser (TyArray _ _) = fail $ "parser: arrays are not supported since they require dynamic memory"
- parser (TyRecord ti fs)
- = fmtFields 1 ti.grd_type ["r" <-> fi.gfd_name\\(fi, _)<-fs]
- //Enumeration
- parser (TyObject ti fs)
- | and [t =: [] \\ (_, t)<-fs]
- = tell ["\t*r = (", consName ti, ") get();\n"]
- //Single constructor, single field (box)
- parser (TyObject ti [(ci, [ty])]) = tell ["\t*r = ":fmtField ci.gcd_type [");\n"]]
- //Single constructor
- parser t=:(TyObject ti [(ci, ts)])
- = fmtFields 1 ci.gcd_type ["r" <-> "f" +++ toString i\\i<-indexList ts]
- //Complex adt
- parser (TyObject ti fs)
- = tell ["\tr" <-> "cons = (", consName ti, ") get();\n"]
- >>| tell ["\tswitch(r" <-> "cons) {\n"]
- >>| mapM_ fmtCons fs
- >>| tell ["\t}\n"]
- where
- fmtCons :: (GenericConsDescriptor,[Type]) -> TPMonad
- fmtCons (ci, ts) = tell ["\tcase ", safe ci.gcd_name, ":\n"]
- >>| fmtFields 2 ci.gcd_type [cs i\\i<-[0..] & ty<-ts]
- >>| tell ["\t\tbreak;\n"]
- where
- cs i = "r" <-> "data" <.> safe ci.gcd_name +++ if (ts=:[_]) "" ("" <-> "f" +++ toString i)
- parser t = fail $ "parser: unsupported type " +++ toString t
-
- fmtFields :: Int GenType [String] -> TPMonad
- fmtFields i _ [] = pure ()
- fmtFields i (GenTypeArrow l r) [x:xs]
- = tell [createArray i '\t', x, " = "] >>| tell (fmtField l []) >>| tell [");\n"] >>| fmtFields i r xs
-
- fmtField :: GenType [String] -> [String]
- fmtField (GenTypeCons a) c = ["parse_", safe a, "(get":c]
- fmtField (GenTypeVar a) c = ["parse_", toString a, "(get":c]
- fmtField t=:(GenTypeApp _ _) c = ufold t c
- where
- ufold (GenTypeApp l r) c = ufold l [", ":fmtField r [")":c]]
- ufold t c = fmtField t c
+++ /dev/null
-definition module GenType.CType
-
-from StdGeneric import :: GenericTypeDefDescriptor
-from Data.Either import :: Either
-from GenType import :: Type
-
-/**
- * generate typedefs for the types grouped by strongly connected components
- */
-typedefs :: [[Type]] -> Either String [String]
-
-/**
- * Generate a single typedef for a type.
- * This does not terminate for recursive types
- */
-flatTypedef :: Type -> Either String [String]
-
-/**
- * Create a C-safe type name
- */
-safe :: String -> String
-
-/**
- * Return the C type prefix, e.g. struct, enum
- */
-prefix :: Type -> String
-
-/**
- * Return the C constructorname
- */
-consName :: GenericTypeDefDescriptor -> String
+++ /dev/null
-implementation module GenType.CType
-
-import Control.Applicative
-import Control.Monad
-import Control.Monad.Fail
-import Control.Monad.Reader
-import Control.Monad.State
-import Control.Monad.Trans
-import Control.Monad.Writer
-import Data.Either
-import Data.Func
-import Data.Functor
-import Data.List
-import qualified Data.Map
-from Data.Map import :: Map(..)
-import Data.Maybe
-import Data.Tuple
-import StdEnv
-import qualified Text
-from Text import class Text(concat), instance Text String
-
-import GenType
-
-instance MonadFail (Either String) where fail s = Left s
-
-safe :: String -> String
-safe s = concat [fromMaybe {c} $ lookup c cs\\c <-:s]
-where
- cs = [('~', "Tld"), ('@', "At"), ('#', "Hsh"), ('$', "Dlr"), ('%', "Prc")
- ,('^', "Hat"), ('?', "Qtn"), ('!', "Bng"), (':', "Cln"), ('+', "Pls")
- ,('-', "Min"), ('*', "Ast"), ('<', "Les"), ('>', "Gre"), ('\\', "Bsl")
- ,('/', "Slh"), ('|', "Pip"), ('&', "Amp"), ('=', "Eq"), ('.', "Dot")]
-
-prefix :: Type -> String
-prefix (TyRecord _ _) = "struct "
-prefix (TyObject _ fs)
- | and [t =: [] \\ (_, t)<-fs] = "enum "
- | fs =: [(_, [_])] = ""
- | fs =: [_] = "struct "
- = "struct "
-prefix _ = ""
-
-consName :: GenericTypeDefDescriptor -> String
-consName s = "enum " +++ safe s.gtd_name +++ "_cons"
-
-iindent = mapWriterT $ mapStateT $ local inc
-indent c = liftT (liftT ask) >>= \i->tell [createArray i '\t':c]
-
-:: FTMonad :== WriterT [String] (StateT [(String, [String])] (ReaderT Int (Either String))) ()
-flatTypedef :: Type -> Either String [String]
-flatTypedef t = (\(w, es)->flatten (map snd es) ++ w)
- <$> runReaderT (runStateT (execWriterT (ftd t True )) []) 0
-where
- ftd :: Type Bool -> FTMonad
- ftd (TyRef s) tl = indent [s]
- ftd (TyBasic t) tl
- | tl = pure ()
- = case t of
- BTInt = indent ["int64_t"]
- BTChar = indent ["char"]
- BTReal = indent ["double"]
- BTBool = indent ["bool"]
- t = fail $ "flatTypedef: there is no basic type for " +++ toString t
- ftd (TyArrow l r) tl = fail "flatTypedef: functions cannot be serialized"
- ftd (TyNewType ti ci a) tl = ftd a tl
- ftd (TyArray _ a) tl = indent ["*"] >>| ftd a tl
- ftd (TyRecord ti fs) tl
- = indent ["struct ", if tl (safe ti.grd_name) "", " {\n"
- ] >>| mapM_ (iindent o fmtField) [(fi.gfd_name, ty)\\(fi, ty)<-fs]
- >>| indent ["}\n"]
- //Enumeration
- ftd (TyObject ti fs) tl
- | and [t =: [] \\ (_, t)<-fs]
- | tl = pure ()
- = indent [] >>| enum ti fs
- //Single constructor, single field (box)
- ftd (TyObject ti [(ci, [ty])]) tl = ftd ty tl
- //Single constructor
- ftd (TyObject ti [(ci, ts)]) tl
- = indent ["struct ", if tl (safe ti.gtd_name) "", " {\n"]
- >>| mapM_ (iindent o fmtField) [("f" +++ toString i, ty)\\i<-[0..] & ty<-ts]
- >>| indent ["}"]
- //Complex adt
- ftd (TyObject ti fs) tl
- = indent ["struct ", if tl (safe ti.gtd_name) "", " {\n"]
- >>| iindent (indent []) >>| enum ti fs >>| tell [" cons;\n"]
- >>| iindent (indent ["struct {\n"])
- >>| mapM_ (iindent o iindent o fmtCons) fs
- >>| iindent (indent ["} data;\n"])
- >>| indent ["}", if tl ";" ""]
- where
- fmtCons (ci, []) = pure ()
- fmtCons (ci, [t]) = ftd t False >>| tell [" ", safe ci.gcd_name, ";\n"]
- fmtCons (ci, ts)
- = indent ["struct {\n"]
- >>| mapM_ (iindent o fmtField) [("f" +++ toString i, ty)\\i<-[0..] & ty<-ts]
- >>| indent ["} ", safe ci.gcd_name, ";\n"]
- ftd t tl = fail $ "cannot flatTypedef: " +++ toString t
-
- enum :: GenericTypeDefDescriptor [(GenericConsDescriptor, [Type])] -> FTMonad
- enum ti fs = liftT (gets (lookup ti.gtd_name)) >>= \e->case e of
- ?None = liftT (modify \s->[(ti.gtd_name, [consName ti, " {", 'Text'.join ", " [safe ci.gcd_name\\(ci, _)<-fs], "};\n"]):s]) >>| enum ti fs
- ?Just _ = tell [consName ti]
-
- fmtField :: (String, Type) -> FTMonad
- fmtField (name, ty) = ftd ty False >>| tell [" ", name, ";\n"]
-
-:: TDMonad :== WriterT [String] (StateT TDState (Either String)) ()
-:: TDState :== ('Data.Map'.Map String (String, Bool), [String])
-typedefs :: [[Type]] -> Either String [String]
-typedefs ts = (\(text, (_, enums))->enums ++ text)
- <$> runStateT (execWriterT (mapM_ typedefgroup ts)) ('Data.Map'.newMap, [])
-where
- typedefgroup :: [Type] -> TDMonad
- typedefgroup ts
- = liftT (modify (appFst $ 'Data.Map'.putList [(typeName ty, (prefix ty, False))\\ty<-ts]))
- >>| mapM_ (\x->printTypeName x >>| tell [";\n"]) (if (ts=:[_,_:_]) (map typeName ts) [])
- >>| liftT (modify (appFst $ flip (foldr $ 'Data.Map'.alter (fmap (fmap \_->True)) o typeName) ts))
- >>| mapM_ (\t->typedef t >>| tell ["\n"]) ts
-
- printTypeName :: String -> TDMonad
- printTypeName tname
- = liftT (gets $ maybe [safe tname, " "] (\(p, b)->[p, safe tname, if b " *" " "]) o 'Data.Map'.get tname o fst)
- >>= tell
-
- typedef :: Type -> TDMonad
- typedef (TyRef s) = printTypeName s
- typedef (TyBasic t) = case t of
- BTInt = tell ["typedef uint64_t Int;"]
- BTChar = tell ["typedef char Char;"]
- BTReal = tell ["typedef double Real;"]
- BTBool = tell ["typedef bool Bool;"]
- t = fail $ "basic type: " +++ toString t +++ " not implemented"
- typedef (TyArray _ a) = tell ["*"] >>| typedef a
- typedef t=:(TyNewType ti ci a)
- = tydef ti.gtd_name ci.gcd_type
- typedef t=:(TyRecord ti fs)
- = tell ["struct ", safe ti.grd_name, " {\n"]
- >>| fmtFields 1 ti.grd_type [fi.gfd_name\\(fi, _)<-fs]
- >>| tell ["};\n"]
- //Enumeration
- typedef t=:(TyObject ti fs)
- | and [t =: [] \\ (_, t)<-fs] = enum ti fs >>| tell [";\n"]
- //[consName ti, " {", 'Text'.join ", " [safe ci.gcd_name\\(ci, _)<-fs], "};\n"]
- //Single constructor, single field (box)
- typedef t=:(TyObject ti [(ci, [ty])]) = tydef ti.gtd_name ci.gcd_type
- //Single constructor
- typedef t=:(TyObject ti [(ci, ts)])
- = tell ["struct ", safe ti.gtd_name, " {\n"]
- >>| fmtFields 1 ci.gcd_type ["f" +++ toString i\\i<-indexList ts]
- >>| tell ["};\n"]
- //Complex adt
- typedef t=:(TyObject ti fs) = tell
- ["struct ", safe ti.gtd_name, " {\n\t"]
- >>| enum ti fs >>| tell [" cons;\n\tstruct {\n"]
- //, consName ti, " {", 'Text'.join ", " [safe ci.gcd_name\\(ci, _)<-fs], "} cons;\n"
- >>| mapM_ fmtCons fs
- >>| tell ["\t} data;\n};\n"]
- where
- fmtCons :: (GenericConsDescriptor, [Type]) -> TDMonad
- fmtCons (ci, []) = pure ()
- fmtCons (ci, [t]) = fmtFields 2 ci.gcd_type [safe ci.gcd_name]
- fmtCons (ci, ts) = tell ["\t\tstruct {\n"]
- >>| fmtFields 3 ci.gcd_type ["f" +++ toString i\\i<-indexList ts]
- >>| tell ["\t\t} ", safe ci.gcd_name, ";\n"]
- typedef t = fail $ toString t +++ " not implemented"
-
- enum :: GenericTypeDefDescriptor [(GenericConsDescriptor, [Type])] -> TDMonad
- enum ti fs = liftT (modify (appSnd \xs->[consName ti, " {", 'Text'.join ", " [safe ci.gcd_name\\(ci, _)<-fs], "};\n":xs]))
- >>| tell [consName ti]
-
- tydef :: String GenType -> TDMonad
- tydef name (GenTypeArrow l r) = tell ["typedef "] >>| fmtField "" l >>| tell [safe name,";\n"]
-
- fmtFields :: Int GenType [String] -> TDMonad
- fmtFields i _ [] = pure ()
- fmtFields i (GenTypeArrow l r) [x:xs]
- = tell [createArray i '\t'] >>| fmtField x l >>| tell [";\n"] >>| fmtFields i r xs
-
- fmtField :: String GenType -> TDMonad
- fmtField x (GenTypeCons a) = printTypeName a >>| tell [x]
- fmtField x (GenTypeVar a) = tell ["void *",x]
- fmtField x (GenTypeApp l r) = fmtField x l
- fmtField x t=:(GenTypeArrow _ _)
- = mapM (fmap (concat o snd) o listen o fmtField "") (collectArgs t [])
- >>= \[r:as]->tell [r, " (*",x,")(",'Text'.join ", " as, ")"]
- where
- collectArgs (GenTypeArrow l r) c = collectArgs r (c ++ [l])
- collectArgs t c = [t:c]
:: PViewT m a :== StateT [NRequest m] m a
:: NRequest m = NRequest String (m ()) Dynamic
+//* @type :: String (m ()) p [NRequest] -> [NRequest] | TC p
+nrequestc p id hnd s :== [NRequest id hnd (dynamic p):s]
+
+//* Used to force kinds of variables in a
+:: KindHelper a b :== b
//* Read a share with one rewrite step
class read v :: (v m p r w) p -> PViewT m (ReadResult m p r w) | Monad m
//* Write a share with one rewrite step
-class write v :: (v m p r w) p w -> PViewT m (WriteResult m p r w) | Monad m
+class write v :: (v m p r w) p w -> PViewT m (WriteResult m p r w) | Monad m & TC p
+//* Generate a unique name
+class identity v :: (v m p r w) (KindHelper (m ()) [String]) -> [String]
//* Observe a share and get notified when it happens
-class observe v
-where
- identity :: (v m p r w) [String] -> [String]
- observe :: (v m p r w) p String (m ()) -> PViewT m () | Monad m & TC p
+class observe v :: (v m p r w) p String (m ()) -> PViewT m () | Monad m & TC p
//* Result of a single read rewrite
:: ReadResult m p r w
- = Read r //* done reading
+ = Read (KindHelper (m ()) r) //* done reading
| E.sds: Reading (sds m p r w) & read sds //* not done reading
- | ReadResultUnused (m ())
//* Result of a single write rewrite
:: WriteResult m p r w
- = Written () //* done writing
+ = Written (KindHelper (m ()) ()) //* done writing
| E.sds: Writing (sds m p r w) & write sds //* not done writing
- | WriteResultUnused (m ())
//* Read lens, it can choose to ignore the source
:: LensRead m p r rs
| LensWriteConst (p w -> m (? ws))
//* Box type, to get rid of a possible complex constructor of combinators
-:: SDS m p r w = E.sds: SDS (sds m p r w) (m ()) /*force kind*/ & read, write, observe sds
-sds :: (sds m p r w) -> SDS m p r w | read, write, observe sds & Monad m
+:: SDS m p r w = E.sds: SDS (KindHelper (m ()) (sds m p r w)) & read, write, identity, observe sds
+sds :: (sds m p r w) -> SDS m p r w | read, write, identity, observe sds & Monad m
instance read SDS
instance write SDS
+instance identity SDS
instance observe SDS
//* Read a share completely
//* Update a share completely
updShare :: (r -> w) (sds m () r w) -> PViewT m w | Monad m & read sds & write sds & TC r & TC w
+
+//* Trigger observing tasks
+trigger :: (v m p r w) (p -> Bool) -> PViewT m () | identity v & TC p & Monad m
import Control.Monad
import Control.Monad.State
import Control.Monad.Trans
+from Text import class Text(concat), instance Text String
import ASDS.Source
import ASDS.Lens
import ASDS.Select
import ASDS.Parallel
-sds :: (sds m p r w) -> SDS m p r w | read, write, observe sds & Monad m
-sds s = SDS s (pure ())
+sds :: (sds m p r w) -> SDS m p r w | read, write, identity, observe sds & Monad m
+sds s = SDS s
-instance read SDS where read (SDS s _) p = read s p
-instance write SDS where write (SDS sds _) p w = write sds p w
-instance observe SDS
-where
- identity (SDS sds _) c = identity sds c
- observe (SDS sds _) p oid handle = observe sds p oid handle
+instance read SDS where read (SDS s) p = read s p
+instance write SDS where write (SDS sds) p w = write sds p w
+instance identity SDS where identity (SDS sds) c = identity sds c
+instance observe SDS where observe (SDS sds) p oid handle = observe sds p oid handle
getShare :: (sds m () r w) -> PViewT m r | Monad m & read sds & TC r & TC w
getShare s = read s () >>= \v->case v of
updShare :: (r -> w) (sds m () r w) -> PViewT m w | Monad m & read sds & write sds & TC r & TC w
updShare f s = f <$> getShare s >>= \v->setShare v s >>| liftT (pure v)
-trigger :: (p -> Bool) -> PViewT m () | TC p & Monad m
-trigger inv = gets (filter (match inv)) >>= mapM_ run
+trigger :: (v m p r w) (p -> Bool) -> PViewT m () | identity v & TC p & Monad m
+trigger sds inv = gets (filter (match (concat (identity sds [])) inv)) >>= mapM_ run
where
- match :: (p -> Bool) (NRequest m) -> Bool | TC p
- match inv (NRequest oid ohnd (a :: p^)) = inv a
- match _ _ = False
+ match :: String (p -> Bool) (NRequest m) -> Bool | TC p
+ match id inv (NRequest oid ohnd (a :: p^)) = id == oid && inv a
+ match _ _ _ = False
run :: (NRequest m) -> PViewT m () | Monad m
run (NRequest oid ohnd _) = liftT ohnd
// Write the share but only if the given value is a Just.
// If it is None, pretend that the value was written
-write` :: (sds m p r w) p (m (? w)) -> PViewT m (WriteResult m p r w) | TC w & Monad m & write sds
+write` :: (sds m p r w) p (m (? w)) -> PViewT m (WriteResult m p r w) | TC w & Monad m & write sds & TC p
write` sds p mmv = liftT mmv >>= \mv->case mv of
?None = liftT $ pure $ Written ()
?Just v = write sds p v
definition module ASDS.Source
-from ASDS import class read, class write, class observe
+from ASDS import class read, class write, class observe, class identity, :: KindHelper
from Control.Monad import class Monad
from Control.Applicative import class Applicative, class <*>, class pure
from Data.Functor import class Functor
:: ReadSource m p r w = ReadSource (p -> m r)
//* Just write something
-:: WriteSource m p r w = WriteSource (p w -> m ())
+:: WriteSource m p r w = WriteSource String (p w -> m (p -> Bool))
//* Pair a two shares to form a read/write sds that only touches one share per action
-:: RWPair sdsr sdsw m p r w = RWPair (sdsr m p r w) (sdsw m p r w) (m ())
-rwpair :: (sdsr m p r w) (sdsw m p r w) -> RWPair sdsr sdsw m p r w | pure m
+:: RWPair sdsr sdsw m p r w = RWPair (KindHelper (m ()) (sdsr m p r w)) (sdsw m p r w)
+rwpair :: (sdsr m p r w) (sdsw m p r w) -> RWPair sdsr sdsw m p r w
//* Special type of RWPair that contains sds sources
:: Source m p r w :== RWPair ReadSource WriteSource m p r w
-source :: (p -> m r) (p w -> m ()) -> Source m p r w | pure m
+source :: String (p -> m r) (p w -> m (p -> Bool)) -> Source m p r w
instance read ReadSource, (RWPair sdsr sdsw) | read sdsr
instance write WriteSource, (RWPair sdsr sdsw) | write sdsw
+instance identity WriteSource, (RWPair sdsr sdsw) | identity sdsw
instance observe WriteSource, (RWPair sdsr sdsw) | observe sdsw
//* Immediately returns the given value on a read
import Control.Monad.Trans
import ASDS
-rwpair :: (sdsr m p r w) (sdsw m p r w) -> RWPair sdsr sdsw m p r w | pure m
-rwpair l r = RWPair l r (pure ())
+rwpair :: (sdsr m p r w) (sdsw m p r w) -> RWPair sdsr sdsw m p r w
+rwpair l r = RWPair l r
-source :: (p -> m r) (p w -> m ()) -> Source m p r w | pure m
-source read write = rwpair (ReadSource read) (WriteSource write)
+source :: String (p -> m r) (p w -> m (p -> Bool)) -> Source m p r w
+source name read write = rwpair (ReadSource read) (WriteSource name write)
instance read ReadSource
where
instance write WriteSource
where
- write (WriteSource write) p w = Written <$> liftT (write p w)
+ write s=:(WriteSource _ write) p w = liftT (write p w)
+ >>= trigger s >>| pure (Written ())
+
+instance identity WriteSource
+where
+ identity (WriteSource n _) c = [n:c]
instance observe WriteSource
where
- observe sds p oid hnd = modify \s->[NRequest oid hnd (dynamic p):s]
+ observe sds p oid hnd = modify (nrequestc p oid hnd)
instance read (RWPair sdsr sdsw) | read sdsr
where
- read (RWPair s w _) p = read s p >>= \v->case v of
+ read (RWPair s w) p = read s p >>= \v->case v of
Reading s = pure $ Reading (rwpair s w)
Read r = pure $ Read r
instance write (RWPair sdsr sdsw) | write sdsw
where
- write (RWPair r s _) p w = write s p w >>= \v->case v of
+ write (RWPair r s) p w = write s p w >>= \v->case v of
Writing s = pure $ Writing $ rwpair r s
Written _ = pure $ Written ()
+instance identity (RWPair sdsr sdsw) | identity sdsw
+where
+ identity (RWPair r w) c = identity w c
+
instance observe (RWPair sdsr sdsw) | observe sdsw
where
- observe (RWPair r s _) p oid hnd = observe s p oid hnd
+ observe (RWPair r s) p oid hnd = observe s p oid hnd
constShare :: a -> ReadSource m p a b | pure m
constShare a = ReadSource \_->pure a
nullShare :: WriteSource m p a b | pure m
-nullShare = WriteSource \_ _->pure ()
+nullShare = WriteSource "null" \_ _->pure \_->False
import StdEnv
import Data.Either
import Data.Func
+import Data.Functor
import Data.Functor.Identity
from Data.Map import :: Map(..)
import qualified Data.Map
import Control.Monad.State
import Control.Monad.Fail
import Control.Monad.Trans
+import System.IO
import ASDS
import ASDS.Source
equal expected mon = mon >>= \v->if (v == expected) (pure ()) (fail "Not equal")
//Start :: Either String (((), [NRequest Identity)]), Map String Dynamic)
-Start = runIdentity (runStateT (observe intsource () "observeid" (pure ()) >>| setShare 42 intsource) [])
+Start w = /*eval*/execIO (runStateT (observe intsource () "int" (putStrLn "blurp" >>| pure ()) >>| setShare 42 intsource) []) w
+
+import Debug.Trace
intsource :: Source m () Int Int | pure m
-intsource = source (\_->pure 42) (\_ _->pure ())
+intsource = source "int" (\_->pure 42) (\_ _->pure (\_->True))
/*
//Start :: Either String ((), Map String Dynamic)
dstore = translate (\i->((), i)) $ keyedStore store
store :: Source (StateT (Map String Dynamic) m) () (Map String Dynamic) (Map String Dynamic) | Monad m
-store = source (\_->getState) \_->put
+store = source "store" (\p->getState) \p w->(\p->True) <$ put w
repositories / clean-tests.git / commitdiff