darcs - DrHylo

1 module FunctorOf (

2 getCtx

3 , functorOfInst

4 , getSeed

5 , hsPat2Exp

6 , typeable

7 , observable

8 ) where

10 import Data.Map hiding (map)

11 import Data.List

12 import Data.Maybe

13 import Language.Haskell.Exts.Syntax as Exts

15 import Control.Monad.State

16 import Data.Char (isUpper)

17 import Data.Generics hiding (Unit,Inl,Inr)

19 import Language.Haskell.Exts.Parser

20 import Language.Haskell.Exts.Pretty

22 import Language.Pointwise.Parser (hsPat2Exp)

23 import Language.Pointwise.Syntax as Pointwise hiding (swap)

25 -- Associates a constructor to definition

27 type Ctx = [(String,Term)]

29 getCtx :: Module -> Ctx

30 getCtx (Module _ _ _ _ _ _ decls)

31 = concat $ catMaybes $ map getCtxDecl decls

33 getCtxDecl :: Decl -> Maybe Ctx

34 getCtxDecl (DataDecl _ _ _ _ _ cons _) = getCtxCons cons In

35 getCtxDecl _ = fail "Only applies to data declarations"

37 getCtxCons :: [QualConDecl] -> (Term -> Term) -> Maybe Ctx

38 getCtxCons [QualConDecl _ _ _ (ConDecl (Ident name) l)] f =

39 return [(name, buildArgs f (length l))]

40 getCtxCons ((QualConDecl _ _ _ (ConDecl (Ident name) l)):t) f =

41 do t' <- getCtxCons t (f . Inr)

