~jojo/Carth

ref: ae1d242d7d48292779dcbd953e5864bb4211e1ca Carth/src/Inferred.hs -rw-r--r-- 5.1 KiB
ae1d242dJoJo Update stackage release & use default-extensions in cabal file 7 months ago
                                                                                
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
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
{-# LANGUAGE TemplateHaskell, DataKinds #-}

-- | Type annotated AST as a result of typechecking
module Inferred (module Inferred, WithPos(..), TVar(..), TPrim(..), Const(..)) where

import Data.Set (Set)
import qualified Data.Set as Set
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Bifunctor
import Lens.Micro.Platform (makeLenses)

import Misc
import qualified Parsed
import Parsed (TVar(..), Const(..))
import SrcPos
import TypeAst hiding (TConst)
import qualified TypeAst


data TypeErr
    = MainNotDefined
    | InvalidUserTypeSig SrcPos Scheme Scheme
    | CtorArityMismatch SrcPos String Int Int
    | ConflictingPatVarDefs SrcPos String
    | UndefCtor SrcPos String
    | UndefVar SrcPos String
    | InfType SrcPos Type Type TVar Type
    | UnificationFailed SrcPos Type Type Type Type
    | ConflictingTypeDef SrcPos String
    | ConflictingCtorDef SrcPos String
    | RedundantCase SrcPos
    | InexhaustivePats SrcPos String
    | ExternNotMonomorphic (Parsed.Id 'Parsed.Small) TVar
    | FoundHole SrcPos
    | RecTypeDef String SrcPos
    | UndefType SrcPos String
    | UnboundTVar SrcPos
    | WrongMainType SrcPos Parsed.Scheme
    | RecursiveVarDef (WithPos String)
    | TypeInstArityMismatch SrcPos String Int Int
    | ConflictingVarDef SrcPos String
    deriving (Show)

type TConst = TypeAst.TConst Type

data Type
    = TVar TVar
    | TPrim TPrim
    | TConst TConst
    | TFun Type Type
    | TBox Type
    deriving (Show, Eq, Ord)

data Scheme = Forall
    { _scmParams :: (Set TVar)
    , _scmBody :: Type
    }
    deriving (Show, Eq)
makeLenses ''Scheme

type Id = WithPos String

data TypedVar = TypedVar Id Type
    deriving (Show, Eq, Ord)

type VariantIx = Integer

type Span = Integer

data Variant = VariantIx VariantIx | VariantStr String
    deriving (Show, Eq, Ord)

data Con = Con
    { variant :: Variant
    , span :: Span
    , argTs :: [Type]
    }
    deriving Show

data Pat'
    = PVar TypedVar
    | PWild
    | PCon Con [Pat]
    | PBox Pat
    deriving Show
type Pat = WithPos Pat'

type Cases = [(Pat, Expr)]
type FunMatch = (Cases, Type, Type)

data Expr'
    = Lit Const
    | Var TypedVar
    | App Expr Expr Type
    | If Expr Expr Expr
    | Let Def Expr
    | FunMatch FunMatch
    | Ctor VariantIx Span TConst [Type]
    | Sizeof Type
    deriving Show

type Expr = WithPos Expr'

type Defs = TopologicalOrder Def
data Def = VarDef VarDef | RecDefs RecDefs deriving Show
type VarDef = (String, WithPos (Scheme, Expr))
type RecDefs = [(String, WithPos (Scheme, WithPos FunMatch))]
type TypeDefs = Map String ([TVar], [(Id, [Type])])
type Ctors = Map String (VariantIx, (String, [TVar]), [Type], Span)
type Externs = Map String (Type, SrcPos)


instance Eq Con where
    (==) (Con c1 _ _) (Con c2 _ _) = c1 == c2

instance Ord Con where
    compare (Con c1 _ _) (Con c2 _ _) = compare c1 c2

instance TypeAst Type where
    tprim = TPrim
    tconst = TConst
    tfun = TFun
    tbox = TBox


ftv :: Type -> Set TVar
ftv = \case
    TVar tv -> Set.singleton tv
    TPrim _ -> Set.empty
    TFun t1 t2 -> Set.union (ftv t1) (ftv t2)
    TBox t -> ftv t
    TConst (_, ts) -> Set.unions (map ftv ts)

builtinExterns :: Map String (Type, SrcPos)
builtinExterns = Map.fromList $ map
    (second (, SrcPos "<builtin>" 0 0 Nothing))
    [("GC_malloc", tfun (TPrim TNatSize) (TBox tByte))]

builtinVirtuals :: Map String Scheme
builtinVirtuals =
    let tv a = TVExplicit (Parsed.Id (WithPos (SrcPos "<builtin>" 0 0 Nothing) a))
        tva = tv "a"
        ta = TVar tva
        tvb = tv "b"
        tb = TVar tvb
        arithScm = Forall (Set.fromList [tva]) (tfun ta (tfun ta ta))
        bitwiseScm = arithScm
        relScm = Forall (Set.fromList [tva]) (tfun ta (tfun ta tBool))
    in  Map.fromList
            $ [ ("+", arithScm)
              , ("-", arithScm)
              , ("*", arithScm)
              , ("/", arithScm)
              , ("rem", arithScm)
              , ("shift-l", bitwiseScm)
              , ("shift-r", bitwiseScm)
              , ("ashift-r", bitwiseScm)
              , ("bit-and", bitwiseScm)
              , ("bit-or", bitwiseScm)
              , ("bit-xor", bitwiseScm)
              , ("=", relScm)
              , ("/=", relScm)
              , (">", relScm)
              , (">=", relScm)
              , ("<", relScm)
              , ("<=", relScm)
              , ("transmute", Forall (Set.fromList [tva, tvb]) (TFun ta tb))
              , ("deref", Forall (Set.fromList [tva]) (TFun (TBox ta) ta))
              , ( "store"
                , Forall (Set.fromList [tva]) (TFun ta (TFun (TBox ta) (TBox ta)))
                )
              , ("cast", Forall (Set.fromList [tva, tvb]) (TFun ta tb))
              ]

defSigs :: Def -> [(String, Scheme)]
defSigs = \case
    VarDef d -> [defSig d]
    RecDefs ds -> map defSig ds

defSig :: (String, WithPos (Scheme, a)) -> (String, Scheme)
defSig d = (fst d, fst (unpos (snd d)))

flattenDefs :: Defs -> [(String, WithPos (Scheme, Expr))]
flattenDefs (Topo defs) = defToVarDefs =<< defs

defToVarDefs :: Def -> [(String, WithPos (Scheme, Expr))]
defToVarDefs = \case
    VarDef d -> [d]
    RecDefs ds -> map (second (mapPosd (second (mapPosd FunMatch)))) ds