[update typing rules for core. move some E code around.
John Meacham <john@repetae.net>**20060222122258] hunk ./E/E.hs 337
+-- the IOErrorCont type from Jhc.IO
+tCont = ltTuple [ELit $ LitCons tc_JumpPoint [] eStar, ELit $ LitCons tc_IOError [] eStar]
+tvrCont = tvr { tvrIdent = 0, tvrType = tCont }
+
+ltTuple ts = ELit $ LitCons (nameTuple TypeConstructor (length ts)) ts eStar
+ltTuple' ts = ELit $ LitCons (unboxedNameTuple TypeConstructor (length ts)) ts eHash
hunk ./E/E.hs 346
+p_toTag = primPrim "toTag"
+p_fromTag = primPrim "fromTag"
hunk ./E/Eval.hs 1
-module E.Eval(eval, unify,strong) where
+module E.Eval(eval, strong) where
hunk ./E/Eval.hs 28
-    eval' (ELit (LitCons n es ty)) (t:rest) = eval' (ELit $ LitCons n (es ++ [t]) (eval $ EAp ty t)) rest
+    eval' (ELit (LitCons n es ty@EPi {})) (t:rest) = eval' (ELit $ LitCons n (es ++ [t]) (eval $ EAp ty t)) rest
hunk ./E/Eval.hs 110
-    eval' ds (ELit (LitCons n es ty)) (t:rest) = do
+    eval' ds (ELit (LitCons n es ty@EPi {})) (t:rest) = do
hunk ./E/SSimplify.hs 85
-        let fvs = mconcat $ [fva,freeVars $ tvrType b, fvb] ++ fvas
+        let fvs = mconcat $ [fva,freeVars $ eCaseType ec, freeVars $ tvrType b, fvb] ++ fvas
hunk ./E/Show.hs 134
+        f e | e == tCont     = return $ atom $ text "IOErrorCont"
hunk ./E/Show.hs 161
-        f (ESort EStar) = return $ symbol UC.star
+        f (ESort EStar) = return $ symbol (text "*")
hunk ./E/Subst.hs 78
-    f (EAp a b) = liftM2 EAp (f a) (f b)
+    f (EAp a b) = liftM2 eAp (f a) (f b)
hunk ./E/Subst.hs 160
-eAp (ELit (LitCons n es t)) b = (ELit (LitCons n (es ++ [b]) (eAp t b)))
+eAp (ELit (LitCons n es (EPi t r))) b = ELit (LitCons n (es ++ [b]) (subst t b r))
hunk ./E/Subst.hs 196
-    f (EAp a b) = liftM2 EAp (f a) (f b)
+    f (EAp a b) = liftM2 eAp (f a) (f b)
hunk ./E/TypeCheck.hs 6
+import Control.Monad.Reader
hunk ./E/TypeCheck.hs 60
+simplifyAp :: Monad m => DataTable -> E -> E -> m E
+simplifyAp dataTable (EAp a b) c = do
+    na <- simplifyAp dataTable a b
+    simplifyAp dataTable na c
+simplifyAp _ (ELit (LitCons n xs (EPi tvr r))) b = do
+        return (ELit (LitCons n (xs ++ [b]) (subst tvr b r)))
+simplifyAp dataTable a@ELit {} b = case followAliases dataTable a  of
+        ELit {} -> fail $ "simplifyAp: " ++ render (tupled [ePretty a, ePretty b])
+        (EPi tvr e) -> do
+                return (subst tvr b e)
+simplifyAp _ a b = fail $ "simplifyAp: " ++ render (tupled [ePretty a, ePretty b])
+
hunk ./E/TypeCheck.hs 81
-    rfc e =  withContextDoc (text "fullCheck:" </> prettyE e) (fc e >>=  strong')
-    rfc' nds e =  withContextDoc (text "fullCheck':" </> prettyE e) (inferType' nds  e >>=  strong')
-    strong' e = withContextDoc (text "Strong:" </> prettyE e) $ strong ds e
+    rfc e =  withContextDoc (text "fullCheck:" </> prettyE e) (fc (followAliases dataTable e) >>=  strong')
+    rfc' nds e = withContextDoc (text "fullCheck:" </> prettyE e) (inferType' nds (followAliases dataTable e) >>=  strong')
+    strong' e = withContextDoc (text "Strong:" </> prettyE e) $ strong ds (followAliases dataTable e)
hunk ./E/TypeCheck.hs 95
-    --fc (EAp (EPi tvr e) b) = rfc (subst tvr b e)
+    fc (EAp (EPi tvr e) b) = rfc (subst tvr b e)
hunk ./E/TypeCheck.hs 97
-        a' <- rfc a
+        withContextDoc (text "EAp:" </> parens (prettyE a) </> parens (prettyE b)) $ do
+            a' <- rfc a
+            return $ eAp (followAliases dataTable a') b
+        {-
hunk ./E/TypeCheck.hs 109
-            x -> fail $ "App: " ++ render (tupled [ePretty x,ePretty a, ePretty b])
+            x -> fail $ "App: " ++ render (tupled [ePretty x,ePretty a, ePretty a', ePretty b])
+            -}
hunk ./E/TypeCheck.hs 164
-
-
-    {-
-    fc (ECase _ []) = fail "Case with no alternatives"
-    -- when checking typecases, we must check that the specialization of the default case matches each of the other alternatives.
-    fc (ECase e alts) | sortTypeLike e = rfc e >>= \et -> mapM (cp et) alts >>= \as ->  return (last as) where
-        cp et (PatLit l,e) = do
-            withContextDoc (hsep [text "Case Pattern: ", parens $ prettyE et, parens $ prettyE (ELit l)]) $ eq et (getType  l)
-            e' <- rfc e
-            return (discardArgs (length es) e') where -- TODO - check these.
-                es = case l of (LitCons _ es _) -> es ; _ -> []
-        cp _ (PatWildCard,e') = rfc (eAp e' e)
-    fc (ECase e alts) = rfc e >>= \et -> mapM (cp et) alts >>= \as@(a:_) -> eqAll  as >> return a where
-        cp et (PatLit l,e) = do
-            withContextDoc (hsep [text "Case Pattern: ", parens $ prettyE et, parens $ prettyE (ELit l)]) $ eq et (getType l)
-            e' <- rfc e
-            return (discardArgs (length es) e')  where -- TODO - check these.
-                es = case l of (LitCons _ es _) -> es ; _ -> []
-        cp _ (PatWildCard,e') = rfc (eAp e' e)
-    -}
hunk ./E/TypeCheck.hs 234
+data TcEnv = TcEnv {
+    tcContext :: [String],
+    tcDataTable :: DataTable
+    }
+   {-! derive: update !-}
+
+newtype Tc a = Tc (Reader TcEnv a)
+    deriving(Monad,Functor,MonadReader TcEnv)
+
+instance ContextMonad String Tc where
+    withContext s = local (tcContext_u (s:))
+
+--tcE :: E -> Tc E
+--tcE e = rfc e where
+
hunk ./E/TypeCheck.hs 253
-    rfc e =  withContextDoc (text "fullCheck:" </> prettyE e) (fc e >>=  strong')
-    rfc' nds e =  withContextDoc (text "fullCheck:" </> prettyE e) (inferType' nds  e >>=  strong')
-    strong' e = withContextDoc (text "Strong:" </> prettyE e) $ strong ds e
-    fc s@(ESort _) = return $ typ s
-    fc (ELit (LitCons _ es t)) = (strong' t)
-    fc e@(ELit _) = strong' (typ e)
-    fc (EVar (TVr { tvrIdent = 0 })) = fail "variable with nothing!"
-    fc (EVar (TVr { tvrType =  t})) =  strong' t
-    fc (EPi (TVr { tvrIdent = n, tvrType = at}) b) =  rfc' [ d | d@(v,_) <- ds, tvrNum v /= n ] b
-    fc (ELam tvr@(TVr { tvrIdent = n, tvrType =  at}) b) = do
+    rfc e =  withContextDoc (text "fullCheck':" </> prettyE e) (fc (followAliases dataTable e) >>=  strong')
+    rfc' nds e =  withContextDoc (text "fullCheck':" </> prettyE e) (inferType' nds  (followAliases dataTable e) >>=  strong')
+    strong' e = withContextDoc (text "Strong':" </> prettyE e) $ strong ds (followAliases dataTable e)
+    fc s@ESort {} = return $ getType s
+    fc (ELit (LitCons _ es t)) = strong' t
+    fc e@ELit {} = strong' (getType e)
+    fc (EVar TVr { tvrIdent = 0 }) = fail "variable with nothing!"
+    fc (EVar TVr { tvrType =  t}) =  strong' t
+    fc (EPi TVr { tvrIdent = n, tvrType = at} b) =  rfc' [ d | d@(v,_) <- ds, tvrNum v /= n ] b
+    fc (ELam tvr@TVr { tvrIdent = n, tvrType =  at} b) = do
hunk ./E/TypeCheck.hs 266
-    --fc (EAp (EPi tvr e) b) = rfc (subst tvr b e)
+    fc (EAp (EPi tvr e) b) = do
+        b <- strong' b
+        rfc (subst tvr b e)
hunk ./E/TypeCheck.hs 271
+        strong' (eAp (followAliases dataTable a') b)
+        {-
hunk ./E/TypeCheck.hs 278
-            x -> fail $ "App: " ++ render (tupled [ePretty x,ePretty a, ePretty b])
+            x -> fail $ "App: " ++ render (tupled [ePretty x,ePretty a, ePretty a',ePretty b])
+            -}
hunk ./E/TypeCheck.hs 284
-    fc (EError _ e) = (strong'  e)
-    fc (EPrim _ ts t) = ( strong' t)
+    fc (EError _ e) = strong' e
+    fc (EPrim _ ts t) = strong' t
hunk ./E/TypeCheck.hs 290
-        --bs <- mapM rfc (caseBodies ec)
-        --return (head bs)
hunk ./E/Values.hs 38
-ltTuple ts = ELit $ LitCons (nameTuple TypeConstructor (length ts)) ts eStar
-ltTuple' ts = ELit $ LitCons (unboxedNameTuple TypeConstructor (length ts)) ts eHash
hunk ./E/Values.hs 43
--- the IOErrorCont type from Jhc.IO
-tCont = ltTuple [ELit $ LitCons tc_JumpPoint [] eStar, ELit $ LitCons tc_IOError [] eStar]
-tvrCont = tvr { tvrIdent = 0, tvrType = tCont }
hunk ./E/Values.hs 185
-    f e = EPrim (primPrim "toTag") [e] tTag
+    f e = EPrim p_toTag [e] tTag