74e9304 · tix · git.iko.soy

git.iko.soy/tix

Renamed things ;p

commit74e9304085e29c786a4f8b9df198f0fb9401dee9 authoriko <ilyakooo0@gmail.com> dateMon 29 Mar 2021, 20:08 (6 years ago) parent1e93c42

3 files changed+39−38

compare with master

unifiedsplit

package.yaml+1 src/Tix/Typechecker.hs+23−23 src/Tix/Types.hs+15−15

package.yaml+1

@@ -88,3 +88,4 @@ default-extensions:

8888 - EmptyDataDeriving

8989 - EmptyCase

9090 - OverloadedLists

91+ - StandaloneDeriving

src/Tix/Typechecker.hs+23−23

@@ -92,38 +92,38 @@ data Constraint = !Scheme :~ !Scheme

9292instance Pretty Constraint where

9393 pretty (x :~ y) = pretty x <+> "~" <+> pretty y

9494

95−newtype DeBrujinContext = DeBrujinContext (Sum Int)

95+newtype DeBruijnContext = DeBruijnContext (Sum Int)

9696 deriving newtype (Eq, Ord, Show, Semigroup, Monoid, Group, Num)

9797

98−instance Act DeBrujinContext DeBrujin where

99− act (DeBrujinContext (Sum n)) (DeBrujin i j) = DeBrujin (i + n) j

98+instance Act DeBruijnContext DeBruijn where

99+ act (DeBruijnContext (Sum n)) (DeBruijn i j) = DeBruijn (i + n) j

100100

101−type TDeBrujinMap = ShiftedMap DeBrujinContext TypeVariable DeBrujin

101+type TDeBruijnMap = ShiftedMap DeBruijnContext TypeVariable DeBruijn

102102

103103close :: Predicate TypeVariable -> Scheme -> Scheme

104104close (Predicate f) =

105105 run

106− . evalState @TDeBrujinMap mempty

106+ . evalState @TDeBruijnMap mempty

107107 . runReader @Int 0

108108 . evalState @Int 0

109109 . close'

110110 where

111111 -- State is the sequential number, Reader is the binding context number

112− close' :: Scheme -> Eff '[State Int, Reader Int, State TDeBrujinMap] Scheme

112+ close' :: Scheme -> Eff '[State Int, Reader Int, State TDeBruijnMap] Scheme

113113 close' x@(NAtomic _) = return x

114114 close' (preds :=> t) =

115115 (:=>) <$> (Preds <$> closePred `traverse` unPreds preds) <*> closeType t

116116

117− closeType :: NType -> Eff '[State Int, Reader Int, State TDeBrujinMap] NType

117+ closeType :: NType -> Eff '[State Int, Reader Int, State TDeBruijnMap] NType

118118 closeType = \case

119− x@(NBrujin _) -> return x

120− (NTypeVariable tv) | f tv -> NBrujin <$> newbrujin tv

119+ x@(NBruijn _) -> return x

120+ (NTypeVariable tv) | f tv -> NBruijn <$> newbruijn tv

121121 x@(NTypeVariable _) -> return x

122122 (x :-> y) -> bndCtx $ (:->) <$> close' x <*> close' y

123123 (List x) -> bndCtx $ List <$> close' x

124124 (NAttrSet x) -> bndCtx $ NAttrSet <$> traverse close' x

125125

126− closePred :: Pred -> Eff '[State Int, Reader Int, State TDeBrujinMap] Pred

126+ closePred :: Pred -> Eff '[State Int, Reader Int, State TDeBruijnMap] Pred

127127 closePred = \case

128128 (Update x y z) -> bndCtx $ Update <$> closeType x <*> closeType y <*> closeType z

129129 (HasField t (k, v)) -> bndCtx $ do

@@ -132,18 +132,18 @@ close (Predicate f) =

132132 return $ HasField t' (k, v')

133133

134134 bndCtx m = do

135− modify @TDeBrujinMap (SM.shift 1)

135+ modify @TDeBruijnMap (SM.shift 1)

136136 x <- local @Int (+ 1) m

137− modify @TDeBrujinMap (SM.shift (-1))

137+ modify @TDeBruijnMap (SM.shift (-1))

138138 return x

139− newbrujin t = do

140− get @TDeBrujinMap <&> SM.lookup t >>= \case

139+ newbruijn t = do

140+ get @TDeBruijnMap <&> SM.lookup t >>= \case

141141 Nothing -> do

142142 i <- ask

143143 j <- get

