1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
|
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE EmptyDataDeriving #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeFamilies #-}
module HSVIS.Typecheck where
import Control.Monad
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Writer.CPS
import Data.Foldable (toList)
import Data.Map.Strict (Map)
import Data.Bag
import Data.List.NonEmpty.Util
import HSVIS.AST
import HSVIS.Parser
import HSVIS.Diagnostic
data StageTC
type instance X DataDef StageTC = CType
type instance X FunDef StageTC = CType
type instance X FunEq StageTC = CType
type instance X Kind StageTC = ()
type instance X Type StageTC = CKind
type instance X Pattern StageTC = CType
type instance X RHS StageTC = CType
type instance X Expr StageTC = CType
data instance E Type StageTC = TUniVar Int
deriving (Show)
type CProgram = Program StageTC
type CDataDef = DataDef StageTC
type CFunDef = FunDef StageTC
type CFunEq = FunEq StageTC
type CKind = Kind StageTC
type CType = Type StageTC
type CPattern = Pattern StageTC
type CRHS = RHS StageTC
type CExpr = Expr StageTC
data StageTyped
type instance X DataDef StageTyped = TType
type instance X FunDef StageTyped = TType
type instance X FunEq StageTyped = TType
type instance X Kind StageTyped = ()
type instance X Type StageTyped = TKind
type instance X Pattern StageTyped = TType
type instance X RHS StageTyped = TType
type instance X Expr StageTyped = TType
data instance E t StageTyped
deriving (Show)
type TProgram = Program StageTyped
type TDataDef = DataDef StageTyped
type TFunDef = FunDef StageTyped
type TFunEq = FunEq StageTyped
type TKind = Kind StageTyped
type TType = Type StageTyped
type TPattern = Pattern StageTyped
type TRHS = RHS StageTyped
type TExpr = Expr StageTyped
typecheck :: FilePath -> String -> Program Range -> ([Diagnostic], Program TType)
typecheck fp source prog =
let (progtc, (ds1, cs)) =
runWriter
. flip evalStateT (Env mempty mempty)
. flip evalStateT 1
. flip runReaderT (fp, source)
. runTCM
$ tcProgram prog
(ds2, sub) = solveConstrs cs
in (toList (ds1 <> ds2), substProg sub progtc)
data Constr =
CEq CType CType Range -- ^ These types must be equal because of the expression here
deriving (Show)
data Env = Env (Map Name CKind) (Map Name CType)
deriving (Show)
newtype TCM a = TCM { runTCM ::
ReaderT (FilePath, String)
(StateT Int
(StateT Env
(Writer (Bag Diagnostic, Bag Constr))))
a }
deriving newtype (Functor, Applicative, Monad)
raise :: Range -> String -> TCM ()
raise rng@(Range (Pos y _) _) msg = do
(fp, source) <- ask
TCM $ lift $ lift $ tell (pure (Diagnostic fp rng [] (source !! y) msg), mempty)
modifyTEnv :: (Map Name CKind -> Map Name CKind) -> TCM ()
modifyTEnv f = TCM $ lift $ lift $ modify (\(Env a b) -> Env (f a) b)
modifyVEnv :: (Map Name CType -> Map Name CType) -> TCM ()
modifyVEnv f = TCM $ lift $ lift $ modify (\(Env a b) -> Env a (f b))
genUniVar :: CKind -> TCM CType
genUniVar k = TCM $ lift $ state (\i -> (TExt k (TUniVar i), i + 1))
tcProgram :: PProgram -> TCM CProgram
tcProgram (Program ddefs fdefs) = do
-- TODO: add preliminary kinds for the data definitions to the environment,
-- then solve for the kind variables in checkDataDef
Program <$> traverse checkDataDef ddefs <*> traverse tcFunDef fdefs
checkDataDef :: PDataDef -> TCM CDataDef
checkDataDef (DataDef rng name params cons) = do
_
tcFunDef :: PFunDef -> TCM CFunDef
tcFunDef (FunDef rng name msig eqs) = do
when (not $ allEq (fmap (length . funeqPats) eqs)) $
raise (sconcatne (fmap extOf eqs)) "Function equations have differing numbers of arguments"
typ <- case msig of
Just sig -> checkType sig
Nothing -> genUniVar (KType ())
_
checkType :: PType -> TCM CType
checkType = \case
TApp r t ts -> _
TTup r ts -> _
TList r t -> _
TFun r s t -> _
TCon r n -> _
TVar r n -> _
allEq :: (Eq a, Foldable t) => t a -> Bool
allEq l = case toList l of
[] -> True
x : xs -> all (== x) xs
funeqPats :: FunEq t -> [Pattern t]
funeqPats (FunEq _ _ pats _) = pats
|
