Permalink
Browse files

Redo type parser. Correct let-polymorphism in unification.

  • Loading branch information...
1 parent 5ba2f27 commit f76a22e1fa568b66d71575980e36537813455932 evancz committed May 18, 2012
Showing with 123 additions and 102 deletions.
  1. +7 −3 src/Initialize.hs
  2. +52 −40 src/Parse/ParseTypes.hs
  3. +11 −7 src/Parse/Parser.hs
  4. +6 −5 src/Parse/ParserLib.hs
  5. +1 −2 src/Types/Constrain.hs
  6. +7 −18 src/Types/Hints.hs
  7. +16 −4 src/Types/Types.hs
  8. +23 −23 src/Types/Unify.hs
View
@@ -11,19 +11,23 @@ import Lexer
import Parser (toExpr,toDefs)
import Rename (rename)
import Replace
-import System.IO.Unsafe
import Unify
+import Hints
-initialize str = unify =<< toDefs =<< tokenize str
-
+initialize str = do
+ (expr, hints') <- toDefs =<< tokenize str
+ subs <- unify (liftM2 (++) hints hints') (rename expr)
+ return (seq subs expr)
+{--
initialize' str = do
expr <- toDefs =<< tokenize str
-- let rexpr = rename expr
-- let init = simp_loop rexpr
-- return $ if depth init < depth rexpr then init else rexpr
return $ rename expr
+--}
{--
simp_loop exp = if exp == exp' then exp' else simp_loop exp'
where exp' = simp exp
@@ -2,56 +2,68 @@ module ParseTypes where
import Ast
import Combinators
-import Data.Char (isUpper)
+import Data.Char (isUpper,isLower)
+import Data.Maybe (fromMaybe)
+import Data.List (lookup)
import ParserLib
import Tokens
import Types
+import Guid
import Control.Monad (liftM)
-typeVar = do whitespace; t <- item
- case t of
- ID "Int" -> return IntT
- ID "String" -> return StringT
- ID "Char" -> return CharT
- ID "Bool" -> return BoolT
- ID (v:vs) -> return (if isUpper v then ADT (v:vs) []
- else VarT 0) --(v:vs))
- _ -> zero
-
-typeList = do t LBRACKET; ti <- typeExpr; t RBRACKET; return $ ADT "List" []
+data ParseType = VarPT String
+ | LambdaPT ParseType ParseType
+ | ADTPT String [ParseType]
+
+listPT t = ADTPT "List" [t]
+tuplePT ts = ADTPT ("Tuple" ++ show (length ts)) ts
+
+typeVar = liftM VarPT lowVar
+typeList = do t LBRACKET; te <- typeExpr; t RBRACKET; return $ listPT te
typeTuple = do { t LPAREN; ts <- sepBy (t COMMA) typeExpr; t RPAREN
- ; return $ case ts of { [t] -> t; _ -> ADT "Tuple" [] } }
+ ; return $ case ts of { [t] -> t ; _ -> tuplePT ts } }
+typeUnambiguous = typeList +|+ typeTuple
-typeUnamb = typeList +|+ typeTuple
+typeSimple = liftM VarPT var
+typeApp = do name <- capVar
+ args <- star (typeSimple +|+ typeUnambiguous)
+ return $ case args of
+ [] -> VarPT name
+ _ -> ADTPT name args
+
+typeExpr = do
+ t1 <- typeVar +|+ typeApp +|+ typeUnambiguous
+ arrow <- optional $ t ARROW
+ case arrow of Just ARROW -> LambdaPT t1 `liftM` typeExpr
+ Nothing -> return t1
-typeTerm = typeApp +|+ typeUnamb
+typeConstructor = do name <- capVar
+ args <- star (typeSimple +|+ typeUnambiguous)
+ return $ (,) name args
-typeApp = do
- tipe <- typeVar
- case tipe of
- ADT name _ -> AppT name `liftM` star typeTerm
- _ -> return tipe
+datatype = do
+ t DATA ; name <- capVar ; args <- star lowVar ; assign
+ tcs <- sepBy1 (opParser (=="|")) typeConstructor
+ return $ (map fst tcs , map toFunc tcs , toTypes name args tcs)
-typeExpr = do t1 <- typeTerm
- arrow <- optional $ t ARROW
- case arrow of
- Just ARROW -> LambdaT t1 `liftM` typeTerm
- Nothing -> return t1
+beta = VarT `liftM` guid
-typeConstr = do
- name <- capVar
- args <- star (typeVar +|+ typeUnamb)
- return (Constructor name args)
+toFunc (name,args) = foldr Lambda (Data name $ map Var argNames) argNames
+ where argNames = map (("a"++) . show) [1..length args]
-constr (Constructor name args) =
- (name, foldr Lambda (Data name (map Var argNames)) argNames)
- where argNames = map (("arg"++) . show) [1..length args]
+toTypes name args constructors = do
+ pairs <- mapM (\x -> (,) x `liftM` guid) args
+ return $ map (toType pairs . ADT name $ map (VarT . snd) pairs) constructors
-datatype = do
- t DATA
- adt <- capVar
- vs <- star var
- assign
- ts <- sepBy1 (opParser (=="|")) typeConstr
- -- (adt, foldr ForallT (ADT adt ts) vs)
- return (map constr ts)
+toType pairs outType (name,args) =
+ foldr (==>) outType (map toT args)
+ where toT (LambdaPT t1 t2) = toT t1 ==> toT t2
+ toT (ADTPT name args) = ADT name $ map toT args
+ toT (VarPT x@(c:_))
+ | isLower c = VarT . fromMaybe (-1) $ lookup x pairs
+ | otherwise = case x of "Int" -> IntT
+ "Number" -> IntT
+ "String" -> StringT
+ "Char" -> CharT
+ "Bool" -> BoolT
+ _ -> ADT x []
View
@@ -3,21 +3,23 @@ module Parser where
import Ast
import Binop (binops)
import Combinators
+import Control.Monad (liftM)
import Data.List (foldl')
+import Guid
import Lexer
import ParserLib
import ParseTypes (datatype)
import ParsePatterns
import Tokens
-import Control.Monad (liftM)
+import Types (Type (VarT))
-------- Basic Terms --------
numTerm = do { whitespace; t <- item
- ; case t of { NUMBER n -> return $ Number n; _ -> zero } }
+ ; case t of { NUMBER n -> return $ Number n; _ -> zero } }
strTerm = do { whitespace; t <- item
- ; case t of { STRING cs -> return . list $ map Chr cs
- ; _ -> zero } }
+ ; case t of { STRING cs -> return . list $ map Chr cs
+ ; _ -> zero } }
varTerm = Var `liftM` var
chrTerm = Chr `liftM` chr
@@ -105,12 +107,14 @@ expr = select [ letExpr
, lambdaExpr
]
-def = (:[]) `liftM` assignExprNospace
+def = do (f,e) <- assignExprNospace
+ return ([f], [e], guid >>= \x -> return [VarT x])
defs = do
- ds <- plus (whitespace >> plus (sat (==NEWLINE)) >> def +|+ datatype)
+ (fss,ess,tss) <- unzip3 `liftM` plus (whitespace >> plus (sat (==NEWLINE)) >> def +|+ datatype)
+ let (fs,es,ts) = (concat fss, concat ess, concat `liftM` sequence tss)
star $ sat (==NEWLINE) +|+ sat (==SPACES)
- return $ Let (concat ds) (Var "main")
+ return (Let (zip fs es) (Var "main"), liftM (zip fs) ts)
err = "Parse Error: Better error messages to come!"
toExpr = extractResult err . parse expr
@@ -2,15 +2,16 @@ module ParserLib where
import Ast
import Combinators
-import Data.Char (isUpper)
-import Control.Monad (liftM)
+import Data.Char (isUpper,isLower)
+import Control.Monad (liftM,guard)
import Tokens
varNoSpace = do { t <- item; case t of { ID v -> return v; _ -> zero } }
var = whitespace >> varNoSpace
-capVar = do
- whitespace; t <- item
- case t of { ID (v:vs) -> if isUpper v then return (v:vs) else zero }
+capVar = do whitespace; t <- item
+ case t of { ID (v:vs) -> guard (isUpper v) >> return (v:vs) ; _ -> zero }
+lowVar = do whitespace; t <- item
+ case t of { ID (v:vs) -> guard (isLower v) >> return (v:vs) ; _ -> zero }
chr = do { whitespace; t <- item; case t of { CHAR c -> return c; _ -> zero } }
@@ -8,7 +8,6 @@ import qualified Data.Map as Map
import Control.Monad (liftM,mapM)
import Control.Monad.State (evalState)
import Guid
-import Hints
data Constraint = Type :=: Type
| Type :<: Type
@@ -19,7 +18,7 @@ beta = VarT `liftM` guid
unionA = Map.unionWith (++)
unionsA = Map.unionsWith (++)
-constrain expr = run $ do
+constrain hints expr = do
(as,cs,t) <- inference expr
hs <- hints
let cMap = Map.intersectionWith (\t -> map (:<: t)) (Map.fromList hs) as
View
@@ -6,20 +6,6 @@ import Control.Arrow (first)
import Types
import Guid
-element = ADT "Element" []
-direction = ADT "Direction" []
-text = ADT "Text" []
-listOf t = ADT "List" [t]
-tuple2 a b = ADT "Tuple2" [a,b]
-string = listOf CharT
-
-infixr ==>
-t1 ==> t2 = LambdaT t1 t2
-
-infix 8 -:
-name -: tipe = (,) name tipe
-
-hasType t = map (-: t)
-------- Text and Elements --------
@@ -30,11 +16,12 @@ textToText = ["header", "italic", "bold", "underline"
textAttrs = [ "toText" -: string ==> text
, "link" -: string ==> text ==> text
- , "height" -: IntT ==> text ==> text
+-- , "height" -: IntT ==> text ==> text
] ++ hasType (text ==> text) textToText
elements = let iee = IntT ==> element ==> element in
[ "flow" -: direction ==> listOf element ==> element
+ , "layers" -: listOf element ==> element
, "opacity" -: iee
, "width" -: iee
, "height" -: iee
@@ -100,7 +87,7 @@ lists = liftM (map (first ("List."++)) . (++ints)) . sequence $
, do a <- var ; "reverse" -:: listOf a ==> listOf a
, do a <- var ; "intersperse" -:: a ==> listOf a ==> listOf a
, do a <- var ; "intercalate" -:: listOf a ==> listOf(listOf a) ==> listOf a
- , do [a,b] <- vars 2 ; "zip" -:: listOf a ==>listOf b ==>listOf(tuple2 a b)
+ , do [a,b] <- vars 2 ; "zip" -:: listOf a ==>listOf b ==>listOf(tupleOf [a,b])
, do [a,b] <- vars 2 ; "map" -:: (a ==> b) ==> listOf a ==> listOf b
, do [a,b] <- vars 2 ; "foldr" -:: (a ==> b ==> b) ==> b ==> listOf a ==> b
, do [a,b] <- vars 2 ; "foldl" -:: (a ==> b ==> b) ==> b ==> listOf a ==> b
@@ -113,5 +100,7 @@ lists = liftM (map (first ("List."++)) . (++ints)) . sequence $
-------- Everything --------
-hints = do fs <- funcs ; ls <- lists
- return $ fs ++ ls ++ str2elem ++ textAttrs ++ elements ++ math ++ bool
+hints = do
+ fs <- funcs ; ls <- lists
+ return $ fs ++ ls ++ math ++ bool
+ {--++ str2elem ++ textAttrs ++ elements--}
View
@@ -12,13 +12,25 @@ data Type = IntT
| BoolT
| LambdaT Type Type
| VarT X
- | AppT String [Type]
| ADT String [Type]
deriving (Eq, Ord)
data Scheme = Forall (Set.Set X) Type deriving (Eq, Ord, Show)
-data Constructor = Constructor String [Type] deriving (Eq, Show)
+element = ADT "Element" []
+direction = ADT "Direction" []
+text = ADT "Text" []
+listOf t = ADT "List" [t]
+tupleOf ts = ADT ("Tuple" ++ show (length ts)) ts
+string = listOf CharT
+
+infixr ==>
+t1 ==> t2 = LambdaT t1 t2
+
+infix 8 -:
+name -: tipe = (,) name tipe
+
+hasType t = map (-: t)
parens = ("("++) . (++")")
@@ -29,9 +41,9 @@ instance Show Type where
; StringT -> "String"
; CharT -> "Char"
; BoolT -> "Bool"
- ; LambdaT t1 t2 -> parens $ show t1 ++ " -> " ++ show t2
+ ; LambdaT t1@(LambdaT _ _) t2 -> parens (show t1) ++ " -> " ++ show t2
+ ; LambdaT t1 t2 -> show t1 ++ " -> " ++ show t2
; VarT x -> show x
- ; AppT name args -> name ++ " " ++ unwords (map show args)
; ADT "List" [tipe] -> "[" ++ show tipe ++ "]"
; ADT name [] -> name
; ADT name cs -> parens $ name ++ " " ++ unwords (map show cs)
View
@@ -3,36 +3,26 @@ module Unify where
import Constrain
import Control.Arrow (second)
+import Control.Monad (liftM)
+import qualified Data.Set as Set
import Types
-unify expr = const expr `fmap` solver (constrain expr) []
+import Guid
-solver [] subs = Right subs
+unify hints expr = run $ do
+ cs <- constrain hints expr
+ solver cs []
--------- Destruct Type-constructors --------
+solver [] subs = return $ Right subs
-solver ((t1@(ADT n1 ts1) :<: t2@(ADT n2 ts2)) : cs) subs =
- solver cs subs
--- if n1 /= n2 then uniError t1 t2 else
--- solver (zipWith (:<:) ts1 ts2 ++ cs) subs
+-------- Destruct Type-constructors --------
solver ((t1@(ADT n1 ts1) :=: t2@(ADT n2 ts2)) : cs) subs =
- solver cs subs
--- if n1 /= n2 then uniError t1 t2 else
--- solver (zipWith (:=:) ts1 ts2 ++ cs) subs
-
-solver ((LambdaT t1 t2 :<: LambdaT t1' t2') : cs) subs =
- solver ([ t1 :<: t1', t2 :<: t2' ] ++ cs) subs
-
+ if n1 /= n2 then uniError t1 t2 else
+ solver (zipWith (:=:) ts1 ts2 ++ cs) subs
solver ((LambdaT t1 t2 :=: LambdaT t1' t2') : cs) subs =
solver ([ t1 :=: t1', t2 :=: t2' ] ++ cs) subs
--------- subtypes --------
-
-solver ((t :<: VarT x) : cs) subs = solver cs' subs
- where cs' = if all isSubtype cs then (t :=: VarT x : cs) else (cs ++ [t :<: VarT x])
-solver ((t1 :<: t2) : cs) subs = solver ((t1 :=: t2) : cs) subs
-
-------- Type-equality --------
solver ((VarT x :=: t) : cs) subs =
@@ -42,16 +32,26 @@ solver ((t :=: VarT x) : cs) subs =
solver ((t1 :=: t2) : cs) subs =
if t1 /= t2 then uniError t1 t2 else solver cs subs
+-------- subtypes --------
+
+solver ((t1 :<: t2) : cs) subs = do
+ let f x = do y <- guid ; return (x,VarT y)
+ t2' <- foldr (uncurry tSub) t2 `liftM` (mapM f . Set.toList $ getVars t2)
+ solver ((t1 :=: t2') : cs) subs
+
cSub k v (t1 :=: t2) = tSub k v t1 :=: tSub k v t2
cSub k v (t1 :<: t2) = tSub k v t1 :<: tSub k v t2
tSub k v (VarT x) = if k == x then v else (VarT x)
tSub k v (LambdaT t1 t2) = LambdaT (tSub k v t1) (tSub k v t2)
+tSub k v (ADT name ts) = ADT name (map (tSub k v) ts)
tSub _ _ t = t
-isSubtype (_ :<: _) = True
-isSubtype _ = False
+getVars (VarT x) = Set.singleton x
+getVars (LambdaT t1 t2) = Set.union (getVars t1) (getVars t2)
+getVars (ADT name ts) = Set.unions $ map getVars ts
+getVars _ = Set.empty
uniError t1 t2 =
- Left $ "Type error: " ++ show t1 ++ " is not equal to " ++ show t2
+ return . Left $ "Type error: " ++ show t1 ++ " is not equal to " ++ show t2

0 comments on commit f76a22e

Please sign in to comment.