42 return ((name, buildArgs (f . Inl) (length l)):t')

43 getCtxCons _ _ = fail "Case not covered"

45 buildArgs :: (Term -> Term) -> Int -> Term

46 buildArgs f 0 = f Unit

47 buildArgs f 1 = Lam "x1" (f (Pointwise.Var "x1"))

48 buildArgs f n = let v = 'x' : show n

49 in Lam v (buildArgs (f . (\t -> (Pointwise.Var v :&: t))) (n-1))

51 {- Calculation of the instances of FunctorOf, when possible. -}

53 type St = StateT ((String,Int),[Type]) Maybe

55 conDecl :: QualConDecl -> ConDecl

56 conDecl (QualConDecl _ _ _ con) = con

58 functorOfInst :: Bool -> Module -> Module

59 functorOfInst ob (Module a b c d e i decls)

60 = let seed = "v" --getSeed decls

61 newDecls = concat $ catMaybes $

62 map (\x -> evalStateT (getInstances ob x) ((seed,0),[])) decls

63 in Module a b c d e i newDecls

65 addConst t = modify (\(s,l) -> (s,t:l))

67 g :: Type -> QualConDecl -> St Type

68 g arg = gCon arg . conDecl

70 gCon :: Type -> ConDecl -> St Type

71 gCon arg (ConDecl _ []) = return constNil

72 gCon arg (ConDecl _ lBangType) = liftM (foldr1 timesType) (mapM (h arg) lBangType)

73 gCon arg (RecDecl hsName l ) = gCon arg (ConDecl hsName (concatMap unRec l))

74 -- fail "data types records not yet supported"

76 h :: Type -> BangType -> St Type

77 h arg (BangedTy hsType ) = ii arg hsType

78 h arg (UnBangedTy hsType ) = ii arg hsType

79 -- what's the diference between Banged and UnBanged?

81 i :: Type -> Type -> St Type

82 i arg (TyFun hsType1 hsType2) = fail "TyFun not yet supported"

83 i arg (TyTuple _ lType) = liftM (foldr1 timesType) (mapM (ii arg) lType)

84 i arg (TyApp hsType1 hsType2) = liftM (appType hsType1) (i arg hsType2)

85 -- fail "TyApp not yet supported" --g :@: h

86 i arg t@(TyVar hsName) = addConst t >> (return $ TyApp (TyCon $ UnQual $ Ident "Const") t)

87 i arg t@(TyCon hsQName) = addConst t >> (return $ TyApp (TyCon $ UnQual $ Ident "Const") t)

89 ii :: Type -> Type -> St Type

90 ii arg typ | typ == arg = return $ TyCon $ UnQual $ Ident "Id"

91 | otherwise = i arg typ

93 genInOut :: Type -> [QualConDecl] -> St [(Pat, Pat)]

94 genInOut arg [] = fail "empty list of constructors"

95 genInOut arg l = liftM genPat (mapM (g' arg) l)

97 genPat :: [(Pat, Pat)] -> [(Pat, Pat)]

98 genPat [] = error "empty list found when generating instance of 'Mu' "

99 genPat l = genPatAux id l

100

101 genPatAux ac [(a,b)] = [(ac a, b)]

102 genPatAux ac ((a,b):t) = (ac . inl $ a, b) : genPatAux (ac . inr) t

103

104 g' :: Type -> QualConDecl -> St (Pat,Pat)

105 g' arg = g'Con arg . conDecl

106

107 g'Con :: Type -> ConDecl -> St (Pat, Pat)

108 g'Con arg (ConDecl hsName []) = return (constPNil,PApp (UnQual hsName) [])

109 g'Con arg (ConDecl hsName lBangType) = do

110 (l2,l3) <- mapAndUnzipM (h' arg) lBangType

111 return (foldr1 times l2,PApp (UnQual hsName) l3)

112 g'Con arg (RecDecl hsName l) = g'Con arg (ConDecl hsName (concatMap unRec l))

113 --fail "data types records not yet supported"

114

115 h' :: Type -> BangType -> St (Pat, Pat)

116 h' arg (BangedTy hsType) = ii' arg hsType

117 h' arg (UnBangedTy hsType) = ii' arg hsType

118 -- what's the diference between Banged and UnBanged?

119

120 i' :: Type -> Type -> St (Pat, Pat)

121 i' arg (TyFun hsType1 hsType2) = fail "TyFun not yet supported"

122 i' arg (TyTuple _ lType) = do

123 (l1,l2) <- mapAndUnzipM (ii' arg) lType

124 return (foldr1 times l1,PTuple l2)

125 i' arg (TyApp hsType1 hsType2) = do

126 a <- getFreshVar

127 let av = PVar a

128 return (av,av)

129 i' arg t@(TyVar hsName) = do

130 a <- getFreshVar

131 let av = PVar a

132 return (av,av)

133 i' arg t@(TyCon hsQName) = do

134 a <- getFreshVar

135 let av = case hsQName of

136 Special _ -> PApp hsQName []

137 _ -> PVar a

138 return (av,av)

139

140 ii' :: Type -> Type -> St (Pat, Pat)

141 ii' arg typ | typ == arg = do

142 a <- getFreshVar

143 let av = PVar a

144 return (av,av)

145 | otherwise = i' arg typ

146

147 mkDataName :: Decl -> Type

148 mkDataName (DataDecl _ _ _ hsName lName _ _) = foldl TyApp (TyCon $ UnQual hsName) . map TyVar $ lName

149

150 getDataDeclFunctor :: Type -> [QualConDecl] -> St (Type,[Type])

151 getDataDeclFunctor arg lConDecl = withStateT (\((s,n),_) -> ((s,n),[])) $ do

152 l1 <- mapM (g arg) lConDecl

153 let functor = foldr1 plusType l1

154 (_,consts) <- get

155 return (functor,consts)

156

157 deriveTypeable :: Decl -> Decl

158 deriveTypeable (DataDecl loc dn ctx hsName lName lConDecl derive) =

159 DataDecl loc dn ctx hsName lName lConDecl (nub $ (UnQual typeable,[]) : derive)

160

161 getInstances :: Bool -- ^ Observable or not

162 -> Decl -- ^ Data types

163 -> St [Decl] -- ^ Instances for functor representation

164 getInstances ob d@(DataDecl loc _ [] hsName lName lConDecl _) = do

165 let arg = mkDataName d

166 (functor,consts) <- getDataDeclFunctor arg lConDecl

167 l <- genInOut arg lConDecl

168 let innOut = [InsDecl (FunBind (map inMatch l)), InsDecl (FunBind (map outMatch l))]

169 let pfTInst = TypeInsDecl loc (TyApp pfType arg) functor

170 let muInst = InstDecl loc [] mu [arg] innOut

171 let observableInst = getObservableInst loc (nub consts) arg

172 if ob then return [deriveTypeable d,pfTInst,muInst,observableInst]

173 else return [d,pfTInst,muInst]

174 where

175 match str (a,b) = Exts.Match mkLoc (Ident str) [a] Nothing

176 (UnGuardedRhs $ hsPat2Exp b) (BDecls [])

177 mkLoc = SrcLoc "" 0 0

178 inMatch = match "inn"

179 outMatch = match "out" . swap

180

181 getInstances _ (DataDecl _ _ _ _ _ _ _ ) =

182 fail "type context not treated"

183 getInstances _ d = return [d]

184

185 -- types

186 opType op = TyApp . TyApp (TyVar $ Symbol op)

187 plusType = opType ":+:"

188 timesType = opType ":*:"

189 appType = opType ":@:"

190 constNil = TyApp (TyCon $ UnQual $ Ident "Const") nil

191 nil = TyCon $ UnQual $ Ident "One"

192 mu = UnQual $ Ident "Mu"

193 pfType = TyCon $ UnQual $ Ident "PF"

194

195 -- patterns

196 constPNil = PWildCard

197 inl = PApp (UnQual $ Ident "Left") . singl . PParen

198 inr = PApp (UnQual $ Ident "Right") . singl . PParen

199 singl = (:[])

200 times a b = PTuple [a,b]

201

202 unRec (a,b) = replicate (length a) b

203

204 getFreshVar = do

205 ((seed,n),l) <- gets id

206 modify (const ((seed,n+1),l))

207 return $ Ident $ seed ++ show (n+1)

208

209 getObservableInst :: SrcLoc -> [Type] -> Type -> Decl

210 getObservableInst loc cts a = InstDecl loc ctx (UnQual (Ident "Observable")) [a] [InsDecl (FunBind [Exts.Match loc (Ident "observer") [PVar (Ident "x")] Nothing (UnGuardedRhs (App (App (Exts.Var (UnQual (Ident "send"))) (Lit (String ""))) (Paren (InfixApp (InfixApp (App (App (App (Exts.Var (UnQual (Ident "omap"))) (Paren (ExpTypeSig loc (Exts.Var (UnQual (Ident "_L"))) a))) (Exts.Var (UnQual (Ident "thk")))) (Paren (App (Exts.Var (UnQual (Ident "out"))) (Exts.Var (UnQual (Ident "x")))))) (QVarOp (UnQual (Symbol ">>="))) (Exts.Var (UnQual (Ident "return")))) (QVarOp (UnQual (Symbol "."))) (Exts.Var (UnQual (Ident "inn"))))))) (BDecls [PatBind loc (PVar (Ident "thk")) Nothing (UnGuardedRhs (ExpTypeSig loc (Exts.Var (UnQual (Ident "thunk"))) thunkSig )) (BDecls [])])])]

211 where ctx = foldr (\c b -> mkIns typeable c : mkIns observable c : b) [] cts

212 thunkSig = TyForall Nothing ctx $ TyFun a (TyApp (TyCon (UnQual (Ident "ObserverM"))) a)

213

214 typeable :: Name

215 typeable = Ident "Typeable"

216 observable :: Name

217 observable = Ident "Observable"

218

219 mkIns :: Name -> Type -> Asst

220 mkIns cl t = ClassA (UnQual cl) [t]

221

222 ---- auxiliary functions