c42b4ec · tix · git.iko.soy

git.iko.soy/tix

on master help sign in

Introduced TraversableNTypes and added binding context in schemes

c42b4eciko6 years ago

src/Tix/Typechecker.hs+1−1

compare with master

unifiedsplit

@@ -641,7 +641,7 @@ instance Act DeBruijnContext DeBruijn where

641

642type TDeBruijnMap = ShiftedMap DeBruijnContext TypeVariable DeBruijn

643

644−close :: Data x => Predicate TypeVariable -> x -> x

644+close :: TraversableNTypes x => Predicate TypeVariable -> x -> x

645close (Predicate f) =

646 run

647 . evalState @TDeBruijnMap mempty

src/Tix/Types.hs+59−39

@@ -6,10 +6,9 @@ module Tix.Types

6 Scheme (..),

7 scheme,

8 Pred (..),

9− (=>>),

10 (//),

9 (//),

11 Preds (..),

10 Preds (..),

12− traverseNTypesWith,

11+ TraversableNTypes (..),

13 traverseNTypes,

12 traverseNTypes,

14 TerminalNType (..),

13 TerminalNType (..),

15 )

14 )

@@ -21,7 +20,6 @@ import Control.Monad.Freer.Reader

21import Data.Bifunctor

20import Data.Bifunctor

22import Data.Data (Data)

21import Data.Data (Data)

23import Data.Data.Lens

22import Data.Data.Lens

24−import Data.Generics.Sum.Subtype

25import Data.Map (Map)

23import Data.Map (Map)

26import qualified Data.Map as M

24import qualified Data.Map as M

27import qualified Data.Map.MultiKey.Strict as MKM

25import qualified Data.Map.MultiKey.Strict as MKM

@@ -33,7 +31,6 @@ import Debug.Trace

33import GHC.Exts

31import GHC.Exts

34import Generic.Data

32import Generic.Data

35import Prettyprinter

33import Prettyprinter

36−import Type.Reflection

38data Pred

35data Pred

39 = -- | '(x // y) ~ z'

36 = -- | '(x // y) ~ z'

@@ -54,6 +51,7 @@ instance MKM.Keyable Pred where

54-- this seems bad. It should not drop constraints.

51-- this seems bad. It should not drop constraints.

