git.iko.soy/tix
on master help sign in
Fir deburjin closing
cd17ff7iko
app/Main.hs+5−3
compare with master
unifiedsplit
@@ -10,6 +10,8 @@ main = do
10 inp <- Text.getContents
10 inp <- Text.getContents
11 case parseNixTextLoc inp of
11 case parseNixTextLoc inp of
12 Failure err -> error $ show err
12 Failure err -> error $ show err
13− Success r -> case getType r of
13+ Success r -> do
14+ let (t, errs, uErrs) = getType r
14− (Right x, _) -> print x
15+ print errs
16+ print uErrs
15− (Left e, _) -> print e
17+ print t
src/Tix/Typechecker.hs+76−15
@@ -28,39 +28,60 @@ import Data.Sequences
28import Data.Set (Set)
28import Data.Set (Set)
29import qualified Data.Set as S
29import qualified Data.Set as S
30import Data.Text (Text)
30import Data.Text (Text)
31+import qualified Data.Text.Lazy.Builder as T
31import Data.Traversable
32import Data.Traversable
33+import Debug.Trace
32import Nix.Atoms
34import Nix.Atoms
33import Nix.Expr
35import Nix.Expr
34
36
35−getType :: NExprLoc -> (Either UnifyingError NType, [(SrcSpan, Errors)])
37+getType :: NExprLoc -> (NType, [(SrcSpan, Errors)], [UnifyingError])
36−getType exp =
38+getType r =
37− let (((t, srcs), cons), errs) =
39+ let ((((t, unifying), srcs), constraints), errs) =
38 run
40 run
39 . runReader (M.empty :: VariableMap)
41 . runReader (M.empty :: VariableMap)
40 . runSeqWriter @[(SrcSpan, Errors)]
42 . runSeqWriter @[(SrcSpan, Errors)]
41 . runSeqWriter @(Seq Constraint)
43 . runSeqWriter @(Seq Constraint)
42 . runSeqWriter @[(TypeVariable, SrcSpan)]
44 . runSeqWriter @[(TypeVariable, SrcSpan)]
45+ . runSeqWriter @[UnifyingError]
43 . runFresh
46 . runFresh
44− $ infer exp
47+ $ getType' r
45− s = run . runError @UnifyingError $ solve cons
48+ in (t, errs, unifying)
46− in ((`sub` t) <$> s, errs)
49+
50+getType' ::
51+ Members
52+ '[ Writer (SrcSpan, Errors),
53+ Reader VariableMap,
54+ Writer (TypeVariable, SrcSpan),
55+ Writer UnifyingError,
56+ Fresh
57+ ]
58+ r =>
59+ NExprLoc ->
60+ Eff r NType
61+getType' r = do
62+ (t, constraints) <-
63+ runSeqWriter @(Seq Constraint) $
64+ infer r
65+ s <- solve (traceShowId constraints)
66+ return . close $ sub s (traceShowId t)
47
67
48newtype TypeVariable = TypeVariable Int
68newtype TypeVariable = TypeVariable Int
49 deriving newtype (Show, Eq, Ord)
69 deriving newtype (Show, Eq, Ord)
50
70
51data Constraint = !NType :~ !NType
71data Constraint = !NType :~ !NType
72+ deriving stock (Eq, Ord, Show)
52
73
53−newtype DeBrujin = DeBrujin {unDeBrujin :: Int}
74+data DeBrujin = DeBrujin !Int !Int
54− deriving newtype (Eq, Ord)
75+ deriving stock (Show, Eq, Ord)
55− deriving stock (Show)
56
76
57data NType
77data NType
58 = NTypeVariable !TypeVariable
78 = NTypeVariable !TypeVariable
59 | NBrujin !DeBrujin
79 | NBrujin !DeBrujin
60 | NAtomic !AtomicType
80 | NAtomic !AtomicType
61− | List !NType
62− | NAttrSet !(Map Text NType)
63 | !NType :-> !NType
81 | !NType :-> !NType
82+ | -- These two introduce a new De Brujin binding context
83+ List !NType
84+ | NAttrSet !(Map Text NType)
64 deriving stock (Eq, Ord, Show)
85 deriving stock (Eq, Ord, Show)
65
86
66data AtomicType
87data AtomicType
@@ -73,6 +94,43 @@ data AtomicType
73 | URI
94 | URI
74 deriving stock (Eq, Ord, Show)
95 deriving stock (Eq, Ord, Show)
75
96
97+isClosed :: NType -> Bool
98+isClosed (NTypeVariable _) = False
99+isClosed (NBrujin _) = True
100+isClosed (NAtomic _) = True
101+isClosed (x :-> y) = isClosed x && isClosed y
102+isClosed (List x) = isClosed x
103+isClosed (NAttrSet xs) = all isClosed . M.elems $ xs
104+
105+close :: NType -> NType
106+close =
107+ run
108+ . evalState @(Map TypeVariable DeBrujin) M.empty
109+ . runReader @Int 0
110+ . evalState @Int 0
111+ . close'
112+ where
113+ -- State is the sequential number, Reader is the binding context number
114+ close' :: NType -> Eff '[State Int, Reader Int, State (Map TypeVariable DeBrujin)] NType
115+ close' x@(NAtomic _) = return x
116+ close' x@(NBrujin _) = return x
117+ close' (x :-> y) = (:->) <$> close' x <*> close' y
118+ close' (NTypeVariable tv) = NBrujin <$> newbrujin tv
119+ close' (List x) = bndCtx $ List <$> close' x
120+ close' (NAttrSet x) = bndCtx $ NAttrSet <$> traverse close' x
121+
122+ bndCtx = local @Int (+ 1)
123+ newbrujin t = do
124+ get @(Map TypeVariable DeBrujin) <&> M.lookup t >>= \case
125+ Nothing -> do
126+ i <- ask
127+ j <- get
128+ modify @Int (+ 1)
129+ let x = DeBrujin i j
130+ modify @(Map TypeVariable DeBrujin) (M.insert t x)
131+ return x
132+ Just x -> return x
133+
76class Free s where
134class Free s where
77 free :: s -> Set TypeVariable
135 free :: s -> Set TypeVariable
78
136
@@ -94,6 +152,7 @@ instance Monoid Substitution where
94sub :: Substitution -> NType -> NType
152sub :: Substitution -> NType -> NType
95sub s r = case r of
153sub s r = case r of
96 NAtomic _ -> r
154 NAtomic _ -> r
155+ NBrujin _ -> r
97 NTypeVariable x -> subTV x
156 NTypeVariable x -> subTV x
98 List x -> List $ sub s x
157 List x -> List $ sub s x
99 NAttrSet m -> NAttrSet $ sub s <$> m
158 NAttrSet m -> NAttrSet $ sub s <$> m
@@ -109,7 +168,7 @@ subCon s (x :~ y) = sub s x :~ sub s y
109 NType ->
168 NType ->
110 UnifyM Substitution
169 UnifyM Substitution
111v <<- (NTypeVariable x) | v == x = return mempty
170v <<- (NTypeVariable x) | v == x = return mempty
112−v <<- x | v `occursIn` x = throwError $ InfinityType x
171+v <<- x | v `occursIn` x = tell (InfinityType x) >> return mempty
113v <<- x = return $ Substitution $ M.singleton v x
172v <<- x = return $ Substitution $ M.singleton v x
114
173
115unify :: Constraint -> UnifyM Substitution
174unify :: Constraint -> UnifyM Substitution
@@ -127,7 +186,7 @@ unify (lhs :~ rhs) =
127 s <- unify (x1 :~ x2)
186 s <- unify (x1 :~ x2)
128 s' <- unify $ subCon s $ y1 :~ y2
187 s' <- unify $ subCon s $ y1 :~ y2
129 return $ s' <> s
188 return $ s' <> s
130− (x, y) -> throwError $ CanNotUnify x y
189+ (x, y) -> tell (CanNotUnify x y) >> return mempty
131
190
132solve :: Seq Constraint -> UnifyM Substitution
191solve :: Seq Constraint -> UnifyM Substitution
133solve Empty = return mempty
192solve Empty = return mempty
@@ -156,6 +215,7 @@ data Errors
156 = UndefinedVariable VarName
215 = UndefinedVariable VarName
157 | UnexpectedType {expected :: NType, got :: NType}
216 | UnexpectedType {expected :: NType, got :: NType}
158 | KeyNotPresent Text
217 | KeyNotPresent Text
218+ deriving stock (Eq, Ord, Show)
159
219
160data Fresh x where
220data Fresh x where
161 Fresh :: Fresh TypeVariable
221 Fresh :: Fresh TypeVariable
@@ -188,14 +248,15 @@ data UnifyingError
188 | CanNotUnify NType NType
248 | CanNotUnify NType NType
189 deriving stock (Eq, Show)
249 deriving stock (Eq, Show)
190
250
191−type UnifyM x = forall r. Members '[Error UnifyingError] r => Eff r x
251+type UnifyM x = forall r. Members '[Writer UnifyingError] r => Eff r x
192
252
193type InferEffs =
253type InferEffs =
194 '[ Fresh,
254 '[ Fresh,
195 Writer (TypeVariable, SrcSpan),
255 Writer (TypeVariable, SrcSpan),
196 Writer Constraint,
256 Writer Constraint,
197 Writer (SrcSpan, Errors),
257 Writer (SrcSpan, Errors),
198− Reader VariableMap
258+ Reader VariableMap,
259+ Writer UnifyingError
199 ]
260 ]
200
261
201type InferM x = forall r. Members InferEffs r => Eff r x
262type InferM x = forall r. Members InferEffs r => Eff r x
stack.yaml+1−1
@@ -68,4 +68,4 @@ extra-deps:
68# compiler-check: newer-minor
68# compiler-check: newer-minor
69
69
70ghc-options:
70ghc-options:
71− "$locals": -Weverything -Wno-implicit-prelude -Wno-missing-safe-haskell-mode -Wno-safe -Wno-prepositive-qualified-module -Wno-missing-import-lists -Wno-partial-fields -Wno-all-missed-specialisations
71+ "$locals": -Weverything -Wno-implicit-prelude -Wno-missing-safe-haskell-mode -Wno-safe -Wno-prepositive-qualified-module -Wno-missing-import-lists -Wno-partial-fields -Wno-all-missed-specialisations -Wno-missing-local-signatures -Wno-unsafe