9f2735e · tix · git.iko.soy

git.iko.soy/tix

Better operator processing

commit9f2735e1912c80d4b43182d5f1e477ae467a4f10 authoriko <ilyakooo0@gmail.com> dateSun 9 May 2021, 15:15 (5 years ago) parent3de5ffe

12 files changed+71−26

compare with master

unifiedsplit

src/Tix/Typechecker.hs+41−13 src/Tix/Types.hs+7−1 test/golden/importless/3dovideo.txt+2−1 test/golden/importless/compiler-rt.txt+3−1 test/golden/importless/extras.txt+2−1 test/golden/importless/iproute2.txt+2−1 test/golden/importless/pre-configure.txt+2−1 test/golden/importless/singularity.txt+2−1 test/golden/importless/wakeonlan.txt+2−1 test/golden/mine/nums.txt+1−1 test/golden/mine/subsumption.txt+3−3 test/golden/mine/variadic.txt+4−1

src/Tix/Typechecker.hs+41−13

@@ -144,9 +144,11 @@ instance Free Pred where

144144 free = \case

145145 Update x y z -> free x <> free y <> free z

146146 HasField _ x (_, y) -> free x <> free y

147+ StringOrNumber x -> free x

147148 sub s = \case

148149 Update x y z -> Update (sub s x) (sub s y) (sub s z)

149150 HasField r t (f, v) -> HasField r (sub s t) (f, sub s v)

151+ StringOrNumber x -> StringOrNumber $ sub s x

150152

151153instance Free Scheme where

152154 free (x :=> y) = free x <> free y

@@ -275,6 +277,7 @@ data UnifyingError

275277data PredicateError

276278 = KeyNotPresent Text NType

277279 | NotAnAttributeSet NType

280+ | NotAddable NType

278281 deriving stock (Eq, Show)

279282

280283data InferError

@@ -378,13 +381,12 @@ infer (Fix (Compose (Ann src x))) = local (const src) $ case x of

378381 y : _ -> return $ List y

379382 NUnary NNeg y -> do

380383 t <- infer y

381− -- TODO: Infer either Float or Integer

382− -- tell $ t :~ (normalType . NAtomic $ )

383− return t

384+ t ~~ NAtomic Number

385+ return $ NAtomic Number

384386 NUnary NNot y -> do

385387 t <- infer y

386388 t ~~ NAtomic Bool

387− return t

389+ return $ NAtomic Bool

388390 NBinary NUpdate lhs rhs -> do

389391 lhsT <- infer lhs

390392 rhsT <- infer rhs

@@ -411,7 +413,12 @@ infer (Fix (Compose (Ann src x))) = local (const src) $ case x of

411413 NBinary NLte lhs rhs -> comparison lhs rhs

412414 NBinary NGt lhs rhs -> comparison lhs rhs

413415 NBinary NGte lhs rhs -> comparison lhs rhs

414− NBinary NPlus lhs rhs -> math lhs rhs

416+ NBinary NPlus lhs rhs -> do

417+ lhst <- infer lhs

418+ rhst <- infer rhs

419+ lhst ~~ rhst

420+ tell $ StringOrNumber lhst

421+ return lhst

415422 NBinary NMinus lhs rhs -> math lhs rhs

416423 NBinary NMult lhs rhs -> math lhs rhs

417424 NBinary NDiv lhs rhs -> math lhs rhs

@@ -514,21 +521,23 @@ infer (Fix (Compose (Ann src x))) = local (const src) $ case x of

514521 comparison lhs rhs = do

515522 lhst <- infer lhs

516523 rhst <- infer rhs

517− -- TODO: Infer lhst and rhst are either Integer or Double or String

524+ tell (StringOrNumber lhst)

518525 lhst ~~ rhst

519526 return $ NAtomic Bool

520527 math lhs rhs = do

521528 lhst <- infer lhs

522529 rhst <- infer rhs

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

524− lhst ~~ rhst

525− return lhst

530+ let t = NAtomic Number

531+ lhst ~~ t

532+ rhst ~~ t

533+ return t

526534 logic lhs rhs = do

527535 lhst <- infer lhs

