7772d8b · tix · git.iko.soy

git.iko.soy/tix

on master help sign in

Slightly changed inferGeneral

7772d8biko6 years ago

src/Data/Range.hs+5−16

compare with master

unifiedsplit

@@ -11,6 +11,11 @@ data Range a

11 | InfiniteRange

12 | EmptyRange

14+instance Show a => Show (Range a) where

15+ show InfiniteRange = "∞"

16+ show EmptyRange = "∅"

17+ show (Range' l r) = show l <> "..<" <> show r

18+

14member :: Ord a => a -> Range a -> Bool

19member :: Ord a => a -> Range a -> Bool

15member _ InfiniteRange = True

20member _ InfiniteRange = True

16member _ EmptyRange = False

21member _ EmptyRange = False

@@ -23,19 +28,3 @@ notMember a r = not $ member a r

24pattern Range :: Ord a => a -> a -> Range a

29pattern Range :: Ord a => a -> a -> Range a

25pattern Range x y <- Range' x y where Range x y = Range' (min x y) (max x y)

30pattern Range x y <- Range' x y where Range x y = Range' (min x y) (max x y)

26−

27−-- pattern EmptyRange :: Range a

28−-- pattern EmptyRange = Range' []

29−

30−-- pattern Range :: Ord a => a -> a -> Range a -> Range a

31−-- pattern Range l r rest <-

32−-- ( ( \x -> case x of

33−-- Range' ((a, b) : rest) -> Just (a, b, Range' rest)

34−-- _ -> Nothing

35−-- ) ->

36−-- Just (l, r, rest)

37−-- )

38−

39−-- addToRange :: Ord a => a -> a -> Range a -> Range a

40−-- addToRange _ _ InfiniteRange = InfiniteRange

41−-- addToRange l r (Range' rs) =

src/Tix/Typechecker.hs+58−52

@@ -10,7 +10,6 @@ where

11import Control.Monad

12import Control.Monad.Freer

13−import Control.Monad.Freer.Error

14import Control.Monad.Freer.Internal (handleRelayS)

13import Control.Monad.Freer.Internal (handleRelayS)

15import Control.Monad.Freer.Reader

14import Control.Monad.Freer.Reader

16import Control.Monad.Freer.State

15import Control.Monad.Freer.State

@@ -19,7 +18,6 @@ import Data.Act

19import Data.Fix

18import Data.Fix

20import Data.Foldable

19import Data.Foldable

21import Data.Functor

20import Data.Functor

22−import Data.Functor.Classes

23import Data.Group

21import Data.Group

24import Data.List.NonEmpty (NonEmpty (..))

22import Data.List.NonEmpty (NonEmpty (..))

25import qualified Data.List.NonEmpty as NE

23import qualified Data.List.NonEmpty as NE

@@ -40,43 +38,48 @@ import Data.Text (Text)

40import qualified Data.Text.Lazy as TL

38import qualified Data.Text.Lazy as TL

41import qualified Data.Text.Lazy.Builder as T

39import qualified Data.Text.Lazy.Builder as T

42import Data.Traversable

40import Data.Traversable

43−import Debug.Trace

44import Nix.Atoms

41import Nix.Atoms

45import Nix.Expr

42import Nix.Expr

44+runConstraintEnv ::

45+ Eff (SubstituteEnv : Writer Substitution : Writer Constraint : State (Seq Constraint) : effs) a ->

46+ Eff effs ((a, Substitution), Seq Constraint)

47+runConstraintEnv =

48+ runState @(Seq Constraint) Empty

49+ . interpret @(Writer Constraint) (\(Tell x) -> modify (x :<|))

50+ . runWriter @Substitution

51+ . interpret @(SubstituteEnv)

52+ ( \(SubstituteEnv x) -> do

53+ modify @(Seq Constraint) (subCon x <$>)

54+ tell x

55+ return ()

56+ )

57+

47getType :: NExprLoc -> (NType, [(SrcSpan, Errors)], [UnifyingError])

58getType :: NExprLoc -> (NType, [(SrcSpan, Errors)], [UnifyingError])

48getType r =

59getType r =

49− let ((((t, unifying), srcs), constraints), errs) =

60+ let (((((t, unifying), errs), srcs), subs), _) =

50 run

61 run

51− . runReader (M.empty :: VariableMap)

62+ . runConstraintEnv

63+ . runState @[(TypeVariable, SrcSpan)] []

64+ . interpret @(Writer (TypeVariable, SrcSpan)) (\(Tell x) -> modify (x :))

52 . runSeqWriter @[(SrcSpan, Errors)]

65 . runSeqWriter @[(SrcSpan, Errors)]

53− . runSeqWriter @(Seq Constraint)

54− . runSeqWriter @[(TypeVariable, SrcSpan)]

55 . runSeqWriter @[UnifyingError]

66 . runSeqWriter @[UnifyingError]

67+ . runReader (M.empty :: VariableMap)

56 . runFresh

68 . runFresh

57− $ getType' r

69+ $ inferGeneral r

58− in (t, errs, unifying)

70+ in (sub subs t, errs, unifying)

60−getType' ::

72+data SubstituteEnv a where

61− Members

73+ SubstituteEnv :: Substitution -> SubstituteEnv ()

62− '[ Writer (SrcSpan, Errors),

74+

63− Reader VariableMap,

75+subEnv :: Member SubstituteEnv r => Substitution -> Eff r ()

64− Writer (TypeVariable, SrcSpan),

76+subEnv = send . SubstituteEnv

65− Writer UnifyingError,

66− Fresh

67− ]