144144 modify @Int (+ 1)

145− let x = DeBrujin i j

146− modify @TDeBrujinMap (SM.insert t x)

145+ let x = DeBruijn i j

146+ modify @TDeBruijnMap (SM.insert t x)

147147 return x

148148 Just x -> return x

149149

@@ -156,10 +156,10 @@ instance Free NType where

156156 free (List x) = free x

157157 free (NAttrSet attrs) = foldMap free . M.elems $ attrs

158158 free (x :-> y) = free x <> free y

159− free (NBrujin _) = S.empty

159+ free (NBruijn _) = S.empty

160160

161161 sub s r = case r of

162− NBrujin _ -> r

162+ NBruijn _ -> r

163163 NTypeVariable x -> NTypeVariable x -- it should be substituted higher in Scheme

164164 List x -> List $ sub s x

165165 NAttrSet m -> NAttrSet $ sub s <$> m

@@ -382,24 +382,24 @@ instantiate ::

382382 Eff effs Scheme

383383instantiate = evalState M.empty . instantiateScheme

384384 where

385− instantiateScheme :: forall. Scheme -> Eff (State (Map DeBrujin TypeVariable) ': effs) Scheme

385+ instantiateScheme :: forall. Scheme -> Eff (State (Map DeBruijn TypeVariable) ': effs) Scheme

386386 instantiateScheme (ps :=> t) =

387387 (:=>) <$> (Preds <$> traverse instantiatePred (unPreds ps)) <*> instantiate' t

388388 instantiateScheme x@(NAtomic _) = return x

389389

390− instantiatePred :: forall. Pred -> Eff (State (Map DeBrujin TypeVariable) ': effs) Pred

390+ instantiatePred :: forall. Pred -> Eff (State (Map DeBruijn TypeVariable) ': effs) Pred

391391 instantiatePred = \case

392392 (Update x y z) -> Update <$> instantiate' x <*> instantiate' y <*> instantiate' z

393393 (x `HasField` (f, y)) -> HasField <$> instantiate' x <*> ((f,) <$> instantiate y)

394394

395− instantiate' :: forall. NType -> Eff (State (Map DeBrujin TypeVariable) ': effs) NType

395+ instantiate' :: forall. NType -> Eff (State (Map DeBruijn TypeVariable) ': effs) NType

396396 instantiate' x@(NTypeVariable _) = return x

397− instantiate' (NBrujin db) = NTypeVariable <$> freshInst db

397+ instantiate' (NBruijn db) = NTypeVariable <$> freshInst db

398398 instantiate' (x :-> y) = (:->) <$> instantiateScheme x <*> instantiateScheme y

399399 instantiate' (List x) = List <$> instantiateScheme x

400400 instantiate' (NAttrSet xs) = NAttrSet <$> traverse instantiateScheme xs

401401

402− freshInst :: DeBrujin -> Eff (State (Map DeBrujin TypeVariable) ': effs) TypeVariable

402+ freshInst :: DeBruijn -> Eff (State (Map DeBruijn TypeVariable) ': effs) TypeVariable

403403 freshInst db = do

404404 gets (M.lookup db) >>= \case

405405 Just t -> return t

src/Tix/Types.hs+15−15

@@ -1,7 +1,7 @@

11module Tix.Types

22 ( NType (..),

33 AtomicType (..),

4− DeBrujin (..),

4+ DeBruijn (..),

55 TypeVariable (..),

66 showNType,

77 Scheme (..),

@@ -59,7 +59,7 @@ scheme t = [] :=> t

5959

6060data NType

6161 = NTypeVariable !TypeVariable

62− | NBrujin !DeBrujin

62+ | NBruijn !DeBruijn

6363 | !Scheme :-> !Scheme

6464 | List !Scheme

6565 | NAttrSet !(Map Text Scheme)

@@ -75,7 +75,7 @@ data AtomicType

7575 | URI

7676 deriving stock (Eq, Ord, Show)

7777

78−data DeBrujin = DeBrujin !Int !Int

78+data DeBruijn = DeBruijn !Int !Int

7979 deriving stock (Show, Eq, Ord)

8080

8181newtype TypeVariable = TypeVariable Int

@@ -95,7 +95,7 @@ showNType t = TL.toStrict . T.toLazyText $ showNType' 0 t

9595 showNType' _ (NAtomic a) = showAtomicType a

9696 showNType' depth (Preds ps :=> u) =

9797 foralls <> predicates <> case u of

98− (NBrujin (DeBrujin i j)) -> greekVars M.! DeBrujin (i - depth) j

98+ (NBruijn (DeBruijn i j)) -> greekVars M.! DeBruijn (i - depth) j

9999 (NTypeVariable _) -> error "should not have free type variables at this point"

100100 (x :-> y) -> showNextNType' x <> " -> " <> showNextNType' y

101101 (List x) -> "[" <> showNextNType' x <> "]"

@@ -109,7 +109,7 @@ showNType t = TL.toStrict . T.toLazyText $ showNType' 0 t

109109 <> " }"

110110 where

111111 showNextNType' = showNType' $ depth + 1

112− currBurjins = S.mapMonotonic (DeBrujin (- depth)) $ getDeBurjins u

112+ currBurjins = S.mapMonotonic (DeBruijn (- depth)) $ getDeBurjins u

113113 foralls =

114114 if S.null currBurjins

115115 then ""

@@ -122,11 +122,11 @@ showNType t = TL.toStrict . T.toLazyText $ showNType' 0 t

122122 then mempty

123123 else "(" <> (fold . L.intersperse ", " $ T.fromString . show <$> ps) <> ") => "

124124

125−-- | Returns the set of all De Brujin type variables relative to the outermost

125+-- | Returns the set of all De Bruijn type variables relative to the outermost

126126-- (current) binding context.

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

128128-- binding context number.

129−getAllDeBurjins :: Scheme -> Set DeBrujin

129+getAllDeBurjins :: Scheme -> Set DeBruijn

130130getAllDeBurjins (NAtomic _) = S.empty

131131getAllDeBurjins (Preds ps :=> t) =

132132 foldMap

@@ -139,28 +139,28 @@ getAllDeBurjins (Preds ps :=> t) =

139139 ps

140140 <> case t of

141141 (NTypeVariable _) -> S.empty

142− (NBrujin x) -> S.singleton x

142+ (NBruijn x) -> S.singleton x

143143 (x :-> y) -> bndCtx $ getAllDeBurjins x <> getAllDeBurjins y

144144 (List x) -> bndCtx $ getAllDeBurjins x

145145 (NAttrSet xs) -> bndCtx . foldMap getAllDeBurjins . M.elems $ xs

146146 where

147− bndCtx = S.mapMonotonic (\(DeBrujin i j) -> DeBrujin (i - 1) j)

147+ bndCtx = S.mapMonotonic (\(DeBruijn i j) -> DeBruijn (i - 1) j)

148148

149−getAllTypeDeBurjins :: NType -> Set DeBrujin

149+getAllTypeDeBurjins :: NType -> Set DeBruijn

150150getAllTypeDeBurjins = getAllDeBurjins . scheme

151151

152−-- | Get all De Brujin type variables that were bound in the the outermost

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

153153-- (current) binding context.

154154-- Only returns the second indexes.

155155getDeBurjins :: NType -> Set Int

156156getDeBurjins = getDeBurjins' 0

157157

158−-- | Gets all De Brujin variables with the given binding context offset.

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

159159-- Only returns the second indexes.

160160getDeBurjins' :: Int -> NType -> Set Int

161161getDeBurjins' _ (NTypeVariable _) = S.empty

162−getDeBurjins' n (NBrujin (DeBrujin m j)) | m == n = S.singleton j

163−getDeBurjins' _ (NBrujin _) = S.empty

162+getDeBurjins' n (NBruijn (DeBruijn m j)) | m == n = S.singleton j

163+getDeBurjins' _ (NBruijn _) = S.empty

164164getDeBurjins' n (x :-> y) = getSchemeDeBurjins' (n + 1) x <> getSchemeDeBurjins' (n + 1) y

165165getDeBurjins' n (List x) = getSchemeDeBurjins' (n + 1) x

166166getDeBurjins' n (NAttrSet xs) = foldMap (getSchemeDeBurjins' (n + 1)) . M.elems $ xs

@@ -194,7 +194,7 @@ variableNames =

194194

195195instance Pretty NType where

196196 pretty (NTypeVariable t) = viaShow t

197− pretty (NBrujin (DeBrujin i j)) = "⟦" <> pretty i <+> pretty j <> "⟧"

197+ pretty (NBruijn (DeBruijn i j)) = "⟦" <> pretty i <+> pretty j <> "⟧"

198198 pretty (x :-> y) = sep [pretty x, "->" <+> pretty y]

199199 pretty (List x) = "[" <> align (pretty x) <> "]"

200200 pretty (NAttrSet x) =