528536 rhst <- infer rhs

529− rhst ~~ NAtomic Bool

530− lhst ~~ NAtomic Bool

531− return $ NAtomic Bool

537+ let t = NAtomic Bool

538+ rhst ~~ t

539+ lhst ~~ t

540+ return t

532541

533542type NormalizedBinding' = F.Free (Map VarName)

534543

@@ -788,6 +797,7 @@ solveAndClose range (cs :=> t) = evalState @Substitution mempty $ do

788797 solveAndClose newRange $ sub s $ (collectedPreds <> solvedPreds) :=> t

789798

790799solveConstraints ::

800+ forall effs.

791801 Members

792802 '[ Fresh,

793803 Writer Pred,

@@ -802,6 +812,15 @@ solveConstraints ::

802812 Eff effs [Pred]

803813solveConstraints _ [] = pure []

804814solveConstraints range (p : ps) = case p of

815+ -- StringOrNumber

816+ StringOrNumber (NTypeVariable _) -> (p :) <$> solveConstraints range ps

817+ StringOrNumber t -> do

818+ case t of

819+ NAtomic String -> pure ()

820+ NAtomic Number -> pure ()

821+ other -> tell $ NotAddable other

822+ solveConstraints range ps

823+ -- HasField

805824 HasField r (NAttrSet ts) (f, t) -> case M.lookup f ts of

806825 Nothing -> do

807826 case r of

@@ -829,10 +848,19 @@ solveConstraints range (p : ps) = case p of

829848 HasField _ t _ -> do

830849 tell $ NotAnAttributeSet t

831850 solveConstraints range ps

851+ -- Update

832852 (Update (NAttrSet a) (NAttrSet b) t) -> do

833853 (NAttrSet $ b <> a) ~~ t

834854 solveConstraints range ps

835− _ -> (p :) <$> solveConstraints range ps

855+ (Update a b _) -> do

856+ allGood <- check `traverse` ([a, b] :: [NType])

857+ (if and allGood then (p :) else id) <$> solveConstraints range ps

858+ where

859+ check :: NType -> Eff effs Bool

860+ check = \case

861+ NTypeVariable _ -> pure True

862+ NAttrSet _ -> pure True

863+ other -> tell (NotAnAttributeSet other) >> pure False

836864

837865partitionWith :: (a -> Either b c) -> [a] -> ([b], [c])

838866partitionWith f = partitionEithers . map f

src/Tix/Types.hs+7−1

@@ -39,7 +39,9 @@ data Pred

3939 -- ^ y

4040 !NType

4141 -- ^ z

42− | HasField {- Is the field optional? -} !FieldStrictness !NType !(Text, Scheme)

42+ | HasField !FieldStrictness !NType !(Text, Scheme)

43+ | -- | supports '+' operator (strings and numbers)

44+ StringOrNumber !NType

4345 deriving stock (Eq, Ord, Show, Generic)

4446

4547data FieldStrictness = OptionalField | RequiredField

@@ -112,6 +114,7 @@ instance TraversableNTypes Pred where

112114 <$> traverseNTypesWith ctx f x

113115 <*> traverseNTypesWith ctx f y

114116 <*> traverseNTypesWith ctx f z

117+ (StringOrNumber x) -> StringOrNumber <$> traverseNTypesWith ctx f x

115118 {-# INLINE traverseNTypesWith #-}

116119

117120traverseNTypes :: TraversableNTypes s => Traversal' s TerminalNType

@@ -251,6 +254,9 @@ prettyScheme u@(cs :=> t) = do

251254 y' <- prettyNType False y

252255 z' <- prettyNType False z

253256 return $ group $ paren x' <+> "//" <> line <> paren y' <+> "~" <> line <> paren z'

257+ prettyPred (StringOrNumber x) = do

258+ x' <- prettyNType False x

259+ return $ "(String | Number)" <+> "~" <+> x'

254260 paren = bracketed "(" ")"

255261

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

test/golden/importless/3dovideo.txt+2−1

@@ -23,7 +23,8 @@

2323 β.tar = ε,

2424 β.toString = ζ -> μ,

2525 ν.licenses = ξ,

26− ξ.bsd3 = ι

26+ ξ.bsd3 = ι,

27+ (String | Number) ~ μ

2728) =>