68− r =>

69− NExprLoc ->

70− Eff r NType

71−getType' r = do

72− ((t, s'), constraints) <-

73− runSeqWriter @(Seq Constraint) . runWriter @Substitution $

74− inferGeneral r

75− s <- solve (traceShowId . fmap (subCon s') $ constraints)

76− return . close InfiniteRange $ sub (s <> s') (traceShowId t)

78newtype TypeVariable = TypeVariable Int

79− deriving newtype (Show, Eq, Ord)

79+ deriving newtype (Eq, Ord)

80+

81+instance Show TypeVariable where

82+ show (TypeVariable n) = "〚" <> show n <> "〛"

81data Constraint = !NType :~ !NType

84data Constraint = !NType :~ !NType

82 deriving stock (Eq, Ord, Show)

85 deriving stock (Eq, Ord, Show)

@@ -175,7 +178,7 @@ getDeBurjins' n (NAttrSet xs) = foldMap (getDeBurjins' (n + 1)) . M.elems $ xs

175-- binding context number.

178-- binding context number.

176getAllDeBurjins :: NType -> Set DeBrujin

179getAllDeBurjins :: NType -> Set DeBrujin

177getAllDeBurjins =

180getAllDeBurjins =

178− traceShowId . \case

181+ \case

179 (NTypeVariable _) -> S.empty

182 (NTypeVariable _) -> S.empty

180 (NAtomic _) -> S.empty

183 (NAtomic _) -> S.empty

181 (NBrujin x) -> S.singleton x

184 (NBrujin x) -> S.singleton x

@@ -206,6 +209,7 @@ close range =

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

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

207 close' x@(NBrujin _) = return x

210 close' x@(NBrujin _) = return x

208 close' (NTypeVariable tv) | tv `R.member` range = NBrujin <$> newbrujin tv

211 close' (NTypeVariable tv) | tv `R.member` range = NBrujin <$> newbrujin tv

212+ close' x@(NTypeVariable _) = return x

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

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

210 close' (List x) = bndCtx $ List <$> close' x

214 close' (List x) = bndCtx $ List <$> close' x

211 close' (NAttrSet x) = bndCtx $ NAttrSet <$> traverse close' x

215 close' (NAttrSet x) = bndCtx $ NAttrSet <$> traverse close' x

@@ -239,6 +243,7 @@ instance Free NType where

239newtype Substitution = Substitution {unSubstitution :: Map TypeVariable NType}

243newtype Substitution = Substitution {unSubstitution :: Map TypeVariable NType}

240 deriving newtype (Eq, Ord, Show)

244 deriving newtype (Eq, Ord, Show)

241

245

246+-- | Prefers the left

242instance Semigroup Substitution where

247instance Semigroup Substitution where

243 x'@(Substitution x) <> (Substitution y) = Substitution (x <> fmap (sub x') y)

248 x'@(Substitution x) <> (Substitution y) = Substitution (x <> fmap (sub x') y)

