on f5bdeae help sign in
elk/src/Types/Constrain.hs
89 lines 2.8 kB history raw
1{-# LANGUAGE GeneralizedNewtypeDeriving #-}
2module Constrain where
4import Ast
5import Types
6import qualified Data.Set as Set
7import qualified Data.Map as Map
8import Control.Monad (liftM,mapM)
9import Control.Monad.State (evalState, State, get, put)
11data Constraint = Type :=: Type
12 | Type :<: Type
13 | Type :<<: Scheme
14 deriving (Eq, Ord, Show)
16-- Wrapper around State monad.
17newtype GuidCounter a = GC { runGC :: State Int a }
18 deriving (Monad)
20-- Get the next GUID, incrementing the counter.
21guid :: GuidCounter Int
22guid = GC $ do n <- get
23 put (n + 1)
24 return n
26beta = VarT `liftM` guid
27unionA = Map.unionWith (++)
28unionsA = Map.unionsWith (++)
30constrain expr = Set.toList cs
31 where (as,cs,t) = evalState (runGC $ inference expr) 0
33inference (Var x) =
34 do b <- beta
35 return (Map.singleton x [b], Set.empty, b)
36inference (App e1 e2) =
37 do (a1,c1,t1) <- inference e1
38 (a2,c2,t2) <- inference e2
39 b <- beta
40 return ( unionA a1 a2
41 , Set.unions [c1,c2,Set.singleton $ t1 :=: (LambdaT t2 b)]
42 , b )
43inference (Lambda x e) =
44 do (a,c,t) <- inference e
45 b <- beta
46 return ( Map.delete x a
47 , Set.union c . Set.fromList . map (:=: b) $
48 Map.findWithDefault [] x a
49 , LambdaT b t )
50inference (Let defs e) =
51 do (a,c,t) <- inference e
52 let (xs,es) = unzip defs
53 (as,cs,ts) <- unzip3 `liftM` mapM inference es
54 let assumptions = unionsA (a:as)
55 let f x t = map (:<: t) $ Map.findWithDefault [] x assumptions
56 let constraints = Set.fromList . concat $ zipWith f xs ts
57 return ( foldr Map.delete assumptions xs
58 , Set.unions $ c:constraints:cs
59 , t )
61inference (If e1 e2 e3) =
62 do (a1,c1,t1) <- inference e1
63 (a2,c2,t2) <- inference e2
64 (a3,c3,t3) <- inference e3
65 return ( unionsA [a1,a2,a3]
66 , Set.unions [c1,c2,c3, Set.fromList [ t1 :=: BoolT, t2 :=: t3 ] ]
67 , t2 )
69inference (Data name es) =
70 do (as,cs,ts) <- unzip3 `liftM` mapM inference es
71 return ( unionsA as, Set.unions cs, ADT name ts )
73inference other =
74 case other of
75 Number _ -> primitive IntT
76 Chr _ -> primitive CharT
77 Boolean _ -> primitive BoolT
78 _ -> beta >>= primitive
80primitive t = return (Map.empty, Set.empty, t)
81{--
82 Let x e1 e2 ->
83 do (a1,c1,t1) <- inference e1
84 (a2,c2,t2) <- inference e2
85 let ts = Map.findWithDefault (error "inference") x a
86 return ( unionA a1 $ Map.delete x a2
87 , Set.unions [ c1, c2, Set.fromList $ map (:<: t1) ts ]
88 , t2 )
89--}