[more work on new typechecker in progress
John Meacham <john@repetae.net>**20051208045453] addfile ./FrontEnd/Tc/Type.hs
hunk ./FrontEnd/TIModule.hs 26
-import FrontEnd.Tc.Main()
+--import FrontEnd.Tc.Main()
hunk ./FrontEnd/Tc/Main.hs 25
+import FrontEnd.Tc.Type
hunk ./FrontEnd/Tc/Main.hs 55
+-- TODO should subsume for rank-n
hunk ./FrontEnd/Tc/Main.hs 62
+tiExpr (HsCon conName) typ = do
+      sc <- lookupName (toName DataConstructor conName)
+      ((ps :=> t)) <- freshInst sc
+      unify t typ
+      return ps
+
+tiExpr (HsLit l) typ = do
+    (ps,t) <- tiLit l
+    unify t typ
+    return ps
+
+tiExpr (HsAsPat n e) typ = do
+    --(br,bt) <- newBox
+    ps <- tiExpr e typ
+    --t <- br
+    addToCollectedEnv (Map.singleton (toName Val n) typ)
+    return ps
+
+tiExpr expr@(HsApp e1 e2) typ = withContext (makeMsg "in the application" $ render $ ppHsExp expr) $ do
+    (br,bt) <- newBox
+    ps <- tiExpr e1 (bt `TArrow` typ)
+    t <- br
+    qs <- tiExpr e2 t
+    return (ps ++ qs)
+
+
+
+-- we need to fix the type to to be in the class
+-- cNum, just for cases such as:
+-- foo = \x -> -x
+
+tiExpr expr@(HsNegApp e) typ = withContext (makeMsg "in the negative expression" $ render $ ppHsExp expr) $ do
+        ps <- tiExpr e typ
+        return (IsIn class_Num typ : ps)
+
+tiExpr expr@(HsLambda sloc pats e) typ = withContext (locSimple sloc $ "in the lambda expression\n   \\" ++ show pats ++ " -> ...") $ do
+        ts <- mapM (const newBox) pats
+        (ps, envP) <- tiPats pats ts
+        (br,bt) <- newBox
+        qs <- localEnv envP $ do
+            tiExpr e bt
+        t <- br
+        unify (foldr fn t ts) typ
+        return (ps ++ qs)
+        --(ps, envP, ts) <- tiPats pats
+        --(qs, envE, t)  <- tiExpr (envP `Map.union` env) e
+
+        --return (ps++qs, envP `Map.union` envE, foldr fn t ts)  -- Boba
+
+tiExpr (HsIf e e1 e2) typ = withContext (simpleMsg $ "in the if expression\n   if " ++ show e ++ "...") $ do
+    ps <- tiExpr e tBool
+    qs <- tiExpr e1 typ
+    rs <- tiExpr e2 typ
+    return (ps ++ qs ++ rs)
+
+
+tiExpr (HsParen e) typ = tiExpr e typ
+
+
+
+tiExpr (HsDo stmts) typ = do
+        let newExp = doToExp stmts
+        withContext (simpleMsg "in a do expression")
+                    (tiExpr newExp typ)
+
+tiExpr e typ = error $ "tiExpr: not implemented for: " ++ (show e,show typ)
+
+-- Typing Patterns
+
+--tiPat :: HsPat -> TI ([Pred], Map.Map Name Scheme, Type)
+tiPat :: HsPat -> Type -> Tc ([Pred], Map.Map Name Scheme)
+
+tiPat (HsPVar i) typ = do
+        v <- newTVar Star
+        unify v typ
+        --let newAssump = assumpToPair $ makeAssump i (toScheme v)
+        --let newAssump = (i,toScheme v)
+        return ([], Map.singleton (toName Val i) (toScheme v))
+
+tiPat (HsPLit l) typ = do
+    (ps, t) <- tiLit l
+    unify t typ
+    return (ps, Map.empty)
+
+-- this is for negative literals only
+-- so the pat must be a literal
+-- it is safe not to make any predicates about
+-- the pat, since the type checking of the literal
+-- will do this for us
+tiPat (HsPNeg pat) = tiPat pat
+
+
+tiPat (HsPApp conName pats) = do
+    (ps,env,ts) <- tiPats pats
+    t'         <- newTVar Star
+    sc <- dConScheme (toName DataConstructor conName)
+    (qs :=> t) <- freshInst sc
+    unify t (foldr fn t' ts)
+    return (ps++qs, env, t')
+
+
+tiPat (HsPList []) typ = do
+        v <- newTVar Star
+        unify (TAp tList v) typ
+        return ([], Map.empty)
+
+tiPat (HsPList pats@(_:_)) = do
+        (ps, env, ts@(hts:_)) <- tiPats pats
+        unifyList ts
+        return (ps, env, TAp tList hts)
+
+tiPat HsPWildCard
+ = do v <- newTVar Star
+      return ([], Map.empty, v)
+
+tiPat (HsPAsPat i pat)
+ = do (ps, env, t) <- tiPat pat
+      --let newAssump = makeAssump i $ toScheme t
+      --let newEnv = addToEnv (assumpToPair newAssump) env
+      let newEnv = Map.insert  (toName Val i) (toScheme t) env
+      return (ps, newEnv, t)
+
+tiPat (HsPIrrPat p) = tiPat p
+
+tiPat (HsPParen p) = tiPat p
+
+tiPats :: [HsPat] -> TI ([Pred], Map.Map Name Scheme, [Type])
+tiPats pats =
+  do psEnvts <- mapM tiPat pats
+     let ps = [ p | (ps,_,_) <- psEnvts, p<-ps ]
+         env = Map.unions $ map snd3 psEnvts
+         ts = [ t | (_,_,t) <- psEnvts ]
+     return (ps, env, ts)
+
+     {-
+tiPat (HsPInfixApp pLeft conName pRight) = do
+        (psLeft, envLeft, tLeft)    <- tiPat pLeft
+        (psRight, envRight, tRight) <- tiPat pRight
+        t'                         <- newTVar Star
+        sc <- dConScheme (toName DataConstructor conName)
+        (qs :=> t) <-  freshInst sc
+        unify t (tLeft `fn` (tRight `fn` t'))
+        return (psLeft ++ psRight, envLeft `Map.union` envRight, t')
+
+tiPat tuple@(HsPTuple pats) = do
+        (ps, env, ts) <- tiPats pats
+        return (ps, env, tTTuple ts)
+
+  -}
+
+{-
+
+tiExpr env expr@(HsLet decls e) = withContext (makeMsg "in the let binding" $ render $ ppHsExp expr) $ do
+         sigEnv <- getSigEnv
+         let bgs = getFunDeclsBg sigEnv decls
+         (ps, env1) <- tiSeq tiBindGroup env bgs
+         (qs, env2, t) <- tiExpr (env1 `Map.union` env) e
+         -- keep the let bound type assumptions in the environment
+
+ tiExpr (HsCase e alts) typ = withContext (simpleMsg $ "in the case expression\n   case " ++ show e ++ " of ...") $ do
+        (pse, env1, te)    <- tiExpr env e
+        psastsAlts     <- mapM (tiAlt env) alts
+        let pstsPats = map fst3 psastsAlts
+        let psPats   = concatMap fst pstsPats
+        let tsPats   = map snd pstsPats
+        let pstsEs   = map trd3 psastsAlts
+        let psEs     = concatMap fst pstsEs
+        let tsEs@(htsEs:_)  = map snd pstsEs
+        let envAlts  = Map.unions $ map snd3 psastsAlts
+        unifyList (te:tsPats)
+        unifyList tsEs
+        -- the list of rhs alternatives must be non-empty
+        -- so it is safe to call head here
+        return (pse ++ psPats ++ psEs, env1 `Map.union` envAlts, htsEs)           return (ps ++ qs, env1 `Map.union` env2, t)
+
+{-
+tiExpr expr@(HsInfixApp e1 e2 e3) = withContext (makeMsg "in the infix application" $ render $ ppHsExp expr) $ do
+       (ps, env1, te1) <- tiExpr env e1
+       (qs, env2, te2) <- tiExpr env e2
+       (rs, env3, te3) <- tiExpr env e3
+       tout      <- newTVar Star
+       unify (te1 `fn` (te3 `fn` tout)) te2
+       return (ps ++ qs ++ rs, env1 `Map.union` env2 `Map.union` env3, tout)
+       -}
+
+ -}
+
+
hunk ./FrontEnd/Tc/Main.hs 251
+
hunk ./FrontEnd/Tc/Main.hs 829
--- Typing Literals
-
-tiLit            :: HsLiteral -> TI ([Pred],Type)
-tiLit (HsChar _) = return ([], tChar)
-tiLit (HsInt _)
-   = do
-        v <- newTVar Star
-        return ([IsIn class_Num v], v)
-
-tiLit (HsFrac _)
-   = do
-        v <- newTVar Star
-        return ([IsIn class_Fractional v], v)
-
-tiLit (HsString _)  = return ([], tString)
hunk ./FrontEnd/Tc/Main.hs 917
+-- Typing Literals
+
+tiLit            :: HsLiteral -> Tc ([Pred],Type)
+tiLit (HsChar _) = return ([], tChar)
+tiLit (HsInt _) = do
+        v <- newTVar Star
+        return ([IsIn class_Num v], v)
+
+tiLit (HsFrac _) = do
+        v <- newTVar Star
+        return ([IsIn class_Fractional v], v)
+
+tiLit (HsString _)  = return ([], tString)
+
+
+
hunk ./FrontEnd/Tc/Monad.hs 11
+    newTVar,
+    newBox,
+    withContext,
+    inst,
hunk ./FrontEnd/Tc/Monad.hs 19
+import Control.Monad.Writer
hunk ./FrontEnd/Tc/Monad.hs 53
-newtype Tc a = Tc (ReaderT TcEnv IO a)
-    deriving(MonadFix,MonadIO,MonadReader TcEnv,Functor)
+newtype Tc a = Tc (ReaderT TcEnv (WriterT [Pred] IO) a)
+    deriving(MonadFix,MonadIO,MonadReader TcEnv,MonadWriter [Pred],Functor)
hunk ./FrontEnd/Tc/Monad.hs 83
-    runReaderT tim TcEnv {
+    (a,out) <- runWriterT $ runReaderT tim TcEnv {
hunk ./FrontEnd/Tc/Monad.hs 90
+    return a
hunk ./FrontEnd/Tc/Monad.hs 163
+
+-- | returns a new box and a function to read said box.
+
+newBox :: Tc (Tc Type,Type)
+newBox = do
+    r <- liftIO $ newIORef (error "empty box")
+    return (liftIO $ readIORef r, TBox r)
+
+
hunk ./FrontEnd/Tc/Type.hs 1
+module FrontEnd.Tc.Type where
+
+import Control.Monad.Trans
+import Control.Monad.Writer
+import Data.IORef
+import qualified Data.Map as Map
+
+import Representation
+import FrontEnd.Tc.Monad
+import GenUtil
+
+type Box = IORef Type
+type BoxySigma = Sigma
+
+openBox :: Box -> Tc Type
+openBox x = liftIO $ readIORef x
+
+fillBox :: Box -> Type -> Tc ()
+fillBox x t = liftIO $ writeIORef x t
+
+isTau :: Type -> Bool
+isTau TForAll {} = False
+isTau TBox {} = False
+isTau (TAp a b) = isTau a && isTau b
+isTau (TArrow a b) = isTau a && isTau b
+isTau _ = True
+
+isTau' :: Type -> Bool
+isTau' TForAll {} = False
+isTau' (TAp a b) = isTau a && isTau b
+isTau' (TArrow a b) = isTau a && isTau b
+isTau' _ = True
+
+
+isRho' :: Type -> Bool
+isRho' TForAll {} = False
+isRho' _ = True
+
+subsumes :: BoxySigma -> BoxySigma -> Tc ()
+-- SBOXY
+subsumes (TBox a) b = boxyMatch (TBox a) b
+
+-- SKOL needs to be after SBOXY
+subsumes s1 fa@TForAll {} = do
+    ps :=> r1 <- freshInst fa
+    tell ps
+    s1 `subsumes` r1
+
+-- SPEC
+subsumes (TForAll as (_ :=> r1))  r2 | isRho' r2 = do
+    bs <- mapM (const newBox) as
+    inst (Map.fromList $ zip (map tyvarAtom as) (snds bs)) r1 `subsumes` r2
+
+-- CON (??)
+subsumes s1@TAp {} s2 = s1 `boxyMatch` s2
+
+-- F1
+subsumes (TArrow s1 s2) (TArrow s3 s4) = do
+    boxyMatch s3 s1
+    subsumes s2 s4
+-- F2
+subsumes t@(TArrow _ _) (TBox box) = do
+    (oa,a) <- newBox
+    (ob,b) <- newBox
+    subsumes t (a `fn` b)
+    na <- oa
+    nb <- ob
+    fillBox box (na `fn` nb)
+
+-- BMONO & MONO
+subsumes a b | isTau a = case b of
+    (TBox b) -> fillBox b a
+    _ | a == b -> return ()
+      | isTau b -> unify a b -- TODO verify? fail $ "taus don't match in MONO" ++ show (a,b)
+
+-- -- MONO
+-- subsumes (TCon a) (TCon b) | a == b = return ()
+
+boxyMatch :: BoxySigma -> BoxySigma -> Tc ()
+
+-- BBEQ
+boxyMatch (TBox ba) (TBox bb) = do
+    tt <- newTVar Star -- is star always right?
+    fillBox ba tt
+    fillBox bb tt
+
+-- AEQ1
+boxyMatch (TArrow s1 s2) (TBox box) = do
+    (ra,a) <- newBox
+    (rb,b) <- newBox
+    boxyMatch (s1 `fn` s2) (a `fn` b)
+    x <- ra
+    y <- rb
+    fillBox box (x `fn` y)
+
+-- AEQ2
+boxyMatch (TArrow s1 s2) (TArrow s3 s4) = do
+    boxyMatch s1 s3
+    boxyMatch s2 s4
+
+-- SEQ1 
+--boxyMatch 
+
+-- MEQ1 MEQ2
+boxyMatch a b | isTau a = case b of
+    (TBox b) -> fillBox b a
+    _ | a == b -> return ()
+      | isTau b -> unify a b -- TODO, verify? fail $ "taus don't match in MEQ[12]" ++ show (a,b)
+
+-- SYM (careful!)
+boxyMatch a b = boxyMatch b a
hunk ./FrontEnd/Type.hs 177
+-- boxes on the right are always empty, boxes on the left are full (for now)
+
+mgu' t (TBox box) = do
+    liftIO $ writeIORef box t
+    return nullSubst
hunk ./FrontEnd/Type.hs 203
+mgu' (TBox box) t2 = do
+    t1 <- liftIO $ readIORef box
+    mgu'' t1 t2
+    return nullSubst