244

249

@@ -308,25 +313,13 @@ solveWithPriority ::

308solveWithPriority _ Empty = return mempty

313solveWithPriority _ Empty = return mempty

309solveWithPriority range (rest :|> c) = do

314solveWithPriority range (rest :|> c) = do

310 s <- unifyWithPriority range c

315 s <- unifyWithPriority range c

311− (<> s) <$> solveWithPriority range (fmap (subCon (traceShowId s)) rest)

316+ (<> s) <$> solveWithPriority range (fmap (subCon s) rest)

312

317

313−pattern Sempty <- (S.null -> True) where Sempty = S.empty

318+-- pattern Sempty <- (S.null -> True) where Sempty = S.empty

314

319

315occursIn :: Free x => TypeVariable -> x -> Bool

320occursIn :: Free x => TypeVariable -> x -> Bool

316occursIn t x = t `S.member` free x

321occursIn t x = t `S.member` free x

317

322

318−data SchemeX x = Scheme (Set TypeVariable) x

319− deriving stock (Eq, Ord, Show)

320−

321−instance Show1 SchemeX where

322− liftShowsPrec s _ p (Scheme Sempty x) = s p x

323− liftShowsPrec s _ p (Scheme tvs x) = ((("forall " <> show tvs)) <>) <> s p x

324−

325−instance Eq1 SchemeX where

326− liftEq eq (Scheme ts1 x1) (Scheme ts2 x2) = ts1 == ts2 && eq x1 x2

327−

328−-- type SchemeS = SchemeX NType

329−

330data Errors

323data Errors

331 = UndefinedVariable VarName

324 = UndefinedVariable VarName

332 | UnexpectedType {expected :: NType, got :: NType}

325 | UnexpectedType {expected :: NType, got :: NType}

@@ -338,8 +331,6 @@ data Fresh x where

338 -- | Inclusive

331 -- | Inclusive

339 MinFreshFromNow :: Fresh TypeVariable

332 MinFreshFromNow :: Fresh TypeVariable

340

333

341−data ResumableExceptions x

342−

343type Runner effect = forall effs a. Eff (effect ': effs) a -> Eff effs a

334type Runner effect = forall effs a. Eff (effect ': effs) a -> Eff effs a

344

335

345runFresh :: Runner Fresh

336runFresh :: Runner Fresh

@@ -384,7 +375,7 @@ type InferEffs =

384 Writer (SrcSpan, Errors),

375 Writer (SrcSpan, Errors),

385 Reader VariableMap,

376 Reader VariableMap,

386 Writer UnifyingError,

377 Writer UnifyingError,

387− Writer Substitution

378+ SubstituteEnv

388 ]

379 ]

389

380

390type InferM x = forall r. Members InferEffs r => Eff r x

381type InferM x = forall r. Members InferEffs r => Eff r x

@@ -482,12 +473,19 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of

482 lhst ~~ rhst

473 lhst ~~ rhst

483 return $ NAtomic Bool

474 return $ NAtomic Bool

484 NBinary op lhs rhs

475 NBinary op lhs rhs

485− | op `elem` [NLt, NLte, NGt, NGte, NPlus, NMinus, NMult, NDiv] -> do

