@@ -11,9 +11,11 @@ where
1111
1212import Control.Monad
1313import Control.Monad.Freer
14+import Control.Monad.Freer.Fresh
1415import Control.Monad.Freer.Internal (handleRelayS)
1516import Control.Monad.Freer.Reader
1617import Control.Monad.Freer.State
18+import Control.Monad.Freer.TreeTracer
1719import Control.Monad.Freer.Writer
1820import Data.Act
1921import qualified Data.Aeson as A
@@ -22,7 +24,6 @@ import Data.Foldable
2224import Data.Functor
2325import Data.Functor.Contravariant
2426import Data.Group hiding ((~~))
25−import qualified Data.HashMap.Strict as HM
2627import Data.List.NonEmpty (NonEmpty (..))
2728import qualified Data.List.NonEmpty as NE
2829import Data.Map.Shifted.Strict (ShiftedMap (..))
@@ -39,14 +40,28 @@ import Data.Set (Set)
3940import qualified Data.Set as S
4041import Data.Text (Text)
4142import qualified Data.Text.Lazy as TL
42−import qualified Data.Text.Lazy.Builder as T
4343import Data.Text.Prettyprint.Doc as P
4444import Data.Text.Prettyprint.Doc.Render.Text
4545import Data.Traversable
46−import qualified Data.Vector as V
4746import Nix.Atoms
4847import Nix.Expr
4948import Nix.Pretty
49+import Tix.Types
50+
51+getType :: NExprLoc -> (NType, [(SrcSpan, Errors)], [UnifyingError], A.Object)
52+getType r =
53+ let ((((((t, traceTree), unifying), errs), srcs), subs), _) =
54+ run
55+ . evalState (M.empty :: VariableMap)
56+ . runConstraintEnv
57+ . runState @[(TypeVariable, SrcSpan)] []
58+ . interpret @(Writer (TypeVariable, SrcSpan)) (\(Tell x) -> modify (x :))
59+ . runSeqWriter @[(SrcSpan, Errors)]
60+ . runSeqWriter @[UnifyingError]
61+ . runFresh
62+ . runTreeTracer
63+ $ inferGeneral r
64+ in (sub subs t, errs, unifying, traceTree)
5065
5166runConstraintEnv ::
5267 Member (State VariableMap) effs =>
@@ -64,143 +79,18 @@ runConstraintEnv =
6479 return ()
6580 )
6681
67−getType :: NExprLoc -> (NType, [(SrcSpan, Errors)], [UnifyingError], A.Object)
68−getType r =
69− let ((((((t, traceTree), unifying), errs), srcs), subs), _) =
70− run
71− . evalState (M.empty :: VariableMap)
72− . runConstraintEnv
73− . runState @[(TypeVariable, SrcSpan)] []
74− . interpret @(Writer (TypeVariable, SrcSpan)) (\(Tell x) -> modify (x :))
75− . runSeqWriter @[(SrcSpan, Errors)]
76− . runSeqWriter @[UnifyingError]
77− . runFresh
78− . runTreeTracer
79− $ inferGeneral r
80− in (sub subs t, errs, unifying, traceTree)
81−
8282data SubstituteEnv a where
8383 SubstituteEnv :: Substitution -> SubstituteEnv ()
8484
8585subEnv :: Member SubstituteEnv r => Substitution -> Eff r ()
8686subEnv = send . SubstituteEnv
8787
88−newtype TypeVariable = TypeVariable Int
89− deriving newtype (Eq, Ord)
90−
91−instance Show TypeVariable where
92− show (TypeVariable n) = "〚" <> show n <> "〛"
93−
9488data Constraint = !NType :~ !NType
9589 deriving stock (Eq, Ord, Show)
9690
9791instance Pretty Constraint where
9892 pretty (x :~ y) = pretty x <+> "~" <+> pretty y
9993
100−data DeBrujin = DeBrujin !Int !Int
101− deriving stock (Show, Eq, Ord)
102−
103−greek :: [T.Builder]
104−greek = ["α", "β", "γ", "δ", "ε", "ζ", "η", "θ", "ι", "κ", "λ", "μ", "ν", "ξ", "ο", "π", "ρ", "σ", "τ", "υ", "φ", "χ", "ψ", "ω"]
105−
106−variableNames :: [T.Builder]
107−variableNames =
108− greek
109− <> (fmap (\(n, g) -> g <> T.fromString (show n)) $ zip [1 :: Int ..] greek)
110−
111−showNType :: NType -> Text
112−showNType t = TL.toStrict . T.toLazyText $ showNType' 0 t
113− where
114− greekVars = M.fromList $ zip (S.toList $ getAllDeBurjins t) variableNames
115− showNType' :: Int -> NType -> T.Builder
116− showNType' depth u =
117− foralls <> case u of
118− (NAtomic a) -> showAtomicType a
119− (NBrujin (DeBrujin i j)) -> greekVars M.! (DeBrujin (i - depth) j)
120− (NTypeVariable _) -> error "should not have free type variables at this point"
121− (x :-> y) -> showNextNType' x <> " -> " <> showNextNType' y
122− (List x) -> "[" <> showNextNType' x <> "]"
123− (NAttrSet x) ->
124− "{ "
125− <> ( mconcat
126− . intersperse "; "
127− . fmap (\(k, v) -> T.fromText k <> " = " <> showNextNType' v)
128− $ M.toList x
129− )
130− <> " }"
131− where
132− showNextNType' = showNType' $ depth + 1
133− currBurjins = S.mapMonotonic (DeBrujin (- depth)) $ getDeBurjins u
134− foralls =
135− if S.null currBurjins
136− then ""
137− else
138− "∀ "
139− <> (mconcat . intersperse " " . M.elems $ M.restrictKeys greekVars currBurjins)
140− <> ". "
141−
142−showAtomicType :: AtomicType -> T.Builder
143−showAtomicType Integer = "Integer"
144−showAtomicType Float = "Float"
145−showAtomicType Bool = "Bool"
146−showAtomicType String = "String"
147−showAtomicType Path = "Path"
148−showAtomicType Null = "Null"
149−showAtomicType URI = "URI"
150−
151−data NType
152− = NTypeVariable !TypeVariable
153− | NBrujin !DeBrujin
154− | NAtomic !AtomicType
155− | -- These two introduce a new De Brujin binding context
156− !NType :-> !NType
157− | List !NType
158− | NAttrSet !(Map Text NType)
159− deriving stock (Eq, Ord, Show)
160−
161−data AtomicType
162− = Integer
163− | Float
164− | Bool
165− | String
166− | Path
167− | Null
168− | URI
169− deriving stock (Eq, Ord, Show)
170−
171−-- | Get all De Brujin type variables that were bound in the the outermost
172−-- (current) binding context.
173−-- Only returns the second indexes.
174−getDeBurjins :: NType -> Set Int
175−getDeBurjins = getDeBurjins' 0
176−
177−-- | Gets all De Brujin variables with the given binding context offset.
178−-- Only returns the second indexes.
179−getDeBurjins' :: Int -> NType -> Set Int
180−getDeBurjins' _ (NTypeVariable _) = S.empty
181−getDeBurjins' _ (NAtomic _) = S.empty
182−getDeBurjins' n (NBrujin (DeBrujin m j)) | m == n = S.singleton j
183−getDeBurjins' _ (NBrujin _) = S.empty
184−getDeBurjins' n (x :-> y) = getDeBurjins' (n + 1) x <> getDeBurjins' (n + 1) y
185−getDeBurjins' n (List x) = getDeBurjins' (n + 1) x
186−getDeBurjins' n (NAttrSet xs) = foldMap (getDeBurjins' (n + 1)) . M.elems $ xs
187−
188−-- | Returns the set of all De Brujin type variables relative to the outermost
189−-- (current) binding context.
190−-- So variables that are bound in one of the inner contexts will have a negative
191−-- binding context number.
192−getAllDeBurjins :: NType -> Set DeBrujin
193−getAllDeBurjins =
194− \case
195− (NTypeVariable _) -> S.empty
196− (NAtomic _) -> S.empty
197− (NBrujin x) -> S.singleton x
198− (x :-> y) -> bndCtx $ getAllDeBurjins x <> getAllDeBurjins y
199− (List x) -> bndCtx $ getAllDeBurjins x
200− (NAttrSet xs) -> bndCtx . foldMap getAllDeBurjins . M.elems $ xs
201− where
202− bndCtx = S.mapMonotonic (\(DeBrujin i j) -> DeBrujin (i - 1) j)
203−
20494newtype DeBrujinContext = DeBrujinContext (Sum Int)
20595 deriving newtype (Eq, Ord, Show, Semigroup, Monoid, Group, Num)
20696
@@ -252,23 +142,7 @@ instance Free NType where
252142 free (List x) = free x
253143 free (NAttrSet attrs) = foldMap free . M.elems $ attrs
254144 free (x :-> y) = free x <> free y
255−
256−instance Pretty NType where
257− pretty (NTypeVariable t) = pretty $ prettyTypeVariable t
258− pretty (NBrujin (DeBrujin i j)) = "⟦" <> pretty i <+> pretty j <> "⟧"
259− pretty (NAtomic a) = viaShow a
260− pretty (x :-> y) = sep [pretty x, "->" <+> pretty y]
261− pretty (List x) = "[" <> align (pretty x) <> "]"
262− pretty (NAttrSet x) =
263− sep
264− [ flatAlt "{ " "{"
265− <+> align
266− ( sep . zipWith (<+>) ("" : repeat ";")
267− . map (\(k, v) -> pretty k <+> "=" <+> align (pretty v))
268− $ M.toList x
269− ),
270− "}"
271− ]
145+ free (NBrujin _) = S.empty
272146
273147instance Free a => Free [a] where
274148 free = foldMap free
@@ -279,11 +153,8 @@ instance Free Substitution where
279153newtype Substitution = Substitution {unSubstitution :: Map TypeVariable NType}
280154 deriving newtype (Eq, Ord, Show)
281155
282−prettyTypeVariable :: TypeVariable -> TL.Text
283−prettyTypeVariable (TypeVariable n) = "⟦" <> (TL.pack . show) n <> "⟧"
284−
285156prettySubstitution :: Substitution -> A.Value
286−prettySubstitution = A.toJSON . M.mapKeysMonotonic prettyTypeVariable . fmap renderPretty . unSubstitution
157+prettySubstitution = A.toJSON . M.mapKeysMonotonic (TL.pack . show) . fmap renderPretty . unSubstitution
287158
288159-- | @older <> newer@
289160instance Semigroup Substitution where
@@ -357,8 +228,6 @@ solveWithPriority range (rest :|> c) = do
357228 s <- unifyWithPriority range c
358229 (<> s) <$> solveWithPriority range (fmap (subCon s) rest)
359230
360−-- pattern Sempty <- (S.null -> True) where Sempty = S.empty
361−
362231occursIn :: Free x => TypeVariable -> x -> Bool
363232occursIn t x = t `S.member` free x
364233
@@ -368,32 +237,6 @@ data Errors
368237 | KeyNotPresent Text
369238 deriving stock (Eq, Ord, Show)
370239
371−data Fresh x where
372− Fresh :: Fresh TypeVariable
373− -- | Inclusive
374− MinFreshFromNow :: Fresh TypeVariable
375−
376−type Runner effect = forall effs a. Eff (effect ': effs) a -> Eff effs a
377−
378−runFresh :: Runner Fresh
379−runFresh =
380− evalState (TypeVariable 0)
381− . reinterpret
382− ( \case
383− Fresh -> do
384− (TypeVariable x) <- get
385− put (TypeVariable $ x + 1)
386− return (TypeVariable x)
387− MinFreshFromNow -> get
388− )
389−
390−registerTypeVariables :: Member Fresh r => Eff r a -> Eff r (a, Range TypeVariable)
391−registerTypeVariables m = do
392− l <- send MinFreshFromNow
393− a <- m
394− r <- send MinFreshFromNow
395− return (a, Range l r)
396−
397240freshSrc ::
398241 Members '[Fresh, Reader SrcSpan, Writer (TypeVariable, SrcSpan)] r =>
399242 Eff r TypeVariable
@@ -618,15 +461,6 @@ inferBinding bindings = do
618461 Just r -> Just (name, r)
619462 return $ M.fromListWith mergeSetTypes bindings'
620463
621−-- traceShowMStack :: (HasCallStack, Applicative f, Show a) => a -> f ()
622−-- traceShowMStack = withFrozenCallStack $ traceShowMStack' ""
623−
624−-- traceShowMStack' :: (HasCallStack, Applicative f, Show a) => String -> a -> f ()
625−-- traceShowMStack' s a = withFrozenCallStack $ do
626−-- case getCallStack callStack of
627−-- (_ : (x, _) : _) -> traceM $ x <> " " <> s <> " \t" <> show a
628−-- _ -> traceM $ s <> " \t" <> show a
629−
630464renderPretty :: Pretty x => x -> TL.Text
631465renderPretty = renderLazy . layoutPretty defaultLayoutOptions . pretty
632466
@@ -739,26 +573,3 @@ lookupAttrSet path = go (NE.toList path)
739573 expectAttrSet x <&> M.lookup p >>= \case
740574 Nothing -> NTypeVariable <$> throwSrcTV (KeyNotPresent p)
741575 Just t -> go ps t
742−
743−data TreeTracer a where
744− TraceTree :: A.Object -> TreeTracer ()
745−
746−traceValue :: (A.ToJSON v, Member TreeTracer eff) => Text -> v -> Eff eff ()
747−traceValue k v = send $ TraceTree $ k A..= v
748−
749−traceSubtree :: Member TreeTracer eff => Text -> Eff eff a -> Eff eff a
750−traceSubtree k = interpose (\(TraceTree o) -> send $ TraceTree (k A..= o))
751−
752−runTreeTracer :: Eff (TreeTracer ': eff) a -> Eff eff (a, A.Object)
753−runTreeTracer = handleRelayS HM.empty (\s x -> pure (x, s)) $ \s (TraceTree o) k ->
754− k (HM.unionWith unionToList s o) ()
755− where
756− unionToList :: A.Value -> A.Value -> A.Value
757− unionToList (A.Array x) (A.Array y) = A.Array $ x <> y
758− unionToList (A.Array x) y = A.Array $ V.snoc x y
759− unionToList x (A.Array y) = A.Array $ V.cons x y
760− unionToList (A.Object x) (A.Object y) = A.Object $ HM.unionWith unionToList x y
761− unionToList x y = A.Array $ V.fromList [x, y]
762−
763−runNoTreeTracer :: Eff (TreeTracer ': eff) a -> Eff eff a
764−runNoTreeTracer = interpret (\(TraceTree _) -> return ())