git.iko.soy/elk
on master help sign in
Start generating constraints for let-expressions. Account for mutual recursion,
351c33cEvan Czaplicki
compiler/Type/Constrain/Expression.hs+59−15
compare with master
unifiedsplit
@@ -48,7 +48,7 @@ constrain env (L _ _ expr) tipe =
48 exists $ \t2 -> do
48 exists $ \t2 -> do
49 fragment <- Pattern.constrain env p t1
49 fragment <- Pattern.constrain env p t1
50 c2 <- constrain env e t2
50 c2 <- constrain env e t2
51− let c = ex (vars fragment) (CLet [Scheme [] [] CTrue (typeEnv fragment)]
51+ let c = ex (vars fragment) (CLet [monoscheme (typeEnv fragment)]
52 (typeConstraint fragment /\ c2 ))
52 (typeConstraint fragment /\ c2 ))
53 return $ c /\ tipe === (t1 ==> t2)
53 return $ c /\ tipe === (t1 ==> t2)
54
54
@@ -66,8 +66,6 @@ constrain env (L _ _ expr) tipe =
66 ce <- constrain env e tipe
66 ce <- constrain env e tipe
67 return (cb /\ ce)
67 return (cb /\ ce)
68
68
69− Let defs body -> error "not defined yet"
70−
71 Case e branches ->
69 Case e branches ->
72 exists $ \t -> do
70 exists $ \t -> do
73 ce <- constrain env e t
71 ce <- constrain env e t
@@ -75,7 +73,7 @@ constrain env (L _ _ expr) tipe =
75 fragment <- Pattern.constrain env p t
73 fragment <- Pattern.constrain env p t
76 c <- constrain env e tipe
74 c <- constrain env e tipe
77 return $ ex (vars fragment)
75 return $ ex (vars fragment)
78− (CLet [Scheme [] [] CTrue (typeEnv fragment)]
76+ (CLet [monoscheme (typeEnv fragment)]
79 (typeConstraint fragment /\ c))
77 (typeConstraint fragment /\ c))
80 CAnd . (:) ce <$> mapM branch branches
78 CAnd . (:) ce <$> mapM branch branches
81
79
@@ -140,16 +138,62 @@ constrain env (L _ _ expr) tipe =
140 Markdown _ ->
138 Markdown _ ->
141 return $ tipe === Env.get env builtin "Element"
139 return $ tipe === Env.get env builtin "Element"
142
140
141+ Let defs body ->
142+ do c <- constrain env body tipe
143+ (schemes, rqs, fqs, header, c2, c1) <-
144+ Monad.foldM (constrainDef env)
145+ ([], [], [], Map.empty, CTrue, CTrue)
146+ (collapseDefs defs)
147+ return $ CLet schemes
148+ (CLet [Scheme rqs fqs (CLet [monoscheme header] c2) header ]
149+ (c1 /\ c))
150+
151+
152+constrainDef env info (name, args, expr, maybeTipe) =
153+ let (schemes, rigidQuantifiers, flexibleQuantifiers, headers, c2, c1) = info in
154+ case maybeTipe of
155+ Just tipe ->
156+ do flexiVars <- mapM (\_ -> flexibleVar) args
157+ let inserts = zipWith (\arg typ -> Map.insert arg (VarN typ)) args flexiVars
158+ env' = env { value = List.foldl' (\x f -> f x) (value env) inserts }
159+ typ = error "This should be the internal representation of the user defined type."
160+ scheme = Scheme { rigidQuantifiers = [],
161+ flexibleQuantifiers = flexiVars,
162+ constraint = CTrue,
163+ header = Map.singleton name typ }
164+ c <- constrain env' expr typ
165+ return ( scheme : schemes
166+ , rigidQuantifiers
167+ , flexibleQuantifiers
168+ , headers
169+ , c2
170+ , fl rigidQuantifiers c /\ c1 )
171+
172+ Nothing ->
173+ do var <- flexibleVar
174+ rigidVars <- mapM (\_ -> rigidVar) args
175+ let tipe = VarN var
176+ inserts = zipWith (\arg typ -> Map.insert arg (VarN typ)) args rigidVars
177+ env' = env { value = List.foldl' (\x f -> f x) (value env) inserts }
178+ c <- constrain env' expr tipe
179+ return ( schemes
180+ , rigidVars ++ rigidQuantifiers
181+ , var : flexibleQuantifiers
182+ , Map.insert name tipe headers
183+ , c /\ c2
184+ , c1 )
143
185
144--collapseDefs :: [Def t v] -> [(String, [String], LExpr t v, Maybe Type)]
186--collapseDefs :: [Def t v] -> [(String, [String], LExpr t v, Maybe Type)]
145−collapseDefs = go Map.empty Map.empty
187+collapseDefs definitions =
188+ map (\(name, (args, expr, tipe)) -> (name, args, expr, tipe)) defPairs
146− where
189+ where
190+ defPairs = Map.toList (go Map.empty Map.empty definitions)
191+
147− go defs typs [] = Map.union (Map.intersectionWith (\f t -> f (Just t)) defs typs)
192+ go defs typs [] = Map.union (Map.intersectionWith (\f t -> f (Just t)) defs typs)
148− (Map.map ($ Nothing) (Map.difference defs typs))
193+ (Map.map ($ Nothing) (Map.difference defs typs))
149− go defs typs (d:ds) =
194+ go defs typs (d:ds) =
150− case d of
195+ case d of
151− Def name args body ->
196+ Def name args body ->
152− go (Map.insert name ((,,) args body) defs) typs ds
197+ go (Map.insert name ((,,) args body) defs) typs ds
153− TypeAnnotation name typ ->
198+ TypeAnnotation name typ ->
154− go defs (Map.insert name typ typs) ds
199+ go defs (Map.insert name typ typs) ds
155−
compiler/Type/Type.hs+9
@@ -37,6 +37,8 @@ data Scheme a b = Scheme {
37 header :: Map.Map String a -- mapping from names to types
37 header :: Map.Map String a -- mapping from names to types
38} deriving Show
38} deriving Show
39
39
40+monoscheme headers = Scheme [] [] CTrue headers
41+
40data Descriptor = Descriptor {
42data Descriptor = Descriptor {
41 structure :: Maybe (Term1 Variable),
43 structure :: Maybe (Term1 Variable),
42 rank :: Int,
44 rank :: Int,
@@ -83,6 +85,13 @@ flexibleVar = UF.fresh $ Descriptor {
83 name = Nothing
85 name = Nothing
84 }
86 }
85
87
88+rigidVar = UF.fresh $ Descriptor {
89+ structure = Nothing,
90+ rank = noRank,
91+ flex = Rigid,
92+ name = Nothing
93+ }
94+
86-- ex qs constraint == exists qs. constraint
95-- ex qs constraint == exists qs. constraint
87ex :: [Variable] -> TypeConstraint -> TypeConstraint
96ex :: [Variable] -> TypeConstraint -> TypeConstraint
88ex fqs constraint = CLet [Scheme [] fqs constraint Map.empty] CTrue
97ex fqs constraint = CLet [Scheme [] fqs constraint Map.empty] CTrue