476+ | op `elem` [NLt, NLte, NGt, NGte] -> do

486 lhst <- infer lhs

477 lhst <- infer lhs

487 rhst <- infer rhs

478 rhst <- infer rhs

488 -- TODO: Infer lhst and rhst are either Integer or Double

479 -- TODO: Infer lhst and rhst are either Integer or Double

489 lhst ~~ rhst

480 lhst ~~ rhst

490 return $ NAtomic Bool

481 return $ NAtomic Bool

482+ NBinary op lhs rhs

483+ | op `elem` [NPlus, NMinus, NMult, NDiv] -> do

484+ lhst <- infer lhs

485+ rhst <- infer rhs

486+ -- TODO: Infer lhst and rhst are either Integer or Double

487+ lhst ~~ rhst

488+ return $ lhst

491 NBinary op lhs rhs | op `elem` [NAnd, NOr, NImpl] -> do

489 NBinary op lhs rhs | op `elem` [NAnd, NOr, NImpl] -> do

492 lhst <- infer lhs

490 lhst <- infer lhs

493 rhst <- infer rhs

491 rhst <- infer rhs

@@ -573,17 +571,25 @@ inferBinding bindings = do

573 Just r -> Just (name, r)

571 Just r -> Just (name, r)

574 return $ M.fromListWith mergeSetTypes bindings'

572 return $ M.fromListWith mergeSetTypes bindings'

575

573

574+-- traceShowMStack :: (HasCallStack, Applicative f, Show a) => a -> f ()

575+-- traceShowMStack = withFrozenCallStack $ traceShowMStack' ""

576+

577+-- traceShowMStack' :: (HasCallStack, Applicative f, Show a) => String -> a -> f ()

578+-- traceShowMStack' s a = withFrozenCallStack $ do

579+-- case getCallStack callStack of

580+-- (_ : (x, _) : _) -> traceM $ x <> " " <> s <> " \t" <> show a

581+-- _ -> traceM $ s <> " \t" <> show a

582+

576inferGeneral :: NExprLoc -> InferM NType

583inferGeneral :: NExprLoc -> InferM NType

577inferGeneral x = do

584inferGeneral x = do

578− ((t, cs), range) <- registerTypeVariables . runSeqWriter @(Seq Constraint) $ infer x

585+ (((t, subs), cs), range) <- registerTypeVariables . runConstraintEnv $ infer x

579− s <- solveWithPriority range cs

586+ s' <- solveWithPriority range cs

587+ let s = subs <> s'

588+ returnedS = Substitution . M.filterWithKey (\k _ -> k `R.notMember` range) . unSubstitution $ s

580 -- Filter for optimization purposes

589 -- Filter for optimization purposes

581− tell . Substitution . M.filterWithKey (\k _ -> k `R.notMember` range) . unSubstitution $ s

590+ subEnv returnedS

582 return . close range $ sub s t

591 return . close range $ sub s t

583

592

584−-- appAll :: (a -> b -> b) -> [a] -> b -> b

585−-- appAll f xs = appEndo (mconcat $ Endo . f <$> xs)

586−

587expectAttrSet :: Members '[Reader SrcSpan, Writer (SrcSpan, Errors)] r => NType -> Eff r VariableMap

593expectAttrSet :: Members '[Reader SrcSpan, Writer (SrcSpan, Errors)] r => NType -> Eff r VariableMap

588expectAttrSet (NAttrSet x) = return x

594expectAttrSet (NAttrSet x) = return x

589expectAttrSet g = do

595expectAttrSet g = do

stack.yaml+1−1

@@ -17,7 +17,7 @@

17#

18# resolver: ./custom-snapshot.yaml

19# resolver: https://example.com/snapshots/2018-01-01.yaml

20−resolver: nightly-2020-10-18

20+resolver: nightly-2020-11-08

22# User packages to be built.

23# Various formats can be used as shown in the example below.