@@ -4,6 +4,7 @@ module Tix.Typechecker
44 runFresh,
55 runSeqWriter,
66 getType,
7+ showNType,
78 )
89where
910
@@ -28,6 +29,7 @@ import Data.Sequences
2829import Data.Set (Set)
2930import qualified Data.Set as S
3031import Data.Text (Text)
32+import qualified Data.Text.Lazy as TL
3133import qualified Data.Text.Lazy.Builder as T
3234import Data.Traversable
3335import Debug.Trace
@@ -74,6 +76,42 @@ data Constraint = !NType :~ !NType
7476data DeBrujin = DeBrujin !Int !Int
7577 deriving stock (Show, Eq, Ord)
7678
79+greek :: [T.Builder]
80+greek = ["α", "β", "γ", "δ", "ε", "ζ", "η", "θ", "ι", "κ", "λ", "μ", "ν", "ξ", "ο", "π", "ρ", "σ", "τ", "υ", "φ", "χ", "ψ", "ω"]
81+
82+variableNames :: [T.Builder]
83+variableNames =
84+ greek
85+ <> (fmap (\(n, g) -> g <> T.fromString (show n)) $ zip [1 :: Int ..] greek)
86+
87+showNType :: NType -> Text
88+showNType t = TL.toStrict . T.toLazyText $ showNType' t
89+ where
90+ greekVars = M.fromList $ zip (S.toList $ getDeBurjins t) variableNames
91+ showNType' :: NType -> T.Builder
92+ showNType' (NAtomic a) = showAtomicType a
93+ showNType' (NBrujin b) = greekVars M.! b
94+ showNType' (NTypeVariable _) = error "should not have free type variables at this point"
95+ showNType' (x :-> y) = showNType' x <> " -> " <> showNType' y
96+ showNType' (List x) = "[" <> showNType' x <> "]"
97+ showNType' (NAttrSet x) =
98+ "AttrSet {"
99+ <> ( mconcat
100+ . intersperse "; "
101+ . fmap (\(k, v) -> T.fromText k <> " :: " <> showNType' v)
102+ $ M.toList x
103+ )
104+ <> "}"
105+
106+showAtomicType :: AtomicType -> T.Builder
107+showAtomicType Integer = "Integer"
108+showAtomicType Float = "Float"
109+showAtomicType Bool = "Bool"
110+showAtomicType String = "String"
111+showAtomicType Path = "Path"
112+showAtomicType Null = "Null"
113+showAtomicType URI = "URI"
114+
77115data NType
78116 = NTypeVariable !TypeVariable
79117 | NBrujin !DeBrujin
@@ -94,6 +132,14 @@ data AtomicType
94132 | URI
95133 deriving stock (Eq, Ord, Show)
96134
135+getDeBurjins :: NType -> Set DeBrujin
136+getDeBurjins (NTypeVariable _) = S.empty
137+getDeBurjins (NBrujin x) = S.singleton x
138+getDeBurjins (NAtomic _) = S.empty
139+getDeBurjins (x :-> y) = getDeBurjins x <> getDeBurjins y
140+getDeBurjins (List x) = getDeBurjins x
141+getDeBurjins (NAttrSet xs) = foldMap getDeBurjins . M.elems $ xs
142+
97143isClosed :: NType -> Bool
98144isClosed (NTypeVariable _) = False
99145isClosed (NBrujin _) = True
@@ -192,7 +238,7 @@ solve :: Seq Constraint -> UnifyM Substitution
192238solve Empty = return mempty
193239solve (rest :|> c) = do
194240 s <- unify c
195− solve $ fmap (subCon s) rest
241+ (<> s) <$> solve (fmap (subCon (traceShowId s)) rest)
196242
197243pattern Sempty <- (S.null -> True) where Sempty = S.empty
198244