git.iko.soy/elk
on master help sign in
Add pretty printing for type constraints.

Convert source-syntax types into type-checker types and print them with pretty type variables. Generate constraints for let-expressions using type annotations. Build test function to turn strings into type constraints.

commit0ed72056b6de32d62a03ca6ca192dffba500fb4f authorEvan Czaplicki <evan@Evans-MacBook-Air.local> dateMon 8 Jul 2013, 16:47 (13 years ago) parent96fd5bf
4 files changed+229−54
compare with master
unifiedsplit
compiler/Parse/Expression.hs+4−5 compiler/Type/Constrain/Expression.hs+79−31 compiler/Type/Environment.hs+14−6 compiler/Type/Type.hs+132−12
compiler/Parse/Expression.hs+4−5
@@ -12,7 +12,6 @@ import qualified Parse.Type as Type
1212import Parse.Binop
1313import Parse.Literal
1414
15−import SourceSyntax.PrettyPrint
1615import SourceSyntax.Location as Location
1716import SourceSyntax.Pattern hiding (tuple,list)
1817import qualified SourceSyntax.Literal as Literal
@@ -215,7 +214,7 @@ typeAnnotation = TypeAnnotation <$> try start <*> Type.expr
215214def :: IParser (Def t v)
216215def = typeAnnotation <|> assignExpr
217216
218−parseDef str =
219− case iParse def "" str of
220− Right result -> Right result
221− Left err -> Left $ "Parse error at " ++ show err
217+attempt f parser str =
218+ case iParse parser "" str of
219+ Right result -> f result
220+ Left err -> error $ "Parse error at " ++ show err
compiler/Type/Constrain/Expression.hs+79−31
@@ -1,25 +1,45 @@
11module Type.Constrain.Expression where
22
3−import Control.Arrow (second)
4−import Control.Applicative ((<$>))
53import qualified Data.List as List
64import qualified Data.Map as Map
7−import qualified Control.Monad as Monad
85import 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)
911
1012import SourceSyntax.Location as Loc
1113import SourceSyntax.Pattern (Pattern(PVar))
1214import SourceSyntax.Expression
15+import qualified SourceSyntax.Type as SrcT
1316import Type.Type hiding (Descriptor(..))
1417import Type.Fragment
15−import Type.Environment as Env
18+import qualified Type.Environment as Env
1619import qualified Type.Constrain.Literal as Literal
1720import qualified Type.Constrain.Pattern as Pattern
1821
19−
20−constrain :: Environment -> LExpr a b -> Type -> IO TypeConstraint
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+
40+constrain :: Env.Environment -> LExpr a b -> Type -> IO TypeConstraint
2141constrain 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
2343 case expr of
2444 Literal lit -> return $ Literal.constrain env lit tipe
2545
@@ -41,7 +61,7 @@ constrain env (L _ _ expr) tipe =
4161 exists $ \t2 -> do
4262 c1 <- constrain env e1 t1
4363 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) ]
4565
4666 Lambda p e ->
4767 exists $ \t1 ->
@@ -60,7 +80,7 @@ constrain env (L _ _ expr) tipe =
6080
6181 MultiIf branches -> CAnd <$> mapM constrain' branches
6282 where
63− bool = Env.get env builtin "Bool"
83+ bool = Env.get env Env.builtin "Bool"
6484 constrain' (b,e) = do
6585 cb <- constrain env b bool
6686 ce <- constrain env e tipe
@@ -135,9 +155,8 @@ constrain env (L _ _ expr) tipe =
135155
136156
137157 Markdown _ ->
138− return $ tipe === Env.get env builtin "Element"
158+ return $ tipe === Env.get env Env.builtin "Element"
139159
140−{--
141160 Let defs body ->
142161 do c <- constrain env body tipe
143162 (schemes, rqs, fqs, header, c2, c1) <-
@@ -149,15 +168,17 @@ constrain env (L _ _ expr) tipe =
149168 (c1 /\ c))
150169
151170
152−constrainDef env info (name, qs, expr, maybeTipe) =
153− let (schemes, rigidQuantifiers, flexibleQuantifiers, headers, c2, c1) = info in
154− case maybeTipe of
155− Just tipe ->
171+constrainDef env info (pattern, expr, maybeTipe) =
172+ let qs = [] -- should come from the def, but I'm not sure what would live there...
173+ (schemes, rigidQuantifiers, flexibleQuantifiers, headers, c2, c1) = info
174+ in
175+ case (pattern, maybeTipe) of
176+ (PVar name, Just tipe) ->
156177 do flexiVars <- mapM (\_ -> flexibleVar) qs
157178 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 }
159− typ = error "This should be the internal representation of the user defined type."
160− scheme = Scheme { rigidQuantifiers = [],
179+ env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
180+ typ <- instantiateType tipe
181+ let scheme = Scheme { rigidQuantifiers = [],
161182 flexibleQuantifiers = flexiVars,
162183 constraint = CTrue,
163184 header = Map.singleton name typ }
@@ -169,12 +190,12 @@ constrainDef env info (name, qs, expr, maybeTipe) =
169190 , c2
170191 , fl rigidQuantifiers c /\ c1 )
171192
172− Nothing ->
193+ (PVar name, Nothing) ->
173194 do var <- flexibleVar
174195 rigidVars <- mapM (\_ -> rigidVar) qs
175196 let tipe = VarN var
176197 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 }
178199 c <- constrain env' expr tipe
179200 return ( schemes
180201 , rigidVars ++ rigidQuantifiers
@@ -183,18 +204,45 @@ constrainDef env info (name, qs, expr, maybeTipe) =
183204 , c /\ c2
184205 , c1 )
185206
186−--collapseDefs :: [Def t v] -> [(String, [String], LExpr t v, Maybe Type)]
187−collapseDefs definitions =
188− map (\(name, (expr, tipe)) -> (name, expr, tipe)) defPairs
207+instantiateType :: SrcT.Type -> IO Type
208+instantiateType sourceType = evalStateT (go sourceType) Map.empty
189209 where
190− defPairs = Map.toList (go Map.empty Map.empty definitions)
191−
192− go defs typs [] = Map.union (Map.intersectionWith (\f t -> f (Just t)) defs typs)
193− (Map.map ($ Nothing) (Map.difference defs typs))
194− go defs typs (d:ds) =
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)]
234+collapseDefs = go [] Map.empty Map.empty
235+ where
236+ go output defs typs [] =
237+ output ++ concatMap Map.elems [
238+ Map.intersectionWithKey (\k v t -> (PVar k, v, Just t)) defs typs,
239+ Map.mapWithKey (\k v -> (PVar k, v, Nothing)) (Map.difference defs typs) ]
240+ go output defs typs (d:ds) =
195241 case d of
196− Def name body ->
197− go (Map.insert name ((,) body) defs) typs ds
242+ Def (PVar name) body ->
243+ go output (Map.insert name body defs) typs ds
244+ Def pattern body ->
245+ go ((pattern, body, Nothing) : output) defs typs ds
198246 TypeAnnotation name typ ->
199− go defs (Map.insert name typ typs) ds
247+ go output defs (Map.insert name typ typs) ds
200248--}
compiler/Type/Environment.hs+14−6
@@ -15,19 +15,27 @@ data Environment = Environment {
1515initialEnvironment :: IO Environment
1616initialEnvironment = do
1717 let mkPair name = fmap ((,) name . VarN) (namedVar name)
18− list <- mkPair "[]"
19− prims <- mapM mkPair ["Int","Float","Char","Bool","Element"]
18+ list <- mkPair "[_]"
19+ int <- mkPair "Int"
20+ prims <- mapM mkPair ["Float","Char","Bool","Element"]
21+ let builtins = list : int : prims
2022
2123 cons <- do v <- flexibleVar
2224 let vlist = TermN (App1 (snd list) (VarN v))
2325 return ([v], VarN v ==> vlist ==> vlist)
2426
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+
2632 return $ Environment {
27− constructor = Map.singleton "::" cons,
33+ constructor = Map.fromList [("::", cons), ("[]", nil)],
2834 builtin = Map.fromList builtins,
29− value = Map.empty
35+ value = Map.empty -- Map.fromList [("+", add)]
3036 }
3137
3238get :: 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 @@
11module Type.Type where
22
3−import Control.Applicative ((<$>))
3+import qualified Data.List as List
44import qualified Data.Map as Map
55import qualified Data.UnionFind.IO as UF
6+import SourceSyntax.PrettyPrint
7+import Text.PrettyPrint as P
68import System.IO.Unsafe
9+import Control.Applicative ((<$>),(<*>))
10+import Control.Monad.State
11+import Data.Traversable (traverse)
712
813data Term1 a
914 = App1 a a
@@ -16,6 +21,7 @@ data Term1 a
1621data TermN a
1722 = VarN a
1823 | TermN (Term1 (TermN a))
24+ deriving Show
1925
2026record fs rec = TermN (Record1 fs rec)
2127
@@ -34,7 +40,7 @@ data Scheme a b = Scheme {
3440 rigidQuantifiers :: [b],
3541 flexibleQuantifiers :: [b],
3642 constraint :: Constraint a b,
37− header :: Map.Map String a -- mapping from names to types
43+ header :: Map.Map String a
3844} deriving Show
3945
4046monoscheme headers = Scheme [] [] CTrue headers
@@ -45,7 +51,7 @@ data Descriptor = Descriptor {
4551 flex :: Flex,
4652 name :: Maybe TypeName,
4753 mark :: Int
48−}
54+} deriving Show
4955
5056noRank = -1
5157outermostRank = 0 :: Int
@@ -114,12 +120,126 @@ exists f = do
114120instance Show a => Show (UF.Point a) where
115121 show point = unsafePerformIO $ fmap show (UF.descriptor point)
116122
117−instance Show Descriptor where
118− show desc = case name desc of
119− Just n -> n
120− Nothing -> show (structure desc)
121−
122−instance Show a => Show (TermN a) where
123− show term = case term of
124− VarN v -> show v
125− TermN t -> "(" ++ show t ++ ")"
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+
145+instance Pretty Descriptor where
146+ pretty desc =
147+ case (structure desc, name desc) of
148+ (Just term, _) -> pretty term
149+ (_, Just name) -> P.text name
150+ _ -> P.text "?"
151+
152+instance (Pretty a, Pretty b) => Pretty (Constraint a b) where
153+ pretty constraint =
154+ case constraint of
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