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.
This commit is contained in:
Evan Czaplicki
parent
96fd5bfd78
commit
0ed72056b6
4 changed files with 226 additions and 51 deletions
|
|
@ -12,7 +12,6 @@ import qualified Parse.Type as Type
|
|||
import Parse.Binop
|
||||
import Parse.Literal
|
||||
|
||||
import SourceSyntax.PrettyPrint
|
||||
import SourceSyntax.Location as Location
|
||||
import SourceSyntax.Pattern hiding (tuple,list)
|
||||
import qualified SourceSyntax.Literal as Literal
|
||||
|
|
@ -215,7 +214,7 @@ typeAnnotation = TypeAnnotation <$> try start <*> Type.expr
|
|||
def :: IParser (Def t v)
|
||||
def = typeAnnotation <|> assignExpr
|
||||
|
||||
parseDef str =
|
||||
case iParse def "" str of
|
||||
Right result -> Right result
|
||||
Left err -> Left $ "Parse error at " ++ show err
|
||||
attempt f parser str =
|
||||
case iParse parser "" str of
|
||||
Right result -> f result
|
||||
Left err -> error $ "Parse error at " ++ show err
|
||||
|
|
|
|||
|
|
@ -1,25 +1,45 @@
|
|||
module Type.Constrain.Expression where
|
||||
|
||||
import Control.Arrow (second)
|
||||
import Control.Applicative ((<$>))
|
||||
import qualified Data.List as List
|
||||
import qualified Data.Map as Map
|
||||
import qualified Control.Monad as Monad
|
||||
import Data.Map ((!))
|
||||
import Control.Arrow (second)
|
||||
import Control.Applicative ((<$>),(<*>))
|
||||
import qualified Control.Monad as Monad
|
||||
import Control.Monad.State
|
||||
import Data.Traversable (traverse)
|
||||
|
||||
import SourceSyntax.Location as Loc
|
||||
import SourceSyntax.Pattern (Pattern(PVar))
|
||||
import SourceSyntax.Expression
|
||||
import qualified SourceSyntax.Type as SrcT
|
||||
import Type.Type hiding (Descriptor(..))
|
||||
import Type.Fragment
|
||||
import Type.Environment as Env
|
||||
import qualified Type.Environment as Env
|
||||
import qualified Type.Constrain.Literal as Literal
|
||||
import qualified Type.Constrain.Pattern as Pattern
|
||||
|
||||
{-- Testing section --}
|
||||
import SourceSyntax.PrettyPrint
|
||||
import Parse.Expression
|
||||
import Parse.Helpers (iParse)
|
||||
|
||||
constrain :: Environment -> LExpr a b -> Type -> IO TypeConstraint
|
||||
test str =
|
||||
case iParse expr "" str of
|
||||
Left err -> error $ "Parse error at " ++ show err
|
||||
Right expression -> do
|
||||
env <- Env.initialEnvironment
|
||||
var <- flexibleVar
|
||||
constraint <- constrain env expression (VarN var)
|
||||
prettyNames constraint
|
||||
print (pretty constraint)
|
||||
print (pretty var)
|
||||
return ()
|
||||
{-- todo: remove testing code --}
|
||||
|
||||
constrain :: Env.Environment -> LExpr a b -> Type -> IO TypeConstraint
|
||||
constrain env (L _ _ expr) tipe =
|
||||
let list t = TermN (App1 (Env.get env builtin "[]") t) in
|
||||
let list t = TermN (App1 (Env.get env Env.builtin "[_]") t) in
|
||||
case expr of
|
||||
Literal lit -> return $ Literal.constrain env lit tipe
|
||||
|
||||
|
|
@ -41,7 +61,7 @@ constrain env (L _ _ expr) tipe =
|
|||
exists $ \t2 -> do
|
||||
c1 <- constrain env e1 t1
|
||||
c2 <- constrain env e2 t2
|
||||
return $ CAnd [ c1, c2, (Env.get env value op) === (t1 ==> t2 ==> tipe) ]
|
||||
return $ CAnd [ c1, c2, op <? (t1 ==> t2 ==> tipe) ]
|
||||
|
||||
Lambda p e ->
|
||||
exists $ \t1 ->
|
||||
|
|
@ -60,7 +80,7 @@ constrain env (L _ _ expr) tipe =
|
|||
|
||||
MultiIf branches -> CAnd <$> mapM constrain' branches
|
||||
where
|
||||
bool = Env.get env builtin "Bool"
|
||||
bool = Env.get env Env.builtin "Bool"
|
||||
constrain' (b,e) = do
|
||||
cb <- constrain env b bool
|
||||
ce <- constrain env e tipe
|
||||
|
|
@ -135,9 +155,8 @@ constrain env (L _ _ expr) tipe =
|
|||
|
||||
|
||||
Markdown _ ->
|
||||
return $ tipe === Env.get env builtin "Element"
|
||||
return $ tipe === Env.get env Env.builtin "Element"
|
||||
|
||||
{--
|
||||
Let defs body ->
|
||||
do c <- constrain env body tipe
|
||||
(schemes, rqs, fqs, header, c2, c1) <-
|
||||
|
|
@ -149,15 +168,17 @@ constrain env (L _ _ expr) tipe =
|
|||
(c1 /\ c))
|
||||
|
||||
|
||||
constrainDef env info (name, qs, expr, maybeTipe) =
|
||||
let (schemes, rigidQuantifiers, flexibleQuantifiers, headers, c2, c1) = info in
|
||||
case maybeTipe of
|
||||
Just tipe ->
|
||||
constrainDef env info (pattern, expr, maybeTipe) =
|
||||
let qs = [] -- should come from the def, but I'm not sure what would live there...
|
||||
(schemes, rigidQuantifiers, flexibleQuantifiers, headers, c2, c1) = info
|
||||
in
|
||||
case (pattern, maybeTipe) of
|
||||
(PVar name, Just tipe) ->
|
||||
do flexiVars <- mapM (\_ -> flexibleVar) qs
|
||||
let inserts = zipWith (\arg typ -> Map.insert arg (VarN typ)) qs flexiVars
|
||||
env' = env { value = List.foldl' (\x f -> f x) (value env) inserts }
|
||||
typ = error "This should be the internal representation of the user defined type."
|
||||
scheme = Scheme { rigidQuantifiers = [],
|
||||
env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
|
||||
typ <- instantiateType tipe
|
||||
let scheme = Scheme { rigidQuantifiers = [],
|
||||
flexibleQuantifiers = flexiVars,
|
||||
constraint = CTrue,
|
||||
header = Map.singleton name typ }
|
||||
|
|
@ -169,12 +190,12 @@ constrainDef env info (name, qs, expr, maybeTipe) =
|
|||
, c2
|
||||
, fl rigidQuantifiers c /\ c1 )
|
||||
|
||||
Nothing ->
|
||||
(PVar name, Nothing) ->
|
||||
do var <- flexibleVar
|
||||
rigidVars <- mapM (\_ -> rigidVar) qs
|
||||
let tipe = VarN var
|
||||
inserts = zipWith (\arg typ -> Map.insert arg (VarN typ)) qs rigidVars
|
||||
env' = env { value = List.foldl' (\x f -> f x) (value env) inserts }
|
||||
env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
|
||||
c <- constrain env' expr tipe
|
||||
return ( schemes
|
||||
, rigidVars ++ rigidQuantifiers
|
||||
|
|
@ -183,18 +204,45 @@ constrainDef env info (name, qs, expr, maybeTipe) =
|
|||
, c /\ c2
|
||||
, c1 )
|
||||
|
||||
--collapseDefs :: [Def t v] -> [(String, [String], LExpr t v, Maybe Type)]
|
||||
collapseDefs definitions =
|
||||
map (\(name, (expr, tipe)) -> (name, expr, tipe)) defPairs
|
||||
instantiateType :: SrcT.Type -> IO Type
|
||||
instantiateType sourceType = evalStateT (go sourceType) Map.empty
|
||||
where
|
||||
defPairs = Map.toList (go Map.empty Map.empty definitions)
|
||||
go :: SrcT.Type -> StateT (Map.Map String Variable) IO Type
|
||||
go sourceType =
|
||||
case sourceType of
|
||||
SrcT.Lambda t1 t2 -> TermN <$> (Fun1 <$> go t1 <*> go t2)
|
||||
|
||||
go defs typs [] = Map.union (Map.intersectionWith (\f t -> f (Just t)) defs typs)
|
||||
(Map.map ($ Nothing) (Map.difference defs typs))
|
||||
go defs typs (d:ds) =
|
||||
SrcT.Var x -> do
|
||||
dict <- get
|
||||
case Map.lookup x dict of
|
||||
Just var -> return (VarN var)
|
||||
Nothing -> do
|
||||
var <- liftIO $ namedVar x -- should this be Constant or Flexible?
|
||||
put (Map.insert x var dict)
|
||||
return (VarN var)
|
||||
|
||||
SrcT.Data name ts -> do
|
||||
ts' <- mapM go ts
|
||||
return $ foldr (\t result -> TermN $ App1 t result) (error "not sure how to look this up yet") ts'
|
||||
|
||||
SrcT.EmptyRecord -> return (TermN EmptyRecord1)
|
||||
|
||||
SrcT.Record fields ext ->
|
||||
TermN <$> (Record1 <$> traverse (mapM go) fields <*> go ext)
|
||||
|
||||
collapseDefs :: [Def t v] -> [(Pattern, LExpr t v, Maybe SrcT.Type)]
|
||||
collapseDefs = go [] Map.empty Map.empty
|
||||
where
|
||||
go output defs typs [] =
|
||||
output ++ concatMap Map.elems [
|
||||
Map.intersectionWithKey (\k v t -> (PVar k, v, Just t)) defs typs,
|
||||
Map.mapWithKey (\k v -> (PVar k, v, Nothing)) (Map.difference defs typs) ]
|
||||
go output defs typs (d:ds) =
|
||||
case d of
|
||||
Def name body ->
|
||||
go (Map.insert name ((,) body) defs) typs ds
|
||||
Def (PVar name) body ->
|
||||
go output (Map.insert name body defs) typs ds
|
||||
Def pattern body ->
|
||||
go ((pattern, body, Nothing) : output) defs typs ds
|
||||
TypeAnnotation name typ ->
|
||||
go defs (Map.insert name typ typs) ds
|
||||
go output defs (Map.insert name typ typs) ds
|
||||
--}
|
||||
|
|
@ -15,19 +15,27 @@ data Environment = Environment {
|
|||
initialEnvironment :: IO Environment
|
||||
initialEnvironment = do
|
||||
let mkPair name = fmap ((,) name . VarN) (namedVar name)
|
||||
list <- mkPair "[]"
|
||||
prims <- mapM mkPair ["Int","Float","Char","Bool","Element"]
|
||||
list <- mkPair "[_]"
|
||||
int <- mkPair "Int"
|
||||
prims <- mapM mkPair ["Float","Char","Bool","Element"]
|
||||
let builtins = list : int : prims
|
||||
|
||||
cons <- do v <- flexibleVar
|
||||
let vlist = TermN (App1 (snd list) (VarN v))
|
||||
return ([v], VarN v ==> vlist ==> vlist)
|
||||
|
||||
let builtins = list : prims
|
||||
nil <- do v <- flexibleVar
|
||||
return ([v], TermN (App1 (snd list) (VarN v)))
|
||||
|
||||
let add = snd int ==> snd int ==> snd int
|
||||
|
||||
return $ Environment {
|
||||
constructor = Map.singleton "::" cons,
|
||||
constructor = Map.fromList [("::", cons), ("[]", nil)],
|
||||
builtin = Map.fromList builtins,
|
||||
value = Map.empty
|
||||
value = Map.empty -- Map.fromList [("+", add)]
|
||||
}
|
||||
|
||||
get :: Environment -> (Environment -> Map.Map String a) -> String -> a
|
||||
get env subDict key = subDict env ! key
|
||||
get env subDict key = Map.findWithDefault err key (subDict env)
|
||||
where
|
||||
err = error $ "Could not find '" ++ key ++ "' in the type environment."
|
||||
|
|
@ -1,9 +1,14 @@
|
|||
module Type.Type where
|
||||
|
||||
import Control.Applicative ((<$>))
|
||||
import qualified Data.List as List
|
||||
import qualified Data.Map as Map
|
||||
import qualified Data.UnionFind.IO as UF
|
||||
import SourceSyntax.PrettyPrint
|
||||
import Text.PrettyPrint as P
|
||||
import System.IO.Unsafe
|
||||
import Control.Applicative ((<$>),(<*>))
|
||||
import Control.Monad.State
|
||||
import Data.Traversable (traverse)
|
||||
|
||||
data Term1 a
|
||||
= App1 a a
|
||||
|
|
@ -16,6 +21,7 @@ data Term1 a
|
|||
data TermN a
|
||||
= VarN a
|
||||
| TermN (Term1 (TermN a))
|
||||
deriving Show
|
||||
|
||||
record fs rec = TermN (Record1 fs rec)
|
||||
|
||||
|
|
@ -34,7 +40,7 @@ data Scheme a b = Scheme {
|
|||
rigidQuantifiers :: [b],
|
||||
flexibleQuantifiers :: [b],
|
||||
constraint :: Constraint a b,
|
||||
header :: Map.Map String a -- mapping from names to types
|
||||
header :: Map.Map String a
|
||||
} deriving Show
|
||||
|
||||
monoscheme headers = Scheme [] [] CTrue headers
|
||||
|
|
@ -45,7 +51,7 @@ data Descriptor = Descriptor {
|
|||
flex :: Flex,
|
||||
name :: Maybe TypeName,
|
||||
mark :: Int
|
||||
}
|
||||
} deriving Show
|
||||
|
||||
noRank = -1
|
||||
outermostRank = 0 :: Int
|
||||
|
|
@ -114,12 +120,126 @@ exists f = do
|
|||
instance Show a => Show (UF.Point a) where
|
||||
show point = unsafePerformIO $ fmap show (UF.descriptor point)
|
||||
|
||||
instance Show Descriptor where
|
||||
show desc = case name desc of
|
||||
Just n -> n
|
||||
Nothing -> show (structure desc)
|
||||
instance Pretty a => Pretty (UF.Point a) where
|
||||
pretty point = unsafePerformIO $ fmap pretty (UF.descriptor point)
|
||||
|
||||
instance Show a => Show (TermN a) where
|
||||
show term = case term of
|
||||
VarN v -> show v
|
||||
TermN t -> "(" ++ show t ++ ")"
|
||||
instance Pretty a => Pretty (Term1 a) where
|
||||
pretty term =
|
||||
case term of
|
||||
App1 f x -> pretty f <+> pretty x
|
||||
Fun1 arg body -> pretty arg <+> P.text "->" <+> pretty body
|
||||
Var1 x -> pretty x
|
||||
EmptyRecord1 -> P.braces P.empty
|
||||
Record1 fields ext ->
|
||||
P.braces (pretty ext <+> P.text "|" <+> P.sep (P.punctuate P.comma prettyFields))
|
||||
where
|
||||
mkPretty f t = P.text f <+> P.text ":" <+> pretty t
|
||||
prettyFields = concatMap (\(f,ts) -> map (mkPretty f) ts) (Map.toList fields)
|
||||
|
||||
instance Pretty a => Pretty (TermN a) where
|
||||
pretty term =
|
||||
case term of
|
||||
VarN x -> pretty x
|
||||
TermN t1 -> pretty t1
|
||||
|
||||
instance Pretty Descriptor where
|
||||
pretty desc =
|
||||
case (structure desc, name desc) of
|
||||
(Just term, _) -> pretty term
|
||||
(_, Just name) -> P.text name
|
||||
_ -> P.text "?"
|
||||
|
||||
instance (Pretty a, Pretty b) => Pretty (Constraint a b) where
|
||||
pretty constraint =
|
||||
case constraint of
|
||||
CTrue -> P.text "True"
|
||||
CEqual a b -> pretty a <+> P.text "=" <+> pretty b
|
||||
CAnd [] -> P.text "True"
|
||||
|
||||
CAnd (c:cs) ->
|
||||
P.parens . P.sep $ pretty c : (map (\c -> P.text "and" <+> pretty c) cs)
|
||||
|
||||
CLet [Scheme [] fqs constraint header] CTrue | Map.null header ->
|
||||
P.hang binder 2 (pretty constraint)
|
||||
where
|
||||
binder = if null fqs then P.empty else
|
||||
P.text "exists" <+> P.hsep (map pretty fqs) <> P.text "."
|
||||
|
||||
CLet schemes constraint ->
|
||||
P.vcat [ P.hang (P.text "let") 4 (P.brackets . P.sep . P.punctuate P.comma $ map pretty schemes)
|
||||
, P.text "in " <+> pretty constraint ]
|
||||
|
||||
CInstance name tipe ->
|
||||
P.text name <+> P.text "<" <+> pretty tipe
|
||||
|
||||
instance (Pretty a, Pretty b) => Pretty (Scheme a b) where
|
||||
pretty (Scheme rqs fqs constraint headers) =
|
||||
P.sep [ forall <+> frees <+> rigids, cs, headers' ]
|
||||
where
|
||||
forall = if Map.size headers + length rqs /= 0 then P.text "forall" else P.empty
|
||||
frees = P.hsep $ map pretty fqs
|
||||
rigids = if length rqs > 0 then P.braces . P.hsep $ map pretty rqs else empty
|
||||
cs = case constraint of
|
||||
CTrue -> P.empty
|
||||
CAnd [] -> P.empty
|
||||
_ -> P.brackets (pretty constraint)
|
||||
headers' = if Map.size headers > 0 then dict else P.empty
|
||||
dict = P.parens . P.sep . P.punctuate P.comma . map prettyPair $ Map.toList headers
|
||||
prettyPair (n,t) = P.text n <+> P.text ":" <+> pretty t
|
||||
|
||||
|
||||
prettyNames constraint = do
|
||||
(_, rawVars) <- fold constraint [] getNames
|
||||
let vars = map head . List.group $ List.sort rawVars
|
||||
letters = map (:[]) ['a'..'z']
|
||||
suffix s = map (++s)
|
||||
allVars = letters ++ suffix "'" letters ++ concatMap (\n -> suffix (show n) letters) [0..]
|
||||
okayVars = filter (`notElem` vars) allVars
|
||||
fold constraint okayVars rename
|
||||
where
|
||||
getNames name vars =
|
||||
case name of
|
||||
Just var -> (name, var:vars)
|
||||
Nothing -> (name, vars)
|
||||
|
||||
rename name vars =
|
||||
case name of
|
||||
Just var -> (name, vars)
|
||||
Nothing -> (Just (head vars), tail vars)
|
||||
|
||||
fold constraint initialState func =
|
||||
runStateT (prettyName constraint) initialState
|
||||
where
|
||||
prettyName constraint =
|
||||
case constraint of
|
||||
CTrue -> return CTrue
|
||||
CEqual a b -> CEqual <$> prettyTypeName a <*> prettyTypeName b
|
||||
CAnd cs -> CAnd <$> mapM prettyName cs
|
||||
CLet schemes c -> CLet <$> mapM prettySchemeName schemes <*> prettyName c
|
||||
CInstance name tipe -> CInstance name <$> prettyTypeName tipe
|
||||
|
||||
prettySchemeName (Scheme rqs fqs c headers) =
|
||||
Scheme <$> mapM prettyVarName rqs <*> mapM prettyVarName fqs <*> prettyName c <*> return headers
|
||||
|
||||
prettyVarName point = do
|
||||
state <- get
|
||||
put =<< do desc <- liftIO $ UF.descriptor point
|
||||
let (name', state') = func (name desc) state
|
||||
liftIO $ UF.setDescriptor point (desc { name = name' })
|
||||
return state'
|
||||
return point
|
||||
|
||||
prettyTypeName tipe =
|
||||
case tipe of
|
||||
VarN x -> VarN <$> prettyVarName x
|
||||
TermN term -> TermN <$> prettyTermName term
|
||||
|
||||
prettyTermName term =
|
||||
case term of
|
||||
App1 a b -> App1 <$> prettyTypeName a <*> prettyTypeName b
|
||||
Fun1 a b -> Fun1 <$> prettyTypeName a <*> prettyTypeName b
|
||||
Var1 a -> Var1 <$> prettyTypeName a
|
||||
EmptyRecord1 -> return EmptyRecord1
|
||||
Record1 fields ext -> Record1 <$> fields' <*> prettyTypeName ext
|
||||
where
|
||||
fields' = traverse (mapM prettyTypeName) fields
|
||||
|
|
|
|||
Loading…
Reference in a new issue