Skip to content

Commit

Permalink
compiler/tc: wip - #61
Browse files Browse the repository at this point in the history 
Plan is:
1. we need to generate constraints when we take/put, to guarantee
that in a single take/put expression, the field is not repetitive.
2. in the solver, we check for well-formedness in `whnf' function.

[skip ci]
  • Loading branch information
Zilin Chen authored and Zilin Chen committed Feb 5, 2018
1 parent 00bbf5a commit ff38b42
Show file tree
Hide file tree
Showing 3 changed files with 40 additions and 34 deletions.
28 changes: 14 additions & 14 deletions cogent/src/Cogent/TypeCheck/Base.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,8 +28,8 @@ import Cogent.Util

import Control.Arrow (second)
import Control.Lens hiding (Context, (:<))
-- import Control.Monad.Except
import Control.Monad.State
import Control.Monad.Trans.Except
import Control.Monad.Trans.Maybe
import Control.Monad.Writer hiding (Alt)
import Data.Either (either, isLeft)
Expand Down Expand Up @@ -296,9 +296,9 @@ instance Monoid TcLogState where


type TcM a = MaybeT (StateT TcLogState (StateT TcState IO)) a
type TcConsM lcl a = StateT lcl (StateT TcState IO) a
type TcBaseM a = StateT TcState IO a

type TcConsM lcl a = StateT lcl (StateT TcState IO) a
type TcErrM err a = ExceptT err (StateT TcState IO) a
type TcBaseM a = StateT TcState IO a


-- -----------------------------------------------------------------------------
Expand Down Expand Up @@ -348,29 +348,29 @@ substType vs (T t) = T (fmap (substType vs) t)

-- Check for type well-formedness
validateType :: [VarName] -> RawType -> TcM TCType
validateType vs t = either (\e -> logErr e >> exitErr) return =<< lift (lift $ validateType' vs t)
validateType vs t = either (\e -> logErr e >> exitErr) return =<< lift (lift $ runExceptT $ validateType' vs t)

-- don't log erros, but instead return them
validateType' :: [VarName] -> RawType -> TcBaseM (Either TypeError TCType)
validateType' :: [VarName] -> RawType -> TcErrM TypeError TCType
validateType' vs (RT t) = do
ts <- use knownTypes
case t of
TVar v _ | v `notElem` vs -> return (Left $ UnknownTypeVariable v)
TCon t as _ | Nothing <- lookup t ts -> return (Left $ UnknownTypeConstructor t)
TVar v _ | v `notElem` vs -> throwE (UnknownTypeVariable v)
TCon t as _ | Nothing <- lookup t ts -> throwE (UnknownTypeConstructor t)
| Just (vs, _) <- lookup t ts
, provided <- length as
, required <- length vs
, provided /= required
-> return (Left $ TypeArgumentMismatch t provided required)
-> throwE (TypeArgumentMismatch t provided required)
TRecord fs _ | fields <- map fst fs
, fields' <- nub fields
-> if fields' == fields
then return . fmap T . sequence =<< traverse (validateType' vs) t
else return (Left $ DuplicateRecordFields (fields \\ fields'))
_ -> return . fmap T . sequence =<< traverse (validateType' vs) t
then T <$> mapM (validateType' vs) t
else throwE (DuplicateRecordFields (fields \\ fields'))
_ -> T <$> mapM (validateType' vs) t

validateTypes' :: (Traversable t) => [VarName] -> t RawType -> TcBaseM (Either TypeError (t TCType))
validateTypes' vs rs = sequence <$> traverse (validateType' vs) rs
validateTypes' :: (Traversable t) => [VarName] -> t RawType -> TcErrM TypeError (t TCType)
validateTypes' vs rs = mapM (validateType' vs) rs


-- Remove a pattern from a type, for case expressions.
Expand Down
10 changes: 5 additions & 5 deletions cogent/src/Cogent/TypeCheck/Generator.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,8 +36,8 @@ import Cogent.Util hiding (Warning)

import Control.Arrow (first, second)
import Control.Lens hiding (Context, each, zoom, (:<))
import Control.Monad.Except
import Control.Monad.State
import Control.Monad.Trans.Except
import Data.Functor.Compose
import qualified Data.Map as M
import qualified Data.IntMap as IM
Expand Down Expand Up @@ -187,7 +187,7 @@ cg' (Lam pat mt e) t = do
Nothing -> return (Sat, alpha)
Just t' -> do
tvs <- use knownTypeVars
lift (validateType' tvs (stripLocT t')) >>= \case
lift (runExceptT $ validateType' tvs (stripLocT t')) >>= \case
Left e -> return (Unsat e, alpha)
Right t'' -> return (F alpha :< F t'', t'')
(s, cp, pat') <- match pat alpha'
Expand Down Expand Up @@ -258,7 +258,7 @@ cg' (Seq e1 e2) t = do

cg' (TypeApp f as i) t = do
tvs <- use knownTypeVars
(ct,as') <- lift (validateTypes' tvs (fmap stripLocT $ Compose as)) >>= \case
(ct,as') <- lift (runExceptT $ validateTypes' tvs (fmap stripLocT $ Compose as)) >>= \case
Left e -> return (Unsat e, [])
Right ts -> return (Sat, getCompose ts)
lift (use $ knownFuns.at f) >>= \case
Expand Down Expand Up @@ -339,7 +339,7 @@ cg' (Match e bs alts) t = do
cg' (Annot e tau) t = do
tvs <- use knownTypeVars
let t' = stripLocT tau
(c, t'') <- lift (validateType' tvs t') >>= \case
(c, t'') <- lift (runExceptT $ validateType' tvs t') >>= \case
Left e'' -> return (Unsat e'', t)
Right t'' -> return (F t :< F t'', t'')
(c', e') <- cg e t''
Expand Down Expand Up @@ -499,7 +499,7 @@ withBindings (Binding pat tau e bs : xs) a = do
Nothing -> return (Sat, alpha)
Just tau' -> do
tvs <- use knownTypeVars
lift (validateType' tvs (stripLocT tau')) >>= \case
lift (runExceptT $ validateType' tvs (stripLocT tau')) >>= \case
Left e -> return (Unsat e, alpha)
Right t -> return (F alpha :< F t, t)
(s, cp, pat') <- match pat alpha'
Expand Down
36 changes: 21 additions & 15 deletions cogent/src/Cogent/TypeCheck/Solver.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,7 @@ import qualified Cogent.TypeCheck.GoalSet as GS
import Control.Applicative
import Control.Lens hiding ((:<))
import Control.Monad.State
import Control.Monad.Trans.Except
import qualified Data.Foldable as F
import Data.Function (on)
import qualified Data.IntMap as IM
Expand Down Expand Up @@ -76,15 +77,15 @@ crunch x = return [Goal [] x]
-- Operators like TUnbox, TBang etc. are left in place if there is
-- a unification variable.

whnf :: TCType -> TcBaseM TCType
whnf :: TCType -> TcErrM TypeError TCType
whnf (T (TUnbox t)) = do
t' <- whnf t
return $ case t' of
_ | notWhnf t' -> T (TUnbox t')
(T (TCon x ps _)) -> T (TCon x ps Unboxed)
(T (TRecord l _)) -> T (TRecord l Unboxed)
(T o) -> T (fmap (T . TUnbox) o)
_ -> error "impossible"
_ -> __impossible "whnf"

whnf (T (TBang t)) = do
t' <- whnf t
Expand All @@ -95,27 +96,27 @@ whnf (T (TBang t)) = do
(T (TVar b _)) -> T (TVar b True)
(T (TFun {})) -> t'
(T o) -> T (fmap (T . TBang) o)
_ -> error "impossible"
_ -> __impossible "whnf"

whnf (T (TTake fs t)) = do
t' <- whnf t
return $ case t' of
(T (TRecord l s)) -> T (TRecord (takeFields fs l) s)
(T (TVariant l)) -> T (TVariant (M.fromList $ takeFields fs $ M.toList l))
_ | Just fs' <- fs, null fs' -> t'
_ -> T (TTake fs t')
case t' of
(T (TRecord l s)) -> return $ T (TRecord (takeFields fs l) s)
(T (TVariant l)) -> return $ T (TVariant (M.fromList $ takeFields fs $ M.toList l))
_ | Just fs' <- fs, null fs' -> return $ t'
_ -> return $ T (TTake fs t')
where
takeFields :: Maybe [FieldName] -> [(FieldName, (a , Bool))] -> [(FieldName, (a, Bool))]
takeFields Nothing = map (fmap (fmap (const True)))
takeFields (Just fs) = map (\(f, (t, b)) -> (f, (t, f `elem` fs || b)))

whnf (T (TPut fs t)) = do
t' <- whnf t
return $ case t' of
(T (TRecord l s)) -> T (TRecord (putFields fs l) s)
(T (TVariant l)) -> T (TVariant (M.fromList $ putFields fs $ M.toList l))
_ | Just fs' <- fs, null fs' -> t'
_ -> T (TPut fs t')
case t' of
(T (TRecord l s)) -> return $ T (TRecord (putFields fs l) s)
(T (TVariant l)) -> return $ T (TVariant (M.fromList $ putFields fs $ M.toList l))
_ | Just fs' <- fs, null fs' -> return $ t'
_ -> return $ T (TPut fs t')
where
putFields :: Maybe [FieldName] -> [(FieldName, (a, Bool))] -> [(FieldName, (a, Bool))]
putFields Nothing = map (fmap (fmap (const False)))
Expand Down Expand Up @@ -412,13 +413,13 @@ auto :: Constraint -> TcBaseM Constraint
auto c = do
traceTc "sol" (text "auto")
let ?lvl = 0
c' <- simp c
c' <- simp' c
liftIO (rule' c') >>= \case
Nothing -> return c'
Just c'' -> auto c''

-- applies whnf to every type in a constraint.
simp :: Constraint -> TcBaseM Constraint
simp :: Constraint -> TcErrM TypeError Constraint
simp (a :< b) = (:<) <$> traverse whnf a <*> traverse whnf b
simp (Upcastable a b) = Upcastable <$> whnf a <*> whnf b
simp (a :& b) = (:&) <$> simp a <*> simp b
Expand All @@ -431,6 +432,11 @@ simp (SemiSat w) = pure (SemiSat w)
simp Sat = pure Sat
simp (Exhaustive t ps) = Exhaustive <$> whnf t <*> pure ps

simp' :: Constraint -> TcBaseM Constraint
simp' c = runExceptT (simp c) >>= \case
Left e -> return $ Unsat e
Right c -> return c

fresh :: VarOrigin -> Solver TCType
fresh ctx = do
i <- flexes <<%= succ
Expand Down

0 comments on commit ff38b42

Please sign in to comment.