2829{ fetchurl = {sha256 = String; url = String;} -> κ;

2930 haskellPackages = ο;

test/golden/importless/compiler-rt.txt+3−1

@@ -40,7 +40,9 @@

4040 ι1.isWasm = Bool,

4141 κ1.optionalString = Bool -> String -> η,

4242 λ1.optionalString = γ -> String -> θ,

43− μ1.optionalString = Bool -> String -> θ

43+ μ1.optionalString = Bool -> String -> θ,

44+ (String | Number) ~ η,

45+ (String | Number) ~ θ

4446) =>

4547{ cmake = ζ;

4648 fetch = String -> String -> ι;

test/golden/importless/extras.txt+2−1

@@ -32,7 +32,8 @@

3232 τ.optionals = Bool -> [String] -> [String],

3333 υ.optionals = Bool -> [String] -> [String],

3434 φ.optionalString = Bool -> String -> γ,

35− χ.optionalString = Bool -> String -> γ

35+ χ.optionalString = Bool -> String -> γ,

36+ (String | Number) ~ γ

3637) =>

3738{ enableLua = Bool;

3839 enableMysql = Bool;

test/golden/importless/iproute2.txt+2−1

@@ -28,7 +28,8 @@

2828 ε.iproute2 = φ,

2929 φ.enable = θ,

3030 φ.rttablesExtraConfig = String,

31− υ.lines = σ

31+ υ.lines = σ,

32+ (String | Number) ~ π

3233) =>

3334α ->

3435{ config = ρ;

test/golden/importless/pre-configure.txt+2−1

@@ -3,7 +3,8 @@

33 α.versionOlder = γ -> String -> Bool,

44 δ.is64bit = Bool,

55 δ.isDarwin = ε,

6− δ.isSunOS = Bool

6+ δ.isSunOS = Bool,

7+ (String | Number) ~ β

78) =>

89{ gnatboot = Null;

910 hostPlatform = δ;

test/golden/importless/singularity.txt+2−1

@@ -15,6 +15,7 @@

1515 μ,

1616 θ.overrideAttrs = (ε -> {installPhase = String;}) -> λ,

1717 η.singularity = ν,

18− ν.enable = κ

18+ ν.enable = κ,

19+ (String | Number) ~ ζ

1920) =>

2021α -> {config = μ; options = {programs = {singularity = {enable = ι;};};};}

test/golden/importless/wakeonlan.txt+2−1

@@ -14,7 +14,8 @@

1414 μ,

1515 δ.throw = String -> String,

1616 ζ.wakeonlan = ν,

17− ν.interfaces = λ

17+ ν.interfaces = λ,

18+ (String | Number) ~ η

1819) =>

1920β ->

2021{ config = {powerManagement = {powerDownCommands = ι;};};

test/golden/mine/nums.txt+1−1

@@ -1 +1 @@

1−{a = Number; b = Number; f = ∀ α. α -> α -> α;}

1+{a = Number; b = Number; f = ∀ α. ((String | Number) ~ α) => α -> α -> α;}

test/golden/mine/subsumption.txt+3−3

@@ -1,4 +1,4 @@

1−{ f = ∀ α β. (α.a = β, α.b = β) => α -> β;

2− g = ∀ α. {a = α; b = α;} -> α;

3− h = ∀ α β. (α.a = β, α.b = β) => α -> β;

1+{ f = ∀ α β. (α.a = β, α.b = β, (String | Number) ~ β) => α -> β;

2+ g = ∀ α. ((String | Number) ~ α) => {a = α; b = α;} -> α;

3+ h = ∀ α β. (α.a = β, α.b = β, (String | Number) ~ β) => α -> β;

44}

test/golden/mine/variadic.txt+4−1

@@ -1 +1,4 @@

1−{a = Number; b = Number; f = ∀ α β. (α.a = β, α.b = β) => α -> β;}

1+{ a = Number;

2+ b = Number;

3+ f = ∀ α β. (α.a = β, α.b = β, (String | Number) ~ β) => α -> β;

4+}