git.iko.soy/elk
on master help sign in
Add pretty printing for type constraints.
0ed7205Evan Czaplicki
compiler/Parse/Expression.hs+4−5
compare with master
unifiedsplit
@@ -12,7 +12,6 @@ import qualified Parse.Type as Type
12import Parse.Binop
12import Parse.Binop
13import Parse.Literal
13import Parse.Literal
14
14
15−import SourceSyntax.PrettyPrint
16import SourceSyntax.Location as Location
15import SourceSyntax.Location as Location
17import SourceSyntax.Pattern hiding (tuple,list)
16import SourceSyntax.Pattern hiding (tuple,list)
18import qualified SourceSyntax.Literal as Literal
17import qualified SourceSyntax.Literal as Literal
@@ -215,7 +214,7 @@ typeAnnotation = TypeAnnotation <$> try start <*> Type.expr
215def :: IParser (Def t v)
214def :: IParser (Def t v)
216def = typeAnnotation <|> assignExpr
215def = typeAnnotation <|> assignExpr
217
216
218−parseDef str =
217+attempt f parser str =
219− case iParse def "" str of
218+ case iParse parser "" str of
220− Right result -> Right result
219+ Right result -> f result
221− Left err -> Left $ "Parse error at " ++ show err
220+ Left err -> error $ "Parse error at " ++ show err
compiler/Type/Constrain/Expression.hs+79−31
@@ -1,25 +1,45 @@
1module Type.Constrain.Expression where
1module Type.Constrain.Expression where
2
2
3−import Control.Arrow (second)
4−import Control.Applicative ((<$>))
5import qualified Data.List as List
3import qualified Data.List as List
6import qualified Data.Map as Map
4import qualified Data.Map as Map
7−import qualified Control.Monad as Monad
8import Data.Map ((!))
5import Data.Map ((!))
6+import Control.Arrow (second)
7+import Control.Applicative ((<$>),(<*>))
8+import qualified Control.Monad as Monad
9+import Control.Monad.State
10+import Data.Traversable (traverse)
9
11
10import SourceSyntax.Location as Loc
12import SourceSyntax.Location as Loc
11import SourceSyntax.Pattern (Pattern(PVar))
13import SourceSyntax.Pattern (Pattern(PVar))
12import SourceSyntax.Expression
14import SourceSyntax.Expression
15+import qualified SourceSyntax.Type as SrcT
13import Type.Type hiding (Descriptor(..))
16import Type.Type hiding (Descriptor(..))
14import Type.Fragment
17import Type.Fragment
15−import Type.Environment as Env
18+import qualified Type.Environment as Env
16import qualified Type.Constrain.Literal as Literal
19import qualified Type.Constrain.Literal as Literal
17import qualified Type.Constrain.Pattern as Pattern
20import qualified Type.Constrain.Pattern as Pattern
18
21
19−
22+{-- Testing section --}
23+import SourceSyntax.PrettyPrint
24+import Parse.Expression
25+import Parse.Helpers (iParse)
26+
27+test str =
28+ case iParse expr "" str of
29+ Left err -> error $ "Parse error at " ++ show err
30+ Right expression -> do
31+ env <- Env.initialEnvironment
32+ var <- flexibleVar
33+ constraint <- constrain env expression (VarN var)
34+ prettyNames constraint
35+ print (pretty constraint)
36+ print (pretty var)
37+ return ()
38+{-- todo: remove testing code --}
39+
20−constrain :: Environment -> LExpr a b -> Type -> IO TypeConstraint
40+constrain :: Env.Environment -> LExpr a b -> Type -> IO TypeConstraint
21constrain env (L _ _ expr) tipe =
41constrain env (L _ _ expr) tipe =
22− let list t = TermN (App1 (Env.get env builtin "[]") t) in
42+ let list t = TermN (App1 (Env.get env Env.builtin "[_]") t) in
23 case expr of
43 case expr of
24 Literal lit -> return $ Literal.constrain env lit tipe
44 Literal lit -> return $ Literal.constrain env lit tipe
25
45
@@ -41,7 +61,7 @@ constrain env (L _ _ expr) tipe =
41 exists $ \t2 -> do
61 exists $ \t2 -> do
42 c1 <- constrain env e1 t1
62 c1 <- constrain env e1 t1
43 c2 <- constrain env e2 t2
63 c2 <- constrain env e2 t2
44− return $ CAnd [ c1, c2, (Env.get env value op) === (t1 ==> t2 ==> tipe) ]
64+ return $ CAnd [ c1, c2, op <? (t1 ==> t2 ==> tipe) ]
45
65
46 Lambda p e ->
66 Lambda p e ->
47 exists $ \t1 ->
67 exists $ \t1 ->
@@ -60,7 +80,7 @@ constrain env (L _ _ expr) tipe =
60
80
61 MultiIf branches -> CAnd <$> mapM constrain' branches
81 MultiIf branches -> CAnd <$> mapM constrain' branches
62 where
82 where
63− bool = Env.get env builtin "Bool"
83+ bool = Env.get env Env.builtin "Bool"
64 constrain' (b,e) = do
84 constrain' (b,e) = do
65 cb <- constrain env b bool
85 cb <- constrain env b bool
66 ce <- constrain env e tipe
86 ce <- constrain env e tipe
@@ -135,9 +155,8 @@ constrain env (L _ _ expr) tipe =
135
155
136
156
137 Markdown _ ->
157 Markdown _ ->
138− return $ tipe === Env.get env builtin "Element"
158+ return $ tipe === Env.get env Env.builtin "Element"
139
159
140−{--
141 Let defs body ->
160 Let defs body ->
142 do c <- constrain env body tipe
161 do c <- constrain env body tipe
143 (schemes, rqs, fqs, header, c2, c1) <-
162 (schemes, rqs, fqs, header, c2, c1) <-
@@ -149,15 +168,17 @@ constrain env (L _ _ expr) tipe =
149 (c1 /\ c))
168 (c1 /\ c))
150
169
151
170
152−constrainDef env info (name, qs, expr, maybeTipe) =
171+constrainDef env info (pattern, expr, maybeTipe) =
172+ let qs = [] -- should come from the def, but I'm not sure what would live there...
153− let (schemes, rigidQuantifiers, flexibleQuantifiers, headers, c2, c1) = info in
173+ (schemes, rigidQuantifiers, flexibleQuantifiers, headers, c2, c1) = info
174+ in
154− case maybeTipe of
175+ case (pattern, maybeTipe) of
155− Just tipe ->
176+ (PVar name, Just tipe) ->
156 do flexiVars <- mapM (\_ -> flexibleVar) qs
177 do flexiVars <- mapM (\_ -> flexibleVar) qs
157 let inserts = zipWith (\arg typ -> Map.insert arg (VarN typ)) qs flexiVars
178 let inserts = zipWith (\arg typ -> Map.insert arg (VarN typ)) qs flexiVars
158− env' = env { value = List.foldl' (\x f -> f x) (value env) inserts }
179+ env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
159− typ = error "This should be the internal representation of the user defined type."
180+ typ <- instantiateType tipe
160− scheme = Scheme { rigidQuantifiers = [],
181+ let scheme = Scheme { rigidQuantifiers = [],
161 flexibleQuantifiers = flexiVars,
182 flexibleQuantifiers = flexiVars,
162 constraint = CTrue,
183 constraint = CTrue,
163 header = Map.singleton name typ }
184 header = Map.singleton name typ }
@@ -169,12 +190,12 @@ constrainDef env info (name, qs, expr, maybeTipe) =
169 , c2
190 , c2
170 , fl rigidQuantifiers c /\ c1 )
191 , fl rigidQuantifiers c /\ c1 )
171
192
172− Nothing ->
193+ (PVar name, Nothing) ->
173 do var <- flexibleVar
194 do var <- flexibleVar
174 rigidVars <- mapM (\_ -> rigidVar) qs
195 rigidVars <- mapM (\_ -> rigidVar) qs
175 let tipe = VarN var
196 let tipe = VarN var
176 inserts = zipWith (\arg typ -> Map.insert arg (VarN typ)) qs rigidVars
197 inserts = zipWith (\arg typ -> Map.insert arg (VarN typ)) qs rigidVars
177− env' = env { value = List.foldl' (\x f -> f x) (value env) inserts }
198+ env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
178 c <- constrain env' expr tipe
199 c <- constrain env' expr tipe
179 return ( schemes
200 return ( schemes
180 , rigidVars ++ rigidQuantifiers
201 , rigidVars ++ rigidQuantifiers
@@ -183,18 +204,45 @@ constrainDef env info (name, qs, expr, maybeTipe) =
183 , c /\ c2
204 , c /\ c2
184 , c1 )
205 , c1 )
185
206
186−--collapseDefs :: [Def t v] -> [(String, [String], LExpr t v, Maybe Type)]
207+instantiateType :: SrcT.Type -> IO Type
187−collapseDefs definitions =
208+instantiateType sourceType = evalStateT (go sourceType) Map.empty
188− map (\(name, (expr, tipe)) -> (name, expr, tipe)) defPairs
189 where
209 where
210+ go :: SrcT.Type -> StateT (Map.Map String Variable) IO Type
211+ go sourceType =
212+ case sourceType of
213+ SrcT.Lambda t1 t2 -> TermN <$> (Fun1 <$> go t1 <*> go t2)
214+
215+ SrcT.Var x -> do
216+ dict <- get
217+ case Map.lookup x dict of
218+ Just var -> return (VarN var)
219+ Nothing -> do
220+ var <- liftIO $ namedVar x -- should this be Constant or Flexible?
221+ put (Map.insert x var dict)
222+ return (VarN var)
223+
224+ SrcT.Data name ts -> do
225+ ts' <- mapM go ts
226+ return $ foldr (\t result -> TermN $ App1 t result) (error "not sure how to look this up yet") ts'
227+
228+ SrcT.EmptyRecord -> return (TermN EmptyRecord1)
229+
230+ SrcT.Record fields ext ->
231+ TermN <$> (Record1 <$> traverse (mapM go) fields <*> go ext)
232+
233+collapseDefs :: [Def t v] -> [(Pattern, LExpr t v, Maybe SrcT.Type)]
190− defPairs = Map.toList (go Map.empty Map.empty definitions)
234+collapseDefs = go [] Map.empty Map.empty
191−
235+ where
192− go defs typs [] = Map.union (Map.intersectionWith (\f t -> f (Just t)) defs typs)
236+ go output defs typs [] =
237+ output ++ concatMap Map.elems [
238+ Map.intersectionWithKey (\k v t -> (PVar k, v, Just t)) defs typs,
193− (Map.map ($ Nothing) (Map.difference defs typs))
239+ Map.mapWithKey (\k v -> (PVar k, v, Nothing)) (Map.difference defs typs) ]
194− go defs typs (d:ds) =
240+ go output defs typs (d:ds) =
195 case d of
241 case d of
196− Def name body ->
242+ Def (PVar name) body ->
197− go (Map.insert name ((,) body) defs) typs ds
243+ go output (Map.insert name body defs) typs ds
244+ Def pattern body ->
245+ go ((pattern, body, Nothing) : output) defs typs ds
198 TypeAnnotation name typ ->
246 TypeAnnotation name typ ->
199− go defs (Map.insert name typ typs) ds
247+ go output defs (Map.insert name typ typs) ds
200--}
248--}
compiler/Type/Environment.hs+14−6
@@ -15,19 +15,27 @@ data Environment = Environment {
15initialEnvironment :: IO Environment
15initialEnvironment :: IO Environment
16initialEnvironment = do
16initialEnvironment = do
17 let mkPair name = fmap ((,) name . VarN) (namedVar name)
17 let mkPair name = fmap ((,) name . VarN) (namedVar name)
18− list <- mkPair "[]"
18+ list <- mkPair "[_]"
19+ int <- mkPair "Int"
19− prims <- mapM mkPair ["Int","Float","Char","Bool","Element"]
20+ prims <- mapM mkPair ["Float","Char","Bool","Element"]
21+ let builtins = list : int : prims
20
22
21 cons <- do v <- flexibleVar
23 cons <- do v <- flexibleVar
22 let vlist = TermN (App1 (snd list) (VarN v))
24 let vlist = TermN (App1 (snd list) (VarN v))
23 return ([v], VarN v ==> vlist ==> vlist)
25 return ([v], VarN v ==> vlist ==> vlist)
24
26
25− let builtins = list : prims
27+ nil <- do v <- flexibleVar
28+ return ([v], TermN (App1 (snd list) (VarN v)))
29+
30+ let add = snd int ==> snd int ==> snd int
31+
26 return $ Environment {
32 return $ Environment {
27− constructor = Map.singleton "::" cons,
33+ constructor = Map.fromList [("::", cons), ("[]", nil)],
28 builtin = Map.fromList builtins,
34 builtin = Map.fromList builtins,
29− value = Map.empty
35+ value = Map.empty -- Map.fromList [("+", add)]
30 }
36 }
31
37
32get :: Environment -> (Environment -> Map.Map String a) -> String -> a
38get :: Environment -> (Environment -> Map.Map String a) -> String -> a
33−get env subDict key = subDict env ! key
39+get env subDict key = Map.findWithDefault err key (subDict env)
40+ where
41+ err = error $ "Could not find '" ++ key ++ "' in the type environment."
compiler/Type/Type.hs+132−12
@@ -1,9 +1,14 @@
1module Type.Type where
1module Type.Type where
2
2
3−import Control.Applicative ((<$>))
3+import qualified Data.List as List
4import qualified Data.Map as Map
4import qualified Data.Map as Map
5import qualified Data.UnionFind.IO as UF
5import qualified Data.UnionFind.IO as UF
6+import SourceSyntax.PrettyPrint
7+import Text.PrettyPrint as P
6import System.IO.Unsafe
8import System.IO.Unsafe
9+import Control.Applicative ((<$>),(<*>))
10+import Control.Monad.State
11+import Data.Traversable (traverse)
7
12
8data Term1 a
13data Term1 a
9 = App1 a a
14 = App1 a a
@@ -16,6 +21,7 @@ data Term1 a
16data TermN a
21data TermN a
17 = VarN a
22 = VarN a
18 | TermN (Term1 (TermN a))
23 | TermN (Term1 (TermN a))
24+ deriving Show
19
25
20record fs rec = TermN (Record1 fs rec)
26record fs rec = TermN (Record1 fs rec)
21
27
@@ -34,7 +40,7 @@ data Scheme a b = Scheme {
34 rigidQuantifiers :: [b],
40 rigidQuantifiers :: [b],
35 flexibleQuantifiers :: [b],
41 flexibleQuantifiers :: [b],
36 constraint :: Constraint a b,
42 constraint :: Constraint a b,
37− header :: Map.Map String a -- mapping from names to types
43+ header :: Map.Map String a
38} deriving Show
44} deriving Show
39
45
40monoscheme headers = Scheme [] [] CTrue headers
46monoscheme headers = Scheme [] [] CTrue headers
@@ -45,7 +51,7 @@ data Descriptor = Descriptor {
45 flex :: Flex,
51 flex :: Flex,
46 name :: Maybe TypeName,
52 name :: Maybe TypeName,
47 mark :: Int
53 mark :: Int
48−}
54+} deriving Show
49
55
50noRank = -1
56noRank = -1
51outermostRank = 0 :: Int
57outermostRank = 0 :: Int
@@ -114,12 +120,126 @@ exists f = do
114instance Show a => Show (UF.Point a) where
120instance Show a => Show (UF.Point a) where
115 show point = unsafePerformIO $ fmap show (UF.descriptor point)
121 show point = unsafePerformIO $ fmap show (UF.descriptor point)
116
122
123+instance Pretty a => Pretty (UF.Point a) where
124+ pretty point = unsafePerformIO $ fmap pretty (UF.descriptor point)
125+
126+instance Pretty a => Pretty (Term1 a) where
127+ pretty term =
128+ case term of
129+ App1 f x -> pretty f <+> pretty x
130+ Fun1 arg body -> pretty arg <+> P.text "->" <+> pretty body
131+ Var1 x -> pretty x
132+ EmptyRecord1 -> P.braces P.empty
133+ Record1 fields ext ->
134+ P.braces (pretty ext <+> P.text "|" <+> P.sep (P.punctuate P.comma prettyFields))
135+ where
136+ mkPretty f t = P.text f <+> P.text ":" <+> pretty t
137+ prettyFields = concatMap (\(f,ts) -> map (mkPretty f) ts) (Map.toList fields)
138+
139+instance Pretty a => Pretty (TermN a) where
140+ pretty term =
141+ case term of
142+ VarN x -> pretty x
143+ TermN t1 -> pretty t1
144+
117−instance Show Descriptor where
145+instance Pretty Descriptor where
118− show desc = case name desc of
146+ pretty desc =
119− Just n -> n
120− Nothing -> show (structure desc)
147+ case (structure desc, name desc) of
121−
148+ (Just term, _) -> pretty term
149+ (_, Just name) -> P.text name
150+ _ -> P.text "?"
151+
122−instance Show a => Show (TermN a) where
152+instance (Pretty a, Pretty b) => Pretty (Constraint a b) where
123− show term = case term of
153+ pretty constraint =
124− VarN v -> show v
154+ case constraint of
125− TermN t -> "(" ++ show t ++ ")"
155+ CTrue -> P.text "True"
156+ CEqual a b -> pretty a <+> P.text "=" <+> pretty b
157+ CAnd [] -> P.text "True"
158+
159+ CAnd (c:cs) ->
160+ P.parens . P.sep $ pretty c : (map (\c -> P.text "and" <+> pretty c) cs)
161+
162+ CLet [Scheme [] fqs constraint header] CTrue | Map.null header ->
163+ P.hang binder 2 (pretty constraint)
164+ where
165+ binder = if null fqs then P.empty else
166+ P.text "exists" <+> P.hsep (map pretty fqs) <> P.text "."
167+
168+ CLet schemes constraint ->
169+ P.vcat [ P.hang (P.text "let") 4 (P.brackets . P.sep . P.punctuate P.comma $ map pretty schemes)
170+ , P.text "in " <+> pretty constraint ]
171+
172+ CInstance name tipe ->
173+ P.text name <+> P.text "<" <+> pretty tipe
174+
175+instance (Pretty a, Pretty b) => Pretty (Scheme a b) where
176+ pretty (Scheme rqs fqs constraint headers) =
177+ P.sep [ forall <+> frees <+> rigids, cs, headers' ]
178+ where
179+ forall = if Map.size headers + length rqs /= 0 then P.text "forall" else P.empty
180+ frees = P.hsep $ map pretty fqs
181+ rigids = if length rqs > 0 then P.braces . P.hsep $ map pretty rqs else empty
182+ cs = case constraint of
183+ CTrue -> P.empty
184+ CAnd [] -> P.empty
185+ _ -> P.brackets (pretty constraint)
186+ headers' = if Map.size headers > 0 then dict else P.empty
187+ dict = P.parens . P.sep . P.punctuate P.comma . map prettyPair $ Map.toList headers
188+ prettyPair (n,t) = P.text n <+> P.text ":" <+> pretty t
189+
190+
191+prettyNames constraint = do
192+ (_, rawVars) <- fold constraint [] getNames
193+ let vars = map head . List.group $ List.sort rawVars
194+ letters = map (:[]) ['a'..'z']
195+ suffix s = map (++s)
196+ allVars = letters ++ suffix "'" letters ++ concatMap (\n -> suffix (show n) letters) [0..]
197+ okayVars = filter (`notElem` vars) allVars
198+ fold constraint okayVars rename
199+ where
200+ getNames name vars =
201+ case name of
202+ Just var -> (name, var:vars)
203+ Nothing -> (name, vars)
204+
205+ rename name vars =
206+ case name of
207+ Just var -> (name, vars)
208+ Nothing -> (Just (head vars), tail vars)
209+
210+fold constraint initialState func =
211+ runStateT (prettyName constraint) initialState
212+ where
213+ prettyName constraint =
214+ case constraint of
215+ CTrue -> return CTrue
216+ CEqual a b -> CEqual <$> prettyTypeName a <*> prettyTypeName b
217+ CAnd cs -> CAnd <$> mapM prettyName cs
218+ CLet schemes c -> CLet <$> mapM prettySchemeName schemes <*> prettyName c
219+ CInstance name tipe -> CInstance name <$> prettyTypeName tipe
220+
221+ prettySchemeName (Scheme rqs fqs c headers) =
222+ Scheme <$> mapM prettyVarName rqs <*> mapM prettyVarName fqs <*> prettyName c <*> return headers
223+
224+ prettyVarName point = do
225+ state <- get
226+ put =<< do desc <- liftIO $ UF.descriptor point
227+ let (name', state') = func (name desc) state
228+ liftIO $ UF.setDescriptor point (desc { name = name' })
229+ return state'
230+ return point
231+
232+ prettyTypeName tipe =
233+ case tipe of
234+ VarN x -> VarN <$> prettyVarName x
235+ TermN term -> TermN <$> prettyTermName term
236+
237+ prettyTermName term =
238+ case term of
239+ App1 a b -> App1 <$> prettyTypeName a <*> prettyTypeName b
240+ Fun1 a b -> Fun1 <$> prettyTypeName a <*> prettyTypeName b
241+ Var1 a -> Var1 <$> prettyTypeName a
242+ EmptyRecord1 -> return EmptyRecord1
243+ Record1 fields ext -> Record1 <$> fields' <*> prettyTypeName ext
244+ where
245+ fields' = traverse (mapM prettyTypeName) fields