[make evaluator not over-apply type constructors, follow more aliases.
John Meacham <john@repetae.net>**20060222135229] hunk ./DataConstructors.hs 307
-followAlias _ e | not (sortTypeLike e) = fail "followAlias: not a type"
+--followAlias _ e | not (sortTypeLike e) = fail "followAlias: not a type"
hunk ./E/Eval.hs 20
+    -- final terms
hunk ./E/Eval.hs 26
-
hunk ./E/Eval.hs 28
+
+    -- argument applications
hunk ./E/Eval.hs 40
+    eval' e@(ELit LitCons {}) stack = unwind e stack
hunk ./E/Eval.hs 51
--- TODO, this should take a set of free variables and α-convert lambdas
-
-unify :: Monad m => E -> E -> m [(E,E)]
-unify e1 e2 = liftM Seq.toList $ execWriterT (un e1 e2 () (-2::Int)) where
-    un _ _ _ c | c `seq` False = undefined
-    un (EAp a b) (EAp a' b') mm c = do
-        un a a' mm c
-        un b b' mm c
-    un a@(EVar (TVr { tvrIdent = i, tvrType =  t}))  b@(EVar (TVr { tvrIdent = j, tvrType =  u})) mm c | i == j || (i > 0 && j > 0) = do
-        un t u mm c
-        when (i /= j) $ tell (Seq.single (a,b))
-    --un (ELam (TVr Nothing ta) ea) (ELam (TVr Nothing tb) eb) mm c = un ta tb mm c >> un ea eb mm c
-    --un (EPi (TVr Nothing ta) ea) (EPi (TVr Nothing tb) eb) mm c = un ta tb mm c >> un ea eb mm c
-    un (ELam va ea) (ELam vb eb) mm c = lam va ea vb eb mm c
-    un (EPi va ea) (EPi vb eb) mm c = lam va ea vb eb mm c
-    un (EPrim s xs t) (EPrim s' ys t') mm c | length xs == length ys = do
-        sequence_ [ un x y mm c | x <- xs | y <- ys]
-        un t t' mm c
-    un (ESort x) (ESort y) mm c | x == y = return ()
-    un (ELit (LitInt x t1))  (ELit (LitInt y t2)) mm c | x == y = un t1 t2 mm c
---    un (ELit (LitChar x))  (ELit (LitChar y)) mm c | x == y = return ()
---    un (ELit (LitFrac x t1 ))  (ELit (LitFrac y t2)) mm c | x == y = un t1 t2 mm c
-    un (ELit (LitCons n xs t))  (ELit (LitCons n' ys t')) mm c | n == n' && length xs == length ys = do
-        sequence_ [ un x y mm c | x <- xs | y <- ys]
-        un t t' mm c
-    un a@EVar {} b _ _ = tell (Seq.single (a,b))
-    --un a b@EVar {} _ _ = tell (Seq.single (a,b))
-    un a b _ _ = fail $ "Expressions do not unify: " ++ show a ++ show b
-    lam va ea vb eb mm c = do
-        un (subst va (EVar va { tvrIdent = c }) ea) (subst vb (EVar vb { tvrIdent = c }) eb) mm (c - 2)
-
-    -- error "cannot handle lambdas yet"
-
-
hunk ./E/Eval.hs 73
-    --eval' ds (ELetRec ds' e) = (Map.fromList ds'
hunk ./E/Eval.hs 90
-    --eval' ds (ELetRec ds' e) stack = eval' ds (f (decomposeDefns ds') e) stack where
-    --    f [] e = e
-    --    f (Left (x,y):ds) e =  subst x y (f ds e)
-    --    f (Right _:_) _ = error $ "cannot eval recursive let"
---    eval' ds (ECase e as) [] = do
---        e' <- eval' ds e []
---        let f (PatLit (LitCons n es t),e) = do
---                e' <- eval' ds e []
---                t' <- eval' ds t []
---                es' <- mapM (\e -> eval' ds e []) es
---                return (PatLit (LitCons n es' t'),e')
---            f (p,e) = do
---                e' <- eval' ds e []
---                return (p,e')
---        as' <- mapM f as
---        return $ ECase e' as'
+    eval' ds e@(ELit LitCons {}) stack = unwind ds e stack
hunk ./E/TypeCheck.hs 31
+typ (EAp (EPi tvr a) b) = getType (subst tvr b a)
hunk ./E/TypeCheck.hs 173
-        e1 <- strong nds t1
-        e2 <- strong nds t2
+        e1 <- strong nds (followAliases dataTable t1)
+        e2 <- strong nds (followAliases dataTable t2)
hunk ./E/TypeCheck.hs 178
-
---        let x
---            --  | e1 == e2 = e1
---              | allShadow e1 == allShadow e2 = return e1
---            --  | e1 == tInt || e2 == tInt = return e1
---              | otherwise = failDoc $ hsep [text "eq:",{- tupled (map pprint $ fsts nds), -} tupled [ prettyE (e1),prettyE (e2) ], tupled [ prettyE (allShadow e1), prettyE (allShadow e2)] {- , tupled [ text (show e1), text (show e2)] -}  ]
---        x
---    -- | Check that the type of e1 is the same as t2 within the given context
hunk ./E/TypeCheck.hs 182
-        --flip (eq' nds) t2 t
-    --eq t1 t2 | Just _ <- E.Eval.unify (smplE t1) (smplE t2) = return (smplE t1)
-    --eq t1 t2 | Just _ <- E.Eval.unify (smplE t2) (smplE t1) = return (smplE t1)
-    --eq t1 t2 | smplE t1 == smplE t2 = return t1
-    --eq t1 t2 | t1 == tInt || t2 == tInt = return t1  --TODO - hack.
-    --eq t1 t2 | Left d <- E.Eval.unify (smplE t1) (smplE t2) = failDoc $ hsep [text "eq:", tupled [text d, prettyE (smplE t1),prettyE (smplE t2) ] ]
-    --eq t1 t2  = failDoc $ hsep [text "eq:", tupled [ prettyE (smplE t1),prettyE (smplE t2) ] ]
-    --valid s | s == eBox = return ()
-    --valid Unknown = fail "valid: Unknown"
-    --valid e = withContextDoc (text "valid:" <+> prettyE e) (rfc e >>= valid)