Pipe source locations through the type checker

This commit is contained in:
Evan Czaplicki 2013-07-30 16:01:20 -07:00
parent c6868f1bd6
commit b1f53d04ed
7 changed files with 77 additions and 52 deletions

View file

@ -22,10 +22,16 @@ import qualified Transform.SortDefinitions as SD
constrain :: Env.Environment -> LExpr a b -> Type -> IO TypeConstraint
constrain env (L _ expr) tipe =
let list t = Env.get env Env.types "_List" <| t in
constrain env (L span expr) tipe =
let list t = Env.get env Env.types "_List" <| t
and = L span . CAnd
true = L span CTrue
t1 === t2 = L span (CEqual t1 t2)
x <? t = L span (CInstance x t)
clet schemes c = L span (CLet schemes c)
in
case expr of
Literal lit -> Literal.constrain env lit tipe
Literal lit -> Literal.constrain env span lit tipe
Var name -> return (name <? tipe)
@ -33,26 +39,26 @@ constrain env (L _ expr) tipe =
exists $ \x -> do
clo <- constrain env lo x
chi <- constrain env hi x
return $ CAnd [clo, chi, list x === tipe]
return $ and [clo, chi, list x === tipe]
ExplicitList exprs ->
exists $ \x -> do
cs <- mapM (\e -> constrain env e x) exprs
return $ CAnd (list x === tipe : cs)
return . and $ list x === tipe : cs
Binop op e1 e2 ->
exists $ \t1 ->
exists $ \t2 -> do
c1 <- constrain env e1 t1
c2 <- constrain env e2 t2
return $ CAnd [ c1, c2, op <? (t1 ==> t2 ==> tipe) ]
return $ and [ c1, c2, op <? (t1 ==> t2 ==> tipe) ]
Lambda p e ->
exists $ \t1 ->
exists $ \t2 -> do
fragment <- Pattern.constrain env p t1
c2 <- constrain env e t2
let c = ex (vars fragment) (CLet [monoscheme (typeEnv fragment)]
let c = ex (vars fragment) (clet [monoscheme (typeEnv fragment)]
(typeConstraint fragment /\ c2 ))
return $ c /\ tipe === (t1 ==> t2)
@ -62,7 +68,7 @@ constrain env (L _ expr) tipe =
c2 <- constrain env e2 t
return $ c1 /\ c2
MultiIf branches -> CAnd <$> mapM constrain' branches
MultiIf branches -> and <$> mapM constrain' branches
where
bool = Env.get env Env.types "Bool"
constrain' (b,e) = do
@ -75,12 +81,12 @@ constrain env (L _ expr) tipe =
ce <- constrain env exp t
let branch (p,e) = do
fragment <- Pattern.constrain env p t
CLet [toScheme fragment] <$> constrain env e tipe
CAnd . (:) ce <$> mapM branch branches
clet [toScheme fragment] <$> constrain env e tipe
and . (:) ce <$> mapM branch branches
Data name exprs ->
do pairs <- mapM pair exprs
(ctipe, cs) <- Monad.foldM step (tipe,CTrue) (reverse pairs)
(ctipe, cs) <- Monad.foldM step (tipe,true) (reverse pairs)
return (cs /\ name <? ctipe)
where
pair e = do v <- var Flexible -- needs an ex
@ -104,7 +110,7 @@ constrain env (L _ expr) tipe =
cVal <- constrain env value tVal
cRec <- constrain env e tRec
let c = tipe === record (Map.singleton label [tVal]) tRec
return (CAnd [cVal, cRec, c])
return (and [cVal, cRec, c])
Modify e fields ->
exists $ \t -> do
@ -118,28 +124,28 @@ constrain env (L _ expr) tipe =
cs <- zipWithM (constrain env) (map snd fields) (map VarN newVars)
return $ cOld /\ ex newVars (CAnd (cNew : cs))
return $ cOld /\ ex newVars (and (cNew : cs))
Record fields ->
do vars <- forM fields $ \_ -> var Flexible
cs <- zipWithM (constrain env) (map snd fields) (map VarN vars)
let fields' = SrcT.fieldMap (zip (map fst fields) (map VarN vars))
recordType = record fields' (TermN EmptyRecord1)
return . ex vars $ CAnd (tipe === recordType : cs)
return . ex vars . and $ tipe === recordType : cs
Markdown _ ->
return $ tipe === Env.get env Env.types "Element"
Let defs body ->
do c <- case body of
L _ (Var name) | name == saveEnvName -> return CSaveEnv
L _ (Var name) | name == saveEnvName -> return (L span CSaveEnv)
_ -> constrain env body tipe
(schemes, rqs, fqs, header, c2, c1) <-
Monad.foldM (constrainDef env)
([], [], [], Map.empty, CTrue, CTrue)
([], [], [], Map.empty, true, true)
(collapseDefs defs)
return $ CLet schemes
(CLet [Scheme rqs fqs (CLet [monoscheme header] c2) header ]
return $ clet schemes
(clet [Scheme rqs fqs (clet [monoscheme header] c2) header ]
(c1 /\ c))
constrainDef env info (pattern, expr, maybeTipe) =
@ -154,7 +160,7 @@ constrainDef env info (pattern, expr, maybeTipe) =
(vars, typ) <- Env.instantiateType env tipe Map.empty
let scheme = Scheme { rigidQuantifiers = [],
flexibleQuantifiers = flexiVars ++ vars,
constraint = CTrue,
constraint = Loc.none CTrue,
header = Map.singleton name typ }
c <- constrain env' expr typ
return ( scheme : schemes

View file

@ -4,16 +4,22 @@ import Data.Map ((!))
import qualified Data.Map as Map
import SourceSyntax.Literal
import SourceSyntax.Location
import Type.Type
import Type.Fragment
import Type.Environment as Env
constrain :: Environment -> Literal -> Type -> IO TypeConstraint
constrain env literal tipe =
let prim name = Env.get env Env.types name in
case literal of
IntNum _ -> fmap (\n -> tipe === VarN n) (var (Is Number))
FloatNum _ -> return $ tipe === prim "Float"
Chr _ -> return $ tipe === prim "Char"
Str _ -> return $ tipe === TermN (App1 (prim "_List") (prim "Char"))
Boolean _ -> return $ tipe === prim "Bool"
constrain :: Environment -> SrcSpan -> Literal -> Type -> IO TypeConstraint
constrain env span literal tipe =
do tipe' <- litType
return . L span $ CEqual tipe tipe'
where
prim name = Env.get env Env.types name
litType =
case literal of
IntNum _ -> VarN `fmap` var (Is Number)
FloatNum _ -> return (prim "Float")
Chr _ -> return (prim "Char")
Str _ -> return (TermN (App1 (prim "_List") (prim "Char")))
Boolean _ -> return (prim "Bool")

View file

@ -9,6 +9,7 @@ import Data.Map ((!))
import qualified Data.Map as Map
import SourceSyntax.Pattern
import qualified SourceSyntax.Location as Loc
import Type.Type
import Type.Fragment
import Type.Environment as Env
@ -17,11 +18,15 @@ import qualified Type.Constrain.Literal as Literal
constrain :: Environment -> Pattern -> Type -> IO Fragment
constrain env pattern tipe =
let span = Loc.NoSpan
t1 === t2 = Loc.L span (CEqual t1 t2)
x <? t = Loc.L span (CInstance x t)
in
case pattern of
PAnything -> return emptyFragment
PLiteral lit -> do
c <- Literal.constrain env lit tipe
c <- Literal.constrain env span lit tipe
return $ emptyFragment { typeConstraint = c }
PVar name -> do

View file

@ -5,6 +5,7 @@ import qualified Data.Map as Map
import Type.Type
import SourceSyntax.Pattern
import SourceSyntax.Location (none)
data Fragment = Fragment {
typeEnv :: Map.Map String Type,
@ -12,7 +13,7 @@ data Fragment = Fragment {
typeConstraint :: TypeConstraint
} deriving Show
emptyFragment = Fragment Map.empty [] CTrue
emptyFragment = Fragment Map.empty [] (none CTrue)
joinFragment f1 f2 = Fragment {
typeEnv = Map.union (typeEnv f1) (typeEnv f2),

View file

@ -10,6 +10,7 @@ import qualified Type.Solve as Solve
import SourceSyntax.Module as Module
import qualified SourceSyntax.Expression as Expr
import SourceSyntax.Location (none)
import SourceSyntax.PrettyPrint
import Text.PrettyPrint
import qualified Type.State as TS
@ -37,7 +38,7 @@ infer interfaces modul = unsafePerformIO $ do
let allTypes = ctors ++ importedVars
vars = concatMap (fst . snd) allTypes
header = Map.map snd (Map.fromList allTypes)
environ = T.CLet [ T.Scheme vars [] T.CTrue header ]
environ = none . T.CLet [ T.Scheme vars [] (none T.CTrue) header ]
fvar <- T.var T.Flexible
constraint <- environ `fmap` TcExpr.constrain env (program modul) (T.VarN fvar)

View file

@ -13,6 +13,7 @@ import Type.Unify
import qualified Type.Environment as Env
import qualified Type.State as TS
import qualified Text.PrettyPrint as P
import SourceSyntax.Location (Located(L))
-- | Every variable has rank less than or equal to the maxRank of the pool.
@ -92,7 +93,7 @@ adjustRank youngMark visitedMark groupRank variable =
solve :: TypeConstraint -> StateT TS.SolverState IO ()
solve constraint =
solve (L span constraint) =
case constraint of
CTrue -> return ()
@ -105,7 +106,7 @@ solve constraint =
CAnd cs -> mapM_ solve cs
CLet [Scheme [] fqs constraint' _] CTrue -> do
CLet [Scheme [] fqs constraint' _] (L _ CTrue) -> do
oldEnv <- TS.getEnv
mapM TS.introduce fqs
solve constraint'

View file

@ -10,6 +10,7 @@ import System.IO.Unsafe
import Control.Applicative ((<$>),(<*>))
import Control.Monad.State
import Data.Traversable (traverse)
import SourceSyntax.Location
import SourceSyntax.Helpers (isTuple)
import qualified SourceSyntax.Type as Src
@ -35,7 +36,8 @@ type Variable = UF.Point Descriptor
type SchemeName = String
type TypeName = String
data Constraint a b
type Constraint a b = Located (BasicConstraint a b)
data BasicConstraint a b
= CTrue
| CSaveEnv
| CEqual a a
@ -54,20 +56,16 @@ data Scheme a b = Scheme {
type TypeConstraint = Constraint Type Variable
type TypeScheme = Scheme Type Variable
monoscheme headers = Scheme [] [] CTrue headers
monoscheme headers = Scheme [] [] (none CTrue) headers
infixl 8 /\
(/\) :: Constraint a b -> Constraint a b -> Constraint a b
a /\ CTrue = a
CTrue /\ b = b
a /\ b = CAnd [a,b]
(===) :: Type -> Type -> TypeConstraint
(===) = CEqual
(<?) :: SchemeName -> Type -> TypeConstraint
x <? t = CInstance x t
a@(L s1 c1) /\ b@(L s2 c2) =
case (c1, c2) of
(CTrue, _) -> b
(_, CTrue) -> a
_ -> merge a b (CAnd [a,b])
infixr 9 ==>
(==>) :: Type -> Type -> Type
@ -126,11 +124,11 @@ structuredVar structure = UF.fresh $ Descriptor {
-- ex qs constraint == exists qs. constraint
ex :: [Variable] -> TypeConstraint -> TypeConstraint
ex fqs constraint = CLet [Scheme [] fqs constraint Map.empty] CTrue
ex fqs constraint@(L s _) = L s $ CLet [Scheme [] fqs constraint Map.empty] (L s CTrue)
-- fl qs constraint == forall qs. constraint
fl :: [Variable] -> TypeConstraint -> TypeConstraint
fl rqs constraint = CLet [Scheme rqs [] constraint Map.empty] CTrue
fl rqs constraint@(L s _) = L s $ CLet [Scheme rqs [] constraint Map.empty] (L s CTrue)
exists :: (Type -> IO TypeConstraint) -> IO TypeConstraint
exists f = do
@ -146,6 +144,10 @@ instance PrettyType a => PrettyType (UF.Point a) where
pretty when point = unsafePerformIO $ fmap (pretty when) (UF.descriptor point)
instance PrettyType a => PrettyType (Located a) where
pretty when (L _ e) = pretty when e
instance PrettyType a => PrettyType (Term1 a) where
pretty when term =
let prty = pretty Never in
@ -194,7 +196,7 @@ instance PrettyType Descriptor where
_ -> P.text "?"
instance (PrettyType a, PrettyType b) => PrettyType (Constraint a b) where
instance (PrettyType a, PrettyType b) => PrettyType (BasicConstraint a b) where
pretty _ constraint =
let prty = pretty Never in
case constraint of
@ -206,12 +208,12 @@ instance (PrettyType a, PrettyType b) => PrettyType (Constraint a b) where
CAnd cs ->
P.parens . P.sep $ P.punctuate (P.text " and") (map (pretty Never) cs)
CLet [Scheme [] fqs constraint header] CTrue | Map.null header ->
CLet [Scheme [] fqs constraint header] (L _ CTrue) | Map.null header ->
P.sep [ binder, pretty Never c ]
where
mergeExists vs c =
mergeExists vs (L _ c) =
case c of
CLet [Scheme [] fqs' c' _] CTrue -> mergeExists (vs ++ fqs') c'
CLet [Scheme [] fqs' c' _] (L _ CTrue) -> mergeExists (vs ++ fqs') c'
_ -> (vs, c)
(fqs', c) = mergeExists fqs constraint
@ -227,7 +229,7 @@ instance (PrettyType a, PrettyType b) => PrettyType (Constraint a b) where
P.text name <+> P.text "<" <+> prty tipe
instance (PrettyType a, PrettyType b) => PrettyType (Scheme a b) where
pretty _ (Scheme rqs fqs constraint headers) =
pretty _ (Scheme rqs fqs (L _ constraint) headers) =
P.sep [ forall, cs, headers' ]
where
prty = pretty Never
@ -287,7 +289,10 @@ class Crawl t where
-> t
-> StateT CrawlState IO t
instance (Crawl t, Crawl v) => Crawl (Constraint t v) where
instance Crawl a => Crawl (Located a) where
crawl nextState (L s e) = L s <$> crawl nextState e
instance (Crawl t, Crawl v) => Crawl (BasicConstraint t v) where
crawl nextState constraint =
let rnm = crawl nextState in
case constraint of