55(//) :: NType -> NType -> NType -> Pred

52(//) :: NType -> NType -> NType -> Pred

56(//) = Update

53(//) = Update

54+{-# INLINE (//) #-}

58data Scheme = Preds :=> !NType

56data Scheme = Preds :=> !NType

59 deriving stock (Eq, Ord, Show, Data, Generic)

57 deriving stock (Eq, Ord, Show, Data, Generic)

@@ -62,12 +60,9 @@ newtype Preds = Preds {unPreds :: [Pred]}

62 deriving newtype (Show, Eq, Ord, Semigroup, Monoid, IsList)

60 deriving newtype (Show, Eq, Ord, Semigroup, Monoid, IsList)

63 deriving stock (Data, Generic)

61 deriving stock (Data, Generic)

65−(=>>) :: Preds -> Scheme -> Scheme

66−[] =>> x = x

67−xs =>> (ys :=> u) = (xs <> ys) :=> u

68−

69scheme :: NType -> Scheme

63scheme :: NType -> Scheme

70scheme t = [] :=> t

64scheme t = [] :=> t

65+{-# INLINE scheme #-}

72data TerminalNType

67data TerminalNType

73 = TAtomic !AtomicType

68 = TAtomic !AtomicType

@@ -75,26 +70,50 @@ data TerminalNType

75 | TBruijn !DeBruijn

70 | TBruijn !DeBruijn

76 deriving stock (Show, Generic)

71 deriving stock (Show, Generic)

73+class TraversableNTypes s where

78−traverseNTypesWith ::

74+ traverseNTypesWith ::

79− (Data s, Applicative f) => (forall x. f x -> f x) -> (TerminalNType -> f TerminalNType) -> s -> f s

75+ (Applicative f) => (forall x. f x -> f x) -> (TerminalNType -> f TerminalNType) -> s -> f s

76+

77+instance TraversableNTypes NType where

80−traverseNTypesWith ctx f s = case eqTypeRep (typeOf s) (typeRep @NType) of

78+ traverseNTypesWith ctx f = \case

81− Just HRefl | Just _ <- projectSub @TerminalNType s -> _Sub @TerminalNType f s

79+ NAtomic a -> f' $ TAtomic a

82− Just HRefl -> ctx $ (template @_ @NType . traverseNTypesWith ctx) f s

80+ NTypeVariable a -> f' $ TTypeVariable a

81+ NBruijn a -> f' $ TBruijn a

82+ x :-> y -> ctx $ (:->) <$> traverseNextType x <*> traverseNextType y

83+ List t -> ctx $ List <$> traverseNextType t

83− _ -> (template @_ @NType . traverseNTypesWith ctx) f s

84+ NAttrSet m -> ctx $ NAttrSet <$> traverseNTypesWith ctx f `traverse` m

85+ where

84−{-# SPECIALIZE traverseNTypesWith ::

86+ traverseNextType = traverseNTypesWith ctx f

85− Applicative f => (forall x. f x -> f x) -> (TerminalNType -> f TerminalNType) -> NType -> f NType

87+ f' = fmap fromTerminalNType . f

86− #-}

88+ fromTerminalNType :: TerminalNType -> NType

89+ fromTerminalNType = \case

90+ TAtomic a -> NAtomic a

91+ TTypeVariable a -> NTypeVariable a

92+ TBruijn a -> NBruijn a

87−{-# SPECIALIZE traverseNTypesWith ::

93+ {-# INLINE traverseNTypesWith #-}

88− Applicative f => (forall x. f x -> f x) -> (TerminalNType -> f TerminalNType) -> Scheme -> f Scheme

94+

89− #-}

95+instance TraversableNTypes Scheme where

96+ traverseNTypesWith ctx f (cs :=> t) =

97+ ctx $

98+ (:=>) <$> traverseNTypesWith ctx f cs <*> traverseNTypesWith ctx f t

90−{-# SPECIALIZE traverseNTypesWith ::

99+ {-# INLINE traverseNTypesWith #-}

91− Monoid r => (forall x. Const r x -> Const r x) -> (TerminalNType -> Const r TerminalNType) -> NType -> Const r NType

100+

92− #-}

101+instance TraversableNTypes Preds where

102+ traverseNTypesWith ctx f (Preds ps) = Preds <$> traverseNTypesWith ctx f `traverse` ps

103+ {-# INLINE traverseNTypesWith #-}

104+

105+instance TraversableNTypes Pred where

106+ traverseNTypesWith ctx f = \case

107+ (HasField t (k, h)) ->

93−{-# SPECIALIZE traverseNTypesWith ::

108+ HasField <$> traverseNTypesWith ctx f t <*> ((k,) <$> traverseNTypesWith ctx f h)

94− Monoid r => (forall x. Const r x -> Const r x) -> (TerminalNType -> Const r TerminalNType) -> Scheme -> Const r Scheme

109+ (Update x y z) ->

95− #-}

110+ Update

96−

111+ <$> traverseNTypesWith ctx f x

112+ <*> traverseNTypesWith ctx f y

113+ <*> traverseNTypesWith ctx f z

114+ {-# INLINE traverseNTypesWith #-}

115+

97−traverseNTypes :: Data s => Traversal' s TerminalNType

116+traverseNTypes :: TraversableNTypes s => Traversal' s TerminalNType

98traverseNTypes = traverseNTypesWith id

117traverseNTypes = traverseNTypesWith id

99{-# INLINE traverseNTypes #-}

118{-# INLINE traverseNTypes #-}

100

119

@@ -142,7 +161,7 @@ instance Pretty NType where

142instance Pretty Scheme where

161instance Pretty Scheme where

143 pretty t = greekifyWith t $ prettyScheme t

162 pretty t = greekifyWith t $ prettyScheme t

144

163

145−greekifyWith :: Data t => t -> Eff '[Reader (Map DeBruijn Text), Reader Depth] x -> x

164+greekifyWith :: TraversableNTypes t => t -> Eff '[Reader (Map DeBruijn Text), Reader Depth] x -> x

146greekifyWith t =

165greekifyWith t =

147 run

166 run

148 . runReader (Depth 0)

167 . runReader (Depth 0)

@@ -153,7 +172,7 @@ newtype Depth = Depth Int

153descend :: Member (Reader Depth) eff => Eff eff x -> Eff eff x

172descend :: Member (Reader Depth) eff => Eff eff x -> Eff eff x

154descend = local (\(Depth n) -> Depth $ n + 1)

173descend = local (\(Depth n) -> Depth $ n + 1)

155

174

156−getDepthedDeBurjins :: (Data x, Member (Reader Depth) eff) => x -> Eff eff (Set DeBruijn)

175+getDepthedDeBurjins :: (TraversableNTypes x, Member (Reader Depth) eff) => x -> Eff eff (Set DeBruijn)

157getDepthedDeBurjins x = do

176getDepthedDeBurjins x = do

158 Depth depth <- ask

177 Depth depth <- ask

159 return $ S.mapMonotonic (DeBruijn (- depth)) $ getDeBurjins x

178 return $ S.mapMonotonic (DeBruijn (- depth)) $ getDeBurjins x

@@ -198,12 +217,13 @@ prettyScheme u@(Preds cs :=> t) = do

198 getDepthedDeBurjins (traceShowId u) <&> \s -> case M.elems . M.restrictKeys greekVars $ traceShowId s of

217 getDepthedDeBurjins (traceShowId u) <&> \s -> case M.elems . M.restrictKeys greekVars $ traceShowId s of

199 [] -> mempty

218 [] -> mempty

200 foralls -> "∀" <+> fillSep (pretty <$> foralls) <> "." <> line

219 foralls -> "∀" <+> fillSep (pretty <$> foralls) <> "." <> line

220+ descend $ do

201− cs' <-

221+ cs' <-

202− prettyPred `traverse` cs <&> \case

222+ prettyPred `traverse` cs <&> \case

203− [] -> mempty

223+ [] -> mempty

204− cs' -> group (paren (vsep $ punctuate "," cs') <+> "=>" <> line)

224+ cs' -> group (paren (vsep $ punctuate "," cs') <+> "=>" <> line)

205− t' <- prettyNType t

225+ t' <- prettyNType t

206− return $ group $ foralls <> cs' <> t'

226+ return $ group $ foralls <> cs' <> t'

207 where

227 where

208 prettyPred :: Pred -> PrettyM (Doc ann)

228 prettyPred :: Pred -> PrettyM (Doc ann)

209 prettyPred (h `HasField` (k, v)) = do

229 prettyPred (h `HasField` (k, v)) = do

@@ -221,7 +241,7 @@ prettyScheme u@(Preds cs :=> t) = do

221-- (current) binding context.

241-- (current) binding context.

222-- So variables that are bound in one of the inner contexts will have a negative

242-- So variables that are bound in one of the inner contexts will have a negative

223-- binding context number.

243-- binding context number.

224−getAllDeBurjins :: Data x => x -> Set DeBruijn

244+getAllDeBurjins :: TraversableNTypes x => x -> Set DeBruijn

225getAllDeBurjins =

245getAllDeBurjins =

226 view $

246 view $

227 traverseNTypesWith (first $ S.mapMonotonic (\(DeBruijn i j) -> DeBruijn (i - 1) j))

247 traverseNTypesWith (first $ S.mapMonotonic (\(DeBruijn i j) -> DeBruijn (i - 1) j))

@@ -235,12 +255,12 @@ getAllDeBurjins =

235-- | Get all De Bruijn type variables that were bound in the the outermost

255-- | Get all De Bruijn type variables that were bound in the the outermost

236-- (current) binding context.

256-- (current) binding context.

237-- Only returns the second indexes.

257-- Only returns the second indexes.

238−getDeBurjins :: Data x => x -> Set Int

258+getDeBurjins :: TraversableNTypes x => x -> Set Int

239getDeBurjins t = getDeBurjins' t 0

259getDeBurjins t = getDeBurjins' t 0

240

260

241-- | Gets all De Bruijn variables with the given binding context offset.

261-- | Gets all De Bruijn variables with the given binding context offset.

242-- Only returns the second indexes.

262-- Only returns the second indexes.

243−getDeBurjins' :: Data x => x -> Int -> Set Int

263+getDeBurjins' :: TraversableNTypes x => x -> Int -> Set Int

244getDeBurjins' =

264getDeBurjins' =

245 view $

265 view $

246 traverseNTypesWith (\(Const f) -> Const (\n -> f (n + 1)))

266 traverseNTypesWith (\(Const f) -> Const (\n -> f (n + 1)))